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.

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.lit b).ite 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.var i).ite 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 ((a.ite b c).ite d e) = IfExpr.eval f (a.ite (b.ite d e) (c.ite d e))

def IfExpr.normSize : IfExpr → ℕ

Custom size function for if-expressions, used for proving termination.

Equations

• (IfExpr.lit a).normSize = 0
• (IfExpr.var a).normSize = 1
• (i.ite t e).normSize = 2 * i.normSize + max t.normSize e.normSize + 1

@[irreducible]

def IfExpr.normalize (l : AList fun (x : ℕ) => Bool) (e : IfExpr) : { e' : IfExpr // (∀ (f : ℕ → Bool), IfExpr.eval f e' = IfExpr.eval (fun (w : ℕ) => (AList.lookup w l).elim (f w) fun (b : Bool) => b) e) ∧ e'.normalized = true ∧ ∀ v ∈ e'.vars, 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

Equations

• One or more equations did not get rendered due to their size.
• IfExpr.normalize l (IfExpr.lit b) = ⟨IfExpr.lit b, ⋯⟩
• IfExpr.normalize l (IfExpr.var v) = match h : AList.lookup v l with | none => ⟨IfExpr.var v, ⋯⟩ | some b => ⟨IfExpr.lit b, ⋯⟩
• IfExpr.normalize l ((IfExpr.lit true).ite t e) = ⟨↑(IfExpr.normalize l t), ⋯⟩
• IfExpr.normalize l ((IfExpr.lit false).ite t e) = ⟨↑(IfExpr.normalize l e), ⋯⟩
• IfExpr.normalize l ((a.ite b c).ite t e) = ⟨↑(IfExpr.normalize l (a.ite (b.ite t e) (c.ite t e))), ⋯⟩