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

fix: return some at simpCnstrPos? if arith expr was normalized, but not simplified

Browse source 
Example: converted `<`, `>`, or `>=` into `<=`.
This commit is contained in:
Leonardo de Moura 2022-03-16 16:36:39 -07:00
parent 9b9ed6db68
commit cb925a3a3c
1 changed files with 7 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/Lean/Meta/Tactic/LinearArith/Nat/Simp.lean
View file

@ -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