From db354d2cde0ce788ec284f17cd86b2862864ae13 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 13 Dec 2024 12:28:53 +1100 Subject: [PATCH] chore: run Batteries linter on Lean (#6364) This PR makes fixes suggested by the Batteries environment linters, particularly `simpNF`, and `unusedHavesSuffices`. --- src/Init/Control/Lawful/Basic.lean | 4 +- src/Init/Data/Array/Attach.lean | 6 +- src/Init/Data/Array/Basic.lean | 5 +- src/Init/Data/Array/BasicAux.lean | 6 +- src/Init/Data/Array/Bootstrap.lean | 9 ++- src/Init/Data/Array/DecidableEq.lean | 2 +- src/Init/Data/Array/Lemmas.lean | 55 +++++--------- src/Init/Data/BitVec/Lemmas.lean | 74 ++++++------------- src/Init/Data/Bool.lean | 4 +- src/Init/Data/Fin/Lemmas.lean | 4 +- src/Init/Data/List/Attach.lean | 6 +- src/Init/Data/List/Find.lean | 1 - src/Init/Data/List/Lemmas.lean | 4 +- src/Init/Data/List/Nat/Modify.lean | 6 +- src/Init/Data/List/Sort/Impl.lean | 10 +-- src/Init/Data/List/Sort/Lemmas.lean | 2 - src/Init/Data/List/ToArray.lean | 2 +- src/Init/Data/Option/Attach.lean | 8 +- src/Init/Data/Sum/Lemmas.lean | 2 +- src/Init/GetElem.lean | 7 +- src/Init/SimpLemmas.lean | 1 + src/Std/Data/DHashMap/Internal/RawLemmas.lean | 4 +- src/Std/Data/DHashMap/Lemmas.lean | 14 ++-- src/Std/Data/HashMap/Lemmas.lean | 9 +-- src/Std/Data/HashSet/Lemmas.lean | 9 +-- .../LRAT/Internal/Formula/Lemmas.lean | 6 +- .../LRAT/Internal/Formula/RupAddResult.lean | 14 ++-- tests/lean/run/array_simp.lean | 3 + 28 files changed, 111 insertions(+), 166 deletions(-) diff --git a/src/Init/Control/Lawful/Basic.lean b/src/Init/Control/Lawful/Basic.lean index a42c6e45bcd0..b457183645e0 100644 --- a/src/Init/Control/Lawful/Basic.lean +++ b/src/Init/Control/Lawful/Basic.lean @@ -106,7 +106,7 @@ theorem seq_eq_bind_map {α β : Type u} [Monad m] [LawfulMonad m] (f : m (α theorem bind_congr [Bind m] {x : m α} {f g : α → m β} (h : ∀ a, f a = g a) : x >>= f = x >>= g := by simp [funext h] -@[simp] theorem bind_pure_unit [Monad m] [LawfulMonad m] {x : m PUnit} : (x >>= fun _ => pure ⟨⟩) = x := by +theorem bind_pure_unit [Monad m] [LawfulMonad m] {x : m PUnit} : (x >>= fun _ => pure ⟨⟩) = x := by rw [bind_pure] theorem map_congr [Functor m] {x : m α} {f g : α → β} (h : ∀ a, f a = g a) : (f <$> x : m β) = g <$> x := by @@ -133,7 +133,7 @@ theorem seqLeft_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x <* y rw [← bind_pure_comp] simp only [bind_assoc, pure_bind] -@[simp] theorem Functor.map_unit [Monad m] [LawfulMonad m] {a : m PUnit} : (fun _ => PUnit.unit) <$> a = a := by +theorem Functor.map_unit [Monad m] [LawfulMonad m] {a : m PUnit} : (fun _ => PUnit.unit) <$> a = a := by simp [map] /-- diff --git a/src/Init/Data/Array/Attach.lean b/src/Init/Data/Array/Attach.lean index a1f0b787c37f..3e87b0aeec7c 100644 --- a/src/Init/Data/Array/Attach.lean +++ b/src/Init/Data/Array/Attach.lean @@ -150,7 +150,6 @@ theorem attach_map_coe (l : Array α) (f : α → β) : theorem attach_map_val (l : Array α) (f : α → β) : (l.attach.map fun i => f i.val) = l.map f := attach_map_coe _ _ -@[simp] theorem attach_map_subtype_val (l : Array α) : l.attach.map Subtype.val = l := by cases l; simp @@ -162,7 +161,6 @@ theorem attachWith_map_val {p : α → Prop} (f : α → β) (l : Array α) (H : ((l.attachWith p H).map fun i => f i.val) = l.map f := attachWith_map_coe _ _ _ -@[simp] theorem attachWith_map_subtype_val {p : α → Prop} (l : Array α) (H : ∀ a ∈ l, p a) : (l.attachWith p H).map Subtype.val = l := by cases l; simp @@ -204,8 +202,8 @@ theorem pmap_ne_empty_iff {P : α → Prop} (f : (a : α) → P a → β) {xs : (H : ∀ (a : α), a ∈ xs → P a) : xs.pmap f H ≠ #[] ↔ xs ≠ #[] := by cases xs; simp -theorem pmap_eq_self {l : Array α} {p : α → Prop} (hp : ∀ (a : α), a ∈ l → p a) - (f : (a : α) → p a → α) : l.pmap f hp = l ↔ ∀ a (h : a ∈ l), f a (hp a h) = a := by +theorem pmap_eq_self {l : Array α} {p : α → Prop} {hp : ∀ (a : α), a ∈ l → p a} + {f : (a : α) → p a → α} : l.pmap f hp = l ↔ ∀ a (h : a ∈ l), f a (hp a h) = a := by cases l; simp [List.pmap_eq_self] @[simp] diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 75e27fa48d77..77efa5a68d40 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -79,7 +79,8 @@ theorem ext' {as bs : Array α} (h : as.toList = bs.toList) : as = bs := by @[simp] theorem toArrayAux_eq (as : List α) (acc : Array α) : (as.toArrayAux acc).toList = acc.toList ++ as := by induction as generalizing acc <;> simp [*, List.toArrayAux, Array.push, List.append_assoc, List.concat_eq_append] -@[simp] theorem toList_toArray (as : List α) : as.toArray.toList = as := rfl +-- This does not need to be a simp lemma, as already after the `whnfR` the right hand side is `as`. +theorem toList_toArray (as : List α) : as.toArray.toList = as := rfl @[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size] @@ -208,7 +209,7 @@ instance : EmptyCollection (Array α) := ⟨Array.empty⟩ instance : Inhabited (Array α) where default := Array.empty -@[simp] def isEmpty (a : Array α) : Bool := +def isEmpty (a : Array α) : Bool := a.size = 0 @[specialize] diff --git a/src/Init/Data/Array/BasicAux.lean b/src/Init/Data/Array/BasicAux.lean index 846183b5ab96..e98b054cb296 100644 --- a/src/Init/Data/Array/BasicAux.lean +++ b/src/Init/Data/Array/BasicAux.lean @@ -32,10 +32,8 @@ private theorem List.of_toArrayAux_eq_toArrayAux {as bs : List α} {cs ds : Arra have := Array.of_push_eq_push ih₂ simp [this] -@[simp] theorem List.toArray_eq_toArray_eq (as bs : List α) : (as.toArray = bs.toArray) = (as = bs) := by - apply propext; apply Iff.intro - · intro h; simpa [toArray] using h - · intro h; rw [h] +theorem List.toArray_eq_toArray_eq (as bs : List α) : (as.toArray = bs.toArray) = (as = bs) := by + simp def Array.mapM' [Monad m] (f : α → m β) (as : Array α) : m { bs : Array β // bs.size = as.size } := go 0 ⟨mkEmpty as.size, rfl⟩ (by simp) diff --git a/src/Init/Data/Array/Bootstrap.lean b/src/Init/Data/Array/Bootstrap.lean index 004f4e2c48c9..e039b4512961 100644 --- a/src/Init/Data/Array/Bootstrap.lean +++ b/src/Init/Data/Array/Bootstrap.lean @@ -93,11 +93,14 @@ theorem foldrM_eq_reverse_foldlM_toList [Monad m] (f : α → β → m β) (init @[simp] theorem appendList_eq_append (arr : Array α) (l : List α) : arr.appendList l = arr ++ l := rfl -@[simp] theorem appendList_toList (arr : Array α) (l : List α) : +@[simp] theorem toList_appendList (arr : Array α) (l : List α) : (arr ++ l).toList = arr.toList ++ l := by rw [← appendList_eq_append]; unfold Array.appendList induction l generalizing arr <;> simp [*] +@[deprecated toList_appendList (since := "2024-12-11")] +abbrev appendList_toList := @toList_appendList + @[deprecated "Use the reverse direction of `foldrM_toList`." (since := "2024-11-13")] theorem foldrM_eq_foldrM_toList [Monad m] (f : α → β → m β) (init : β) (arr : Array α) : @@ -149,7 +152,7 @@ abbrev pop_data := @pop_toList @[deprecated toList_append (since := "2024-09-09")] abbrev append_data := @toList_append -@[deprecated appendList_toList (since := "2024-09-09")] -abbrev appendList_data := @appendList_toList +@[deprecated toList_appendList (since := "2024-09-09")] +abbrev appendList_data := @toList_appendList end Array diff --git a/src/Init/Data/Array/DecidableEq.lean b/src/Init/Data/Array/DecidableEq.lean index be545d6e13eb..d55799b08848 100644 --- a/src/Init/Data/Array/DecidableEq.lean +++ b/src/Init/Data/Array/DecidableEq.lean @@ -42,7 +42,7 @@ theorem rel_of_isEqv {r : α → α → Bool} {a b : Array α} : · exact fun h' => ⟨h, fun i => rel_of_isEqvAux h (Nat.le_refl ..) h'⟩ · intro; contradiction -theorem isEqv_iff_rel (a b : Array α) (r) : +theorem isEqv_iff_rel {a b : Array α} {r} : Array.isEqv a b r ↔ ∃ h : a.size = b.size, ∀ (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h ▸ h')) := ⟨rel_of_isEqv, fun ⟨h, w⟩ => by simp only [isEqv, ← h, ↓reduceDIte] diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 80ded6d67c4f..d2773aaaf173 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -53,7 +53,7 @@ theorem ne_empty_of_size_pos (h : 0 < l.size) : l ≠ #[] := by cases l simpa using List.ne_nil_of_length_pos h -@[simp] theorem size_eq_zero : l.size = 0 ↔ l = #[] := +theorem size_eq_zero : l.size = 0 ↔ l = #[] := ⟨eq_empty_of_size_eq_zero, fun h => h ▸ rfl⟩ theorem size_pos_of_mem {a : α} {l : Array α} (h : a ∈ l) : 0 < l.size := by @@ -224,7 +224,7 @@ theorem getElem?_singleton (a : α) (i : Nat) : #[a][i]? = if i = 0 then some a /-! ### mem -/ -@[simp] theorem not_mem_empty (a : α) : ¬ a ∈ #[] := nofun +theorem not_mem_empty (a : α) : ¬ a ∈ #[] := by simp @[simp] theorem mem_push {a : Array α} {x y : α} : x ∈ a.push y ↔ x ∈ a ∨ x = y := by simp only [mem_def] @@ -912,8 +912,8 @@ theorem singleton_eq_toArray_singleton (a : α) : #[a] = [a].toArray := rfl @[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl -@[simp] theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size] - +@[deprecated size_toArray (since := "2024-12-11")] +theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size] theorem foldrM_push [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) : (arr.push a).foldrM f init = f a init >>= arr.foldrM f := by @@ -982,11 +982,6 @@ where @[simp] theorem appendList_cons (arr : Array α) (a : α) (l : List α) : arr ++ (a :: l) = arr.push a ++ l := Array.ext' (by simp) -@[simp] theorem toList_appendList (arr : Array α) (l : List α) : - (arr ++ l).toList = arr.toList ++ l := by - cases arr - simp - theorem foldl_toList_eq_flatMap (l : List α) (acc : Array β) (F : Array β → α → Array β) (G : α → List β) (H : ∀ acc a, (F acc a).toList = acc.toList ++ G a) : @@ -1027,7 +1022,7 @@ theorem getElem?_len_le (a : Array α) {i : Nat} (h : a.size ≤ i) : a[i]? = no theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default := rfl -@[simp] theorem get!_eq_getElem? [Inhabited α] (a : Array α) (i : Nat) : +theorem get!_eq_getElem? [Inhabited α] (a : Array α) (i : Nat) : a.get! i = (a.get? i).getD default := by by_cases p : i < a.size <;> simp only [get!_eq_getD, getD_eq_get?, getD_getElem?, p, get?_eq_getElem?] @@ -1205,8 +1200,8 @@ theorem getElem?_swap (a : Array α) (i j : Nat) (hi hj) (k : Nat) : (a.swap i j @[simp] theorem swapAt_def (a : Array α) (i : Nat) (v : α) (hi) : a.swapAt i v hi = (a[i], a.set i v) := rfl -@[simp] theorem size_swapAt (a : Array α) (i : Nat) (v : α) (hi) : - (a.swapAt i v hi).2.size = a.size := by simp [swapAt_def] +theorem size_swapAt (a : Array α) (i : Nat) (v : α) (hi) : + (a.swapAt i v hi).2.size = a.size := by simp @[simp] theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) : @@ -1700,13 +1695,9 @@ theorem mem_append_right {a : α} (l₁ : Array α) {l₂ : Array α} (h : a ∈ @[simp] theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by simp only [size, toList_append, List.length_append] -@[simp] theorem empty_append (as : Array α) : #[] ++ as = as := by - cases as - simp +theorem empty_append (as : Array α) : #[] ++ as = as := by simp -@[simp] theorem append_empty (as : Array α) : as ++ #[] = as := by - cases as - simp +theorem append_empty (as : Array α) : as ++ #[] = as := by simp theorem getElem_append {as bs : Array α} (h : i < (as ++ bs).size) : (as ++ bs)[i] = if h' : i < as.size then as[i] else bs[i - as.size]'(by simp at h; omega) := by @@ -2062,8 +2053,7 @@ namespace List Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible. -/ -@[simp] theorem toListRev_toArray (l : List α) : l.toArray.toListRev = l.reverse := by - simp +theorem toListRev_toArray (l : List α) : l.toArray.toListRev = l.reverse := by simp @[simp] theorem take_toArray (l : List α) (n : Nat) : l.toArray.take n = (l.take n).toArray := by apply ext' @@ -2087,10 +2077,8 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible. apply ext' simp -@[simp] theorem uset_toArray (l : List α) (i : USize) (a : α) (h : i.toNat < l.toArray.size) : - l.toArray.uset i a h = (l.set i.toNat a).toArray := by - apply ext' - simp +theorem uset_toArray (l : List α) (i : USize) (a : α) (h : i.toNat < l.toArray.size) : + l.toArray.uset i a h = (l.set i.toNat a).toArray := by simp @[simp] theorem swap_toArray (l : List α) (i j : Nat) {hi hj}: l.toArray.swap i j hi hj = ((l.set i l[j]).set j l[i]).toArray := by @@ -2126,7 +2114,8 @@ theorem filterMap_toArray (f : α → Option β) (l : List α) : l.toArray.filterMap f = (l.filterMap f).toArray := by simp -@[simp] theorem flatten_toArray (l : List (List α)) : (l.toArray.map List.toArray).flatten = l.flatten.toArray := by +@[simp] theorem flatten_toArray (l : List (List α)) : + (l.toArray.map List.toArray).flatten = l.flatten.toArray := by apply ext' simp [Function.comp_def] @@ -2334,19 +2323,15 @@ end List namespace Array -@[simp] theorem toList_fst_unzip (as : Array (α × β)) : - as.unzip.1.toList = as.toList.unzip.1 := by - cases as - simp +theorem toList_fst_unzip (as : Array (α × β)) : + as.unzip.1.toList = as.toList.unzip.1 := by simp -@[simp] theorem toList_snd_unzip (as : Array (α × β)) : - as.unzip.2.toList = as.toList.unzip.2 := by - cases as - simp +theorem toList_snd_unzip (as : Array (α × β)) : + as.unzip.2.toList = as.toList.unzip.2 := by simp @[simp] theorem flatMap_empty {β} (f : α → Array β) : (#[] : Array α).flatMap f = #[] := rfl -@[simp] theorem flatMap_toArray_cons {β} (f : α → Array β) (a : α) (as : List α) : +theorem flatMap_toArray_cons {β} (f : α → Array β) (a : α) (as : List α) : (a :: as).toArray.flatMap f = f a ++ as.toArray.flatMap f := by simp [flatMap] suffices ∀ cs, List.foldl (fun bs a => bs ++ f a) (f a ++ cs) as = @@ -2362,7 +2347,7 @@ namespace Array | nil => simp | cons a as ih => apply ext' - simp [ih] + simp [ih, flatMap_toArray_cons] end Array diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index a5036d1367c8..0b6596bf4388 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -332,11 +332,11 @@ theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) : private theorem lt_two_pow_of_le {x m n : Nat} (lt : x < 2 ^ m) (le : m ≤ n) : x < 2 ^ n := Nat.lt_of_lt_of_le lt (Nat.pow_le_pow_of_le_right (by trivial : 0 < 2) le) -@[simp] theorem getElem_zero_ofNat_zero (i : Nat) (h : i < w) : (BitVec.ofNat w 0)[i] = false := by - simp [getElem_eq_testBit_toNat] +theorem getElem_zero_ofNat_zero (i : Nat) (h : i < w) : (BitVec.ofNat w 0)[i] = false := by + simp -@[simp] theorem getElem_zero_ofNat_one (h : 0 < w) : (BitVec.ofNat w 1)[0] = true := by - simp [getElem_eq_testBit_toNat, h] +theorem getElem_zero_ofNat_one (h : 0 < w) : (BitVec.ofNat w 1)[0] = true := by + simp theorem getElem?_zero_ofNat_zero : (BitVec.ofNat (w+1) 0)[0]? = some false := by simp @@ -362,12 +362,7 @@ theorem getLsbD_ofBool (b : Bool) (i : Nat) : (ofBool b).getLsbD i = ((i = 0) && · simp only [ofBool, ofNat_eq_ofNat, cond_true, getLsbD_ofNat, Bool.and_true] by_cases hi : i = 0 <;> simp [hi] <;> omega -@[simp] -theorem getElem_ofBool {b : Bool} {i : Nat} : (ofBool b)[0] = b := by - rcases b with rfl | rfl - · simp [ofBool] - · simp only [ofBool] - by_cases hi : i = 0 <;> simp [hi] <;> omega +theorem getElem_ofBool {b : Bool} : (ofBool b)[0] = b := by simp @[simp] theorem getMsbD_ofBool (b : Bool) : (ofBool b).getMsbD i = (decide (i = 0) && b) := by cases b <;> simp [getMsbD] @@ -538,7 +533,7 @@ theorem toInt_zero {w : Nat} : (0#w).toInt = 0 := by A bitvector, when interpreted as an integer, is less than zero iff its most significant bit is true. -/ -theorem slt_zero_iff_msb_cond (x : BitVec w) : x.slt 0#w ↔ x.msb = true := by +theorem slt_zero_iff_msb_cond {x : BitVec w} : x.slt 0#w ↔ x.msb = true := by have := toInt_eq_msb_cond x constructor · intros h @@ -1120,12 +1115,8 @@ theorem not_eq_comm {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y := by rw [h] simp -@[simp] theorem getMsb_not {x : BitVec w} : - (~~~x).getMsbD i = (decide (i < w) && !(x.getMsbD i)) := by - simp only [getMsbD] - by_cases h : i < w - · simp [h]; omega - · simp [h]; +theorem getMsb_not {x : BitVec w} : + (~~~x).getMsbD i = (decide (i < w) && !(x.getMsbD i)) := by simp @[simp] theorem msb_not {x : BitVec w} : (~~~x).msb = (decide (0 < w) && !x.msb) := by simp [BitVec.msb] @@ -1243,7 +1234,6 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} : @[simp] theorem getMsbD_shiftLeftZeroExtend (x : BitVec m) (n : Nat) : getMsbD (shiftLeftZeroExtend x n) i = getMsbD x i := by - have : n ≤ i + n := by omega simp_all [shiftLeftZeroExtend_eq] @[simp] theorem msb_shiftLeftZeroExtend (x : BitVec w) (i : Nat) : @@ -1291,10 +1281,9 @@ theorem getLsbD_shiftLeft' {x : BitVec w₁} {y : BitVec w₂} {i : Nat} : (x <<< y).getLsbD i = (decide (i < w₁) && !decide (i < y.toNat) && x.getLsbD (i - y.toNat)) := by simp [shiftLeft_eq', getLsbD_shiftLeft] -@[simp] theorem getElem_shiftLeft' {x : BitVec w₁} {y : BitVec w₂} {i : Nat} (h : i < w₁) : (x <<< y)[i] = (!decide (i < y.toNat) && x.getLsbD (i - y.toNat)) := by - simp [shiftLeft_eq', getLsbD_shiftLeft] + simp /-! ### ushiftRight -/ @@ -1597,39 +1586,25 @@ theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat} : @[simp] theorem sshiftRight_eq' (x : BitVec w) : x.sshiftRight' y = x.sshiftRight y.toNat := rfl -@[simp] -theorem getLsbD_sshiftRight' {x y: BitVec w} {i : Nat} : +-- This should not be a `@[simp]` lemma as the left hand side is not in simp normal form. +theorem getLsbD_sshiftRight' {x y : BitVec w} {i : Nat} : getLsbD (x.sshiftRight' y) i = (!decide (w ≤ i) && if y.toNat + i < w then x.getLsbD (y.toNat + i) else x.msb) := by simp only [BitVec.sshiftRight', BitVec.getLsbD_sshiftRight] -@[simp] +-- This should not be a `@[simp]` lemma as the left hand side is not in simp normal form. theorem getElem_sshiftRight' {x y : BitVec w} {i : Nat} (h : i < w) : (x.sshiftRight' y)[i] = (!decide (w ≤ i) && if y.toNat + i < w then x.getLsbD (y.toNat + i) else x.msb) := by simp only [← getLsbD_eq_getElem, BitVec.sshiftRight', BitVec.getLsbD_sshiftRight] -@[simp] theorem getMsbD_sshiftRight' {x y: BitVec w} {i : Nat} : - (x.sshiftRight y.toNat).getMsbD i = (decide (i < w) && if i < y.toNat then x.msb else x.getMsbD (i - y.toNat)) := by - simp only [BitVec.sshiftRight', getMsbD, BitVec.getLsbD_sshiftRight] - by_cases h : i < w - · simp only [h, decide_true, Bool.true_and] - by_cases h₁ : w ≤ w - 1 - i - · simp [h₁] - omega - · simp only [h₁, decide_false, Bool.not_false, Bool.true_and] - by_cases h₂ : i < y.toNat - · simp only [h₂, ↓reduceIte, ite_eq_right_iff] - omega - · simp only [show i - y.toNat < w by omega, h₂, ↓reduceIte, decide_true, Bool.true_and] - by_cases h₄ : y.toNat + (w - 1 - i) < w <;> (simp only [h₄, ↓reduceIte]; congr; omega) - · simp [h] + (x.sshiftRight y.toNat).getMsbD i = + (decide (i < w) && if i < y.toNat then x.msb else x.getMsbD (i - y.toNat)) := by + simp -@[simp] theorem msb_sshiftRight' {x y: BitVec w} : - (x.sshiftRight' y).msb = x.msb := by - simp [BitVec.sshiftRight', BitVec.msb_sshiftRight] + (x.sshiftRight' y).msb = x.msb := by simp /-! ### signExtend -/ @@ -1883,7 +1858,6 @@ theorem setWidth_append {x : BitVec w} {y : BitVec v} : · simp_all · simp_all only [Bool.iff_and_self, decide_eq_true_eq] intro h - have := BitVec.lt_of_getLsbD h omega @[simp] theorem setWidth_cons {x : BitVec w} : (cons a x).setWidth w = x := by @@ -2091,8 +2065,9 @@ theorem getElem_concat (x : BitVec w) (b : Bool) (i : Nat) (h : i < w + 1) : @[simp] theorem getLsbD_concat_succ : (concat x b).getLsbD (i + 1) = x.getLsbD i := by simp [getLsbD_concat] -@[simp] theorem getElem_concat_succ {x : BitVec w} {i : Nat} (h : i < w) : +@[simp] theorem getElem_concat_succ {x : BitVec w} {i : Nat} (h : i + 1 < w + 1) : (concat x b)[i + 1] = x[i] := by + simp only [Nat.add_lt_add_iff_right] at h simp [getElem_concat, h, getLsbD_eq_getElem] @[simp] @@ -2195,7 +2170,6 @@ theorem toNat_shiftConcat_lt_of_lt {x : BitVec w} {b : Bool} {k : Nat} (hk : k < w) (hx : x.toNat < 2 ^ k) : (x.shiftConcat b).toNat < 2 ^ (k + 1) := by rw [toNat_shiftConcat_eq_of_lt hk hx] - have : 2 ^ (k + 1) ≤ 2 ^ w := Nat.pow_le_pow_of_le_right (by decide) (by assumption) have := Bool.toNat_lt b omega @@ -2704,7 +2678,7 @@ theorem smtSDiv_eq (x y : BitVec w) : smtSDiv x y = @[simp] theorem smtSDiv_zero {x : BitVec n} : x.smtSDiv 0#n = if x.slt 0#n then 1#n else (allOnes n) := by - rcases hx : x.msb <;> simp [smtSDiv, slt_zero_iff_msb_cond x, hx, ← negOne_eq_allOnes] + rcases hx : x.msb <;> simp [smtSDiv, slt_zero_iff_msb_cond, hx, ← negOne_eq_allOnes] /-! ### srem -/ @@ -3024,10 +2998,10 @@ theorem getMsbD_rotateRightAux_of_ge {x : BitVec w} {r : Nat} {i : Nat} (hi : i simp [rotateRightAux, show ¬ i < r by omega, show i + (w - r) ≥ w by omega] /-- When `m < w`, we give a formula for `(x.rotateLeft m).getMsbD i`. -/ -@[simp] -theorem getMsbD_rotateRight_of_lt {w n m : Nat} {x : BitVec w} (hr : m < w): +-- This should not be a simp lemma as `getMsbD_rotateRight` will apply first. +theorem getMsbD_rotateRight_of_lt {w n m : Nat} {x : BitVec w} (hr : m < w) : (x.rotateRight m).getMsbD n = (decide (n < w) && (if (n < m % w) - then x.getMsbD ((w + n - m % w) % w) else x.getMsbD (n - m % w))):= by + then x.getMsbD ((w + n - m % w) % w) else x.getMsbD (n - m % w))) := by rcases w with rfl | w · simp · rw [rotateRight_eq_rotateRightAux_of_lt (by omega)] @@ -3590,9 +3564,7 @@ Note, however, that for large numerals the decision procedure may be very slow. instance instDecidableExistsBitVec : ∀ (n : Nat) (P : BitVec n → Prop) [DecidablePred P], Decidable (∃ v, P v) | 0, _, _ => inferInstance - | n + 1, _, _ => - have := instDecidableExistsBitVec n - inferInstance + | _ + 1, _, _ => inferInstance /-! ### Deprecations -/ diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean index 681c078ad6c3..2b9a494eff9d 100644 --- a/src/Init/Data/Bool.lean +++ b/src/Init/Data/Bool.lean @@ -225,7 +225,7 @@ theorem bne_not_self : ∀ (x : Bool), (x != !x) = true := by decide Added for equivalence with `Bool.not_beq_self` and needed for confluence due to `beq_iff_eq`. -/ -@[simp] theorem not_eq_self : ∀(b : Bool), ((!b) = b) ↔ False := by decide +theorem not_eq_self : ∀(b : Bool), ((!b) = b) ↔ False := by simp @[simp] theorem eq_not_self : ∀(b : Bool), (b = (!b)) ↔ False := by decide @[simp] theorem beq_self_left : ∀(a b : Bool), (a == (a == b)) = b := by decide @@ -420,7 +420,7 @@ def toInt (b : Bool) : Int := cond b 1 0 @[simp] theorem ite_eq_true_else_eq_false {q : Prop} : (if b = true then q else b = false) ↔ (b = true → q) := by - cases b <;> simp + cases b <;> simp [not_eq_self] /- `not_ite_eq_true_eq_true` and related theorems below are added for diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean index 803515dee3ac..44c675611760 100644 --- a/src/Init/Data/Fin/Lemmas.lean +++ b/src/Init/Data/Fin/Lemmas.lean @@ -545,10 +545,8 @@ theorem natAdd_natAdd (m n : Nat) {p : Nat} (i : Fin p) : natAdd m (natAdd n i) = (natAdd (m + n) i).cast (Nat.add_assoc ..) := Fin.ext <| (Nat.add_assoc ..).symm -@[simp] theorem cast_natAdd_zero {n n' : Nat} (i : Fin n) (h : 0 + n = n') : - (natAdd 0 i).cast h = i.cast ((Nat.zero_add _).symm.trans h) := - Fin.ext <| Nat.zero_add _ + (natAdd 0 i).cast h = i.cast ((Nat.zero_add _).symm.trans h) := by simp @[simp] theorem cast_natAdd (n : Nat) {m : Nat} (i : Fin m) : diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean index 30495ba7b153..a13f7dfa6fc6 100644 --- a/src/Init/Data/List/Attach.lean +++ b/src/Init/Data/List/Attach.lean @@ -118,7 +118,6 @@ theorem attach_map_coe (l : List α) (f : α → β) : theorem attach_map_val (l : List α) (f : α → β) : (l.attach.map fun i => f i.val) = l.map f := attach_map_coe _ _ -@[simp] theorem attach_map_subtype_val (l : List α) : l.attach.map Subtype.val = l := (attach_map_coe _ _).trans (List.map_id _) @@ -130,7 +129,6 @@ theorem attachWith_map_val {p : α → Prop} (f : α → β) (l : List α) (H : ((l.attachWith p H).map fun i => f i.val) = l.map f := attachWith_map_coe _ _ _ -@[simp] theorem attachWith_map_subtype_val {p : α → Prop} (l : List α) (H : ∀ a ∈ l, p a) : (l.attachWith p H).map Subtype.val = l := (attachWith_map_coe _ _ _).trans (List.map_id _) @@ -174,8 +172,8 @@ theorem pmap_ne_nil_iff {P : α → Prop} (f : (a : α) → P a → β) {xs : Li (H : ∀ (a : α), a ∈ xs → P a) : xs.pmap f H ≠ [] ↔ xs ≠ [] := by simp -theorem pmap_eq_self {l : List α} {p : α → Prop} (hp : ∀ (a : α), a ∈ l → p a) - (f : (a : α) → p a → α) : l.pmap f hp = l ↔ ∀ a (h : a ∈ l), f a (hp a h) = a := by +theorem pmap_eq_self {l : List α} {p : α → Prop} {hp : ∀ (a : α), a ∈ l → p a} + {f : (a : α) → p a → α} : l.pmap f hp = l ↔ ∀ a (h : a ∈ l), f a (hp a h) = a := by rw [pmap_eq_map_attach] conv => lhs; rhs; rw [← attach_map_subtype_val l] rw [map_inj_left] diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean index 5fece2e68120..dd9c73ccf279 100644 --- a/src/Init/Data/List/Find.lean +++ b/src/Init/Data/List/Find.lean @@ -566,7 +566,6 @@ theorem not_of_lt_findIdx {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs | inl e => simpa [e, Fin.zero_eta, get_cons_zero] | inr e => have ipm := Nat.succ_pred_eq_of_pos e - have ilt := Nat.le_trans ho (findIdx_le_length p) simp +singlePass only [← ipm, getElem_cons_succ] rw [← ipm, Nat.succ_lt_succ_iff] at h simpa using ih h diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index db95591bd005..998ec193d956 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -216,7 +216,9 @@ We simplify `l[i]!` to `(l[i]?).getD default`. @[simp] theorem getElem!_eq_getElem?_getD [Inhabited α] (l : List α) (i : Nat) : l[i]! = (l[i]?).getD (default : α) := by simp only [getElem!_def] - split <;> simp_all + match l[i]? with + | some _ => simp + | none => simp /-! ### getElem? and getElem -/ diff --git a/src/Init/Data/List/Nat/Modify.lean b/src/Init/Data/List/Nat/Modify.lean index 60dc4e3fa39a..aac841c02ac3 100644 --- a/src/Init/Data/List/Nat/Modify.lean +++ b/src/Init/Data/List/Nat/Modify.lean @@ -68,8 +68,8 @@ theorem getElem?_modifyHead {l : List α} {f : α → α} {n} : (l.modifyHead f).drop n = l.drop n := by cases l <;> cases n <;> simp_all -@[simp] theorem eraseIdx_modifyHead_zero {f : α → α} {l : List α} : - (l.modifyHead f).eraseIdx 0 = l.eraseIdx 0 := by cases l <;> simp +theorem eraseIdx_modifyHead_zero {f : α → α} {l : List α} : + (l.modifyHead f).eraseIdx 0 = l.eraseIdx 0 := by simp @[simp] theorem eraseIdx_modifyHead_of_pos {f : α → α} {l : List α} {n} (h : 0 < n) : (l.modifyHead f).eraseIdx n = (l.eraseIdx n).modifyHead f := by cases l <;> cases n <;> simp_all @@ -142,7 +142,7 @@ theorem modifyTailIdx_modifyTailIdx_self {f g : List α → List α} (n : Nat) ( theorem modifyHead_eq_modify_zero (f : α → α) (l : List α) : l.modifyHead f = l.modify f 0 := by cases l <;> simp -@[simp] theorem modify_eq_nil_iff (f : α → α) (n) (l : List α) : +@[simp] theorem modify_eq_nil_iff {f : α → α} {n} {l : List α} : l.modify f n = [] ↔ l = [] := by cases l <;> cases n <;> simp theorem getElem?_modify (f : α → α) : diff --git a/src/Init/Data/List/Sort/Impl.lean b/src/Init/Data/List/Sort/Impl.lean index 51271b5b296d..9a9c947d6012 100644 --- a/src/Init/Data/List/Sort/Impl.lean +++ b/src/Init/Data/List/Sort/Impl.lean @@ -147,23 +147,21 @@ where mergeTR (run' r) (run l) le theorem splitRevInTwo'_fst (l : { l : List α // l.length = n }) : - (splitRevInTwo' l).1 = ⟨(splitInTwo ⟨l.1.reverse, by simpa using l.2⟩).2.1, by have := l.2; simp; omega⟩ := by + (splitRevInTwo' l).1 = ⟨(splitInTwo ⟨l.1.reverse, by simpa using l.2⟩).2.1, by simp; omega⟩ := by simp only [splitRevInTwo', splitRevAt_eq, reverse_take, splitInTwo_snd] congr - have := l.2 omega theorem splitRevInTwo'_snd (l : { l : List α // l.length = n }) : - (splitRevInTwo' l).2 = ⟨(splitInTwo ⟨l.1.reverse, by simpa using l.2⟩).1.1.reverse, by have := l.2; simp; omega⟩ := by + (splitRevInTwo' l).2 = ⟨(splitInTwo ⟨l.1.reverse, by simpa using l.2⟩).1.1.reverse, by simp; omega⟩ := by simp only [splitRevInTwo', splitRevAt_eq, reverse_take, splitInTwo_fst, reverse_reverse] congr 2 - have := l.2 simp omega theorem splitRevInTwo_fst (l : { l : List α // l.length = n }) : - (splitRevInTwo l).1 = ⟨(splitInTwo l).1.1.reverse, by have := l.2; simp; omega⟩ := by + (splitRevInTwo l).1 = ⟨(splitInTwo l).1.1.reverse, by simp; omega⟩ := by simp only [splitRevInTwo, splitRevAt_eq, reverse_take, splitInTwo_fst] theorem splitRevInTwo_snd (l : { l : List α // l.length = n }) : - (splitRevInTwo l).2 = ⟨(splitInTwo l).2.1, by have := l.2; simp; omega⟩ := by + (splitRevInTwo l).2 = ⟨(splitInTwo l).2.1, by simp; omega⟩ := by simp only [splitRevInTwo, splitRevAt_eq, reverse_take, splitInTwo_snd] theorem mergeSortTR_run_eq_mergeSort : {n : Nat} → (l : { l : List α // l.length = n }) → mergeSortTR.run le l = mergeSort l.1 le diff --git a/src/Init/Data/List/Sort/Lemmas.lean b/src/Init/Data/List/Sort/Lemmas.lean index 494b82331f1f..4b850aff7b73 100644 --- a/src/Init/Data/List/Sort/Lemmas.lean +++ b/src/Init/Data/List/Sort/Lemmas.lean @@ -285,8 +285,6 @@ theorem sorted_mergeSort | [] => by simp [mergeSort] | [a] => by simp [mergeSort] | a :: b :: xs => by - have : (splitInTwo ⟨a :: b :: xs, rfl⟩).1.1.length < xs.length + 1 + 1 := by simp [splitInTwo_fst]; omega - have : (splitInTwo ⟨a :: b :: xs, rfl⟩).2.1.length < xs.length + 1 + 1 := by simp [splitInTwo_snd]; omega rw [mergeSort] apply sorted_merge @trans @total apply sorted_mergeSort trans total diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean index 4c199cd539d7..d50476e3eb23 100644 --- a/src/Init/Data/List/ToArray.lean +++ b/src/Init/Data/List/ToArray.lean @@ -38,7 +38,7 @@ theorem toArray_inj {a b : List α} (h : a.toArray = b.toArray) : a = b := by simp @[simp] theorem isEmpty_toArray (l : List α) : l.toArray.isEmpty = l.isEmpty := by - cases l <;> simp + cases l <;> simp [Array.isEmpty] @[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = singleton a := rfl diff --git a/src/Init/Data/Option/Attach.lean b/src/Init/Data/Option/Attach.lean index bc00241e71fc..50639ccb9f45 100644 --- a/src/Init/Data/Option/Attach.lean +++ b/src/Init/Data/Option/Attach.lean @@ -56,7 +56,6 @@ theorem attach_map_val (o : Option α) (f : α → β) : (o.attach.map fun i => f i.val) = o.map f := attach_map_coe _ _ -@[simp] theorem attach_map_subtype_val (o : Option α) : o.attach.map Subtype.val = o := (attach_map_coe _ _).trans (congrFun Option.map_id _) @@ -69,12 +68,11 @@ theorem attachWith_map_val {p : α → Prop} (f : α → β) (o : Option α) (H ((o.attachWith p H).map fun i => f i.val) = o.map f := attachWith_map_coe _ _ _ -@[simp] theorem attachWith_map_subtype_val {p : α → Prop} (o : Option α) (H : ∀ a ∈ o, p a) : (o.attachWith p H).map Subtype.val = o := (attachWith_map_coe _ _ _).trans (congrFun Option.map_id _) -@[simp] theorem mem_attach : ∀ (o : Option α) (x : {x // x ∈ o}), x ∈ o.attach +theorem mem_attach : ∀ (o : Option α) (x : {x // x ∈ o}), x ∈ o.attach | none, ⟨x, h⟩ => by simp at h | some a, ⟨x, h⟩ => by simpa using h @@ -92,14 +90,14 @@ theorem attachWith_map_subtype_val {p : α → Prop} (o : Option α) (H : ∀ a (o.attachWith p H).isSome = o.isSome := by cases o <;> simp -@[simp] theorem attach_eq_none_iff (o : Option α) : o.attach = none ↔ o = none := by +@[simp] theorem attach_eq_none_iff {o : Option α} : o.attach = none ↔ o = none := by cases o <;> simp @[simp] theorem attach_eq_some_iff {o : Option α} {x : {x // x ∈ o}} : o.attach = some x ↔ o = some x.val := by cases o <;> cases x <;> simp -@[simp] theorem attachWith_eq_none_iff {p : α → Prop} (o : Option α) (H : ∀ a ∈ o, p a) : +@[simp] theorem attachWith_eq_none_iff {p : α → Prop} {o : Option α} (H : ∀ a ∈ o, p a) : o.attachWith p H = none ↔ o = none := by cases o <;> simp diff --git a/src/Init/Data/Sum/Lemmas.lean b/src/Init/Data/Sum/Lemmas.lean index 72a96a48ab46..0a316e1207d8 100644 --- a/src/Init/Data/Sum/Lemmas.lean +++ b/src/Init/Data/Sum/Lemmas.lean @@ -30,7 +30,7 @@ protected theorem «exists» {p : α ⊕ β → Prop} : | Or.inl ⟨a, h⟩ => ⟨inl a, h⟩ | Or.inr ⟨b, h⟩ => ⟨inr b, h⟩⟩ -theorem forall_sum {γ : α ⊕ β → Sort _} (p : (∀ ab, γ ab) → Prop) : +theorem forall_sum {γ : α ⊕ β → Sort _} {p : (∀ ab, γ ab) → Prop} : (∀ fab, p fab) ↔ (∀ fa fb, p (Sum.rec fa fb)) := by refine ⟨fun h fa fb => h _, fun h fab => ?_⟩ have h1 : fab = Sum.rec (fun a => fab (Sum.inl a)) (fun b => fab (Sum.inr b)) := by diff --git a/src/Init/GetElem.lean b/src/Init/GetElem.lean index 03ba85787eca..b536d2cca25c 100644 --- a/src/Init/GetElem.lean +++ b/src/Init/GetElem.lean @@ -176,11 +176,14 @@ theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem d simp only [getElem?_def] at h ⊢ split <;> simp_all -@[simp] theorem isNone_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] - (c : cont) (i : idx) [Decidable (dom c i)] : c[i]?.isNone = ¬dom c i := by +@[simp] theorem getElem?_eq_none [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] + (c : cont) (i : idx) [Decidable (dom c i)] : c[i]? = none ↔ ¬dom c i := by simp only [getElem?_def] split <;> simp_all +@[deprecated getElem?_eq_none (since := "2024-12-11")] +abbrev isNone_getElem? := @getElem?_eq_none + @[simp] theorem isSome_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] (c : cont) (i : idx) [Decidable (dom c i)] : c[i]?.isSome = dom c i := by simp only [getElem?_def] diff --git a/src/Init/SimpLemmas.lean b/src/Init/SimpLemmas.lean index beb1b18bcb9e..089559d63bbe 100644 --- a/src/Init/SimpLemmas.lean +++ b/src/Init/SimpLemmas.lean @@ -153,6 +153,7 @@ instance : Std.LawfulIdentity Or False where @[simp] theorem false_implies (p : Prop) : (False → p) = True := eq_true False.elim @[simp] theorem forall_false (p : False → Prop) : (∀ h : False, p h) = True := eq_true (False.elim ·) @[simp] theorem implies_true (α : Sort u) : (α → True) = True := eq_true fun _ => trivial +-- This is later proved by the simp lemma `forall_const`, but this is useful during bootstrapping. @[simp] theorem true_implies (p : Prop) : (True → p) = p := propext ⟨(· trivial), (fun _ => ·)⟩ @[simp] theorem not_false_eq_true : (¬ False) = True := eq_true False.elim @[simp] theorem not_true_eq_false : (¬ True) = False := by decide diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean index 837b6c76545c..60343ea5fbac 100644 --- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean +++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean @@ -830,9 +830,9 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} : simp_to_model using List.containsKey_eq_keys_contains.symm @[simp] -theorem mem_keys [LawfulBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} : +theorem mem_keys [LawfulBEq α] (h : m.1.WF) {k : α} : k ∈ m.1.keys ↔ m.contains k := by - simp_to_model + simp_to_model rw [List.containsKey_eq_keys_contains] theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) : diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean index e6016179028c..bb61c54e1d2f 100644 --- a/src/Std/Data/DHashMap/Lemmas.lean +++ b/src/Std/Data/DHashMap/Lemmas.lean @@ -111,15 +111,11 @@ theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k a ∈ m.insert k v → (k == a) = false → a ∈ m := by simpa [mem_iff_contains, -contains_insert] using contains_of_contains_insert -@[simp] theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} : - (m.insert k v).contains k := - Raw₀.contains_insert_self ⟨m.1, _⟩ m.2 + (m.insert k v).contains k := by simp -@[simp] theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} : - k ∈ m.insert k v := by - simp [mem_iff_contains, contains_insert_self] + k ∈ m.insert k v := by simp @[simp] theorem size_empty {c} : (empty c : DHashMap α β).size = 0 := @@ -959,13 +955,13 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] {k : α} : Raw₀.contains_keys ⟨m.1, _⟩ m.2 @[simp] -theorem mem_keys [LawfulBEq α] [LawfulHashable α] {k : α} : - k ∈ m.keys ↔ k ∈ m := by +theorem mem_keys [LawfulBEq α] {k : α} : + k ∈ m.keys ↔ k ∈ m := by rw [mem_iff_contains] exact Raw₀.mem_keys ⟨m.1, _⟩ m.2 theorem distinct_keys [EquivBEq α] [LawfulHashable α] : - m.keys.Pairwise (fun a b => (a == b) = false) := + m.keys.Pairwise (fun a b => (a == b) = false) := Raw₀.distinct_keys ⟨m.1, m.2.size_buckets_pos⟩ m.2 end Std.DHashMap diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean index c852d0acd36f..5e9f89e692fa 100644 --- a/src/Std/Data/HashMap/Lemmas.lean +++ b/src/Std/Data/HashMap/Lemmas.lean @@ -119,14 +119,11 @@ theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} a ∈ m.insert k v → (k == a) = false → a ∈ m := DHashMap.mem_of_mem_insert -@[simp] theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : - (m.insert k v).contains k := - DHashMap.contains_insert_self + (m.insert k v).contains k := by simp -@[simp] -theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : k ∈ m.insert k v := - DHashMap.mem_insert_self +theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : k ∈ m.insert k v := by + simp @[simp] theorem size_empty {c} : (empty c : HashMap α β).size = 0 := diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean index 245f8ce9416c..232724f26c0d 100644 --- a/src/Std/Data/HashSet/Lemmas.lean +++ b/src/Std/Data/HashSet/Lemmas.lean @@ -122,13 +122,10 @@ theorem mem_of_mem_insert' [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m.insert k → ¬((k == a) ∧ ¬k ∈ m) → a ∈ m := DHashMap.mem_of_mem_insertIfNew' -@[simp] -theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} : (m.insert k).contains k := - HashMap.contains_insertIfNew_self +theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} : (m.insert k).contains k := by + simp -@[simp] -theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} : k ∈ m.insert k := - HashMap.mem_insertIfNew_self +theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} : k ∈ m.insert k := by simp @[simp] theorem size_empty {c} : (empty c : HashSet α).size = 0 := diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean index 410e68e7b36a..41d343c3dd26 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean @@ -494,7 +494,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor · next id_eq_idx => exfalso have idx_in_bounds2 : idx < f.clauses.size := by - conv => rhs; rw [Array.size_mk] + conv => rhs; rw [Array.size_toArray] exact hbound simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, ↓reduceDIte, Fin.eta, Array.get_eq_getElem, ← Array.getElem_toList, decidableGetElem?] at heq @@ -527,7 +527,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor · next id_eq_idx => exfalso have idx_in_bounds2 : idx < f.clauses.size := by - conv => rhs; rw [Array.size_mk] + conv => rhs; rw [Array.size_toArray] exact hbound simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, ↓reduceDIte, Fin.eta, Array.get_eq_getElem, ← Array.getElem_toList, decidableGetElem?] at heq @@ -587,7 +587,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor · next id_eq_idx => exfalso have idx_in_bounds2 : idx < f.clauses.size := by - conv => rhs; rw [Array.size_mk] + conv => rhs; rw [Array.size_toArray] exact hbound simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, ↓reduceDIte, Fin.eta, Array.get_eq_getElem, ← Array.getElem_toList, decidableGetElem?] at heq diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean index 4ba79bcc390f..5603cfec865e 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean @@ -1115,11 +1115,11 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n) simp [li, Array.getElem_mem] have i_in_bounds : i.1 < derivedLits.length := by have i_property := i.2 - simp only [derivedLits_arr_def, Array.size_mk] at i_property + simp only [derivedLits_arr_def, Array.size_toArray] at i_property exact i_property have j_in_bounds : j.1 < derivedLits.length := by have j_property := j.2 - simp only [derivedLits_arr_def, Array.size_mk] at j_property + simp only [derivedLits_arr_def, Array.size_toArray] at j_property exact j_property rcases derivedLits_satisfies_invariant ⟨li.1.1, li.1.2.2⟩ with ⟨_, h2⟩ | ⟨k, _, _, _, h3⟩ | ⟨k1, k2, _, _, k1_eq_true, k2_eq_false, _, _, h3⟩ @@ -1216,7 +1216,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu exact h2 derivedLits_arr[j] idx_in_list · apply Or.inr ∘ Or.inl have j_lt_derivedLits_arr_size : j.1 < derivedLits_arr.size := by - simp only [derivedLits_arr_def, Array.size_mk] + simp only [derivedLits_arr_def, Array.size_toArray] exact j.2 have i_gt_zero : i.1 > 0 := by rw [← j_eq_i]; exact (List.get derivedLits j).1.2.1 refine ⟨⟨j.1, j_lt_derivedLits_arr_size⟩, List.get derivedLits j |>.2, i_gt_zero, ?_⟩ @@ -1229,7 +1229,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu intro k _ k_ne_j have k_in_bounds : k < derivedLits.length := by have k_property := k.2 - simp only [derivedLits_arr_def, Array.size_mk] at k_property + simp only [derivedLits_arr_def, Array.size_toArray] at k_property exact k_property have k_ne_j : ⟨k.1, k_in_bounds⟩ ≠ j := by apply Fin.ne_of_val_ne @@ -1239,10 +1239,10 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu exact h3 ⟨k.1, k_in_bounds⟩ k_ne_j · apply Or.inr ∘ Or.inr have j1_lt_derivedLits_arr_size : j1.1 < derivedLits_arr.size := by - simp only [derivedLits_arr_def, Array.size_mk] + simp only [derivedLits_arr_def, Array.size_toArray] exact j1.2 have j2_lt_derivedLits_arr_size : j2.1 < derivedLits_arr.size := by - simp only [derivedLits_arr_def, Array.size_mk] + simp only [derivedLits_arr_def, Array.size_toArray] exact j2.2 have i_gt_zero : i.1 > 0 := by rw [← j1_eq_i]; exact (List.get derivedLits j1).1.2.1 refine ⟨⟨j1.1, j1_lt_derivedLits_arr_size⟩, @@ -1260,7 +1260,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu intro k _ k_ne_j1 k_ne_j2 have k_in_bounds : k < derivedLits.length := by have k_property := k.2 - simp only [derivedLits_arr_def, Array.size_mk] at k_property + simp only [derivedLits_arr_def, Array.size_toArray] at k_property exact k_property have k_ne_j1 : ⟨k.1, k_in_bounds⟩ ≠ j1 := by apply Fin.ne_of_val_ne diff --git a/tests/lean/run/array_simp.lean b/tests/lean/run/array_simp.lean index 4e6ff093b14c..51e772b27d2b 100644 --- a/tests/lean/run/array_simp.lean +++ b/tests/lean/run/array_simp.lean @@ -6,6 +6,9 @@ #check_simp #[1,2,3,4,5][7]! ~> (default : Nat) #check_simp (#[] : Array Nat)[0]! ~> (default : Nat) +variable {xs : Array α} in +#check_simp xs.size = 0 ~> xs = #[] + attribute [local simp] Id.run in #check_simp (Id.run do