diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean index 01fa752649f8..cba6898dbe27 100644 --- a/src/Init/Control/Except.lean +++ b/src/Init/Control/Except.lean @@ -128,7 +128,7 @@ end Except /-- Adds exceptions of type `ε` to a monad `m`. -/ -def ExceptT (ε : Type u) (m : Type u → Type v) (α : Type u) : Type v := +@[implicit_reducible] def ExceptT (ε : Type u) (m : Type u → Type v) (α : Type u) : Type v := m (Except ε α) /-- diff --git a/src/Init/Control/ExceptCps.lean b/src/Init/Control/ExceptCps.lean index d38cbd99b91b..22d39a8475d5 100644 --- a/src/Init/Control/ExceptCps.lean +++ b/src/Init/Control/ExceptCps.lean @@ -21,7 +21,7 @@ Adds exceptions of type `ε` to a monad `m`. Instead of using `Except ε` to model exceptions, this implementation uses continuation passing style. This has different performance characteristics from `ExceptT ε`. -/ -@[expose] def ExceptCpsT (ε : Type u) (m : Type u → Type v) (α : Type u) := (β : Type u) → (α → m β) → (ε → m β) → m β +@[expose, implicit_reducible] def ExceptCpsT (ε : Type u) (m : Type u → Type v) (α : Type u) := (β : Type u) → (α → m β) → (ε → m β) → m β namespace ExceptCpsT diff --git a/src/Init/Control/Id.lean b/src/Init/Control/Id.lean index 6f2de218d45f..3132c428c7f7 100644 --- a/src/Init/Control/Id.lean +++ b/src/Init/Control/Id.lean @@ -36,7 +36,7 @@ def containsFive (xs : List Nat) : Bool := Id.run do true ``` -/ -@[expose] def Id (type : Type u) : Type u := type +@[expose, implicit_reducible] def Id (type : Type u) : Type u := type namespace Id diff --git a/src/Init/Control/Lawful/MonadLift/Instances.lean b/src/Init/Control/Lawful/MonadLift/Instances.lean index a15130c871a3..7454ed9dc961 100644 --- a/src/Init/Control/Lawful/MonadLift/Instances.lean +++ b/src/Init/Control/Lawful/MonadLift/Instances.lean @@ -103,11 +103,11 @@ namespace StateRefT' instance {ω σ : Type} {m : Type → Type} [Monad m] : LawfulMonadLift m (StateRefT' ω σ m) where monadLift_pure _ := by simp only [MonadLift.monadLift, pure] - unfold StateRefT'.lift instMonad._aux_5 ReaderT.pure + unfold StateRefT'.lift ReaderT.pure simp only monadLift_bind _ _ := by simp only [MonadLift.monadLift, bind] - unfold StateRefT'.lift instMonad._aux_13 ReaderT.bind + unfold StateRefT'.lift ReaderT.bind simp only end StateRefT' diff --git a/src/Init/Control/Option.lean b/src/Init/Control/Option.lean index 56688d610d65..7c9f69e13455 100644 --- a/src/Init/Control/Option.lean +++ b/src/Init/Control/Option.lean @@ -21,7 +21,7 @@ instance : ToBool (Option α) := ⟨Option.isSome⟩ Adds the ability to fail to a monad. Unlike ordinary exceptions, there is no way to signal why a failure occurred. -/ -@[expose] def OptionT (m : Type u → Type v) (α : Type u) : Type v := +@[expose, implicit_reducible] def OptionT (m : Type u → Type v) (α : Type u) : Type v := m (Option α) /-- diff --git a/src/Init/Control/State.lean b/src/Init/Control/State.lean index 4106ebc8da41..75479ff2840f 100644 --- a/src/Init/Control/State.lean +++ b/src/Init/Control/State.lean @@ -22,7 +22,7 @@ Adds a mutable state of type `σ` to a monad. Actions in the resulting monad are functions that take an initial state and return, in `m`, a tuple of a value and a state. -/ -@[expose] def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) := +@[expose, implicit_reducible] def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) := σ → m (α × σ) /-- diff --git a/src/Init/Control/StateCps.lean b/src/Init/Control/StateCps.lean index 96a533956938..447a56b5c79a 100644 --- a/src/Init/Control/StateCps.lean +++ b/src/Init/Control/StateCps.lean @@ -21,7 +21,7 @@ The State monad transformer using CPS style. An alternative implementation of a state monad transformer that internally uses continuation passing style instead of tuples. -/ -@[expose] def StateCpsT (σ : Type u) (m : Type u → Type v) (α : Type u) := (δ : Type u) → σ → (α → σ → m δ) → m δ +@[expose, implicit_reducible] def StateCpsT (σ : Type u) (m : Type u → Type v) (α : Type u) := (δ : Type u) → σ → (α → σ → m δ) → m δ namespace StateCpsT diff --git a/src/Init/Control/StateRef.lean b/src/Init/Control/StateRef.lean index 833811aa9685..272d9c54da29 100644 --- a/src/Init/Control/StateRef.lean +++ b/src/Init/Control/StateRef.lean @@ -20,7 +20,7 @@ A state monad that uses an actual mutable reference cell (i.e. an `ST.Ref ω σ` The macro `StateRefT σ m α` infers `ω` from `m`. It should normally be used instead. -/ -@[expose] def StateRefT' (ω : Type) (σ : Type) (m : Type → Type) (α : Type) : Type := ReaderT (ST.Ref ω σ) m α +@[expose, implicit_reducible] def StateRefT' (ω : Type) (σ : Type) (m : Type → Type) (α : Type) : Type := ReaderT (ST.Ref ω σ) m α /-! Recall that `StateRefT` is a macro that infers `ω` from the `m`. -/ diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 4496fd76d775..07c700416822 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -1331,7 +1331,7 @@ def Subrelation {α : Sort u} (q r : α → α → Prop) := The inverse image of `r : β → β → Prop` by a function `α → β` is the relation `s : α → α → Prop` defined by `s a b = r (f a) (f b)`. -/ -def InvImage {α : Sort u} {β : Sort v} (r : β → β → Prop) (f : α → β) : α → α → Prop := +@[implicit_reducible] def InvImage {α : Sort u} {β : Sort v} (r : β → β → Prop) (f : α → β) : α → α → Prop := fun a₁ a₂ => r (f a₁) (f a₂) /-- @@ -1478,7 +1478,7 @@ Examples: * `(1, 2).map (· + 1) (· * 3) = (2, 6)` * `(1, 2).map toString (· * 3) = ("1", 6)` -/ -def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂} +@[implicit_reducible] def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂} (f : α₁ → α₂) (g : β₁ → β₂) : α₁ × β₁ → α₂ × β₂ | (a, b) => (f a, g b) diff --git a/src/Init/Data/Array/DecidableEq.lean b/src/Init/Data/Array/DecidableEq.lean index a7a702c66578..a4d25cabac4e 100644 --- a/src/Init/Data/Array/DecidableEq.lean +++ b/src/Init/Data/Array/DecidableEq.lean @@ -76,7 +76,7 @@ theorem isEqv_eq_decide (xs ys : Array α) (r) : simpa [isEqv_iff_rel] using h' @[simp, grind =] theorem isEqv_toList [BEq α] (xs ys : Array α) : (xs.toList.isEqv ys.toList r) = (xs.isEqv ys r) := by - simp [isEqv_eq_decide, List.isEqv_eq_decide, Array.size]; rfl + simp [isEqv_eq_decide, List.isEqv_eq_decide, Array.size] theorem eq_of_isEqv [DecidableEq α] (xs ys : Array α) (h : Array.isEqv xs ys (fun x y => x = y)) : xs = ys := by have ⟨h, h'⟩ := rel_of_isEqv h @@ -154,7 +154,7 @@ theorem beq_eq_decide [BEq α] (xs ys : Array α) : simp [BEq.beq, isEqv_eq_decide] @[simp, grind =] theorem beq_toList [BEq α] (xs ys : Array α) : (xs.toList == ys.toList) = (xs == ys) := by - simp [beq_eq_decide, List.beq_eq_decide, Array.size]; rfl + simp [beq_eq_decide, List.beq_eq_decide, Array.size] end Array diff --git a/src/Init/Data/Array/FinRange.lean b/src/Init/Data/Array/FinRange.lean index dc743a3d2300..9d51d3a045a6 100644 --- a/src/Init/Data/Array/FinRange.lean +++ b/src/Init/Data/Array/FinRange.lean @@ -26,7 +26,7 @@ Examples: * `Array.finRange 0 = (#[] : Array (Fin 0))` * `Array.finRange 2 = (#[0, 1] : Array (Fin 2))` -/ -protected def finRange (n : Nat) : Array (Fin n) := ofFn fun i => i +@[expose, implicit_reducible] protected def finRange (n : Nat) : Array (Fin n) := ofFn fun i => i @[simp, grind =] theorem size_finRange {n} : (Array.finRange n).size = n := by simp [Array.finRange] diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index f43763fa9029..c4384d9e7dbb 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -2831,6 +2831,7 @@ theorem getElem_extract_aux {xs : Array α} {start stop : Nat} (h : i < (xs.extr rw [size_extract] at h; apply Nat.add_lt_of_lt_sub'; apply Nat.lt_of_lt_of_le h apply Nat.sub_le_sub_right; apply Nat.min_le_right +set_option backward.isDefEq.respectTransparency.types false in @[simp, grind =] theorem getElem_extract {xs : Array α} {start stop : Nat} (h : i < (xs.extract start stop).size) : (xs.extract start stop)[i] = xs[start + i]'(getElem_extract_aux h) := diff --git a/src/Init/Data/Array/MapIdx.lean b/src/Init/Data/Array/MapIdx.lean index 98defc144722..f1949d738dee 100644 --- a/src/Init/Data/Array/MapIdx.lean +++ b/src/Init/Data/Array/MapIdx.lean @@ -198,6 +198,7 @@ theorem mapFinIdx_append {xs ys : Array α} {f : (i : Nat) → α → (h : i < ( cases ys simp [List.mapFinIdx_append, Array.size] +set_option backward.isDefEq.respectTransparency.types false in @[simp, grind =] theorem mapFinIdx_push {xs : Array α} {a : α} {f : (i : Nat) → α → (h : i < (xs.push a).size) → β} : mapFinIdx (xs.push a) f = diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean index 07c71162a302..26c03bf2143c 100644 --- a/src/Init/Data/BitVec/Basic.lean +++ b/src/Init/Data/BitVec/Basic.lean @@ -559,6 +559,7 @@ As a numeric operation, this is equivalent to `x / 2^s`, rounding down. SMT-LIB name: `bvlshr` except this operator uses a `Nat` shift value. -/ +@[implicit_reducible] def ushiftRight (x : BitVec n) (s : Nat) : BitVec n := (x.toNat >>> s)#'(by let ⟨x, lt⟩ := x @@ -576,6 +577,7 @@ As a numeric operation, this is equivalent to `x.toInt >>> s`. SMT-LIB name: `bvashr` except this operator uses a `Nat` shift value. -/ +@[implicit_reducible] def sshiftRight (x : BitVec n) (s : Nat) : BitVec n := .ofInt n (x.toInt >>> s) instance {n} : HShiftLeft (BitVec m) (BitVec n) (BitVec m) := ⟨fun x y => x <<< y.toNat⟩ diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 71c9ef5714f8..b3f8df3fccf8 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -2004,6 +2004,7 @@ theorem toInt_smod {x y : BitVec w} : simp [BitVec.toInt_eq_neg_toNat_neg_of_msb_true, hxmsb, hymsb, Int.fmod_eq_emod_of_nonneg _] +set_option backward.isDefEq.respectTransparency.types false in theorem getElem_smod {x y : BitVec w} (h : i < w) : (x.smod y)[i] = match x.msb, y.msb with @@ -2029,6 +2030,7 @@ theorem getLsbD_smod {x y : BitVec w} : · by_cases hxy : x % -y = 0#w <;> simp [hx, hy, hxy] · simp [hx, hy] +set_option backward.isDefEq.respectTransparency.types false in theorem getMsbD_smod {x y : BitVec w} : (x.smod y).getMsbD i = match x.msb, y.msb with diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 696ed3ea6e4c..11b8134875d5 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -2115,7 +2115,7 @@ theorem ushiftRight_eq_zero {x : BitVec w} {n : Nat} (hn : w ≤ n) : have : 2^w ≤ 2^n := Nat.pow_le_pow_of_le Nat.one_lt_two hn rw [Nat.shiftRight_eq_div_pow, Nat.div_eq_of_lt (by omega)] - +set_option backward.isDefEq.respectTransparency.types false in /-- Unsigned shift right by at least one bit makes the interpretations of the bitvector as an `Int` or `Nat` agree, because it makes the value of the bitvector less than or equal to `2^(w-1)`. @@ -4702,6 +4702,7 @@ theorem toFin_srem {x y : BitVec w} : (x.srem y).toFin = /-! ### smod -/ +set_option backward.isDefEq.respectTransparency.types false in /-- Equation theorem for `smod` in terms of `umod`. -/ theorem smod_eq (x y : BitVec w) : x.smod y = match x.msb, y.msb with @@ -6142,6 +6143,7 @@ theorem clzAuxRec_le {x : BitVec w} (n : Nat) : · simp only [hxn, Bool.false_eq_true, reduceIte] exact ihn +set_option backward.isDefEq.respectTransparency.types false in theorem clzAuxRec_eq_iff_of_getLsbD_false {x : BitVec w} (h : ∀ i, n < i → x.getLsbD i = false) : x.clzAuxRec n = BitVec.ofNat w w ↔ ∀ j, j ≤ n → x.getLsbD j = false := by rcases w with _|w diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean index edc24c29b690..03d7bdafc3e4 100644 --- a/src/Init/Data/Bool.lean +++ b/src/Init/Data/Bool.lean @@ -64,8 +64,8 @@ theorem ne_false_iff : {b : Bool} → b ≠ false ↔ b = true := by decide theorem eq_iff_iff {a b : Bool} : a = b ↔ (a ↔ b) := by cases b <;> simp -@[simp] theorem decide_eq_true {b : Bool} [Decidable (b = true)] : decide (b = true) = b := by cases b <;> simp -@[simp] theorem decide_eq_false {b : Bool} [Decidable (b = false)] : decide (b = false) = !b := by cases b <;> simp +@[simp] theorem decide_eq_true {b : Bool} {_ : Decidable (b = true)} : decide (b = true) = b := by cases b <;> simp +@[simp] theorem decide_eq_false {b : Bool} {_ : Decidable (b = false)} : decide (b = false) = !b := by cases b <;> simp theorem decide_true_eq {b : Bool} [Decidable (true = b)] : decide (true = b) = b := by cases b <;> simp theorem decide_false_eq {b : Bool} [Decidable (false = b)] : decide (false = b) = !b := by cases b <;> simp diff --git a/src/Init/Data/ByteArray/Lemmas.lean b/src/Init/Data/ByteArray/Lemmas.lean index 02cc3efb3de8..8b0d9d3302e6 100644 --- a/src/Init/Data/ByteArray/Lemmas.lean +++ b/src/Init/Data/ByteArray/Lemmas.lean @@ -111,13 +111,13 @@ theorem getElem_eq_getElem_data {a : ByteArray} {i : Nat} {h : i < a.size} : theorem getElem_append_left {i : Nat} {a b : ByteArray} {h : i < (a ++ b).size} (hlt : i < a.size) : (a ++ b)[i] = a[i] := by simp only [getElem_eq_getElem_data, data_append] - rw [Array.getElem_append_left (by simpa)]; rfl + rw [Array.getElem_append_left (by simpa)] theorem getElem_append_right {i : Nat} {a b : ByteArray} {h : i < (a ++ b).size} (hle : a.size ≤ i) : (a ++ b)[i] = b[i - a.size]'(by simp_all; omega) := by simp only [getElem_eq_getElem_data, data_append] rw [Array.getElem_append_right (by simpa)] - simp; rfl + simp @[simp] theorem _root_.List.getElem_toByteArray {l : List UInt8} {i : Nat} {h : i < l.toByteArray.size} : @@ -223,7 +223,7 @@ theorem getElem_extract_aux {xs : ByteArray} {start stop : Nat} (h : i < (xs.ext theorem getElem_extract {i : Nat} {b : ByteArray} {start stop : Nat} (h) : (b.extract start stop)[i]'h = b[start + i]'(getElem_extract_aux h) := by - simp [getElem_eq_getElem_data]; rfl + simp [getElem_eq_getElem_data] theorem extract_eq_extract_left {a : ByteArray} {i i' j : Nat} : a.extract i j = a.extract i' j ↔ min j a.size - i = min j a.size - i' := by @@ -236,25 +236,25 @@ theorem extract_add_one {a : ByteArray} {i : Nat} (ha : i + 1 ≤ a.size) : omega · rename_i j hj hj' obtain rfl : j = 0 := by simpa using hj' - simp [ByteArray.getElem_eq_getElem_data]; rfl + simp [ByteArray.getElem_eq_getElem_data] theorem extract_add_two {a : ByteArray} {i : Nat} (ha : i + 2 ≤ a.size) : a.extract i (i + 2) = [a[i], a[i + 1]].toByteArray := by rw [extract_eq_extract_append_extract (i + 1) (by simp) (by omega), extract_add_one (by omega), extract_add_one (by omega)] - simp [← List.toByteArray_append]; rfl + simp [← List.toByteArray_append] theorem extract_add_three {a : ByteArray} {i : Nat} (ha : i + 3 ≤ a.size) : a.extract i (i + 3) = [a[i], a[i + 1], a[i + 2]].toByteArray := by rw [extract_eq_extract_append_extract (i + 1) (by simp) (by omega), extract_add_one (by omega), extract_add_two (by omega)] - simp [← List.toByteArray_append]; rfl + simp [← List.toByteArray_append] theorem extract_add_four {a : ByteArray} {i : Nat} (ha : i + 4 ≤ a.size) : a.extract i (i + 4) = [a[i], a[i + 1], a[i + 2], a[i + 3]].toByteArray := by rw [extract_eq_extract_append_extract (i + 1) (by simp) (by omega), extract_add_one (by omega), extract_add_three (by omega)] - simp [← List.toByteArray_append]; rfl + simp [← List.toByteArray_append] theorem append_assoc {a b c : ByteArray} : a ++ b ++ c = a ++ (b ++ c) := by ext1 diff --git a/src/Init/Data/Dyadic/Basic.lean b/src/Init/Data/Dyadic/Basic.lean index fe78c8478bc0..bc5faf5e05aa 100644 --- a/src/Init/Data/Dyadic/Basic.lean +++ b/src/Init/Data/Dyadic/Basic.lean @@ -408,7 +408,7 @@ theorem ofIntWithPrec_shiftLeft_add {n : Nat} : /-- The "precision" of a dyadic number, i.e. in `n * 2^(-p)` with `n` odd the precision is `p`. -/ -- TODO: If `WithBot` is upstreamed, replace this with `WithBot Int`. -def precision : Dyadic → Option Int +@[implicit_reducible] def precision : Dyadic → Option Int | .zero => none | .ofOdd _ p _ => some p diff --git a/src/Init/Data/Fin/Basic.lean b/src/Init/Data/Fin/Basic.lean index e4f0208e41a2..890733cbbdc3 100644 --- a/src/Init/Data/Fin/Basic.lean +++ b/src/Init/Data/Fin/Basic.lean @@ -40,7 +40,7 @@ Examples: * `(2 : Fin 3).succ = (3 : Fin 4)` * `(2 : Fin 3) + 1 = (0 : Fin 3)` -/ -def succ : Fin n → Fin (n + 1) +@[instance_reducible] def succ : Fin n → Fin (n + 1) | ⟨i, h⟩ => ⟨i+1, Nat.succ_lt_succ h⟩ variable {n : Nat} @@ -276,7 +276,7 @@ Examples: * `Fin.last 4 = (4 : Fin 5)` * `(Fin.last 0).val = (0 : Nat)` -/ -@[inline] def last (n : Nat) : Fin (n + 1) := ⟨n, n.lt_succ_self⟩ +@[inline, implicit_reducible] def last (n : Nat) : Fin (n + 1) := ⟨n, n.lt_succ_self⟩ /-- Replaces the bound with another that is suitable for the value. @@ -302,14 +302,14 @@ Coarsens a bound to one at least as large. See also `Fin.castAdd` for a version that represents the larger bound with addition rather than an explicit inequality proof. -/ -@[inline] def castLE (h : n ≤ m) (i : Fin n) : Fin m := ⟨i, Nat.lt_of_lt_of_le i.2 h⟩ +@[inline, implicit_reducible] def castLE (h : n ≤ m) (i : Fin n) : Fin m := ⟨i, Nat.lt_of_lt_of_le i.2 h⟩ /-- Uses a proof that two bounds are equal to allow a value bounded by one to be used with the other. In other words, when `eq : n = m`, `Fin.cast eq i` converts `i : Fin n` into a `Fin m`. -/ -@[inline] protected def cast (eq : n = m) (i : Fin n) : Fin m := ⟨i, eq ▸ i.2⟩ +@[inline, implicit_reducible] protected def cast (eq : n = m) (i : Fin n) : Fin m := ⟨i, eq ▸ i.2⟩ /-- Coarsens a bound to one at least as large. @@ -317,13 +317,13 @@ Coarsens a bound to one at least as large. See also `Fin.natAdd` and `Fin.addNat` for addition functions that increase the bound, and `Fin.castLE` for a version that uses an explicit inequality proof. -/ -@[inline] def castAdd (m) : Fin n → Fin (n + m) := +@[inline, implicit_reducible] def castAdd (m) : Fin n → Fin (n + m) := castLE <| Nat.le_add_right n m /-- Coarsens a bound by one. -/ -@[inline] def castSucc : Fin n → Fin (n + 1) := castAdd 1 +@[inline, implicit_reducible] def castSucc : Fin n → Fin (n + 1) := castAdd 1 /-- Adds a natural number to a `Fin`, increasing the bound. diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean index 48f4a7fb8639..784727a5e0c2 100644 --- a/src/Init/Data/Fin/Lemmas.lean +++ b/src/Init/Data/Fin/Lemmas.lean @@ -1012,7 +1012,7 @@ For the induction: @[simp, grind =] theorem reverseInduction_last {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ} : (reverseInduction zero succ (Fin.last n) : motive (Fin.last n)) = zero := by - rw [reverseInduction, reverseInduction.go]; simp; rfl + rw [reverseInduction, reverseInduction.go]; simp private theorem reverseInduction_castSucc_aux {n : Nat} {motive : Fin (n + 1) → Sort _} {succ} (i : Fin n) (j : Nat) (h) (h2 : i.1 < j) (zero : motive ⟨j, h⟩) : @@ -1023,7 +1023,7 @@ private theorem reverseInduction_castSucc_aux {n : Nat} {motive : Fin (n + 1) | succ j ih => rw [reverseInduction.go, dif_neg (by exact Nat.ne_of_lt h2)] by_cases hij : i = j - · subst hij; simp [reverseInduction.go]; rfl + · subst hij; simp [reverseInduction.go] · dsimp only rw [ih _ _ (by omega), eq_comm, reverseInduction.go, dif_neg (by change i.1 + 1 ≠ _; omega)] diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean index 7098c0dad879..81112d605bec 100644 --- a/src/Init/Data/Int/Basic.lean +++ b/src/Init/Data/Int/Basic.lean @@ -157,7 +157,7 @@ Examples: * `(7 : Int) + (6 : Int) = 13` * `(6 : Int) + (-6 : Int) = 0` -/ -@[extern "lean_int_add"] +@[extern "lean_int_add", implicit_reducible] protected def add (m n : @& Int) : Int := match m, n with | ofNat m, ofNat n => ofNat (m + n) @@ -323,7 +323,7 @@ Examples: * `(0 : Int).natAbs = 0` * `(-11 : Int).natAbs = 11` -/ -@[extern "lean_nat_abs"] +@[extern "lean_nat_abs", implicit_reducible] def natAbs (m : @& Int) : Nat := match m with | ofNat m => m diff --git a/src/Init/Data/Int/Order.lean b/src/Init/Data/Int/Order.lean index 7fd2319375b6..e0a2d830d099 100644 --- a/src/Init/Data/Int/Order.lean +++ b/src/Init/Data/Int/Order.lean @@ -1406,7 +1406,7 @@ theorem natAbs_mul_self : ∀ {a : Int}, ↑(natAbs a * natAbs a) = a * a protected theorem eq_nat_or_neg (a : Int) : ∃ n : Nat, a = n ∨ a = -↑n := ⟨_, natAbs_eq a⟩ theorem natAbs_mul_natAbs_eq {a b : Int} {c : Nat} - (h : a * b = (c : Int)) : a.natAbs * b.natAbs = c := by rw [← natAbs_mul, h, natAbs.eq_def] + (h : a * b = (c : Int)) : a.natAbs * b.natAbs = c := by rw [← natAbs_mul, h, natAbs_natCast] @[simp] theorem natAbs_mul_self' (a : Int) : (natAbs a * natAbs a : Int) = a * a := by rw [← Int.natCast_mul, natAbs_mul_self] diff --git a/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean b/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean index 290f4c754c44..3d93c8d59313 100644 --- a/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean +++ b/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean @@ -18,7 +18,7 @@ section ULiftT namespace Iterators /-- `ULiftT.{v, u}` shrinks a monad on `Type max u v` to a monad on `Type u`. -/ -@[expose] -- for codegen +@[expose, implicit_reducible] -- for codegen def ULiftT (n : Type max u v → Type v') (α : Type u) := n (ULift.{v} α) /-- Returns the underlying `n`-monadic representation of a `ULiftT n α` value. -/ diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean index 2d486ce3a44d..77bfc7088df6 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean @@ -207,6 +207,7 @@ theorem Iter.step_mapM {f : β → n γ} | .skip it' h => rfl | .done h => rfl +set_option backward.isDefEq.respectTransparency.types false in theorem Iter.step_filterMap {f : β → Option γ} : (it.filterMap f).step = match it.step with | .yield it' out h => @@ -247,6 +248,7 @@ theorem Iter.val_step_filterMap {f : β → Option γ} : · simp · simp +set_option backward.isDefEq.respectTransparency.types false in theorem Iter.step_map {f : β → γ} : (it.map f).step = match it.step with | .yield it' out h => @@ -259,6 +261,7 @@ theorem Iter.step_map {f : β → γ} : generalize it.toIterM.step.run = step cases step.inflate using PlausibleIterStep.casesOn <;> simp +set_option backward.isDefEq.respectTransparency.types false in def Iter.step_filter {f : β → Bool} : (it.filter f).step = match it.step with | .yield it' out h => @@ -278,6 +281,7 @@ def Iter.step_filter {f : β → Bool} : · simp · simp +set_option backward.isDefEq.respectTransparency.types false in def Iter.val_step_filter {f : β → Bool} : (it.filter f).step.val = match it.step.val with | .yield it' out => diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Take.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Take.lean index d2f9a602f7b8..63a4f325f0e3 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/Take.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/Take.lean @@ -102,6 +102,7 @@ theorem Iter.toList_take_zero {α β} [Iterator α Id β] rw [toList_eq_match_step] simp [step_take] +set_option backward.isDefEq.respectTransparency.types false in theorem Iter.step_toTake {α β} [Iterator α Id β] [Finite α Id] {it : Iter (α := α) β} : it.toTake.step = ( diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean index 660518dc265b..5db4d9d7f85d 100644 --- a/src/Init/Data/List/Attach.lean +++ b/src/Init/Data/List/Attach.lean @@ -404,7 +404,7 @@ theorem foldr_attach {l : List α} {f : α → β → β} {b : β} : theorem attach_map {l : List α} {f : α → β} : (l.map f).attach = l.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem h⟩) := by - induction l <;> simp [*] + induction l <;> simp [*, map] theorem attachWith_map {l : List α} {f : α → β} {P : β → Prop} (H : ∀ (b : β), b ∈ l.map f → P b) : (l.map f).attachWith P H = (l.attachWith (P ∘ f) (fun _ h => H _ (mem_map_of_mem h))).map diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index 354a7cfb216d..0ab3a2f3a00a 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -474,8 +474,8 @@ We define the basic functional programming operations on `List`: /-! ### map -/ -@[simp, grind =] theorem map_nil {f : α → β} : map f [] = [] := rfl -@[simp, grind =] theorem map_cons {f : α → β} {a : α} {l : List α} : map f (a :: l) = f a :: map f l := rfl +@[simp, grind =] theorem map_nil {f : α → β} : map f [] = [] := id rfl +@[simp, grind =] theorem map_cons {f : α → β} {a : α} {l : List α} : map f (a :: l) = f a :: map f l := id rfl /-! ### filter -/ @@ -937,8 +937,8 @@ def drop : (n : Nat) → (xs : List α) → List α @[simp, grind =] theorem drop_nil : ([] : List α).drop i = [] := by cases i <;> rfl -@[simp, grind =] theorem drop_zero {l : List α} : l.drop 0 = l := rfl -@[simp, grind =] theorem drop_succ_cons {a : α} {l : List α} {i : Nat} : (a :: l).drop (i + 1) = l.drop i := rfl +@[simp, grind =] theorem drop_zero {l : List α} : l.drop 0 = l := id rfl +@[simp, grind =] theorem drop_succ_cons {a : α} {l : List α} {i : Nat} : (a :: l).drop (i + 1) = l.drop i := id rfl theorem drop_eq_nil_of_le {as : List α} {i : Nat} (h : as.length ≤ i) : as.drop i = [] := by match as, i with diff --git a/src/Init/Data/List/FinRange.lean b/src/Init/Data/List/FinRange.lean index 6f9b08b9438b..9e88ddc6baff 100644 --- a/src/Init/Data/List/FinRange.lean +++ b/src/Init/Data/List/FinRange.lean @@ -25,7 +25,7 @@ Examples: * `List.finRange 0 = ([] : List (Fin 0))` * `List.finRange 2 = ([0, 1] : List (Fin 2))` -/ -@[expose] def finRange (n : Nat) : List (Fin n) := ofFn fun i => i +@[expose, implicit_reducible] def finRange (n : Nat) : List (Fin n) := ofFn fun i => i @[simp, grind =] theorem length_finRange {n : Nat} : (List.finRange n).length = n := by simp [List.finRange] diff --git a/src/Init/Data/List/MinMaxOn.lean b/src/Init/Data/List/MinMaxOn.lean index 25b6e091c2dc..42fdd58a32c0 100644 --- a/src/Init/Data/List/MinMaxOn.lean +++ b/src/Init/Data/List/MinMaxOn.lean @@ -247,7 +247,7 @@ protected theorem min_map (xs.map f).min (by simpa) = f (xs.minOn f h) := by match xs with | x :: xs => - simp only [List.minOn, map_cons, List.min, foldl_map] + simp only [List.minOn, map, List.min, foldl_map] rw [foldl_hom] simp [min_apply] diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean index 7694777b40bf..00ce45810586 100644 --- a/src/Init/Data/List/TakeDrop.lean +++ b/src/Init/Data/List/TakeDrop.lean @@ -256,7 +256,7 @@ theorem dropLast_eq_take {l : List α} : l.dropLast = l.take (l.length - 1) := b | [], i => by simp | l, 0 => by simp | _ :: tl, n + 1 => by - dsimp + simp rw [map_drop] theorem drop_eq_extract {l : List α} {k : Nat} : diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean index dfec099a93a9..3c652630391f 100644 --- a/src/Init/Data/List/ToArray.lean +++ b/src/Init/Data/List/ToArray.lean @@ -512,8 +512,8 @@ private theorem takeWhile_go_succ (p : α → Bool) (a : α) (l : List α) (i : simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, getElem_toArray, getElem_cons_succ] split - rw [takeWhile_go_succ] - rfl + · rw [takeWhile_go_succ] + · rfl private theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) : Array.takeWhile.go p l.toArray i r = r ++ (takeWhile p (l.drop i)).toArray := by diff --git a/src/Init/Data/Option/Attach.lean b/src/Init/Data/Option/Attach.lean index 9fe81974d481..d448370861dc 100644 --- a/src/Init/Data/Option/Attach.lean +++ b/src/Init/Data/Option/Attach.lean @@ -322,7 +322,7 @@ If this function is encountered in a proof state, the right approach is usually It is a synonym for `Option.map Subtype.val`. -/ -@[expose] +@[expose, implicit_reducible] def unattach {α : Type _} {p : α → Prop} (o : Option { x // p x }) := o.map (·.val) @[simp] theorem unattach_none {p : α → Prop} : (none : Option { x // p x }).unattach = none := rfl diff --git a/src/Init/Data/Option/Basic.lean b/src/Init/Data/Option/Basic.lean index 707348ca449a..1bdc153ad975 100644 --- a/src/Init/Data/Option/Basic.lean +++ b/src/Init/Data/Option/Basic.lean @@ -58,7 +58,7 @@ deriving instance BEq for Option @[simp, grind =] theorem map_some (a) (f : α → β) : (some a).map f = some (f a) := rfl /-- Lifts an optional value to any `Alternative`, sending `none` to `failure`. -/ -def getM [Alternative m] : Option α → m α +@[implicit_reducible] def getM [Alternative m] : Option α → m α | none => failure | some a => pure a @@ -66,7 +66,7 @@ def getM [Alternative m] : Option α → m α @[simp, grind =] theorem getM_some [Alternative m] {a : α} : getM (some a) = (pure a : m α) := rfl /-- Returns `true` on `some x` and `false` on `none`. -/ -@[inline] def isSome : Option α → Bool +@[inline, implicit_reducible] def isSome : Option α → Bool | some _ => true | none => false @@ -82,7 +82,7 @@ Examples: * `(none : Option Nat).isNone = true` * `(some Nat.add).isNone = false` -/ -@[inline] def isNone : Option α → Bool +@[inline, implicit_reducible] def isNone : Option α → Bool | some _ => false | none => true @@ -118,7 +118,7 @@ Examples: * `(some 2).bind (Option.guard (· > 2)) = none` * `(some 4).bind (Option.guard (· > 2)) = some 4` -/ -@[inline] protected def bind : Option α → (α → Option β) → Option β +@[inline, implicit_reducible] protected def bind : Option α → (α → Option β) → Option β | none, _ => none | some a, f => f a @@ -194,7 +194,7 @@ Examples: * `none.filter (fun x : Nat => x % 2 == 0) = none` * `none.filter (fun x : Nat => true) = none` -/ -@[always_inline, inline] protected def filter (p : α → Bool) : Option α → Option α +@[always_inline, inline, implicit_reducible] protected def filter (p : α → Bool) : Option α → Option α | some a => if p a then some a else none | none => none @@ -206,7 +206,7 @@ Examples: * `(some 22).all (· % 2 == 0) = true * `none.all (fun x : Nat => x % 2 == 0) = true -/ -@[always_inline, inline] protected def all (p : α → Bool) : Option α → Bool +@[always_inline, inline, implicit_reducible] protected def all (p : α → Bool) : Option α → Bool | some a => p a | none => true @@ -221,7 +221,7 @@ Examples: * `(some 22).any (· % 2 == 0) = true * `none.any (fun x : Nat => true) = false -/ -@[always_inline, inline] protected def any (p : α → Bool) : Option α → Bool +@[always_inline, inline, implicit_reducible] protected def any (p : α → Bool) : Option α → Bool | some a => p a | none => false @@ -393,7 +393,7 @@ Examples: * `Option.guard (· > 2) 1 = none` * `Option.guard (· > 2) 5 = some 5` -/ -@[inline] def guard (p : α → Bool) (a : α) : Option α := +@[inline, implicit_reducible] def guard (p : α → Bool) (a : α) : Option α := if p a then some a else none /-- @@ -436,7 +436,7 @@ Examples: * `(some none).join = none` * `(some (some v)).join = some v` -/ -@[inline] def join (x : Option (Option α)) : Option α := x.bind id +@[inline, implicit_reducible] def join (x : Option (Option α)) : Option α := x.bind id @[simp, grind =] theorem join_none : (none : Option (Option α)).join = none := rfl @[simp, grind =] theorem join_some : (some o).join = o := rfl diff --git a/src/Init/Data/Option/Instances.lean b/src/Init/Data/Option/Instances.lean index bf7e5187d2cc..a840a7529e21 100644 --- a/src/Init/Data/Option/Instances.lean +++ b/src/Init/Data/Option/Instances.lean @@ -134,14 +134,14 @@ some ⟨3, ⋯⟩ none ``` -/ -@[inline, expose] def pelim (o : Option α) (b : β) (f : (a : α) → o = some a → β) : β := +@[inline, expose, implicit_reducible] def pelim (o : Option α) (b : β) (f : (a : α) → o = some a → β) : β := match o with | none => b | some a => f a rfl /-- Partial filter. If `o : Option α`, `p : (a : α) → o = some a → Bool`, then `o.pfilter p` is the same as `o.filter p` but `p` is passed the proof that `o = some a`. -/ -@[inline, expose] def pfilter (o : Option α) (p : (a : α) → o = some a → Bool) : Option α := +@[inline, expose, implicit_reducible] def pfilter (o : Option α) (p : (a : α) → o = some a → Bool) : Option α := match o with | none => none | some a => bif p a rfl then o else none diff --git a/src/Init/Data/Range/Lemmas.lean b/src/Init/Data/Range/Lemmas.lean index ebedf0c84d50..4c28b502132d 100644 --- a/src/Init/Data/Range/Lemmas.lean +++ b/src/Init/Data/Range/Lemmas.lean @@ -59,6 +59,7 @@ private theorem size_eq (r : Range) (h : i < r.stop) : rw [Nat.div_eq_iff] <;> omega omega +set_option backward.isDefEq.respectTransparency.types false in private theorem forIn'_loop_eq_forIn'_range' [Monad m] (r : Range) (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) (i) (w₁) (w₂) : forIn'.loop r f init i w₁ w₂ = diff --git a/src/Init/Data/Range/Polymorphic/Lemmas.lean b/src/Init/Data/Range/Polymorphic/Lemmas.lean index a0421905be16..33fbd3b307d8 100644 --- a/src/Init/Data/Range/Polymorphic/Lemmas.lean +++ b/src/Init/Data/Range/Polymorphic/Lemmas.lean @@ -872,7 +872,8 @@ theorem toArray_eq_if_roo [UpwardEnumerable α] [LT α] [DecidableLT α] #[] := by rw [Internal.toArray_eq_toArray_iter, Rxo.Iterator.toArray_eq_match]; rfl -theorem toList_eq_if_rco [UpwardEnumerable α] [LT α] [DecidableLT α] +set_option backward.isDefEq.respectTransparency.types false in +public theorem toList_eq_if_rco [UpwardEnumerable α] [LT α] [DecidableLT α] [LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerableLT α] : r.toList = if r.lower < r.upper then match UpwardEnumerable.succ? r.lower with @@ -889,7 +890,8 @@ theorem toList_eq_if_rco [UpwardEnumerable α] [LT α] [DecidableLT α] rfl · rfl -theorem toArray_eq_if_rco [UpwardEnumerable α] [LT α] [DecidableLT α] +set_option backward.isDefEq.respectTransparency.types false in +public theorem toArray_eq_if_rco [UpwardEnumerable α] [LT α] [DecidableLT α] [LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerableLT α] : r.toArray = if r.lower < r.upper then match UpwardEnumerable.succ? r.lower with @@ -1317,7 +1319,8 @@ namespace Roc variable {r : Roc α} -theorem toList_eq_match [LE α] [DecidableLE α] [UpwardEnumerable α] +set_option backward.isDefEq.respectTransparency.types false in +public theorem toList_eq_match [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : r.toList = match UpwardEnumerable.succ? r.lower with | none => [] @@ -1329,7 +1332,8 @@ theorem toList_eq_match [LE α] [DecidableLE α] [UpwardEnumerable α] rw [Internal.toList_eq_toList_iter, Rxc.Iterator.toList_eq_match (it := Internal.iter r)] simp [Internal.iter, Internal.toList_eq_toList_iter] -theorem toArray_eq_match [LE α] [DecidableLE α] [UpwardEnumerable α] +set_option backward.isDefEq.respectTransparency.types false in +public theorem toArray_eq_match [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : r.toArray = match UpwardEnumerable.succ? r.lower with | none => #[] @@ -1585,6 +1589,7 @@ theorem toArray_eq_match [LE α] [LT α] [DecidableLT α] [UpwardEnumerable α] #[] := by rw [Internal.toArray_eq_toArray_iter, Rxo.Iterator.toArray_eq_match]; rfl +set_option backward.isDefEq.respectTransparency.types false in @[cbv_eval] theorem toList_eq_match_rco [UpwardEnumerable α] [LT α] [DecidableLT α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] : @@ -1597,7 +1602,8 @@ theorem toList_eq_match_rco [UpwardEnumerable α] [LT α] [DecidableLT α] · rfl · simp [Rco.toList_eq_if_roo, Roo.toList, Internal.iter] -theorem toArray_eq_match_rco [UpwardEnumerable α] [LT α] [DecidableLT α] +set_option backward.isDefEq.respectTransparency.types false in +public theorem toArray_eq_match_rco [UpwardEnumerable α] [LT α] [DecidableLT α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] : r.toArray = match UpwardEnumerable.succ? r.lower with | none => #[] @@ -2055,6 +2061,7 @@ theorem toList_toArray [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α r.toArray.toList = r.toList := by simp [Internal.toList_eq_toList_iter, Internal.toArray_eq_toArray_iter] +set_option backward.isDefEq.respectTransparency.types false in @[cbv_eval] theorem toList_eq_match_rcc [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] @@ -2358,6 +2365,7 @@ theorem toList_toArray [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α r.toArray.toList = r.toList := by simp [Internal.toList_eq_toList_iter, Internal.toArray_eq_toArray_iter] +set_option backward.isDefEq.respectTransparency.types false in @[cbv_eval] theorem toList_eq_match_rco [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] @@ -2370,7 +2378,8 @@ theorem toList_eq_match_rco [LT α] [DecidableLT α] [Least? α] [UpwardEnumerab Rxo.Iterator.toList_eq_match (it := Rco.Internal.iter _)] simp [Internal.iter, Rco.Internal.iter] -theorem toArray_eq_match_rco [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α] +set_option backward.isDefEq.respectTransparency.types false in +public theorem toArray_eq_match_rco [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] : r.toArray = match Least?.least? (α := α) with diff --git a/src/Init/Data/Range/Polymorphic/RangeIterator.lean b/src/Init/Data/Range/Polymorphic/RangeIterator.lean index 94f4c951d574..8f87eec5f970 100644 --- a/src/Init/Data/Range/Polymorphic/RangeIterator.lean +++ b/src/Init/Data/Range/Polymorphic/RangeIterator.lean @@ -80,6 +80,7 @@ def Iterator.step [UpwardEnumerable α] [LE α] [DecidableLE α] else .done +set_option backward.isDefEq.respectTransparency.types false in theorem Iterator.step_eq_monadicStep [UpwardEnumerable α] [LE α] [DecidableLE α] {it : Iter (α := Rxc.Iterator α) α} : Iterator.step it = (Iterator.Monadic.step it.toIterM).mapIterator IterM.toIter := by @@ -660,6 +661,7 @@ def Iterator.step [UpwardEnumerable α] [LT α] [DecidableLT α] else .done +set_option backward.isDefEq.respectTransparency.types false in theorem Iterator.step_eq_monadicStep [UpwardEnumerable α] [LT α] [DecidableLT α] {it : Iter (α := Rxo.Iterator α) α} : Iterator.step it = (Iterator.Monadic.step it.toIterM).mapIterator IterM.toIter := by diff --git a/src/Init/Data/Rat/Lemmas.lean b/src/Init/Data/Rat/Lemmas.lean index c31acd531937..90eb3e09a3fa 100644 --- a/src/Init/Data/Rat/Lemmas.lean +++ b/src/Init/Data/Rat/Lemmas.lean @@ -1242,6 +1242,7 @@ theorem lt_floor {x : Rat} : # ceil -/ +set_option backward.isDefEq.respectTransparency.types false in theorem ceil_eq_neg_floor_neg (a : Rat) : a.ceil = -((-a).floor) := by rw [Rat.ceil, Rat.floor] simp only [neg_den, neg_num] diff --git a/src/Init/Data/SInt/Lemmas.lean b/src/Init/Data/SInt/Lemmas.lean index 9bac38deecd2..cb2d4df8fbb2 100644 --- a/src/Init/Data/SInt/Lemmas.lean +++ b/src/Init/Data/SInt/Lemmas.lean @@ -1162,12 +1162,15 @@ theorem ISize.toInt8_ofIntLE {n} (h₁ h₂) : (ISize.ofIntLE n h₁ h₂).toInt @[simp] theorem Int64.toInt8_ofNat {n} : toInt8 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt8_ofNat' @[simp] theorem ISize.toInt8_ofNat {n} : toInt8 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt8_ofNat' +set_option backward.isDefEq.respectTransparency.types false in theorem Int16.toInt8_ofIntClamp {n : Int} (h₁ : -2 ^ 15 ≤ n) (h₂ : n < 2 ^ 15) : (Int16.ofIntClamp n).toInt8 = Int8.ofInt n := by rw [← ofIntLE_eq_ofIntClamp (h₁ := h₁) (h₂ := Int.le_of_lt_add_one h₂), toInt8_ofIntLE] +set_option backward.isDefEq.respectTransparency.types false in theorem Int32.toInt8_ofIntClamp {n : Int} (h₁ : -2 ^ 31 ≤ n) (h₂ : n < 2 ^ 31) : (Int32.ofIntClamp n).toInt8 = Int8.ofInt n := by rw [← ofIntLE_eq_ofIntClamp (h₁ := h₁) (h₂ := Int.le_of_lt_add_one h₂), toInt8_ofIntLE] +set_option backward.isDefEq.respectTransparency.types false in theorem Int64.toInt8_ofIntClamp {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) : (Int64.ofIntClamp n).toInt8 = Int8.ofInt n := by rw [← ofIntLE_eq_ofIntClamp (h₁ := h₁) (h₂ := Int.le_of_lt_add_one h₂), toInt8_ofIntLE] @@ -1209,9 +1212,11 @@ theorem ISize.toInt16_ofIntLE {n} (h₁ h₂) : (ISize.ofIntLE n h₁ h₂).toIn @[simp] theorem Int64.toInt16_ofNat {n} : toInt16 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt16_ofNat' @[simp] theorem ISize.toInt16_ofNat {n} : toInt16 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt16_ofNat' +set_option backward.isDefEq.respectTransparency.types false in theorem Int32.toInt16_ofIntClamp {n : Int} (h₁ : -2 ^ 31 ≤ n) (h₂ : n < 2 ^ 31) : (Int32.ofIntClamp n).toInt16 = Int16.ofInt n := by rw [← ofIntLE_eq_ofIntClamp (h₁ := h₁) (h₂ := Int.le_of_lt_add_one h₂), toInt16_ofIntLE] +set_option backward.isDefEq.respectTransparency.types false in theorem Int64.toInt16_ofIntClamp {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) : (Int64.ofIntClamp n).toInt16 = Int16.ofInt n := by rw [← ofIntLE_eq_ofIntClamp (h₁ := h₁) (h₂ := Int.le_of_lt_add_one h₂), toInt16_ofIntLE] @@ -1246,6 +1251,7 @@ theorem ISize.toInt32_ofIntLE {n} (h₁ h₂) : (ISize.ofIntLE n h₁ h₂).toIn @[simp] theorem Int64.toInt32_ofNat {n} : toInt32 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt32_ofNat' @[simp] theorem ISize.toInt32_ofNat {n} : toInt32 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt32_ofNat' +set_option backward.isDefEq.respectTransparency.types false in theorem Int64.toInt32_ofIntClamp {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) : (Int64.ofIntClamp n).toInt32 = Int32.ofInt n := by rw [← ofIntLE_eq_ofIntClamp (h₁ := h₁) (h₂ := Int.le_of_lt_add_one h₂), toInt32_ofIntLE] @@ -1269,6 +1275,7 @@ theorem Int64.toISize_ofIntLE {n} (h₁ h₂) : (Int64.ofIntLE n h₁ h₂).toIS @[simp] theorem Int64.toISize_ofNat {n} : toISize (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toISize_ofNat' +set_option backward.isDefEq.respectTransparency.types false in theorem Int64.toISize_ofIntClamp {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) : (Int64.ofIntClamp n).toISize = ISize.ofInt n := by rw [← ofIntLE_eq_ofIntClamp (h₁ := h₁) (h₂ := Int.le_of_lt_add_one h₂), toISize_ofIntLE] diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index d57fc023958c..f0089b5f37eb 100644 --- a/src/Init/Data/String/Basic.lean +++ b/src/Init/Data/String/Basic.lean @@ -513,6 +513,7 @@ theorem Pos.Raw.IsValid.isValidUTF8_extract_utf8ByteSize {s : String} {p : Pos.R simpa [utf8ByteSize, Pos.Raw.le_iff] using h.le_rawEndPos · simp [utf8ByteSize] +set_option backward.isDefEq.respectTransparency.types false in theorem Pos.Raw.isValid_iff_exists_append {s : String} {p : Pos.Raw} : p.IsValid s ↔ ∃ s₁ s₂ : String, s = s₁ ++ s₂ ∧ p = s₁.rawEndPos := by refine ⟨fun h => ⟨⟨_, h.isValidUTF8_extract_zero⟩, ⟨_, h.isValidUTF8_extract_utf8ByteSize⟩, ?_, ?_⟩, ?_⟩ @@ -647,6 +648,7 @@ where rw [List.reverse_cons] exact append_singleton _ _ ih +set_option backward.isDefEq.respectTransparency.types false in theorem Pos.Raw.isValid_iff_isUTF8FirstByte {s : String} {p : Pos.Raw} : p.IsValid s ↔ p = s.rawEndPos ∨ ∃ (h : p < s.rawEndPos), (s.getUTF8Byte p h).IsUTF8FirstByte := by induction s using push_induction with @@ -1035,7 +1037,7 @@ theorem Slice.Pos.offset_ofStr {s : Slice} {pos : s.str.Pos} {h₁ h₂} : /-- Given a slice and a valid position within the slice, obtain a new slice on the same underlying string by replacing the start of the slice with the given position. -/ -@[inline, expose] -- for the defeq `(s.sliceFrom pos).str = s.str` +@[inline, expose, implicit_reducible] -- for the defeq `(s.sliceFrom pos).str = s.str` def Slice.sliceFrom (s : Slice) (pos : s.Pos) : Slice where str := s.str startInclusive := pos.str @@ -1060,7 +1062,7 @@ theorem Slice.endExclusive_sliceFrom {s : Slice} {pos : s.Pos} : /-- Given a slice and a valid position within the slice, obtain a new slice on the same underlying string by replacing the end of the slice with the given position. -/ -@[inline, expose] -- for the defeq `(s.sliceTo pos).str = s.str` +@[inline, expose, implicit_reducible] -- for the defeq `(s.sliceTo pos).str = s.str` def Slice.sliceTo (s : Slice) (pos : s.Pos) : Slice where str := s.str startInclusive := s.startInclusive @@ -1085,7 +1087,7 @@ theorem Slice.endExclusive_sliceTo {s : Slice} {pos : s.Pos} : /-- Given a slice and two valid positions within the slice, obtain a new slice on the same underlying string formed by the new bounds. -/ -@[inline, expose] -- for the defeq `(s.slice newStart newEnd).str = s.str` +@[inline, expose, implicit_reducible] -- for the defeq `(s.slice newStart newEnd).str = s.str` def Slice.slice (s : Slice) (newStart newEnd : s.Pos) (h : newStart ≤ newEnd) : Slice where str := s.str @@ -1224,7 +1226,7 @@ theorem Pos.Raw.IsValidForSlice.ofSlice {s : String} {p : Pos.Raw} (h : p.IsVali isValidForSlice_toSlice_iff.1 h /-- Turns a valid position on the string `s` into a valid position on the slice `s.toSlice`. -/ -@[inline, expose] +@[inline, expose, implicit_reducible] def Pos.toSlice {s : String} (pos : s.Pos) : s.toSlice.Pos where offset := pos.offset isValidForSlice := pos.isValid.toSlice @@ -2166,7 +2168,7 @@ theorem Slice.Pos.next_eq_nextFast : @Slice.Pos.next = @Slice.Pos.nextFast := by omega /-- The slice from the beginning of `s` up to `p` (exclusive). -/ -@[inline, expose] +@[inline, expose, implicit_reducible] def sliceTo (s : String) (p : s.Pos) : Slice := s.toSlice.sliceTo p.toSlice @@ -2197,7 +2199,7 @@ theorem Pos.Raw.isValidForSlice_stringSliceTo {s : String} {p : s.Pos} {q : Pos. rw [sliceTo, isValidForSlice_sliceTo, Pos.offset_toSlice, isValidForSlice_toSlice_iff] /-- The slice from `p` (inclusive) up to the end of `s`. -/ -@[inline, expose] +@[inline, expose, implicit_reducible] def sliceFrom (s : String) (p : s.Pos) : Slice := s.toSlice.sliceFrom p.toSlice @@ -2251,7 +2253,7 @@ the two positions. This happens to be equivalent to the constructor of `String.Slice`. -/ -@[inline, expose] -- For the defeq `(s.slice p₁ p₂).str = s` +@[inline, expose, implicit_reducible] -- For the defeq `(s.slice p₁ p₂).str = s` def slice (s : String) (startInclusive endExclusive : s.Pos) (h : startInclusive ≤ endExclusive) : String.Slice := s.toSlice.slice startInclusive.toSlice endExclusive.toSlice (by simpa) @@ -2520,6 +2522,7 @@ theorem Pos.Raw.isValidForSlice_slice {s : Slice} {p₀ p₁ : s.Pos} {h} (pos : omega · simpa [offsetBy_assoc] using h₂.isValid_offsetBy +set_option backward.isDefEq.respectTransparency.types false in theorem Pos.Raw.isValidForSlice_stringSlice {s : String} {p₀ p₁ : s.Pos} {h} (pos : Pos.Raw) : pos.IsValidForSlice (s.slice p₀ p₁ h) ↔ pos.offsetBy p₀.offset ≤ p₁.offset ∧ (pos.offsetBy p₀.offset).IsValid s := by diff --git a/src/Init/Data/String/Defs.lean b/src/Init/Data/String/Defs.lean index b9d5fa5acbf7..59331178afcf 100644 --- a/src/Init/Data/String/Defs.lean +++ b/src/Init/Data/String/Defs.lean @@ -422,7 +422,7 @@ instance : Inhabited Slice where /-- Returns a slice that contains the entire string. -/ -@[inline, expose] -- expose for the defeq `s.toSlice.str = s`. +@[inline, expose, implicit_reducible] -- expose for the defeq `s.toSlice.str = s`. def toSlice (s : String) : Slice where str := s startInclusive := s.startPos diff --git a/src/Init/Data/String/Lemmas/Iterate.lean b/src/Init/Data/String/Lemmas/Iterate.lean index 32bd888af7d5..4f417f8b208d 100644 --- a/src/Init/Data/String/Lemmas/Iterate.lean +++ b/src/Init/Data/String/Lemmas/Iterate.lean @@ -76,6 +76,7 @@ theorem Model.map_get_positionsFrom_startPos {s : Slice} : (Model.positionsFrom s.startPos).map (fun p => p.1.get p.2) = s.copy.toList := Model.map_get_positionsFrom_of_splits (splits_startPos s) +set_option backward.isDefEq.respectTransparency.types false in @[cbv_eval, simp] theorem toList_positionsFrom {s : Slice} {p : s.Pos} : (s.positionsFrom p).toList = Model.positionsFrom p := by @@ -162,6 +163,7 @@ theorem Model.map_get_revPositionsFrom_endPos {s : Slice} : (Model.revPositionsFrom s.endPos).map (fun p => p.1.get p.2) = s.copy.toList.reverse := Model.map_get_revPositionsFrom_of_splits (splits_endPos s) +set_option backward.isDefEq.respectTransparency.types false in @[simp] theorem toList_revPositionsFrom {s : Slice} {p : s.Pos} : (s.revPositionsFrom p).toList = Model.revPositionsFrom p := by diff --git a/src/Init/Data/String/Lemmas/Pattern/Basic.lean b/src/Init/Data/String/Lemmas/Pattern/Basic.lean index 956269e15f36..dff493ee4cd8 100644 --- a/src/Init/Data/String/Lemmas/Pattern/Basic.lean +++ b/src/Init/Data/String/Lemmas/Pattern/Basic.lean @@ -913,6 +913,7 @@ class LawfulToForwardSearcherModel {ρ : Type} (pat : ρ) [PatternModel pat] {σ [∀ 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.types false in theorem LawfulToForwardSearcherModel.defaultImplementation {pat : ρ} [ForwardPattern pat] [StrictForwardPattern pat] [PatternModel pat] [LawfulForwardPatternModel pat] : letI : ToForwardSearcher pat (ToForwardSearcher.DefaultForwardSearcher pat) := .defaultImplementation @@ -1024,6 +1025,7 @@ class LawfulToBackwardSearcherModel {ρ : Type} (pat : ρ) [PatternModel pat] { [∀ s, Std.Iterators.Finite (σ s) Id] : Prop where isValidRevSearchFrom_toList (s) : IsValidRevSearchFrom pat s.endPos (ToBackwardSearcher.toSearcher pat s).toList +set_option backward.isDefEq.respectTransparency.types false in theorem LawfulToBackwardSearcherModel.defaultImplementation {pat : ρ} [BackwardPattern pat] [StrictBackwardPattern pat] [PatternModel pat] [LawfulBackwardPatternModel pat] : letI : ToBackwardSearcher pat (ToBackwardSearcher.DefaultBackwardSearcher pat) := .defaultImplementation diff --git a/src/Init/Data/String/Lemmas/Pattern/String/ForwardSearcher.lean b/src/Init/Data/String/Lemmas/Pattern/String/ForwardSearcher.lean index 50d1d1d85210..1ebbf8bc39ac 100644 --- a/src/Init/Data/String/Lemmas/Pattern/String/ForwardSearcher.lean +++ b/src/Init/Data/String/Lemmas/Pattern/String/ForwardSearcher.lean @@ -319,6 +319,7 @@ theorem computeDistance_eq_prefixFunctionRecurrence {s : Slice} (i : Nat) · simp only [ht'.eq_prefixFunction, ih] · simp [getUTF8Byte_eq_getUTF8Byte_copy, String.getUTF8Byte, *] +set_option backward.isDefEq.respectTransparency.types false in theorem isTable_buildTableGo {pat : Slice} {table : Array Nat} {ht₀ ht h} (ht' : IsTable pat.copy.toByteArray table) : IsTable pat.copy.toByteArray (buildTable.go pat table ht₀ ht h).1 := by diff --git a/src/Init/Data/Vector/Attach.lean b/src/Init/Data/Vector/Attach.lean index ce98f61e8cf5..2ece137f6c4c 100644 --- a/src/Init/Data/Vector/Attach.lean +++ b/src/Init/Data/Vector/Attach.lean @@ -139,6 +139,7 @@ theorem attachWith_congr {xs ys : Vector α n} (w : xs = ys) {P : α → Prop} { subst w simp +set_option backward.isDefEq.respectTransparency.types false in @[simp] theorem attach_push {a : α} {xs : Vector α n} : (xs.push a).attach = (xs.attach.map (fun ⟨x, h⟩ => ⟨x, mem_push_of_mem a h⟩)).push ⟨a, by simp⟩ := by @@ -354,6 +355,7 @@ theorem pmap_append' {p : α → Prop} {f : ∀ a : α, p a → β} {xs : Vector xs.pmap f h₁ ++ ys.pmap f h₂ := pmap_append _ +set_option backward.isDefEq.respectTransparency.types false in @[simp] theorem attach_append {xs : Vector α n} {ys : Vector α m} : (xs ++ ys).attach = xs.attach.map (fun ⟨x, h⟩ => (⟨x, mem_append_left ys h⟩ : { x // x ∈ xs ++ ys })) ++ ys.attach.map (fun ⟨y, h⟩ => (⟨y, mem_append_right xs h⟩ : { y // y ∈ xs ++ ys })) := by diff --git a/src/Init/Data/Vector/DecidableEq.lean b/src/Init/Data/Vector/DecidableEq.lean index 8e78e9f7e52f..7525ad8f84f2 100644 --- a/src/Init/Data/Vector/DecidableEq.lean +++ b/src/Init/Data/Vector/DecidableEq.lean @@ -22,6 +22,7 @@ theorem isEqv_iff_rel {xs ys : Vector α n} {r} : rcases ys with ⟨ys, h⟩ simp [Array.isEqv_iff_rel, h] +set_option backward.isDefEq.respectTransparency.types false in theorem isEqv_eq_decide (xs ys : Vector α n) (r) : Vector.isEqv xs ys r = decide (∀ (i : Nat) (h' : i < n), r xs[i] ys[i]) := by rcases xs with ⟨xs, rfl⟩ diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index ef332ffea50c..7daf0c49d39c 100644 --- a/src/Init/Data/Vector/Lemmas.lean +++ b/src/Init/Data/Vector/Lemmas.lean @@ -706,11 +706,13 @@ theorem toList_zip {as : Vector α n} {bs : Vector β n} : cases xs simp +set_option backward.isDefEq.respectTransparency.types false in @[simp] theorem finIdxOf?_toList [BEq α] {a : α} {xs : Vector α n} : xs.toList.finIdxOf? a = (xs.finIdxOf? a).map (Fin.cast (by exact xs.size_toArray.symm)) := by rcases xs with ⟨xs, rfl⟩ simp +set_option backward.isDefEq.respectTransparency.types false in @[simp] theorem findFinIdx?_toList {p : α → Bool} {xs : Vector α n} : xs.toList.findFinIdx? p = (xs.findFinIdx? p).map (Fin.cast (by exact xs.size_toArray.symm)) := by rcases xs with ⟨xs, rfl⟩ diff --git a/src/Init/Data/Vector/Monadic.lean b/src/Init/Data/Vector/Monadic.lean index 4f1e5f7e122d..dfa23ed96069 100644 --- a/src/Init/Data/Vector/Monadic.lean +++ b/src/Init/Data/Vector/Monadic.lean @@ -154,6 +154,7 @@ theorem idRun_forIn'_yield_eq_foldl xs.attach.foldl (fun b ⟨a, h⟩ => f a h b |>.run) init := by simp +set_option backward.isDefEq.respectTransparency.types false in @[simp, grind =] theorem forIn'_map [Monad m] [LawfulMonad m] {xs : Vector α n} (g : α → β) (f : (b : β) → b ∈ xs.map g → γ → m (ForInStep γ)) : forIn' (xs.map g) init f = forIn' xs init fun a h y => f (g a) (mem_map_of_mem h) y := by diff --git a/src/Init/GetElem.lean b/src/Init/GetElem.lean index 7d6300b1d5fe..8e28f99f50fc 100644 --- a/src/Init/GetElem.lean +++ b/src/Init/GetElem.lean @@ -408,7 +408,7 @@ instance : LawfulGetElem (Array α) Nat α fun xs i => i < xs.size where split <;> rfl @[simp] theorem getInternal_eq_getElem (a : Array α) (i : Nat) (h) : - a.getInternal i h = a[i] := rfl + a.getInternal i h = a[i] := id rfl @[simp] theorem get!Internal_eq_getElem! [Inhabited α] (a : Array α) (i : Nat) : a.get!Internal i = a[i]! := by diff --git a/src/Init/Grind/Module/Envelope.lean b/src/Init/Grind/Module/Envelope.lean index 1c88171701e6..8494966fcdda 100644 --- a/src/Init/Grind/Module/Envelope.lean +++ b/src/Init/Grind/Module/Envelope.lean @@ -32,7 +32,7 @@ local instance : Std.Commutative (· + · : α → α → α) where @[local simp] def r : (α × α) → (α × α) → Prop | (a, b), (c, d) => ∃ k, a + d + k = b + c + k -def Q := Quot (r α) +@[expose, implicit_reducible] def Q := Quot (r α) variable {α} diff --git a/src/Init/Grind/Ring/Envelope.lean b/src/Init/Grind/Ring/Envelope.lean index bb22f3f5614c..3840029ffd47 100644 --- a/src/Init/Grind/Ring/Envelope.lean +++ b/src/Init/Grind/Ring/Envelope.lean @@ -35,6 +35,7 @@ local instance : Std.Associative (· * · : α → α → α) where @[local simp] def r : (α × α) → (α × α) → Prop | (a, b), (c, d) => ∃ k, a + d + k = b + c + k +@[implicit_reducible] def Q := Quot (r α) variable {α} diff --git a/src/Init/Internal/Order/Basic.lean b/src/Init/Internal/Order/Basic.lean index 10e5888e1e43..1f50a87e767f 100644 --- a/src/Init/Internal/Order/Basic.lean +++ b/src/Init/Internal/Order/Basic.lean @@ -795,6 +795,7 @@ noncomputable def flat_csup (c : FlatOrder b → Prop) : FlatOrder b := by · exact Classical.choose h · exact b +set_option backward.isDefEq.respectTransparency.types false in theorem flat_csup_is_sup (c : FlatOrder b → Prop) (hc : chain c) : is_sup c (flat_csup c) := by intro x diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 9ed192846b92..61efc793890a 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -128,7 +128,7 @@ difference for typeclass inference, since `T` and `T'` may have different typeclass instances on them. `show T' from e` is sugar for an `@id T' e` expression. -/ -@[inline] def id {α : Sort u} (a : α) : α := a +@[inline, implicit_reducible] def id {α : Sort u} (a : α) : α := a /-- Function composition, usually written with the infix operator `∘`. A new function is created from @@ -138,7 +138,7 @@ Examples: * `Function.comp List.reverse (List.drop 2) [3, 2, 4, 1] = [1, 4]` * `(List.reverse ∘ List.drop 2) [3, 2, 4, 1] = [1, 4]` -/ -@[inline] def Function.comp {α : Sort u} {β : Sort v} {δ : Sort w} (f : β → δ) (g : α → β) : α → δ := +@[inline, implicit_reducible] def Function.comp {α : Sort u} {β : Sort v} {δ : Sort w} (f : β → δ) (g : α → β) : α → δ := fun x => f (g x) /-- @@ -314,7 +314,7 @@ so if your goal is `¬p` you can use `intro h` to turn the goal into and `(hn h).elim` will prove anything. For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic) -/ -def Not (a : Prop) : Prop := a → False +@[implicit_reducible] def Not (a : Prop) : Prop := a → False /-- `False.elim : False → C` says that from `False`, any desired proposition @@ -407,7 +407,7 @@ definitionally sometimes there isn't anything better you can do. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) -/ -@[macro_inline] def cast {α β : Sort u} (h : Eq α β) (a : α) : β := +@[macro_inline, implicit_reducible] def cast {α β : Sort u} (h : Eq α β) (a : α) : β := h.rec a /-- @@ -1157,7 +1157,7 @@ Just like `ite`, `cond` is declared `@[macro_inline]`, which causes applications unfolded. As a result, `x` and `y` are not evaluated at runtime until one of them is selected, and only the selected branch is evaluated. -/ -@[macro_inline] def cond {α : Sort u} (c : Bool) (x y : α) : α := +@[macro_inline, implicit_reducible] def cond {α : Sort u} (c : Bool) (x y : α) : α := match c with | true => x | false => y @@ -1895,7 +1895,7 @@ Strict inequality of natural numbers, usually accessed via the `<` operator. It is defined as `n < m = n + 1 ≤ m`. -/ -protected def Nat.lt (n m : Nat) : Prop := +@[implicit_reducible] protected def Nat.lt (n m : Nat) : Prop := Nat.le (succ n) m instance instLTNat : LT Nat where @@ -1954,7 +1954,7 @@ The predecessor of a natural number is one less than it. The predecessor of `0` This definition is overridden in the compiler with an efficient implementation. This definition is the logical model. -/ -@[extern "lean_nat_pred"] +@[extern "lean_nat_pred", implicit_reducible] def Nat.pred : (@& Nat) → Nat | 0 => 0 | succ a => a @@ -2923,7 +2923,7 @@ Examples: * `(some "hello").getD "goodbye" = "hello"` * `none.getD "goodbye" = "goodbye"` -/ -@[macro_inline] def Option.getD (opt : Option α) (dflt : α) : α := +@[macro_inline, implicit_reducible] def Option.getD (opt : Option α) (dflt : α) : α := match opt with | some x => x | none => dflt @@ -2938,7 +2938,7 @@ Examples: * `(none : Option Nat).map (· + 1) = none` * `(some 3).map (· + 1) = some 4` -/ -@[inline] protected def Option.map (f : α → β) : Option α → Option β +@[inline, implicit_reducible] protected def Option.map (f : α → β) : Option α → Option β | some x => some (f x) | none => none @@ -3055,6 +3055,7 @@ Examples: * `["spring", "summer", "fall", "winter"].get (2 : Fin 4) = "fall"` * `["spring", "summer", "fall", "winter"].get (0 : Fin 4) = "spring"` -/ +@[implicit_reducible] def List.get {α : Type u} : (as : List α) → Fin as.length → α | cons a _, ⟨0, _⟩ => a | cons _ as, ⟨Nat.succ i, h⟩ => get as ⟨i, Nat.le_of_succ_le_succ h⟩ @@ -3256,7 +3257,7 @@ This function does not use `get_elem_tactic` to automatically find the proof tha the index is in bounds. This is because the tactic itself needs to look up values in arrays. -/ -@[extern "lean_array_fget"] +@[extern "lean_array_fget", implicit_reducible] def Array.getInternal {α : Type u} (a : @& Array α) (i : @& Nat) (h : LT.lt i a.size) : α := a.toList.get ⟨i, h⟩ @@ -3441,7 +3442,7 @@ Returns the number of bytes in the byte array. This is the number of bytes actually in the array, as distinct from its capacity, which is the amount of memory presently allocated for the array. -/ -@[extern "lean_byte_array_size", tagged_return] +@[extern "lean_byte_array_size", tagged_return, implicit_reducible] def ByteArray.size : (@& ByteArray) → Nat | ⟨bs⟩ => bs.size @@ -3600,7 +3601,7 @@ The number of bytes used by the string's UTF-8 encoding. At runtime, this function takes constant time because the byte length of strings is cached. -/ -@[extern "lean_string_utf8_byte_size", tagged_return] +@[extern "lean_string_utf8_byte_size", tagged_return, implicit_reducible] def String.utf8ByteSize (s : @& String) : Nat := s.toByteArray.size @@ -3610,7 +3611,7 @@ A UTF-8 byte position that points at the end of a string, just after the last ch * `"abc".rawEndPos = ⟨3⟩` * `"L∃∀N".rawEndPos = ⟨8⟩` -/ -@[inline] def String.rawEndPos (s : String) : String.Pos.Raw where +@[inline, implicit_reducible] def String.rawEndPos (s : String) : String.Pos.Raw where byteIdx := utf8ByteSize s /-- @@ -4101,7 +4102,7 @@ overridden by `withReader`, but it cannot be mutated. Actions in the resulting monad are functions that take the local value as a parameter, returning ordinary actions in `m`. -/ -def ReaderT (ρ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) := +@[implicit_reducible] def ReaderT (ρ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) := (a : @&ρ) → m α /-- @@ -5025,7 +5026,7 @@ def Syntax.node8 (info : SourceInfo) (kind : SyntaxNodeKind) (a₁ a₂ a₃ a Singleton `SyntaxNodeKinds` are extremely common. They are written as name literals, rather than as lists; list syntax is required only for empty or non-singleton sets of kinds. -/ -@[expose] def SyntaxNodeKinds := List SyntaxNodeKind +@[expose, implicit_reducible] def SyntaxNodeKinds := List SyntaxNodeKind /-- Typed syntax, which tracks the potential kinds of the `Syntax` it contains. diff --git a/src/Init/WF.lean b/src/Init/WF.lean index 6225c703fef3..28a731b48d0f 100644 --- a/src/Init/WF.lean +++ b/src/Init/WF.lean @@ -519,7 +519,7 @@ The `wfParam` gadget is used internally during the construction of recursive fun wellfounded recursion, to keep track of the parameter for which the automatic introduction of `List.attach` (or similar) is plausible. -/ -def wfParam {α : Sort u} (a : α) : α := a +@[implicit_reducible] def wfParam {α : Sort u} (a : α) : α := a /-- Reverse direction of `dite_eq_ite`. Used by the well-founded definition preprocessor to extend the diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index 43bf97a60cb1..ee5e2ecf292f 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -53,7 +53,7 @@ Controls the transparency used to check whether the type of metavariable matches term being assigned to it. -/ register_builtin_option backward.isDefEq.respectTransparency.types : Bool := { - defValue := false -- TODO: replace with `true` after we fix stage0 + defValue := true descr := "if true, do not bump transparency to `.default` \ when checking whether the type of a metavariable matches the type of the term being assigned to it." } diff --git a/src/Std/Data/DHashMap/Internal/Model.lean b/src/Std/Data/DHashMap/Internal/Model.lean index 5739c4b108b6..7baae63d5be6 100644 --- a/src/Std/Data/DHashMap/Internal/Model.lean +++ b/src/Std/Data/DHashMap/Internal/Model.lean @@ -526,6 +526,7 @@ theorem getKey!_eq_getKey!ₘ [BEq α] [Hashable α] [Inhabited α] (m : Raw₀ theorem contains_eq_containsₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) : m.contains a = m.containsₘ a := (rfl) +set_option backward.isDefEq.respectTransparency.types false in theorem insert_eq_insertₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (b : β a) : m.insert a b = m.insertₘ a b := by rw [insert, insertₘ, containsₘ, bucket] @@ -536,6 +537,7 @@ theorem insert_eq_insertₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) ( simp only [Array.uset, Array.ugetElem_eq_getElem] · rfl +set_option backward.isDefEq.respectTransparency.types false in theorem alter_eq_alterₘ [BEq α] [Hashable α] [LawfulBEq α] (m : Raw₀ α β) (a : α) (f : Option (β a) → Option (β a)) : m.alter a f = m.alterₘ a f := by simp only [alter, alterₘ, containsₘ, ← bucket_eq] @@ -566,6 +568,7 @@ namespace Const variable {β : Type v} +set_option backward.isDefEq.respectTransparency.types false in theorem alter_eq_alterₘ [BEq α] [Hashable α] [EquivBEq α] (m : Raw₀ α (fun _ => β)) (a : α) (f : Option β → Option β) : Const.alter m a f = Const.alterₘ m a f := by simp only [alter, alterₘ, containsₘ, ← bucket_eq] @@ -594,6 +597,7 @@ theorem modify_eq_modifyₘ [BEq α] [Hashable α] [EquivBEq α] (m : Raw₀ α end Const +set_option backward.isDefEq.respectTransparency.types false in theorem containsThenInsert_eq_insertₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (b : β a) : (m.containsThenInsert a b).2 = m.insertₘ a b := by rw [containsThenInsert, insertₘ, containsₘ, bucket] @@ -610,6 +614,7 @@ theorem containsThenInsert_eq_containsₘ [BEq α] [Hashable α] (m : Raw₀ α dsimp only [Array.ugetElem_eq_getElem, Array.uset] split <;> simp_all +set_option backward.isDefEq.respectTransparency.types false in theorem containsThenInsertIfNew_eq_insertIfNewₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (b : β a) : (m.containsThenInsertIfNew a b).2 = m.insertIfNewₘ a b := by rw [containsThenInsertIfNew, insertIfNewₘ, containsₘ, bucket] @@ -639,6 +644,7 @@ theorem getThenInsertIfNew?_eq_get?ₘ [BEq α] [Hashable α] [LawfulBEq α] (m dsimp only [Array.ugetElem_eq_getElem, Array.uset] split <;> simp_all +set_option backward.isDefEq.respectTransparency.types false in theorem erase_eq_eraseₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) : m.erase a = m.eraseₘ a := by rw [erase, eraseₘ, containsₘ, bucket] diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean index f4a940097c73..94648cfea7ff 100644 --- a/src/Std/Data/DHashMap/Internal/WF.lean +++ b/src/Std/Data/DHashMap/Internal/WF.lean @@ -457,11 +457,13 @@ theorem getEntry?ₘ_eq_getEntry? [BEq α] [PartialEquivBEq α] [Hashable α] [L m.getEntry?ₘ a = List.getEntry? a (toListModel m.1.buckets) := apply_bucket hm AssocList.getEntry?_eq getEntry?_of_perm getEntry?_append_of_containsKey_eq_false +set_option backward.isDefEq.respectTransparency.types false in theorem get_eq_getValueCast [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (hm : Raw.WFImp m.1) {a : α} {h : m.contains a} : m.get a h = getValueCast a (toListModel m.1.buckets) (contains_eq_containsKey hm ▸ h) := by rw [get_eq_getₘ, getₘ_eq_getValue hm] +set_option backward.isDefEq.respectTransparency.types false in theorem getEntry_eq_getEntry [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.1) {a : α} {h : m.contains a} : m.getEntry a h = List.getEntry a (toListModel m.1.buckets) (contains_eq_containsKey hm ▸ h) := by @@ -572,6 +574,7 @@ theorem Const.getₘ_eq_getValue [BEq α] [Hashable α] [PartialEquivBEq α] [La apply_bucket_with_proof hm a AssocList.get List.getValue AssocList.get_eq List.getValue_of_perm List.getValue_append_of_containsKey_eq_false +set_option backward.isDefEq.respectTransparency.types false in theorem Const.get_eq_getValue [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Raw₀ α (fun _ => β)} (hm : Raw.WFImp m.1) {a : α} {h} : Const.get m a h = getValue a (toListModel m.1.buckets) (contains_eq_containsKey hm ▸ h) := by diff --git a/src/Std/Data/DTreeMap/Internal/Balancing.lean b/src/Std/Data/DTreeMap/Internal/Balancing.lean index f665717ed3a8..1a6e66b408be 100644 --- a/src/Std/Data/DTreeMap/Internal/Balancing.lean +++ b/src/Std/Data/DTreeMap/Internal/Balancing.lean @@ -534,6 +534,7 @@ def balanceₘ (k : α) (v : β k) (l r : Impl α β) : Impl α β := attribute [Std.Internal.tree_tac] and_true true_and and_self heq_eq_eq inner.injEq +set_option backward.isDefEq.respectTransparency.types false in theorem balance!_eq_balanceₘ {k v} {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced) (hlr : BalanceLErasePrecond l.size r.size ∨ BalanceLErasePrecond r.size l.size) : balance! k v l r = balanceₘ k v l r := by diff --git a/src/Std/Data/DTreeMap/Internal/Model.lean b/src/Std/Data/DTreeMap/Internal/Model.lean index 804f9f0b245c..e81fadeff365 100644 --- a/src/Std/Data/DTreeMap/Internal/Model.lean +++ b/src/Std/Data/DTreeMap/Internal/Model.lean @@ -1002,6 +1002,7 @@ def getEntryGT?ₘ' [Ord α] (k : α) (t : Impl α β) : Option ((a : α) × β | base, .eq _ _ r => r.head?.or base | base, .gt _ _ _ _ => base +set_option backward.isDefEq.respectTransparency.types false in theorem getEntryGT?_eq_getEntryGT?ₘ' [Ord α] (k : α) (t : Impl α β) : getEntryGT? k t = getEntryGT?ₘ' k t := by rw [getEntryGT?ₘ', getEntryGT?] diff --git a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean index 97d1868af729..c1f8ed9b02bf 100644 --- a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean @@ -2032,6 +2032,7 @@ theorem WF.constAlter! {_ : Ord α} {β : Type v} {t : Impl α β} {a f} (h : t. ### mergeWith! -/ +set_option backward.isDefEq.respectTransparency.types false in theorem mergeWith_eq_mergeWith! {_ : Ord α} [LawfulEqOrd α] {mergeFn} {t₁ t₂ : Impl α β} (h : t₁.Balanced) : (mergeWith mergeFn t₁ t₂ h).impl = mergeWith! mergeFn t₁ t₂ := by @@ -2048,11 +2049,13 @@ theorem mergeWith_eq_mergeWith! {_ : Ord α} [LawfulEqOrd α] {mergeFn} {t₁ t congr exact ihl h +set_option backward.isDefEq.respectTransparency.types false in theorem WF.mergeWith! {_ : Ord α} [LawfulEqOrd α] {mergeFn} {t₁ t₂ : Impl α β} (h : t₁.WF) : (Impl.mergeWith! mergeFn t₁ t₂).WF := by rw [← mergeWith_eq_mergeWith! h.balanced] exact h.mergeWith +set_option backward.isDefEq.respectTransparency.types false in theorem Const.mergeWith_eq_mergeWith! {β : Type v} {_ : Ord α} {mergeFn} {t₁ t₂ : Impl α β} (h : t₁.Balanced) : (mergeWith mergeFn t₁ t₂ h).impl = mergeWith! mergeFn t₁ t₂ := by diff --git a/src/Std/Data/Internal/List/Associative.lean b/src/Std/Data/Internal/List/Associative.lean index 4c8f6673d1f3..a2618af7a502 100644 --- a/src/Std/Data/Internal/List/Associative.lean +++ b/src/Std/Data/Internal/List/Associative.lean @@ -8491,6 +8491,7 @@ theorem containsKey_minKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l obtain ⟨e, ⟨hm, _⟩, rfl⟩ := hkm exact containsKey_of_mem hm +set_option backward.isDefEq.respectTransparency.types false in theorem min?_keys [Ord α] [TransOrd α] [LawfulEqOrd α] [LE α] [LawfulOrderOrd α] [Min α] [LawfulOrderLeftLeaningMin α] (l : List ((a : α) × β a)) : diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean index 9c030f916e7f..50583aa1c80f 100644 --- a/src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean +++ b/src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean @@ -26,6 +26,7 @@ theorem Iter.drop_eq {α β} [Iterator α Id β] {n : Nat} it.drop n = (it.toIterM.drop n).toIter := rfl +set_option backward.isDefEq.respectTransparency.types false in theorem Iter.step_drop {α β} [Iterator α Id β] {n : Nat} {it : Iter (α := α) β} : (it.drop n).step = (match it.step with diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/DropWhile.lean b/src/Std/Data/Iterators/Lemmas/Combinators/DropWhile.lean index 4fbc5e4b0fdc..2b0f06b0f9f5 100644 --- a/src/Std/Data/Iterators/Lemmas/Combinators/DropWhile.lean +++ b/src/Std/Data/Iterators/Lemmas/Combinators/DropWhile.lean @@ -34,6 +34,7 @@ theorem Iter.dropWhile_eq_dropWhile_toIterM {α β} [Iterator α Id β] {P} it.dropWhile P = (it.toIterM.dropWhile P).toIter := rfl +set_option backward.isDefEq.respectTransparency.types false in theorem Iter.step_intermediateDropWhile {α β} [Iterator α Id β] {it : Iter (α := α) β} {P} {dropping} : (Iter.Intermediate.dropWhile P dropping it).step = (match it.step with diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean index 6cb54f7be75c..10d1a076e77d 100644 --- a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean +++ b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean @@ -14,6 +14,7 @@ public import Std.Data.Iterators.Lemmas.Equivalence.StepCongr namespace Std open Std.Internal Std.Iterators +set_option backward.isDefEq.respectTransparency.types false in theorem IterM.stepAsHetT_filterMapWithPostcondition [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Iterator α m β] [MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → PostconditionT n (Option γ)} {it : IterM (α := α) m β} : diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/TakeWhile.lean b/src/Std/Data/Iterators/Lemmas/Combinators/TakeWhile.lean index 19a969ad431c..0f7400a6c76f 100644 --- a/src/Std/Data/Iterators/Lemmas/Combinators/TakeWhile.lean +++ b/src/Std/Data/Iterators/Lemmas/Combinators/TakeWhile.lean @@ -24,6 +24,7 @@ theorem Iter.takeWhile_eq {α β} [Iterator α Id β] {P} it.takeWhile P = (it.toIterM.takeWhile P).toIter := rfl +set_option backward.isDefEq.respectTransparency.types false in theorem Iter.step_takeWhile {α β} [Iterator α Id β] {P} {it : Iter (α := α) β} : (it.takeWhile P).step = (match it.step with @@ -40,6 +41,7 @@ theorem Iter.step_takeWhile {α β} [Iterator α Id β] {P} · simp · simp +set_option backward.isDefEq.respectTransparency.types false in theorem Iter.val_step_takeWhile {α β} [Iterator α Id β] {P} {it : Iter (α := α) β} : (it.takeWhile P).step.val = (match it.step.val with @@ -107,6 +109,7 @@ theorem Iter.atIdxSlow?_takeWhile {α β} step_takeWhile] split <;> rfl +set_option backward.isDefEq.respectTransparency.types false in private theorem List.getElem?_takeWhile {l : List α} {P : α → Bool} {k} : (l.takeWhile P)[k]? = if ∀ k' : Nat, k' ≤ k → l[k']?.any P then l[k]? else none := by induction l generalizing k diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean index 1bc94d766344..db3f8bddcad1 100644 --- a/src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean +++ b/src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean @@ -69,6 +69,7 @@ theorem Iter.zip_eq_intermediateZip [Iterator α₁ Id β₁] it₁.zip it₂ = Intermediate.zip it₁ none it₂ := by rfl +set_option backward.isDefEq.respectTransparency.types false in theorem Iter.step_intermediateZip [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] {it₁ : Iter (α := α₁) β₁} diff --git a/src/Std/Data/Iterators/Lemmas/Equivalence/Basic.lean b/src/Std/Data/Iterators/Lemmas/Equivalence/Basic.lean index 320bee2c34f3..472393a9ccd5 100644 --- a/src/Std/Data/Iterators/Lemmas/Equivalence/Basic.lean +++ b/src/Std/Data/Iterators/Lemmas/Equivalence/Basic.lean @@ -96,6 +96,7 @@ coinductive_fixpoint monotonicity by end Definition +set_option backward.isDefEq.respectTransparency.types false in @[simp] theorem Equivalence.prun_liftInner_step [Iterator α m β] [Monad m] [Monad n] [MonadLiftT m n] [LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m n] @@ -109,6 +110,7 @@ theorem Equivalence.property_step [Iterator α m β] [Monad m] [LawfulMonad m] {it : IterM (α := α) m β} : (IterM.stepAsHetT it).Property = it.IsPlausibleStep := rfl +set_option backward.isDefEq.respectTransparency.types false in @[simp] theorem Equivalence.prun_step [Iterator α m β] [Monad m] [LawfulMonad m] {it : IterM (α := α) m β} {f : (step : _) → _ → m γ} : @@ -240,6 +242,7 @@ theorem Iter.Equiv.trans {α₁ α₂ α₃ β : Type w} (hbc : Iter.Equiv itb itc) : Iter.Equiv ita itc := BundledIterM.Equiv.trans hab hbc +set_option backward.isDefEq.respectTransparency.types false in theorem IterM.Equiv.of_morphism {α₁ α₂} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {β : Type w} [Iterator α₁ m β] [Iterator α₂ m β] (ita : IterM (α := α₁) m β) diff --git a/src/Std/Data/Iterators/Lemmas/Equivalence/HetT.lean b/src/Std/Data/Iterators/Lemmas/Equivalence/HetT.lean index 5a1d3208dd1f..fde287b3e2a4 100644 --- a/src/Std/Data/Iterators/Lemmas/Equivalence/HetT.lean +++ b/src/Std/Data/Iterators/Lemmas/Equivalence/HetT.lean @@ -187,6 +187,7 @@ attribute [-simp] HetT.mk.injEq /-- Converts `PostconditionT m α` to `HetT m α`, preserving the postcondition property. -/ +@[implicit_reducible] noncomputable def HetT.ofPostconditionT [Monad m] (x : PostconditionT m α) : HetT m α := ⟨x.Property, inferInstance, USquash.deflate <$> x.operation⟩ @@ -198,6 +199,7 @@ Lifts `x : m α` into `HetT m α` with the trivial postcondition. Caution: This is not a lawful monad lifting function -/ +@[implicit_reducible] noncomputable def HetT.lift {α : Type w} {m : Type w → Type w'} [Monad m] (x : m α) : HetT m α := x @@ -206,14 +208,14 @@ noncomputable def HetT.lift {α : Type w} {m : Type w → Type w'} [Monad m] (x A universe-heterogeneous version of `Pure.pure`. Given `a : α`, it returns an element of `HetT m α` with the postcondition `(a = ·)`. -/ -protected noncomputable def HetT.pure {m : Type w → Type w'} [Pure m] {α : Type v} +@[implicit_reducible] protected noncomputable def HetT.pure {m : Type w → Type w'} [Pure m] {α : Type v} (a : α) : HetT m α := ⟨(a = ·), inferInstance, pure (.deflate ⟨a, rfl⟩)⟩ /-- A generalization of `HetT.map` that provides the postcondition property to the mapping function. -/ -protected noncomputable def HetT.pmap {m : Type w → Type w'} [Functor m] {α : Type u} {β : Type v} +@[implicit_reducible] protected noncomputable def HetT.pmap {m : Type w → Type w'} [Functor m] {α : Type u} {β : Type v} (x : HetT m α) (f : (a : α) → x.Property a → β) : HetT m β := have : Small.{w} (Subtype x.Property) := x.small have := Small.map x.Property f @@ -222,13 +224,14 @@ protected noncomputable def HetT.pmap {m : Type w → Type w'} [Functor m] {α : /-- A universe-heterogeneous version of `Functor.map`. -/ -protected noncomputable def HetT.map {m : Type w → Type w'} [Functor m] {α : Type u} {β : Type v} +@[implicit_reducible] protected noncomputable def HetT.map {m : Type w → Type w'} [Functor m] {α : Type u} {β : Type v} (f : α → β) (x : HetT m α) : HetT m β := x.pmap (fun a _ => f a) /-- A generalization of `HetT.bind` that provides the postcondition property to the mapping function. -/ +@[implicit_reducible] protected noncomputable def HetT.pbind {m : Type w → Type w'} [Monad m] {α : Type u} {β : Type v} (x : HetT m α) (f : (a : α) → x.Property a → HetT m β) : HetT m β := have := x.small @@ -241,7 +244,7 @@ protected noncomputable def HetT.pbind {m : Type w → Type w'} [Monad m] {α : /-- A universe-heterogeneous version of `Bind.bind`. -/ -protected noncomputable def HetT.bind {m : Type w → Type w'} [Monad m] {α : Type u} {β : Type v} +@[implicit_reducible] protected noncomputable def HetT.bind {m : Type w → Type w'} [Monad m] {α : Type u} {β : Type v} (x : HetT m α) (f : α → HetT m β) : HetT m β := have := x.small have := fun a => (f a).small @@ -290,6 +293,7 @@ theorem HetT.prun_ofPostconditionT [Monad m] [LawfulMonad m] {x : PostconditionT /-- If the monad `m` is liftable to `n`, lifts `HetT m α` to `HetT n α`. -/ +@[implicit_reducible] noncomputable def HetT.liftInner {m : Type w → Type w'} (n : Type w → Type w'') [MonadLiftT m n] (x : HetT m α) : HetT n α := ⟨x.Property, x.small, x.operation⟩ diff --git a/src/Std/Data/Iterators/Lemmas/Equivalence/StepCongr.lean b/src/Std/Data/Iterators/Lemmas/Equivalence/StepCongr.lean index f20833768a33..f154b17bde17 100644 --- a/src/Std/Data/Iterators/Lemmas/Equivalence/StepCongr.lean +++ b/src/Std/Data/Iterators/Lemmas/Equivalence/StepCongr.lean @@ -115,6 +115,7 @@ theorem IterStep.restrict_bundle [Iterator α₁ m β] [Iterator α₂ m β] [Mo IterM.QuotStep.restrict ⟨step.bundledQuotient, h⟩ = Quot.mk _ h.choose := by rfl +set_option backward.isDefEq.respectTransparency.types false in /- Equivalence and usage of `transportAlongEquiv` tells us: @@ -198,6 +199,7 @@ theorem IterM.Equiv.lift_step_bind_congr {α₁ α₂ : Type w} [Monad m] [Lawfu have hex := exists_step_of_step h.symm step.inflate simp [hfg (.deflate hex.choose) step (by simpa using hex.choose_spec.symm)] +set_option backward.isDefEq.respectTransparency.types false in theorem IterM.Equiv.liftInner_stepAsHetT_pbind_congr [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α₁ m β] [Iterator α₂ m β] diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean index ee41fc51db27..277f0947022a 100644 --- a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean +++ b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean @@ -53,6 +53,7 @@ theorem Array.step_iterM {array : Array β} : section Equivalence +set_option backward.isDefEq.respectTransparency.types 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 e2a949d6178d..4b3db1ebcbc0 100644 --- a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean +++ b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean @@ -15,6 +15,7 @@ open Std.Internal Std.Iterators Std.Iterators.Types variable {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] {β : Type w} +set_option backward.isDefEq.respectTransparency.types false in -- We don't want to pollute `List` with this rarely used lemma. public theorem Types.ListIterator.stepAsHetT_iterM [LawfulMonad m] {l : List β} : (l.iterM m).stepAsHetT = (match l with diff --git a/src/Std/Do/PostCond.lean b/src/Std/Do/PostCond.lean index ddc76b50b266..9e601c2c488c 100644 --- a/src/Std/Do/PostCond.lean +++ b/src/Std/Do/PostCond.lean @@ -104,7 +104,7 @@ example : ExceptConds (.arg σ (.except ε .pure)) = ((ε → ULift Prop) × Uni example : ExceptConds (.except ε (.arg σ .pure)) = ((ε → σ → ULift Prop) × Unit) := rfl ``` -/ -def ExceptConds : PostShape.{u} → Type u +@[implicit_reducible] def ExceptConds : PostShape.{u} → Type u | .pure => PUnit | .arg _ ps => ExceptConds ps | .except ε ps => (ε → Assertion ps) × ExceptConds ps diff --git a/src/Std/Do/WP/Basic.lean b/src/Std/Do/WP/Basic.lean index dc6e035271c8..ca1acacd29a7 100644 --- a/src/Std/Do/WP/Basic.lean +++ b/src/Std/Do/WP/Basic.lean @@ -152,7 +152,7 @@ theorem Except.of_wp_eq {ε α : Type u} {x prog : Except ε α} (h : prog = x) (⊢ₛ wp⟦prog⟧ post⟨fun a => ⌜P (.ok a)⌝, fun e => ⌜P (.error e)⌝⟩) → P x := by subst h intro hspec - simp only [wp, ExceptT.run, Id.run, PredTrans.apply_pushExcept, PredTrans.apply_Pure_pure, instWP._aux_1] at hspec + simp only [wp, ExceptT.run, Id.run, PredTrans.apply_pushExcept, PredTrans.apply_Pure_pure] at hspec split at hspec <;> exact hspec True.intro /-- @@ -164,7 +164,7 @@ Useful if you want to prove a property about an expression `prog : Except ε α` theorem Except.of_wp {ε α : Type u} {prog : Except ε α} (P : Except ε α → Prop) : (⊢ₛ wp⟦prog⟧ post⟨fun a => ⌜P (.ok a)⌝, fun e => ⌜P (.error e)⌝⟩) → P prog := by intro hspec - simp only [wp, ExceptT.run, Id.run, PredTrans.apply_pushExcept, PredTrans.apply_Pure_pure, instWP._aux_1] at hspec + simp only [wp, ExceptT.run, Id.run, PredTrans.apply_pushExcept, PredTrans.apply_Pure_pure] at hspec split at hspec <;> exact hspec True.intro /-- @@ -176,7 +176,7 @@ theorem Option.of_wp_eq {α : Type u} {x prog : Option α} (h : prog = x) (P : O (⊢ₛ wp⟦prog⟧ post⟨fun a => ⌜P (some a)⌝, fun _ => ⌜P none⌝⟩) → P x := by subst h intro hspec - simp only [wp, OptionT.run, Id.run, PredTrans.apply_pushOption, PredTrans.apply_Pure_pure, instWP._aux_1] at hspec + simp only [wp, OptionT.run, Id.run, PredTrans.apply_pushOption, PredTrans.apply_Pure_pure] at hspec split at hspec <;> exact hspec True.intro /-- diff --git a/src/Std/Do/WP/SimpLemmas.lean b/src/Std/Do/WP/SimpLemmas.lean index b2ae319e9092..875833376967 100644 --- a/src/Std/Do/WP/SimpLemmas.lean +++ b/src/Std/Do/WP/SimpLemmas.lean @@ -422,7 +422,7 @@ theorem throwThe [MonadExceptOf ε m] [WP m ps] : @[simp] theorem throw_Except : wp⟦MonadExceptOf.throw e : Except ε α⟧ Q = Q.2.1 e := by - simp [wp, MonadExceptOf.throw, Id.run, ExceptT.run, Except.instWP._aux_1] + simp [wp, MonadExceptOf.throw, Id.run, ExceptT.run] @[simp] theorem throw_ExceptT [Monad m] [WPMonad m ps] : @@ -432,7 +432,7 @@ theorem throw_ExceptT [Monad m] [WPMonad m ps] : @[simp] theorem throw_Option : wp⟦MonadExceptOf.throw e : Option α⟧ Q = Q.2.1 e := by - simp [wp, MonadExceptOf.throw, Id.run, OptionT.run, Option.instWP._aux_1] + simp [wp, MonadExceptOf.throw, Id.run, OptionT.run] @[simp] theorem throw_OptionT [Monad m] [WPMonad m ps] : @@ -484,7 +484,7 @@ theorem tryCatchThe [MonadExceptOf ε m] [WP m ps] : @[simp] theorem tryCatch_Except : wp⟦MonadExceptOf.tryCatch x h : Except ε α⟧ Q = wp⟦x⟧ (Q.1, fun e => wp⟦h e⟧ Q, Q.2.2) := by - simp only [wp, Except.instWP._aux_1, ExceptT.run, Id.run, MonadExceptOf.tryCatch, Except.tryCatch, + simp only [wp, ExceptT.run, Id.run, MonadExceptOf.tryCatch, Except.tryCatch, PredTrans.apply_pushExcept] cases x <;> simp @@ -501,7 +501,7 @@ theorem tryCatch_ExceptT [Monad m] [WPMonad m ps] : @[simp] theorem tryCatch_Option : wp⟦MonadExceptOf.tryCatch x h : Option α⟧ Q = wp⟦x⟧ (Q.1, fun e => wp⟦h e⟧ Q, Q.2.2) := by - simp only [wp, Option.instWP._aux_1, Id.run, OptionT.run, MonadExceptOf.tryCatch, Option.tryCatch, + simp only [wp, Id.run, OptionT.run, MonadExceptOf.tryCatch, Option.tryCatch, PredTrans.apply_pushOption] cases x <;> simp @@ -590,7 +590,7 @@ theorem orElse_ExceptT [Monad m] [WPMonad m ps] : @[simp] theorem orElse_Option : wp⟦OrElse.orElse x h : Option α⟧ Q = wp⟦x⟧ (Q.1, fun _ => wp⟦h ()⟧ Q, Q.2.2) := by - cases x <;> simp [OrElse.orElse, Option.orElse, wp, Id.run, OptionT.run, Option.instWP._aux_1] + cases x <;> simp [OrElse.orElse, Option.orElse, wp, Id.run, OptionT.run] @[simp] theorem orElse_OptionT [Monad m] [WPMonad m ps] : diff --git a/src/Std/Sat/AIG/CachedLemmas.lean b/src/Std/Sat/AIG/CachedLemmas.lean index ddef402dad09..c8f9dd5509e2 100644 --- a/src/Std/Sat/AIG/CachedLemmas.lean +++ b/src/Std/Sat/AIG/CachedLemmas.lean @@ -25,6 +25,7 @@ namespace AIG variable {α : Type} [Hashable α] [DecidableEq α] +set_option backward.isDefEq.respectTransparency.types false in /-- If we find a cached atom declaration in the AIG, denoting it is equivalent to denoting `AIG.mkAtom`. -/ @@ -97,6 +98,7 @@ theorem mkAtomCached_eval_eq_mkAtom_eval {aig : AIG α} : rw [denote_mkAtom_cached heq1] · simp [mkAtom, denote] +set_option backward.isDefEq.respectTransparency.types false in /-- The central equality theorem between `mkConstCached` and `mkConst`. -/ @@ -110,6 +112,7 @@ theorem denote_mkConstCached {aig : AIG α} : next heq => simp [aig.hconst] at heq next heq => simp [aig.hconst] at heq +set_option backward.isDefEq.respectTransparency.types false in /-- If we find a cached gate declaration in the AIG, denoting it is equivalent to denoting `AIG.mkGate`. -/ diff --git a/src/Std/Sat/AIG/If.lean b/src/Std/Sat/AIG/If.lean index bab08411832b..786473caf260 100644 --- a/src/Std/Sat/AIG/If.lean +++ b/src/Std/Sat/AIG/If.lean @@ -61,6 +61,7 @@ def mkIfCached (aig : AIG α) (input : TernaryInput aig) : Entrypoint α := apply AIG.LawfulOperator.le_size (f := mkNotCached) aig.mkOrCached ⟨lhsRef, rhsRef⟩ +set_option backward.isDefEq.respectTransparency.types false in instance : LawfulOperator α TernaryInput mkIfCached where le_size := by intros @@ -92,6 +93,7 @@ theorem if_as_bool (d l r : Bool) : (if d then l else r) = ((d && l) || (!d && r revert d l r decide +set_option backward.isDefEq.respectTransparency.types false in @[simp] theorem denote_mkIfCached {aig : AIG α} {input : TernaryInput aig} : ⟦aig.mkIfCached input, assign⟧ @@ -173,6 +175,7 @@ termination_by w - curr end ite +set_option backward.isDefEq.respectTransparency.types false in instance : LawfulVecOperator α IfInput ite where le_size := by intros @@ -200,7 +203,7 @@ theorem go_get_aux {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (d intros rw [go_get_aux (hidx := Nat.lt_succ_of_lt hidx) (hfoo := go_le_size ..)] rw [AIG.RefVec.get_push_ref_lt (hidx := hidx)] - simp only [Ref.cast, Ref.mk.injEq] + simp only [Ref.cast] rw [AIG.RefVec.get_cast] simp · rw [← hgo] @@ -235,6 +238,7 @@ theorem go_denote_mem_prefix {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr · intros apply go_le_size +set_option backward.isDefEq.respectTransparency.types false in theorem denote_go {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (discr : Ref aig) (lhs rhs : RefVec aig w) (s : RefVec aig curr) : ∀ (idx : Nat) (hidx1 : idx < w), diff --git a/src/Std/Sat/AIG/Lemmas.lean b/src/Std/Sat/AIG/Lemmas.lean index e473093e8f61..92725b5b6fb5 100644 --- a/src/Std/Sat/AIG/Lemmas.lean +++ b/src/Std/Sat/AIG/Lemmas.lean @@ -116,6 +116,7 @@ instance : LawfulOperator α BinaryInput mkGate where intros apply mkGate_decl_eq +set_option backward.isDefEq.respectTransparency.types false in @[simp] theorem denote_mkGate {aig : AIG α} {input : BinaryInput aig} : ⟦aig.mkGate input, assign⟧ @@ -163,6 +164,7 @@ instance : LawfulOperator α (fun _ => α) mkAtom where intros apply mkAtom_decl_eq +set_option backward.isDefEq.respectTransparency.types false in @[simp] theorem denote_mkAtom {aig : AIG α} : ⟦(aig.mkAtom var), assign⟧ = assign var := by @@ -203,6 +205,7 @@ instance : LawfulOperator α (fun _ => Bool) mkConst where intros apply mkConst_decl_eq +set_option backward.isDefEq.respectTransparency.types false in @[simp] theorem denote_mkConst {aig : AIG α} : ⟦(aig.mkConst val), assign⟧ = val := by unfold denote denote.go @@ -217,6 +220,7 @@ theorem denote_mkConst {aig : AIG α} : ⟦(aig.mkConst val), assign⟧ = val := rw [mkConst, Array.getElem_push_eq] at heq contradiction +set_option backward.isDefEq.respectTransparency.types false in /-- If an index contains a `Decl.false` we know how to denote it. -/ @@ -225,6 +229,7 @@ theorem denote_idx_false {aig : AIG α} {hstart} (h : aig.decls[start]'hstart = unfold denote denote.go split <;> simp_all +set_option backward.isDefEq.respectTransparency.types false in /-- If an index contains a `Decl.atom` we know how to denote it. -/ @@ -233,6 +238,7 @@ theorem denote_idx_atom {aig : AIG α} {hstart} (h : aig.decls[start] = .atom a) unfold denote denote.go split <;> simp_all +set_option backward.isDefEq.respectTransparency.types false in /-- If an index contains a `Decl.gate` we know how to denote it. -/ diff --git a/src/Std/Sat/AIG/RefVecOperator/Fold.lean b/src/Std/Sat/AIG/RefVecOperator/Fold.lean index 94c07ea1301c..f6c19ebb93bc 100644 --- a/src/Std/Sat/AIG/RefVecOperator/Fold.lean +++ b/src/Std/Sat/AIG/RefVecOperator/Fold.lean @@ -82,6 +82,7 @@ theorem fold.go_decl_eq {aig : AIG α} (acc : Ref aig) (i : Nat) (s : RefVec aig simp termination_by len - i +set_option backward.isDefEq.respectTransparency.types false in theorem fold_decl_eq {aig : AIG α} (vec : RefVec aig len) (func : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput func] : ∀ idx (h1 : idx < aig.decls.size) (h2), diff --git a/src/Std/Sat/AIG/RelabelNat.lean b/src/Std/Sat/AIG/RelabelNat.lean index 40de5d64b1d6..4cdc43aba1e2 100644 --- a/src/Std/Sat/AIG/RelabelNat.lean +++ b/src/Std/Sat/AIG/RelabelNat.lean @@ -331,6 +331,7 @@ theorem relabelNat'_fst_eq_relabelNat {aig : AIG α} : aig.relabelNat'.fst = aig theorem relabelNat_size_eq_size {aig : AIG α} : aig.relabelNat.decls.size = aig.decls.size := by simp [relabelNat, relabelNat'] +set_option backward.isDefEq.respectTransparency.types false in theorem relabelNat_unsat_iff_of_NonEmpty [Nonempty α] {aig : AIG α} {hidx1} {hidx2} : (aig.relabelNat).UnsatAt idx invert hidx1 ↔ aig.UnsatAt idx invert hidx2 := by dsimp only [relabelNat, relabelNat'] diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Carry.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Carry.lean index 06dad774daa4..ec3bc90f0baa 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Carry.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Carry.lean @@ -82,6 +82,7 @@ theorem go_decl_eq {aig : AIG α} {cin} {lhs rhs : AIG.RefVec aig w} : · simp [← hgo] termination_by w - curr +set_option backward.isDefEq.respectTransparency.types false in instance : AIG.LawfulOperator α OverflowInput mkOverflowBit where le_size := by intros diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean index fb5e48ff543d..d13b63a78578 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean @@ -71,6 +71,7 @@ def mkFullAdderOut (aig : AIG α) (input : FullAdderInput aig) : AIG.Entrypoint let cin := cin.cast <| AIG.LawfulOperator.le_size (f := AIG.mkXorCached) .. aig.mkXorCached ⟨subExprRef, cin⟩ +set_option backward.isDefEq.respectTransparency.types false in instance : AIG.LawfulOperator α FullAdderInput mkFullAdderOut where le_size := by intros @@ -113,6 +114,7 @@ def mkFullAdderCarry (aig : AIG α) (input : FullAdderInput aig) : AIG.Entrypoin let lorRef := lorRef.cast hror aig.mkOrCached ⟨lorRef, rorRef⟩ +set_option backward.isDefEq.respectTransparency.types false in instance : AIG.LawfulOperator α FullAdderInput mkFullAdderCarry where le_size := by intros @@ -212,6 +214,7 @@ theorem go_le_size (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : AIG.R · simp termination_by w - curr +set_option backward.isDefEq.respectTransparency.types false in theorem go_decl_eq (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : AIG.Ref aig) (s : AIG.RefVec aig curr) (lhs rhs : AIG.RefVec aig w) : ∀ (idx : Nat) (h1) (h2), @@ -236,6 +239,7 @@ theorem go_decl_eq (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : AIG.R · simp [← hgo] termination_by w - curr +set_option backward.isDefEq.respectTransparency.types false in instance : AIG.LawfulVecOperator α AIG.BinaryRefVec blast where le_size := by intros diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Cpop.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Cpop.lean index 605cf8c8156e..3e386ca4f30e 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Cpop.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Cpop.lean @@ -48,6 +48,7 @@ def blastExtractAndExtendBit (aig : AIG α) (target : ExtractAndExtendBitTarget let extend := res.vec ⟨aig, extend⟩ +set_option backward.isDefEq.respectTransparency.types false in instance : AIG.LawfulVecOperator α ExtractAndExtendBitTarget blastExtractAndExtendBit where le_size := by intros diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Eq.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Eq.lean index b653adfa915d..744fb4c2ba73 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Eq.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Eq.lean @@ -28,6 +28,7 @@ def mkEq (aig : AIG α) (pair : AIG.BinaryRefVec aig w) : AIG.Entrypoint α := let bits := res.vec AIG.RefVec.fold aig bits AIG.mkAndCached +set_option backward.isDefEq.respectTransparency.types false in instance {w : Nat} : AIG.LawfulOperator α (AIG.BinaryRefVec · w) mkEq where le_size := by intros diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Neg.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Neg.lean index c9b8ec88397f..73ab200c397c 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Neg.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Neg.lean @@ -34,6 +34,7 @@ def blastNeg (aig : AIG α) (input : AIG.RefVec aig w) : AIG.RefVecEntry α w := blastAdd aig ⟨notInput, one⟩ +set_option backward.isDefEq.respectTransparency.types false in instance : AIG.LawfulVecOperator α AIG.RefVec blastNeg where le_size := by intros diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Sub.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Sub.lean index 517f8fc78c47..233d69714cdc 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Sub.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Sub.lean @@ -32,6 +32,7 @@ def blastSub (aig : AIG α) (input : AIG.BinaryRefVec aig w) : AIG.RefVecEntry blastAdd aig ⟨lhs, negRhs⟩ +set_option backward.isDefEq.respectTransparency.types false in instance : AIG.LawfulVecOperator α AIG.BinaryRefVec blastSub where le_size := by intros diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Udiv.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Udiv.lean index 2e96c8758d9c..c567f340d89c 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Udiv.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Udiv.lean @@ -41,6 +41,7 @@ def blastShiftConcat (aig : AIG α) (input : ShiftConcatInput aig w) : AIG.RefVe let new := bit.append lhs blastZeroExtend aig ⟨1 + w, new⟩ +set_option backward.isDefEq.respectTransparency.types false in instance : AIG.LawfulVecOperator α ShiftConcatInput blastShiftConcat where le_size := by intros @@ -276,6 +277,7 @@ def blastUdiv (aig : AIG α) (input : AIG.BinaryRefVec aig w) : AIG.RefVecEntry AIG.RefVec.ite aig ⟨discr, zero, divRes⟩ +set_option backward.isDefEq.respectTransparency.types false in instance : AIG.LawfulVecOperator α AIG.BinaryRefVec blastUdiv where le_size := by intros diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Ult.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Ult.lean index 16cf64d2003b..d37b11fdbb86 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Ult.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Ult.lean @@ -38,6 +38,7 @@ def mkUlt (aig : AIG α) (pair : AIG.BinaryRefVec aig w) : AIG.Entrypoint α := let overflowRef := res.ref aig.mkNotCached overflowRef +set_option backward.isDefEq.respectTransparency.types false in instance {w : Nat} : AIG.LawfulOperator α (AIG.BinaryRefVec · w) mkUlt where le_size := by intros diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Umod.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Umod.lean index 24688b4309da..c0aafda3fc15 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Umod.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Umod.lean @@ -45,6 +45,7 @@ def blastUmod (aig : AIG α) (input : AIG.BinaryRefVec aig w) : AIG.RefVecEntry AIG.RefVec.ite aig ⟨discr, lhs, modRes⟩ +set_option backward.isDefEq.respectTransparency.types false in instance : AIG.LawfulVecOperator α AIG.BinaryRefVec blastUmod where le_size := by intros diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean index 94d51d73ad1e..e690055e87e8 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean @@ -62,6 +62,7 @@ def bitblast (aig : AIG BVBit) (input : BVExpr.WithCache BVPred aig) : Return ai let res := blastGetLsbD aig ⟨refs, idx⟩ ⟨⟨⟨aig, res⟩, hrefs⟩, cache⟩ +set_option backward.isDefEq.respectTransparency.types false in theorem bitblast_decl_eq (aig : AIG BVBit) (input : BVExpr.WithCache BVPred aig) : ∀ (idx : Nat) (h1) (h2), (bitblast aig input).result.val.aig.decls[idx]'h2 = aig.decls[idx]'h1 := by intro idx h1 h2 diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean index 9289e6d209b1..8a0e4130eb7d 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean @@ -60,6 +60,7 @@ theorem Inv_cast (cache : Cache aig1) (hpref : IsPrefix aig1.decls aig2.decls) apply denote.eq_of_isPrefix (entry := ⟨aig1, _, _, _⟩) exact hpref +set_option backward.isDefEq.respectTransparency.types false in theorem Inv_insert (cache : Cache aig) (expr : BVExpr w) (refs : AIG.RefVec aig w) (hinv : Inv assign aig cache) (hrefs : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, refs.get idx hidx, assign.toAIGAssignment⟧ = (expr.eval assign).getLsbD idx) : diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean index c4b3e755090b..279f87c35259 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean @@ -39,6 +39,7 @@ theorem denote_mkFullAdderOut (assign : α → Bool) (aig : AIG α) (input : Ful ] rw [LawfulOperator.denote_mem_prefix (f := mkXorCached)] +set_option backward.isDefEq.respectTransparency.types false in @[simp] theorem denote_mkFullAdderCarry (assign : α → Bool) (aig : AIG α) (input : FullAdderInput aig) : ⟦mkFullAdderCarry aig input, assign⟧ @@ -138,6 +139,7 @@ theorem atLeastTwo_eq_halfAdder (lhsBit rhsBit carry : Bool) : revert lhsBit rhsBit carry decide +set_option backward.isDefEq.respectTransparency.types false in theorem go_denote_eq (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : Ref aig) (s : AIG.RefVec aig curr) (lhs rhs : AIG.RefVec aig w) (assign : α → Bool) (lhsExpr rhsExpr : BitVec w) diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Cpop.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Cpop.lean index d1812ff62631..5791aaad99c9 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Cpop.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Cpop.lean @@ -140,6 +140,7 @@ theorem denote_blastExtractAndExtend (assign : α → Bool) (aig : AIG α) (w : · simp · exact hx +set_option backward.isDefEq.respectTransparency.types false in theorem denote_blastCpopLayer.go (aig : AIG α) (iterNum : Nat) (oldLayer : AIG.RefVec aig (len * w)) (newLayer : AIG.RefVec aig (iterNum * w)) (oldLayerBv : BitVec (len * w)) (hold' : 2 * (iterNum - 1) < len) diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean index ca7efc24217d..a3c36fc4c358 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean @@ -79,6 +79,7 @@ theorem blastDivSubtractShift_denote_mem_prefix (aig : AIG α) · intros apply blastDivSubtractShift_le_size +set_option backward.isDefEq.respectTransparency.types false in theorem denote_blastDivSubtractShift_q (aig : AIG α) (assign : α → Bool) (lhs rhs : BitVec w) (n d : AIG.RefVec aig w) (wn wr : Nat) (q r : AIG.RefVec aig w) (qbv rbv : BitVec w) @@ -173,6 +174,7 @@ theorem denote_blastDivSubtractShift_q (aig : AIG α) (assign : α → Bool) (lh · rw [denote_mkConstCached] . simp [Ref.hgate] +set_option backward.isDefEq.respectTransparency.types false in theorem denote_blastDivSubtractShift_r (aig : AIG α) (assign : α → Bool) (lhs rhs : BitVec w) (n d : AIG.RefVec aig w) (wn wr : Nat) (q r : AIG.RefVec aig w) (qbv rbv : BitVec w) diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean index 8768924f6520..8da205eb1e84 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean @@ -65,6 +65,7 @@ theorem entails_of_irrelevant_assignment {n : Nat} {p : (PosFin n) → Bool} {c · simp [Clause.toList, delete_iff, negl_ne_v, v_in_c_del_l] · grind +set_option backward.isDefEq.respectTransparency.types false in theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n) (hf : f.ratUnits = #[] ∧ AssignmentsInvariant f) (units : CNF.Clause (PosFin n)) : AssignmentsInvariant (insertRatUnits f units).1 := by @@ -471,6 +472,7 @@ theorem performRatCheck_success_of_performRatCheck_fold_success {n : Nat} (f : D have h := (Array.foldl_induction motive h_base h_inductive).2 performRatCheck_fold_success i simpa [getElem!_def, i.2, dite_true] using h +set_option backward.isDefEq.respectTransparency.types false in theorem safe_insert_of_performRatCheck_fold_success {n : Nat} (f : DefaultFormula n) (f_readyForRatAdd : ReadyForRatAdd f) (c : DefaultClause n) (pivot : Literal (PosFin n)) (rupHints : Array Nat) (ratHints : Array (Nat × Array Nat)) diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean index 80cfab7431b7..2cfc84df6e77 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean @@ -232,6 +232,7 @@ theorem safe_insert_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRup · simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq] at pf exact pf c' c'_in_f +set_option backward.isDefEq.respectTransparency.types false in theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : ReadyForRupAdd f) (units : CNF.Clause (PosFin n)) : AssignmentsInvariant (insertRupUnits f units).1 := by diff --git a/src/Std/Time/Date/Unit/Year.lean b/src/Std/Time/Date/Unit/Year.lean index a8fd4b0350e5..0f214c59762f 100644 --- a/src/Std/Time/Date/Unit/Year.lean +++ b/src/Std/Time/Date/Unit/Year.lean @@ -36,7 +36,7 @@ instance : ToString Era where /-- `Offset` represents a year offset, defined as an `Int`. -/ -@[expose] def Offset : Type := Int +@[expose, implicit_reducible] def Offset : Type := Int deriving Repr, DecidableEq, Inhabited, Add, Sub, Neg, LE, LT, ToString set_option backward.inferInstanceAs.wrap.instances false in diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index e44444704908..223763431f74 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -12,6 +12,7 @@ options get_default_options() { // switch to `true` for ABI-breaking changes affecting meta code; // see also next option! opts = opts.update({"interpreter", "prefer_native"}, false); + opts = opts.update({"backward", "isDefEq", "respectTransparency", "types"}, true); // switch to `false` when enabling `prefer_native` should also affect use // of built-in parsers in quotations; this is usually the case, but setting // both to `true` may be necessary for handling non-builtin parsers with diff --git a/tests/elab/1385.lean b/tests/elab/1385.lean index dffa4d1d3c90..23ede6c1719f 100644 --- a/tests/elab/1385.lean +++ b/tests/elab/1385.lean @@ -1,6 +1,6 @@ -def S := List Nat +abbrev S := List Nat opaque TSpec : NonemptyType -def T (s : S) : Type := TSpec.type +abbrev T (s : S) : Type := TSpec.type instance (s : S) : Nonempty (T s) := TSpec.property diff --git a/tests/elab/2552.lean b/tests/elab/2552.lean index bfb3f05fd31e..47f4f4682933 100644 --- a/tests/elab/2552.lean +++ b/tests/elab/2552.lean @@ -1,4 +1,4 @@ -@[inline] def decidable_of_iff'' {b : Prop} (a : Prop) (h : a ↔ b) [Decidable a] : Decidable b := +@[implicit_reducible] def decidable_of_iff'' {b : Prop} (a : Prop) (h : a ↔ b) [Decidable a] : Decidable b := decidable_of_decidable_of_iff h theorem LE.le.lt_or_eq_dec {a b : Nat} (hab : a ≤ b) : a < b ∨ a = b := diff --git a/tests/elab/2901.lean b/tests/elab/2901.lean index f972cbe12b30..17b124a8769e 100644 --- a/tests/elab/2901.lean +++ b/tests/elab/2901.lean @@ -1,4 +1,4 @@ -def Vector' (α : Type u) (n : Nat) := +abbrev Vector' (α : Type u) (n : Nat) := { l : List α // l.length = n } inductive HVect : (n : Nat) -> (Vector' (Type v) n) -> Type (v+1) where diff --git a/tests/elab/3524.lean b/tests/elab/3524.lean index e63efe1b9d2b..0982c0a2ada3 100644 --- a/tests/elab/3524.lean +++ b/tests/elab/3524.lean @@ -1,3 +1,4 @@ +set_option maxRecDepth 1024 -- TODO: investigate why we had to increase it example (a : Nat) : ((2 ^ 7) + a) - 2 ^ 7 = 0 := by generalize 0 - 0 = x sorry diff --git a/tests/elab/3524.lean.out.expected b/tests/elab/3524.lean.out.expected index 27a6378d42ea..52db2666793f 100644 --- a/tests/elab/3524.lean.out.expected +++ b/tests/elab/3524.lean.out.expected @@ -1 +1 @@ -3524.lean:1:0-1:7: warning: declaration uses `sorry` +3524.lean:2:0-2:7: warning: declaration uses `sorry` diff --git a/tests/elab/6090.lean b/tests/elab/6090.lean index f4312077572e..b9f2646e7c17 100644 --- a/tests/elab/6090.lean +++ b/tests/elab/6090.lean @@ -10,7 +10,7 @@ section #guard_msgs in #check @id -- '#print' was unaffected, but throw in a test anyway. /-- -info: def id.{u} : {α : Sort u} → α → α := +info: @[implicit_reducible] def id.{u} : {α : Sort u} → α → α := fun {α} a => a -/ #guard_msgs in #print id @@ -23,7 +23,7 @@ set_option pp.raw true #guard_msgs in #check @id -- '#print' was unaffected, but throw in a test anyway. /-- -info: def id.{u} : forall {α : Sort.{u}}, α -> α := +info: @[implicit_reducible] def id.{u} : forall {α : Sort.{u}}, α -> α := fun {α : Sort.{u}} (a : α) => a -/ #guard_msgs in #print id diff --git a/tests/elab/async_tcp_half.lean b/tests/elab/async_tcp_half.lean index d17a05f2388a..a5430a14a4d0 100644 --- a/tests/elab/async_tcp_half.lean +++ b/tests/elab/async_tcp_half.lean @@ -20,14 +20,14 @@ def runJoe (addr: SocketAddress) : Async Unit := do client.shutdown def listenClose : IO Unit := do - let addr := SocketAddressV4.mk (.ofParts 127 0 0 1) 8080 + let addr := SocketAddressV4.mk (.ofParts 127 0 0 1) 8787 let server ← TCP.Socket.Server.mk server.bind addr server.listen 128 def acceptClose : IO Unit := do - let addr := SocketAddressV4.mk (.ofParts 127 0 0 1) 8081 + let addr := SocketAddressV4.mk (.ofParts 127 0 0 1) 8781 let server ← TCP.Socket.Server.mk server.bind addr diff --git a/tests/elab/delabMatch.lean b/tests/elab/delabMatch.lean index a03f180b4d78..2c13cde85f66 100644 --- a/tests/elab/delabMatch.lean +++ b/tests/elab/delabMatch.lean @@ -8,7 +8,7 @@ import Lean Basic functionality -/ /-- -info: def Nat.pred : Nat → Nat := +info: @[implicit_reducible] def Nat.pred : Nat → Nat := fun x => match x with | 0 => 0 diff --git a/tests/elab/eq_some_iff_get_eq_issue.lean b/tests/elab/eq_some_iff_get_eq_issue.lean index 20961edf86c4..137ff6d35e8a 100644 --- a/tests/elab/eq_some_iff_get_eq_issue.lean +++ b/tests/elab/eq_some_iff_get_eq_issue.lean @@ -3,4 +3,4 @@ namespace Option theorem eq_some_iff_get_eq' {o : Option α} {a : α} : o = some a ↔ ∃ h : o.isSome, Option.get _ h = a := by cases o; simp only [isSome_none, false_iff, reduceCtorEq]; intro h; cases h; contradiction - simp [exists_prop] + simp diff --git a/tests/elab/guessLex.lean b/tests/elab/guessLex.lean index 44df94ae1202..d40c92d5611a 100644 --- a/tests/elab/guessLex.lean +++ b/tests/elab/guessLex.lean @@ -198,7 +198,7 @@ end MutualNotNat1 namespace MutualNotNat2 -- A type that is defeq to Nat, but with a different `sizeOf`, checking that the -- inferred argument uses `sizeOf` so that the types of the termination measure aligns. -def OddNat3 := Nat +@[implicit_reducible] def OddNat3 := Nat instance : SizeOf OddNat3 := ⟨fun n => 42 - @id Nat n⟩ @[simp] theorem OddNat3.sizeOf_eq (n : OddNat3) : sizeOf n = 42 - @id Nat n := rfl mutual @@ -219,7 +219,7 @@ namespace MutualNotNat3 -- Previously `GuessLex` was inferring the `SizeOf` instance based on the type of the -- *concrete* parameter or argument, which was wrong. -- The inference needs to be based on the parameter type in the function's signature. -def OddNat3 := Nat +@[implicit_reducible] def OddNat3 := Nat instance : SizeOf OddNat3 := ⟨fun n => 42 - @id Nat n⟩ @[simp] theorem OddNat3.sizeOf_eq (n : OddNat3) : sizeOf n = 42 - @id Nat n := rfl mutual diff --git a/tests/elab/heapSort.lean b/tests/elab/heapSort.lean index 5b65410eef2e..84cf547330bd 100644 --- a/tests/elab/heapSort.lean +++ b/tests/elab/heapSort.lean @@ -81,7 +81,7 @@ instance (lt) : EmptyCollection (BinaryHeap α lt) := ⟨empty _⟩ def singleton (lt) (x : α) : BinaryHeap α lt := ⟨#[x]⟩ /-- `O(1)`. Get the number of elements in a `BinaryHeap`. -/ -def size {lt} (self : BinaryHeap α lt) : Nat := self.1.size +@[implicit_reducible] def size {lt} (self : BinaryHeap α lt) : Nat := self.1.size /-- `O(1)`. Get an element in the heap by index. -/ def get {lt} (self : BinaryHeap α lt) (i : Fin self.size) : α := self.1[i]'i.2 diff --git a/tests/elab/ind_whnf.lean b/tests/elab/ind_whnf.lean index 21ba1c557639..c44843a3cd56 100644 --- a/tests/elab/ind_whnf.lean +++ b/tests/elab/ind_whnf.lean @@ -1,4 +1,6 @@ -inductive Expr : id Type +abbrev id' (α : Sort u) := α + +inductive Expr : id' Type | var : Nat → Expr | app : String → List Expr → Expr diff --git a/tests/elab/isDefEqCheckAssignmentBug.lean.out.expected b/tests/elab/isDefEqCheckAssignmentBug.lean.out.expected index 2fd0b5e7b8f9..6561fcfe88e4 100644 --- a/tests/elab/isDefEqCheckAssignmentBug.lean.out.expected +++ b/tests/elab/isDefEqCheckAssignmentBug.lean.out.expected @@ -24,12 +24,13 @@ (StateRefT' IO.RealWorld Elab.Command.State (EIO Exception)) =?= ReaderT Context (StateRefT' IO.RealWorld State CoreM) [Meta.isDefEq] ❌️ Elab.Command.Context =?= Context - [Meta.isDefEq.onFailure] ❌️ ReaderT Elab.Command.Context - (StateRefT' IO.RealWorld Elab.Command.State - (EIO Exception)) =?= ReaderT Context (StateRefT' IO.RealWorld State CoreM) - [Meta.isDefEq.onFailure] ❌️ ReaderT Elab.Command.Context - (StateRefT' IO.RealWorld Elab.Command.State - (EIO Exception)) =?= ReaderT Context (StateRefT' IO.RealWorld State CoreM) + [Meta.isDefEq] ❌️ fun α => + Elab.Command.Context → + StateRefT' IO.RealWorld Elab.Command.State (EIO Exception) + α =?= fun α => Context → StateRefT' IO.RealWorld State CoreM α + [Meta.isDefEq] ✅️ Type =?= Type + [Meta.isDefEq] ❌️ Elab.Command.Context =?= Context + [Meta.isDefEq] ❌️ Elab.Command.Context =?= Context [Meta.isDefEq.onFailure] ❌️ MonadEvalT MetaM Elab.Command.CommandElabM =?= MonadEvalT ?m ?m [Meta.isDefEq.onFailure] ❌️ MonadEvalT MetaM Elab.Command.CommandElabM =?= MonadEvalT ?m ?m [Meta.isDefEq] ✅️ MonadEvalT MetaM Elab.Command.CommandElabM =?= MonadEvalT ?m ?m @@ -79,10 +80,13 @@ [Meta.isDefEq] ❌️ ReaderT Elab.Term.Context (StateRefT' IO.RealWorld Elab.Term.State MetaM) =?= ReaderT Context (StateRefT' IO.RealWorld State CoreM) [Meta.isDefEq] ❌️ Elab.Term.Context =?= Context - [Meta.isDefEq.onFailure] ❌️ ReaderT Elab.Term.Context - (StateRefT' IO.RealWorld Elab.Term.State MetaM) =?= ReaderT Context (StateRefT' IO.RealWorld State CoreM) - [Meta.isDefEq.onFailure] ❌️ ReaderT Elab.Term.Context - (StateRefT' IO.RealWorld Elab.Term.State MetaM) =?= ReaderT Context (StateRefT' IO.RealWorld State CoreM) + [Meta.isDefEq] ❌️ fun α => + Elab.Term.Context → + StateRefT' IO.RealWorld Elab.Term.State MetaM + α =?= fun α => Context → StateRefT' IO.RealWorld State CoreM α + [Meta.isDefEq] ✅️ Type =?= Type + [Meta.isDefEq] ❌️ Elab.Term.Context =?= Context + [Meta.isDefEq] ❌️ Elab.Term.Context =?= Context [Meta.isDefEq.onFailure] ❌️ MonadEvalT MetaM Elab.TermElabM =?= MonadEvalT ?m ?m [Meta.isDefEq.onFailure] ❌️ MonadEvalT MetaM Elab.TermElabM =?= MonadEvalT ?m ?m [Meta.isDefEq] ✅️ MonadEvalT MetaM Elab.TermElabM =?= MonadEvalT ?m ?m @@ -177,11 +181,21 @@ [Meta.isDefEq] ❌️ StateRefT' IO.RealWorld Elab.Term.State MetaM =?= MetaM [Meta.isDefEq] ❌️ StateRefT' IO.RealWorld Elab.Term.State MetaM =?= ReaderT Context (StateRefT' IO.RealWorld State CoreM) - [Meta.isDefEq] ❌️ StateRefT' =?= ReaderT - [Meta.isDefEq.onFailure] ❌️ StateRefT' IO.RealWorld Elab.Term.State - MetaM =?= ReaderT Context (StateRefT' IO.RealWorld State CoreM) - [Meta.isDefEq.onFailure] ❌️ StateRefT' IO.RealWorld Elab.Term.State - MetaM =?= ReaderT Context (StateRefT' IO.RealWorld State CoreM) + [Meta.isDefEq] ❌️ fun α => + ReaderT (ST.Ref IO.RealWorld Elab.Term.State) MetaM + α =?= ReaderT Context (StateRefT' IO.RealWorld State CoreM) + [Meta.isDefEq] ❌️ fun α => + ReaderT (ST.Ref IO.RealWorld Elab.Term.State) MetaM + α =?= fun α => ReaderT Context (StateRefT' IO.RealWorld State CoreM) α + [Meta.isDefEq] ✅️ Type =?= Type + [Meta.isDefEq] ❌️ ReaderT (ST.Ref IO.RealWorld Elab.Term.State) MetaM + α =?= ReaderT Context (StateRefT' IO.RealWorld State CoreM) α + [Meta.isDefEq] ❌️ ST.Ref IO.RealWorld Elab.Term.State =?= Context + [Meta.isDefEq.onFailure] ❌️ ST.Ref IO.RealWorld Elab.Term.State =?= Context + [Meta.isDefEq] ❌️ ST.Ref IO.RealWorld Elab.Term.State → + MetaM α =?= Context → StateRefT' IO.RealWorld State CoreM α + [Meta.isDefEq] ❌️ ST.Ref IO.RealWorld Elab.Term.State =?= Context + [Meta.isDefEq] ❌️ ST.Ref IO.RealWorld Elab.Term.State =?= Context [Meta.isDefEq.onFailure] ❌️ MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM) =?= MonadEvalT ?m ?m [Meta.isDefEq.onFailure] ❌️ MonadEvalT MetaM diff --git a/tests/elab/issue11450.lean b/tests/elab/issue11450.lean index 85131ed22d5a..54ddc005691c 100644 --- a/tests/elab/issue11450.lean +++ b/tests/elab/issue11450.lean @@ -22,8 +22,7 @@ info: @[reducible] def Term.var.noConfusion.{u} : {L : Nat → Type} → #guard_msgs in #print sig Term.var.noConfusion - -def Vector' (α : Type u) (n : Nat) := +abbrev Vector' (α : Type u) (n : Nat) := { l : List α // l.length = n } inductive HVect : (n : Nat) -> (Vector' (Type v) n) -> Type (v+1) where diff --git a/tests/elab/krivine.lean b/tests/elab/krivine.lean index 4ff5785dd024..81a19d97302d 100644 --- a/tests/elab/krivine.lean +++ b/tests/elab/krivine.lean @@ -8,6 +8,7 @@ inductive KrivineClosure namespace Ex1 +@[implicit_reducible] def KrivineEnv := List KrivineClosure -- We need to define a `SizeOf` instance for `KrivineEnv`. Otherwise, we cannot use the auto-generated well-founded relation in diff --git a/tests/elab/partial_fixpoint_probability.lean b/tests/elab/partial_fixpoint_probability.lean index 8ff412d0e804..a14283085674 100644 --- a/tests/elab/partial_fixpoint_probability.lean +++ b/tests/elab/partial_fixpoint_probability.lean @@ -46,6 +46,7 @@ end /-- Distributions (not normalized, which is curcial, else we don't have ⊥.) -/ +@[implicit_reducible] def Distr (α : Type) : Type := α → ENNReal noncomputable def Distr.join : Distr (Distr α) → Distr α := fun dd x => diff --git a/tests/elab/print_cmd.lean b/tests/elab/print_cmd.lean index 24d0a25cbe94..b7ac06304d67 100644 --- a/tests/elab/print_cmd.lean +++ b/tests/elab/print_cmd.lean @@ -5,7 +5,7 @@ private def foo (x : Nat) : Nat := x + 1 /-- info: hello -/ #guard_msgs in #print "hello" /-- -info: def id.{u} : {α : Sort u} → α → α := +info: @[implicit_reducible] def id.{u} : {α : Sort u} → α → α := fun {α} a => a -/ #guard_msgs in #print id diff --git a/tests/elab/renaming.lean b/tests/elab/renaming.lean index 4534517ed6f7..41fb1f08c0af 100644 --- a/tests/elab/renaming.lean +++ b/tests/elab/renaming.lean @@ -4,7 +4,7 @@ inductive Ty | base | arr (a b : Ty) -def Cxt := List Ty +@[implicit_reducible] def Cxt := List Ty inductive Var : (g : Cxt) → (a : Ty) → Type | vz {g a} : Var (a :: g) a diff --git a/tests/elab/set.lean b/tests/elab/set.lean index c1238693617a..6fc6abb4d97a 100644 --- a/tests/elab/set.lean +++ b/tests/elab/set.lean @@ -1,4 +1,4 @@ -def Set (α : Type u) := α → Prop +abbrev Set (α : Type u) := α → Prop def Set.in (s : Set α) (a : α) := s a notation:50 a " ∈ " s:50 => Set.in s a diff --git a/tests/elab/slice.lean b/tests/elab/slice.lean index d06c44075a64..321ad0c9a8e5 100644 --- a/tests/elab/slice.lean +++ b/tests/elab/slice.lean @@ -47,6 +47,9 @@ example : #[1, 2, 3, 4, 5][1...*][*...2].toList = [2, 3] := by simp example : #[1, 2, 3, 4, 5][1...*][*...=2].toList = [2, 3, 4] := by simp example : #[1, 2, 3, 4, 5][1...*][*...*].toList = [2, 3, 4, 5] := by simp example : #[1, 2, 3][0...2][*...*].toList = [1, 2] := by simp + +set_option backward.isDefEq.respectTransparency.types false -- FIXME + example : #[1, 2, 3][0...2][1...2].toArray = #[2] := by simp example : #[1, 2, 3][0...2][1...5].toArray = #[2] := by simp example : #[1, 2, 3][1...2][0...2].toArray = #[2] := by simp diff --git a/tests/elab/sym_pattern_3.lean b/tests/elab/sym_pattern_3.lean index 504c223f71ad..cc841f192ec3 100644 --- a/tests/elab/sym_pattern_3.lean +++ b/tests/elab/sym_pattern_3.lean @@ -14,7 +14,6 @@ theorem Exec.bind (k₁ : M α) (k₂ : α → M β) (post : β → S → Prop) Exec s k₁ (fun a s₁ => Exec s₁ (k₂ a) post) → Exec s (k₁ >>= k₂) post := by simp [Exec, Bind.bind, StateT.bind] - cases k₁ s; simp def goal := ∀ a b, Exec b (set a >>= fun _ => get) fun v _ => v = a set_option pp.explicit true diff --git a/tests/elab/symbolFrequency_foldRelevantConsts.lean b/tests/elab/symbolFrequency_foldRelevantConsts.lean index d4d14adac082..3a109ad612af 100644 --- a/tests/elab/symbolFrequency_foldRelevantConsts.lean +++ b/tests/elab/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, HAdd.hAdd, OfNat.ofNat, Array.swap, Not] -/ +/-- info: [Array, Nat, LT.lt, HAdd.hAdd, OfNat.ofNat, Array.swap] -/ #guard_msgs in run_meta do let ci ← getConstInfo `Array.eraseIdx.induct diff --git a/tests/elab_bench/cbv_aes.lean b/tests/elab_bench/cbv_aes.lean index 417c6281552c..a476de1eb28c 100644 --- a/tests/elab_bench/cbv_aes.lean +++ b/tests/elab_bench/cbv_aes.lean @@ -279,6 +279,7 @@ namespace AESArm open BitVec def WordSize := 32 +@[implicit_reducible] def BlockSize := 128 def Rcon : List (BitVec WordSize) := @@ -306,6 +307,7 @@ structure KBR where h : block_size = BlockSize deriving DecidableEq, Repr +@[implicit_reducible] def AES128KBR : KBR := {key_len := 128, block_size := BlockSize, Nr := 10, h := by decide} def AES192KBR : KBR := diff --git a/tests/elab_fail/simp_trace.lean.out.expected b/tests/elab_fail/simp_trace.lean.out.expected index 1392a09d93a1..cd717661d616 100644 --- a/tests/elab_fail/simp_trace.lean.out.expected +++ b/tests/elab_fail/simp_trace.lean.out.expected @@ -43,7 +43,7 @@ Try this: simp only [g, pure] [Meta.Tactic.simp.rewrite] unfold g, g x ==> (have x := x; pure x).run Try this: simp (config := { unfoldPartialApp := true }) only [f1, modify, modifyGet, MonadStateOf.modifyGet, - StateT.modifyGet, pure, f2, bind, StateT.bind, get, getThe, MonadStateOf.get, StateT.get, set, StateT.set] + StateT.modifyGet, pure, f2, bind, StateT.bind, set, StateT.set, StateT.get] [Meta.Tactic.simp.rewrite] unfold f1, f1 ==> modify fun x => g x [Meta.Tactic.simp.rewrite] unfold modify, modify fun x => g x ==> modifyGet fun s => (PUnit.unit, (fun x => g x) s) [Meta.Tactic.simp.rewrite] unfold StateT.modifyGet, StateT.modifyGet fun s => @@ -55,9 +55,9 @@ Try this: simp (config := { unfoldPartialApp := true }) only [f1, modify, modify let __x ← get s match __x with | (a, s) => (fun s => set (g s)) a s -[Meta.Tactic.simp.rewrite] unfold getThe, getThe Nat s ==> MonadStateOf.get s +[Meta.Tactic.simp.rewrite] unfold StateT.set, StateT.set (g (StateT.get s).fst) + (StateT.get s).snd ==> pure (PUnit.unit, g (StateT.get s).fst) [Meta.Tactic.simp.rewrite] unfold StateT.get, StateT.get s ==> pure (s, s) -[Meta.Tactic.simp.rewrite] unfold StateT.set, StateT.set (g s) s ==> pure (PUnit.unit, g s) [Meta.Tactic.simp.rewrite] eq_self:1000: (fun s => (PUnit.unit, g s)) = fun s => (PUnit.unit, g s) ==>