From 9a032cd261b10a4d57cb952c5a5ed08eafe2161e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 16 Feb 2026 07:57:21 -0800 Subject: [PATCH] feat: `backward.isDefEq.respectTransparency` (#12179) This PR ensures `isDefEq` does not increase the transparency mode to `.default` when checking whether implicit arguments are definitionally equal. The previous behavior was creating scalability problems in Mathlib. That said, this is a very disruptive change. The previous behavior can be restored using the command ``` set_option backward.isDefEq.respectTransparency false ``` --- src/Init/Control/Lawful/Instances.lean | 4 ++ .../Control/Lawful/MonadAttach/Instances.lean | 9 +++-- src/Init/Data/Array/Basic.lean | 2 +- src/Init/Data/Array/Bootstrap.lean | 4 +- src/Init/Data/Array/Count.lean | 2 + src/Init/Data/Array/DecidableEq.lean | 5 ++- src/Init/Data/Array/Find.lean | 8 ++-- src/Init/Data/Array/Lemmas.lean | 10 ++++- src/Init/Data/Array/MapIdx.lean | 2 + src/Init/Data/Array/OfFn.lean | 2 + src/Init/Data/BitVec/Bitblast.lean | 1 + src/Init/Data/BitVec/Lemmas.lean | 9 +++-- src/Init/Data/ByteArray/Lemmas.lean | 14 +++---- src/Init/Data/Fin/Fold.lean | 11 +++--- src/Init/Data/Fin/Iterate.lean | 4 +- src/Init/Data/Fin/Lemmas.lean | 11 +++--- .../Lemmas/Combinators/FilterMap.lean | 1 + .../Iterators/Lemmas/Combinators/FlatMap.lean | 2 + .../Lemmas/Combinators/Monadic/FilterMap.lean | 5 +++ .../Lemmas/Combinators/Monadic/FlatMap.lean | 2 +- .../Lemmas/Combinators/Monadic/ULift.lean | 2 +- .../Iterators/Lemmas/Combinators/ULift.lean | 3 ++ .../Data/Iterators/Lemmas/Consumers/Loop.lean | 2 +- .../Data/Iterators/Lemmas/Producers/List.lean | 3 +- .../Lemmas/Producers/Monadic/List.lean | 2 +- src/Init/Data/List/Count.lean | 8 +++- src/Init/Data/List/Find.lean | 4 +- src/Init/Data/List/Lemmas.lean | 8 ++-- src/Init/Data/List/MapIdx.lean | 1 + src/Init/Data/List/MinMaxIdx.lean | 1 + src/Init/Data/List/Nat/Count.lean | 1 + src/Init/Data/List/Nat/Pairwise.lean | 2 + src/Init/Data/List/OfFn.lean | 9 +++-- src/Init/Data/List/Sort/Basic.lean | 1 + src/Init/Data/List/Sort/Impl.lean | 4 +- src/Init/Data/List/ToArray.lean | 15 +++++--- src/Init/Data/Nat/Fold.lean | 5 ++- src/Init/Data/Option/Attach.lean | 2 + src/Init/Data/Order/PackageFactories.lean | 1 + .../Data/Range/Polymorphic/RangeIterator.lean | 10 +++-- src/Init/Data/Slice/Array/Lemmas.lean | 6 ++- src/Init/Data/Slice/List/Lemmas.lean | 2 +- src/Init/Data/String/Basic.lean | 1 + src/Init/Data/String/Decode.lean | 5 +++ src/Init/Data/String/Lemmas/Basic.lean | 5 ++- src/Init/Data/String/Lemmas/Iterate.lean | 4 ++ .../Data/String/Lemmas/Pattern/Basic.lean | 1 + .../Data/String/Lemmas/Pattern/Split.lean | 1 + .../Pattern/String/ForwardSearcher.lean | 3 ++ src/Init/Data/Vector/Attach.lean | 2 +- src/Init/Data/Vector/Count.lean | 5 ++- src/Init/Data/Vector/Extract.lean | 3 +- src/Init/Data/Vector/Find.lean | 4 +- src/Init/Data/Vector/Lemmas.lean | 5 ++- src/Init/Data/Vector/Monadic.lean | 2 +- src/Init/Data/Vector/OfFn.lean | 1 + src/Init/Grind/Ring/Basic.lean | 2 +- src/Init/GrindInstances/Ring/Fin.lean | 1 + src/Init/Hints.lean | 4 +- src/Lean/Meta/ExprDefEq.lean | 2 +- src/Std/Data/DHashMap/IteratorLemmas.lean | 4 +- src/Std/Data/DTreeMap/Internal/Zipper.lean | 33 ++++++++++++++++- .../Lemmas/Combinators/Monadic/DropWhile.lean | 1 + .../Lemmas/Combinators/Monadic/FilterMap.lean | 1 + .../Iterators/Lemmas/Combinators/Zip.lean | 1 + .../Iterators/Lemmas/Equivalence/Basic.lean | 1 + .../Lemmas/Equivalence/StepCongr.lean | 2 + .../Iterators/Lemmas/Producers/Empty.lean | 2 +- .../Lemmas/Producers/Monadic/Array.lean | 1 + .../Lemmas/Producers/Monadic/List.lean | 1 + .../Iterators/Lemmas/Producers/Repeat.lean | 1 + src/Std/Do/Triple/SpecLemmas.lean | 3 ++ .../Circuit/Impl/Operations/Extract.lean | 2 +- .../Circuit/Impl/Operations/RotateLeft.lean | 2 +- .../Circuit/Impl/Operations/RotateRight.lean | 2 +- .../Circuit/Impl/Operations/ShiftRight.lean | 2 +- .../Circuit/Lemmas/Operations/Replicate.lean | 2 + .../LRAT/Internal/Formula/Lemmas.lean | 1 + .../LRAT/Internal/Formula/RatAddSound.lean | 1 + .../LRAT/Internal/Formula/RupAddResult.lean | 1 + src/Std/Time/Date/ValidDate.lean | 1 + stage0/src/stdlib_flags.h | 1 + tests/lean/beginEndAsMacro.lean | 2 +- tests/lean/run/1302.lean | 6 ++- tests/lean/run/1986.lean | 2 +- tests/lean/run/3807.lean | 37 +++++++++++++++++-- tests/lean/run/4171.lean | 5 +++ tests/lean/run/doLogicTests.lean | 2 + tests/lean/run/mvcgenTutorial.lean | 1 + tests/lean/run/ofNatNormNum.lean | 4 +- tests/lean/run/structWithAlgTCSynth.lean | 2 +- 91 files changed, 280 insertions(+), 98 deletions(-) diff --git a/src/Init/Control/Lawful/Instances.lean b/src/Init/Control/Lawful/Instances.lean index ae4ef4b783..39b2cf3d7f 100644 --- a/src/Init/Control/Lawful/Instances.lean +++ b/src/Init/Control/Lawful/Instances.lean @@ -116,6 +116,7 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (ExceptT ε m) where ExceptT.run (liftWith f) = Except.ok <$> (f fun x => x.run) := rfl +set_option backward.isDefEq.respectTransparency false in @[simp] theorem run_controlAt [Monad m] [LawfulMonad m] (f : ({β : Type u} → ExceptT ε m β → m (stM m (ExceptT ε m) β)) → m (stM m (ExceptT ε m) α)) : ExceptT.run (controlAt m f) = f fun x => x.run := by simp [controlAt, run_bind, bind_map_left] @@ -256,6 +257,7 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (OptionT m) where rw [← bind_pure_comp] rfl +set_option backward.isDefEq.respectTransparency false in @[simp] theorem run_controlAt [Monad m] [LawfulMonad m] (f : ({β : Type u} → OptionT m β → m (stM m (OptionT m) β)) → m (stM m (OptionT m) α)) : OptionT.run (controlAt m f) = f fun x => x.run := by simp [controlAt, Option.elimM, Option.elim] @@ -343,6 +345,7 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (ReaderT ρ m) where ReaderT.run (liftWith f) ctx = (f fun x => x.run ctx) := rfl +set_option backward.isDefEq.respectTransparency false in @[simp] theorem run_controlAt [Monad m] [LawfulMonad m] (f : ({β : Type u} → ReaderT ρ m β → m (stM m (ReaderT ρ m) β)) → m (stM m (ReaderT ρ m) α)) (ctx : ρ) : ReaderT.run (controlAt m f) ctx = f fun x => x.run ctx := by simp [controlAt] @@ -443,6 +446,7 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (StateT σ m) where StateT.run (liftWith f) s = ((·, s) <$> f fun x => x.run s) := by simp [liftWith, MonadControl.liftWith, Function.comp_def] +set_option backward.isDefEq.respectTransparency false in @[simp] theorem run_controlAt [Monad m] [LawfulMonad m] (f : ({β : Type u} → StateT σ m β → m (stM m (StateT σ m) β)) → m (stM m (StateT σ m) α)) (s : σ) : StateT.run (controlAt m f) s = f fun x => x.run s := by simp [controlAt] diff --git a/src/Init/Control/Lawful/MonadAttach/Instances.lean b/src/Init/Control/Lawful/MonadAttach/Instances.lean index 814622e006..0bdc9a298a 100644 --- a/src/Init/Control/Lawful/MonadAttach/Instances.lean +++ b/src/Init/Control/Lawful/MonadAttach/Instances.lean @@ -15,7 +15,8 @@ public import Init.Ext public instance [Monad m] [LawfulMonad m] [MonadAttach m] [WeaklyLawfulMonadAttach m] : WeaklyLawfulMonadAttach (ReaderT ρ m) where map_attach := by - simp only [Functor.map, MonadAttach.attach, Functor.map_map, WeaklyLawfulMonadAttach.map_attach] + simp only [Functor.map, MonadAttach.attach, Functor.map_map, WeaklyLawfulMonadAttach.map_attach, + MonadAttach.CanReturn] intros; rfl public instance [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m] : @@ -30,7 +31,7 @@ public instance [Monad m] [LawfulMonad m] [MonadAttach m] [WeaklyLawfulMonadAtta map_attach := by intro α x simp only [Functor.map, StateT, funext_iff, StateT.map, bind_pure_comp, MonadAttach.attach, - Functor.map_map] + Functor.map_map, MonadAttach.CanReturn] exact fun s => WeaklyLawfulMonadAttach.map_attach public instance [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m] : @@ -45,7 +46,7 @@ public instance [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m] public instance [Monad m] [LawfulMonad m] [MonadAttach m] [WeaklyLawfulMonadAttach m] : WeaklyLawfulMonadAttach (ExceptT ε m) where map_attach {α} x := by - simp only [Functor.map, MonadAttach.attach, ExceptT.map] + simp only [Functor.map, MonadAttach.attach, ExceptT.map, MonadAttach.CanReturn] simp conv => rhs; rw [← WeaklyLawfulMonadAttach.map_attach (m := m) (x := x)] simp only [map_eq_pure_bind] @@ -83,6 +84,6 @@ attribute [local instance] MonadAttach.trivial public instance [Monad m] [LawfulMonad m] : WeaklyLawfulMonadAttach m where - map_attach := by simp [MonadAttach.attach] + map_attach := by simp [MonadAttach.attach, MonadAttach.CanReturn] end diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 09b114bbb8..cddd2a50ea 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -93,7 +93,7 @@ theorem ext' {xs ys : Array α} (h : xs.toList = ys.toList) : xs = ys := by @[simp, grind =] theorem getElem?_toList {xs : Array α} {i : Nat} : xs.toList[i]? = xs[i]? := by simp only [getElem?_def, getElem_toList] - simp only [Array.size] + simp only [Array.size]; rfl /-- `a ∈ as` is a predicate which asserts that `a` is in the array `as`. -/ -- NB: This is defined as a structure rather than a plain def so that a lemma diff --git a/src/Init/Data/Array/Bootstrap.lean b/src/Init/Data/Array/Bootstrap.lean index 8300d23bc6..89252603cf 100644 --- a/src/Init/Data/Array/Bootstrap.lean +++ b/src/Init/Data/Array/Bootstrap.lean @@ -52,7 +52,9 @@ theorem foldrM_eq_reverse_foldlM_toList.aux [Monad m] unfold foldrM.fold match i with | 0 => simp - | i+1 => rw [← List.take_concat_get h]; simp [← aux] + | i+1 => + set_option backward.isDefEq.respectTransparency false in + rw [← List.take_concat_get h]; simp [← aux] theorem foldrM_eq_reverse_foldlM_toList [Monad m] {f : α → β → m β} {init : β} {xs : Array α} : xs.foldrM f init = xs.toList.reverse.foldlM (fun x y => f y x) init := by diff --git a/src/Init/Data/Array/Count.lean b/src/Init/Data/Array/Count.lean index 43106fe38c..86e6c5f0a2 100644 --- a/src/Init/Data/Array/Count.lean +++ b/src/Init/Data/Array/Count.lean @@ -117,11 +117,13 @@ grind_pattern Std.Internal.Array.not_of_countP_eq_zero_of_mem => xs.countP p, x theorem countP_replicate {a : α} {n : Nat} : countP p (replicate n a) = if p a then n else 0 := by simp [← List.toArray_replicate, List.countP_replicate] +set_option backward.isDefEq.respectTransparency false in theorem boole_getElem_le_countP {xs : Array α} {i : Nat} (h : i < xs.size) : (if p xs[i] then 1 else 0) ≤ xs.countP p := by rcases xs with ⟨xs⟩ simp [List.boole_getElem_le_countP] +set_option backward.isDefEq.respectTransparency false in @[grind =] theorem countP_set {xs : Array α} {i : Nat} {a : α} (h : i < xs.size) : (xs.set i a).countP p = xs.countP p - (if p xs[i] then 1 else 0) + (if p a then 1 else 0) := by diff --git a/src/Init/Data/Array/DecidableEq.lean b/src/Init/Data/Array/DecidableEq.lean index bb003760fe..a7a702c665 100644 --- a/src/Init/Data/Array/DecidableEq.lean +++ b/src/Init/Data/Array/DecidableEq.lean @@ -76,7 +76,7 @@ theorem isEqv_eq_decide (xs ys : Array α) (r) : simpa [isEqv_iff_rel] using h' @[simp, grind =] theorem isEqv_toList [BEq α] (xs ys : Array α) : (xs.toList.isEqv ys.toList r) = (xs.isEqv ys r) := by - simp [isEqv_eq_decide, List.isEqv_eq_decide, Array.size] + simp [isEqv_eq_decide, List.isEqv_eq_decide, Array.size]; rfl theorem eq_of_isEqv [DecidableEq α] (xs ys : Array α) (h : Array.isEqv xs ys (fun x y => x = y)) : xs = ys := by have ⟨h, h'⟩ := rel_of_isEqv h @@ -87,6 +87,7 @@ private theorem isEqvAux_self (r : α → α → Bool) (hr : ∀ a, r a a) (xs : induction i with | zero => simp [Array.isEqvAux] | succ i ih => + set_option backward.isDefEq.respectTransparency false in simp_all only [isEqvAux, Bool.and_self] theorem isEqv_self_beq [BEq α] [ReflBEq α] (xs : Array α) : Array.isEqv xs xs (· == ·) = true := by @@ -153,7 +154,7 @@ theorem beq_eq_decide [BEq α] (xs ys : Array α) : simp [BEq.beq, isEqv_eq_decide] @[simp, grind =] theorem beq_toList [BEq α] (xs ys : Array α) : (xs.toList == ys.toList) = (xs == ys) := by - simp [beq_eq_decide, List.beq_eq_decide, Array.size] + simp [beq_eq_decide, List.beq_eq_decide, Array.size]; rfl end Array diff --git a/src/Init/Data/Array/Find.lean b/src/Init/Data/Array/Find.lean index d60713d2c1..2a920ac588 100644 --- a/src/Init/Data/Array/Find.lean +++ b/src/Init/Data/Array/Find.lean @@ -425,6 +425,7 @@ theorem lt_findIdx_of_not {p : α → Bool} {xs : Array α} {i : Nat} (h : i < x simp only [Nat.not_lt] at f exact absurd (@findIdx_getElem _ p xs (Nat.lt_of_le_of_lt f h)) (h2 (xs.findIdx p) f) +set_option backward.isDefEq.respectTransparency false in /-- `xs.findIdx p = i` iff `p xs[i]` and `¬ p xs [j]` for all `j < i`. -/ theorem findIdx_eq {p : α → Bool} {xs : Array α} {i : Nat} (h : i < xs.size) : xs.findIdx p = i ↔ p xs[i] ∧ ∀ j (hji : j < i), p (xs[j]'(Nat.lt_trans hji h)) = false := by @@ -613,12 +614,12 @@ theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : Array α} {p q : α → Bo /-! ### findFinIdx? -/ @[grind =] -theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := by simp +theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := by simp; rfl @[grind =] theorem findFinIdx?_singleton {a : α} {p : α → Bool} : #[a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by - simp + simp; rfl -- We can't mark this as a `@[congr]` lemma since the head of the RHS is not `findFinIdx?`. theorem findFinIdx?_congr {p : α → Bool} {xs ys : Array α} (w : xs = ys) : @@ -714,6 +715,7 @@ theorem findFinIdx?_eq_bind_find?_finIdxOf? [BEq α] [LawfulBEq α] {xs : Array xs.findFinIdx? p = (xs.find? p).bind (xs.finIdxOf? ·) := by cases xs simp [List.findFinIdx?_eq_bind_find?_finIdxOf?] + rfl theorem findIdx_eq_getD_bind_find?_idxOf? [BEq α] [LawfulBEq α] {xs : Array α} {p : α → Bool} : xs.findIdx p = ((xs.find? p).bind (xs.idxOf? ·)).getD xs.size := by @@ -792,7 +794,7 @@ theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : Array α} {a : α} : xs.idxOf? a = (xs.finIdxOf? a).map (·.val) := by simp [idxOf?, finIdxOf?] -@[grind =] theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by simp +@[grind =] theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by simp; rfl @[simp, grind =] theorem finIdxOf?_eq_none_iff [BEq α] [LawfulBEq α] {xs : Array α} {a : α} : xs.finIdxOf? a = none ↔ a ∉ xs := by diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 65a19b9b50..dbaa5b0f4e 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -170,6 +170,7 @@ theorem getD_getElem? {xs : Array α} {i : Nat} {d : α} : @[simp] theorem getElem?_empty {i : Nat} : (#[] : Array α)[i]? = none := rfl +set_option backward.isDefEq.respectTransparency false in theorem getElem_push_lt {xs : Array α} {x : α} {i : Nat} (h : i < xs.size) : have : i < (xs.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt] (xs.push x)[i] = xs[i] := by @@ -895,7 +896,7 @@ theorem all_push {xs : Array α} {a : α} {p : α → Bool} : @[simp] theorem getElem_set_ne {xs : Array α} {i : Nat} (h' : i < xs.size) {v : α} {j : Nat} (pj : j < xs.size) (h : i ≠ j) : (xs.set i v)[j]'(by simp [*]) = xs[j] := by - simp only [set, ← getElem_toList, List.getElem_set_ne h] + simp only [set, ← getElem_toList, List.getElem_set_ne h]; rfl @[simp] theorem getElem?_set_ne {xs : Array α} {i : Nat} (h : i < xs.size) {v : α} {j : Nat} (ne : i ≠ j) : (xs.set i v)[j]? = xs[j]? := by @@ -2854,7 +2855,7 @@ theorem getElem?_extract {xs : Array α} {start stop : Nat} : · simp only [length_toList, size_extract, List.length_take, List.length_drop] omega · intro n h₁ h₂ - simp + simp; rfl @[simp] theorem extract_size {xs : Array α} : xs.extract 0 xs.size = xs := by apply ext @@ -3974,6 +3975,7 @@ theorem all_filterMap {xs : Array α} {f : α → Option β} {p : β → Bool} : · simp only [Id.run_pure] rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))] +set_option backward.isDefEq.respectTransparency false in @[simp, grind =] theorem toList_modify {xs : Array α} {f : α → α} {i : Nat} : (xs.modify i f).toList = xs.toList.modify i f := by apply List.ext_getElem @@ -4259,6 +4261,7 @@ private theorem getElem_ofFn_go {f : Fin n → α} {acc i k} (h : i ≤ n) (w₁ · simp omega +set_option backward.isDefEq.respectTransparency false in @[simp] theorem getElem_ofFn {f : Fin n → α} {i : Nat} (h : i < (ofFn f).size) : (ofFn f)[i] = f ⟨i, size_ofFn (f := f) ▸ h⟩ := by unfold ofFn @@ -4490,11 +4493,13 @@ theorem getElem?_push_eq {xs : Array α} {x : α} : (xs.push x)[xs.size]? = some cases xs simp +set_option backward.isDefEq.respectTransparency false in @[simp, grind =] theorem finIdxOf?_toList [BEq α] {a : α} {xs : Array α} : xs.toList.finIdxOf? a = (xs.finIdxOf? a).map (Fin.cast (by simp)) := by cases xs simp +set_option backward.isDefEq.respectTransparency false in @[simp, grind =] theorem findFinIdx?_toList {p : α → Bool} {xs : Array α} : xs.toList.findFinIdx? p = (xs.findFinIdx? p).map (Fin.cast (by simp)) := by cases xs @@ -4619,6 +4624,7 @@ namespace List as.toArray.unzip = Prod.map List.toArray List.toArray as.unzip := by ext1 <;> simp +set_option backward.isDefEq.respectTransparency false in @[simp, grind =] theorem firstM_toArray [Alternative m] {as : List α} {f : α → m β} : as.toArray.firstM f = as.firstM f := by unfold Array.firstM diff --git a/src/Init/Data/Array/MapIdx.lean b/src/Init/Data/Array/MapIdx.lean index 98defc1447..5afea12fe2 100644 --- a/src/Init/Data/Array/MapIdx.lean +++ b/src/Init/Data/Array/MapIdx.lean @@ -72,6 +72,7 @@ theorem mapFinIdx_spec {xs : Array α} {f : (i : Nat) → α → (h : i < xs.siz simp only [getElem?_def, size_mapFinIdx, getElem_mapFinIdx] split <;> simp_all +set_option backward.isDefEq.respectTransparency false in @[simp, grind =] theorem toList_mapFinIdx {xs : Array α} {f : (i : Nat) → α → (h : i < xs.size) → β} : (xs.mapFinIdx f).toList = xs.toList.mapFinIdx (fun i a h => f i a (by simpa)) := by apply List.ext_getElem <;> simp @@ -105,6 +106,7 @@ theorem mapIdx_spec {f : Nat → α → β} {xs : Array α} xs[i]?.map (f i) := by simp [getElem?_def, size_mapIdx, getElem_mapIdx] +set_option backward.isDefEq.respectTransparency false in @[simp, grind =] theorem toList_mapIdx {f : Nat → α → β} {xs : Array α} : (xs.mapIdx f).toList = xs.toList.mapIdx (fun i a => f i a) := by apply List.ext_getElem <;> simp diff --git a/src/Init/Data/Array/OfFn.lean b/src/Init/Data/Array/OfFn.lean index 88c58cc7d9..963cfb9549 100644 --- a/src/Init/Data/Array/OfFn.lean +++ b/src/Init/Data/Array/OfFn.lean @@ -41,6 +41,7 @@ theorem ofFn_succ {f : Fin (n+1) → α} : intro h₃ simp only [show i = n by omega] +set_option backward.isDefEq.respectTransparency false in theorem ofFn_add {n m} {f : Fin (n + m) → α} : ofFn f = (ofFn (fun i => f (i.castLE (Nat.le_add_right n m)))) ++ (ofFn (fun i => f (i.natAdd n))) := by induction m with @@ -107,6 +108,7 @@ theorem ofFnM_succ {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} : pure (as.push a)) := by simp [ofFnM, Fin.foldlM_succ_last] +set_option backward.isDefEq.respectTransparency false in theorem ofFnM_add {n m} [Monad m] [LawfulMonad m] {f : Fin (n + k) → m α} : ofFnM f = (do let as ← ofFnM fun i : Fin n => f (i.castLE (Nat.le_add_right n k)) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 0e56de9112..d0f20db667 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -2192,6 +2192,7 @@ def uppcRec {w} (x : BitVec w) (s : Nat) (hs : s < w) : Bool := | 0 => x.msb | i + 1 => x[w - 1 - i] || uppcRec x i (by omega) +set_option backward.isDefEq.respectTransparency false in /-- The unsigned parallel prefix of `x` at `s` is `true` if and only if x interpreted as a natural number is greater or equal than `2 ^ (w - 1 - (s - 1))`. -/ @[simp] diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index ac6ef10139..7200999731 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -1198,7 +1198,7 @@ let x' = x.extractLsb' 7 5 = _ _ 9 8 7 (decide (0 < len) && (decide (start + len ≤ w) && x.getMsbD (w - (start + len)))) := by - simp [BitVec.msb, getMsbD_extractLsb'] + simp [BitVec.msb, getMsbD_extractLsb']; rfl @[simp, grind =] theorem getElem_extract {hi lo : Nat} {x : BitVec n} {i : Nat} (h : i < hi - lo + 1) : (extractLsb hi lo x)[i] = getLsbD x (lo+i) := by @@ -1234,7 +1234,7 @@ let x' = x.extractLsb' 7 5 = _ _ 9 8 7 @[simp, grind =] theorem msb_extractLsb {hi lo : Nat} {x : BitVec w} : (extractLsb hi lo x).msb = (decide (max hi lo < w) && x.getMsbD (w - 1 - max hi lo)) := by - simp [BitVec.msb] + simp [BitVec.msb]; rfl theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h : len > 0) : x.extractLsb' start len = (x.extractLsb (len - 1 + start) start).cast (by omega) := by @@ -2771,8 +2771,9 @@ theorem msb_append {x : BitVec w} {y : BitVec v} : @[simp] theorem append_zero_width (x : BitVec w) (y : BitVec 0) : x ++ y = x := by ext i ih rw [getElem_append] -- Why does this not work with `simp [getElem_append]`? - simp + simp; rfl +set_option backward.isDefEq.respectTransparency false in @[grind =] theorem toInt_append {x : BitVec n} {y : BitVec m} : (x ++ y).toInt = if n == 0 then y.toInt else (2 ^ m) * x.toInt + y.toNat := by @@ -5278,6 +5279,7 @@ theorem and_one_eq_setWidth_ofBool_getLsbD {x : BitVec w} : theorem replicate_zero {x : BitVec w} : x.replicate 0 = 0#0 := by simp [replicate] +set_option backward.isDefEq.respectTransparency false in @[simp, grind =] theorem replicate_one {w : Nat} {x : BitVec w} : (x.replicate 1) = x.cast (by rw [Nat.mul_one]) := by @@ -5329,6 +5331,7 @@ theorem append_assoc {x₁ : BitVec w₁} {x₂ : BitVec w₂} {x₃ : BitVec w theorem append_assoc' {x₁ : BitVec w₁} {x₂ : BitVec w₂} {x₃ : BitVec w₃} : (x₁ ++ (x₂ ++ x₃)) = ((x₁ ++ x₂) ++ x₃).cast (by omega) := by simp [append_assoc] +set_option backward.isDefEq.respectTransparency false in theorem replicate_append_self {x : BitVec w} : x ++ x.replicate n = (x.replicate n ++ x).cast (by omega) := by induction n with diff --git a/src/Init/Data/ByteArray/Lemmas.lean b/src/Init/Data/ByteArray/Lemmas.lean index 8b0d9d3302..02cc3efb3d 100644 --- a/src/Init/Data/ByteArray/Lemmas.lean +++ b/src/Init/Data/ByteArray/Lemmas.lean @@ -111,13 +111,13 @@ theorem getElem_eq_getElem_data {a : ByteArray} {i : Nat} {h : i < a.size} : theorem getElem_append_left {i : Nat} {a b : ByteArray} {h : i < (a ++ b).size} (hlt : i < a.size) : (a ++ b)[i] = a[i] := by simp only [getElem_eq_getElem_data, data_append] - rw [Array.getElem_append_left (by simpa)] + rw [Array.getElem_append_left (by simpa)]; rfl theorem getElem_append_right {i : Nat} {a b : ByteArray} {h : i < (a ++ b).size} (hle : a.size ≤ i) : (a ++ b)[i] = b[i - a.size]'(by simp_all; omega) := by simp only [getElem_eq_getElem_data, data_append] rw [Array.getElem_append_right (by simpa)] - simp + simp; rfl @[simp] theorem _root_.List.getElem_toByteArray {l : List UInt8} {i : Nat} {h : i < l.toByteArray.size} : @@ -223,7 +223,7 @@ theorem getElem_extract_aux {xs : ByteArray} {start stop : Nat} (h : i < (xs.ext theorem getElem_extract {i : Nat} {b : ByteArray} {start stop : Nat} (h) : (b.extract start stop)[i]'h = b[start + i]'(getElem_extract_aux h) := by - simp [getElem_eq_getElem_data] + simp [getElem_eq_getElem_data]; rfl theorem extract_eq_extract_left {a : ByteArray} {i i' j : Nat} : a.extract i j = a.extract i' j ↔ min j a.size - i = min j a.size - i' := by @@ -236,25 +236,25 @@ theorem extract_add_one {a : ByteArray} {i : Nat} (ha : i + 1 ≤ a.size) : omega · rename_i j hj hj' obtain rfl : j = 0 := by simpa using hj' - simp [ByteArray.getElem_eq_getElem_data] + simp [ByteArray.getElem_eq_getElem_data]; rfl theorem extract_add_two {a : ByteArray} {i : Nat} (ha : i + 2 ≤ a.size) : a.extract i (i + 2) = [a[i], a[i + 1]].toByteArray := by rw [extract_eq_extract_append_extract (i + 1) (by simp) (by omega), extract_add_one (by omega), extract_add_one (by omega)] - simp [← List.toByteArray_append] + simp [← List.toByteArray_append]; rfl theorem extract_add_three {a : ByteArray} {i : Nat} (ha : i + 3 ≤ a.size) : a.extract i (i + 3) = [a[i], a[i + 1], a[i + 2]].toByteArray := by rw [extract_eq_extract_append_extract (i + 1) (by simp) (by omega), extract_add_one (by omega), extract_add_two (by omega)] - simp [← List.toByteArray_append] + simp [← List.toByteArray_append]; rfl theorem extract_add_four {a : ByteArray} {i : Nat} (ha : i + 4 ≤ a.size) : a.extract i (i + 4) = [a[i], a[i + 1], a[i + 2], a[i + 3]].toByteArray := by rw [extract_eq_extract_append_extract (i + 1) (by simp) (by omega), extract_add_one (by omega), extract_add_three (by omega)] - simp [← List.toByteArray_append] + simp [← List.toByteArray_append]; rfl theorem append_assoc {a b c : ByteArray} : a ++ b ++ c = a ++ (b ++ c) := by ext1 diff --git a/src/Init/Data/Fin/Fold.lean b/src/Init/Data/Fin/Fold.lean index e70887f13b..562bfc29c5 100644 --- a/src/Init/Data/Fin/Fold.lean +++ b/src/Init/Data/Fin/Fold.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: François G. Dorais -/ module - prelude public import Init.Control.Lawful.Basic public import Init.Ext @@ -13,7 +12,7 @@ import Init.Data.Nat.Lemmas import Init.Omega import Init.TacticsExtra import Init.WFTactics - +import Init.Hints public section namespace Fin @@ -165,7 +164,7 @@ theorem foldlM_add [Monad m] [LawfulMonad m] (f : α → Fin (n + k) → m α) : simp | succ k ih => funext x - simp [foldlM_succ_last, ← Nat.add_assoc, ih] + simp [foldlM_succ_last, ← Nat.add_assoc, ih]; rfl /-! ### foldrM -/ @@ -223,7 +222,7 @@ theorem foldrM_add [Monad m] [LawfulMonad m] (f : Fin (n + k) → α → m α) : simp | succ k ih => funext x - simp [foldrM_succ_last, ← Nat.add_assoc, ih] + simp [foldrM_succ_last, ← Nat.add_assoc, ih]; rfl /-! ### foldl -/ @@ -269,7 +268,7 @@ theorem foldl_add (f : α → Fin (n + m) → α) (x) : (foldl n (fun x i => f x (i.castLE (Nat.le_add_right n m))) x):= by induction m with | zero => simp - | succ m ih => simp [foldl_succ_last, ih, ← Nat.add_assoc] + | succ m ih => simp [foldl_succ_last, ih, ← Nat.add_assoc]; rfl theorem foldl_eq_foldlM (f : α → Fin n → α) (x) : foldl n f x = (foldlM (m := Id) n (pure <| f · ·) x).run := by @@ -322,7 +321,7 @@ theorem foldr_add (f : Fin (n + m) → α → α) (x) : (foldr m (fun i => f (i.natAdd n)) x) := by induction m generalizing x with | zero => simp - | succ m ih => simp [foldr_succ_last, ih, ← Nat.add_assoc] + | succ m ih => simp [foldr_succ_last, ih, ← Nat.add_assoc]; rfl theorem foldr_eq_foldrM (f : Fin n → α → α) (x) : foldr n f x = (foldrM (m := Id) n (pure <| f · ·) x).run := by diff --git a/src/Init/Data/Fin/Iterate.lean b/src/Init/Data/Fin/Iterate.lean index 9e19561829..6434041503 100644 --- a/src/Init/Data/Fin/Iterate.lean +++ b/src/Init/Data/Fin/Iterate.lean @@ -4,14 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joe Hendrix -/ module - prelude public import Init.Data.Fin.Basic import Init.PropLemmas import Init.WFTactics - +import Init.Hints public section - namespace Fin /-- diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean index 34159ce285..224da8e746 100644 --- a/src/Init/Data/Fin/Lemmas.lean +++ b/src/Init/Data/Fin/Lemmas.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro, Leonardo de Moura -/ module - prelude public import Init.Ext public import Init.Data.Nat.Div.Basic @@ -15,7 +14,7 @@ import Init.Data.Nat.Lemmas import Init.Data.Nat.Linear import Init.Omega import Init.TacticsExtra - +import Init.Hints @[expose] public section open Std @@ -998,7 +997,7 @@ For the induction: @[simp, grind =] theorem reverseInduction_last {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ} : (reverseInduction zero succ (Fin.last n) : motive (Fin.last n)) = zero := by - rw [reverseInduction, reverseInduction.go]; simp + rw [reverseInduction, reverseInduction.go]; simp; rfl private theorem reverseInduction_castSucc_aux {n : Nat} {motive : Fin (n + 1) → Sort _} {succ} (i : Fin n) (j : Nat) (h) (h2 : i.1 < j) (zero : motive ⟨j, h⟩) : @@ -1009,9 +1008,9 @@ private theorem reverseInduction_castSucc_aux {n : Nat} {motive : Fin (n + 1) | succ j ih => rw [reverseInduction.go, dif_neg (by exact Nat.ne_of_lt h2)] by_cases hij : i = j - · subst hij; simp [reverseInduction.go] - dsimp only - rw [ih _ _ (by omega), eq_comm, reverseInduction.go, dif_neg (by change i.1 + 1 ≠ _; omega)] + · subst hij; simp [reverseInduction.go]; rfl + · dsimp only + rw [ih _ _ (by omega), eq_comm, reverseInduction.go, dif_neg (by change i.1 + 1 ≠ _; omega)] @[simp, grind =] theorem reverseInduction_castSucc {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ} (i : Fin n) : reverseInduction (motive := motive) zero succ (castSucc i) = diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean index b2811ecdf3..fc919fe55b 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean @@ -750,6 +750,7 @@ theorem Iter.anyM_filterMapM {α β β' : Type w} {m : Type w → Type w'} simp only [filterMapM_eq_toIter_filterMapM_toIterM, IterM.anyM_filterMapM] rfl +set_option backward.isDefEq.respectTransparency false in -- There is hope to generalize the following theorem as soon there is a `Shrink` type. /-- This lemma expresses `Iter.anyM` in terms of `IterM.anyM`. diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean index 5d1bf63d65..af874ee622 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean @@ -232,6 +232,7 @@ public theorem Iter.toArray_flatMapM {α α₂ β γ : Type w} {m : Type w → T (it₁.flatMapM f).toArray = Array.flatten <$> (it₁.mapM fun b => do (← f b).toArray).toArray := by simp [flatMapM, toArray_flatMapAfterM] +set_option backward.isDefEq.respectTransparency false in public theorem Iter.toList_flatMapAfter {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ] [Finite α Id] [Finite α₂ Id] {f : β → Iter (α := α₂) γ} {it₁ : Iter (α := α) β} {it₂ : Option (Iter (α := α₂) γ)} : @@ -242,6 +243,7 @@ public theorem Iter.toList_flatMapAfter {α α₂ β γ : Type w} [Iterator α I simp only [flatMapAfter, Iter.toList, toIterM_toIter, IterM.toList_flatMapAfter] cases it₂ <;> simp [map, IterM.toList_map_eq_toList_mapM, - IterM.toList_map] +set_option backward.isDefEq.respectTransparency false in public theorem Iter.toArray_flatMapAfter {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ] [Finite α Id] [Finite α₂ Id] {f : β → Iter (α := α₂) γ} {it₁ : Iter (α := α) β} {it₂ : Option (Iter (α := α₂) γ)} : diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean index 05c9113137..0831d40b5e 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean @@ -600,6 +600,7 @@ theorem IterM.toList_map_mapM {α β γ δ : Type w} toList_filterMapM_mapM] congr <;> simp +set_option backward.isDefEq.respectTransparency false in @[simp] theorem IterM.toList_filterMapWithPostcondition {α β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] @@ -623,6 +624,7 @@ theorem IterM.toList_filterMapWithPostcondition {α β γ : Type w} {m : Type w · simp [ihs ‹_›, heq] · simp [heq] +set_option backward.isDefEq.respectTransparency false in @[simp] theorem IterM.toList_mapWithPostcondition {α β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α Id β] [Finite α Id] @@ -643,6 +645,7 @@ theorem IterM.toList_mapWithPostcondition {α β γ : Type w} {m : Type w → Ty · simp [ihs ‹_›, heq] · simp [heq] +set_option backward.isDefEq.respectTransparency false in @[simp] theorem IterM.toList_filterMapM {α β γ : Type w} {m : Type w → Type w'} [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] @@ -652,6 +655,7 @@ theorem IterM.toList_filterMapM {α β γ : Type w} {m : Type w → Type w'} simp [toList_filterMapM_eq_toList_filterMapWithPostcondition, toList_filterMapWithPostcondition, PostconditionT.attachLift, PostconditionT.run_eq_map, WeaklyLawfulMonadAttach.map_attach] +set_option backward.isDefEq.respectTransparency false in @[simp] theorem IterM.toList_mapM {α β γ : Type w} {m : Type w → Type w'} [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] @@ -1297,6 +1301,7 @@ theorem IterM.forIn_filterMap rw [filterMap, forIn_filterMapWithPostcondition] simp [PostconditionT.run_eq_map] +set_option backward.isDefEq.respectTransparency false in theorem IterM.forIn_mapWithPostcondition [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o] diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FlatMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FlatMap.lean index 245e3453e5..c45bad0c10 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FlatMap.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FlatMap.lean @@ -36,7 +36,7 @@ theorem IterM.step_flattenAfter {α α₂ β : Type w} {m : Type w → Type w'} cases it₂ all_goals · apply bind_congr; intro step - cases step.inflate using PlausibleIterStep.casesOn <;> simp [IterM.flattenAfter] + cases step.inflate using PlausibleIterStep.casesOn <;> simp [IterM.flattenAfter] <;> rfl namespace Iterators.Types diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean index 247b7c6db7..a8c24cd27e 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean @@ -29,7 +29,7 @@ theorem IterM.step_uLift [Iterator α m β] [Monad n] {it : IterM (α := α) m | .done h => return .deflate (.done ⟨_, h, rfl⟩)) := by simp only [IterM.step, Iterator.step, IterM.uLift] apply bind_congr; intro step - split <;> simp [Types.ULiftIterator.Monadic.modifyStep, *] + split <;> simp [Types.ULiftIterator.Monadic.modifyStep, *] <;> rfl @[simp] theorem IterM.toList_uLift [Iterator α m β] [Monad m] [Monad n] {it : IterM (α := α) m β} diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean b/src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean index 65c8f3d6cf..43d70a9db2 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean @@ -26,6 +26,7 @@ theorem Iter.uLift_eq_toIter_uLift_toIterM {it : Iter (α := α) β} : it.uLift = (it.toIterM.uLift Id).toIter := rfl +set_option backward.isDefEq.respectTransparency false in theorem Iter.step_uLift [Iterator α Id β] {it : Iter (α := α) β} : it.uLift.step = match it.step with | .yield it' out h => .yield it'.uLift (.up out) ⟨_, h, rfl⟩ @@ -38,6 +39,7 @@ theorem Iter.step_uLift [Iterator α Id β] {it : Iter (α := α) β} : PlausibleIterStep.done, pure_bind] cases it.toIterM.step.run.inflate using PlausibleIterStep.casesOn <;> simp +set_option backward.isDefEq.respectTransparency false in @[simp] theorem Iter.toList_uLift [Iterator α Id β] {it : Iter (α := α) β} [Finite α Id] : @@ -59,6 +61,7 @@ theorem Iter.toArray_uLift [Iterator α Id β] {it : Iter (α := α) β} rw [← toArray_toList, ← toArray_toList, toList_uLift] simp [-toArray_toList] +set_option backward.isDefEq.respectTransparency false in @[simp] theorem Iter.length_uLift [Iterator α Id β] {it : Iter (α := α) β} [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] : diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean index 62c9ae918e..acf94566c7 100644 --- a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean +++ b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean @@ -398,7 +398,7 @@ theorem Iter.fold_eq_fold_toIterM {α β : Type w} {γ : Type w} [Iterator α Id [Finite α Id] [IteratorLoop α Id Id] {f : γ → β → γ} {init : γ} {it : Iter (α := α) β} : it.fold (init := init) f = (it.toIterM.fold (init := init) f).run := by - rw [fold_eq_foldM, foldM_eq_foldM_toIterM, IterM.fold_eq_foldM] + rw [fold_eq_foldM, foldM_eq_foldM_toIterM, IterM.fold_eq_foldM]; rfl @[simp] theorem Iter.forIn_pure_yield_eq_fold {α β : Type w} {γ : Type x} [Iterator α Id β] diff --git a/src/Init/Data/Iterators/Lemmas/Producers/List.lean b/src/Init/Data/Iterators/Lemmas/Producers/List.lean index 32a61c1306..7ea26c0745 100644 --- a/src/Init/Data/Iterators/Lemmas/Producers/List.lean +++ b/src/Init/Data/Iterators/Lemmas/Producers/List.lean @@ -23,6 +23,7 @@ open Std Std.Iterators variable {β : Type w} +set_option backward.isDefEq.respectTransparency false in @[simp] theorem List.step_iter_nil : (([] : List β).iter).step = ⟨.done, rfl⟩ := by @@ -31,7 +32,7 @@ theorem List.step_iter_nil : @[simp] theorem List.step_iter_cons {x : β} {xs : List β} : ((x :: xs).iter).step = ⟨.yield xs.iter x, rfl⟩ := by - simp [List.iter, List.iterM, IterM.toIter, Iter.step_eq] + simp [List.iter, List.iterM, IterM.toIter, Iter.step_eq]; rfl @[simp, grind =] theorem List.toArray_iter {l : List β} : diff --git a/src/Init/Data/Iterators/Lemmas/Producers/Monadic/List.lean b/src/Init/Data/Iterators/Lemmas/Producers/Monadic/List.lean index 58ed0a95c2..5924c76916 100644 --- a/src/Init/Data/Iterators/Lemmas/Producers/Monadic/List.lean +++ b/src/Init/Data/Iterators/Lemmas/Producers/Monadic/List.lean @@ -31,7 +31,7 @@ theorem List.step_iterM_nil : @[simp] theorem List.step_iterM_cons {x : β} {xs : List β} : ((x :: xs).iterM m).step = pure (.deflate ⟨.yield (xs.iterM m) x, rfl⟩) := by - simp only [List.iterM, IterM.step, Iterator.step] + simp only [List.iterM, IterM.step, Iterator.step]; rfl theorem List.step_iterM {l : List β} : (l.iterM m).step = match l with diff --git a/src/Init/Data/List/Count.lean b/src/Init/Data/List/Count.lean index 514beca269..8decc4d648 100644 --- a/src/Init/Data/List/Count.lean +++ b/src/Init/Data/List/Count.lean @@ -132,7 +132,9 @@ theorem boole_getElem_le_countP {p : α → Bool} {l : List α} {i : Nat} (h : i | nil => simp at h | cons x l ih => cases i with - | zero => simp [countP_cons] + | zero => + set_option backward.isDefEq.respectTransparency false in + simp [countP_cons] | succ i => simp only [length_cons, add_one_lt_add_one_iff] at h simp only [getElem_cons_succ, countP_cons] @@ -263,7 +265,9 @@ theorem count_eq_length_filter {a : α} {l : List α} : count a l = (filter (· theorem count_tail : ∀ {l : List α} {a : α}, l.tail.count a = l.count a - if l.head? == some a then 1 else 0 | [], a => by simp - | _ :: _, a => by simp [count_cons] + | _ :: _, a => by + set_option backward.isDefEq.respectTransparency false in + simp [count_cons] theorem count_le_length {a : α} {l : List α} : count a l ≤ l.length := countP_le_length diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean index 57f9ccb471..92ed75323a 100644 --- a/src/Init/Data/List/Find.lean +++ b/src/Init/Data/List/Find.lean @@ -654,6 +654,7 @@ theorem lt_findIdx_of_not {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs simp only [Nat.not_lt] at f exact absurd (@findIdx_getElem _ p xs (Nat.lt_of_le_of_lt f h)) (h2 (xs.findIdx p) f) +set_option backward.isDefEq.respectTransparency false in /-- `xs.findIdx p = i` iff `p xs[i]` and `¬ p xs [j]` for all `j < i`. -/ theorem findIdx_eq {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs.length) : xs.findIdx p = i ↔ p xs[i] ∧ ∀ j (hji : j < i), p (xs[j]'(Nat.lt_trans hji h)) = false := by @@ -1038,7 +1039,7 @@ theorem findFinIdx?_append {xs ys : List α} {p : α → Bool} : @[simp, grind =] theorem findFinIdx?_singleton {a : α} {p : α → Bool} : [a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by - simp [findFinIdx?_cons, findFinIdx?_nil] + simp [findFinIdx?_cons, findFinIdx?_nil]; rfl @[simp, grind =] theorem findFinIdx?_eq_none_iff {l : List α} {p : α → Bool} : l.findFinIdx? p = none ↔ ∀ x ∈ l, ¬ p x := by @@ -1080,6 +1081,7 @@ theorem isNone_findFinIdx? {l : List α} {p : α → Bool} : induction l with | nil => simp | cons a l ih => + set_option backward.isDefEq.respectTransparency false in simp [hf, findFinIdx?_cons] split <;> simp [ih, Function.comp_def] diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 0ebeacbec0..0b775dbdfc 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -3525,7 +3525,7 @@ theorem getElem?_insert_succ {l : List α} {a : α} {i : Nat} : · split · rfl · have h' : i - 1 < l.length := Nat.lt_of_le_of_lt (Nat.pred_le _) h - simp [h'] + simp [h']; rfl theorem head?_insert {l : List α} {a : α} : (l.insert a).head? = some (if h : a ∈ l then l.head (ne_nil_of_mem h) else a) := by @@ -3679,11 +3679,13 @@ theorem get_of_eq {l l' : List α} (h : l = l') (i : Fin l.length) : theorem getElem!_nil [Inhabited α] {n : Nat} : ([] : List α)[n]! = default := rfl theorem getElem!_cons_zero [Inhabited α] {l : List α} : (a::l)[0]! = a := by - rw [getElem!_pos] <;> simp + rw [getElem!_pos]; rfl; simp theorem getElem!_cons_succ [Inhabited α] {l : List α} : (a::l)[i+1]! = l[i]! := by by_cases h : i < l.length - · rw [getElem!_pos, getElem!_pos] <;> simp_all [Nat.succ_lt_succ_iff] + · rw [getElem!_pos, getElem!_pos] + · rfl + · simp; apply Nat.succ_lt_succ; assumption · rw [getElem!_neg, getElem!_neg] <;> simp_all [Nat.succ_lt_succ_iff] theorem getElem!_of_getElem? [Inhabited α] : ∀ {l : List α} {i : Nat}, l[i]? = some a → l[i]! = a diff --git a/src/Init/Data/List/MapIdx.lean b/src/Init/Data/List/MapIdx.lean index 37501e4081..a5ee541d66 100644 --- a/src/Init/Data/List/MapIdx.lean +++ b/src/Init/Data/List/MapIdx.lean @@ -350,6 +350,7 @@ theorem getElem?_mapIdx_go : ∀ {l : List α} {acc : Array β} {i : Nat}, | [], acc, i => by simp only [mapIdx.go, getElem?_def, Array.length_toList, ← Array.getElem_toList, length_nil, Nat.not_lt_zero, ↓reduceDIte, Option.map_none] + rfl | a :: l, acc, i => by rw [mapIdx.go, getElem?_mapIdx_go] simp only [Array.size_push] diff --git a/src/Init/Data/List/MinMaxIdx.lean b/src/Init/Data/List/MinMaxIdx.lean index 7bd616ca0d..89c12e499a 100644 --- a/src/Init/Data/List/MinMaxIdx.lean +++ b/src/Init/Data/List/MinMaxIdx.lean @@ -410,6 +410,7 @@ private theorem minIdxOn_append_aux [LE β] [DecidableLE β] match xs with | [] => simp [minIdxOn_cons_aux (xs := ys) ‹_›] | z :: zs => + set_option backward.isDefEq.respectTransparency false in simp +singlePass only [cons_append] simp only [minIdxOn_cons_aux (xs := z :: zs ++ ys) (by simp), ih (by simp), minIdxOn_cons_aux (xs := z :: zs) (by simp), combineMinIdxOn_assoc] diff --git a/src/Init/Data/List/Nat/Count.lean b/src/Init/Data/List/Nat/Count.lean index 94e1a55ad7..d8174e3621 100644 --- a/src/Init/Data/List/Nat/Count.lean +++ b/src/Init/Data/List/Nat/Count.lean @@ -25,6 +25,7 @@ namespace List open Nat +set_option backward.isDefEq.respectTransparency false in @[grind =] theorem countP_set {p : α → Bool} {l : List α} {i : Nat} {a : α} (h : i < l.length) : (l.set i a).countP p = l.countP p - (if p l[i] then 1 else 0) + (if p a then 1 else 0) := by diff --git a/src/Init/Data/List/Nat/Pairwise.lean b/src/Init/Data/List/Nat/Pairwise.lean index 97eb00fcd7..511a51b3e5 100644 --- a/src/Init/Data/List/Nat/Pairwise.lean +++ b/src/Init/Data/List/Nat/Pairwise.lean @@ -53,10 +53,12 @@ theorem sublist_eq_map_getElem {l l' : List α} (h : l' <+ l) : ∃ is : List (F | cons _ _ IH => let ⟨is, IH⟩ := IH refine ⟨is.map (·.succ), ?_⟩ + set_option backward.isDefEq.respectTransparency false in simpa [Function.comp_def, pairwise_map] | cons₂ _ _ IH => rcases IH with ⟨is,IH⟩ refine ⟨⟨0, by simp [Nat.zero_lt_succ]⟩ :: is.map (·.succ), ?_⟩ + set_option backward.isDefEq.respectTransparency false in simp [Function.comp_def, pairwise_map, IH, ← get_eq_getElem, get_cons_zero, get_cons_succ'] set_option linter.listVariables false in diff --git a/src/Init/Data/List/OfFn.lean b/src/Init/Data/List/OfFn.lean index f07e3ac75d..51766ca7a4 100644 --- a/src/Init/Data/List/OfFn.lean +++ b/src/Init/Data/List/OfFn.lean @@ -98,7 +98,9 @@ theorem ofFn_add {n m} {f : Fin (n + m) → α} : ofFn f = (ofFn fun i => f (i.castLE (Nat.le_add_right n m))) ++ (ofFn fun i => f (i.natAdd n)) := by induction m with | zero => simp - | succ m ih => simp [-ofFn_succ, ofFn_succ_last, ih] + | succ m ih => + set_option backward.isDefEq.respectTransparency false in + simp [-ofFn_succ, ofFn_succ_last, ih] @[simp] theorem ofFn_eq_nil_iff {f : Fin n → α} : ofFn f = [] ↔ n = 0 := by @@ -154,8 +156,9 @@ theorem ofFnM_add {n m} [Monad m] [LawfulMonad m] {f : Fin (n + k) → m α} : pure (as ++ bs)) := by induction k with | zero => simp - | succ k ih => simp [ofFnM_succ_last, ih] - + | succ k ih => + set_option backward.isDefEq.respectTransparency false in + simp [ofFnM_succ_last, ih] end List diff --git a/src/Init/Data/List/Sort/Basic.lean b/src/Init/Data/List/Sort/Basic.lean index 3b62966c7f..74e3845a99 100644 --- a/src/Init/Data/List/Sort/Basic.lean +++ b/src/Init/Data/List/Sort/Basic.lean @@ -64,6 +64,7 @@ def MergeSort.Internal.splitInTwo (l : { l : List α // l.length = n }) : open MergeSort.Internal in set_option linter.unusedVariables false in +set_option backward.isDefEq.respectTransparency false in /-- A stable merge sort. diff --git a/src/Init/Data/List/Sort/Impl.lean b/src/Init/Data/List/Sort/Impl.lean index 41e13fca20..e0044cf21d 100644 --- a/src/Init/Data/List/Sort/Impl.lean +++ b/src/Init/Data/List/Sort/Impl.lean @@ -182,14 +182,14 @@ private theorem mergeSortTR_run_eq_mergeSort : {n : Nat} → (l : { l : List α simp only [mergeSortTR.run, mergeSortTR.run, mergeSort] rw [merge_eq_mergeTR] rw [mergeSortTR_run_eq_mergeSort, mergeSortTR_run_eq_mergeSort] + rfl -- We don't make this a `@[csimp]` lemma because `mergeSort_eq_mergeSortTR₂` is faster. theorem mergeSort_eq_mergeSortTR : @mergeSort = @mergeSortTR := by funext rw [mergeSortTR, mergeSortTR_run_eq_mergeSort] --- This mutual block is unfortunately quite slow to elaborate. -set_option maxHeartbeats 400000 in +set_option backward.isDefEq.respectTransparency false in mutual private theorem mergeSortTR₂_run_eq_mergeSort : {n : Nat} → (l : { l : List α // l.length = n }) → mergeSortTR₂.run le l = mergeSort l.1 le | 0, ⟨[], _⟩ diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean index 34c8352fd6..d6a052e7fd 100644 --- a/src/Init/Data/List/ToArray.lean +++ b/src/Init/Data/List/ToArray.lean @@ -280,6 +280,7 @@ theorem findRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : Lis simp only [forIn_cons, find?] by_cases f a <;> simp_all +set_option backward.isDefEq.respectTransparency false in private theorem findFinIdx?_loop_toArray (w : l' = l.drop j) : Array.findFinIdx?.loop p l.toArray j = List.findFinIdx?.go p l l' j h := by unfold findFinIdx?.loop @@ -316,6 +317,7 @@ termination_by l.length - j rw [Array.findIdx?_eq_map_findFinIdx?_val, findIdx?_eq_map_findFinIdx?_val] simp [Array.size] +set_option backward.isDefEq.respectTransparency false in private theorem idxAuxOf_toArray [BEq α] (a : α) (l : List α) (j : Nat) (w : l' = l.drop j) (h) : l.toArray.idxOfAux a j = findFinIdx?.go (fun x => x == a) l l' j h := by unfold idxOfAux @@ -361,6 +363,7 @@ termination_by l.length - j as.toArray.idxOf a = as.idxOf a := by rw [Array.idxOf, findIdx_toArray, idxOf] +set_option backward.isDefEq.respectTransparency false in theorem isPrefixOfAux_toArray_succ [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : Nat) : Array.isPrefixOfAux l₁.toArray l₂.toArray hle (i + 1) = Array.isPrefixOfAux l₁.tail.toArray l₂.tail.toArray (by simp; omega) i := by @@ -586,7 +589,7 @@ theorem flatMap_toArray_cons {β} (f : α → Array β) (a : α) (as : List α) @[simp, grind =] 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 apply ext' - simp + simp; rfl @[simp, grind =] theorem eraseIdx_toArray (l : List α) (i : Nat) (h : i < l.toArray.size) : l.toArray.eraseIdx i h = (l.eraseIdx i).toArray := by @@ -616,13 +619,13 @@ decreasing_by @[simp, grind =] theorem eraseP_toArray {as : List α} {p : α → Bool} : as.toArray.eraseP p = (as.eraseP p).toArray := by rw [Array.eraseP, List.eraseP_eq_eraseIdx, findFinIdx?_toArray] - split <;> simp [*, findIdx?_eq_map_findFinIdx?_val] + split <;> simp [*, findIdx?_eq_map_findFinIdx?_val] <;> rfl @[simp, grind =] theorem erase_toArray [BEq α] {as : List α} {a : α} : as.toArray.erase a = (as.erase a).toArray := by rw [Array.erase, finIdxOf?_toArray, List.erase_eq_eraseIdx] rw [idxOf?_eq_map_finIdxOf?_val] - split <;> simp_all + split <;> simp_all <;> rfl private theorem insertIdx_loop_toArray (i : Nat) (l : List α) (j : Nat) (hj : j < l.toArray.size) (h : i ≤ j) : insertIdx.loop i l.toArray ⟨j, hj⟩ = (l.take i ++ l[j] :: (l.take j).drop i ++ l.drop (j + 1)).toArray := by @@ -639,10 +642,10 @@ private theorem insertIdx_loop_toArray (i : Nat) (l : List α) (j : Nat) (hj : j getElem_set_self, take_set_of_le (j := j - 1) (by omega), take_set_of_le (j := j - 1) (by omega), take_eq_append_getElem_of_pos (by omega) hj, drop_append_of_le_length (by simp; omega)] - simp only [append_assoc, cons_append, nil_append, append_cancel_right_eq] + simp only [append_assoc, cons_append, nil_append] cases i with - | zero => simp - | succ i => rw [take_set_of_le (by omega)] + | zero => simp; rfl + | succ i => rw [take_set_of_le (by omega)]; rfl · simp only [Nat.not_lt] at h' have : i = j := by omega subst this diff --git a/src/Init/Data/Nat/Fold.lean b/src/Init/Data/Nat/Fold.lean index d7b6760e83..be23ade521 100644 --- a/src/Init/Data/Nat/Fold.lean +++ b/src/Init/Data/Nat/Fold.lean @@ -400,6 +400,7 @@ theorem dfold_add induction m with | zero => simp; rfl | succ m ih => + set_option backward.isDefEq.respectTransparency false in simp [dfold_congr (Nat.add_assoc n m 1).symm, ih] @[simp] theorem dfoldRev_zero @@ -434,7 +435,9 @@ theorem dfoldRev_add (dfoldRev m (α := fun i h => α (n + i)) (fun i h => f (n + i) (by omega)) init) := by induction m with | zero => simp; rfl - | succ m ih => simp [← Nat.add_assoc, ih] + | succ m ih => + set_option backward.isDefEq.respectTransparency false in + simp [← Nat.add_assoc, ih] end Nat diff --git a/src/Init/Data/Option/Attach.lean b/src/Init/Data/Option/Attach.lean index 39cc812639..f862c5b934 100644 --- a/src/Init/Data/Option/Attach.lean +++ b/src/Init/Data/Option/Attach.lean @@ -444,6 +444,7 @@ instance : MonadAttach Option where CanReturn x a := x = some a attach x := x.attach +set_option backward.isDefEq.respectTransparency false in public instance : LawfulMonadAttach Option where map_attach {α} x := by simp [MonadAttach.attach] canReturn_map_imp {α P x a} := by @@ -455,6 +456,7 @@ end Option namespace OptionT +set_option backward.isDefEq.respectTransparency false in public instance [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] : WeaklyLawfulMonadAttach (OptionT m) where map_attach {α} x := by diff --git a/src/Init/Data/Order/PackageFactories.lean b/src/Init/Data/Order/PackageFactories.lean index 81c7e9cea6..44728a0615 100644 --- a/src/Init/Data/Order/PackageFactories.lean +++ b/src/Init/Data/Order/PackageFactories.lean @@ -794,6 +794,7 @@ automatically. If it fails, it is necessary to provide some of the fields manual @[expose] public def LinearOrderPackage.ofOrd (α : Type u) (args : Packages.LinearOrderOfOrdArgs α := by exact {}) : LinearOrderPackage α := + set_option backward.isDefEq.respectTransparency false in letI := LinearPreorderPackage.ofOrd α args.toLinearPreorderOfOrdArgs haveI : LawfulEqOrd α := ⟨args.eq_of_compare _ _⟩ letI : Min α := args.min diff --git a/src/Init/Data/Range/Polymorphic/RangeIterator.lean b/src/Init/Data/Range/Polymorphic/RangeIterator.lean index 9b00655978..f6b42833d0 100644 --- a/src/Init/Data/Range/Polymorphic/RangeIterator.lean +++ b/src/Init/Data/Range/Polymorphic/RangeIterator.lean @@ -102,7 +102,7 @@ theorem Iterator.Monadic.isPlausibleStep_iff [UpwardEnumerable α] [LE α] [Deci theorem Iterator.Monadic.step_eq_step [UpwardEnumerable α] [LE α] [DecidableLE α] {it : IterM (α := Rxc.Iterator α) Id α} : Std.Iterator.step it = pure (.deflate ⟨Iterator.Monadic.step it, isPlausibleStep_iff.mpr rfl⟩) := by - simp [Std.Iterator.step] + simp [Std.Iterator.step]; rfl theorem Iterator.isPlausibleStep_iff [UpwardEnumerable α] [LE α] [DecidableLE α] {it : Iter (α := Rxc.Iterator α) α} {step} : @@ -535,6 +535,7 @@ private theorem Iterator.instIteratorLoop.loop_eq_wf [UpwardEnumerable α] [LE · rw [WellFounded.fix_eq] simp_all +set_option backward.isDefEq.respectTransparency false in private theorem Iterator.instIteratorLoop.loopWf_eq [UpwardEnumerable α] [LE α] [DecidableLE α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] {n : Type u → Type w} [Monad n] [LawfulMonad n] (γ : Type u) @@ -586,6 +587,7 @@ termination_by IteratorLoop.WithWF.mk ⟨⟨some next, upperBound⟩⟩ acc (hwf decreasing_by simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *] +set_option backward.isDefEq.respectTransparency false in instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α] [LE α] [DecidableLE α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] {n : Type u → Type w} [Monad n] [LawfulMonad n] : @@ -678,7 +680,7 @@ theorem Iterator.Monadic.isPlausibleStep_iff [UpwardEnumerable α] [LT α] [Deci theorem Iterator.Monadic.step_eq_step [UpwardEnumerable α] [LT α] [DecidableLT α] {it : IterM (α := Rxo.Iterator α) Id α} : Std.Iterator.step it = pure (.deflate ⟨Iterator.Monadic.step it, isPlausibleStep_iff.mpr rfl⟩) := by - simp [Std.Iterator.step] + simp [Std.Iterator.step]; rfl theorem Iterator.isPlausibleStep_iff [UpwardEnumerable α] [LT α] [DecidableLT α] {it : Iter (α := Rxo.Iterator α) α} {step} : @@ -1107,6 +1109,7 @@ private theorem Iterator.instIteratorLoop.loop_eq_wf [UpwardEnumerable α] [LT · rw [WellFounded.fix_eq] simp_all +set_option backward.isDefEq.respectTransparency false in private theorem Iterator.instIteratorLoop.loopWf_eq [UpwardEnumerable α] [LT α] [DecidableLT α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] {n : Type u → Type w} [Monad n] [LawfulMonad n] (γ : Type u) @@ -1158,6 +1161,7 @@ termination_by IteratorLoop.WithWF.mk ⟨⟨some next, upperBound⟩⟩ acc (hwf decreasing_by simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *] +set_option backward.isDefEq.respectTransparency false in instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α] [LT α] [DecidableLT α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] {n : Type u → Type w} [Monad n] [LawfulMonad n] : @@ -1240,7 +1244,7 @@ theorem Iterator.Monadic.isPlausibleStep_iff [UpwardEnumerable α] theorem Iterator.Monadic.step_eq_step [UpwardEnumerable α] {it : IterM (α := Rxi.Iterator α) Id α} : it.step = pure (.deflate ⟨Iterator.Monadic.step it, isPlausibleStep_iff.mpr rfl⟩) := by - simp [IterM.step, Std.Iterator.step] + simp [IterM.step, Std.Iterator.step]; rfl theorem Iterator.isPlausibleStep_iff [UpwardEnumerable α] {it : Iter (α := Rxi.Iterator α) α} {step} : diff --git a/src/Init/Data/Slice/Array/Lemmas.lean b/src/Init/Data/Slice/Array/Lemmas.lean index 0390bac902..98085f0655 100644 --- a/src/Init/Data/Slice/Array/Lemmas.lean +++ b/src/Init/Data/Slice/Array/Lemmas.lean @@ -28,6 +28,7 @@ open Std Std.Iterators Std.PRange Std.Slice namespace SubarrayIterator +set_option backward.isDefEq.respectTransparency false in theorem step_eq {it : Iter (α := SubarrayIterator α) α} : it.step = if h : it.1.xs.start < it.1.xs.stop then haveI := it.1.xs.start_le_stop @@ -66,6 +67,7 @@ theorem val_step_eq {it : Iter (α := SubarrayIterator α) α} : simp only [step_eq] split <;> simp +set_option backward.isDefEq.respectTransparency false in theorem toList_eq {α : Type u} {it : Iter (α := SubarrayIterator α) α} : it.toList = (it.internalState.xs.array.toList.take it.internalState.xs.stop).drop it.internalState.xs.start := by @@ -104,11 +106,13 @@ theorem Internal.iter_eq {α : Type u} {s : Subarray α} : Internal.iter s = ⟨⟨s⟩⟩ := rfl +set_option backward.isDefEq.respectTransparency false in theorem Internal.toList_iter {α : Type u} {s : Subarray α} : (Internal.iter s).toList = (s.array.toList.take s.stop).drop s.start := by simp [SubarrayIterator.toList_eq, Internal.iter_eq_toIteratorIter, ToIterator.iter_eq] +set_option backward.isDefEq.respectTransparency false in public instance : LawfulSliceSize (Internal.SubarrayData α) where lawful s := by simp [SliceSize.size, ToIterator.iter_eq, @@ -274,7 +278,7 @@ public theorem Subarray.getElem_eq_getElem_array {xs : Subarray α} {h : i < xs. public theorem Subarray.getElem_toList {xs : Subarray α} {h : i < xs.toList.length} : xs.toList[i]'h = xs[i]'(by simpa using h) := by - simp [getElem_eq_getElem_array, toList_eq_drop_take] + simp [getElem_eq_getElem_array, toList_eq_drop_take]; rfl public theorem Subarray.getElem_eq_getElem_toList {xs : Subarray α} {h : i < xs.size} : xs[i]'h = xs.toList[i]'(by simpa using h) := by diff --git a/src/Init/Data/Slice/List/Lemmas.lean b/src/Init/Data/Slice/List/Lemmas.lean index b7e84374ca..81c5bbf0e1 100644 --- a/src/Init/Data/Slice/List/Lemmas.lean +++ b/src/Init/Data/Slice/List/Lemmas.lean @@ -27,7 +27,7 @@ theorem internalIter_eq {α : Type u} {s : ListSlice α} : Internal.iter s = match s.internalRepresentation.stop with | some stop => s.internalRepresentation.list.iter.take stop | none => s.internalRepresentation.list.iter.toTake := by - simp only [Internal.iter, ToIterator.iter_eq]; rfl + simp only [Internal.iter]; rfl theorem toList_internalIter {α : Type u} {s : ListSlice α} : (Internal.iter s).toList = match s.internalRepresentation.stop with diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index 4e6ed23b9b..cc7384f254 100644 --- a/src/Init/Data/String/Basic.lean +++ b/src/Init/Data/String/Basic.lean @@ -748,6 +748,7 @@ theorem _root_.ByteArray.IsValidUTF8.isUTF8FirstByte_getElem_zero {b : ByteArray theorem isUTF8FirstByte_getUTF8Byte_zero {b : String} {h} : (b.getUTF8Byte 0 h).IsUTF8FirstByte := b.isValidUTF8.isUTF8FirstByte_getElem_zero _ +set_option backward.isDefEq.respectTransparency false in theorem Pos.Raw.isValidUTF8_extract_iff {s : String} (p₁ p₂ : Pos.Raw) (hle : p₁ ≤ p₂) (hle' : p₂ ≤ s.rawEndPos) : (s.toByteArray.extract p₁.byteIdx p₂.byteIdx).IsValidUTF8 ↔ p₁ = p₂ ∨ (p₁.IsValid s ∧ p₂.IsValid s) := by have hle'' : p₂.byteIdx ≤ s.toByteArray.size := by simpa [le_iff] using hle' diff --git a/src/Init/Data/String/Decode.lean b/src/Init/Data/String/Decode.lean index 89f63cb211..2b61e19b59 100644 --- a/src/Init/Data/String/Decode.lean +++ b/src/Init/Data/String/Decode.lean @@ -1121,30 +1121,35 @@ theorem utf8Size_le_of_utf8DecodeChar?_eq_some {b : ByteArray} {c : Char} : | case8 => simp | case9 => simp +set_option backward.isDefEq.respectTransparency false in theorem utf8DecodeChar?_eq_assemble₁ {b : ByteArray} (hb : 1 ≤ b.size) (h : parseFirstByte b[0] = .done) : b.utf8DecodeChar? 0 = assemble₁ b[0] h := by fun_cases ByteArray.utf8DecodeChar? all_goals try (simp_all; done) all_goals omega +set_option backward.isDefEq.respectTransparency false in theorem utf8DecodeChar?_eq_assemble₂ {b : ByteArray} (hb : 2 ≤ b.size) (h : parseFirstByte b[0] = .oneMore) : b.utf8DecodeChar? 0 = assemble₂ b[0] b[1] := by fun_cases ByteArray.utf8DecodeChar? all_goals try (simp_all; done) all_goals omega +set_option backward.isDefEq.respectTransparency false in theorem utf8DecodeChar?_eq_assemble₃ {b : ByteArray} (hb : 3 ≤ b.size) (h : parseFirstByte b[0] = .twoMore) : b.utf8DecodeChar? 0 = assemble₃ b[0] b[1] b[2] := by fun_cases ByteArray.utf8DecodeChar? all_goals try (simp_all; done) all_goals omega +set_option backward.isDefEq.respectTransparency false in theorem utf8DecodeChar?_eq_assemble₄ {b : ByteArray} (hb : 4 ≤ b.size) (h : parseFirstByte b[0] = .threeMore) : b.utf8DecodeChar? 0 = assemble₄ b[0] b[1] b[2] b[3] := by fun_cases ByteArray.utf8DecodeChar? all_goals try (simp_all; done) all_goals omega +set_option backward.isDefEq.respectTransparency false in theorem utf8DecodeChar?_append_eq_assemble₁ {l : List UInt8} {b : ByteArray} (hl : l.length = 1) (h : parseFirstByte l[0] = .done) : (l.toByteArray ++ b).utf8DecodeChar? 0 = assemble₁ l[0] h := by have : (l.toByteArray ++ b)[0]'(by simp [hl]; omega) = l[0] := by diff --git a/src/Init/Data/String/Lemmas/Basic.lean b/src/Init/Data/String/Lemmas/Basic.lean index 66cb298ab4..0c48d9da57 100644 --- a/src/Init/Data/String/Lemmas/Basic.lean +++ b/src/Init/Data/String/Lemmas/Basic.lean @@ -106,25 +106,28 @@ These lemmas are slightly evil because they are non-definitional equalities betw are useful and they are at least equalities between slices with definitionally equal underlying strings, so it should be fine. -/ - +set_option backward.isDefEq.respectTransparency false in @[simp] theorem Slice.sliceTo_sliceFrom {s : Slice} {pos pos'} : (s.sliceFrom pos).sliceTo pos' = s.slice pos (Slice.Pos.ofSliceFrom pos') Slice.Pos.le_ofSliceFrom := by ext <;> simp [String.Pos.ext_iff, Pos.Raw.offsetBy_assoc] +set_option backward.isDefEq.respectTransparency false in @[simp] theorem Slice.sliceFrom_sliceTo {s : Slice} {pos pos'} : (s.sliceTo pos).sliceFrom pos' = s.slice (Slice.Pos.ofSliceTo pos') pos Slice.Pos.ofSliceTo_le := by ext <;> simp [String.Pos.ext_iff] +set_option backward.isDefEq.respectTransparency false in @[simp] theorem Slice.sliceFrom_sliceFrom {s : Slice} {pos pos'} : (s.sliceFrom pos).sliceFrom pos' = s.sliceFrom (Slice.Pos.ofSliceFrom pos') := by ext <;> simp [String.Pos.ext_iff, Pos.Raw.offsetBy_assoc] +set_option backward.isDefEq.respectTransparency false in @[simp] theorem Slice.sliceTo_sliceTo {s : Slice} {pos pos'} : (s.sliceTo pos).sliceTo pos' = s.sliceTo (Slice.Pos.ofSliceTo pos') := by diff --git a/src/Init/Data/String/Lemmas/Iterate.lean b/src/Init/Data/String/Lemmas/Iterate.lean index 9bb6ed82fa..d028b82c13 100644 --- a/src/Init/Data/String/Lemmas/Iterate.lean +++ b/src/Init/Data/String/Lemmas/Iterate.lean @@ -60,6 +60,7 @@ theorem Model.map_get_positionsFrom_startPos {s : Slice} : (Model.positionsFrom s.startPos).map (fun p => p.1.get p.2) = s.copy.toList := Model.map_get_positionsFrom_of_splits (splits_startPos s) +set_option backward.isDefEq.respectTransparency false in @[simp] theorem toList_positionsFrom {s : Slice} {p : s.Pos} : (s.positionsFrom p).toList = Model.positionsFrom p := by @@ -114,6 +115,7 @@ theorem Model.map_get_revPositionsFrom_endPos {s : Slice} : (Model.revPositionsFrom s.endPos).map (fun p => p.1.get p.2) = s.copy.toList.reverse := Model.map_get_revPositionsFrom_of_splits (splits_endPos s) +set_option backward.isDefEq.respectTransparency false in @[simp] theorem toList_revPositionsFrom {s : Slice} {p : s.Pos} : (s.revPositionsFrom p).toList = Model.revPositionsFrom p := by @@ -184,6 +186,7 @@ theorem Model.map_get_positionsFrom_startPos {s : String} : (Model.positionsFrom s.startPos).map (fun p => p.1.get p.2) = s.toList := Model.map_get_positionsFrom_of_splits (splits_startPos s) +set_option backward.isDefEq.respectTransparency false in @[simp] theorem toList_positionsFrom {s : String} {p : s.Pos} : (s.positionsFrom p).toList = Model.positionsFrom p := by @@ -237,6 +240,7 @@ theorem Model.map_get_revPositionsFrom_endPos {s : String} : (Model.revPositionsFrom s.endPos).map (fun p => p.1.get p.2) = s.toList.reverse := Model.map_get_revPositionsFrom_of_splits (splits_endPos s) +set_option backward.isDefEq.respectTransparency false in @[simp] theorem toList_revPositionsFrom {s : String} {p : s.Pos} : (s.revPositionsFrom p).toList = Model.revPositionsFrom p := by diff --git a/src/Init/Data/String/Lemmas/Pattern/Basic.lean b/src/Init/Data/String/Lemmas/Pattern/Basic.lean index e1dda18d85..5842fc13f8 100644 --- a/src/Init/Data/String/Lemmas/Pattern/Basic.lean +++ b/src/Init/Data/String/Lemmas/Pattern/Basic.lean @@ -296,6 +296,7 @@ class LawfulToForwardSearcherModel {ρ : Type} (pat : ρ) [ForwardPatternModel p [∀ s, Std.Iterators.Finite (σ s) Id] : Prop where isValidSearchFrom_toList (s) : IsValidSearchFrom pat s.startPos (ToForwardSearcher.toSearcher pat s).toList +set_option backward.isDefEq.respectTransparency false in theorem LawfulToForwardSearcherModel.defaultImplementation {pat : ρ} [ForwardPattern pat] [StrictForwardPattern pat] [ForwardPatternModel pat] [LawfulForwardPatternModel pat] : letI : ToForwardSearcher pat (ToForwardSearcher.DefaultForwardSearcher pat) := .defaultImplementation diff --git a/src/Init/Data/String/Lemmas/Pattern/Split.lean b/src/Init/Data/String/Lemmas/Pattern/Split.lean index 96d2d135dc..caa1f29527 100644 --- a/src/Init/Data/String/Lemmas/Pattern/Split.lean +++ b/src/Init/Data/String/Lemmas/Pattern/Split.lean @@ -197,6 +197,7 @@ theorem IsValidSearchFrom.splitFromSteps_eq_extend_split {ρ : Type} (pat : ρ) · exact h' p hp₁ hp · exact rej _ (Std.not_lt.1 hp) hp₂ +set_option backward.isDefEq.respectTransparency false in theorem SplitIterator.toList_eq_splitFromSteps {ρ : Type} {pat : ρ} {σ : Slice → Type} [ToForwardSearcher pat σ] [∀ s, Std.Iterator (σ s) Id (SearchStep s)] [∀ s, Std.Iterators.Finite (σ s) Id] {s : Slice} diff --git a/src/Init/Data/String/Lemmas/Pattern/String/ForwardSearcher.lean b/src/Init/Data/String/Lemmas/Pattern/String/ForwardSearcher.lean index 9398f50c32..cb118dfed4 100644 --- a/src/Init/Data/String/Lemmas/Pattern/String/ForwardSearcher.lean +++ b/src/Init/Data/String/Lemmas/Pattern/String/ForwardSearcher.lean @@ -294,6 +294,7 @@ theorem IsTable.push {b : ByteArray} {v : Array Nat} (h : IsTable b v) {d : Nat} obtain rfl : i = v.size := by omega exact hd +set_option backward.isDefEq.respectTransparency false in theorem computeDistance_eq_prefixFunctionRecurrence {s : Slice} (i : Nat) (hi : i < s.copy.toByteArray.size) {patByte : UInt8} (hpat : patByte = s.copy.toByteArray[i]) @@ -403,6 +404,7 @@ theorem Invariants.isLongestMatchAt {pat s : Slice} {stackPos needlePos : String cases h' exact h.partialMatch.isLongestMatchAt h.isEmpty_eq_false h.isValidForSlice +set_option backward.isDefEq.respectTransparency false in theorem Invariants.not_matchesAt_of_prefixFunction_eq {pat s : Slice} {stackPos needlePos : String.Pos.Raw} (h : Invariants pat s needlePos stackPos) {k : Nat} {hki} (hk : prefixFunction pat.copy.toByteArray (needlePos.byteIdx - 1) hki = k) @@ -433,6 +435,7 @@ theorem Invariants.of_prefixFunction_eq {pat s : Slice} {stackPos needlePos : St rw [Nat.sub_add_cancel (by simp at h'; omega)] at this exact hk ▸ (h.partialMatch.partialMatch_iff.1 this).2 +set_option backward.isDefEq.respectTransparency false in theorem Invariants.isValidSearchFrom_toList {pat s : Slice} {stackPos needlePos : String.Pos.Raw} (it : Std.Iter (α := ForwardSliceSearcher s) (SearchStep s)) (h : Invariants pat s needlePos stackPos) diff --git a/src/Init/Data/Vector/Attach.lean b/src/Init/Data/Vector/Attach.lean index c6c40701e6..9d0d0cb09a 100644 --- a/src/Init/Data/Vector/Attach.lean +++ b/src/Init/Data/Vector/Attach.lean @@ -359,7 +359,7 @@ theorem pmap_append' {p : α → Prop} {f : ∀ a : α, p a → β} {xs : Vector ys.attach.map (fun ⟨y, h⟩ => (⟨y, mem_append_right xs h⟩ : { y // y ∈ xs ++ ys })) := by rcases xs with ⟨xs, rfl⟩ rcases ys with ⟨ys, rfl⟩ - simp [Array.map_attach_eq_pmap] + simp [Array.map_attach_eq_pmap]; rfl @[simp] theorem attachWith_append {P : α → Prop} {xs : Vector α n} {ys : Vector α m} {H : ∀ (a : α), a ∈ xs ++ ys → P a} : diff --git a/src/Init/Data/Vector/Count.lean b/src/Init/Data/Vector/Count.lean index 1fc2b395b9..f290520ed9 100644 --- a/src/Init/Data/Vector/Count.lean +++ b/src/Init/Data/Vector/Count.lean @@ -96,11 +96,13 @@ theorem countP_replicate {a : α} {n : Nat} : countP p (replicate n a) = if p a simp only [replicate_eq_mk_replicate, countP_mk] simp [Array.countP_replicate] +set_option backward.isDefEq.respectTransparency false in theorem boole_getElem_le_countP {p : α → Bool} {xs : Vector α n} (h : i < n) : (if p xs[i] then 1 else 0) ≤ xs.countP p := by rcases xs with ⟨xs, rfl⟩ simp [Array.boole_getElem_le_countP] +set_option backward.isDefEq.respectTransparency false in @[grind =] theorem countP_set {p : α → Bool} {xs : Vector α n} {a : α} (h : i < n) : (xs.set i a).countP p = xs.countP p - (if p xs[i] then 1 else 0) + (if p a then 1 else 0) := by @@ -188,6 +190,7 @@ theorem count_le_count_push {a b : α} {xs : Vector α n} : count a xs ≤ count rcases xs with ⟨xs, rfl⟩ simp +set_option backward.isDefEq.respectTransparency false in theorem boole_getElem_le_count {a : α} {xs : Vector α n} (h : i < n) : (if xs[i] == a then 1 else 0) ≤ xs.count a := by rcases xs with ⟨xs, rfl⟩ @@ -196,7 +199,7 @@ theorem boole_getElem_le_count {a : α} {xs : Vector α n} (h : i < n) : theorem count_set {a b : α} {xs : Vector α n} (h : i < n) : (xs.set i a).count b = xs.count b - (if xs[i] == b then 1 else 0) + (if a == b then 1 else 0) := by rcases xs with ⟨xs, rfl⟩ - simp [Array.count_set] + simp [Array.count_set]; rfl @[simp] theorem count_cast {xs : Vector α n} : (xs.cast h).count a = xs.count a := by rcases xs with ⟨xs, rfl⟩ diff --git a/src/Init/Data/Vector/Extract.lean b/src/Init/Data/Vector/Extract.lean index c912d676ea..8d30dd1daf 100644 --- a/src/Init/Data/Vector/Extract.lean +++ b/src/Init/Data/Vector/Extract.lean @@ -132,6 +132,7 @@ theorem extract_append {xs : Vector α n} {ys : Vector α m} {i j : Nat} : rcases ys with ⟨ys, rfl⟩ simp +set_option backward.isDefEq.respectTransparency false in theorem extract_append_left {xs : Vector α n} {ys : Vector α m} : (xs ++ ys).extract 0 n = (xs.extract 0 n).cast (by omega) := by ext i h @@ -178,7 +179,7 @@ theorem mem_extract_iff_getElem {xs : Vector α n} {a : α} {i j : Nat} : theorem set_eq_push_extract_append_extract {xs : Vector α n} {i : Nat} (h : i < n) {a : α} : xs.set i a = ((xs.extract 0 i).push a ++ (xs.extract (i + 1) n)).cast (by omega) := by rcases xs with ⟨as, rfl⟩ - simp [Array.set_eq_push_extract_append_extract] + simp [Array.set_eq_push_extract_append_extract]; rfl theorem extract_reverse {xs : Vector α n} {i j : Nat} : xs.reverse.extract i j = (xs.extract (n - j) (n - i)).reverse.cast (by omega) := by diff --git a/src/Init/Data/Vector/Find.lean b/src/Init/Data/Vector/Find.lean index 018e9abfcc..0dd3e4dca0 100644 --- a/src/Init/Data/Vector/Find.lean +++ b/src/Init/Data/Vector/Find.lean @@ -295,12 +295,12 @@ theorem find?_eq_some_iff_getElem {xs : Vector α n} {p : α → Bool} {b : α} /-! ### findFinIdx? -/ @[grind =] -theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p (#v[] : Vector α 0) = none := by simp +theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p (#v[] : Vector α 0) = none := by simp; rfl @[grind =] theorem findFinIdx?_singleton {a : α} {p : α → Bool} : #[a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by - simp + simp; rfl @[congr] theorem findFinIdx?_congr {p : α → Bool} {xs : Vector α n} {ys : Vector α n} (w : xs = ys) : findFinIdx? p xs = findFinIdx? p ys := by diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index f2cb884edd..e1ef20991a 100644 --- a/src/Init/Data/Vector/Lemmas.lean +++ b/src/Init/Data/Vector/Lemmas.lean @@ -528,7 +528,7 @@ theorem toList_zip {as : Vector α n} {bs : Vector β n} : @[simp] theorem getElem_toList {xs : Vector α n} {i : Nat} (h : i < xs.toList.length) : xs.toList[i] = xs[i]'(by simpa using h) := by cases xs - simp + simp; rfl @[simp] theorem getElem?_toList {xs : Vector α n} {i : Nat} : xs.toList[i]? = xs[i]? := by @@ -2908,6 +2908,7 @@ theorem replace_extract {xs : Vector α n} {i : Nat} : rcases xs with ⟨xs, rfl⟩ simp [Array.replace_extract] +set_option backward.isDefEq.respectTransparency false in @[simp] theorem replace_replicate_self {a : α} (h : 0 < n) : (replicate n a).replace a b = (#v[b] ++ replicate (n - 1) a).cast (by omega) := by match n, h with @@ -2926,6 +2927,7 @@ set_option linter.indexVariables false in theorem getElem_push_last {xs : Vector α n} {x : α} : (xs.push x)[n] = x := by simp +set_option backward.isDefEq.respectTransparency false in @[simp] theorem push_pop_back (xs : Vector α (n + 1)) : xs.pop.push xs.back = xs := by ext i by_cases h : i < n @@ -3019,6 +3021,7 @@ theorem forall_zero_iff {P : Vector α 0 → Prop} : obtain (rfl : xs = #v[]) := (by ext i h; simp at h) apply h +set_option backward.isDefEq.respectTransparency false in theorem forall_cons_iff {P : Vector α (n + 1) → Prop} : (∀ xs : Vector α (n + 1), P xs) ↔ (∀ (x : α) (xs : Vector α n), P (xs.push x)) := by constructor diff --git a/src/Init/Data/Vector/Monadic.lean b/src/Init/Data/Vector/Monadic.lean index 4f1e5f7e12..de23d28ff4 100644 --- a/src/Init/Data/Vector/Monadic.lean +++ b/src/Init/Data/Vector/Monadic.lean @@ -53,7 +53,7 @@ theorem mapM_pure [Monad m] [LawfulMonad m] {xs : Vector α n} (f : α → β) : (mk #[] rfl).mapM f = pure #v[] := by unfold mapM unfold mapM.go - simp + simp; rfl @[simp, grind =] theorem mapM_append [Monad m] [LawfulMonad m] {f : α → m β} {xs : Vector α n} {ys : Vector α n'} : diff --git a/src/Init/Data/Vector/OfFn.lean b/src/Init/Data/Vector/OfFn.lean index 33402360ad..c910271fce 100644 --- a/src/Init/Data/Vector/OfFn.lean +++ b/src/Init/Data/Vector/OfFn.lean @@ -119,6 +119,7 @@ theorem ofFnM_succ {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} : pure (as.push a)) := by simp [ofFnM, ofFnM_go_succ] +set_option backward.isDefEq.respectTransparency false in theorem ofFnM_add {n m} [Monad m] [LawfulMonad m] {f : Fin (n + k) → m α} : ofFnM f = (do let as ← ofFnM (fun i => f (i.castLE (Nat.le_add_right n k))) diff --git a/src/Init/Grind/Ring/Basic.lean b/src/Init/Grind/Ring/Basic.lean index fbcfd2bb33..2032f112d5 100644 --- a/src/Init/Grind/Ring/Basic.lean +++ b/src/Init/Grind/Ring/Basic.lean @@ -184,7 +184,7 @@ theorem natCast_succ (n : Nat) : ((n + 1 : Nat) : α) = ((n : α) + 1) := by theorem ofNat_mul (a b : Nat) : OfNat.ofNat (α := α) (a * b) = OfNat.ofNat a * OfNat.ofNat b := by induction b with - | zero => simp [Nat.mul_zero, mul_zero] + | zero => simp [Nat.mul_zero, mul_zero]; rfl | succ a ih => rw [Nat.mul_succ, ofNat_add, ih, ofNat_add, left_distrib, mul_one] theorem natCast_mul (a b : Nat) : ((a * b : Nat) : α) = ((a : α) * (b : α)) := by diff --git a/src/Init/GrindInstances/Ring/Fin.lean b/src/Init/GrindInstances/Ring/Fin.lean index 2806f6b235..f19ad2b2f4 100644 --- a/src/Init/GrindInstances/Ring/Fin.lean +++ b/src/Init/GrindInstances/Ring/Fin.lean @@ -142,6 +142,7 @@ instance (n : Nat) [NeZero n] : IsCharP (Fin n) n := IsCharP.mk' _ _ example [NeZero n] : ToInt.Neg (Fin n) (.co 0 n) := inferInstance example [NeZero n] : ToInt.Sub (Fin n) (.co 0 n) := inferInstance +set_option backward.isDefEq.respectTransparency false in instance [i : NeZero n] : ToInt.Pow (Fin n) (.co 0 n) where toInt_pow x k := by induction k with diff --git a/src/Init/Hints.lean b/src/Init/Hints.lean index 163dfd9219..2ee004e781 100644 --- a/src/Init/Hints.lean +++ b/src/Init/Hints.lean @@ -4,17 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ module - prelude public import Init.Grind.Tactics import Init.NotationExtra - public section /- Hint for making sure `Not p` is definitionally equal to `p → False` even when `TransparencyMode.reducible` -/ unif_hint (p : Prop) where - |- Not p =?= p → False + ⊢ Not p =?= p → False unif_hint (n : Nat) where ⊢ n - 0 =?= n diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index 570174e6ae..c9a2e11c2e 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -22,7 +22,7 @@ register_builtin_option backward.isDefEq.lazyWhnfCore : Bool := { } register_builtin_option backward.isDefEq.respectTransparency : Bool := { - defValue := false + defValue := true descr := "if true (the default), do not bump transparency to `.default` \ when checking whether implicit arguments are definitionally equal" } diff --git a/src/Std/Data/DHashMap/IteratorLemmas.lean b/src/Std/Data/DHashMap/IteratorLemmas.lean index 890b6d6122..0d542c027b 100644 --- a/src/Std/Data/DHashMap/IteratorLemmas.lean +++ b/src/Std/Data/DHashMap/IteratorLemmas.lean @@ -22,12 +22,12 @@ open Std.Iterators @[simp] public theorem step_iter_nil {α : Type u} {β : α → Type v} : ((.nil : AssocList α β).iter).step = ⟨.done, rfl⟩ := by - simp [Iter.step_eq, iter] + simp [Iter.step_eq, iter]; rfl @[simp] public theorem step_iter_cons {α : Type u} {β : α → Type v} {k v} {l : AssocList α β} : ((AssocList.cons k v l).iter).step = ⟨.yield l.iter ⟨k, v⟩, rfl⟩ := by - simp [Iter.step_eq, iter] + simp [Iter.step_eq, iter]; rfl @[simp] public theorem toList_iter {α : Type u} {β : α → Type v} {l : AssocList α β} : diff --git a/src/Std/Data/DTreeMap/Internal/Zipper.lean b/src/Std/Data/DTreeMap/Internal/Zipper.lean index 898574701d..24140d72ca 100644 --- a/src/Std/Data/DTreeMap/Internal/Zipper.lean +++ b/src/Std/Data/DTreeMap/Internal/Zipper.lean @@ -390,8 +390,8 @@ theorem Zipper.step_done : (done : Zipper α β).step = .done := rfl @[simp] theorem Zipper.step_cons : (cons k v t it : Zipper α β).step = .yield ⟨it.prependMap t⟩ ⟨k, v⟩ := rfl -@[simp] -theorem Zipper.val_run_step_toIterM_iter {z : Zipper α β} : z.iter.toIterM.step.run.inflate.val = z.step := by +set_option backward.isDefEq.respectTransparency false in +@[simp] theorem Zipper.val_run_step_toIterM_iter {z : Zipper α β} : z.iter.toIterM.step.run.inflate.val = z.step := by rw [IterM.step] simp only [Iterator.step, Id.run_pure, Shrink.inflate_deflate] rfl @@ -495,6 +495,7 @@ theorem RxcIterator.step_cons_of_not_LE [Ord α] {upper : α} {h : (compare k up rw [step, h] simp only [Bool.false_eq_true, ↓reduceIte] +set_option backward.isDefEq.respectTransparency false in @[simp] theorem RxcIterator.val_run_step_toIterM_iter [Ord α] {z : RxcIterator α β} : (⟨z⟩ : Iter (α := RxcIterator α β) ((a : α) × β a)).toIterM.step.run.inflate.val = z.step := by rw [IterM.step] @@ -624,6 +625,7 @@ theorem RxoIterator.step_cons_of_isLT_eq_false [Ord α] {upper : α} {h : (compa rw [step, h] simp only [Bool.false_eq_true, ↓reduceIte] +set_option backward.isDefEq.respectTransparency false in @[simp] theorem RxoIterator.val_run_step_toIterM_iter [Ord α] {z : RxoIterator α β} : (⟨z⟩ : Iter (α := RxoIterator α β) ((a : α) × β a)).toIterM.step.run.inflate.val = z.step := by rw [IterM.step] @@ -692,6 +694,7 @@ public def RicSlice.instToIterator {β : α → Type v} [Ord α] := (fun s => ⟨RxcIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩) attribute [instance] RicSlice.instToIterator +set_option backward.isDefEq.respectTransparency false in public theorem toList_ric {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β) (ordered : t.Ordered) (bound : α) : t[*...=bound].toList = t.toList.filter (fun e => (compare e.fst bound).isLE) := by simp only [Ric.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter_eq_toIteratorIter, @@ -721,6 +724,7 @@ public def RicSlice.instToIterator [Ord α] := (⟨RxcIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1) attribute [instance] RicSlice.instToIterator +set_option backward.isDefEq.respectTransparency false in public theorem toList_ric {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit)) (ordered : t.Ordered) (bound : α) : (t : Impl α (fun _ => Unit))[*...=bound].toList = (Internal.Impl.keys t).filter (fun e => (compare e bound).isLE) := by simp only [Ric.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter, @@ -755,6 +759,7 @@ public def RicSlice.instToIterator {β : Type v} [Ord α] := (⟨RxcIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2) attribute [instance] RicSlice.instToIterator +set_option backward.isDefEq.respectTransparency false in public theorem toList_ric {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β)) (ordered : t.Ordered) (bound : α) : t[*...=bound].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst bound).isLE) := by simp only [Ric.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter, @@ -789,6 +794,7 @@ public def RioSlice.instToIterator {β : α → Type v} [Ord α] := ⟨RxoIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩ attribute [instance] RioSlice.instToIterator +set_option backward.isDefEq.respectTransparency false in public theorem toList_rio {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β) (ordered : t.Ordered) (bound : α) : t[*...bound].toList = t.toList.filter (fun e => (compare e.fst bound).isLT) := by simp only [Rio.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter, @@ -819,6 +825,7 @@ public def RioSlice.instToIterator [Ord α] := (⟨RxoIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1) attribute [instance] RioSlice.instToIterator +set_option backward.isDefEq.respectTransparency false in public theorem toList_rio {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit)) (ordered : t.Ordered) (bound : α) : (t : Impl α (fun _ => Unit))[*... (compare e bound).isLT) := by simp only [Rio.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter, @@ -853,6 +860,7 @@ public def RioSlice.instToIterator {β : Type v} [Ord α] := (⟨RxoIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2) attribute [instance] RioSlice.instToIterator +set_option backward.isDefEq.respectTransparency false in public theorem toList_rio {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β)) (ordered : t.Ordered) (bound : α) : t[*... (compare e.fst bound).isLT) := by simp only [Rio.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter, @@ -920,6 +928,7 @@ public def RccSlice.instToIterator {β : α → Type v} [Ord α] := (rccIterator s.1.treeMap s.1.range.lower s.1.range.upper) attribute [instance] RccSlice.instToIterator +set_option backward.isDefEq.respectTransparency false in public theorem toList_rcc {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β) (ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound...=upperBound].toList = t.toList.filter (fun e => (compare e.fst lowerBound).isGE ∧ (compare e.fst upperBound).isLE) := by simp only [Rcc.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter, @@ -947,6 +956,7 @@ public def RccSlice.instToIterator [Ord α] := (⟨RxcIterator.mk (Zipper.prependMapGE s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1) attribute [instance] RccSlice.instToIterator +set_option backward.isDefEq.respectTransparency false in public theorem toList_rcc {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit)) (ordered : t.Ordered) (lowerBound upperBound: α) : (t : Impl α (fun _ => Unit))[lowerBound...=upperBound].toList = (Internal.Impl.keys t).filter (fun e => (compare e lowerBound).isGE ∧ (compare e upperBound).isLE) := by simp only [Rcc.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter, @@ -983,6 +993,7 @@ public def RccSlice.instToIterator {β : Type v} [Ord α] := (⟨RxcIterator.mk (Zipper.prependMapGE s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2) attribute [instance] RccSlice.instToIterator +set_option backward.isDefEq.respectTransparency false in public theorem toList_rcc {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β)) (ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound...=upperBound].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst lowerBound).isGE ∧ (compare e.fst upperBound).isLE) := by simp only [Rcc.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter, @@ -1054,6 +1065,7 @@ public def RcoSlice.instToIterator {β : α → Type v} [Ord α] := rcoIterator s.1.treeMap s.1.range.lower s.1.range.upper attribute [instance] RcoSlice.instToIterator +set_option backward.isDefEq.respectTransparency false in public theorem toList_rco {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β) (ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound... (compare e.fst lowerBound).isGE ∧ (compare e.fst upperBound).isLT) := by simp only [Rco.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter, @@ -1081,6 +1093,7 @@ public def RcoSlice.instToIterator [Ord α] := (⟨RxoIterator.mk (Zipper.prependMapGE s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1) attribute [instance] RcoSlice.instToIterator +set_option backward.isDefEq.respectTransparency false in public theorem toList_rco {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit)) (ordered : t.Ordered) (lowerBound upperBound: α) : (t : Impl α (fun _ => Unit))[lowerBound... (compare e lowerBound).isGE ∧ (compare e upperBound).isLT) := by simp only [Rco.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter, @@ -1117,6 +1130,7 @@ public def RcoSlice.instToIterator {β : Type v} [Ord α] := (⟨RxoIterator.mk (Zipper.prependMapGE s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2) attribute [instance] RcoSlice.instToIterator +set_option backward.isDefEq.respectTransparency false in public theorem toList_rco {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β)) (ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound... (compare e.fst lowerBound).isGE ∧ (compare e.fst upperBound).isLT) := by simp only [Rco.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter, @@ -1187,6 +1201,7 @@ public def RooSlice.instToIterator {β : α → Type v} [Ord α] := rooIterator s.1.treeMap s.1.range.lower s.1.range.upper attribute [instance] RooSlice.instToIterator +set_option backward.isDefEq.respectTransparency false in public theorem toList_roo {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β) (ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound<... (compare e.fst lowerBound).isGT ∧ (compare e.fst upperBound).isLT) := by simp only [Roo.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter, @@ -1214,6 +1229,7 @@ public def RooSlice.instToIterator [Ord α] := (⟨RxoIterator.mk (Zipper.prependMapGT s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1) attribute [instance] RooSlice.instToIterator +set_option backward.isDefEq.respectTransparency false in public theorem toList_roo {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit)) (ordered : t.Ordered) (lowerBound upperBound: α) : (t : Impl α (fun _ => Unit))[lowerBound<... (compare e lowerBound).isGT ∧ (compare e upperBound).isLT) := by simp only [Roo.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter, @@ -1250,6 +1266,7 @@ public def RooSlice.instToIterator {β : Type v} [Ord α] := (⟨RxoIterator.mk (Zipper.prependMapGT s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2) attribute [instance] RooSlice.instToIterator +set_option backward.isDefEq.respectTransparency false in public theorem toList_roo {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β)) (ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound<... (compare e.fst lowerBound).isGT ∧ (compare e.fst upperBound).isLT) := by simp only [Roo.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter, @@ -1321,6 +1338,7 @@ public def RocSlice.instToIterator {β : α → Type v} [Ord α] := rocIterator s.1.treeMap s.1.range.lower s.1.range.upper attribute [instance] RocSlice.instToIterator +set_option backward.isDefEq.respectTransparency false in public theorem toList_roc {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β) (ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound<...=upperBound].toList = t.toList.filter (fun e => (compare e.fst lowerBound).isGT ∧ (compare e.fst upperBound).isLE) := by simp only [Roc.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter, @@ -1348,6 +1366,7 @@ public def RocSlice.instToIterator [Ord α] := (⟨RxcIterator.mk (Zipper.prependMapGT s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1) attribute [instance] RocSlice.instToIterator +set_option backward.isDefEq.respectTransparency false in public theorem toList_roc {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit)) (ordered : t.Ordered) (lowerBound upperBound: α) : (t : Impl α (fun _ => Unit))[lowerBound<...=upperBound].toList = (Internal.Impl.keys t).filter (fun e => (compare e lowerBound).isGT ∧ (compare e upperBound).isLE) := by simp only [Roc.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter, @@ -1384,6 +1403,7 @@ public def RocSlice.instToIterator {β : Type v} [Ord α] := (⟨RxcIterator.mk (Zipper.prependMapGT s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2) attribute [instance] RocSlice.instToIterator +set_option backward.isDefEq.respectTransparency false in public theorem toList_roc {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β)) (ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound<...=upperBound].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst lowerBound).isGT ∧ (compare e.fst upperBound).isLE) := by simp only [Roc.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter, @@ -1440,6 +1460,7 @@ public def RciSlice.instToIterator {β : α → Type v} [Ord α] := rciIterator s.1.treeMap s.1.range.lower attribute [instance] RciSlice.instToIterator +set_option backward.isDefEq.respectTransparency false in public theorem toList_rci {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β) (ordered : t.Ordered) (lowerBound : α) : t[lowerBound...*].toList = t.toList.filter (fun e => (compare e.fst lowerBound).isGE) := by simp only [Rci.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter, @@ -1467,6 +1488,7 @@ public def RciSlice.instToIterator [Ord α] := (⟨Zipper.prependMapGE s.1.treeMap s.1.range.lower Zipper.done⟩ : Iter _ ).map fun e => (e.1) attribute [instance] RciSlice.instToIterator +set_option backward.isDefEq.respectTransparency false in public theorem toList_rci {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit)) (ordered : t.Ordered) (lowerBound : α) : (t : Impl α (fun _ => Unit))[lowerBound...*].toList = (Internal.Impl.keys t).filter (fun e => (compare e lowerBound).isGE) := by simp only [Rci.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter, @@ -1506,6 +1528,7 @@ public def RciSlice.instToIterator {β : Type v} [Ord α] := (⟨(Zipper.prependMapGE s.1.treeMap s.1.range.lower Zipper.done)⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2) attribute [instance] RciSlice.instToIterator +set_option backward.isDefEq.respectTransparency false in public theorem toList_rci {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β)) (ordered : t.Ordered) (lowerBound : α) : t[lowerBound...*].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst lowerBound).isGE) := by simp only [Rci.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter, @@ -1563,6 +1586,7 @@ public def RoiSlice.instToIterator {β : α → Type v} [Ord α] := roiIterator s.1.treeMap s.1.range.lower attribute [instance] RoiSlice.instToIterator +set_option backward.isDefEq.respectTransparency false in public theorem toList_roi {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β) (ordered : t.Ordered) (lowerBound : α) : t[lowerBound<...*].toList = t.toList.filter (fun e => (compare e.fst lowerBound).isGT) := by simp only [Roi.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter, @@ -1590,6 +1614,7 @@ public def RoiSlice.instToIterator [Ord α] := (⟨Zipper.prependMapGT s.1.treeMap s.1.range.lower Zipper.done⟩ : Iter _ ).map fun e => (e.1) attribute [instance] RoiSlice.instToIterator +set_option backward.isDefEq.respectTransparency false in public theorem toList_roi {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit)) (ordered : t.Ordered) (lowerBound : α) : (t : Impl α (fun _ => Unit))[lowerBound<...*].toList = (Internal.Impl.keys t).filter (fun e => (compare e lowerBound).isGT) := by simp only [Roi.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter, @@ -1629,6 +1654,7 @@ public def RoiSlice.instToIterator {β : Type v} [Ord α] := (⟨(Zipper.prependMapGT s.1.treeMap s.1.range.lower .done)⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2) attribute [instance] RoiSlice.instToIterator +set_option backward.isDefEq.respectTransparency false in public theorem toList_roi {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β)) (ordered : t.Ordered) (lowerBound : α) : t[lowerBound<...*].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst lowerBound).isGT) := by simp only [Roi.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter, @@ -1680,6 +1706,7 @@ public def RiiSlice.instToIterator {β : α → Type v} := riiIterator s.1.treeMap attribute [instance] RiiSlice.instToIterator +set_option backward.isDefEq.respectTransparency false in public theorem toList_rii {α : Type u} {β : α → Type v} (t : Impl α β) : t[*...*].toList = t.toList := by simp only [Rii.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter, Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq, @@ -1705,6 +1732,7 @@ public def RiiSlice.instToIterator {α : Type u} := (⟨Zipper.prependMap s.internalRepresentation.treeMap .done⟩ : Iter _ ).map fun e => (e.1) attribute [instance] RiiSlice.instToIterator +set_option backward.isDefEq.respectTransparency false in public theorem toList_rii {α : Type u} (t : Impl α (fun _ => Unit)) : (t : Impl α fun _ => Unit)[*...*].toList = Internal.Impl.keys t := by simp only [Rii.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter, @@ -1737,6 +1765,7 @@ public def RiiSlice.instToIterator {α : Type u} {β : Type v} := (⟨Zipper.prependMap s.internalRepresentation.treeMap .done⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2) attribute [instance] RiiSlice.instToIterator +set_option backward.isDefEq.respectTransparency false in public theorem toList_rii {α : Type u} {β : Type v} (t : Impl α (fun _ => β)) : (t : Impl α fun _ => β)[*...*].toList = Internal.Impl.Const.toList t := by simp only [Rii.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter, diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/DropWhile.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/DropWhile.lean index 5a8bbf2c72..fcc685751f 100644 --- a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/DropWhile.lean +++ b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/DropWhile.lean @@ -42,6 +42,7 @@ theorem IterM.dropWhile_eq_intermediateDropWhile {α m β} [Monad m] it.dropWhile P = Intermediate.dropWhile P true it := rfl +set_option backward.isDefEq.respectTransparency false in theorem IterM.step_intermediateDropWhileWithPostcondition {α m β} [Monad m] [Iterator α m β] {it : IterM (α := α) m β} {P} {dropping} : (IterM.Intermediate.dropWhileWithPostcondition P dropping it).step = (do diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean index 4adfc028ba..8504af86ab 100644 --- a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean +++ b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean @@ -76,6 +76,7 @@ theorem IterM.stepAsHetT_filterMapWithPostcondition [Monad m] [LawfulMonad m] [M · simp [pure] · simp [pure] +set_option backward.isDefEq.respectTransparency false in theorem IterM.Equiv.filterMapWithPostcondition {α₁ α₂ β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Iterator α₁ m β] [Iterator α₂ m β] diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean index e810699be5..95f9b45d3d 100644 --- a/src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean +++ b/src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean @@ -178,6 +178,7 @@ theorem Iter.toList_intermediateZip_of_finite [Iterator α₁ Id β₁] [Iterato · cases hs simp +set_option backward.isDefEq.respectTransparency false in theorem Iter.atIdxSlow?_intermediateZip [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] [Productive α₁ Id] [Productive α₂ Id] {it₁ : Iter (α := α₁) β₁} {memo} {it₂ : Iter (α := α₂) β₂} {n : Nat} : diff --git a/src/Std/Data/Iterators/Lemmas/Equivalence/Basic.lean b/src/Std/Data/Iterators/Lemmas/Equivalence/Basic.lean index fed008c342..d9dfdf99f5 100644 --- a/src/Std/Data/Iterators/Lemmas/Equivalence/Basic.lean +++ b/src/Std/Data/Iterators/Lemmas/Equivalence/Basic.lean @@ -235,6 +235,7 @@ theorem Iter.Equiv.trans {α₁ α₂ α₃ β : Type w} (hbc : Iter.Equiv itb itc) : Iter.Equiv ita itc := BundledIterM.Equiv.trans hab hbc +set_option backward.isDefEq.respectTransparency false in theorem IterM.Equiv.of_morphism {α₁ α₂} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {β : Type w} [Iterator α₁ m β] [Iterator α₂ m β] (ita : IterM (α := α₁) m β) diff --git a/src/Std/Data/Iterators/Lemmas/Equivalence/StepCongr.lean b/src/Std/Data/Iterators/Lemmas/Equivalence/StepCongr.lean index f1a30f0606..7a67ed5181 100644 --- a/src/Std/Data/Iterators/Lemmas/Equivalence/StepCongr.lean +++ b/src/Std/Data/Iterators/Lemmas/Equivalence/StepCongr.lean @@ -127,6 +127,7 @@ The difficulty in this lemma is that we want to argue that we can cancel `HetT.map QuotStep.bundledQuotient` because `QuotStep.bundledQuotient` is injective. This cancellation property does not hold for all monads. -/ +set_option backward.isDefEq.respectTransparency false in theorem IterM.Equiv.step_eq {α₁ α₂ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α₁ m β] [Iterator α₂ m β] {ita : IterM (α := α₁) m β} {itb : IterM (α := α₂) m β} (h : IterM.Equiv ita itb) : @@ -161,6 +162,7 @@ theorem IterM.Equiv.step_eq {α₁ α₂ : Type w} {m : Type w → Type w'} [Mon let hex := ?hex exact hex.choose_spec +set_option backward.isDefEq.respectTransparency false in theorem IterM.Equiv.lift_step_bind_congr {α₁ α₂ : Type w} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α₁ m β] [Iterator α₂ m β] diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Empty.lean b/src/Std/Data/Iterators/Lemmas/Producers/Empty.lean index cb7ce228b1..a5819b6198 100644 --- a/src/Std/Data/Iterators/Lemmas/Producers/Empty.lean +++ b/src/Std/Data/Iterators/Lemmas/Producers/Empty.lean @@ -22,7 +22,7 @@ theorem Iter.toIterM_empty {β} : @[simp] theorem Iter.step_empty {β} : (Iter.empty β).step = ⟨.done, rfl⟩ := by - simp [Iter.step] + simp [Iter.step]; rfl @[simp] theorem Iter.toList_empty {β} : diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean index de64c028ea..976ffd1704 100644 --- a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean +++ b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean @@ -53,6 +53,7 @@ theorem Array.step_iterM {array : Array β} : section Equivalence +set_option backward.isDefEq.respectTransparency false in theorem Std.Iterators.Types.ArrayIterator.stepAsHetT_iterFromIdxM [LawfulMonad m] {array : Array β} {pos : Nat} : (array.iterFromIdxM m pos).stepAsHetT = (if _ : pos < array.size then diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean index 95cfdf7f04..fc680c7179 100644 --- a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean +++ b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean @@ -16,6 +16,7 @@ open Std.Internal Std.Iterators Std.Iterators.Types variable {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] {β : Type w} -- We don't want to pollute `List` with this rarely used lemma. +set_option backward.isDefEq.respectTransparency false in public theorem Types.ListIterator.stepAsHetT_iterM [LawfulMonad m] {l : List β} : (l.iterM m).stepAsHetT = (match l with | [] => pure .done diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Repeat.lean b/src/Std/Data/Iterators/Lemmas/Producers/Repeat.lean index 42240f827f..5f85398c02 100644 --- a/src/Std/Data/Iterators/Lemmas/Producers/Repeat.lean +++ b/src/Std/Data/Iterators/Lemmas/Producers/Repeat.lean @@ -19,6 +19,7 @@ open Std.Iterators variable {α : Type w} {f : α → α} {init : α} +set_option backward.isDefEq.respectTransparency false in theorem Iter.step_repeat : (Iter.repeat f init).step = .yield (Iter.repeat f (f init)) init ⟨rfl, rfl⟩ := by simp [Iter.«repeat», Iter.step, Iter.toIterM, IterM.step, Iterator.step, IterM.toIter] diff --git a/src/Std/Do/Triple/SpecLemmas.lean b/src/Std/Do/Triple/SpecLemmas.lean index 3b215c0215..722756981f 100644 --- a/src/Std/Do/Triple/SpecLemmas.lean +++ b/src/Std/Do/Triple/SpecLemmas.lean @@ -331,6 +331,7 @@ theorem Spec.liftWith_OptionT [Monad m] [WPMonad m ps] (wp⟦f (fun x => x.run)⟧ (Q.1, Q.2.2)) Q := by simp [Triple.iff] +set_option backward.isDefEq.respectTransparency false in @[spec] theorem Spec.restoreM_StateT [Monad m] [WPMonad m ps] (x : m (α × σ)) : Triple @@ -345,6 +346,7 @@ theorem Spec.restoreM_ReaderT [Monad m] [WPMonad m ps] (x : m α) : (fun s => wp⟦x⟧ (fun a => Q.1 a s, Q.2)) Q := by simp [Triple.iff] +set_option backward.isDefEq.respectTransparency false in @[spec] theorem Spec.restoreM_ExceptT [Monad m] [WPMonad m ps] (x : m (Except ε α)) : Triple (ps := .except ε ps) @@ -352,6 +354,7 @@ theorem Spec.restoreM_ExceptT [Monad m] [WPMonad m ps] (x : m (Except ε α)) : (wp⟦x⟧ (fun e => e.casesOn Q.2.1 Q.1, Q.2.2)) Q := by simp [Triple.iff] +set_option backward.isDefEq.respectTransparency false in @[spec] theorem Spec.restoreM_OptionT [Monad m] [WPMonad m ps] (x : m (Option α)) : Triple (ps := .except PUnit ps) diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Extract.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Extract.lean index 7dc1bfbeee..fa25db6dc0 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Extract.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Extract.lean @@ -56,7 +56,7 @@ instance : AIG.LawfulVecOperator α ExtractTarget blastExtract where decl_eq := by intros unfold blastExtract - simp + simp; rfl end bitblast end BVExpr diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateLeft.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateLeft.lean index b1323d005d..31a55e4603 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateLeft.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateLeft.lean @@ -57,7 +57,7 @@ instance : AIG.LawfulVecOperator α AIG.ShiftTarget blastRotateLeft where decl_eq := by intros unfold blastRotateLeft - dsimp only + dsimp only; rfl end bitblast end BVExpr diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateRight.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateRight.lean index 0e0e0149c9..ee7e032c93 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateRight.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateRight.lean @@ -57,7 +57,7 @@ instance : AIG.LawfulVecOperator α AIG.ShiftTarget blastRotateRight where decl_eq := by intros unfold blastRotateRight - dsimp only + dsimp only; rfl end bitblast end BVExpr diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.lean index 0856ab2f50..a1b53670c9 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.lean @@ -117,7 +117,7 @@ instance : AIG.LawfulVecOperator α AIG.ShiftTarget blastArithShiftRightConst wh decl_eq := by intros unfold blastArithShiftRightConst - simp + simp; rfl structure TwoPowShiftTarget (aig : AIG α) (w : Nat) where n : Nat diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.lean index 9f2c0dfc1c..fb123f7aa3 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.lean @@ -52,6 +52,7 @@ theorem aux4 {a b c : Nat} (hidx : a < b * c) (h : c ≤ n) : a < b * n := by | inl h => apply aux3 <;> assumption | inr h => simp_all +set_option backward.isDefEq.respectTransparency false in theorem go_get_aux (aig : AIG α) (n : Nat) (curr : Nat) (hcurr : curr ≤ n) (input : AIG.RefVec aig w) (s : AIG.RefVec aig (w * curr)) : ∀ (idx : Nat) (hidx : idx < w * curr), @@ -72,6 +73,7 @@ theorem go_get_aux (aig : AIG α) (n : Nat) (curr : Nat) (hcurr : curr ≤ n) simp termination_by n - curr +set_option backward.isDefEq.respectTransparency false in theorem go_get (aig : AIG α) (n : Nat) (curr : Nat) (hcurr : curr ≤ n) (input : AIG.RefVec aig w) (s : AIG.RefVec aig (w * curr)) : ∀ (idx : Nat) (hidx1 : idx < w * n), diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean index 5bb664e7f5..7e2bd3f500 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean @@ -358,6 +358,7 @@ theorem deleteOne_preserves_assignments_size {n : Nat} (f : DefaultFormula n) (i simp only [deleteOne] grind +set_option backward.isDefEq.respectTransparency false in theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFormula n) (id : Nat) : StrongAssignmentsInvariant f → StrongAssignmentsInvariant (deleteOne f id) := by intro hf diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean index e4e1a0412c..858292b790 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean @@ -403,6 +403,7 @@ theorem c_without_negPivot_of_performRatCheck_success {n : Nat} (f : DefaultForm rw [DefaultFormula.formulaEntails_def, List.all_eq_true] at pfc exact of_decide_eq_true (pfc (c.delete negPivot) (by simp [insert_iff])) +set_option backward.isDefEq.respectTransparency false in theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n) (f_readyForRatAdd : ReadyForRatAdd f) (pivot : Literal (PosFin n)) (ratHints : Array (Nat × Array Nat)) diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean index 38ca3ff46b..6635cb8174 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean @@ -951,6 +951,7 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n) specialize h3 ⟨j.1, j_in_bounds⟩ j_ne_k simp only [derivedLits_arr_def, Fin.getElem_fin] at li_eq_lj simp only [Fin.getElem_fin, derivedLits_arr_def, ne_eq, li, li_eq_lj] at h3 + set_option backward.isDefEq.respectTransparency false in simp only [List.get_eq_getElem, ← Array.getElem_toList, not_true_eq_false] at h3 next k_ne_i => have i_ne_k : ⟨i.1, i_in_bounds⟩ ≠ k := by intro i_eq_k; simp only [← i_eq_k, not_true] at k_ne_i diff --git a/src/Std/Time/Date/ValidDate.lean b/src/Std/Time/Date/ValidDate.lean index 6c84059764..dada36eb02 100644 --- a/src/Std/Time/Date/ValidDate.lean +++ b/src/Std/Time/Date/ValidDate.lean @@ -57,6 +57,7 @@ def dayOfYear (ordinal : ValidDate leap) : Day.Ordinal.OfYear leap := | true, bounded => bounded | false, bounded => bounded +set_option backward.isDefEq.respectTransparency false in /-- Transforms a `Day.Ordinal.OfYear` into a tuple of a `Month` and a `Day`. -/ diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 79a0e58edd..3730fe85fa 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -12,6 +12,7 @@ options get_default_options() { // switch to `true` for ABI-breaking changes affecting meta code; // see also next option! opts = opts.update({"interpreter", "prefer_native"}, false); + opts = opts.update({"backward", "isDefEq", "respectTransparency"}, true); // switch to `false` when enabling `prefer_native` should also affect use // of built-in parsers in quotations; this is usually the case, but setting // both to `true` may be necessary for handling non-builtin parsers with diff --git a/tests/lean/beginEndAsMacro.lean b/tests/lean/beginEndAsMacro.lean index 5e66e90c8e..1cdab8b12b 100644 --- a/tests/lean/beginEndAsMacro.lean +++ b/tests/lean/beginEndAsMacro.lean @@ -8,7 +8,7 @@ macro "begin " ts:tactic,*,? i:"end" : term => do theorem ex1 (x : Nat) : x + 0 = 0 + x := begin rw [Nat.add_zero], - rw [Nat.zero_add], + rw [Nat.zero_add] end /- ANCHOR_END: doc -/ diff --git a/tests/lean/run/1302.lean b/tests/lean/run/1302.lean index baab71aece..5c70da2de9 100644 --- a/tests/lean/run/1302.lean +++ b/tests/lean/run/1302.lean @@ -10,4 +10,8 @@ example (a : Bool) : (a :: as).get ⟨0, by simp +arith⟩ = a := by simp example (a b c : α) : [a, b, c].get ⟨0, by simp (config := { decide := true })⟩ = a := by - rw [Fin.zero_eta, get_cons_zero] + erw [Fin.zero_eta] + rw [get_cons_zero] + +example (a b c : α) : [a, b, c].get ⟨0, by simp (config := { decide := true })⟩ = a := by + rw [List.get] diff --git a/tests/lean/run/1986.lean b/tests/lean/run/1986.lean index 6923b53d08..0a4e1bf962 100644 --- a/tests/lean/run/1986.lean +++ b/tests/lean/run/1986.lean @@ -197,7 +197,7 @@ instance Pi.completeDistribLattice' {ι : Type _} {π : ι → Type _} CompleteDistribLattice.mk (Pi.coframe.infᵢ_sup_le_sup_infₛ) -- User: takes around 2 seconds wall clock time on my PC (but very quick in Lean 3) -set_option maxHeartbeats 400 -- make sure it stays fast +set_option maxHeartbeats 600 -- make sure it stays fast set_option synthInstance.maxHeartbeats 400 instance Pi.completeDistribLattice'' {ι : Type _} {π : ι → Type _} [∀ i, CompleteDistribLattice (π i)] : CompleteDistribLattice (∀ i, π i) := diff --git a/tests/lean/run/3807.lean b/tests/lean/run/3807.lean index c2e7988447..ce26f3f233 100644 --- a/tests/lean/run/3807.lean +++ b/tests/lean/run/3807.lean @@ -1,5 +1,4 @@ import Lean.Elab.Binders - /-! This is a test case extracted from Mathlib exhibiting a slow-down in `IsDefEq` after @@ -12,9 +11,6 @@ but I think it makes a better test case going forward as is. The original declaration take around 16,000 heartbeats prior to #3807, but around 210,000 after. -/ - - - section Mathlib.Tactic.Spread open Lean Parser.Term Macro @@ -1151,6 +1147,7 @@ variable [FunLike F α β] variable {_ : NonAssocSemiring α} {_ : NonAssocSemiring β} [RingHomClass F α β] +@[instance_reducible] def RingHomClass.toRingHom (f : F) : α →+* β := { (f : α →* β), (f : α →+ β) with } @@ -1178,6 +1175,7 @@ end coe variable {_ : NonAssocSemiring α} {_ : NonAssocSemiring β} {_ : NonAssocSemiring γ} +@[instance_reducible] def comp (g : β →+* γ) (f : α →+* β) : α →+* γ := { g.toNonUnitalRingHom.comp f.toNonUnitalRingHom with toFun := g ∘ f @@ -1196,33 +1194,41 @@ namespace Injective variable {M₁ : Type _} {M₂ : Type _} [Mul M₁] +@[instance_reducible] protected def semigroup [Semigroup M₂] (f : M₁ → M₂) (hf : Injective f) : Semigroup M₁ := { ‹Mul M₁› with mul_assoc := sorry } +@[instance_reducible] protected def addSemigroup {M₁} [Add M₁] [AddSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) : AddSemigroup M₁ := { ‹Add M₁› with add_assoc := sorry } +@[instance_reducible] protected def commMagma [CommMagma M₂] (f : M₁ → M₂) (hf : Injective f) : CommMagma M₁ where mul_comm x y := sorry +@[instance_reducible] protected def addCommMagma {M₁} [Add M₁] [AddCommMagma M₂] (f : M₁ → M₂) (hf : Injective f) : AddCommMagma M₁ where add_comm x y := sorry +@[instance_reducible] protected def commSemigroup [CommSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) : CommSemigroup M₁ where toSemigroup := hf.semigroup f __ := hf.commMagma f +@[instance_reducible] protected def addCommSemigroup {M₁} [Add M₁] [AddCommSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) : AddCommSemigroup M₁ where toAddSemigroup := hf.addSemigroup f __ := hf.addCommMagma f variable [One M₁] +@[instance_reducible] protected def mulOneClass [MulOneClass M₂] (f : M₁ → M₂) (hf : Injective f) : MulOneClass M₁ := { ‹One M₁›, ‹Mul M₁› with one_mul := sorry, mul_one := sorry } +@[instance_reducible] protected def addZeroClass {M₁} [Zero M₁] [Add M₁] [AddZeroClass M₂] (f : M₁ → M₂) (hf : Injective f) : AddZeroClass M₁ := { ‹Zero M₁›, ‹Add M₁› with zero_add := sorry, @@ -1230,18 +1236,21 @@ protected def addZeroClass {M₁} [Zero M₁] [Add M₁] [AddZeroClass M₂] (f variable [Pow M₁ Nat] +@[instance_reducible] protected def monoid [Monoid M₂] (f : M₁ → M₂) (hf : Injective f) : Monoid M₁ := { hf.mulOneClass f, hf.semigroup f with npow := fun n x => x ^ n, npow_zero := sorry, npow_succ := sorry } +@[instance_reducible] protected def addMonoid {M₁} [Zero M₁] [Add M₁] [SMul Nat M₁] [AddMonoid M₂] (f : M₁ → M₂) (hf : Injective f) : AddMonoid M₁ := { hf.addZeroClass f, hf.addSemigroup f with nsmul := fun n x => n • x, nsmul_zero := sorry, nsmul_succ := sorry } +@[instance_reducible] protected def addMonoidWithOne {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul Nat M₁] [NatCast M₁] [AddMonoidWithOne M₂] (f : M₁ → M₂) (hf : Injective f) : AddMonoidWithOne M₁ := { hf.addMonoid f with @@ -1250,16 +1259,19 @@ protected def addMonoidWithOne {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul Na natCast_succ := sorry, one := 1 } +@[instance_reducible] protected def commMonoid [CommMonoid M₂] (f : M₁ → M₂) (hf : Injective f) : CommMonoid M₁ := { hf.monoid f, hf.commSemigroup f with } +@[instance_reducible] protected def addCommMonoid {M₁} [Zero M₁] [Add M₁] [SMul Nat M₁] [AddCommMonoid M₂] (f : M₁ → M₂) (hf : Injective f) : AddCommMonoid M₁ := { hf.addMonoid f, hf.addCommSemigroup f with } variable [Inv M₁] [Div M₁] [Pow M₁ Int] +@[instance_reducible] protected def divInvMonoid [DivInvMonoid M₂] (f : M₁ → M₂) (hf : Injective f) : DivInvMonoid M₁ := { hf.monoid f, ‹Inv M₁›, ‹Div M₁› with zpow := fun n x => x ^ n, @@ -1268,6 +1280,7 @@ protected def divInvMonoid [DivInvMonoid M₂] (f : M₁ → M₂) (hf : Injecti zpow_neg' := sorry, div_eq_mul_inv := sorry } +@[instance_reducible] protected def subNegMonoid {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul Nat M₁] [Neg M₁] [Sub M₁] [SMul Int M₁] [SubNegMonoid M₂] (f : M₁ → M₂) (hf : Injective f) : SubNegMonoid M₁ := { hf.addMonoid f, ‹Neg M₁›, ‹Sub M₁› with @@ -1277,15 +1290,18 @@ protected def subNegMonoid {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul Nat M zsmul_neg' := sorry, sub_eq_add_neg := sorry } +@[instance_reducible] protected def group [Group M₂] (f : M₁ → M₂) (hf : Injective f) : Group M₁ := { hf.divInvMonoid f with mul_left_inv := sorry } +@[instance_reducible] protected def addGroup {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul Nat M₁] [Neg M₁] [Sub M₁] [SMul Int M₁] [AddGroup M₂] (f : M₁ → M₂) (hf : Injective f) : AddGroup M₁ := { hf.subNegMonoid f with add_left_neg := sorry } +@[instance_reducible] protected def addGroupWithOne {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul Nat M₁] [Neg M₁] [Sub M₁] [SMul Int M₁] [NatCast M₁] [IntCast M₁] [AddGroupWithOne M₂] (f : M₁ → M₂) (hf : Injective f) : AddGroupWithOne M₁ := { hf.addGroup f, @@ -1294,9 +1310,11 @@ protected def addGroupWithOne {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul Nat intCast_ofNat := sorry, intCast_negSucc := sorry } +@[instance_reducible] protected def commGroup [CommGroup M₂] (f : M₁ → M₂) (hf : Injective f) : CommGroup M₁ := { hf.commMonoid f, hf.group f with } +@[instance_reducible] protected def addCommGroup {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul Nat M₁] [Neg M₁] [Sub M₁] [SMul Int M₁] [AddCommGroup M₂] (f : M₁ → M₂) (hf : Injective f) : AddCommGroup M₁ := { hf.addCommMonoid f, hf.addGroup f with } @@ -1316,6 +1334,7 @@ section MulZeroClass variable [MulZeroClass M₀] {a b : M₀} +@[instance_reducible] protected def Function.Injective.mulZeroClass [Mul M₀'] [Zero M₀'] (f : M₀' → M₀) (hf : Injective f) : MulZeroClass M₀' where mul := (· * ·) zero := 0 @@ -1328,6 +1347,7 @@ section MulZeroOneClass variable [MulZeroOneClass M₀] +@[instance_reducible] protected def Function.Injective.mulZeroOneClass [Mul M₀'] [Zero M₀'] [One M₀'] (f : M₀' → M₀) (hf : Injective f) : MulZeroOneClass M₀' := @@ -1337,6 +1357,7 @@ end MulZeroOneClass section SemigroupWithZero +@[instance_reducible] protected def Function.Injective.semigroupWithZero [Zero M₀'] [Mul M₀'] [SemigroupWithZero M₀] (f : M₀' → M₀) (hf : Injective f) : SemigroupWithZero M₀' := @@ -1346,6 +1367,7 @@ end SemigroupWithZero section MonoidWithZero +@[instance_reducible] protected def Function.Injective.monoidWithZero [Zero M₀'] [Mul M₀'] [One M₀'] [Pow M₀' Nat] [MonoidWithZero M₀] (f : M₀' → M₀) (hf : Injective f) : MonoidWithZero M₀' := @@ -1357,6 +1379,7 @@ section GroupWithZero variable [GroupWithZero G₀] {a b c g h x : G₀} +@[instance_reducible] protected def Function.Injective.groupWithZero [Zero G₀'] [Mul G₀'] [One G₀'] [Inv G₀'] [Div G₀'] [Pow G₀' Nat] [Pow G₀' Int] (f : G₀' → G₀) (hf : Injective f) : GroupWithZero G₀' := { hf.monoidWithZero f, @@ -1376,6 +1399,7 @@ universe u v x variable {α : Type u} {β : Type v} {R : Type x} +@[instance_reducible] protected def Function.Injective.distrib {S} [Mul R] [Add R] [Distrib S] (f : R → S) (hf : Injective f) : Distrib R where @@ -1385,28 +1409,33 @@ protected def Function.Injective.distrib {S} [Mul R] [Add R] [Distrib S] (f : R variable [Zero β] [One β] [Add β] [Mul β] [Neg β] [Sub β] [SMul Nat β] [SMul Int β] [Pow β Nat] [NatCast β] [IntCast β] +@[instance_reducible] protected def Function.Injective.nonUnitalNonAssocSemiring {α : Type u} [NonUnitalNonAssocSemiring α] (f : β → α) (hf : Injective f) : NonUnitalNonAssocSemiring β where toAddCommMonoid := hf.addCommMonoid f __ := hf.distrib f __ := hf.mulZeroClass f +@[instance_reducible] protected def Function.Injective.nonUnitalSemiring {α : Type u} [NonUnitalSemiring α] (f : β → α) (hf : Injective f) : NonUnitalSemiring β where toNonUnitalNonAssocSemiring := hf.nonUnitalNonAssocSemiring f __ := hf.semigroupWithZero f +@[instance_reducible] protected def Function.Injective.nonAssocSemiring {α : Type u} [NonAssocSemiring α] [NatCast β] (f : β → α) (hf : Injective f) : NonAssocSemiring β where toNonUnitalNonAssocSemiring := hf.nonUnitalNonAssocSemiring f __ := hf.mulZeroOneClass f __ := hf.addMonoidWithOne f +@[instance_reducible] protected def Function.Injective.semiring {α : Type u} [Semiring α] [NatCast β] (f : β → α) (hf : Injective f) : Semiring β where toNonUnitalSemiring := hf.nonUnitalSemiring f __ := hf.nonAssocSemiring f __ := hf.monoidWithZero f +@[instance_reducible] protected def Function.Injective.ring [Ring α] (f : β → α) (hf : Injective f) : Ring β where toSemiring := hf.semiring f __ := hf.addGroupWithOne f diff --git a/tests/lean/run/4171.lean b/tests/lean/run/4171.lean index a73c49603d..fba0b819c1 100644 --- a/tests/lean/run/4171.lean +++ b/tests/lean/run/4171.lean @@ -685,6 +685,7 @@ def toComon_ : Comon_ (Mon_ C) ⥤ Comon_ C := (Mon_.forget C).mapComon theorem foo {V} [Quiver V] {X Y x} : @Quiver.Hom.unop V _ X Y (Opposite.op (unop := x)) = x := rfl +set_option backward.isDefEq.respectTransparency false in example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where X := (toComon_ C).obj M one := { hom := M.X.one } @@ -693,6 +694,7 @@ example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where ext simp [(foo)] -- parentheses around `foo` works +set_option backward.isDefEq.respectTransparency false in example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where X := (toComon_ C).obj M one := { hom := M.X.one } @@ -704,6 +706,7 @@ example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where theorem foo' {V} [Quiver V] {X Y x} : @Quiver.Hom.unop V _ X Y no_index (Opposite.op (unop := x)) = x := rfl +set_option backward.isDefEq.respectTransparency false in example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where X := (toComon_ C).obj M one := { hom := M.X.one } @@ -713,6 +716,7 @@ example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where simp [foo'] -- or adding a `no_index` in the statement +set_option backward.isDefEq.respectTransparency false in /-- trace: [simp] Diagnostics [simp] theorems with bad keys @@ -734,6 +738,7 @@ example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where attribute [simp] foo +set_option backward.isDefEq.respectTransparency false in /-- trace: [simp] Diagnostics [simp] theorems with bad keys diff --git a/tests/lean/run/doLogicTests.lean b/tests/lean/run/doLogicTests.lean index 3a21a15bff..50dc8b1918 100644 --- a/tests/lean/run/doLogicTests.lean +++ b/tests/lean/run/doLogicTests.lean @@ -570,6 +570,7 @@ instance Result.instWP : WP Result (.except Error .pure) where | .fail e => wp (throw e : Except Error _) | .div => PredTrans.const ⌜False⌝ +set_option backward.isDefEq.respectTransparency false in instance Result.instWPMonad : WPMonad Result (.except Error .pure) where wp_pure _ := by ext Q; simp [wp] wp_bind x f := by @@ -577,6 +578,7 @@ instance Result.instWPMonad : WPMonad Result (.except Error .pure) where ext Q grind +set_option backward.isDefEq.respectTransparency false in theorem Result.of_wp {α} {x : Result α} (P : Result α → Prop) : (⊢ₛ wp⟦x⟧ post⟨fun a => ⌜P (.ok a)⌝, fun e => ⌜P (.fail e)⌝⟩) → P x := by intro hspec diff --git a/tests/lean/run/mvcgenTutorial.lean b/tests/lean/run/mvcgenTutorial.lean index 37c82c89ec..175dac740b 100644 --- a/tests/lean/run/mvcgenTutorial.lean +++ b/tests/lean/run/mvcgenTutorial.lean @@ -220,6 +220,7 @@ instance Result.instWP : WP Result (.except Error .pure) where | .fail e => wp (throw e : Except Error _) | .div => PredTrans.const ⌜False⌝ +set_option backward.isDefEq.respectTransparency false in instance Result.instWPMonad : WPMonad Result (.except Error .pure) where wp_pure _ := by ext Q diff --git a/tests/lean/run/ofNatNormNum.lean b/tests/lean/run/ofNatNormNum.lean index 5182cb85a7..734d1cc72e 100644 --- a/tests/lean/run/ofNatNormNum.lean +++ b/tests/lean/run/ofNatNormNum.lean @@ -26,12 +26,12 @@ instance [S α] : OfNat α n where instance [S α] : OfNatSound α where ofNat_add n m := by induction m with - | zero => simp [S.ofNat]; erw [S.add_zero]; done + | zero => simp; erw [S.add_zero]; rfl | succ m ih => simp [OfNat.ofNat, S.ofNat] at *; erw [← ih]; rw [S.add_assoc] theorem S.ofNat_mul [S α] (n m : Nat) : (OfNat.ofNat n : α) * OfNat.ofNat m = OfNat.ofNat (n * m) := by induction m with - | zero => rw [S.mul_zero, Nat.mul_zero] + | zero => rw [Nat.mul_zero]; erw [S.mul_zero]; rfl | succ m ih => show OfNat.ofNat (α := α) n * OfNat.ofNat (m + 1) = OfNat.ofNat (n * m.succ) rw [Nat.mul_succ, ← ofNat_add, ← ofNat_add, ← ih, left_distrib] diff --git a/tests/lean/run/structWithAlgTCSynth.lean b/tests/lean/run/structWithAlgTCSynth.lean index 0107703e29..6c96ee448f 100644 --- a/tests/lean/run/structWithAlgTCSynth.lean +++ b/tests/lean/run/structWithAlgTCSynth.lean @@ -1265,7 +1265,7 @@ variable (R : Type u) [CommSemiring R] (M : Type v) inductive r : (MvPolynomial M R) → (MvPolynomial M R) → Prop -def Quot_r := RingQuot (r R M) +abbrev Quot_r := RingQuot (r R M) instance : Semiring (Quot_r R M) := RingQuot.instSemiring _