# A solution to the if normalization challenge in Lean. #

See Statement.lean for background.

Equations
Instances For
Equations
Instances For

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 : } :
= b
@[simp]
theorem IfExpr.eval_var {i : } {f : } :
= f i
@[simp]
theorem IfExpr.eval_ite_lit {b : Bool} {t : IfExpr} {e : IfExpr} {f : } :
IfExpr.eval f (().ite t e) = bif b then else
@[simp]
theorem IfExpr.eval_ite_var {i : } {t : IfExpr} {e : IfExpr} {f : } :
IfExpr.eval f (().ite t e) = bif f i then else
@[simp]
theorem IfExpr.eval_ite_ite {a : IfExpr} {b : IfExpr} {c : IfExpr} {d : IfExpr} {e : IfExpr} {f : } :
IfExpr.eval f ((a.ite b c).ite d e) = IfExpr.eval f (a.ite (b.ite d e) (c.ite d e))

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

Equations
• ().normSize = 0
• ().normSize = 1
• (i.ite t e).normSize = 2 * i.normSize + max t.normSize e.normSize + 1
Instances For
@[irreducible]
def IfExpr.normalize (l : AList fun (x : ) => Bool) (e : IfExpr) :
{ e' : IfExpr // (∀ (f : ), IfExpr.eval f e' = IfExpr.eval (fun (w : ) => ().elim (f w) fun (b : Bool) => b) e) e'.normalized = true ve'.vars, = none }

Normalizes the expression at the same time as assigning all variables in e to the literal booleans given by l

Equations
Instances For