A variant of Chris Hughes' solution for the if normalization challenge. #

In this variant we eschew the use of aesop, and instead write out the proofs.

(In order to avoid duplicated names with Result.lean, we put primes on the declarations in the file.)

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

    • One or more equations did not get rendered due to their size.
    Instances For