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

fix: bug at matchEqBwdPat (#9172)

Browse source 
This PR fixes a bug at `matchEqBwdPat`. The type may contain pattern
variables.
This commit is contained in:
Leonardo de Moura 2025-07-03 00:05:01 -07:00 • committed by GitHub
parent c06af84d9f
commit ff130a25a2
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 12 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/Lean/Meta/Tactic/Grind/EMatch.lean
View file

@ -509,15 +509,14 @@ private def matchEqBwdPat (p : Expr) : M Unit := do
if (n.heqProofs || n.isCongrRoot) &&
(!useMT || n.mt == gmt) then
let_expr Eq α lhs rhs := n.self | pure ()
if (← isDefEq α pα) then
let c₀ : Choice := { cnstrs := [], assignment, gen := n.generation }
let go (lhs rhs : Expr) : M Unit := do
let some c₁ ← matchArg? c₀ plhs lhs |>.run | return ()
let some c₂ ← matchArg? c₁ prhs rhs |>.run | return ()
modify fun s => { s with choiceStack := [c₂] }
processChoices
go lhs rhs
go rhs lhs
if let some c₀ ← matchArg? { cnstrs := [], assignment, gen := n.generation } pα α |>.run then
let go (lhs rhs : Expr) : M Unit := do
let some c₁ ← matchArg? c₀ plhs lhs |>.run | return ()
let some c₂ ← matchArg? c₁ prhs rhs |>.run | return ()
modify fun s => { s with choiceStack := [c₂] }
processChoices
go lhs rhs
go rhs lhs
if isSameExpr n.next false then return ()
curr := n.next

4
tests/lean/run/grind_eq_bwd_pat_bug.lean Normal file
View file

@ -0,0 +1,4 @@
@[grind ←=] theorem inv_eq {α : Type} [One α] [Mul α] [Inv α] {a b : α} (w : a * b = 1) : a⁻¹ = b := sorry
theorem test {α : Type} [One α] [Mul α] [Inv α] {a b : α} (w : a * b = 1) : a⁻¹ = b := by
grind