Documentation

Archive.Examples.IfNormalization.WithoutAesop

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} :
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
Instances For
    @[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) id) e) e'.normalized = true ve'.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
    Instances For