From cb925a3a3c7a15bdd72f5a2fb487db35fef978eb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 16 Mar 2022 16:36:39 -0700 Subject: [PATCH] fix: return `some` at `simpCnstrPos?` if arith expr was normalized, but not simplified Example: converted `<`, `>`, or `>=` into `<=`. --- src/Lean/Meta/Tactic/LinearArith/Nat/Simp.lean | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/Lean/Meta/Tactic/LinearArith/Nat/Simp.lean b/src/Lean/Meta/Tactic/LinearArith/Nat/Simp.lean index 8993b82b84..f201698022 100644 --- a/src/Lean/Meta/Tactic/LinearArith/Nat/Simp.lean +++ b/src/Lean/Meta/Tactic/LinearArith/Nat/Simp.lean @@ -17,13 +17,14 @@ def simpCnstrPos? (e : Expr) : MetaM (Option (Expr × Expr)) := do else if c₂.isValid then let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_true_of_isValid) (← toContextExpr ctx) (toExpr c) reflTrue return some (mkConst ``True, p) - else if c₁ != c₂ then - let c₂ : LinearCnstr := c₂.toExpr - let p := mkApp4 (mkConst ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq) (← toContextExpr ctx) (toExpr c) (toExpr c₂) reflTrue - let r ← c₂.toArith ctx - return some (r, p) else - return none + let c₂ : LinearCnstr := c₂.toExpr + let r ← c₂.toArith ctx + if r != e then + let p := mkApp4 (mkConst ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq) (← toContextExpr ctx) (toExpr c) (toExpr c₂) reflTrue + return some (r, p) + else + return none def simpCnstr? (e : Expr) : MetaM (Option (Expr × Expr)) := do if let some arg := e.not? then