From ab26eaf647c36df820450f3a1efdc414194c3be3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 19 Feb 2026 19:28:48 -0800 Subject: [PATCH] feat: enable implicit argument transparency bump (part 2) (#12572) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR is part 2 of the `implicit_reducible` refactoring (part 1: #12567). **Background.** When Lean checks definitional equality of function applications `f a₁ ... aₙ =?= f b₁ ... bₙ`, it compares arguments `aᵢ =?= bᵢ` at a transparency level determined by the binder type. Previously, only instance-implicit (`[C]`) arguments received a transparency bump to `.instances`. With `backward.isDefEq.implicitBump` enabled, ALL implicit arguments (`{x}`, `⦃x⦄`, and `[x]`) are bumped to `.instances`, so that definitions marked `[implicit_reducible]` unfold when comparing implicit arguments. This is important because implicit arguments often carry type information (e.g., `P (i + 0)` vs `P i`) where the mismatch is in non-proof positions (Sort arguments to `cast`) — proof irrelevance does not help here, so the relevant definitions must actually unfold. **`[implicit_reducible]`** (renamed from `[instance_reducible]` in part 1) marks definitions that should unfold at `TransparencyMode.instances` — between `[reducible]` (unfolds at `.reducible` and above) and the default `[semireducible]` (unfolds only at `.default` and above). This is the right level for core arithmetic operations that appear in type indices. ## Changes - **Enable `backward.isDefEq.implicitBump` by default** and set it in `stage0/src/stdlib_flags.h` so stage0 also compiles with it - **Mark `Nat.add`, `Nat.mul`, `Nat.sub`, `Array.size` as `[implicit_reducible]`** so they unfold when comparing implicit arguments at `.instances` transparency - **Remove redundant unification hints** (`n + 0 =?= n`, `n - 0 =?= n`, `n * 0 =?= 0`) that are now handled by `[implicit_reducible]` - **Rename all remaining `[instance_reducible]` attribute usages** to `[implicit_reducible]` across the codebase (the old name remains as an alias) - **Remove 28 `set_option backward.isDefEq.respectTransparency false in`** workarounds that are no longer needed 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.6 --------- Co-authored-by: Claude Opus 4.6 --- src/Init/Classical.lean | 2 +- src/Init/Control/Lawful/Instances.lean | 5 +- src/Init/Control/MonadAttach.lean | 2 +- src/Init/Data/Array/Basic.lean | 2 +- src/Init/Data/Array/Find.lean | 1 - src/Init/Data/Array/Lemmas.lean | 4 +- src/Init/Data/Array/MapIdx.lean | 2 - src/Init/Data/Array/OfFn.lean | 2 - src/Init/Data/BitVec/Lemmas.lean | 9 +-- src/Init/Data/Bool.lean | 2 +- src/Init/Data/Char/Lemmas.lean | 2 +- src/Init/Data/Fin/Fold.lean | 8 +-- src/Init/Data/Fin/Iterate.lean | 2 +- src/Init/Data/Fin/Lemmas.lean | 4 +- .../Lemmas/Combinators/FilterMap.lean | 1 - .../Data/Iterators/Lemmas/Producers/List.lean | 3 +- .../Lemmas/Producers/Monadic/List.lean | 2 +- src/Init/Data/List/Lemmas.lean | 2 +- src/Init/Data/List/MapIdx.lean | 1 - src/Init/Data/List/OfFn.lean | 2 - src/Init/Data/List/ToArray.lean | 6 +- src/Init/Data/Nat/Fold.lean | 2 - src/Init/Data/Option/Attach.lean | 2 - src/Init/Data/Ord/Basic.lean | 14 ++-- src/Init/Data/Order/Factories.lean | 4 +- src/Init/Data/Order/FactoriesExtra.lean | 6 +- src/Init/Data/Order/Opposite.lean | 2 +- src/Init/Data/Order/PackageFactories.lean | 8 +-- .../Data/Range/Polymorphic/RangeIterator.lean | 6 +- src/Init/Data/SInt/Basic.lean | 20 +++--- src/Init/Data/Slice/Array/Iterator.lean | 2 +- src/Init/Data/Slice/Array/Lemmas.lean | 2 +- src/Init/Data/Slice/List/Iterator.lean | 2 +- .../Data/String/Lemmas/Pattern/Basic.lean | 1 - .../Data/String/Lemmas/Pattern/Split.lean | 1 - src/Init/Data/UInt/Basic.lean | 8 +-- src/Init/Data/UInt/BasicAux.lean | 4 +- src/Init/Data/Vector/Algebra.lean | 2 +- src/Init/Data/Vector/Extract.lean | 3 +- src/Init/Data/Vector/Lemmas.lean | 2 +- src/Init/Data/Vector/OfFn.lean | 1 - src/Init/Grind/Module/Basic.lean | 4 +- src/Init/Grind/Module/Envelope.lean | 2 +- src/Init/Grind/Ring/Basic.lean | 6 +- src/Init/Grind/Ring/Envelope.lean | 4 +- src/Init/Grind/Ring/Field.lean | 2 +- src/Init/GrindInstances/Ring/SInt.lean | 20 +++--- src/Init/GrindInstances/Ring/UInt.lean | 20 +++--- src/Init/Hints.lean | 8 --- src/Init/Prelude.lean | 16 ++--- src/Init/WF.lean | 8 +-- src/Lean/Meta/ExprDefEq.lean | 2 +- src/Std/Data/DHashMap/IteratorLemmas.lean | 4 +- src/Std/Data/DHashMap/Lemmas.lean | 2 +- src/Std/Data/DTreeMap/Internal/Zipper.lean | 56 ++++++++-------- src/Std/Data/DTreeMap/Lemmas.lean | 2 +- .../Lemmas/Producers/Monadic/Array.lean | 1 - .../Lemmas/Producers/Monadic/List.lean | 1 - .../Iterators/Lemmas/Producers/Repeat.lean | 1 - .../Circuit/Lemmas/Operations/Replicate.lean | 2 - src/lake/Lake/Build/Data.lean | 2 +- stage0/src/stdlib_flags.h | 2 + tests/lean/ppMotives.lean.expected.out | 4 +- tests/lean/run/3807.lean | 66 +++++++++---------- tests/lean/run/boxing_bug.lean | 2 +- tests/lean/run/diagnostics.lean | 6 +- tests/lean/run/grind_10160.lean | 2 +- tests/lean/run/grind_bitvec2.lean | 5 +- tests/lean/run/instanceReducibility.lean | 2 +- tests/lean/run/instanceReducible.lean | 2 +- tests/lean/run/ofNatNormNum.lean | 2 +- .../symbolFrequency_foldRelevantConsts.lean | 2 +- tests/lean/unfold1.lean | 3 - tests/lean/unfold1.lean.expected.out | 8 +-- tests/lean/whnfProj.lean.expected.out | 2 +- 75 files changed, 191 insertions(+), 236 deletions(-) diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean index 9f4dee03f8..aae447d34c 100644 --- a/src/Init/Classical.lean +++ b/src/Init/Classical.lean @@ -142,7 +142,7 @@ is classically true but not constructively. -/ /-- Transfer decidability of `¬ p` to decidability of `p`. -/ -- This can not be an instance as it would be tried everywhere. -@[instance_reducible] +@[implicit_reducible] def decidable_of_decidable_not (p : Prop) [h : Decidable (¬ p)] : Decidable p := match h with | isFalse h => isTrue (Classical.not_not.mp h) diff --git a/src/Init/Control/Lawful/Instances.lean b/src/Init/Control/Lawful/Instances.lean index fd0cac9eb9..510a57d133 100644 --- a/src/Init/Control/Lawful/Instances.lean +++ b/src/Init/Control/Lawful/Instances.lean @@ -258,7 +258,6 @@ 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] @@ -346,10 +345,9 @@ 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] + simp [controlAt]; exact bind_pure _ @[simp] theorem run_control [Monad m] [LawfulMonad m] (f : ({β : Type u} → ReaderT ρ m β → m (stM m (ReaderT ρ m) β)) → m (stM m (ReaderT ρ m) α)) (ctx : ρ) : ReaderT.run (control f) ctx = f fun x => x.run ctx := run_controlAt f ctx @@ -447,7 +445,6 @@ 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/MonadAttach.lean b/src/Init/Control/MonadAttach.lean index 49d5167b24..b62a6add2c 100644 --- a/src/Init/Control/MonadAttach.lean +++ b/src/Init/Control/MonadAttach.lean @@ -70,7 +70,7 @@ information to the return value, except a trivial proof of {name}`True`. This instance is used whenever no more useful {name}`MonadAttach` instance can be implemented. It always has a {name}`WeaklyLawfulMonadAttach`, but usually no {name}`LawfulMonadAttach` instance. -/ -@[expose, instance_reducible] +@[expose, implicit_reducible] public protected def MonadAttach.trivial {m : Type u → Type v} [Monad m] : MonadAttach m where CanReturn _ _ := True attach x := (⟨·, .intro⟩) <$> x diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index cddd2a50ea..09b114bbb8 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]; rfl + simp only [Array.size] /-- `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/Find.lean b/src/Init/Data/Array/Find.lean index 660b62fef0..eb29c3359a 100644 --- a/src/Init/Data/Array/Find.lean +++ b/src/Init/Data/Array/Find.lean @@ -723,7 +723,6 @@ 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 diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index ab5b3dfe0d..f8cdb902eb 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -896,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]; rfl + simp only [set, ← getElem_toList, List.getElem_set_ne h] @[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 @@ -2855,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; rfl + simp @[simp] theorem extract_size {xs : Array α} : xs.extract 0 xs.size = xs := by apply ext diff --git a/src/Init/Data/Array/MapIdx.lean b/src/Init/Data/Array/MapIdx.lean index 5afea12fe2..98defc1447 100644 --- a/src/Init/Data/Array/MapIdx.lean +++ b/src/Init/Data/Array/MapIdx.lean @@ -72,7 +72,6 @@ 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 @@ -106,7 +105,6 @@ 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 963cfb9549..88c58cc7d9 100644 --- a/src/Init/Data/Array/OfFn.lean +++ b/src/Init/Data/Array/OfFn.lean @@ -41,7 +41,6 @@ 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 @@ -108,7 +107,6 @@ 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/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 56941ece09..ef64c6a9b0 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']; rfl + simp [BitVec.msb, getMsbD_extractLsb'] @[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]; rfl + simp [BitVec.msb] 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 @@ -2784,9 +2784,8 @@ 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; rfl + simp -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 @@ -5292,7 +5291,6 @@ 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 @@ -5344,7 +5342,6 @@ 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/Bool.lean b/src/Init/Data/Bool.lean index 5e097556b4..b680f85f53 100644 --- a/src/Init/Data/Bool.lean +++ b/src/Init/Data/Bool.lean @@ -636,7 +636,7 @@ def boolPredToPred : Coe (α → Bool) (α → Prop) where This should not be turned on globally as an instance because it degrades performance in Mathlib, but may be used locally. -/ -@[expose, instance_reducible] def boolRelToRel : Coe (α → α → Bool) (α → α → Prop) where +@[expose, implicit_reducible] def boolRelToRel : Coe (α → α → Bool) (α → α → Prop) where coe r := fun a b => Eq (r a b) true /-! ### subtypes -/ diff --git a/src/Init/Data/Char/Lemmas.lean b/src/Init/Data/Char/Lemmas.lean index e8727e877e..25514c8f25 100644 --- a/src/Init/Data/Char/Lemmas.lean +++ b/src/Init/Data/Char/Lemmas.lean @@ -50,7 +50,7 @@ instance ltTrans : Trans (· < · : Char → Char → Prop) (· < ·) (· < ·) trans := Char.lt_trans -- This instance is useful while setting up instances for `String`. -@[instance_reducible] +@[implicit_reducible] def notLTTrans : Trans (¬ · < · : Char → Char → Prop) (¬ · < ·) (¬ · < ·) where trans h₁ h₂ := by simpa using Char.le_trans (by simpa using h₂) (by simpa using h₁) diff --git a/src/Init/Data/Fin/Fold.lean b/src/Init/Data/Fin/Fold.lean index 562bfc29c5..6a447971e9 100644 --- a/src/Init/Data/Fin/Fold.lean +++ b/src/Init/Data/Fin/Fold.lean @@ -164,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]; rfl + simp [foldlM_succ_last, ← Nat.add_assoc, ih] /-! ### foldrM -/ @@ -222,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]; rfl + simp [foldrM_succ_last, ← Nat.add_assoc, ih] /-! ### foldl -/ @@ -268,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]; rfl + | succ m ih => simp [foldl_succ_last, ih, ← Nat.add_assoc] theorem foldl_eq_foldlM (f : α → Fin n → α) (x) : foldl n f x = (foldlM (m := Id) n (pure <| f · ·) x).run := by @@ -321,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]; rfl + | succ m ih => simp [foldr_succ_last, ih, ← Nat.add_assoc] 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 6434041503..0a1cd6d194 100644 --- a/src/Init/Data/Fin/Iterate.lean +++ b/src/Init/Data/Fin/Iterate.lean @@ -69,7 +69,7 @@ private theorem hIterateFrom_elim {P : Nat → Sort _}(Q : ∀(i : Nat), P i → have g : ¬ (i < n) := by simp at p; simp [p] have r : Q n (_root_.cast (congrArg P p) s) := @Eq.rec Nat i (fun k eq => Q k (_root_.cast (congrArg P eq) s)) init n p - simp only [g, r, dite_false] + simp only [g, dite_false]; exact r | succ j inv => unfold hIterateFrom have d : Nat.succ i + j = n := by simp [Nat.succ_add]; exact p diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean index 224da8e746..f149e36f63 100644 --- a/src/Init/Data/Fin/Lemmas.lean +++ b/src/Init/Data/Fin/Lemmas.lean @@ -123,7 +123,7 @@ For example, for `x : Fin k` and `n : Nat`, it causes `x < n` to be elaborated as `x < ↑n` rather than `↑x < n`, silently introducing wraparound arithmetic. -/ -@[expose, instance_reducible] +@[expose, implicit_reducible] def instNatCast (n : Nat) [NeZero n] : NatCast (Fin n) where natCast a := Fin.ofNat n a @@ -145,7 +145,7 @@ This is not a global instance, but may be activated locally via `open Fin.IntCas See the doc-string for `Fin.NatCast.instNatCast` for more details. -/ -@[expose, instance_reducible] +@[expose, implicit_reducible] def instIntCast (n : Nat) [NeZero n] : IntCast (Fin n) where intCast := Fin.intCast diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean index fc919fe55b..b2811ecdf3 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean @@ -750,7 +750,6 @@ 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/Producers/List.lean b/src/Init/Data/Iterators/Lemmas/Producers/List.lean index 7ea26c0745..32a61c1306 100644 --- a/src/Init/Data/Iterators/Lemmas/Producers/List.lean +++ b/src/Init/Data/Iterators/Lemmas/Producers/List.lean @@ -23,7 +23,6 @@ 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 @@ -32,7 +31,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]; rfl + simp [List.iter, List.iterM, IterM.toIter, Iter.step_eq] @[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 5924c76916..58ed0a95c2 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]; rfl + simp only [List.iterM, IterM.step, Iterator.step] theorem List.step_iterM {l : List β} : (l.iterM m).step = match l with diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index a6bc3f9788..fe08754e69 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']; rfl + simp [h'] 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 diff --git a/src/Init/Data/List/MapIdx.lean b/src/Init/Data/List/MapIdx.lean index a5ee541d66..37501e4081 100644 --- a/src/Init/Data/List/MapIdx.lean +++ b/src/Init/Data/List/MapIdx.lean @@ -350,7 +350,6 @@ 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/OfFn.lean b/src/Init/Data/List/OfFn.lean index 51766ca7a4..44bbb2d7e2 100644 --- a/src/Init/Data/List/OfFn.lean +++ b/src/Init/Data/List/OfFn.lean @@ -99,7 +99,6 @@ theorem ofFn_add {n m} {f : Fin (n + m) → α} : induction m with | zero => simp | succ m ih => - set_option backward.isDefEq.respectTransparency false in simp [-ofFn_succ, ofFn_succ_last, ih] @[simp] @@ -157,7 +156,6 @@ theorem ofFnM_add {n m} [Monad m] [LawfulMonad m] {f : Fin (n + k) → m α} : induction k with | zero => simp | succ k ih => - set_option backward.isDefEq.respectTransparency false in simp [ofFnM_succ_last, ih] end List diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean index d6a052e7fd..94d90cf152 100644 --- a/src/Init/Data/List/ToArray.lean +++ b/src/Init/Data/List/ToArray.lean @@ -589,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; rfl + simp @[simp, grind =] theorem eraseIdx_toArray (l : List α) (i : Nat) (h : i < l.toArray.size) : l.toArray.eraseIdx i h = (l.eraseIdx i).toArray := by @@ -644,8 +644,8 @@ private theorem insertIdx_loop_toArray (i : Nat) (l : List α) (j : Nat) (hj : j drop_append_of_le_length (by simp; omega)] simp only [append_assoc, cons_append, nil_append] cases i with - | zero => simp; rfl - | succ i => rw [take_set_of_le (by omega)]; rfl + | zero => simp + | succ i => rw [take_set_of_le (by omega)] · 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 be23ade521..579a2bab97 100644 --- a/src/Init/Data/Nat/Fold.lean +++ b/src/Init/Data/Nat/Fold.lean @@ -400,7 +400,6 @@ 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 @@ -436,7 +435,6 @@ theorem dfoldRev_add induction m with | zero => simp; rfl | 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 f862c5b934..39cc812639 100644 --- a/src/Init/Data/Option/Attach.lean +++ b/src/Init/Data/Option/Attach.lean @@ -444,7 +444,6 @@ 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 @@ -456,7 +455,6 @@ 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/Ord/Basic.lean b/src/Init/Data/Ord/Basic.lean index b353591b16..dea4c6a5cb 100644 --- a/src/Init/Data/Ord/Basic.lean +++ b/src/Init/Data/Ord/Basic.lean @@ -619,7 +619,7 @@ protected theorem compare_nil_right_eq_eq {α} [Ord α] {xs : List α} : end List /-- The lexicographic order on pairs. -/ -@[expose, instance_reducible] +@[expose, implicit_reducible] def lexOrd [Ord α] [Ord β] : Ord (α × β) where compare := compareLex (compareOn (·.1)) (compareOn (·.2)) @@ -627,14 +627,14 @@ def lexOrd [Ord α] [Ord β] : Ord (α × β) where Constructs an `BEq` instance from an `Ord` instance that asserts that the result of `compare` is `Ordering.eq`. -/ -@[expose, instance_reducible] def beqOfOrd [Ord α] : BEq α where +@[expose, implicit_reducible] def beqOfOrd [Ord α] : BEq α where beq a b := (compare a b).isEq /-- Constructs an `LT` instance from an `Ord` instance that asserts that the result of `compare` is `Ordering.lt`. -/ -@[expose, instance_reducible] def ltOfOrd [Ord α] : LT α where +@[expose, implicit_reducible] def ltOfOrd [Ord α] : LT α where lt a b := compare a b = Ordering.lt @[inline] @@ -645,7 +645,7 @@ instance [Ord α] : DecidableRel (@LT.lt α ltOfOrd) := fun a b => Constructs an `LE` instance from an `Ord` instance that asserts that the result of `compare` satisfies `Ordering.isLE`. -/ -@[expose, instance_reducible] def leOfOrd [Ord α] : LE α where +@[expose, implicit_reducible] def leOfOrd [Ord α] : LE α where le a b := (compare a b).isLE @[inline] @@ -677,7 +677,7 @@ Inverts the order of an `Ord` instance. The result is an `Ord α` instance that returns `Ordering.lt` when `ord` would return `Ordering.gt` and that returns `Ordering.gt` when `ord` would return `Ordering.lt`. -/ -@[expose, instance_reducible] protected def opposite (ord : Ord α) : Ord α where +@[expose, implicit_reducible] protected def opposite (ord : Ord α) : Ord α where compare x y := ord.compare y x /-- @@ -688,7 +688,7 @@ In particular, `ord.on f` compares `x` and `y` by comparing `f x` and `f y` acco The function `compareOn` can be used to perform this comparison without constructing an intermediate `Ord` instance. -/ -@[expose, instance_reducible] protected def on (_ : Ord β) (f : α → β) : Ord α where +@[expose, implicit_reducible] protected def on (_ : Ord β) (f : α → β) : Ord α where compare := compareOn f /-- @@ -707,7 +707,7 @@ The function `compareLex` can be used to perform this comparison without constru intermediate `Ord` instance. `Ordering.then` can be used to lexicographically combine the results of comparisons. -/ -@[expose, instance_reducible] protected def lex' (ord₁ ord₂ : Ord α) : Ord α where +@[expose, implicit_reducible] protected def lex' (ord₁ ord₂ : Ord α) : Ord α where compare := compareLex ord₁.compare ord₂.compare end Ord diff --git a/src/Init/Data/Order/Factories.lean b/src/Init/Data/Order/Factories.lean index 0a6ed5325b..cbfcba3e1f 100644 --- a/src/Init/Data/Order/Factories.lean +++ b/src/Init/Data/Order/Factories.lean @@ -23,7 +23,7 @@ preferring `a` over `b` when in doubt. Has a `LawfulOrderLeftLeaningMin α` instance. -/ -@[inline, instance_reducible] +@[inline, implicit_reducible] public def _root_.Min.leftLeaningOfLE (α : Type u) [LE α] [DecidableLE α] : Min α where min a b := if a ≤ b then a else b @@ -33,7 +33,7 @@ preferring `a` over `b` when in doubt. Has a `LawfulOrderLeftLeaningMax α` instance. -/ -@[inline, instance_reducible] +@[inline, implicit_reducible] public def _root_.Max.leftLeaningOfLE (α : Type u) [LE α] [DecidableLE α] : Max α where max a b := if b ≤ a then a else b diff --git a/src/Init/Data/Order/FactoriesExtra.lean b/src/Init/Data/Order/FactoriesExtra.lean index 5a766f59b2..cbce850566 100644 --- a/src/Init/Data/Order/FactoriesExtra.lean +++ b/src/Init/Data/Order/FactoriesExtra.lean @@ -19,7 +19,7 @@ Creates an `LE α` instance from an `Ord α` instance. `OrientedOrd α` must be satisfied so that the resulting `LE α` instance faithfully represents the `Ord α` instance. -/ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def _root_.LE.ofOrd (α : Type u) [Ord α] : LE α where le a b := (compare a b).isLE @@ -39,7 +39,7 @@ Creates an `LT α` instance from an `Ord α` instance. `OrientedOrd α` must be satisfied so that the resulting `LT α` instance faithfully represents the `Ord α` instance. -/ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def _root_.LT.ofOrd (α : Type u) [Ord α] : LT α where lt a b := compare a b = .lt @@ -104,7 +104,7 @@ public def _root_.DecidableLT.ofOrd (α : Type u) [LE α] [LT α] [Ord α] [Lawf /-- Creates a `BEq α` instance from an `Ord α` instance. -/ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def _root_.BEq.ofOrd (α : Type u) [Ord α] : BEq α where beq a b := compare a b = .eq diff --git a/src/Init/Data/Order/Opposite.lean b/src/Init/Data/Order/Opposite.lean index d26ad4fe91..d8622fe601 100644 --- a/src/Init/Data/Order/Opposite.lean +++ b/src/Init/Data/Order/Opposite.lean @@ -52,7 +52,7 @@ def max' [LE α] [DecidableLE α] (a b : α) : α := Without the `open scoped` command, Lean would not find the required {lit}`DecidableLE α` instance for the opposite order. -/ -@[instance_reducible] def LE.opposite (le : LE α) : LE α where +@[implicit_reducible] def LE.opposite (le : LE α) : LE α where le a b := b ≤ a theorem LE.opposite_def {le : LE α} : diff --git a/src/Init/Data/Order/PackageFactories.lean b/src/Init/Data/Order/PackageFactories.lean index 44728a0615..c14364170d 100644 --- a/src/Init/Data/Order/PackageFactories.lean +++ b/src/Init/Data/Order/PackageFactories.lean @@ -169,7 +169,7 @@ automatically. If it fails, it is necessary to provide some of the fields manual * Other proof obligations, namely `le_refl` and `le_trans`, can be omitted if `Refl` and `Trans` instances can be synthesized. -/ -@[expose, instance_reducible] +@[expose, implicit_reducible] public def PreorderPackage.ofLE (α : Type u) (args : Packages.PreorderOfLEArgs α := by exact {}) : PreorderPackage α where toLE := args.le @@ -254,7 +254,7 @@ automatically. If it fails, it is necessary to provide some of the fields manual * Other proof obligations, namely `le_refl`, `le_trans` and `le_antisymm`, can be omitted if `Refl`, `Trans` and `Antisymm` instances can be synthesized. -/ -@[expose, instance_reducible] +@[expose, implicit_reducible] public def PartialOrderPackage.ofLE (α : Type u) (args : Packages.PartialOrderOfLEArgs α := by exact {}) : PartialOrderPackage α where toPreorderPackage := .ofLE α args.toPreorderOfLEArgs @@ -383,7 +383,7 @@ automatically. If it fails, it is necessary to provide some of the fields manual * Other proof obligations, namely `le_total` and `le_trans`, can be omitted if `Total` and `Trans` instances can be synthesized. -/ -@[expose, instance_reducible] +@[expose, implicit_reducible] public def LinearPreorderPackage.ofLE (α : Type u) (args : Packages.LinearPreorderOfLEArgs α := by exact {}) : LinearPreorderPackage α where toPreorderPackage := .ofLE α args.toPreorderOfLEArgs @@ -485,7 +485,7 @@ automatically. If it fails, it is necessary to provide some of the fields manual * Other proof obligations, namely `le_total`, `le_trans` and `le_antisymm`, can be omitted if `Total`, `Trans` and `Antisymm` instances can be synthesized. -/ -@[expose, instance_reducible] +@[expose, implicit_reducible] public def LinearOrderPackage.ofLE (α : Type u) (args : Packages.LinearOrderOfLEArgs α := by exact {}) : LinearOrderPackage α where toLinearPreorderPackage := .ofLE α args.toLinearPreorderOfLEArgs diff --git a/src/Init/Data/Range/Polymorphic/RangeIterator.lean b/src/Init/Data/Range/Polymorphic/RangeIterator.lean index f6b42833d0..2980b7dba4 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]; rfl + simp [Std.Iterator.step] theorem Iterator.isPlausibleStep_iff [UpwardEnumerable α] [LE α] [DecidableLE α] {it : Iter (α := Rxc.Iterator α) α} {step} : @@ -680,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]; rfl + simp [Std.Iterator.step] theorem Iterator.isPlausibleStep_iff [UpwardEnumerable α] [LT α] [DecidableLT α] {it : Iter (α := Rxo.Iterator α) α} {step} : @@ -1244,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]; rfl + simp [IterM.step, Std.Iterator.step] theorem Iterator.isPlausibleStep_iff [UpwardEnumerable α] {it : Iter (α := Rxi.Iterator α) α} {step} : diff --git a/src/Init/Data/SInt/Basic.lean b/src/Init/Data/SInt/Basic.lean index bae137bcf2..3c7574429f 100644 --- a/src/Init/Data/SInt/Basic.lean +++ b/src/Init/Data/SInt/Basic.lean @@ -409,7 +409,7 @@ Examples: * `(if (5 : Int8) < 5 then "yes" else "no") = "no"` * `show ¬((7 : Int8) < 7) by decide` -/ -@[extern "lean_int8_dec_lt", instance_reducible] +@[extern "lean_int8_dec_lt", implicit_reducible] def Int8.decLt (a b : Int8) : Decidable (a < b) := inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec)) @@ -425,7 +425,7 @@ Examples: * `(if (15 : Int8) ≤ 5 then "yes" else "no") = "no"` * `show (7 : Int8) ≤ 7 by decide` -/ -@[extern "lean_int8_dec_le", instance_reducible] +@[extern "lean_int8_dec_le", implicit_reducible] def Int8.decLe (a b : Int8) : Decidable (a ≤ b) := inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec)) @@ -778,7 +778,7 @@ Examples: * `(if (5 : Int16) < 5 then "yes" else "no") = "no"` * `show ¬((7 : Int16) < 7) by decide` -/ -@[extern "lean_int16_dec_lt", instance_reducible] +@[extern "lean_int16_dec_lt", implicit_reducible] def Int16.decLt (a b : Int16) : Decidable (a < b) := inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec)) @@ -794,7 +794,7 @@ Examples: * `(if (15 : Int16) ≤ 5 then "yes" else "no") = "no"` * `show (7 : Int16) ≤ 7 by decide` -/ -@[extern "lean_int16_dec_le", instance_reducible] +@[extern "lean_int16_dec_le", implicit_reducible] def Int16.decLe (a b : Int16) : Decidable (a ≤ b) := inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec)) @@ -1163,7 +1163,7 @@ Examples: * `(if (5 : Int32) < 5 then "yes" else "no") = "no"` * `show ¬((7 : Int32) < 7) by decide` -/ -@[extern "lean_int32_dec_lt", instance_reducible] +@[extern "lean_int32_dec_lt", implicit_reducible] def Int32.decLt (a b : Int32) : Decidable (a < b) := inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec)) @@ -1179,7 +1179,7 @@ Examples: * `(if (15 : Int32) ≤ 5 then "yes" else "no") = "no"` * `show (7 : Int32) ≤ 7 by decide` -/ -@[extern "lean_int32_dec_le", instance_reducible] +@[extern "lean_int32_dec_le", implicit_reducible] def Int32.decLe (a b : Int32) : Decidable (a ≤ b) := inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec)) @@ -1568,7 +1568,7 @@ Examples: * `(if (5 : Int64) < 5 then "yes" else "no") = "no"` * `show ¬((7 : Int64) < 7) by decide` -/ -@[extern "lean_int64_dec_lt", instance_reducible] +@[extern "lean_int64_dec_lt", implicit_reducible] def Int64.decLt (a b : Int64) : Decidable (a < b) := inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec)) /-- @@ -1583,7 +1583,7 @@ Examples: * `(if (15 : Int64) ≤ 5 then "yes" else "no") = "no"` * `show (7 : Int64) ≤ 7 by decide` -/ -@[extern "lean_int64_dec_le", instance_reducible] +@[extern "lean_int64_dec_le", implicit_reducible] def Int64.decLe (a b : Int64) : Decidable (a ≤ b) := inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec)) @@ -1958,7 +1958,7 @@ Examples: * `(if (5 : ISize) < 5 then "yes" else "no") = "no"` * `show ¬((7 : ISize) < 7) by decide` -/ -@[extern "lean_isize_dec_lt", instance_reducible] +@[extern "lean_isize_dec_lt", implicit_reducible] def ISize.decLt (a b : ISize) : Decidable (a < b) := inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec)) @@ -1974,7 +1974,7 @@ Examples: * `(if (15 : ISize) ≤ 5 then "yes" else "no") = "no"` * `show (7 : ISize) ≤ 7 by decide` -/ -@[extern "lean_isize_dec_le", instance_reducible] +@[extern "lean_isize_dec_le", implicit_reducible] def ISize.decLe (a b : ISize) : Decidable (a ≤ b) := inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec)) diff --git a/src/Init/Data/Slice/Array/Iterator.lean b/src/Init/Data/Slice/Array/Iterator.lean index cd2c4cbd9c..f566abdbf6 100644 --- a/src/Init/Data/Slice/Array/Iterator.lean +++ b/src/Init/Data/Slice/Array/Iterator.lean @@ -55,7 +55,7 @@ instance SubarrayIterator.instFinite : Finite (SubarrayIterator α) Id := instance [Monad m] : IteratorLoop (SubarrayIterator α) Id m := .defaultImplementation -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] def Subarray.instToIterator := ToIterator.of (γ := Slice (Internal.SubarrayData α)) (β := α) (SubarrayIterator α) (⟨⟨·⟩⟩) attribute [instance] Subarray.instToIterator diff --git a/src/Init/Data/Slice/Array/Lemmas.lean b/src/Init/Data/Slice/Array/Lemmas.lean index 43ec1e3bf6..680ba83638 100644 --- a/src/Init/Data/Slice/Array/Lemmas.lean +++ b/src/Init/Data/Slice/Array/Lemmas.lean @@ -278,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]; rfl + simp [getElem_eq_getElem_array, toList_eq_drop_take] 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/Iterator.lean b/src/Init/Data/Slice/List/Iterator.lean index 23e681c900..94688e9a73 100644 --- a/src/Init/Data/Slice/List/Iterator.lean +++ b/src/Init/Data/Slice/List/Iterator.lean @@ -22,7 +22,7 @@ open Std Slice PRange Iterators variable {α : Type u} -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] def ListSlice.instToIterator := ToIterator.of (γ := Slice (Internal.ListSliceData α)) _ (fun s => match s.internalRepresentation.stop with | some n => s.internalRepresentation.list.iter.take n diff --git a/src/Init/Data/String/Lemmas/Pattern/Basic.lean b/src/Init/Data/String/Lemmas/Pattern/Basic.lean index 5842fc13f8..e1dda18d85 100644 --- a/src/Init/Data/String/Lemmas/Pattern/Basic.lean +++ b/src/Init/Data/String/Lemmas/Pattern/Basic.lean @@ -296,7 +296,6 @@ 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 caa1f29527..96d2d135dc 100644 --- a/src/Init/Data/String/Lemmas/Pattern/Split.lean +++ b/src/Init/Data/String/Lemmas/Pattern/Split.lean @@ -197,7 +197,6 @@ 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/UInt/Basic.lean b/src/Init/Data/UInt/Basic.lean index d78c8d183b..8845b1db4f 100644 --- a/src/Init/Data/UInt/Basic.lean +++ b/src/Init/Data/UInt/Basic.lean @@ -372,7 +372,7 @@ Examples: * `(if (5 : UInt16) < 5 then "yes" else "no") = "no"` * `show ¬((7 : UInt16) < 7) by decide` -/ -@[extern "lean_uint16_dec_lt", instance_reducible] +@[extern "lean_uint16_dec_lt", implicit_reducible] def UInt16.decLt (a b : UInt16) : Decidable (a < b) := inferInstanceAs (Decidable (a.toBitVec < b.toBitVec)) @@ -389,7 +389,7 @@ Examples: * `(if (5 : UInt16) ≤ 15 then "yes" else "no") = "yes"` * `show (7 : UInt16) ≤ 7 by decide` -/ -@[extern "lean_uint16_dec_le", instance_reducible] +@[extern "lean_uint16_dec_le", implicit_reducible] def UInt16.decLe (a b : UInt16) : Decidable (a ≤ b) := inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec)) @@ -736,7 +736,7 @@ Examples: * `(if (5 : UInt64) < 5 then "yes" else "no") = "no"` * `show ¬((7 : UInt64) < 7) by decide` -/ -@[extern "lean_uint64_dec_lt", instance_reducible] +@[extern "lean_uint64_dec_lt", implicit_reducible] def UInt64.decLt (a b : UInt64) : Decidable (a < b) := inferInstanceAs (Decidable (a.toBitVec < b.toBitVec)) @@ -752,7 +752,7 @@ Examples: * `(if (5 : UInt64) ≤ 15 then "yes" else "no") = "yes"` * `show (7 : UInt64) ≤ 7 by decide` -/ -@[extern "lean_uint64_dec_le", instance_reducible] +@[extern "lean_uint64_dec_le", implicit_reducible] def UInt64.decLe (a b : UInt64) : Decidable (a ≤ b) := inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec)) diff --git a/src/Init/Data/UInt/BasicAux.lean b/src/Init/Data/UInt/BasicAux.lean index 4dd3d314ce..35b68a6834 100644 --- a/src/Init/Data/UInt/BasicAux.lean +++ b/src/Init/Data/UInt/BasicAux.lean @@ -399,7 +399,7 @@ Examples: * `(if (5 : USize) < 5 then "yes" else "no") = "no"` * `show ¬((7 : USize) < 7) by decide` -/ -@[extern "lean_usize_dec_lt", instance_reducible] +@[extern "lean_usize_dec_lt", implicit_reducible] def USize.decLt (a b : USize) : Decidable (a < b) := inferInstanceAs (Decidable (a.toBitVec < b.toBitVec)) @@ -415,7 +415,7 @@ Examples: * `(if (5 : USize) ≤ 15 then "yes" else "no") = "yes"` * `show (7 : USize) ≤ 7 by decide` -/ -@[extern "lean_usize_dec_le", instance_reducible] +@[extern "lean_usize_dec_le", implicit_reducible] def USize.decLe (a b : USize) : Decidable (a ≤ b) := inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec)) diff --git a/src/Init/Data/Vector/Algebra.lean b/src/Init/Data/Vector/Algebra.lean index db098b3660..f92a21df4a 100644 --- a/src/Init/Data/Vector/Algebra.lean +++ b/src/Init/Data/Vector/Algebra.lean @@ -75,7 +75,7 @@ def mul [Mul α] (xs ys : Vector α n) : Vector α n := Pointwise multiplication of vectors. This is not a global instance as in some applications different multiplications may be relevant. -/ -@[instance_reducible] +@[implicit_reducible] def instMul [Mul α] : Mul (Vector α n) := ⟨mul⟩ section mul diff --git a/src/Init/Data/Vector/Extract.lean b/src/Init/Data/Vector/Extract.lean index 8d30dd1daf..c912d676ea 100644 --- a/src/Init/Data/Vector/Extract.lean +++ b/src/Init/Data/Vector/Extract.lean @@ -132,7 +132,6 @@ 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 @@ -179,7 +178,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]; rfl + simp [Array.set_eq_push_extract_append_extract] 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/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index e1ef20991a..984d66c1a2 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; rfl + simp @[simp] theorem getElem?_toList {xs : Vector α n} {i : Nat} : xs.toList[i]? = xs[i]? := by diff --git a/src/Init/Data/Vector/OfFn.lean b/src/Init/Data/Vector/OfFn.lean index c910271fce..33402360ad 100644 --- a/src/Init/Data/Vector/OfFn.lean +++ b/src/Init/Data/Vector/OfFn.lean @@ -119,7 +119,6 @@ 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/Module/Basic.lean b/src/Init/Grind/Module/Basic.lean index a5ec5c5911..4d05a07a20 100644 --- a/src/Init/Grind/Module/Basic.lean +++ b/src/Init/Grind/Module/Basic.lean @@ -60,7 +60,7 @@ class NatModule (M : Type u) extends AddCommMonoid M where /-- Scalar multiplication by a successor. -/ add_one_nsmul : ∀ n : Nat, ∀ a : M, (n + 1) • a = n • a + a -attribute [instance_reducible] NatModule.nsmul +attribute [implicit_reducible] NatModule.nsmul attribute [instance 100] NatModule.toAddCommMonoid NatModule.nsmul /-- @@ -83,7 +83,7 @@ class IntModule (M : Type u) extends AddCommGroup M where /-- Scalar multiplication by natural numbers is consistent with scalar multiplication by integers. -/ zsmul_natCast_eq_nsmul : ∀ n : Nat, ∀ a : M, (n : Int) • a = n • a -attribute [instance_reducible] IntModule.zsmul +attribute [implicit_reducible] IntModule.zsmul attribute [instance 100] IntModule.toAddCommGroup IntModule.zsmul namespace IntModule diff --git a/src/Init/Grind/Module/Envelope.lean b/src/Init/Grind/Module/Envelope.lean index d0b4345d9c..1c88171701 100644 --- a/src/Init/Grind/Module/Envelope.lean +++ b/src/Init/Grind/Module/Envelope.lean @@ -204,7 +204,7 @@ theorem zsmul_natCast_eq_nsmul (n : Nat) (a : Q α) : zsmul (n : Int) a = nsmul induction a using Q.ind with | _ a rcases a with ⟨a₁, a₂⟩; simp; omega -@[instance_reducible] +@[implicit_reducible] def ofNatModule : IntModule (Q α) := { nsmul := ⟨nsmul⟩, zsmul := ⟨zsmul⟩, diff --git a/src/Init/Grind/Ring/Basic.lean b/src/Init/Grind/Ring/Basic.lean index 2032f112d5..8e3688c40c 100644 --- a/src/Init/Grind/Ring/Basic.lean +++ b/src/Init/Grind/Ring/Basic.lean @@ -94,7 +94,7 @@ class Semiring (α : Type u) extends Add α, Mul α where -/ nsmul_eq_natCast_mul : ∀ n : Nat, ∀ a : α, n • a = Nat.cast n * a := by intros; rfl -attribute [instance_reducible] Semiring.npow Semiring.ofNat Semiring.natCast +attribute [implicit_reducible] Semiring.npow Semiring.ofNat Semiring.natCast /-- A ring, i.e. a type equipped with addition, negation, multiplication, and a map from the integers, @@ -120,7 +120,7 @@ class Ring (α : Type u) extends Semiring α, Neg α, Sub α where /-- The canonical map from the integers is consistent with negation. -/ intCast_neg : ∀ i : Int, Int.cast (R := α) (-i) = -Int.cast i := by intros; rfl -attribute [instance_reducible] Ring.intCast Ring.zsmul +attribute [implicit_reducible] Ring.intCast Ring.zsmul /-- A commutative semiring, i.e. a semiring with commutative multiplication. @@ -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]; rfl + | zero => simp [Nat.mul_zero, mul_zero] | 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/Grind/Ring/Envelope.lean b/src/Init/Grind/Ring/Envelope.lean index 6dd4ebb40b..b93b17551c 100644 --- a/src/Init/Grind/Ring/Envelope.lean +++ b/src/Init/Grind/Ring/Envelope.lean @@ -245,7 +245,7 @@ theorem neg_zsmul (i : Int) (a : Q α) : zsmul (-i) a = neg (zsmul i a) := by · have : i = 0 := by omega simp [this] -@[instance_reducible] +@[implicit_reducible] def ofSemiring : Ring (Q α) := { nsmul := ⟨nsmul⟩ zsmul := ⟨zsmul⟩ @@ -506,7 +506,7 @@ theorem mul_comm (a b : OfSemiring.Q α) : OfSemiring.mul a b = OfSemiring.mul b obtain ⟨⟨b₁, b₂⟩⟩ := b apply Quot.sound; refine ⟨0, ?_⟩; simp; ac_rfl -@[instance_reducible] +@[implicit_reducible] def ofCommSemiring : CommRing (OfSemiring.Q α) := { OfSemiring.ofSemiring with mul_comm := mul_comm } diff --git a/src/Init/Grind/Ring/Field.lean b/src/Init/Grind/Ring/Field.lean index b9165295e3..63d58c7f57 100644 --- a/src/Init/Grind/Ring/Field.lean +++ b/src/Init/Grind/Ring/Field.lean @@ -38,7 +38,7 @@ class Field (α : Type u) extends CommRing α, Inv α, Div α where /-- Raising to a negative power is the inverse of raising to the positive power. -/ zpow_neg : ∀ (a : α) (n : Int), a ^ (-n) = (a ^ n)⁻¹ -attribute [instance_reducible] Field.zpow +attribute [implicit_reducible] Field.zpow attribute [instance 100] Field.toInv Field.toDiv Field.zpow namespace Field diff --git a/src/Init/GrindInstances/Ring/SInt.lean b/src/Init/GrindInstances/Ring/SInt.lean index 89c3e90508..3c3705fbe9 100644 --- a/src/Init/GrindInstances/Ring/SInt.lean +++ b/src/Init/GrindInstances/Ring/SInt.lean @@ -20,11 +20,11 @@ public section namespace Lean.Grind -@[expose, instance_reducible] +@[expose, implicit_reducible] def Int8.natCast : NatCast Int8 where natCast x := Int8.ofNat x -@[expose, instance_reducible] +@[expose, implicit_reducible] def Int8.intCast : IntCast Int8 where intCast x := Int8.ofInt x @@ -75,11 +75,11 @@ example : ToInt.Sub Int8 (.sint 8) := inferInstance instance : ToInt.Pow Int8 (.sint 8) := ToInt.pow_of_semiring (by simp) -@[expose, instance_reducible] +@[expose, implicit_reducible] def Int16.natCast : NatCast Int16 where natCast x := Int16.ofNat x -@[expose, instance_reducible] +@[expose, implicit_reducible] def Int16.intCast : IntCast Int16 where intCast x := Int16.ofInt x @@ -130,11 +130,11 @@ example : ToInt.Sub Int16 (.sint 16) := inferInstance instance : ToInt.Pow Int16 (.sint 16) := ToInt.pow_of_semiring (by simp) -@[expose, instance_reducible] +@[expose, implicit_reducible] def Int32.natCast : NatCast Int32 where natCast x := Int32.ofNat x -@[expose, instance_reducible] +@[expose, implicit_reducible] def Int32.intCast : IntCast Int32 where intCast x := Int32.ofInt x @@ -185,11 +185,11 @@ example : ToInt.Sub Int32 (.sint 32) := inferInstance instance : ToInt.Pow Int32 (.sint 32) := ToInt.pow_of_semiring (by simp) -@[expose, instance_reducible] +@[expose, implicit_reducible] def Int64.natCast : NatCast Int64 where natCast x := Int64.ofNat x -@[expose, instance_reducible] +@[expose, implicit_reducible] def Int64.intCast : IntCast Int64 where intCast x := Int64.ofInt x @@ -240,11 +240,11 @@ example : ToInt.Sub Int64 (.sint 64) := inferInstance instance : ToInt.Pow Int64 (.sint 64) := ToInt.pow_of_semiring (by simp) -@[expose, instance_reducible] +@[expose, implicit_reducible] def ISize.natCast : NatCast ISize where natCast x := ISize.ofNat x -@[expose, instance_reducible] +@[expose, implicit_reducible] def ISize.intCast : IntCast ISize where intCast x := ISize.ofInt x diff --git a/src/Init/GrindInstances/Ring/UInt.lean b/src/Init/GrindInstances/Ring/UInt.lean index 5b83956f8e..e22334045a 100644 --- a/src/Init/GrindInstances/Ring/UInt.lean +++ b/src/Init/GrindInstances/Ring/UInt.lean @@ -20,11 +20,11 @@ namespace UInt8 /-- Variant of `UInt8.ofNat_mod_size` replacing `2 ^ 8` with `256`.-/ theorem ofNat_mod_size' : ofNat (x % 256) = ofNat x := ofNat_mod_size -@[expose, instance_reducible] +@[expose, implicit_reducible] def natCast : NatCast UInt8 where natCast x := UInt8.ofNat x -@[expose, instance_reducible] +@[expose, implicit_reducible] def intCast : IntCast UInt8 where intCast x := UInt8.ofInt x @@ -51,11 +51,11 @@ namespace UInt16 /-- Variant of `UInt16.ofNat_mod_size` replacing `2 ^ 16` with `65536`.-/ theorem ofNat_mod_size' : ofNat (x % 65536) = ofNat x := ofNat_mod_size -@[expose, instance_reducible] +@[expose, implicit_reducible] def natCast : NatCast UInt16 where natCast x := UInt16.ofNat x -@[expose, instance_reducible] +@[expose, implicit_reducible] def intCast : IntCast UInt16 where intCast x := UInt16.ofInt x @@ -82,11 +82,11 @@ namespace UInt32 /-- Variant of `UInt32.ofNat_mod_size` replacing `2 ^ 32` with `4294967296`.-/ theorem ofNat_mod_size' : ofNat (x % 4294967296) = ofNat x := ofNat_mod_size -@[expose, instance_reducible] +@[expose, implicit_reducible] def natCast : NatCast UInt32 where natCast x := UInt32.ofNat x -@[expose, instance_reducible] +@[expose, implicit_reducible] def intCast : IntCast UInt32 where intCast x := UInt32.ofInt x @@ -113,11 +113,11 @@ namespace UInt64 /-- Variant of `UInt64.ofNat_mod_size` replacing `2 ^ 64` with `18446744073709551616`.-/ theorem ofNat_mod_size' : ofNat (x % 18446744073709551616) = ofNat x := ofNat_mod_size -@[expose, instance_reducible] +@[expose, implicit_reducible] def natCast : NatCast UInt64 where natCast x := UInt64.ofNat x -@[expose, instance_reducible] +@[expose, implicit_reducible] def intCast : IntCast UInt64 where intCast x := UInt64.ofInt x @@ -141,11 +141,11 @@ end UInt64 namespace USize -@[expose, instance_reducible] +@[expose, implicit_reducible] def natCast : NatCast USize where natCast x := USize.ofNat x -@[expose, instance_reducible] +@[expose, implicit_reducible] def intCast : IntCast USize where intCast x := USize.ofInt x diff --git a/src/Init/Hints.lean b/src/Init/Hints.lean index 2ee004e781..a6d63e81e6 100644 --- a/src/Init/Hints.lean +++ b/src/Init/Hints.lean @@ -14,11 +14,3 @@ public section unif_hint (p : Prop) where ⊢ Not p =?= p → False -unif_hint (n : Nat) where - ⊢ n - 0 =?= n - -unif_hint (n : Nat) where - ⊢ n + 0 =?= n - -unif_hint (n : Nat) where - ⊢ n * 0 =?= 0 diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index acc1fc9d75..a64b888b55 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -1726,7 +1726,7 @@ Addition of natural numbers, typically used via the `+` operator. This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model. -/ -@[extern "lean_nat_add"] +@[extern "lean_nat_add", implicit_reducible] protected def Nat.add : (@& Nat) → (@& Nat) → Nat | a, Nat.zero => a | a, Nat.succ b => Nat.succ (Nat.add a b) @@ -1745,7 +1745,7 @@ Multiplication of natural numbers, usually accessed via the `*` operator. This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model. -/ -@[extern "lean_nat_mul"] +@[extern "lean_nat_mul", implicit_reducible] protected def Nat.mul : (@& Nat) → (@& Nat) → Nat | _, 0 => 0 | a, Nat.succ b => Nat.add (Nat.mul a b) a @@ -2076,7 +2076,7 @@ Examples: * `8 - 8 = 0` * `8 - 20 = 0` -/ -@[extern "lean_nat_sub"] +@[extern "lean_nat_sub", implicit_reducible] protected def Nat.sub : (@& Nat) → (@& Nat) → Nat | a, 0 => a | a, succ b => pred (Nat.sub a b) @@ -2478,7 +2478,7 @@ Examples: * `(if (5 : UInt8) < 5 then "yes" else "no") = "no"` * `show ¬((7 : UInt8) < 7) by decide` -/ -@[extern "lean_uint8_dec_lt", instance_reducible] +@[extern "lean_uint8_dec_lt", implicit_reducible] def UInt8.decLt (a b : UInt8) : Decidable (LT.lt a b) := inferInstanceAs (Decidable (LT.lt a.toBitVec b.toBitVec)) @@ -2494,7 +2494,7 @@ Examples: * `(if (5 : UInt8) ≤ 15 then "yes" else "no") = "yes"` * `show (7 : UInt8) ≤ 7 by decide` -/ -@[extern "lean_uint8_dec_le", instance_reducible] +@[extern "lean_uint8_dec_le", implicit_reducible] def UInt8.decLe (a b : UInt8) : Decidable (LE.le a b) := inferInstanceAs (Decidable (LE.le a.toBitVec b.toBitVec)) @@ -2638,7 +2638,7 @@ Examples: * `(if (5 : UInt32) < 5 then "yes" else "no") = "no"` * `show ¬((7 : UInt32) < 7) by decide` -/ -@[extern "lean_uint32_dec_lt", instance_reducible] +@[extern "lean_uint32_dec_lt", implicit_reducible] def UInt32.decLt (a b : UInt32) : Decidable (LT.lt a b) := inferInstanceAs (Decidable (LT.lt a.toBitVec b.toBitVec)) @@ -2654,7 +2654,7 @@ Examples: * `(if (5 : UInt32) ≤ 15 then "yes" else "no") = "yes"` * `show (7 : UInt32) ≤ 7 by decide` -/ -@[extern "lean_uint32_dec_le", instance_reducible] +@[extern "lean_uint32_dec_le", implicit_reducible] def UInt32.decLe (a b : UInt32) : Decidable (LE.le a b) := inferInstanceAs (Decidable (LE.le a.toBitVec b.toBitVec)) @@ -3208,7 +3208,7 @@ This is a cached value, so it is `O(1)` to access. The space allocated for an ar its _capacity_, is at least as large as its size, but may be larger. The capacity of an array is an internal detail that's not observable by Lean code. -/ -@[extern "lean_array_get_size", tagged_return] +@[extern "lean_array_get_size", tagged_return, implicit_reducible] def Array.size {α : Type u} (a : @& Array α) : Nat := a.toList.length diff --git a/src/Init/WF.lean b/src/Init/WF.lean index 1eb80f8a1c..6225c703fe 100644 --- a/src/Init/WF.lean +++ b/src/Init/WF.lean @@ -144,7 +144,7 @@ end WellFounded open WellFounded -- Empty relation is well-founded -@[instance_reducible] +@[implicit_reducible] def emptyWf {α : Sort u} : WellFoundedRelation α where rel := emptyRelation wf := by @@ -218,7 +218,7 @@ theorem WellFounded.transGen (h : WellFounded r) : WellFounded (TransGen r) := namespace Nat -- less-than is well-founded -@[instance_reducible] +@[implicit_reducible] def lt_wfRel : WellFoundedRelation Nat where rel := (· < ·) wf := by @@ -363,7 +363,7 @@ theorem RProdSubLex (a : α × β) (b : α × β) (h : RProd ra rb a b) : Prod.L | intro h₁ h₂ => exact Prod.Lex.left _ _ h₁ -- The relational product of well founded relations is well-founded -@[instance_reducible] +@[implicit_reducible] def rprod (ha : WellFoundedRelation α) (hb : WellFoundedRelation β) : WellFoundedRelation (α × β) where rel := RProd ha.rel hb.rel wf := by @@ -456,7 +456,7 @@ section def SkipLeft (α : Type u) {β : Type v} (s : β → β → Prop) : @PSigma α (fun _ => β) → @PSigma α (fun _ => β) → Prop := RevLex emptyRelation s -@[instance_reducible] +@[implicit_reducible] def skipLeft (α : Type u) {β : Type v} (hb : WellFoundedRelation β) : WellFoundedRelation (PSigma fun _ : α => β) where rel := SkipLeft α hb.rel wf := revLex emptyWf.wf hb.wf diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index 9a32311c42..3343566186 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -64,7 +64,7 @@ to `.instances`; other implicit arguments stay at the caller's transparency. This option only has an effect when `backward.isDefEq.respectTransparency` is `true`. -/ register_builtin_option backward.isDefEq.implicitBump : Bool := { - defValue := false + defValue := true descr := "if true, bump transparency to `.instances` for all implicit arguments, \ not just instance-implicit ones" } diff --git a/src/Std/Data/DHashMap/IteratorLemmas.lean b/src/Std/Data/DHashMap/IteratorLemmas.lean index 0d542c027b..890b6d6122 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]; rfl + simp [Iter.step_eq, iter] @[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]; rfl + simp [Iter.step_eq, iter] @[simp] public theorem toList_iter {α : Type u} {β : α → Type v} {l : AssocList α β} : diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean index 61cd82b36f..77eb65ed83 100644 --- a/src/Std/Data/DHashMap/Lemmas.lean +++ b/src/Std/Data/DHashMap/Lemmas.lean @@ -4549,7 +4549,7 @@ end Const end Equiv /-- Internal implementation detail of the hash map. -/ -@[instance_reducible] +@[implicit_reducible] def isSetoid (α β) [BEq α] [Hashable α] : Setoid (DHashMap α β) where r := Equiv iseqv := { diff --git a/src/Std/Data/DTreeMap/Internal/Zipper.lean b/src/Std/Data/DTreeMap/Internal/Zipper.lean index 24140d72ca..ba71ef4cc5 100644 --- a/src/Std/Data/DTreeMap/Internal/Zipper.lean +++ b/src/Std/Data/DTreeMap/Internal/Zipper.lean @@ -373,7 +373,7 @@ public def Zipper.iter (t : Zipper α β) : Iter (α := Zipper α β) ((a : α) public def Zipper.iterOfTree (t : Impl α β) : Iter (α := Zipper α β) ((a : α) × β a) := Zipper.iter <| Zipper.done.prependMap t -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def Zipper.instToIterator := ToIterator.of (γ := Zipper α β) _ (fun z => z.iter) attribute [instance] Zipper.instToIterator @@ -688,7 +688,7 @@ public abbrev RicSlice α β [Ord α] := Slice (RicSliceData α β) public instance {α : Type u} {β : α → Type v} [Ord α] : Ric.Sliceable (Impl α β) α (RicSlice α β) where mkSlice carrier range := ⟨carrier, range⟩ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def RicSlice.instToIterator {β : α → Type v} [Ord α] := ToIterator.of (γ := Slice (Internal.RicSliceData α β)) (β := ((a : α) × β a)) _ (fun s => ⟨RxcIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩) @@ -718,7 +718,7 @@ public abbrev RicSlice α [Ord α] := Slice (RicSliceData α) public instance {α : Type u} [Ord α] : Ric.Sliceable (Impl α (fun _ => Unit)) α (Unit.RicSlice α) where mkSlice carrier range := ⟨carrier, range⟩ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def RicSlice.instToIterator [Ord α] := ToIterator.of (γ := Slice (RicSliceData α)) (β := α) _ fun s => (⟨RxcIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1) @@ -753,7 +753,7 @@ public abbrev RicSlice α β [Ord α] := Slice (RicSliceData α β) public instance {α : Type u} {β : Type v} [Ord α] : Ric.Sliceable (Impl α (fun _ => β)) α (RicSlice α β) where mkSlice carrier range := ⟨carrier, range⟩ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def RicSlice.instToIterator {β : Type v} [Ord α] := ToIterator.of (γ := Slice (RicSliceData α β)) _ fun s => (⟨RxcIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2) @@ -788,7 +788,7 @@ public abbrev RioSlice α β [Ord α] := Slice (RioSliceData α β) public instance {α : Type u} {β : α → Type v} [Ord α] : Rio.Sliceable (Impl α β) α (RioSlice α β) where mkSlice carrier range := ⟨carrier, range⟩ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def RioSlice.instToIterator {β : α → Type v} [Ord α] := ToIterator.of (γ := Slice (RioSliceData α β)) (β := (a : α) × β a) _ fun s => ⟨RxoIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩ @@ -819,7 +819,7 @@ public abbrev RioSlice α [Ord α] := Slice (RioSliceData α) public instance {α : Type u} [Ord α] : Rio.Sliceable (Impl α (fun _ => Unit)) α (Unit.RioSlice α) where mkSlice carrier range := ⟨carrier, range⟩ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def RioSlice.instToIterator [Ord α] := ToIterator.of (γ := Slice (RioSliceData α)) _ fun s => (⟨RxoIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1) @@ -854,7 +854,7 @@ public abbrev RioSlice α β [Ord α] := Slice (RioSliceData α β) public instance {α : Type u} {β : Type v} [Ord α] : Rio.Sliceable (Impl α (fun _ => β)) α (RioSlice α β) where mkSlice carrier range := ⟨carrier, range⟩ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def RioSlice.instToIterator {β : Type v} [Ord α] := ToIterator.of (γ := Slice (RioSliceData α β)) _ fun s => (⟨RxoIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2) @@ -922,7 +922,7 @@ public abbrev RccSlice α β [Ord α] := Slice (RccSliceData α β) public instance {α : Type u} {β : α → Type v} [Ord α] : Rcc.Sliceable (Impl α β) α (RccSlice α β) where mkSlice carrier range := ⟨carrier, range⟩ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def RccSlice.instToIterator {β : α → Type v} [Ord α] := ToIterator.of (γ := Slice (RccSliceData α β)) (β := (a : α) × β a) _ fun s => (rccIterator s.1.treeMap s.1.range.lower s.1.range.upper) @@ -950,7 +950,7 @@ public abbrev RccSlice α [Ord α] := Slice (RccSliceData α) public instance {α : Type u} [Ord α] : Rcc.Sliceable (Impl α (fun _ => Unit)) α (Unit.RccSlice α) where mkSlice carrier range := ⟨carrier, range⟩ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def RccSlice.instToIterator [Ord α] := ToIterator.of (γ := Slice (RccSliceData α)) _ fun s => (⟨RxcIterator.mk (Zipper.prependMapGE s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1) @@ -987,7 +987,7 @@ public abbrev RccSlice α β [Ord α] := Slice (RccSliceData α β) public instance {α : Type u} {β : Type v} [Ord α] : Rcc.Sliceable (Impl α (fun _ => β)) α (RccSlice α β) where mkSlice carrier range := ⟨carrier, range⟩ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def RccSlice.instToIterator {β : Type v} [Ord α] := ToIterator.of (γ := Slice (RccSliceData α β)) _ fun s => (⟨RxcIterator.mk (Zipper.prependMapGE s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2) @@ -1059,7 +1059,7 @@ public abbrev RcoSlice α β [Ord α] := Slice (RcoSliceData α β) public instance {α : Type u} {β : α → Type v} [Ord α] : Rco.Sliceable (Impl α β) α (RcoSlice α β) where mkSlice carrier range := ⟨carrier, range⟩ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def RcoSlice.instToIterator {β : α → Type v} [Ord α] := ToIterator.of (γ := Slice (RcoSliceData α β)) (β := (a : α) × β a) _ fun s => rcoIterator s.1.treeMap s.1.range.lower s.1.range.upper @@ -1087,7 +1087,7 @@ public abbrev RcoSlice α [Ord α] := Slice (RcoSliceData α) public instance {α : Type u} [Ord α] : Rco.Sliceable (Impl α (fun _ => Unit)) α (Unit.RcoSlice α) where mkSlice carrier range := ⟨carrier, range⟩ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def RcoSlice.instToIterator [Ord α] := ToIterator.of (γ := Slice (RcoSliceData α)) _ fun s => (⟨RxoIterator.mk (Zipper.prependMapGE s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1) @@ -1124,7 +1124,7 @@ public abbrev RcoSlice α β [Ord α] := Slice (RcoSliceData α β) public instance {α : Type u} {β : Type v} [Ord α] : Rco.Sliceable (Impl α (fun _ => β)) α (RcoSlice α β) where mkSlice carrier range := ⟨carrier, range⟩ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def RcoSlice.instToIterator {β : Type v} [Ord α] := ToIterator.of (γ := Slice (RcoSliceData α β)) _ fun s => (⟨RxoIterator.mk (Zipper.prependMapGE s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2) @@ -1195,7 +1195,7 @@ public abbrev RooSlice α β [Ord α] := Slice (RooSliceData α β) public instance {α : Type u} {β : α → Type v} [Ord α] : Roo.Sliceable (Impl α β) α (RooSlice α β) where mkSlice carrier range := ⟨carrier, range⟩ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def RooSlice.instToIterator {β : α → Type v} [Ord α] := ToIterator.of (γ := Slice (RooSliceData α β)) (β := (a : α) × β a) _ fun s => rooIterator s.1.treeMap s.1.range.lower s.1.range.upper @@ -1223,7 +1223,7 @@ public abbrev RooSlice α [Ord α] := Slice (RooSliceData α) public instance {α : Type u} [Ord α] : Roo.Sliceable (Impl α (fun _ => Unit)) α (Unit.RooSlice α) where mkSlice carrier range := ⟨carrier, range⟩ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def RooSlice.instToIterator [Ord α] := ToIterator.of (γ := Slice (RooSliceData α)) _ fun s => (⟨RxoIterator.mk (Zipper.prependMapGT s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1) @@ -1260,7 +1260,7 @@ public abbrev RooSlice α β [Ord α] := Slice (RooSliceData α β) public instance {α : Type u} {β : Type v} [Ord α] : Roo.Sliceable (Impl α (fun _ => β)) α (RooSlice α β) where mkSlice carrier range := ⟨carrier, range⟩ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def RooSlice.instToIterator {β : Type v} [Ord α] := ToIterator.of (γ := Slice (RooSliceData α β)) _ fun s => (⟨RxoIterator.mk (Zipper.prependMapGT s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2) @@ -1332,7 +1332,7 @@ public abbrev RocSlice α β [Ord α] := Slice (RocSliceData α β) public instance {α : Type u} {β : α → Type v} [Ord α] : Roc.Sliceable (Impl α β) α (RocSlice α β) where mkSlice carrier range := ⟨carrier, range⟩ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def RocSlice.instToIterator {β : α → Type v} [Ord α] := ToIterator.of (γ := Slice (RocSliceData α β)) (β := (a : α) × β a) _ fun s => rocIterator s.1.treeMap s.1.range.lower s.1.range.upper @@ -1360,7 +1360,7 @@ public abbrev RocSlice α [Ord α] := Slice (RocSliceData α) public instance {α : Type u} [Ord α] : Roc.Sliceable (Impl α (fun _ => Unit)) α (Unit.RocSlice α) where mkSlice carrier range := ⟨carrier, range⟩ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def RocSlice.instToIterator [Ord α] := ToIterator.of (γ := Slice (RocSliceData α)) _ fun s => (⟨RxcIterator.mk (Zipper.prependMapGT s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1) @@ -1397,7 +1397,7 @@ public abbrev RocSlice α β [Ord α] := Slice (RocSliceData α β) public instance {α : Type u} {β : Type v} [Ord α] : Roc.Sliceable (Impl α (fun _ => β)) α (RocSlice α β) where mkSlice carrier range := ⟨carrier, range⟩ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def RocSlice.instToIterator {β : Type v} [Ord α] := ToIterator.of (γ := Slice (RocSliceData α β)) _ fun s => (⟨RxcIterator.mk (Zipper.prependMapGT s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2) @@ -1454,7 +1454,7 @@ public abbrev RciSlice α β [Ord α] := Slice (RciSliceData α β) public instance {α : Type u} {β : α → Type v} [Ord α] : Rci.Sliceable (Impl α β) α (RciSlice α β) where mkSlice carrier range := ⟨carrier, range⟩ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def RciSlice.instToIterator {β : α → Type v} [Ord α] := ToIterator.of (γ := Slice (RciSliceData α β)) (β := (a : α) × β a) _ fun s => rciIterator s.1.treeMap s.1.range.lower @@ -1482,7 +1482,7 @@ public abbrev RciSlice α [Ord α] := Slice (RciSliceData α) public instance {α : Type u} [Ord α] : Rci.Sliceable (Impl α (fun _ => Unit)) α (Unit.RciSlice α) where mkSlice carrier range := ⟨carrier, range⟩ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def RciSlice.instToIterator [Ord α] := ToIterator.of (γ := Slice (RciSliceData α)) _ fun s => (⟨Zipper.prependMapGE s.1.treeMap s.1.range.lower Zipper.done⟩ : Iter _ ).map fun e => (e.1) @@ -1522,7 +1522,7 @@ public abbrev RciSlice α β [Ord α] := Slice (RciSliceData α β) public instance {α : Type u} {β : Type v} [Ord α] : Rci.Sliceable (Impl α (fun _ => β)) α (RciSlice α β) where mkSlice carrier range := ⟨carrier, range⟩ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def RciSlice.instToIterator {β : Type v} [Ord α] := ToIterator.of (γ := Slice (RciSliceData α β)) _ fun s => (⟨(Zipper.prependMapGE s.1.treeMap s.1.range.lower Zipper.done)⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2) @@ -1580,7 +1580,7 @@ public abbrev RoiSlice α β [Ord α] := Slice (RoiSliceData α β) public instance {α : Type u} {β : α → Type v} [Ord α] : Roi.Sliceable (Impl α β) α (RoiSlice α β) where mkSlice carrier range := ⟨carrier, range⟩ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def RoiSlice.instToIterator {β : α → Type v} [Ord α] := ToIterator.of (γ := Slice (RoiSliceData α β)) (β := (a : α) × β a) _ fun s => roiIterator s.1.treeMap s.1.range.lower @@ -1608,7 +1608,7 @@ public abbrev RoiSlice α [Ord α] := Slice (RoiSliceData α) public instance {α : Type u} [Ord α] : Roi.Sliceable (Impl α (fun _ => Unit)) α (Unit.RoiSlice α) where mkSlice carrier range := ⟨carrier, range⟩ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def RoiSlice.instToIterator [Ord α] := ToIterator.of (γ := Slice (RoiSliceData α)) _ fun s => (⟨Zipper.prependMapGT s.1.treeMap s.1.range.lower Zipper.done⟩ : Iter _ ).map fun e => (e.1) @@ -1648,7 +1648,7 @@ public abbrev RoiSlice α β [Ord α] := Slice (RoiSliceData α β) public instance {α : Type u} {β : Type v} [Ord α] : Roi.Sliceable (Impl α (fun _ => β)) α (RoiSlice α β) where mkSlice carrier range := ⟨carrier, range⟩ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def RoiSlice.instToIterator {β : Type v} [Ord α] := ToIterator.of (γ := Slice (RoiSliceData α β)) _ fun s => (⟨(Zipper.prependMapGT s.1.treeMap s.1.range.lower .done)⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2) @@ -1700,7 +1700,7 @@ public abbrev RiiSlice α β := Slice (RiiSliceData α β) public instance {α : Type u} {β : α → Type v} : Rii.Sliceable (Impl α β) α (RiiSlice α β) where mkSlice carrier range := ⟨carrier, range⟩ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def RiiSlice.instToIterator {β : α → Type v} := ToIterator.of (γ := Slice (RiiSliceData α β)) (β := (a : α) × β a) _ fun s => riiIterator s.1.treeMap @@ -1726,7 +1726,7 @@ public abbrev RiiSlice α := Slice (RiiSliceData α) public instance {α : Type u} : Rii.Sliceable (Impl α (fun _ => Unit)) α (Unit.RiiSlice α) where mkSlice carrier range := ⟨carrier, range⟩ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def RiiSlice.instToIterator {α : Type u} := ToIterator.of (γ := Slice (RiiSliceData α)) _ fun s => (⟨Zipper.prependMap s.internalRepresentation.treeMap .done⟩ : Iter _ ).map fun e => (e.1) @@ -1759,7 +1759,7 @@ public abbrev RiiSlice α β := Slice (RiiSliceData α β) public instance {α : Type u} {β : Type v} : Rii.Sliceable (Impl α (fun _ => β)) α (Const.RiiSlice α β) where mkSlice carrier range := ⟨carrier, range⟩ -@[inline, expose, instance_reducible] +@[inline, expose, implicit_reducible] public def RiiSlice.instToIterator {α : Type u} {β : Type v} := ToIterator.of (γ := Slice (RiiSliceData α β)) _ fun s => (⟨Zipper.prependMap s.internalRepresentation.treeMap .done⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2) diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean index 72010506fb..2a3b1e1a9e 100644 --- a/src/Std/Data/DTreeMap/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Lemmas.lean @@ -5882,7 +5882,7 @@ end Equiv section Equiv /-- Implementation detail of the tree map -/ -@[instance_reducible] +@[implicit_reducible] def isSetoid (α : Type u) (β : α → Type v) (cmp : α → α → Ordering := by exact compare) : Setoid (Std.DTreeMap α β cmp) where r := Equiv diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean index 976ffd1704..de64c028ea 100644 --- a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean +++ b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean @@ -53,7 +53,6 @@ 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 fc680c7179..95cfdf7f04 100644 --- a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean +++ b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean @@ -16,7 +16,6 @@ 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 5f85398c02..42240f827f 100644 --- a/src/Std/Data/Iterators/Lemmas/Producers/Repeat.lean +++ b/src/Std/Data/Iterators/Lemmas/Producers/Repeat.lean @@ -19,7 +19,6 @@ 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/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.lean index fb123f7aa3..9f2c0dfc1c 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,7 +52,6 @@ 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), @@ -73,7 +72,6 @@ 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/lake/Lake/Build/Data.lean b/src/lake/Lake/Build/Data.lean index d7a2c56677..5cdc72c1ae 100644 --- a/src/lake/Lake/Build/Data.lean +++ b/src/lake/Lake/Build/Data.lean @@ -51,7 +51,7 @@ public class OptDataKind (α : Type u) where namespace OptDataKind -@[instance_reducible, instance low] +@[implicit_reducible, instance low] public def anonymous : OptDataKind α where name := .anonymous wf h := by simp [Name.isAnonymous_iff_eq_anonymous] at h diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 79a0e58edd..7abc12c659 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -22,6 +22,8 @@ options get_default_options() { opts = opts.update({"quotPrecheck"}, true); opts = opts.update({"pp", "rawOnError"}, true); + // enable implicit argument transparency bump + opts = opts.update({"backward", "isDefEq", "implicitBump"}, true); #endif return opts; } diff --git a/tests/lean/ppMotives.lean.expected.out b/tests/lean/ppMotives.lean.expected.out index e6c4f0de25..06516682a1 100644 --- a/tests/lean/ppMotives.lean.expected.out +++ b/tests/lean/ppMotives.lean.expected.out @@ -1,4 +1,4 @@ -protected def Nat.add : Nat → Nat → Nat := +@[implicit_reducible] protected def Nat.add : Nat → Nat → Nat := fun x x_1 => Nat.brecOn x_1 (fun x f x_2 => @@ -7,7 +7,7 @@ fun x x_1 => | a, b.succ => fun x => (x.1 a).succ) f) x -protected def Nat.add : Nat → Nat → Nat := +@[implicit_reducible] protected def Nat.add : Nat → Nat → Nat := fun x x_1 => Nat.brecOn (motive := fun x => Nat → Nat) x_1 (fun x f x_2 => diff --git a/tests/lean/run/3807.lean b/tests/lean/run/3807.lean index ce26f3f233..3670e4cfac 100644 --- a/tests/lean/run/3807.lean +++ b/tests/lean/run/3807.lean @@ -1147,7 +1147,7 @@ variable [FunLike F α β] variable {_ : NonAssocSemiring α} {_ : NonAssocSemiring β} [RingHomClass F α β] -@[instance_reducible] +@[implicit_reducible] def RingHomClass.toRingHom (f : F) : α →+* β := { (f : α →* β), (f : α →+ β) with } @@ -1175,7 +1175,7 @@ end coe variable {_ : NonAssocSemiring α} {_ : NonAssocSemiring β} {_ : NonAssocSemiring γ} -@[instance_reducible] +@[implicit_reducible] def comp (g : β →+* γ) (f : α →+* β) : α →+* γ := { g.toNonUnitalRingHom.comp f.toNonUnitalRingHom with toFun := g ∘ f @@ -1194,41 +1194,41 @@ namespace Injective variable {M₁ : Type _} {M₂ : Type _} [Mul M₁] -@[instance_reducible] +@[implicit_reducible] protected def semigroup [Semigroup M₂] (f : M₁ → M₂) (hf : Injective f) : Semigroup M₁ := { ‹Mul M₁› with mul_assoc := sorry } -@[instance_reducible] +@[implicit_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] +@[implicit_reducible] protected def commMagma [CommMagma M₂] (f : M₁ → M₂) (hf : Injective f) : CommMagma M₁ where mul_comm x y := sorry -@[instance_reducible] +@[implicit_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] +@[implicit_reducible] protected def commSemigroup [CommSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) : CommSemigroup M₁ where toSemigroup := hf.semigroup f __ := hf.commMagma f -@[instance_reducible] +@[implicit_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] +@[implicit_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] +@[implicit_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, @@ -1236,21 +1236,21 @@ protected def addZeroClass {M₁} [Zero M₁] [Add M₁] [AddZeroClass M₂] (f variable [Pow M₁ Nat] -@[instance_reducible] +@[implicit_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] +@[implicit_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] +@[implicit_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 @@ -1259,19 +1259,19 @@ protected def addMonoidWithOne {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul Na natCast_succ := sorry, one := 1 } -@[instance_reducible] +@[implicit_reducible] protected def commMonoid [CommMonoid M₂] (f : M₁ → M₂) (hf : Injective f) : CommMonoid M₁ := { hf.monoid f, hf.commSemigroup f with } -@[instance_reducible] +@[implicit_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] +@[implicit_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, @@ -1280,7 +1280,7 @@ protected def divInvMonoid [DivInvMonoid M₂] (f : M₁ → M₂) (hf : Injecti zpow_neg' := sorry, div_eq_mul_inv := sorry } -@[instance_reducible] +@[implicit_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 @@ -1290,18 +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] +@[implicit_reducible] protected def group [Group M₂] (f : M₁ → M₂) (hf : Injective f) : Group M₁ := { hf.divInvMonoid f with mul_left_inv := sorry } -@[instance_reducible] +@[implicit_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] +@[implicit_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, @@ -1310,11 +1310,11 @@ protected def addGroupWithOne {M₁} [Zero M₁] [One M₁] [Add M₁] [SMul Nat intCast_ofNat := sorry, intCast_negSucc := sorry } -@[instance_reducible] +@[implicit_reducible] protected def commGroup [CommGroup M₂] (f : M₁ → M₂) (hf : Injective f) : CommGroup M₁ := { hf.commMonoid f, hf.group f with } -@[instance_reducible] +@[implicit_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 } @@ -1334,7 +1334,7 @@ section MulZeroClass variable [MulZeroClass M₀] {a b : M₀} -@[instance_reducible] +@[implicit_reducible] protected def Function.Injective.mulZeroClass [Mul M₀'] [Zero M₀'] (f : M₀' → M₀) (hf : Injective f) : MulZeroClass M₀' where mul := (· * ·) zero := 0 @@ -1347,7 +1347,7 @@ section MulZeroOneClass variable [MulZeroOneClass M₀] -@[instance_reducible] +@[implicit_reducible] protected def Function.Injective.mulZeroOneClass [Mul M₀'] [Zero M₀'] [One M₀'] (f : M₀' → M₀) (hf : Injective f) : MulZeroOneClass M₀' := @@ -1357,7 +1357,7 @@ end MulZeroOneClass section SemigroupWithZero -@[instance_reducible] +@[implicit_reducible] protected def Function.Injective.semigroupWithZero [Zero M₀'] [Mul M₀'] [SemigroupWithZero M₀] (f : M₀' → M₀) (hf : Injective f) : SemigroupWithZero M₀' := @@ -1367,7 +1367,7 @@ end SemigroupWithZero section MonoidWithZero -@[instance_reducible] +@[implicit_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₀' := @@ -1379,7 +1379,7 @@ section GroupWithZero variable [GroupWithZero G₀] {a b c g h x : G₀} -@[instance_reducible] +@[implicit_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, @@ -1399,7 +1399,7 @@ universe u v x variable {α : Type u} {β : Type v} {R : Type x} -@[instance_reducible] +@[implicit_reducible] protected def Function.Injective.distrib {S} [Mul R] [Add R] [Distrib S] (f : R → S) (hf : Injective f) : Distrib R where @@ -1409,33 +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] +@[implicit_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] +@[implicit_reducible] protected def Function.Injective.nonUnitalSemiring {α : Type u} [NonUnitalSemiring α] (f : β → α) (hf : Injective f) : NonUnitalSemiring β where toNonUnitalNonAssocSemiring := hf.nonUnitalNonAssocSemiring f __ := hf.semigroupWithZero f -@[instance_reducible] +@[implicit_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] +@[implicit_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] +@[implicit_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/boxing_bug.lean b/tests/lean/run/boxing_bug.lean index 9d8e25673d..08171a49f6 100644 --- a/tests/lean/run/boxing_bug.lean +++ b/tests/lean/run/boxing_bug.lean @@ -1,4 +1,4 @@ -@[instance_reducible] +@[implicit_reducible] def myCast : NatCast UInt8 where natCast := UInt8.ofNat diff --git a/tests/lean/run/diagnostics.lean b/tests/lean/run/diagnostics.lean index 82cf0e98a0..270867ca92 100644 --- a/tests/lean/run/diagnostics.lean +++ b/tests/lean/run/diagnostics.lean @@ -8,11 +8,10 @@ theorem f_eq : f (x + 1) = q (f x) := rfl /-- trace: [diag] Diagnostics - [reduction] unfolded declarations (max: 15, num: 4): + [reduction] unfolded declarations (max: 15, num: 3): [reduction] Nat.rec ↦ 15 [reduction] Add.add ↦ 10 [reduction] HAdd.hAdd ↦ 10 - [reduction] Nat.add ↦ 10 [reduction] unfolded reducible declarations (max: 15, num: 1): [reduction] Nat.casesOn ↦ 15 use `set_option diagnostics.threshold ` to control threshold for reporting counters @@ -25,11 +24,10 @@ example : f (x + 5) = q (q (q (q (q (f x))))) := /-- trace: [diag] Diagnostics - [reduction] unfolded declarations (max: 15, num: 4): + [reduction] unfolded declarations (max: 15, num: 3): [reduction] Nat.rec ↦ 15 [reduction] Add.add ↦ 10 [reduction] HAdd.hAdd ↦ 10 - [reduction] Nat.add ↦ 10 [reduction] unfolded reducible declarations (max: 15, num: 1): [reduction] Nat.casesOn ↦ 15 use `set_option diagnostics.threshold ` to control threshold for reporting counters diff --git a/tests/lean/run/grind_10160.lean b/tests/lean/run/grind_10160.lean index 763191e34f..4b1c55cc52 100644 --- a/tests/lean/run/grind_10160.lean +++ b/tests/lean/run/grind_10160.lean @@ -28,7 +28,7 @@ theorem MyInt.natCast_eq (n : Nat) : (n : MyInt) = formalDiff n 0 := rfl theorem MyInt.natCast_inj (n m : Nat) : (n : MyInt) = (m : MyInt) ↔ n = m := by - rw [natCast_eq, natCast_eq, eq] + rw [natCast_eq, natCast_eq, eq]; simp example (n m : Nat) : (n : MyInt) = (m : MyInt) ↔ n = m := by grind [MyInt.natCast_eq, MyInt.eq] diff --git a/tests/lean/run/grind_bitvec2.lean b/tests/lean/run/grind_bitvec2.lean index 0bbe4f6007..1c07550e6c 100644 --- a/tests/lean/run/grind_bitvec2.lean +++ b/tests/lean/run/grind_bitvec2.lean @@ -2001,8 +2001,7 @@ theorem toInt_append {x : BitVec n} {y : BitVec m} : · subst n0 simp [BitVec.eq_nil x, BitVec.toInt] · by_cases m0 : m = 0 - · subst m0 - simp [BitVec.eq_nil y, n0] + · subst m0; rw [BitVec.eq_nil y, append_zero_width]; simp [n0] · simp only [n0, ↓reduceIte] by_cases x.msb case pos h => @@ -3961,7 +3960,7 @@ theorem replicate_zero {x : BitVec w} : x.replicate 0 = 0#0 := by grind theorem replicate_one {w : Nat} {x : BitVec w} : (x.replicate 1) = x.cast (by rw [Nat.mul_one]) := by - simp [replicate] + simp only [replicate]; rw [append_zero_width] theorem replicate_succ {x : BitVec w} : x.replicate (n + 1) = diff --git a/tests/lean/run/instanceReducibility.lean b/tests/lean/run/instanceReducibility.lean index 5e75966085..285e5aaaf7 100644 --- a/tests/lean/run/instanceReducibility.lean +++ b/tests/lean/run/instanceReducibility.lean @@ -1,6 +1,6 @@ module -/-! Reducibility of instances should default to `[instance_reducible]` but be overridable. -/ +/-! Reducibility of instances should default to `[implicit_reducible]` but be overridable. -/ instance i1 : Inhabited Nat := inferInstance diff --git a/tests/lean/run/instanceReducible.lean b/tests/lean/run/instanceReducible.lean index 45a1affe43..1da9f6de09 100644 --- a/tests/lean/run/instanceReducible.lean +++ b/tests/lean/run/instanceReducible.lean @@ -23,7 +23,7 @@ attribute [instance] exposed #guard_msgs in attribute [local instance] exposed -@[expose, instance_reducible] +@[expose, implicit_reducible] public def exposedAndReducible : Inhabited Nat := inferInstance #guard_msgs in diff --git a/tests/lean/run/ofNatNormNum.lean b/tests/lean/run/ofNatNormNum.lean index 734d1cc72e..768e4aebf7 100644 --- a/tests/lean/run/ofNatNormNum.lean +++ b/tests/lean/run/ofNatNormNum.lean @@ -26,7 +26,7 @@ instance [S α] : OfNat α n where instance [S α] : OfNatSound α where ofNat_add n m := by induction m with - | zero => simp; erw [S.add_zero]; rfl + | zero => simp [OfNat.ofNat, S.ofNat]; erw [S.add_zero] | 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 diff --git a/tests/lean/run/symbolFrequency_foldRelevantConsts.lean b/tests/lean/run/symbolFrequency_foldRelevantConsts.lean index c206a6986d..d4d14adac0 100644 --- a/tests/lean/run/symbolFrequency_foldRelevantConsts.lean +++ b/tests/lean/run/symbolFrequency_foldRelevantConsts.lean @@ -19,7 +19,7 @@ run_meta do let consts ← ci.type.foldRelevantConstants (init := #[]) (fun n ns => return ns.push n) logInfo m!"{consts}" -/-- info: [Array, Nat, LT.lt, Array.size, HAdd.hAdd, OfNat.ofNat, Array.swap, Not] -/ +/-- info: [Array, Nat, LT.lt, HAdd.hAdd, OfNat.ofNat, Array.swap, Not] -/ #guard_msgs in run_meta do let ci ← getConstInfo `Array.eraseIdx.induct diff --git a/tests/lean/unfold1.lean b/tests/lean/unfold1.lean index d13a64c7e5..b47c757f79 100644 --- a/tests/lean/unfold1.lean +++ b/tests/lean/unfold1.lean @@ -15,11 +15,8 @@ theorem isEven_double (x : Nat) : isEven (2 * x) = true := by | succ x ih => unfold isEven trace_state - rw [Nat.mul_succ, Nat.add_succ] - simp unfold isOdd trace_state - simp exact ih theorem isEven_succ_succ (x : Nat) : isEven (x + 2) = isEven x := by diff --git a/tests/lean/unfold1.lean.expected.out b/tests/lean/unfold1.lean.expected.out index 82a91a8284..e0de7543d3 100644 --- a/tests/lean/unfold1.lean.expected.out +++ b/tests/lean/unfold1.lean.expected.out @@ -1,12 +1,8 @@ -unfold1.lean:22:4-22:8: error: `simp` made no progress case succ x : Nat ih : isEven (2 * x) = true -⊢ (match 2 * (x + 1) with - | 0 => true - | n.succ => isOdd n) = - true +⊢ isOdd (Nat.mul 2 x + 1) = true case succ x : Nat ih : isEven (2 * x) = true -⊢ isEven (2 * x) = true +⊢ isEven (Nat.mul 2 x) = true diff --git a/tests/lean/whnfProj.lean.expected.out b/tests/lean/whnfProj.lean.expected.out index d3a8c24ff1..440f526a63 100644 --- a/tests/lean/whnfProj.lean.expected.out +++ b/tests/lean/whnfProj.lean.expected.out @@ -1,6 +1,6 @@ [Meta.debug] 1. x + 1 [Meta.debug] 2. x + 1 -[Meta.debug] 3. x.add 1 +[Meta.debug] 3. (x.add 0).succ [Meta.debug] 4. (x.add 0).succ [Meta.debug] 1. (x, x + 1).fst [Meta.debug] 2. x