A solution to the if normalization challenge in Lean.

See Statement.lean for background.

def «tactic◾» : Lean.ParserDescr

Equations

• «tactic◾» = Lean.ParserDescr.node `tactic◾ 1024 (Lean.ParserDescr.nonReservedSymbol "◾" false)

def «term◾» : Lean.ParserDescr

Equations

• «term◾» = Lean.ParserDescr.node `term◾ 1024 (Lean.ParserDescr.symbol "◾")

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_lit {b : Bool} {f : ℕ → Bool} : IfExpr.eval f (IfExpr.lit b) = b

@[simp]

theorem IfExpr.eval_var {i : ℕ} {f : ℕ → Bool} : IfExpr.eval f (IfExpr.var i) = f 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))

def IfExpr.normSize : IfExpr → ℕ

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

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