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

fix: incorrect proof term in grind linarith (#9487)

Browse source 
This PR fixes an incorrect proof term constructed by `grind linarith`,
as reported in #9485.

closes #9485
This commit is contained in:
Leonardo de Moura 2025-07-23 10:34:44 -07:00 • committed by GitHub
parent 6cf22b32aa
commit 2dce18655d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 33 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Meta/Tactic/Grind/Arith/Linear/PropagateEq.lean
View file

@ -19,7 +19,7 @@ namespace Lean.Meta.Grind.Arith.Linear
private def _root_.Lean.Grind.Linarith.Poly.substVar (p : Poly) : LinearM (Option (Var × EqCnstr × Poly)) := do
let some (a, x, c) ← p.findVarToSubst | return none
let b := c.p.coeff x
let p' := p.mul (-b) |>.combine (c.p.mul a)
let p' := p.mul b |>.combine (c.p.mul (-a))
trace[grind.debug.linarith.subst] "{← p.denoteExpr}, {a}, {← getVar x}, {← c.denoteExpr}, {b}, {← p'.denoteExpr}"
return some (x, c, p')

32
tests/lean/run/grind_9485.lean Normal file
View file

@ -0,0 +1,32 @@
variable (G : Type)
structure G' where p : G
@[ext, grind ext]
theorem ext_ {f g : G' G} (h : f.p = g.p) : f = g := by
cases f
subst h
rfl
variable [Lean.Grind.IntModule G]
instance : Add (G' G) where add f g := ⟨f.p + g.p⟩
@[grind] theorem add_p (f g : G' G) : (f + g).p = f.p + g.p := rfl
instance : Zero (G' G) where zero := ⟨0⟩
@[grind] theorem zero_p : (0 : G' G).p = 0 := rfl
instance : Neg (G' G) where neg x := ⟨-x.p⟩
@[grind] theorem neg_p (f : G' G) : (-f).p = -(f.p) := rfl
example (f g h : G' G) :
f + g + h = f + (g + h) := by
grind -- should work without extra options
example (f g h : G' G) :
f + g + h = f + (g + h) := by
grind [Lean.Grind.AddCommMonoid.add_assoc] -- should work too
example (f g h : G' G) :
f + g + h = f + (g + h) := by
grind -linarith [Lean.Grind.AddCommMonoid.add_assoc] -- should work too