From 07013da720e1841fc06ea865906685332a50c919 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 24 Aug 2024 17:10:07 +1000 Subject: [PATCH] chore: running the simpNF linter over Lean (#5133) This should resolve nearly all of the simpNF lints. This is a follow-up to #4620. --- src/Init/Data/BitVec/Lemmas.lean | 9 ++--- src/Init/Data/List/Basic.lean | 7 ++-- src/Init/Data/List/BasicAux.lean | 2 +- src/Init/Data/List/Find.lean | 3 +- src/Init/Data/List/Lemmas.lean | 33 +++++++++---------- src/Init/Data/List/Perm.lean | 2 -- src/Init/Data/List/TakeDrop.lean | 4 +-- src/Init/Data/Nat/Basic.lean | 2 +- src/Init/SimpLemmas.lean | 2 +- .../DHashMap/Internal/List/Associative.lean | 2 ++ 10 files changed, 30 insertions(+), 36 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 59c89b0105..77bb33ebbc 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -413,11 +413,9 @@ theorem msb_truncate (x : BitVec w) : (x.truncate (k + 1)).msb = x.getLsb k := b (x.truncate l).truncate k = x.truncate k := zeroExtend_zeroExtend_of_le x h -/--Truncating by the bitwidth has no effect. -/ -@[simp] -theorem truncate_eq_self {x : BitVec w} : x.truncate w = x := by - ext i - simp [getLsb_zeroExtend] +/-- Truncating by the bitwidth has no effect. -/ +-- This doesn't need to be a `@[simp]` lemma, as `zeroExtend_eq` applies. +theorem truncate_eq_self {x : BitVec w} : x.truncate w = x := zeroExtend_eq _ @[simp] theorem truncate_cast {h : w = v} : (cast h x).truncate k = x.truncate k := by apply eq_of_getLsb_eq @@ -776,7 +774,6 @@ theorem shiftLeft_shiftLeft {w : Nat} (x : BitVec w) (n m : Nat) : @[simp] theorem shiftLeft_eq' {x : BitVec w₁} {y : BitVec w₂} : x <<< y = x <<< y.toNat := by rfl -@[simp] theorem shiftLeft_zero' {x : BitVec w₁} : x <<< 0#w₂ = x := by simp theorem shiftLeft_shiftLeft' {x : BitVec w₁} {y : BitVec w₂} {z : BitVec w₃} : diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index cdefad5646..c60845772b 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -96,7 +96,7 @@ namespace List /-! ### concat -/ -@[simp high] theorem length_concat (as : List α) (a : α) : (concat as a).length = as.length + 1 := by +theorem length_concat (as : List α) (a : α) : (concat as a).length = as.length + 1 := by induction as with | nil => rfl | cons _ xs ih => simp [concat, ih] @@ -278,8 +278,9 @@ def getLastD : (as : List α) → (fallback : α) → α | [], a₀ => a₀ | a::as, _ => getLast (a::as) (fun h => List.noConfusion h) -@[simp] theorem getLastD_nil (a) : @getLastD α [] a = a := rfl -@[simp] theorem getLastD_cons (a b l) : @getLastD α (b::l) a = getLastD l b := by cases l <;> rfl +-- These aren't `simp` lemmas since we always simplify `getLastD` in terms of `getLast?`. +theorem getLastD_nil (a) : @getLastD α [] a = a := rfl +theorem getLastD_cons (a b l) : @getLastD α (b::l) a = getLastD l b := by cases l <;> rfl /-! ## Head and tail -/ diff --git a/src/Init/Data/List/BasicAux.lean b/src/Init/Data/List/BasicAux.lean index e37af41afe..b33b57495d 100644 --- a/src/Init/Data/List/BasicAux.lean +++ b/src/Init/Data/List/BasicAux.lean @@ -222,7 +222,7 @@ theorem append_cancel_right {as bs cs : List α} (h : as ++ bs = cs ++ bs) : as next => apply append_cancel_right next => intro h; simp [h] -@[simp] theorem sizeOf_get [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.get i) < sizeOf as := by +theorem sizeOf_get [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.get i) < sizeOf as := by match as, i with | a::as, ⟨0, _⟩ => simp_arith [get] | a::as, ⟨i+1, h⟩ => diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean index 35d8b60ca6..a9f1a33875 100644 --- a/src/Init/Data/List/Find.lean +++ b/src/Init/Data/List/Find.lean @@ -298,7 +298,8 @@ theorem find?_replicate : find? p (replicate n a) = if n = 0 then none else if p @[simp] theorem find?_replicate_of_neg (h : ¬ p a) : find? p (replicate n a) = none := by simp [find?_replicate, h] -@[simp] theorem find?_replicate_eq_none (n : Nat) (a : α) (p : α → Bool) : +-- This isn't a `@[simp]` lemma since there is already a lemma for `l.find? p = none` for any `l`. +theorem find?_replicate_eq_none (n : Nat) (a : α) (p : α → Bool) : (replicate n a).find? p = none ↔ n = 0 ∨ !p a := by simp [Classical.or_iff_not_imp_left] diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 5c9eacec6a..108c16ba73 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -379,19 +379,15 @@ theorem forall_mem_ne {a : α} {l : List α} : (∀ a' : α, a' ∈ l → ¬a = theorem forall_mem_ne' {a : α} {l : List α} : (∀ a' : α, a' ∈ l → ¬a' = a) ↔ a ∉ l := ⟨fun h m => h _ m rfl, fun h _ m e => h (e.symm ▸ m)⟩ -@[simp] theorem any_beq [BEq α] [LawfulBEq α] {l : List α} : (l.any fun x => a == x) ↔ a ∈ l := by induction l <;> simp_all -@[simp] theorem any_beq' [BEq α] [LawfulBEq α] {l : List α} : (l.any fun x => x == a) ↔ a ∈ l := by induction l <;> simp_all [eq_comm (a := a)] -@[simp] theorem all_bne [BEq α] [LawfulBEq α] {l : List α} : (l.all fun x => a != x) ↔ a ∉ l := by induction l <;> simp_all -@[simp] theorem all_bne' [BEq α] [LawfulBEq α] {l : List α} : (l.all fun x => x != a) ↔ a ∉ l := by induction l <;> simp_all [eq_comm (a := a)] @@ -515,7 +511,7 @@ theorem isEmpty_iff_length_eq_zero {l : List α} : l.isEmpty ↔ l.length = 0 := @[simp] theorem isEmpty_eq_true {l : List α} : l.isEmpty ↔ l = [] := by cases l <;> simp -@[simp] theorem isEmpty_eq_false {l : List α} : ¬ l.isEmpty ↔ l ≠ [] := by +@[simp] theorem isEmpty_eq_false {l : List α} : l.isEmpty = false ↔ l ≠ [] := by cases l <;> simp /-! ### any / all -/ @@ -555,7 +551,7 @@ theorem get_set_eq {l : List α} {i : Nat} {a : α} (h : i < (l.set i a).length) simp_all [getElem?_eq_some] @[simp] -theorem getElem?_set_eq' {l : List α} {i : Nat} {a : α} : (set l i a)[i]? = (fun _ => a) <$> l[i]? := by +theorem getElem?_set_eq' {l : List α} {i : Nat} {a : α} : (set l i a)[i]? = Function.const _ a <$> l[i]? := by by_cases h : i < l.length · simp [getElem?_set_eq h, getElem?_eq_getElem h] · simp only [Nat.not_lt] at h @@ -612,7 +608,7 @@ theorem getElem?_set {l : List α} {i j : Nat} {a : α} : theorem getElem?_set' {l : List α} {i j : Nat} {a : α} : (set l i a)[j]? = if i = j then (fun _ => a) <$> l[j]? else l[j]? := by by_cases i = j - · simp only [getElem?_set_eq', Option.map_eq_map, ↓reduceIte, *] + · simp only [getElem?_set_eq', Option.map_eq_map, ↓reduceIte, *]; rfl · simp only [ne_eq, not_false_eq_true, getElem?_set_ne, ↓reduceIte, *] theorem set_eq_of_length_le {l : List α} {n : Nat} (h : l.length ≤ n) {a : α} : @@ -892,7 +888,7 @@ theorem getLast?_eq_get? (l : List α) : getLast? l = l.get? (l.length - 1) := b @[simp] theorem getLast?_concat (l : List α) : getLast? (l ++ [a]) = some a := by simp [getLast?_eq_getElem?, Nat.succ_sub_succ] -@[simp] theorem getLastD_concat (a b l) : @getLastD α (l ++ [b]) a = b := by +theorem getLastD_concat (a b l) : @getLastD α (l ++ [b]) a = b := by rw [getLastD_eq_getLast?, getLast?_concat]; rfl /-! ## Head and tail -/ @@ -1504,9 +1500,9 @@ theorem getElem?_append {l₁ l₂ : List α} {n : Nat} : · exact getElem?_append_left h · exact getElem?_append_right (by simpa using h) -@[simp] theorem head_append_of_ne_nil {l : List α} (w : l ≠ []) : - head (l ++ l') (by simp_all) = head l w := by - match l, w with +@[simp] theorem head_append_of_ne_nil {l : List α} {w₁} (w₂) : + head (l ++ l') w₁ = head l w₂ := by + match l, w₂ with | a :: l, _ => rfl theorem head_append {l₁ l₂ : List α} (w : l₁ ++ l₂ ≠ []) : @@ -2135,18 +2131,19 @@ theorem bind_replicate {β} (f : α → List β) : (replicate n a).bind f = (rep | nil => rfl | cons a as ih => simp [ih] -@[simp] theorem mem_reverseAux {x : α} : ∀ {as bs}, x ∈ reverseAux as bs ↔ x ∈ as ∨ x ∈ bs +theorem mem_reverseAux {x : α} : ∀ {as bs}, x ∈ reverseAux as bs ↔ x ∈ as ∨ x ∈ bs | [], _ => ⟨.inr, fun | .inr h => h⟩ | a :: _, _ => by rw [reverseAux, mem_cons, or_assoc, or_left_comm, mem_reverseAux, mem_cons] -@[simp] theorem mem_reverse {x : α} {as : List α} : x ∈ reverse as ↔ x ∈ as := by simp [reverse] +@[simp] theorem mem_reverse {x : α} {as : List α} : x ∈ reverse as ↔ x ∈ as := by + simp [reverse, mem_reverseAux] @[simp] theorem reverse_eq_nil_iff {xs : List α} : xs.reverse = [] ↔ xs = [] := by match xs with | [] => simp | x :: xs => simp -@[simp] theorem reverse_ne_nil_iff {xs : List α} : xs.reverse ≠ [] ↔ xs ≠ [] := +theorem reverse_ne_nil_iff {xs : List α} : xs.reverse ≠ [] ↔ xs ≠ [] := not_congr reverse_eq_nil_iff theorem getElem?_reverse' : ∀ {l : List α} (i j), i + j + 1 = length l → @@ -2290,8 +2287,8 @@ theorem head_eq_getLast_reverse {l : List α} (h : l ≠ []) : l.head h = l.reverse.getLast (by simp_all) := by rw [← getLast_reverse] -@[simp] theorem getLast_append_of_ne_nil {l : List α} (h : l' ≠ []) : - (l ++ l').getLast (append_ne_nil_of_right_ne_nil l h) = l'.getLast (by simp_all) := by +@[simp] theorem getLast_append_of_ne_nil {l : List α} {h₁} (h₂ : l' ≠ []) : + (l ++ l').getLast h₁ = l'.getLast h₂ := by simp only [getLast_eq_head_reverse, reverse_append] rw [head_append_of_ne_nil] @@ -2463,8 +2460,8 @@ theorem dropLast_append {l₁ l₂ : List α} : (l₁ ++ l₂).dropLast = if l₂.isEmpty then l₁.dropLast else l₁ ++ l₂.dropLast := by split <;> simp_all -@[simp] theorem dropLast_append_cons : dropLast (l₁ ++ b::l₂) = l₁ ++ dropLast (b::l₂) := by - simp only [ne_eq, not_false_eq_true, dropLast_append_of_ne_nil] +theorem dropLast_append_cons : dropLast (l₁ ++ b::l₂) = l₁ ++ dropLast (b::l₂) := by + simp @[simp 1100] theorem dropLast_concat : dropLast (l₁ ++ [b]) = l₁ := by simp diff --git a/src/Init/Data/List/Perm.lean b/src/Init/Data/List/Perm.lean index 3d2019673c..5691056973 100644 --- a/src/Init/Data/List/Perm.lean +++ b/src/Init/Data/List/Perm.lean @@ -123,10 +123,8 @@ theorem Perm.nil_eq {l : List α} (p : [] ~ l) : [] = l := p.symm.eq_nil.symm @[simp] theorem nil_perm {l₁ : List α} : [] ~ l₁ ↔ l₁ = [] := perm_comm.trans perm_nil -@[simp] theorem not_perm_nil_cons (x : α) (l : List α) : ¬[] ~ x :: l := (nomatch ·.symm.eq_nil) -@[simp] theorem not_perm_cons_nil {l : List α} {a : α} : ¬(Perm (a::l) []) := fun h => by simpa using h.length_eq diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean index 8499ecbb24..468b179333 100644 --- a/src/Init/Data/List/TakeDrop.lean +++ b/src/Init/Data/List/TakeDrop.lean @@ -95,9 +95,7 @@ theorem getElem?_take_of_lt {l : List α} {n m : Nat} (h : m < n) : (l.take n)[m theorem get?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n).get? m = l.get? m := by simp [getElem?_take_of_lt, h] -@[simp] -theorem getElem?_take_of_succ {l : List α} {n : Nat} : (l.take (n + 1))[n]? = l[n]? := - getElem?_take_of_lt (Nat.lt_succ_self n) +theorem getElem?_take_of_succ {l : List α} {n : Nat} : (l.take (n + 1))[n]? = l[n]? := by simp @[simp] theorem drop_drop (n : Nat) : ∀ (m) (l : List α), drop n (drop m l) = drop (n + m) l | m, [] => by simp diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean index 01a12c9dde..2b57dac0d5 100644 --- a/src/Init/Data/Nat/Basic.lean +++ b/src/Init/Data/Nat/Basic.lean @@ -158,7 +158,7 @@ theorem add_one (n : Nat) : n + 1 = succ n := rfl @[simp] theorem add_one_ne_zero (n : Nat) : n + 1 ≠ 0 := nofun -@[simp] theorem zero_ne_add_one (n : Nat) : 0 ≠ n + 1 := nofun +theorem zero_ne_add_one (n : Nat) : 0 ≠ n + 1 := by simp protected theorem add_comm : ∀ (n m : Nat), n + m = m + n | n, 0 => Eq.symm (Nat.zero_add n) diff --git a/src/Init/SimpLemmas.lean b/src/Init/SimpLemmas.lean index aad9ac67a3..38acaa073e 100644 --- a/src/Init/SimpLemmas.lean +++ b/src/Init/SimpLemmas.lean @@ -244,7 +244,7 @@ instance : Std.Associative (· || ·) := ⟨Bool.or_assoc⟩ @[simp] theorem decide_not [g : Decidable p] [h : Decidable (Not p)] : decide (Not p) = !(decide p) := by cases g <;> (rename_i gp; simp [gp]; rfl) -@[simp] theorem not_decide_eq_true [h : Decidable p] : ((!decide p) = true) = ¬ p := by simp +theorem not_decide_eq_true [h : Decidable p] : ((!decide p) = true) = ¬ p := by simp @[simp] theorem heq_eq_eq (a b : α) : HEq a b = (a = b) := propext <| Iff.intro eq_of_heq heq_of_eq diff --git a/src/Std/Data/DHashMap/Internal/List/Associative.lean b/src/Std/Data/DHashMap/Internal/List/Associative.lean index c829b607fa..2aa1ce2d13 100644 --- a/src/Std/Data/DHashMap/Internal/List/Associative.lean +++ b/src/Std/Data/DHashMap/Internal/List/Associative.lean @@ -26,6 +26,8 @@ open List (Perm) namespace Std.DHashMap.Internal.List +attribute [-simp] List.isEmpty_eq_false + @[elab_as_elim] theorem assoc_induction {motive : List ((a : α) × β a) → Prop} (nil : motive []) (cons : (k : α) → (v : β k) → (tail : List ((a : α) × β a)) →