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
- (IfExpr.lit a).normSize' = 0
- (IfExpr.var a).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 : ℕ → Bool), IfExpr.eval f e' = IfExpr.eval (fun (w : ℕ) => (AList.lookup w l).elim (f w) id) e) ∧ e'.normalized = true ∧ ∀ v ∈ e'.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
- One or more equations did not get rendered due to their size.
- IfExpr.normalize' l (IfExpr.lit b) = ⟨IfExpr.lit b, ⋯⟩
- IfExpr.normalize' l (IfExpr.var v) = match h : AList.lookup v l with | none => ⟨IfExpr.var v, ⋯⟩ | some b => ⟨IfExpr.lit b, ⋯⟩
- IfExpr.normalize' l ((IfExpr.lit true).ite t e) = match IfExpr.normalize' l t with | ⟨t', ht'⟩ => ⟨t', ⋯⟩
- IfExpr.normalize' l ((IfExpr.lit false).ite t e) = match IfExpr.normalize' l e with | ⟨e', he'⟩ => ⟨e', ⋯⟩
- IfExpr.normalize' l ((a.ite b c).ite d e) = match IfExpr.normalize' l (a.ite (b.ite d e) (c.ite d e)) with | ⟨t', ⋯⟩ => ⟨t', ⋯⟩