From d37ecf6b1ce1ba82b5f588ec88cac611620a6133 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 31 Dec 2024 10:27:11 -0500 Subject: [PATCH 1/2] fix: make sure `#guard_*` uses syntactic equality This PR fixes the `syntactic` option for the `#guard_*` commands to actually use syntactic equality, to differentiate it from `alphaEq` mode. In particular, previously both were using `Expr.eqv`, but now `syntactic` uses `Expr.equal`. --- src/Lean/Elab/Tactic/Guard.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Elab/Tactic/Guard.lean b/src/Lean/Elab/Tactic/Guard.lean index 53443b340256..1c6de76f6445 100644 --- a/src/Lean/Elab/Tactic/Guard.lean +++ b/src/Lean/Elab/Tactic/Guard.lean @@ -19,7 +19,7 @@ have to be to pass the tactic. This inductive gives the different specifiers that can be selected. -/ inductive MatchKind -/-- A syntactic match means that the `Expr`s are `==` after stripping `MData` -/ +/-- A syntactic match means that the `Expr`s are `=` after stripping `MData` -/ | syntactic /-- A defeq match `isDefEqGuarded` returns true. (Note that unification is allowed here.) -/ | defEq (red : TransparencyMode := .reducible) @@ -54,7 +54,7 @@ def equal.toMatchKind : TSyntax ``equal → Option MatchKind /-- Applies the selected matching rule to two expressions. -/ def MatchKind.isEq (a b : Expr) : MatchKind → MetaM Bool - | .syntactic => return a.consumeMData == b.consumeMData + | .syntactic => return a.consumeMData.equal b.consumeMData | .alphaEq => return a.eqv b | .defEq red => withoutModifyingState <| withTransparency red <| Lean.Meta.isDefEqGuarded a b From 457a755f6e17f187c97c753eb4d6b8fd485c19ed Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 31 Dec 2024 11:22:15 -0500 Subject: [PATCH 2/2] fix tests --- tests/lean/run/3943.lean | 12 ++++++------ tests/lean/run/6065.lean | 2 +- tests/lean/run/6263.lean | 4 ++-- tests/lean/run/grind_canon_insts.lean | 2 +- tests/lean/run/grind_revertAll.lean | 2 +- tests/lean/run/simpLetFunIssue.lean | 2 +- 6 files changed, 12 insertions(+), 12 deletions(-) diff --git a/tests/lean/run/3943.lean b/tests/lean/run/3943.lean index 2f7059709e32..22910bc3c977 100644 --- a/tests/lean/run/3943.lean +++ b/tests/lean/run/3943.lean @@ -5,12 +5,12 @@ example (f : Nat → Nat) : (if f x = 0 then f x else f x + 1) + f x = y := by example (f : Nat → Nat) : f x = 0 → f x + 1 = y := by simp (config := { contextual := true }) - guard_target =ₛ f x = 0 → 1 = y + guard_target =ₐ f x = 0 → 1 = y sorry example (f : Nat → Nat) : let _ : f x = 0 := sorryAx _ false; f x + 1 = y := by simp (config := { contextual := true, zeta := false }) - guard_target =ₛ let _ : f x = 0 := sorryAx _ false; 1 = y + guard_target =ₐ let _ : f x = 0 := sorryAx _ false; 1 = y sorry def overlap : Nat → Nat @@ -20,20 +20,20 @@ def overlap : Nat → Nat example : (if (n = 0 → False) then overlap (n+1) else overlap (n+1)) = overlap n := by simp (config := { contextual := true }) only [overlap] - guard_target =ₛ (if (n = 0 → False) then overlap n else overlap (n+1)) = overlap n + guard_target =ₐ (if (n = 0 → False) then overlap n else overlap (n+1)) = overlap n sorry example : (if (n = 0 → False) then overlap (n+1) else overlap (n+1)) = overlap n := by -- The following tactic should because the default discharger only uses assumptions available -- when `simp` was invoked unless `contextual := true` fail_if_success simp only [overlap] - guard_target =ₛ (if (n = 0 → False) then overlap (n+1) else overlap (n+1)) = overlap n + guard_target =ₐ (if (n = 0 → False) then overlap (n+1) else overlap (n+1)) = overlap n sorry example : (if (n = 0 → False) then overlap (n+1) else overlap (n+1)) = overlap n := by -- assumption is not a well-behaved discharger, and the following should still work as expected simp (discharger := assumption) only [overlap] - guard_target =ₛ (if (n = 0 → False) then overlap n else overlap (n+1)) = overlap n + guard_target =ₐ (if (n = 0 → False) then overlap n else overlap (n+1)) = overlap n sorry opaque p : Nat → Bool @@ -47,5 +47,5 @@ example : (if p x then g x else g x + 1) + g x = y := by example : (let _ : p x := sorryAx _ false; g x + 1 = y) ↔ g x = y := by simp (config := { zeta := false }) (discharger := assumption) - guard_target =ₛ (let _ : p x := sorryAx _ false; x + 1 = y) ↔ g x = y + guard_target =ₐ (let _ : p x := sorryAx _ false; x + 1 = y) ↔ g x = y sorry diff --git a/tests/lean/run/6065.lean b/tests/lean/run/6065.lean index 0325e8fdc7f8..3036a3663a26 100644 --- a/tests/lean/run/6065.lean +++ b/tests/lean/run/6065.lean @@ -11,7 +11,7 @@ def foo (r : Nat) : Nat := example {r : Nat} : foo r = 0 := by simp only [foo.eq_def] - guard_target =ₛ + guard_target =ₐ (match r with | Nat.zero => 0 | l@h:(Nat.succ n) => diff --git a/tests/lean/run/6263.lean b/tests/lean/run/6263.lean index b9d0b7d7904d..2f7b0eb94b03 100644 --- a/tests/lean/run/6263.lean +++ b/tests/lean/run/6263.lean @@ -5,10 +5,10 @@ open Lean.Elab.Tactic variable (p q : Prop) theorem foo (h : p ∧ q) : q ∧ p := by run_tac liftMetaTactic1 (·.revertAll) - guard_target =ₛ ∀ (p q : Prop), p ∧ q → q ∧ p + guard_target =ₐ ∀ (p q : Prop), p ∧ q → q ∧ p sorry theorem bla (h : p ∧ q) : q ∧ p := by revert p q - guard_target =ₛ ∀ (p q : Prop), p ∧ q → q ∧ p + guard_target =ₐ ∀ (p q : Prop), p ∧ q → q ∧ p sorry diff --git a/tests/lean/run/grind_canon_insts.lean b/tests/lean/run/grind_canon_insts.lean index ddbadb62f5e9..17266a604c88 100644 --- a/tests/lean/run/grind_canon_insts.lean +++ b/tests/lean/run/grind_canon_insts.lean @@ -80,7 +80,7 @@ warning: declaration uses 'sorry' example (a b c d : Nat) : b * a = d * b → False := by rw [CommMonoid.mul_comm d b] -- Introduces a new (non-canonical) instance for `Mul Nat` -- See target here - guard_target =ₛ + guard_target =ₐ @HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) b a = @HMul.hMul Nat Nat Nat (@instHMul Nat (@Semigroup.toMul Nat (@Monoid.toSemigroup Nat (@CommMonoid.toMonoid Nat instCommMonoidNat)))) b d diff --git a/tests/lean/run/grind_revertAll.lean b/tests/lean/run/grind_revertAll.lean index 79ee7bde59d5..ae52f42c8b87 100644 --- a/tests/lean/run/grind_revertAll.lean +++ b/tests/lean/run/grind_revertAll.lean @@ -13,7 +13,7 @@ elab "ensure_no_mvar" : tactic => do example {α : Type u} [Inhabited α] (a : α) (f : α → α) (h : f a = default) : default = f a := by revert_all ensure_no_mvar - guard_target =ₛ∀ {α : Type u} [inst : Inhabited α] (a : α) (f : α → α), f a = default → default = f a + guard_target =ₐ ∀ {α : Type u} [inst : Inhabited α] (a : α) (f : α → α), f a = default → default = f a intro α inst a f h exact h.symm diff --git a/tests/lean/run/simpLetFunIssue.lean b/tests/lean/run/simpLetFunIssue.lean index 4c55be0a0598..08bf397502f7 100644 --- a/tests/lean/run/simpLetFunIssue.lean +++ b/tests/lean/run/simpLetFunIssue.lean @@ -4,7 +4,7 @@ example : (λ x => x) let_fun foo := λ y => id (id y) foo (0 + x)) := by simp -zeta only [id] - guard_target =ₛ + guard_target =ₐ (λ x => x) = (λ x : Nat =>