From dd78012ddd3f848fe48e0d173f2a0fb4682cddf4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Miyahara=20K=C5=8D?= <52843868+Komyyy@users.noreply.github.com> Date: Fri, 20 Jun 2025 16:47:33 +0900 Subject: [PATCH] =?UTF-8?q?style:=20replace=20`HEq=20x=20y`=20with=20`x=20?= =?UTF-8?q?=E2=89=8D=20y`=20(#8872)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Although `HEq` was abbreviated as `≍` in #8503, many instances of the form `HEq x y` still remain. Therefore, I searched for occurrences of `HEq x y` using the regular expression `(? apply p₁.symm.subset <;> assumption theorem Perm.rec_heq {β : List α → Sort _} {f : ∀ a l, β l → β (a :: l)} {b : β []} {l l' : List α} - (hl : l ~ l') (f_congr : ∀ {a l l' b b'}, l ~ l' → HEq b b' → HEq (f a l b) (f a l' b')) - (f_swap : ∀ {a a' l b}, HEq (f a (a' :: l) (f a' l b)) (f a' (a :: l) (f a l b))) : - HEq (@List.rec α β b f l) (@List.rec α β b f l') := by + (hl : l ~ l') (f_congr : ∀ {a l l' b b'}, l ~ l' → b ≍ b' → f a l b ≍ f a l' b') + (f_swap : ∀ {a a' l b}, f a (a' :: l) (f a' l b) ≍ f a' (a :: l) (f a l b)) : + @List.rec α β b f l ≍ @List.rec α β b f l' := by induction hl with | nil => rfl | cons a h ih => exact f_congr h ih diff --git a/src/Init/Grind/Util.lean b/src/Init/Grind/Util.lean index 96e98de29d..06320cebf3 100644 --- a/src/Init/Grind/Util.lean +++ b/src/Init/Grind/Util.lean @@ -53,7 +53,7 @@ will not eliminate it. After we apply `simp`, we replace it with `MatchCond`. -/ def PreMatchCond (p : Prop) : Prop := p -theorem nestedProof_congr (p q : Prop) (h : p = q) (hp : p) (hq : q) : HEq (@nestedProof p hp) (@nestedProof q hq) := by +theorem nestedProof_congr (p q : Prop) (h : p = q) (hp : p) (hq : q) : @nestedProof p hp ≍ @nestedProof q hq := by subst h; apply HEq.refl @[app_unexpander nestedProof] diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 29d1f623fe..4a1e6be980 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -470,16 +470,16 @@ Unsafe auxiliary constant used by the compiler to erase `Quot.lift`. unsafe axiom Quot.lcInv {α : Sort u} {r : α → α → Prop} (q : Quot r) : α /-- -Heterogeneous equality. `HEq a b` asserts that `a` and `b` have the same +Heterogeneous equality. `a ≍ b` asserts that `a` and `b` have the same type, and casting `a` across the equality yields `b`, and vice versa. You should avoid using this type if you can. Heterogeneous equality does not have all the same properties as `Eq`, because the assumption that the types of `a` and `b` are equal is often too weak to prove theorems of interest. One -important non-theorem is the analogue of `congr`: If `HEq f g` and `HEq x y` -and `f x` and `g y` are well typed it does not follow that `HEq (f x) (g y)`. +important non-theorem is the analogue of `congr`: If `f ≍ g` and `x ≍ y` +and `f x` and `g y` are well typed it does not follow that `f x ≍ g y`. (This does follow if you have `f = g` instead.) However if `a` and `b` have -the same type then `a = b` and `HEq a b` are equivalent. +the same type then `a = b` and `a ≍ b` are equivalent. -/ inductive HEq : {α : Sort u} → α → {β : Sort u} → β → Prop where /-- Reflexivity of heterogeneous equality. -/ diff --git a/src/Init/PropLemmas.lean b/src/Init/PropLemmas.lean index 914b31443a..81e03923a5 100644 --- a/src/Init/PropLemmas.lean +++ b/src/Init/PropLemmas.lean @@ -25,7 +25,7 @@ set_option linter.missingDocs true -- keep it documented @[simp] theorem eq_true_eq_id : Eq True = id := by funext _; simp only [true_iff, id_def, eq_iff_iff] -theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) : HEq hp hq := by +theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) : hp ≍ hq := by cases propext (iff_of_true hp hq); rfl /-! ## not -/ diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 8f8125d79e..ab3eac9bb2 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -1170,7 +1170,7 @@ macro "exists " es:term,+ : tactic => `(tactic| (refine ⟨$es,*, ?_⟩; try trivial)) /-- -Apply congruence (recursively) to goals of the form `⊢ f as = f bs` and `⊢ HEq (f as) (f bs)`. +Apply congruence (recursively) to goals of the form `⊢ f as = f bs` and `⊢ f as ≍ f bs`. The optional parameter is the depth of the recursive applications. This is useful when `congr` is too aggressive in breaking down the goal. For example, given `⊢ f (g (x + y)) = f (g (y + x))`, diff --git a/src/Lean/Elab/Tactic/Ext.lean b/src/Lean/Elab/Tactic/Ext.lean index 8b0b8e1762..7f65640cbe 100644 --- a/src/Lean/Elab/Tactic/Ext.lean +++ b/src/Lean/Elab/Tactic/Ext.lean @@ -30,7 +30,7 @@ states that two structures are equal if their fields are equal. Calls the continuation `k` with the list of parameters to the structure, two structure variables `x` and `y`, and a list of pairs `(field, ty)` -where each `ty` is of the form `x.field = y.field` or `HEq x.field y.field`. +where each `ty` is of the form `x.field = y.field` or `x.field ≍ y.field`. If `flat` parses to `true`, any fields inherited from parent structures are treated as fields of the given structure type. diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean index 35024b6b2b..182906b52c 100644 --- a/src/Lean/Meta/AppBuilder.lean +++ b/src/Lean/Meta/AppBuilder.lean @@ -57,7 +57,7 @@ def mkEq (a b : Expr) : MetaM Expr := do let u ← getLevel aType return mkApp3 (mkConst ``Eq [u]) aType a b -/-- Returns `HEq a b`. -/ +/-- Returns `a ≍ b`. -/ def mkHEq (a b : Expr) : MetaM Expr := do let aType ← inferType a let bType ← inferType b @@ -65,7 +65,7 @@ def mkHEq (a b : Expr) : MetaM Expr := do return mkApp4 (mkConst ``HEq [u]) aType a bType b /-- - If `a` and `b` have definitionally equal types, returns `Eq a b`, otherwise returns `HEq a b`. + If `a` and `b` have definitionally equal types, returns `a = b`, otherwise returns `a ≍ b`. -/ def mkEqHEq (a b : Expr) : MetaM Expr := do let aType ← inferType a @@ -82,7 +82,7 @@ def mkEqRefl (a : Expr) : MetaM Expr := do let u ← getLevel aType return mkApp2 (mkConst ``Eq.refl [u]) aType a -/-- Returns a proof of `HEq a a`. -/ +/-- Returns a proof of `a ≍ a`. -/ def mkHEqRefl (a : Expr) : MetaM Expr := do let aType ← inferType a let u ← getLevel aType @@ -148,7 +148,7 @@ def mkEqTrans? (h₁? h₂? : Option Expr) : MetaM (Option Expr) := | some h, none => return h | some h₁, some h₂ => mkEqTrans h₁ h₂ -/-- Given `h : HEq a b`, returns a proof of `HEq b a`. -/ +/-- Given `h : a ≍ b`, returns a proof of `b ≍ a`. -/ def mkHEqSymm (h : Expr) : MetaM Expr := do if h.isAppOf ``HEq.refl then return h @@ -161,7 +161,7 @@ def mkHEqSymm (h : Expr) : MetaM Expr := do | none => throwAppBuilderException ``HEq.symm ("heterogeneous equality proof expected" ++ hasTypeMsg h hType) -/-- Given `h₁ : HEq a b`, `h₂ : HEq b c`, returns a proof of `HEq a c`. -/ +/-- Given `h₁ : a ≍ b`, `h₂ : b ≍ c`, returns a proof of `a ≍ c`. -/ def mkHEqTrans (h₁ h₂ : Expr) : MetaM Expr := do if h₁.isAppOf ``HEq.refl then return h₂ @@ -177,7 +177,7 @@ def mkHEqTrans (h₁ h₂ : Expr) : MetaM Expr := do | none, _ => throwAppBuilderException ``HEq.trans ("heterogeneous equality proof expected" ++ hasTypeMsg h₁ hType₁) | _, none => throwAppBuilderException ``HEq.trans ("heterogeneous equality proof expected" ++ hasTypeMsg h₂ hType₂) -/-- Given `h : HEq a b` where `a` and `b` have the same type, returns a proof of `Eq a b`. -/ +/-- Given `h : a ≍ b` where `a` and `b` have the same type, returns a proof of `a = b`. -/ def mkEqOfHEq (h : Expr) (check := true) : MetaM Expr := do let hType ← infer h match hType.heq? with @@ -190,7 +190,7 @@ def mkEqOfHEq (h : Expr) (check := true) : MetaM Expr := do | _ => throwAppBuilderException ``eq_of_heq m!"heterogeneous equality proof expected{indentExpr h}" -/-- Given `h : Eq a b`, returns a proof of `HEq a b`. -/ +/-- Given `h : a = b`, returns a proof of `a ≍ b`. -/ def mkHEqOfEq (h : Expr) : MetaM Expr := do let hType ← infer h let some (α, a, b) := hType.eq? diff --git a/src/Lean/Meta/CongrTheorems.lean b/src/Lean/Meta/CongrTheorems.lean index 6bc8dc7d1d..4a3d1e831a 100644 --- a/src/Lean/Meta/CongrTheorems.lean +++ b/src/Lean/Meta/CongrTheorems.lean @@ -28,7 +28,7 @@ inductive CongrArgKind where They correspond to arguments that are subsingletons/propositions. -/ | cast /-- - The lemma contains three parameters for this kind of argument `a_i`, `b_i` and `eq_i : HEq a_i b_i`. + The lemma contains three parameters for this kind of argument `a_i`, `b_i` and `eq_i : a_i ≍ b_i`. `a_i` and `b_i` represent the left and right hand sides, and `eq_i` is a proof for their heterogeneous equality. -/ | heq /-- diff --git a/src/Lean/Meta/Injective.lean b/src/Lean/Meta/Injective.lean index b72dc8437b..aca1f93cae 100644 --- a/src/Lean/Meta/Injective.lean +++ b/src/Lean/Meta/Injective.lean @@ -47,7 +47,7 @@ def elimOptParam (type : Expr) : CoreM Expr := do ```lean theorem Tmₛ.app.inj {T : Type u} {A : T → Tyₛ} {a : Tmₛ (Tyₛ.SPi T A)} {arg : T} {T_1 : Type u} {a_1 : Tmₛ (Tyₛ.SPi T_1 A)} : Tmₛ.app a arg = Tmₛ.app a_1 arg → - T = T_1 ∧ HEq a a_1 := fun x => Tmₛ.noConfusion x fun T_eq A_eq a_eq arg_eq => eq_of_heq a_eq + T = T_1 ∧ a ≍ a_1 := fun x => Tmₛ.noConfusion x fun T_eq A_eq a_eq arg_eq => eq_of_heq a_eq ``` Instead of checking the type of every subterm, we only need to check the type of free variables, since free variables introduced in the constructor may only appear in the type of other free variables introduced after them. diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean index 054bacb936..6e98a16ebd 100644 --- a/src/Lean/Meta/Match/MatchEqs.lean +++ b/src/Lean/Meta/Match/MatchEqs.lean @@ -544,15 +544,15 @@ where (t₂ : Foo l₂) → ((s₁ : Foo l₂) → motive (Foo.cons s₁)) → ((x : Foo l₂) → motive x) → motive t₂ := fun {l₂} t₂ motive t₂_1 h_1 h_2 => (fun t₂_2 => - Foo.casesOn (motive := fun a x => l₂ = a → HEq t₂_1 x → motive t₂_1) t₂_2 + Foo.casesOn (motive := fun a x => l₂ = a → t₂_1 ≍ x → motive t₂_1) t₂_2 (fun h => Eq.ndrec (motive := fun {l₂} => (t₂ t₂ : Foo l₂) → (motive : Foo l₂ → Sort u_1) → - ((s₁ : Foo l₂) → motive (Foo.cons s₁)) → ((x : Foo l₂) → motive x) → HEq t₂ Foo.nil → motive t₂) + ((s₁ : Foo l₂) → motive (Foo.cons s₁)) → ((x : Foo l₂) → motive x) → t₂ ≍ Foo.nil → motive t₂) (fun t₂ t₂ motive h_1 h_2 h => Eq.symm (eq_of_heq h) ▸ h_2 Foo.nil) (Eq.symm h) t₂ t₂_1 motive h_1 h_2) --- HERE fun {l} t h => - Eq.ndrec (motive := fun {l} => (t : Foo l) → HEq t₂_1 (Foo.cons t) → motive t₂_1) + Eq.ndrec (motive := fun {l} => (t : Foo l) → t₂_1 ≍ Foo.cons t → motive t₂_1) (fun t h => Eq.symm (eq_of_heq h) ▸ h_1 t) h t) t₂_1 (Eq.refl l₂) (HEq.refl t₂_1) ``` diff --git a/src/Lean/Meta/Match/MatcherApp/Transform.lean b/src/Lean/Meta/Match/MatcherApp/Transform.lean index 7e7e8d9a07..2ab42bd4b0 100644 --- a/src/Lean/Meta/Match/MatcherApp/Transform.lean +++ b/src/Lean/Meta/Match/MatcherApp/Transform.lean @@ -246,7 +246,7 @@ def transform throwError "unexpected matcher application, motive must be lambda expression with #{matcherApp.discrs.size} arguments" let mut motiveBody' ← onMotive motiveArgs motiveBody - -- Prepend `(x = e) →` or `(HEq x e) → ` to the motive when an equality is requested + -- Prepend `(x = e) →` or `(x ≍ e) → ` to the motive when an equality is requested -- and not already present, and remember whether we added an Eq or a HEq let mut addHEqualities : Array (Option Bool) := #[] for arg in motiveArgs, discr in discrs', di in matcherApp.discrInfos do diff --git a/src/Lean/Meta/Tactic/Congr.lean b/src/Lean/Meta/Tactic/Congr.lean index 518ffe646c..bc30a4e5b3 100644 --- a/src/Lean/Meta/Tactic/Congr.lean +++ b/src/Lean/Meta/Tactic/Congr.lean @@ -74,7 +74,7 @@ def MVarId.congrImplies? (mvarId : MVarId) : MetaM (Option (List MVarId)) := return [mvarId₁, mvarId₂] /-- -Given a goal of the form `⊢ f as = f bs`, `⊢ (p → q) = (p' → q')`, or `⊢ HEq (f as) (f bs)`, try to apply congruence. +Given a goal of the form `⊢ f as = f bs`, `⊢ (p → q) = (p' → q')`, or `⊢ f as ≍ f bs`, try to apply congruence. It takes proof irrelevance into account, and the fact that `Decidable p` is a subsingleton. -/ def MVarId.congrCore (mvarId : MVarId) : MetaM (List MVarId) := do @@ -88,7 +88,7 @@ def MVarId.congrCore (mvarId : MVarId) : MetaM (List MVarId) := do throwTacticEx `congr mvarId "failed to apply congruence" /-- -Given a goal of the form `⊢ f as = f bs`, `⊢ (p → q) = (p' → q')`, or `⊢ HEq (f as) (f bs)`, try to apply congruence. +Given a goal of the form `⊢ f as = f bs`, `⊢ (p → q) = (p' → q')`, or `⊢ f as ≍ f bs`, try to apply congruence. It takes proof irrelevance into account, and the fact that `Decidable p` is a subsingleton. * Applies `congr` recursively up to depth `depth`. diff --git a/src/Lean/Meta/Tactic/Contradiction.lean b/src/Lean/Meta/Tactic/Contradiction.lean index 0b16d48327..4bc2cff31b 100644 --- a/src/Lean/Meta/Tactic/Contradiction.lean +++ b/src/Lean/Meta/Tactic/Contradiction.lean @@ -178,7 +178,7 @@ def _root_.Lean.MVarId.contradictionCore (mvarId : MVarId) (config : Contradicti mvarId.assign (← mkNoConfusion (← mvarId.getType) localDecl.toExpr) return true let mut isHEq := false - -- (h : HEq (ctor₁ ...) (ctor₂ ...)) + -- (h : ctor₁ ... ≍ ctor₂ ...) if let some (α, lhs, β, rhs) ← matchHEq? localDecl.type then isHEq := true if let some lhsCtor ← matchConstructorApp? lhs then diff --git a/src/Lean/Meta/Tactic/Grind/Canon.lean b/src/Lean/Meta/Tactic/Grind/Canon.lean index b5abb9eba1..c079a52fa2 100644 --- a/src/Lean/Meta/Tactic/Grind/Canon.lean +++ b/src/Lean/Meta/Tactic/Grind/Canon.lean @@ -38,7 +38,7 @@ but it does not solve all problems. For example, consider a situation where we h and `(b : BitVec m)`, along with instances `inst1 n : Add (BitVec n)` and `inst2 m : Add (BitVec m)` where `inst1` and `inst2` are structurally different. Now consider the terms `a + a` and `b + b`. After canonicalization, the two additions will still use structurally different (and definitionally different) instances: `inst1 n` and `inst2 m`. -Furthermore, `grind` will not be able to infer that `HEq (a + a) (b + b)` even if we add the assumptions `n = m` and `HEq a b`. +Furthermore, `grind` will not be able to infer that `a + a ≍ b + b` even if we add the assumptions `n = m` and `a ≍ b`. -/ @[inline] private def get' : GoalM State := diff --git a/src/Lean/Meta/Tactic/Grind/Core.lean b/src/Lean/Meta/Tactic/Grind/Core.lean index cd5725d2fe..cac7c6bb29 100644 --- a/src/Lean/Meta/Tactic/Grind/Core.lean +++ b/src/Lean/Meta/Tactic/Grind/Core.lean @@ -353,7 +353,7 @@ private def addEqCore (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit := do private def addEq (lhs rhs proof : Expr) : GoalM Unit := do addEqCore lhs rhs proof false -/-- Adds a new heterogeneous equality `HEq lhs rhs`. It assumes `lhs` and `rhs` have already been internalized. -/ +/-- Adds a new heterogeneous equality `lhs ≍ rhs`. It assumes `lhs` and `rhs` have already been internalized. -/ private def addHEq (lhs rhs proof : Expr) : GoalM Unit := do addEqCore lhs rhs proof true diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean index 12cf2bc8c8..31e2d71297 100644 --- a/src/Lean/Meta/Tactic/Grind/Internalize.lean +++ b/src/Lean/Meta/Tactic/Grind/Internalize.lean @@ -112,7 +112,7 @@ private def checkAndAddSplitCandidate (e : Expr) : GoalM Unit := do | _ => pure () /-- -If `e` is a `cast`-like term (e.g., `cast h a`), add `HEq e a` to the to-do list. +If `e` is a `cast`-like term (e.g., `cast h a`), add `e ≍ a` to the to-do list. It could be an E-matching theorem, but we want to ensure it is always applied since we want to rely on the fact that `cast h a` and `a` are in the same equivalence class. -/ diff --git a/src/Lean/Meta/Tactic/Grind/MatchCond.lean b/src/Lean/Meta/Tactic/Grind/MatchCond.lean index 318ae450e3..31d19342f0 100644 --- a/src/Lean/Meta/Tactic/Grind/MatchCond.lean +++ b/src/Lean/Meta/Tactic/Grind/MatchCond.lean @@ -152,14 +152,14 @@ Gruesome details for heterogenenous equalities. When pattern matching on indexing families, the generated conditions often use heterogenenous equalities. Here is an example: ``` -(∀ (x : Vec α 0), n = 0 → HEq as Vec.nil → HEq bs x → False) +(∀ (x : Vec α 0), n = 0 → as ≍ Vec.nil → bs ≍ x → False) ``` In this case, it is not sufficient to abstract the left-hand side. We also have to abstract its type. The following is produced in this case. ``` (#[n, Vec α n, as, Vec α n, bs], (fun (x_0 : Nat) (ty_1 : Type u_1) (x_1 : ty_1) (ty_2 : Type u_1) (x_2 : ty_2) => - ∀ (x : Vec α 0), x_0 = 0 → HEq x_1 Vec.nil → HEq x_2 x → False) + ∀ (x : Vec α 0), x_0 = 0 → x_1 ≍ Vec.nil → x_2 ≍ x → False) n (Vec α n) as (Vec α n) bs) ``` The example makes it clear why this is needed, `as` and `bs` depend on `n`. diff --git a/src/Lean/Meta/Tactic/Grind/Proof.lean b/src/Lean/Meta/Tactic/Grind/Proof.lean index 1853b71d47..59f959820f 100644 --- a/src/Lean/Meta/Tactic/Grind/Proof.lean +++ b/src/Lean/Meta/Tactic/Grind/Proof.lean @@ -35,7 +35,7 @@ private def mkTrans' (h₁ : Option Expr) (h₂ : Expr) (heq : Bool) : MetaM Exp mkTrans h₁ h₂ heq /-- -Given `h : HEq a b`, returns a proof `a = b` if `heq == false`. +Given `h : a ≍ b`, returns a proof `a = b` if `heq == false`. Otherwise, it returns `h`. -/ private def mkEqOfHEqIfNeeded (h : Expr) (heq : Bool) : MetaM Expr := do @@ -94,7 +94,7 @@ private partial def isCongrDefaultProofTarget (lhs rhs : Expr) (f g : Expr) (num mutual /-- Given `lhs` and `rhs` proof terms of the form `nestedProof p hp` and `nestedProof q hq`, - constructs a congruence proof for `HEq (nestedProof p hp) (nestedProof q hq)`. + constructs a congruence proof for `nestedProof p hp ≍ nestedProof q hq`. `p` and `q` are in the same equivalence class. -/ private partial def mkNestedProofCongr (lhs rhs : Expr) (heq : Bool) : GoalM Expr := do @@ -152,8 +152,8 @@ mutual /- `lhs` is of the form `f a_1 ... a_n` `rhs` is of the form `g b_1 ... b_n` - `proof : HEq (f a_1 ... a_n) (f b_1 ... b_n)` - We construct a proof for `HEq (f a_1 ... a_n) (g b_1 ... b_n)` using `Eq.ndrec` + `proof : f a_1 ... a_n ≍ f b_1 ... b_n` + We construct a proof for `f a_1 ... a_n ≍ g b_1 ... b_n` using `Eq.ndrec` -/ let motive ← withLocalDeclD (← mkFreshUserName `x) (← inferType f) fun x => do mkLambdaFVars #[x] (← mkHEq lhs (mkAppN x rhs.getAppArgs)) @@ -226,7 +226,7 @@ mutual mkTrans' h' h heq /-- - Returns a proof of `lhs = rhs` (`HEq lhs rhs`) if `heq = false` (`heq = true`). + Returns a proof of `lhs = rhs` (`lhs ≍ rhs`) if `heq = false` (`heq = true`). If `heq = false`, this function assumes that `lhs` and `rhs` have the same type. -/ private partial def mkEqProofCore (lhs rhs : Expr) (heq : Bool) : GoalM Expr := do diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean index 820a1d17d1..83bb66281a 100644 --- a/src/Lean/Meta/Tactic/Grind/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Types.lean @@ -914,7 +914,7 @@ def Goal.getTarget? (goal : Goal) (e : Expr) : Option Expr := Id.run do /-- If `isHEq` is `false`, it pushes `lhs = rhs` with `proof` to `newEqs`. -Otherwise, it pushes `HEq lhs rhs`. +Otherwise, it pushes `lhs ≍ rhs`. -/ def pushEqCore (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit := do if grind.debug.get (← getOptions) then @@ -945,7 +945,7 @@ def hasSameType (a b : Expr) : MetaM Bool := @[inline] def pushEq (lhs rhs proof : Expr) : GoalM Unit := pushEqCore lhs rhs proof (isHEq := false) -/-- Pushes `HEq lhs rhs` with `proof` to `newEqs`. -/ +/-- Pushes `lhs ≍ rhs` with `proof` to `newEqs`. -/ @[inline] def pushHEq (lhs rhs proof : Expr) : GoalM Unit := pushEqCore lhs rhs proof (isHEq := true) @@ -1260,7 +1260,7 @@ It assumes `a` and `b` are in the same equivalence class, and have the same type opaque mkEqProof (a b : Expr) : GoalM Expr /-- -Returns a proof that `HEq a b`. +Returns a proof that `a ≍ b`. It assumes `a` and `b` are in the same equivalence class. -/ -- Forward definition @@ -1276,7 +1276,7 @@ opaque internalize (e : Expr) (generation : Nat) (parent? : Option Expr := none) opaque processNewFacts : GoalM Unit /-- -Returns a proof that `a = b` if they have the same type. Otherwise, returns a proof of `HEq a b`. +Returns a proof that `a = b` if they have the same type. Otherwise, returns a proof of `a ≍ b`. It assumes `a` and `b` are in the same equivalence class. -/ def mkEqHEqProof (a b : Expr) : GoalM Expr := do diff --git a/src/Lean/Meta/Tactic/Subst.lean b/src/Lean/Meta/Tactic/Subst.lean index b061399cce..7749269dd6 100644 --- a/src/Lean/Meta/Tactic/Subst.lean +++ b/src/Lean/Meta/Tactic/Subst.lean @@ -117,7 +117,7 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst : m!"invalid equality proof, it is not of the form {eqMsg}{indentExpr hLocalDecl.type}\nafter WHNF, variable expected, but obtained{indentExpr a}" /-- - Given `h : HEq α a α b` in the given goal, produce a new goal where `h : Eq α a b`. + Given `h : @HEq α a α b` in the given goal, produce a new goal where `h : @Eq α a b`. If `h` is not of the give form, then just return `(h, mvarId)` -/ def heqToEq (mvarId : MVarId) (fvarId : FVarId) (tryToClear : Bool := true) : MetaM (FVarId × MVarId) := diff --git a/src/Std/Data/Iterators/Lemmas/Equivalence/StepCongr.lean b/src/Std/Data/Iterators/Lemmas/Equivalence/StepCongr.lean index b55502a6e6..9b981e9040 100644 --- a/src/Std/Data/Iterators/Lemmas/Equivalence/StepCongr.lean +++ b/src/Std/Data/Iterators/Lemmas/Equivalence/StepCongr.lean @@ -92,7 +92,7 @@ private theorem IterM.Equiv.step_eq.aux {α₁ α₂ : Type w} {m : Type w → T private theorem IterM.Equiv.step_eq.aux_subtypeMk_congr {α : Type u} {P Q R : α → Prop} {h₁ : ∀ a, P a → R a} {h₂ : ∀ a, Q a → R a} (h : P = Q) : - HEq (fun (a : α) (ha : P a) => Subtype.mk a (h₁ a ha)) + (fun (a : α) (ha : P a) => Subtype.mk a (h₁ a ha)) ≍ (fun (a : α) (ha : Q a) => Subtype.mk a (h₂ a ha)) := by cases h simp diff --git a/tests/lean/223.lean b/tests/lean/223.lean index c44647b8a9..ce4b0e5098 100644 --- a/tests/lean/223.lean +++ b/tests/lean/223.lean @@ -7,8 +7,7 @@ def h {α β} {f : α → β} : {b : β} → Imf f b → α | _, Imf.mk a => a #print h -infix:50 " ≅ " => HEq -theorem ex : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≅ a +theorem ex : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≍ a | α, _, rfl, a => HEq.refl a #print ex diff --git a/tests/lean/223.lean.expected.out b/tests/lean/223.lean.expected.out index 394bd67842..6a13a1a718 100644 --- a/tests/lean/223.lean.expected.out +++ b/tests/lean/223.lean.expected.out @@ -2,7 +2,7 @@ def h.{u_1, u_2} : {α : Type u_1} → {β : Type u_2} → {f : α → β} → { fun {α} {β} {f} x x_1 => match x, x_1 with | .(f a), Imf.mk a => a -theorem ex.{u} : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≅ a := +theorem ex.{u} : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≍ a := fun x x_1 x_2 x_3 => match x, x_1, x_2, x_3 with | α, .(α), Eq.refl α, a => HEq.refl a diff --git a/tests/lean/calcErrors.lean b/tests/lean/calcErrors.lean index b79ed83cb9..6b85abc226 100644 --- a/tests/lean/calcErrors.lean +++ b/tests/lean/calcErrors.lean @@ -32,23 +32,22 @@ theorem ex5 (p : Nat → Nat → Prop) (a b : Nat) (h₁ : p a b) (h₂ : p b c) /-! Relation with bad signature -/ -infix:50 " ≅ " => HEq -instance {α β γ} : Trans (· ≅ · : α → β → Prop) (· ≅ · : β → γ → Prop) (· ≅ · : α → γ → Prop) where +instance {α β γ} : Trans (· ≍ · : α → β → Prop) (· ≍ · : β → γ → Prop) (· ≍ · : α → γ → Prop) where trans h₁ h₂ := HEq.trans h₁ h₂ -theorem ex6 {a : α} {b : β} {c : γ} (h₁ : HEq a b) (h₂ : b ≅ c) : a ≅ c := - calc a ≅ b := h₁ - _ ≅ c := h₂ -- Error because the last two arguments of HEq are not explicit +theorem ex6 {a : α} {b : β} {c : γ} (h₁ : a ≍ b) (h₂ : b ≍ c) : a ≍ c := + calc a ≍ b := h₁ + _ ≍ c := h₂ -- Error because the last two arguments of HEq are not explicit -- fixed -abbrev HEqRel {α β} (a : α) (b : β) := HEq a b +abbrev HEqRel {α β} (a : α) (b : β) := a ≍ b infix:50 "===" => HEqRel instance {α β γ} : Trans (HEqRel : α → β → Prop) (HEqRel : β → γ → Prop) (HEqRel : α → γ → Prop) where trans h₁ h₂ := HEq.trans h₁ h₂ -theorem ex7 {a : α} {b : β} {c : γ} (h₁ : a ≅ b) (h₂ : b ≅ c) : a === c := +theorem ex7 {a : α} {b : β} {c : γ} (h₁ : a ≍ b) (h₂ : b ≍ c) : a === c := calc a === b := h₁ _ === c := h₂ diff --git a/tests/lean/calcErrors.lean.expected.out b/tests/lean/calcErrors.lean.expected.out index b5ce9626ca..dc185115a9 100644 --- a/tests/lean/calcErrors.lean.expected.out +++ b/tests/lean/calcErrors.lean.expected.out @@ -14,8 +14,8 @@ calcErrors.lean:31:8-31:13: error: invalid 'calc' step, failed to synthesize `Tr Trans p p ?m Additional diagnostic information may be available using the `set_option diagnostics true` command. -calcErrors.lean:41:7-41:12: error: invalid 'calc' step, left-hand side is +calcErrors.lean:40:7-40:12: error: invalid 'calc' step, left-hand side is γ : Sort u_1 but previous right-hand side is b : β -calcErrors.lean:61:18-61:19: error: unexpected token '['; expected command +calcErrors.lean:60:18-60:19: error: unexpected token '['; expected command diff --git a/tests/lean/doSeqRightIssue.lean b/tests/lean/doSeqRightIssue.lean index b050dd9450..e26cd43e14 100644 --- a/tests/lean/doSeqRightIssue.lean +++ b/tests/lean/doSeqRightIssue.lean @@ -3,7 +3,6 @@ set_option autoImplicit false universe u variable {α : Type u} variable {β : α → Type v} -infix:50 " ≅ " => HEq -theorem ex {p₁ p₂ : Sigma (fun a => β a)} (h₁ : p₁.1 = p₂.1) (h : p₁.2 ≅ p₂.2) : p₁ = p₂ := +theorem ex {p₁ p₂ : Sigma (fun a => β a)} (h₁ : p₁.1 = p₂.1) (h : p₁.2 ≍ p₂.2) : p₁ = p₂ := match p₁, p₂, h₁, h with | ⟨_, _⟩, ⟨_, _⟩, rfl, HEq.refl _ => rfl diff --git a/tests/lean/doSeqRightIssue.lean.expected.out b/tests/lean/doSeqRightIssue.lean.expected.out index 405f86ef10..93d9eec5f4 100644 --- a/tests/lean/doSeqRightIssue.lean.expected.out +++ b/tests/lean/doSeqRightIssue.lean.expected.out @@ -1,3 +1,3 @@ doSeqRightIssue.lean:5:23-5:24: error: unknown universe level 'v' -doSeqRightIssue.lean:8:0-9:40: warning: declaration uses 'sorry' -doSeqRightIssue.lean:7:8-7:10: warning: declaration uses 'sorry' +doSeqRightIssue.lean:7:0-8:40: warning: declaration uses 'sorry' +doSeqRightIssue.lean:6:8-6:10: warning: declaration uses 'sorry' diff --git a/tests/lean/match3.lean b/tests/lean/match3.lean index ddfad75da5..e1741e22f1 100644 --- a/tests/lean/match3.lean +++ b/tests/lean/match3.lean @@ -9,28 +9,27 @@ match x with #eval f 30 universe u -infix:50 " ≅ " => HEq -theorem ex1 {α : Sort u} {a b : α} (h : a ≅ b) : a = b := +theorem ex1 {α : Sort u} {a b : α} (h : a ≍ b) : a = b := match α, a, b, h with | _, _, _, HEq.refl _ => rfl -theorem ex2 {α : Sort u} {a b : α} (h : a ≅ b) : a = b := +theorem ex2 {α : Sort u} {a b : α} (h : a ≍ b) : a = b := match a, b, h with | _, _, HEq.refl _ => rfl -theorem ex3 {α : Sort u} {a b : α} (h : a ≅ b) : a = b := +theorem ex3 {α : Sort u} {a b : α} (h : a ≍ b) : a = b := match b, h with | _, HEq.refl _ => rfl -theorem ex4 {α β : Sort u} {b : β} {a a' : α} (h₁ : a = a') (h₂ : a' ≅ b) : a ≅ b := +theorem ex4 {α β : Sort u} {b : β} {a a' : α} (h₁ : a = a') (h₂ : a' ≍ b) : a ≍ b := match β, a', b, h₁, h₂ with | _, _, _, rfl, HEq.refl _ => HEq.refl _ -theorem ex5 {α β : Sort u} {b : β} {a a' : α} (h₁ : a = a') (h₂ : a' ≅ b) : a ≅ b := +theorem ex5 {α β : Sort u} {b : β} {a a' : α} (h₁ : a = a') (h₂ : a' ≍ b) : a ≍ b := match a', h₁, h₂ with | _, rfl, h₂ => h₂ -theorem ex6 {α β : Sort u} {b : β} {a a' : α} (h₁ : a = a') (h₂ : a' ≅ b) : a ≅ b := +theorem ex6 {α β : Sort u} {b : β} {a a' : α} (h₁ : a = a') (h₂ : a' ≍ b) : a ≍ b := by { subst h₁; assumption @@ -60,7 +59,7 @@ match a1, a2, h with universe v variable {β : α → Type v} -theorem ex9 {p₁ p₂ : Sigma (fun a => β a)} (h₁ : p₁.1 = p₂.1) (h : p₁.2 ≅ p₂.2) : p₁ = p₂ := +theorem ex9 {p₁ p₂ : Sigma (fun a => β a)} (h₁ : p₁.1 = p₂.1) (h : p₁.2 ≍ p₂.2) : p₁ = p₂ := match p₁, p₂, h₁, h with | ⟨_, _⟩, ⟨_, _⟩, rfl, HEq.refl _ => rfl diff --git a/tests/lean/ppMotives.lean b/tests/lean/ppMotives.lean index 79458499fd..528064d32f 100644 --- a/tests/lean/ppMotives.lean +++ b/tests/lean/ppMotives.lean @@ -6,7 +6,7 @@ set_option pp.motives.pi true #print Nat.add -theorem ex : ∀ {α β : Sort u} (h : α = β) (a : α), HEq (cast h a) a +theorem ex : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≍ a | α, _, rfl, a => HEq.refl a set_option pp.motives.nonConst false diff --git a/tests/lean/run/congrTactic.lean b/tests/lean/run/congrTactic.lean index fe21da83d1..d93ec82876 100644 --- a/tests/lean/run/congrTactic.lean +++ b/tests/lean/run/congrTactic.lean @@ -22,7 +22,7 @@ example (h : a = b) : f True (a + 1) (by simp +arith) = f (0 = 0) (b + 1) (by si · show a + 1 = b + 1 rw [h] -example (h₁ : α = β) (h₂ : α = γ) (a : α) : HEq (cast h₁ a) (cast h₂ a) := by +example (h₁ : α = β) (h₂ : α = γ) (a : α) : cast h₁ a ≍ cast h₂ a := by congr · subst h₁ h₂; rfl · subst h₁ h₂; apply heq_of_eq; rfl diff --git a/tests/lean/run/discrRefinement2.lean b/tests/lean/run/discrRefinement2.lean index ccaef6d862..d7a761d505 100644 --- a/tests/lean/run/discrRefinement2.lean +++ b/tests/lean/run/discrRefinement2.lean @@ -1,28 +1,27 @@ -infix:50 " ≅ " => HEq -theorem ex1 {α : Sort u} {a b : α} (h : a ≅ b) : a = b := +theorem ex1 {α : Sort u} {a b : α} (h : a ≍ b) : a = b := match h with | HEq.refl _ => rfl -def ex2 {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} (m : motive a) {β : Sort u2} {b : β} (h : a ≅ b) : motive b := +def ex2 {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} (m : motive a) {β : Sort u2} {b : β} (h : a ≍ b) : motive b := match h, m with | HEq.refl _, m => m -def ex3 {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a ≅ b) (h₂ : p a) : p b := +def ex3 {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a ≍ b) (h₂ : p a) : p b := match h₁, h₂ with | HEq.refl _, h₂ => h₂ -theorem ex4 {α β : Sort u} {a : α} {b : β} (h : a ≅ b) : b ≅ a := +theorem ex4 {α β : Sort u} {a : α} {b : β} (h : a ≍ b) : b ≍ a := match h with | HEq.refl _ => HEq.refl _ -theorem ex5 {α : Sort u} {a a' : α} (h : a = a') : a ≅ a' := +theorem ex5 {α : Sort u} {a a' : α} (h : a = a') : a ≍ a' := match h with | rfl => HEq.refl _ -theorem ex6 {α β : Sort u} (h : α = β) (a : α) : cast h a ≅ a := +theorem ex6 {α β : Sort u} (h : α = β) (a : α) : cast h a ≍ a := match h with | rfl => HEq.refl _ -theorem ex7 {α β σ : Sort u} {a : α} {b : β} {c : σ} (h₁ : a ≅ b) (h₂ : b ≅ c) : a ≅ c := +theorem ex7 {α β σ : Sort u} {a : α} {b : β} {c : σ} (h₁ : a ≍ b) (h₂ : b ≍ c) : a ≍ c := match h₁, h₂ with | HEq.refl _, HEq.refl _ => HEq.refl _ diff --git a/tests/lean/run/ext.lean b/tests/lean/run/ext.lean index 3c513dccbf..d9e3039474 100644 --- a/tests/lean/run/ext.lean +++ b/tests/lean/run/ext.lean @@ -22,7 +22,7 @@ example (a b : C n) : a = b := by ext guard_target = a.a = b.a; exact mySorry guard_target = a.b = b.b; exact mySorry - guard_target = HEq a.i b.i; exact mySorry + guard_target = a.i ≍ b.i; exact mySorry guard_target = a.c = b.c; exact mySorry @[ext (flat := false)] structure C' (n) extends B n where diff --git a/tests/lean/run/ext1.lean b/tests/lean/run/ext1.lean index 6df3c04ff3..f11b84d0a4 100644 --- a/tests/lean/run/ext1.lean +++ b/tests/lean/run/ext1.lean @@ -20,7 +20,7 @@ example (a b : C n) : a = b := by ext guard_target = a.a = b.a; exact mySorry guard_target = a.b = b.b; exact mySorry - guard_target = HEq a.i b.i; exact mySorry + guard_target = a.i ≍ b.i; exact mySorry guard_target = a.c = b.c; exact mySorry @[ext (flat := false)] structure C' (n) extends B n where diff --git a/tests/lean/run/grind_bool_prop.lean b/tests/lean/run/grind_bool_prop.lean index 1bb3c4a768..cfc409ad90 100644 --- a/tests/lean/run/grind_bool_prop.lean +++ b/tests/lean/run/grind_bool_prop.lean @@ -30,7 +30,7 @@ example (a b : Nat) : (a != b, c) = d → d = (false, true) → a = b := by grin example (a b : Bool) : (a ^^ b, c) = d → d = (false, true) → a = b := by grind (splits := 0) example (a b : Bool) : (a == b, c) = d → d = (true, true) → a = true → true = b := by grind (splits := 0) -example (h : α = β) (a : α) (b : β) : h ▸ a = b → HEq a b := by grind +example (h : α = β) (a : α) (b : β) : h ▸ a = b → a ≍ b := by grind example {α : Type u} [BEq α] [LawfulBEq α] (x : Nat) (a b : α) : x = (if a == b then 2 else 1) → x = (if (b == a) then 1 else 2) → False := by diff --git a/tests/lean/run/grind_congr1.lean b/tests/lean/run/grind_congr1.lean index d1faacb568..dd8d621bd4 100644 --- a/tests/lean/run/grind_congr1.lean +++ b/tests/lean/run/grind_congr1.lean @@ -23,18 +23,16 @@ example (a b c : Nat) (f : Nat → Nat → Nat) : a = b → c = b → f (f a b) example (a b c d : Nat) : a = b → b = c → c = d → a = d := by grind -infix:50 "===" => HEq - -example (a b c d : Nat) : a === b → b = c → c === d → a === d := by +example (a b c d : Nat) : a ≍ b → b = c → c ≍ d → a ≍ d := by grind -example (a b c d : Nat) : a = b → b = c → c === d → a === d := by +example (a b c d : Nat) : a = b → b = c → c ≍ d → a ≍ d := by grind opaque f {α : Type} : α → α → α := fun a _ => a opaque g : Nat → Nat -example (a b c : Nat) : a = b → g a === g b := by +example (a b c : Nat) : a = b → g a ≍ g b := by grind example (a b c : Nat) : a = b → c = b → f (f a b) (g c) = f (f c a) (g b) := by @@ -59,12 +57,12 @@ end Ex1 namespace Ex2 def f (α : Type) (a : α) : α := a -example (a : α) (b : β) : (h₁ : α = β) → (h₂ : HEq a b) → HEq (f α a) (f β b) := by +example (a : α) (b : β) : (h₁ : α = β) → (h₂ : a ≍ b) → f α a ≍ f β b := by grind end Ex2 -example (f g : (α : Type) → α → α) (a : α) (b : β) : (h₁ : α = β) → (h₂ : HEq a b) → (h₃ : f = g) → HEq (f α a) (g β b) := by +example (f g : (α : Type) → α → α) (a : α) (b : β) : (h₁ : α = β) → (h₂ : a ≍ b) → (h₃ : f = g) → f α a ≍ g β b := by grind set_option trace.grind.debug.proof true in @@ -83,15 +81,15 @@ theorem ex1 (f : {α : Type} → α → Nat → Bool → Nat) (a b c : Nat) : f example (n1 n2 n3 : Nat) (v1 w1 : Vector Nat n1) (w1' : Vector Nat n3) (v2 w2 : Vector Nat n2) : - n1 = n3 → v1 = w1 → HEq w1 w1' → v2 = w2 → HEq (v1 ++ v2) (w1' ++ w2) := by + n1 = n3 → v1 = w1 → w1 ≍ w1' → v2 = w2 → v1 ++ v2 ≍ w1' ++ w2 := by grind example (n1 n2 n3 : Nat) (v1 w1 : Vector Nat n1) (w1' : Vector Nat n3) (v2 w2 : Vector Nat n2) : - HEq n1 n3 → v1 = w1 → HEq w1 w1' → HEq v2 w2 → HEq (v1 ++ v2) (w1' ++ w2) := by + n1 ≍ n3 → v1 = w1 → w1 ≍ w1' → v2 ≍ w2 → v1 ++ v2 ≍ w1' ++ w2 := by grind theorem ex2 (n1 n2 n3 : Nat) (v1 w1 v : Vector Nat n1) (w1' : Vector Nat n3) (v2 w2 w : Vector Nat n2) : - HEq n1 n3 → v1 = w1 → HEq w1 w1' → HEq v2 w2 → HEq (w1' ++ w2) (v ++ w) → HEq (v1 ++ v2) (v ++ w) := by + n1 ≍ n3 → v1 = w1 → w1 ≍ w1' → v2 ≍ w2 → w1' ++ w2 ≍ v ++ w → v1 ++ v2 ≍ v ++ w := by grind #print ex2 diff --git a/tests/lean/run/grind_eq.lean b/tests/lean/run/grind_eq.lean index 4a65eea50b..9a2103cb13 100644 --- a/tests/lean/run/grind_eq.lean +++ b/tests/lean/run/grind_eq.lean @@ -62,7 +62,7 @@ opaque appV (xs : Vector α n) (ys : Vector α m) : Vector α (n + m) := @[grind =] theorem appV_assoc (a : Vector α n) (b : Vector α m) (c : Vector α n') : - HEq (appV a (appV b c)) (appV (appV a b) c) := sorry + appV a (appV b c) ≍ appV (appV a b) c := sorry /-- trace: [grind.assert] x1 = appV a_2 b @@ -74,7 +74,7 @@ trace: [grind.assert] x1 = appV a_2 b [grind.assert] appV a_2 (appV b c) ≍ appV (appV a_2 b) c -/ #guard_msgs (trace) in -example : x1 = appV a b → x2 = appV x1 c → x3 = appV b c → x4 = appV a x3 → HEq x2 x4 := by +example : x1 = appV a b → x2 = appV x1 c → x3 = appV b c → x4 = appV a x3 → x2 ≍ x4 := by grind @@ -84,4 +84,4 @@ info: appV_assoc': [@appV #6 #5 (@HAdd.hAdd `[Nat] `[Nat] `[Nat] `[instHAdd] #4 #guard_msgs (info) in @[grind? =] theorem appV_assoc' (a : Vector α n) (b : Vector α m) (c : Vector α n') : - HEq (appV a (appV b c)) (appV (appV a b) c) := sorry + appV a (appV b c) ≍ appV (appV a b) c := sorry diff --git a/tests/lean/run/grind_heq_proof_issue.lean b/tests/lean/run/grind_heq_proof_issue.lean index bc568cc3b0..1c16050d7f 100644 --- a/tests/lean/run/grind_heq_proof_issue.lean +++ b/tests/lean/run/grind_heq_proof_issue.lean @@ -1,7 +1,7 @@ def f (a : α) := a -example (a b : α) (x y : β) : HEq a x → x = y → HEq y b → f a = f b := by +example (a b : α) (x y : β) : a ≍ x → x = y → y ≍ b → f a = f b := by grind -example (a b : α) (x y : β) : x = y → HEq a x → HEq y b → f a = f b := by +example (a b : α) (x y : β) : x = y → a ≍ x → y ≍ b → f a = f b := by grind diff --git a/tests/lean/run/grind_pre.lean b/tests/lean/run/grind_pre.lean index 9a6cd0b04c..dd6e0bcadf 100644 --- a/tests/lean/run/grind_pre.lean +++ b/tests/lean/run/grind_pre.lean @@ -163,13 +163,13 @@ right : r [cases] source: Initial goal -/ #guard_msgs (error) in -example (a : α) (p q r : Prop) : (h₁ : HEq p a) → (h₂ : HEq q a) → (h₃ : p = r) → False := by +example (a : α) (p q r : Prop) : (h₁ : p ≍ a) → (h₂ : q ≍ a) → (h₃ : p = r) → False := by grind example (a b : Nat) (f : Nat → Nat) : (h₁ : a = b) → (h₂ : f a ≠ f b) → False := by grind -example (a : α) (p q r : Prop) : (h₁ : HEq p a) → (h₂ : HEq q a) → (h₃ : p = r) → q = r := by +example (a : α) (p q r : Prop) : (h₁ : p ≍ a) → (h₂ : q ≍ a) → (h₃ : p = r) → q = r := by grind /-- @@ -182,7 +182,7 @@ trace: [grind.issues] found congruence between #guard_msgs (trace) in set_option trace.grind.issues true in set_option trace.grind.debug.proof false in -example (f : Nat → Bool) (g : Int → Bool) (a : Nat) (b : Int) : HEq f g → HEq a b → f a = g b := by +example (f : Nat → Bool) (g : Int → Bool) (a : Nat) (b : Int) : f ≍ g → a ≍ b → f a = g b := by fail_if_success grind sorry @@ -215,5 +215,5 @@ h_2 : ¬f a = g b but functions have different types -/ #guard_msgs (error) in -example (f : Nat → Bool) (g : Int → Bool) (a : Nat) (b : Int) : HEq f g → HEq a b → f a = g b := by +example (f : Nat → Bool) (g : Int → Bool) (a : Nat) (b : Int) : f ≍ g → a ≍ b → f a = g b := by grind diff --git a/tests/lean/run/grind_propagate_connectives.lean b/tests/lean/run/grind_propagate_connectives.lean index 4949410adf..350b59b66f 100644 --- a/tests/lean/run/grind_propagate_connectives.lean +++ b/tests/lean/run/grind_propagate_connectives.lean @@ -73,7 +73,7 @@ trace: [Meta.debug] true: [p] [Meta.debug] [b, a] -/ #guard_msgs (trace) in -example (p : Prop) (a : Vector Nat 5) (b : Vector Nat 6) : (p → HEq a b) → p → False := by +example (p : Prop) (a : Vector Nat 5) (b : Vector Nat 6) : (p → a ≍ b) → p → False := by grind on_failure fallback /-- diff --git a/tests/lean/run/grind_t1.lean b/tests/lean/run/grind_t1.lean index 0e19aad2b9..1b9d0d8c48 100644 --- a/tests/lean/run/grind_t1.lean +++ b/tests/lean/run/grind_t1.lean @@ -146,7 +146,7 @@ example (α : Type) (β : Type) (a₁ a₂ : α) (b₁ b₂ : β) (h₂ : cast h₁ a₁ = b₁) (h₃ : a₁ = a₂) (h₄ : b₁ = b₂) - : HEq a₂ b₂ := by + : a₂ ≍ b₂ := by grind example (α : Type) (β : Type) (a₁ a₂ : α) (b₁ b₂ : β) @@ -154,7 +154,7 @@ example (α : Type) (β : Type) (a₁ a₂ : α) (b₁ b₂ : β) (h₂ : h₁ ▸ a₁ = b₁) (h₃ : a₁ = a₂) (h₄ : b₁ = b₂) - : HEq a₂ b₂ := by + : a₂ ≍ b₂ := by grind example (α : Type) (β : Type) (a₁ a₂ : α) (b₁ b₂ : β) @@ -162,7 +162,7 @@ example (α : Type) (β : Type) (a₁ a₂ : α) (b₁ b₂ : β) (h₂ : Eq.recOn h₁ a₁ = b₁) (h₃ : a₁ = a₂) (h₄ : b₁ = b₂) - : HEq a₂ b₂ := by + : a₂ ≍ b₂ := by grind example (α : Type) (β : Type) (a₁ a₂ : α) (b₁ b₂ : β) @@ -170,7 +170,7 @@ example (α : Type) (β : Type) (a₁ a₂ : α) (b₁ b₂ : β) (h₂ : Eq.ndrec (motive := id) a₁ h₁ = b₁) (h₃ : a₁ = a₂) (h₄ : b₁ = b₂) - : HEq a₂ b₂ := by + : a₂ ≍ b₂ := by grind example (α : Type) (β : Type) (a₁ a₂ : α) (b₁ b₂ : β) @@ -178,7 +178,7 @@ example (α : Type) (β : Type) (a₁ a₂ : α) (b₁ b₂ : β) (h₂ : Eq.rec (motive := fun x _ => x) a₁ h₁ = b₁) (h₃ : a₁ = a₂) (h₄ : b₁ = b₂) - : HEq a₂ b₂ := by + : a₂ ≍ b₂ := by grind /-- diff --git a/tests/lean/run/heqSubst.lean b/tests/lean/run/heqSubst.lean index ec9aff4689..6c3c16692a 100644 --- a/tests/lean/run/heqSubst.lean +++ b/tests/lean/run/heqSubst.lean @@ -1,3 +1,3 @@ -example (f : α → α) (a b : α) (h : HEq a b) : f a = f b := by +example (f : α → α) (a b : α) (h : a ≍ b) : f a = f b := by subst h rfl diff --git a/tests/lean/run/injHEq.lean b/tests/lean/run/injHEq.lean index 4bd6bfb20e..07b75019ea 100644 --- a/tests/lean/run/injHEq.lean +++ b/tests/lean/run/injHEq.lean @@ -1,2 +1,2 @@ -example (h : HEq Nat.zero (Nat.succ Nat.zero)) : False := by +example (h : Nat.zero ≍ Nat.succ Nat.zero) : False := by injection h diff --git a/tests/lean/run/linearNoConfusion.lean b/tests/lean/run/linearNoConfusion.lean index d5012336e7..59bb05a909 100644 --- a/tests/lean/run/linearNoConfusion.lean +++ b/tests/lean/run/linearNoConfusion.lean @@ -51,7 +51,7 @@ example : @Vec.noConfusionType.withCtor.{u_1,u} = @Vec.noConfusionType.withCtor' fun {α} {a} P x1 x2 => Vec.casesOn x1 (Vec.noConfusionType.withCtor' α (Sort u_1) 0 (fun _x => P → P) P a x2) - (fun {n} a_1 a_2 => Vec.noConfusionType.withCtor' α (Sort u_1) 1 (fun _x {n_1} a a_3 => (n = n_1 → a_1 = a → HEq a_2 a_3 → P) → P) P a x2) + (fun {n} a_1 a_2 => Vec.noConfusionType.withCtor' α (Sort u_1) 1 (fun _x {n_1} a a_3 => (n = n_1 → a_1 = a → a_2 ≍ a_3 → P) → P) P a x2) /-- info: @[reducible] protected def Vec.noConfusionType.{u_1, u} : {α : Type} → diff --git a/tests/lean/run/rflTacticErrors.lean b/tests/lean/run/rflTacticErrors.lean index 86a2724b2c..750b23ca01 100644 --- a/tests/lean/run/rflTacticErrors.lean +++ b/tests/lean/run/rflTacticErrors.lean @@ -82,7 +82,7 @@ and all using `apply_rfl` and `with_reducible apply_rfl` -- Syntactic equal example : true = true := by apply_rfl -example : HEq true true := by apply_rfl +example : true ≍ true := by apply_rfl example : True ↔ True := by apply_rfl example : P true true := by apply_rfl example : Q true true := by apply_rfl @@ -100,7 +100,7 @@ error: tactic 'rfl' failed, no @[refl] lemma registered for relation #guard_msgs in example : R true true := by apply_rfl -- Error example : true = true := by with_reducible apply_rfl -example : HEq true true := by with_reducible apply_rfl +example : true ≍ true := by with_reducible apply_rfl example : True ↔ True := by with_reducible apply_rfl example : P true true := by with_reducible apply_rfl example : Q true true := by with_reducible apply_rfl @@ -125,7 +125,7 @@ abbrev true' := true abbrev True' := True example : true' = true := by apply_rfl -example : HEq true' true := by apply_rfl +example : true' ≍ true := by apply_rfl example : True' ↔ True := by apply_rfl example : P true' true := by apply_rfl example : Q true' true := by apply_rfl @@ -145,7 +145,7 @@ error: tactic 'rfl' failed, no @[refl] lemma registered for relation example : R true' true := by apply_rfl -- Error example : true' = true := by with_reducible apply_rfl -example : HEq true' true := by with_reducible apply_rfl +example : true' ≍ true := by with_reducible apply_rfl example : True' ↔ True := by with_reducible apply_rfl example : P true' true := by with_reducible apply_rfl example : Q true' true := by with_reducible apply_rfl -- NB: No error, Q and true' reducible @@ -170,7 +170,7 @@ def true'' := true def True'' := True example : true'' = true := by apply_rfl -example : HEq true'' true := by apply_rfl +example : true'' ≍ true := by apply_rfl example : True'' ↔ True := by apply_rfl example : P true'' true := by apply_rfl example : Q true'' true := by apply_rfl @@ -211,7 +211,7 @@ Note: The full type of 'HEq.refl' is ⊢ true'' ≍ true -/ #guard_msgs in -example : HEq true'' true := by with_reducible apply_rfl -- Error +example : true'' ≍ true := by with_reducible apply_rfl -- Error /-- error: tactic 'rfl' failed, the left-hand side True'' @@ -279,7 +279,7 @@ Note: The full type of 'HEq.refl' is ⊢ false ≍ true -/ #guard_msgs in -example : HEq false true := by apply_rfl -- Error +example : false ≍ true := by apply_rfl -- Error /-- error: tactic 'rfl' failed, the left-hand side False @@ -346,7 +346,7 @@ Note: The full type of 'HEq.refl' is ⊢ false ≍ true -/ #guard_msgs in -example : HEq false true := by with_reducible apply_rfl -- Error +example : false ≍ true := by with_reducible apply_rfl -- Error /-- error: tactic 'rfl' failed, the left-hand side False @@ -406,7 +406,7 @@ Note: The full type of 'HEq.refl' is ⊢ true ≍ 1 -/ #guard_msgs in -example : HEq true 1 := by apply_rfl -- Error +example : true ≍ 1 := by apply_rfl -- Error /-- error: tactic 'apply' failed, could not unify the conclusion of 'HEq.refl' ?a ≍ ?a @@ -418,7 +418,7 @@ Note: The full type of 'HEq.refl' is ⊢ true ≍ 1 -/ #guard_msgs in -example : HEq true 1 := by with_reducible apply_rfl -- Error +example : true ≍ 1 := by with_reducible apply_rfl -- Error -- Rfl lemma with side condition: -- Error message should show left-over goal diff --git a/tests/lean/run/splitList.lean b/tests/lean/run/splitList.lean index 0e50f740ae..8c2caf4647 100644 --- a/tests/lean/run/splitList.lean +++ b/tests/lean/run/splitList.lean @@ -26,7 +26,7 @@ def len : List α → Nat match h₂ : splitList l with | ListSplit.split fst snd => -- Remark: `match` refined `h₁`s type to `h₁ : fst ++ snd = a :: b :: as` - -- h₂ : HEq (splitList l) (ListSplit.split fst snd) + -- h₂ : splitList l ≍ ListSplit.split fst snd have := splitList_length (fst ++ snd) (by simp +arith [h₁]) h₁ -- The following two proofs ase used to justify the recursive applications `len fst` and `len snd` have dec₁ : fst.length < as.length + 2 := by subst l; simp +arith [eq_of_heq h₂] at this |- ; simp [this]