From f2b3f907243146aa247bb88d3968be3cde406cf4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 11 Nov 2025 17:10:37 -0800 Subject: [PATCH] refactor: symmetric equality congruence in `grind` (#11147) This PR refactors the implementation of the symmetric equality congruence rule used in `grind`. --- src/Lean/Meta/Tactic/Grind/Internalize.lean | 32 +++++-------------- src/Lean/Meta/Tactic/Grind/Proof.lean | 24 ++++++++++----- src/Lean/Meta/Tactic/Grind/Types.lean | 34 ++++++++++++++++++++- 3 files changed, 57 insertions(+), 33 deletions(-) diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean index 30f0b9bbec..1faaa753aa 100644 --- a/src/Lean/Meta/Tactic/Grind/Internalize.lean +++ b/src/Lean/Meta/Tactic/Grind/Internalize.lean @@ -32,27 +32,9 @@ def addCongrTable (e : Expr) : GoalM Unit := do reportIssue! "found congruence between{indentExpr e}\nand{indentExpr e'}\nbut functions have different types" return () trace_goal[grind.debug.congr] "{e} = {e'}" - if (← isEqCongrProp e) then - /- - **Note**: We added this case to avoid a non-termination during proof construction. - We had the following equivalence class - ``` - {p, q, p = q, q = p, True} - ``` - Recall that `True` is always the root of its equivalence class. - We had the following two paths in the equivalence class: - ``` - 1. p -> p = q -> q = p -> True - 2. q -> True - ``` - Then, suppose we try to build a proof for `p = True`. - We have to construct a proof for `(p = q) = (q = p)`. - The equalities are congruent, but if we try to prove `p = q` and `q = p`, - We have to construct `p = True` and `True = q`, and we are back to `p = True`. - By constructing the congruence proof eagerly we ensure the non-termination cannot happen. - Note that this can only happen if `α₁` is a `Prop`. - -/ - pushEqHEq e e' (← mkEqCongrProof e e') + if (← isEqCongrSymm e e') then + -- **Note**: See comment at `eqCongrSymmPlaceholderProof` + pushEqHEq e e' eqCongrSymmPlaceholderProof else pushEqHEq e e' congrPlaceholderProof if (← swapCgrRepr e e') then @@ -74,9 +56,11 @@ def addCongrTable (e : Expr) : GoalM Unit := do else modify fun s => { s with congrTable := s.congrTable.insert { e } } where - isEqCongrProp (e : Expr) : GoalM Bool := do - let_expr Eq α _ _ := e | return false - return α.isProp + isEqCongrSymm (e e' : Expr) : GoalM Bool := do + let_expr Eq _ a₁ b₁ := e | return false + let_expr Eq _ a₂ b₂ := e' | return false + let goal ← get + return goal.hasSameRoot a₁ b₂ && goal.hasSameRoot b₁ a₂ swapCgrRepr (e e' : Expr) : GoalM Bool := do let_expr Eq _ _ _ := e | return false diff --git a/src/Lean/Meta/Tactic/Grind/Proof.lean b/src/Lean/Meta/Tactic/Grind/Proof.lean index cf10ab5f7a..3273f8c30d 100644 --- a/src/Lean/Meta/Tactic/Grind/Proof.lean +++ b/src/Lean/Meta/Tactic/Grind/Proof.lean @@ -210,16 +210,21 @@ mutual partial def mkEqCongrProof (lhs rhs : Expr) : GoalM Expr := withIncRecDepth do let_expr f@Eq α₁ a₁ b₁ := lhs | unreachable! let_expr Eq α₂ a₂ b₂ := rhs | unreachable! + assert! (← get).hasSameRoot a₁ a₂ && (← get).hasSameRoot b₁ b₂ let us := f.constLevels! if !isSameExpr α₁ α₂ then - if (← get).hasSameRoot a₁ a₂ && (← get).hasSameRoot b₁ b₂ then - return mkApp8 (mkConst ``Grind.heq_congr us) α₁ α₂ a₁ b₁ a₂ b₂ (← mkEqProofCore a₁ a₂ true) (← mkEqProofCore b₁ b₂ true) - else - return mkApp8 (mkConst ``Grind.heq_congr' us) α₁ α₂ a₁ b₁ a₂ b₂ (← mkEqProofCore a₁ b₂ true) (← mkEqProofCore b₁ a₂ true) - if (← get).hasSameRoot a₁ a₂ && (← get).hasSameRoot b₁ b₂ then - return mkApp7 (mkConst ``Grind.eq_congr us) α₁ a₁ b₁ a₂ b₂ (← mkEqProofCore a₁ a₂ false) (← mkEqProofCore b₁ b₂ false) + return mkApp8 (mkConst ``Grind.heq_congr us) α₁ α₂ a₁ b₁ a₂ b₂ (← mkEqProofCore a₁ a₂ true) (← mkEqProofCore b₁ b₂ true) + else + return mkApp7 (mkConst ``Grind.eq_congr us) α₁ a₁ b₁ a₂ b₂ (← mkEqProofCore a₁ a₂ false) (← mkEqProofCore b₁ b₂ false) + + partial def mkEqCongrSymmProof (lhs rhs : Expr) : GoalM Expr := withIncRecDepth do + let_expr f@Eq α₁ a₁ b₁ := lhs | unreachable! + let_expr Eq α₂ a₂ b₂ := rhs | unreachable! + assert! (← get).hasSameRoot a₁ b₂ && (← get).hasSameRoot b₁ a₂ + let us := f.constLevels! + if !isSameExpr α₁ α₂ then + return mkApp8 (mkConst ``Grind.heq_congr' us) α₁ α₂ a₁ b₁ a₂ b₂ (← mkEqProofCore a₁ b₂ true) (← mkEqProofCore b₁ a₂ true) else - assert! (← get).hasSameRoot a₁ b₂ && (← get).hasSameRoot b₁ a₂ return mkApp7 (mkConst ``Grind.eq_congr' us) α₁ a₁ b₁ a₂ b₂ (← mkEqProofCore a₁ b₂ false) (← mkEqProofCore b₁ a₂ false) /-- Constructs a congruence proof for `lhs` and `rhs`. -/ @@ -247,8 +252,11 @@ mutual mkHCongrProof lhs rhs heq private partial def realizeEqProof (lhs rhs : Expr) (h : Expr) (flipped : Bool) (heq : Bool) : GoalM Expr := do - let h ← if h == congrPlaceholderProof then + if h == congrPlaceholderProof then mkCongrProof lhs rhs heq + else if h == eqCongrSymmPlaceholderProof then + let r ← mkEqCongrSymmProof lhs rhs + if heq then mkHEqOfEq r else return r else flipProof h flipped heq diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean index df92b9cb4b..7d929539a7 100644 --- a/src/Lean/Meta/Tactic/Grind/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Types.lean @@ -23,6 +23,38 @@ namespace Lean.Meta.Grind /-- We use this auxiliary constant to mark delayed congruence proofs. -/ def congrPlaceholderProof := mkConst (Name.mkSimple "[congruence]") +/-- +We use this auxiliary constant to mark delayed symmetric congruence proofs. +**Example:** `a = b` is symmetrically congruent to `c = d` if `a = d` and `b = c`. + +**Note:** We previously used `congrPlaceholderProof` for this case, but it +caused non-termination during proof term construction when `a = b = c = d`. +The issue was that we did not have enough information to determine how +`a = b` and `c = d` became congruent. The new marker resolves this issue. + +If `congrPlaceholderProof` is used, then `a = b` became congruent to `c = d` +because `a = c` and `b = d`. +If `eqCongrSymmPlaceholderProof` is used, then it was because `a = d` and `b = c`. + +**Example:** suppose we have the following equivalence class: +``` +{p, q, p = q, q = p, True} +``` +Recall that `True` is always the root of its equivalence class. +Assume we also have the following two paths in the class: +``` +1. p -> p = q -> q = p -> True +2. q -> True +``` +Now suppose we try to build a proof for `p = True`. +We must construct a proof for `(p = q) = (q = p)`. +These equalities are congruent, but if we try to prove `p = q` and `q = p` +using the facts `p = True` and `q = True`, we end up trying to prove `p = True` again. +In other words, we are missing the information that `p = q` became congruent to `q = p` +because of the symmetric case. By using `eqCongrSymmPlaceholderProof`, we retain this information. +-/ +def eqCongrSymmPlaceholderProof := mkConst (Name.mkSimple "[eq_congr_symm]") + /-- Similar to `isDefEq`, but ensures default transparency is used. -/ def isDefEqD (t s : Expr) : MetaM Bool := withDefault <| isDefEq t s @@ -1122,7 +1154,7 @@ def pushEqCore (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit := do throwError "`grind` internal error, lhs of new equality has not been internalized{indentExpr lhs}" unless (← alreadyInternalized rhs) do throwError "`grind` internal error, rhs of new equality has not been internalized{indentExpr rhs}" - unless proof == congrPlaceholderProof do + if proof != congrPlaceholderProof && proof != eqCongrSymmPlaceholderProof then let expectedType ← if isHEq then mkHEq lhs rhs else mkEq lhs rhs unless (← withReducible <| isDefEq (← inferType proof) expectedType) do throwError "`grind` internal error, trying to assert equality{indentExpr expectedType}\n\