From 00600806ad19f5b2094d9041eff33ad09e78b533 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 19 Nov 2025 20:52:18 -0800 Subject: [PATCH] fix: proof construction in `grind ring` (#11273) This PR fixes a bug during proof construction in `grind`. --- src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean | 2 +- tests/lean/run/grind_ring_norm_ring_proof.lean | 5 +++++ 2 files changed, 6 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/grind_ring_norm_ring_proof.lean diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean index e94e71aab1..8f72a7e980 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean @@ -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]! diff --git a/tests/lean/run/grind_ring_norm_ring_proof.lean b/tests/lean/run/grind_ring_norm_ring_proof.lean new file mode 100644 index 0000000000..723c3a332e --- /dev/null +++ b/tests/lean/run/grind_ring_norm_ring_proof.lean @@ -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