A solution to the if normalization challenge in Lean. #
See Statement.lean
for background.
Equations
- «tactic◾» = Lean.ParserDescr.node `tactic◾ 1024 (Lean.ParserDescr.nonReservedSymbol "◾" false)
Instances For
Equations
- «term◾» = Lean.ParserDescr.node `term◾ 1024 (Lean.ParserDescr.symbol "◾")
Instances For
We add some local simp lemmas so we can unfold the definitions of the normalization condition.
Simp lemmas for eval
.
We don't want a simp
lemma for (ite i t e).eval
in general, only once we know the shape of i
.
@[simp]
theorem
IfExpr.eval_ite_lit
{b : Bool}
{f : ℕ → Bool}
{t : IfExpr}
{e : IfExpr}
:
IfExpr.eval f ((IfExpr.lit b).ite t e) = bif b then IfExpr.eval f t else IfExpr.eval f e
@[simp]
theorem
IfExpr.eval_ite_var
{f : ℕ → Bool}
{i : ℕ}
{t : IfExpr}
{e : IfExpr}
:
IfExpr.eval f ((IfExpr.var i).ite t e) = bif f i then IfExpr.eval f t else IfExpr.eval f e
@[simp]
theorem
IfExpr.eval_ite_ite
{f : ℕ → Bool}
{a : IfExpr}
{b : IfExpr}
{c : IfExpr}
{d : IfExpr}
{e : IfExpr}
:
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) = ⟨↑(IfExpr.normalize l t), ⋯⟩
- IfExpr.normalize l ((IfExpr.lit false).ite t e) = ⟨↑(IfExpr.normalize l e), ⋯⟩
- IfExpr.normalize l ((a.ite b c).ite t e) = ⟨↑(IfExpr.normalize l (a.ite (b.ite t e) (c.ite t e))), ⋯⟩