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 b c d e : IfExpr} {f : ℕ → Bool} : eval f ((a.ite b c).ite d e) = eval f (a.ite (b.ite d e) (c.ite d e))

def IfExpr.normSize' : IfExpr → ℕ

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

@[irreducible]

def IfExpr.normalize' (l : AList fun (x : ℕ) => Bool) (e : IfExpr) : { e' : IfExpr // (∀ (f : ℕ → Bool), eval f e' = eval (fun (w : ℕ) => (AList.lookup w l).elim (f w) id) e) ∧ e'.normalized = true ∧ ∀ (v : ℕ), 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', ⋯⟩