A solution to the if normalization challenge in Lean. #

See Statement.lean for background.

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.

theorem IfExpr.eval_lit {b : Bool} {f : Bool} :
theorem IfExpr.eval_var {i : } {f : Bool} :
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
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
theorem IfExpr.eval_ite_ite {a : IfExpr} {b : IfExpr} {c : IfExpr} {d : IfExpr} {e : IfExpr} {f : Bool} :

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

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 vIfExpr.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

    Instances For