8. A Verified Transformation
Constant folding replaces 1 + 2 by 3 before the program runs. Over
parametric syntax it is written once, for every v. Its correctness proof
then makes the choice that matters for correctness, the values, and becomes
a plain structural induction.Structural induction is recursion for
proofs: one case per constructor, with the statement already established for
the sub-terms.
namespace Typed
open Exp'
def Exp'.cfold : Exp' v t → Exp' v t
| var x => var x
| const n => const n
| plus a b =>
match a.cfold, b.cfold with
| const n, const m => const (n + m)
| a', b' => plus a' b'
| lam b => lam fun x => (b x).cfold
| app f a => app f.cfold a.cfold
def Exp.cfold (e : Exp t) : Exp t := fun v => (e v).cfold
The theorem: a folded program means the same as the original. Only plus
needs thought. split asks whether both folded sides became constants, and
simp_all closes each case with the induction hypotheses. The other cases
hold by definition or by one rewrite.
theorem Exp'.cfold_denote (e : Exp' Ty.denote t) :
e.cfold.denote = e.denote := t:Tye:Exp' Ty.denote t⊢ e.cfold.denote = e.denote
induction e with
t:Tyt✝:Tya✝:t✝.denote⊢ (var a✝).cfold.denote = (var a✝).denote All goals completed! 🐙
t:Tya✝:Nat⊢ (const a✝).cfold.denote = (const a✝).denote All goals completed! 🐙
t:Tya:Exp' Ty.denote Ty.natb:Exp' Ty.denote Ty.natiha:a.cfold.denote = a.denoteihb:b.cfold.denote = b.denote⊢ (a.plus b).cfold.denote = (a.plus b).denote
t:Tya:Exp' Ty.denote Ty.natb:Exp' Ty.denote Ty.natiha:a.cfold.denote = a.denoteihb:b.cfold.denote = b.denote⊢ (match a.cfold, b.cfold with
| const n, const m => const (n + m)
| a', b' => a'.plus b').denote =
(a.plus b).denote
t:Tya:Exp' Ty.denote Ty.natb:Exp' Ty.denote Ty.natiha:a.cfold.denote = a.denoteihb:b.cfold.denote = b.denotex✝¹:Exp' Ty.denote Ty.natx✝:Exp' Ty.denote Ty.natn✝:Natm✝:Natheq✝¹:a.cfold = const n✝heq✝:b.cfold = const m✝⊢ (const (n✝ + m✝)).denote = (a.plus b).denotet:Tya:Exp' Ty.denote Ty.natb:Exp' Ty.denote Ty.natiha:a.cfold.denote = a.denoteihb:b.cfold.denote = b.denotex✝²:Exp' Ty.denote Ty.natx✝¹:Exp' Ty.denote Ty.natx✝:∀ (n m : Nat), a.cfold = const n → b.cfold = const m → False⊢ (a.cfold.plus b.cfold).denote = (a.plus b).denote t:Tya:Exp' Ty.denote Ty.natb:Exp' Ty.denote Ty.natiha:a.cfold.denote = a.denoteihb:b.cfold.denote = b.denotex✝¹:Exp' Ty.denote Ty.natx✝:Exp' Ty.denote Ty.natn✝:Natm✝:Natheq✝¹:a.cfold = const n✝heq✝:b.cfold = const m✝⊢ (const (n✝ + m✝)).denote = (a.plus b).denotet:Tya:Exp' Ty.denote Ty.natb:Exp' Ty.denote Ty.natiha:a.cfold.denote = a.denoteihb:b.cfold.denote = b.denotex✝²:Exp' Ty.denote Ty.natx✝¹:Exp' Ty.denote Ty.natx✝:∀ (n m : Nat), a.cfold = const n → b.cfold = const m → False⊢ (a.cfold.plus b.cfold).denote = (a.plus b).denote All goals completed! 🐙
t:Tydom✝:Tyran✝:Tyb:dom✝.denote → Exp' Ty.denote ran✝ih:∀ (a : dom✝.denote), (b a).cfold.denote = (b a).denote⊢ (lam b).cfold.denote = (lam b).denote
t:Tydom✝:Tyran✝:Tyb:dom✝.denote → Exp' Ty.denote ran✝ih:∀ (a : dom✝.denote), (b a).cfold.denote = (b a).denotex:dom✝.denote⊢ (lam b).cfold.denote x = (lam b).denote x
All goals completed! 🐙
t:Tydom✝:Tyran✝:Tyf:Exp' Ty.denote (dom✝ ⇒ ran✝)a:Exp' Ty.denote dom✝ihf:f.cfold.denote = f.denoteiha:a.cfold.denote = a.denote⊢ (f.app a).cfold.denote = (f.app a).denote All goals completed! 🐙
theorem Exp.cfold_denote (e : Exp t) :
e.cfold.denote = e.denote :=
Exp'.cfold_denote (e _)
The lam case is everything this proof has to say about binders: funext x,
then exact ih x. Tap each step to watch the goal change.funext
is function extensionality: two
functions are equal when they agree on every argument. To be fair, a
first-order version of this particular proof would be short too: evaluate
with an environment, state the theorem for every environment, and let the
lam case extend it. Constant folding never moves code across a binder. The
gap opens for transformations that do, such as inlining or β-reduction.
There, first-order proofs need shifting or freshness lemmas; PHOAS proofs
avoid those, though some need the well-formedness hypothesis instead.
Another choice of v confirms that folding happened: with nothing stored at
variables, count the additions that remain.
def Exp'.plusCount : Exp' (fun _ => Unit) t → Nat
| plus a b => a.plusCount + b.plusCount + 1
| lam b => (b ()).plusCount
| app f a => f.plusCount + a.plusCount
| _ => 0
def Exp.plusCount (e : Exp t) : Nat := (e _).plusCount
def addThree : Exp (.nat ⇒ .nat) := fun _ =>
lam fun x => plus (var x) (plus (const 1) (const 2))
example : addThree.plusCount = 2 := rfl
example : addThree.cfold.plusCount = 1 := rfl
example : addThree.cfold.denote 10 = 13 := rfl
end Typed