A solution to the if normalization challenge in Lean. #
See Statement.lean
for background.
Equations
- «tactic◾» = Lean.ParserDescr.node `tactic◾ 1024 (Lean.ParserDescr.nonReservedSymbol "◾" false)
Instances For
Equations
- «term◾» = Lean.ParserDescr.node `term◾ 1024 (Lean.ParserDescr.symbol "◾")
Instances For
We add some local simp lemmas so we can unfold the definitions of the normalization condition.
Adding these lemmas to the simp set allows Lean to handle the termination proof automatically.
Some further simp lemmas for handling if-then-else statements.
Simp lemmas for eval
.
We don't want a simp
lemma for (ite i t e).eval
in general, only once we know the shape of i
.
@[simp]
theorem
IfExpr.eval_ite_lit
{b : Bool}
{t : IfExpr}
{e : IfExpr}
{f : ℕ → Bool}
:
IfExpr.eval f (IfExpr.ite (IfExpr.lit b) t e) = bif b then IfExpr.eval f t else IfExpr.eval f e
@[simp]
theorem
IfExpr.eval_ite_var
{i : ℕ}
{t : IfExpr}
{e : IfExpr}
{f : ℕ → Bool}
:
IfExpr.eval f (IfExpr.ite (IfExpr.var i) t e) = bif f i then IfExpr.eval f t else IfExpr.eval f e
@[simp]
theorem
IfExpr.eval_ite_ite
{a : IfExpr}
{b : IfExpr}
{c : IfExpr}
{d : IfExpr}
{e : IfExpr}
{f : ℕ → Bool}
:
IfExpr.eval f (IfExpr.ite (IfExpr.ite a b c) d e) = IfExpr.eval f (IfExpr.ite a (IfExpr.ite b d e) (IfExpr.ite c d e))
Custom size function for if-expressions, used for proving termination.
Equations
- IfExpr.normSize (IfExpr.lit a) = 0
- IfExpr.normSize (IfExpr.var a) = 1
- IfExpr.normSize (IfExpr.ite i t e) = 2 * IfExpr.normSize i + max (IfExpr.normSize t) (IfExpr.normSize e) + 1
Instances For
def
IfExpr.normalize
(l : AList fun (x : ℕ) => Bool)
(e : IfExpr)
:
{ e' : IfExpr //
(∀ (f : ℕ → Bool),
IfExpr.eval f e' = IfExpr.eval (fun (w : ℕ) => Option.elim (AList.lookup w l) (f w) fun (b : Bool) => b) e) ∧ IfExpr.normalized e' = true ∧ ∀ v ∈ IfExpr.vars e', AList.lookup v l = none }
Normalizes the expression at the same time as assigning all variables in
e
to the literal booleans given by l