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

fix: proof construction in grind ring (#11273)

Browse source 
This PR fixes a bug during proof construction in `grind`.
This commit is contained in:
Leonardo de Moura 2025-11-19 20:52:18 -08:00 • committed by GitHub
parent 5c8ebd8868
commit 00600806ad
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 6 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/CommRing/Proof.lean
View file

@ -383,7 +383,7 @@ private structure NormResult where
vars : Array Expr
private def norm (vars : PArray Expr) (lhs rhs lhs' rhs' : RingExpr) : NormResult :=
let usedVars := lhs.collectVars >> lhs.collectVars >> lhs'.collectVars >> rhs'.collectVars <| {}
let usedVars := lhs.collectVars >> rhs.collectVars >> lhs'.collectVars >> rhs'.collectVars <| {}
let vars' := usedVars.toArray
let varRename := mkVarRename vars'
let vars := vars'.map fun x => vars[x]!

5
tests/lean/run/grind_ring_norm_ring_proof.lean Normal file
View file

@ -0,0 +1,5 @@
example [LE α] [LT α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α] [Lean.Grind.CommRing α] [DecidableLE α] [Lean.Grind.OrderedRing α] (a b c : α) :
(if a - b ≤ -(a - b) then -(a - b) else a - b) ≤
((if a - c ≤ -(a - c) then -(a - c) else a - c) + if c - d ≤ -(c - d) then -(c - d) else c - d) +
if b - d ≤ -(b - d) then -(b - d) else b - d := by
split <;> split <;> split <;> split <;> grind