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 (IfExpr.ite (IfExpr.ite a b c) d e) = IfExpr.eval f (IfExpr.ite a (IfExpr.ite b d e) (IfExpr.ite c d e))
Custom size function for if-expressions, used for proving termination.
Equations
- IfExpr.normSize' (IfExpr.lit a) = 0
- IfExpr.normSize' (IfExpr.var a) = 1
- IfExpr.normSize' (IfExpr.ite i t e) = 2 * IfExpr.normSize' i + max (IfExpr.normSize' t) (IfExpr.normSize' e) + 1
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 ∧ ∀ v ∈ IfExpr.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
Equations
- One or more equations did not get rendered due to their size.