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

perf: use RArray in simp_arith meta code (#6068 part 1)

Browse source 
This PR prepares #6068 by using the `RArray` data structure in
`simp_arith` the simp-arith meta code.

After the subsequent stage0 we can change the simp-arith theorems in
`Init`.
This commit is contained in:
Joachim Breitner 2024-11-13 15:37:59 +01:00 • committed by Sebastian Ullrich
parent 85f25967ea
commit 3f47871e73
2 changed files with 10 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/Meta/Tactic/LinearArith/Nat/Basic.lean
View file

@ -8,6 +8,7 @@ import Lean.Meta.Check
import Lean.Meta.Offset
import Lean.Meta.AppBuilder
import Lean.Meta.KExprMap
import Lean.Data.RArray
namespace Lean.Meta.Linear.Nat
@ -141,8 +142,11 @@ end ToLinear
export ToLinear (toLinearCnstr? toLinearExpr)
def toContextExpr (ctx : Array Expr) : MetaM Expr := do
mkListLit (mkConst ``Nat) ctx.toList
def toContextExpr (ctx : Array Expr) : Expr :=
if h : 0 < ctx.size then
RArray.toExpr (mkConst ``Nat) id (RArray.ofArray ctx h)
else
RArray.toExpr (mkConst ``Nat) id (RArray.leaf (mkNatLit 0))
def reflTrue : Expr :=
mkApp2 (mkConst ``Eq.refl [levelOne]) (mkConst ``Bool) (mkConst ``Bool.true)

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

@ -31,17 +31,17 @@ def simpCnstrPos? (e : Expr) : MetaM (Option (Expr × Expr)) := do
let c₂ := c₁.norm
if c₂.isUnsat then
let r := mkConst ``False
let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_false_of_isUnsat) (← toContextExpr ctx) (toExpr c) reflTrue
let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_false_of_isUnsat) (toContextExpr ctx) (toExpr c) reflTrue
return some (r, ← mkExpectedTypeHint p (← mkEq lhs r))
else if c₂.isValid then
let r := mkConst ``True
let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_true_of_isValid) (← toContextExpr ctx) (toExpr c) reflTrue
let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_true_of_isValid) (toContextExpr ctx) (toExpr c) reflTrue
return some (r, ← mkExpectedTypeHint p (← mkEq lhs r))
else
let c₂ : LinearCnstr := c₂.toExpr
let r ← c₂.toArith ctx
if r != lhs then
let p := mkApp4 (mkConst ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq) (← toContextExpr ctx) (toExpr c) (toExpr c₂) reflTrue
let p := mkApp4 (mkConst ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq) (toContextExpr ctx) (toExpr c) (toExpr c₂) reflTrue
return some (r, ← mkExpectedTypeHint p (← mkEq lhs r))
else
return none
@ -81,7 +81,7 @@ def simpExpr? (e : Expr) : MetaM (Option (Expr × Expr)) := do
if p'.length < p.length then
-- We only return some if monomials were fused
let e' : LinearExpr := p'.toExpr
let p := mkApp4 (mkConst ``Nat.Linear.Expr.eq_of_toNormPoly_eq) (← toContextExpr ctx) (toExpr e) (toExpr e') reflTrue
let p := mkApp4 (mkConst ``Nat.Linear.Expr.eq_of_toNormPoly_eq) (toContextExpr ctx) (toExpr e) (toExpr e') reflTrue
let r ← e'.toArith ctx
return some (r, p)
else