max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: handle heterogeneous equality in closeGoalWithValuesEq (#12477)

Browse source 
This PR fixes an internal `grind` error where `mkEqProof` is invoked
with terms of different types. When equivalence classes contain
heterogeneous equalities (e.g., `0 : Fin 3` and `0 : Fin 2` merged via
`HEq`), `closeGoalWithValuesEq` would call `mkEqProof` on terms with
incompatible types, triggering an internal error.

Closes #12140

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This commit is contained in:
Leonardo de Moura 2026-02-13 23:12:01 -08:00 • committed by GitHub
parent d77efe6a5f
commit 57a2dc0146
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 58 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Lean/Meta/Tactic/Grind/Core.lean
View file

@ -73,7 +73,10 @@ private def closeGoalWithTrueEqFalse : GoalM Unit := do
let falseProof := mkApp4 (mkConst ``Eq.mp [levelZero]) (← getTrueExpr) (← getFalseExpr) trueEqFalse (mkConst ``True.intro)
closeGoal falseProof
/-- Closes the goal when `lhs` and `rhs` are both literal values and belong to the same equivalence class. -/
/--
Closes the goal when `lhs` and `rhs` are both literal values and belong to the same equivalence class,
and have the same type.
-/
private def closeGoalWithValuesEq (lhs rhs : Expr) : GoalM Unit := do
let p ← mkEq lhs rhs
let hp ← mkEqProof lhs rhs
@ -168,7 +171,10 @@ private partial def addEqStep (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit
markAsInconsistent
trueEqFalse := true
else
valueInconsistency := true
let hasHEq := isHEq || lhsRoot.heqProofs || rhsRoot.heqProofs
-- **Note**: We only have to check the types if there are heterogenous equalities.
if (← pure !hasHEq <||> hasSameType lhsRoot.self rhsRoot.self) then
valueInconsistency := true
if (lhsRoot.interpreted && !rhsRoot.interpreted)
|| (lhsRoot.ctor && !rhsRoot.ctor)
|| (lhsRoot.size > rhsRoot.size && !rhsRoot.interpreted && !rhsRoot.ctor) then

50
tests/lean/run/grind_12140.lean Normal file
View file

@ -0,0 +1,50 @@
inductive Foo (α : Type) (x : α) where
| c1 : Foo α x
| c2 : Foo α x
def Foo.mk (n : Nat) : Foo (Fin (n + 1)) 0 :=
match n with
| .zero => .c1
| .succ _ => .c1
def Foo.num {α : Type} {x : α} (f : Foo α x) : Nat :=
0
/-
Issue #12140: `closeGoalWithValuesEq` must check that the two interpreted values
have the same type before calling `mkEqProof`. When equivalence classes contain
heterogeneous equalities (e.g., `0 : Fin 3` and `0 : Fin 2` merged via `HEq`),
`mkEqProof` would fail with an internal error.
-/
/--
error: `grind` failed
case grind.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1
n : Nat
ih : (Foo.mk n).num = 0
h : ¬(Foo.mk (n + 1)).num = 0
h_1 : n + 1 = Nat.zero + 1
h_2 : 1 = Nat.zero + 1
h_3 : 1 = Nat.zero.succ + 1
h_4 : 1 = (n + 1).succ + 1
h_5 : 1 = (Nat.zero + 2).succ + 1
h_6 : (n + 2).succ + 1 = (Nat.zero + 2).succ + 1
h_7 : 2 = Nat.zero + 2
h_8 : 1 = (Nat.zero + 3).succ + 1
h_9 : (n + 3).succ + 1 = (Nat.zero + 3).succ + 1
h_10 : 3 = Nat.zero + 3
h_11 : 1 = (Nat.zero + 4).succ + 1
h_12 : (n + 4).succ + 1 = (Nat.zero + 4).succ + 1
h_13 : 4 = Nat.zero + 4
h_14 : 1 = (Nat.zero + 5).succ + 1
h_15 : (n + 5).succ + 1 = (Nat.zero + 5).succ + 1
h_16 : 5 = Nat.zero + 5
h_17 : 1 = (Nat.zero + 6).succ + 1
⊢ False
-/
#guard_msgs in
theorem foo (n : Nat) : (Foo.mk n).num = 0 := by
induction n with
| zero => rfl
| succ n ih =>
grind -verbose [Foo.mk]