Library Intensional
The essential benefit of higher-order encodings is that variable contexts are implicit. We represent the object language's contexts within the meta language's contexts. For translations like CPS conversion, this is a clear win, since such translations do not need to keep track of details of which variables are available. Other important translations, including closure conversion, need to work with variables as first-class, analyzable values.
Another example is conversion from PHOAS terms to de Bruijn terms. The output format makes the structure of variables explicit, so the translation requires explicit reasoning about variable identity. In this chapter, we implement verified translations in both directions between last chapter's PHOAS language and a de Bruijn version of it. Along the way, we show one approach to avoiding the use of axioms with PHOAS.
Another example is conversion from PHOAS terms to de Bruijn terms. The output format makes the structure of variables explicit, so the translation requires explicit reasoning about variable identity. In this chapter, we implement verified translations in both directions between last chapter's PHOAS language and a de Bruijn version of it. Along the way, we show one approach to avoiding the use of axioms with PHOAS.
The de Bruijn version of simply-typed lambda calculus is defined in a manner that should be old hat by now.
Module DeBruijn.
Inductive exp : list type -> type -> Type :=
| Var : forall G t,
member t G
-> exp G t
| Const : forall G, nat -> exp G Nat
| Plus : forall G, exp G Nat -> exp G Nat -> exp G Nat
| App : forall G t1 t2,
exp G (t1 --> t2)
-> exp G t1
-> exp G t2
| Abs : forall G t1 t2,
exp (t1 :: G) t2
-> exp G (t1 --> t2).
Implicit Arguments Const [G].
Fixpoint expDenote G t (e : exp G t) : hlist typeDenote G -> typeDenote t :=
match e with
| Var _ _ v => fun s => hget s v
| Const _ n => fun _ => n
| Plus _ e1 e2 => fun s => expDenote e1 s + expDenote e2 s
| App _ _ _ e1 e2 => fun s => (expDenote e1 s) (expDenote e2 s)
| Abs _ _ _ e' => fun s x => expDenote e' (x ::: s)
end.
End DeBruijn.
Import Phoas DeBruijn.
The heart of the translation into PHOAS is this function phoasify, which is parameterized by an hlist that represents a mapping from de Bruijn variables to PHOAS variables.
Section phoasify.
Variable var : type -> Type.
Fixpoint phoasify G t (e : DeBruijn.exp G t) : hlist var G -> Phoas.exp var t :=
match e with
| Var _ _ v => fun s => #(hget s v)
| Const _ n => fun _ => *)n
| Plus _ e1 e2 => fun s => phoasify e1 s +^ phoasify e2 s
| App _ _ _ e1 e2 => fun s => phoasify e1 s @ phoasify e2 s
| Abs _ _ _ e' => fun s => \x, phoasify e' (x ::: s)
end.
End phoasify.
Definition Phoasify t (e : DeBruijn.exp nil t) : Phoas.Exp t :=
fun _ => phoasify e HNil.
It turns out to be trivial to establish the translation's soundness.
Theorem phoasify_sound : forall G t (e : DeBruijn.exp G t) s,
Phoas.expDenote (phoasify e s) = DeBruijn.expDenote e s.
induction e; crush; (let x := fresh in extensionality x); crush.
Qed.
We can prove that any output of Phoasify is well-formed, in a sense strong enough to let us avoid asserting last chapter's axiom.
Print Wf.
Wf =
fun (t : type) (E : Exp t) =>
forall var1 var2 : type -> Type, exp_equiv nil (E var1) (E var2)
: forall t : type, Exp t -> Prop
In the course of proving well-formedness, we will need to translate back and forth between the de Bruijn and PHOAS representations of free variable information. The function zip combines two de Bruijn substitutions into a single PHOAS context.
Fixpoint zip G (s1 : hlist var1 G)
: hlist var2 G -> list {t : type & var1 t * var2 t}%type :=
match s1 with
| HNil => fun _ => nil
| HCons _ _ v1 s1' => fun s2 => existT _ _ (v1, hhd s2) :: zip s1' (htl s2)
end.
Two simple lemmas about zip will make useful hints.
Lemma In_zip : forall t G (s1 : hlist _ G) s2 (m : member t G),
In (existT _ t (hget s1 m, hget s2 m)) (zip s1 s2).
induction s1; intro s2; dep_destruct s2; intro m; dep_destruct m; crush.
Qed.
Lemma unsimpl_zip : forall t (v1 : var1 t) (v2 : var2 t)
G (s1 : hlist _ G) s2 t' (e1 : Phoas.exp _ t') e2,
exp_equiv (zip (v1 ::: s1) (v2 ::: s2)) e1 e2
-> exp_equiv (existT _ _ (v1, v2) :: zip s1 s2) e1 e2.
trivial.
Qed.
Hint Resolve In_zip unsimpl_zip.
Now it is trivial to prove the main inductive lemma about well-formedness.
Lemma phoasify_wf : forall G t (e : DeBruijn.exp G t) s1 s2,
exp_equiv (zip s1 s2) (phoasify e s1) (phoasify e s2).
Hint Constructors exp_equiv.
induction e; crush.
Qed.
End vars.
We apply phoasify_wf manually to prove the final theorem.
Theorem Phoasify_wf : forall t (e : DeBruijn.exp nil t),
Wf (Phoasify e).
unfold Wf, Phoasify; intros;
apply (phoasify_wf e (HNil (B := var1)) (HNil (B := var2))).
Qed.
Now, if we compose Phoasify with any translation over PHOAS terms, we can verify the composed translation without relying on axioms. The conclusion of Phoasify_wf is robustly useful in verifying a wide variety of translations that use a wide variety of var instantiations.
The translation to de Bruijn terms is more involved. We will essentially be instantiating and using a PHOAS term following a convention isomorphic to de Bruijn levels, which are different from the de Bruijn indices that we have treated so far. With levels, a given bound variable is referred to by the same number at each of its occurrences. In any expression, the binders that are not enclosed by other binders are assigned level 0, a binder with just one enclosing binder is assigned level 1, and so on. The uniformity of references to any binder will be critical to our translation, since it is compatible with the pattern of filling in all of a PHOAS variable's locations at once by applying a function.
We implement a special lookup function, for reading a numbered variable's type out of a de Bruijn level typing context. The last variable in the list is taken to have level 0, the next-to-last level 1, and so on.
We implement a special lookup function, for reading a numbered variable's type out of a de Bruijn level typing context. The last variable in the list is taken to have level 0, the next-to-last level 1, and so on.
Fixpoint lookup (ts : list type) (n : nat) : option type :=
match ts with
| nil => None
| t :: ts' => if eq_nat_dec n (length ts') then Some t else lookup ts' n
end.
Infix "##" := lookup (left associativity, at level 1).
With lookup, we can define a notion of well-formedness for PHOAS expressions that we are treating according to the de Bruijn level convention.
Fixpoint wf (ts : list type) t (e : Phoas.exp (fun _ => nat) t) : Prop :=
match e with
| Phoas.Var t n => ts ## n = Some t
| Phoas.Const _ => True
| Phoas.Plus e1 e2 => wf ts e1 /\ wf ts e2
| Phoas.App _ _ e1 e2 => wf ts e1 /\ wf ts e2
| Phoas.Abs t1 _ e1 => wf (t1 :: ts) (e1 (length ts))
end.
Our first order of business now is to prove that any well-formed Exp instantiates to a well-formed de Bruijn level expression. We start by characterizing, as a function of de Bruijn level contexts, the set of PHOAS contexts that will occur in the proof, where we will be inducting over an exp_equiv derivation.
Fixpoint makeG (ts : list type) : list { t : type & nat * nat }%type :=
match ts with
| nil => nil
| t :: ts' => existT _ t (length ts', length ts') :: makeG ts'
end.
Opaque eq_nat_dec.
Hint Extern 1 (_ >= _) => omega.
Lemma lookup_contra' : forall t ts n,
ts ## n = Some t
-> n >= length ts
-> False.
induction ts; crush;
match goal with
| [ _ : context[if ?E then _ else _] |- _ ] => destruct E; crush
end; eauto.
Qed.
Lemma lookup_contra : forall t ts,
ts ## (length ts) = Some t
-> False.
intros; eapply lookup_contra'; eauto.
Qed.
Hint Resolve lookup_contra.
Lemma lookup_In : forall t v1 v2 ts,
In (existT (fun _ : type => (nat * nat)%type) t (v1, v2)) (makeG ts)
-> ts ## v1 = Some t.
induction ts; crush;
match goal with
| [ |- context[if ?E then _ else _] ] => destruct E; crush
end; elimtype False; eauto.
Qed.
Hint Resolve lookup_In.
We can prove the main inductive lemma by induction over exp_equiv derivations.
Hint Extern 1 (_ :: _ = makeG (_ :: _)) => reflexivity.
Lemma Wf_wf' : forall G t e1 (e2 : Phoas.exp (fun _ => nat) t),
exp_equiv G e1 e2
-> forall ts, G = makeG ts
-> wf ts e1.
induction 1; crush; eauto.
Qed.
Lemma Wf_wf : forall t (E : Exp t),
Wf E
-> wf nil (E (fun _ => nat)).
intros; eapply Wf_wf'; eauto.
Qed.
Implementing the translation itself will require some proofs. Our main function dbify will take wf proofs as arguments, and these proofs will be critical to constructing de Bruijn index terms. First, we use congruence to prove two basic theorems about options.
Theorem None_Some : forall T (x : T),
None = Some x
-> False.
congruence.
Qed.
Theorem Some_Some : forall T (x y : T),
Some x = Some y
-> x = y.
congruence.
Qed.
We can use these theorems to implement makeVar, which translates a proof about lookup into a de Bruijn index variable with a closely related type.
Fixpoint makeVar {ts n t} : ts ## n = Some t -> member t ts :=
match ts with
| nil => fun Heq => match None_Some Heq with end
| t' :: ts' => if eq_nat_dec n (length ts') as b return (if b then _ else _) = _ -> _
then fun Heq => match Some_Some Heq with refl_equal => HFirst end
else fun Heq => HNext (makeVar Heq)
end.
Now dbify is straightforward to define. We use the functions proj1 and proj2 to decompose proofs of conjunctions.
Fixpoint dbify {ts} t (e : Phoas.exp (fun _ => nat) t) : wf ts e -> DeBruijn.exp ts t :=
match e in Phoas.exp _ t return wf ts e -> DeBruijn.exp ts t with
| Phoas.Var _ n => fun wf => DeBruijn.Var (makeVar wf)
| Phoas.Const n => fun _ => DeBruijn.Const n
| Phoas.Plus e1 e2 => fun wf =>
DeBruijn.Plus (dbify e1 (proj1 wf)) (dbify e2 (proj2 wf))
| Phoas.App _ _ e1 e2 => fun wf =>
DeBruijn.App (dbify e1 (proj1 wf)) (dbify e2 (proj2 wf))
| Phoas.Abs _ _ e1 => fun wf => DeBruijn.Abs (dbify (e1 (length ts)) wf)
end.
We define the parametric translation Dbify by appealing to the well-formedness translation theorem Wf_wf that we proved earlier.
To prove soundness, it is helpful to classify a set of contexts which depends on a de Bruijn index substitution.
Fixpoint makeG' ts (s : hlist typeDenote ts)
: list { t : type & nat * typeDenote t }%type :=
match s with
| HNil => nil
| HCons _ ts' v s' => existT _ _ (length ts', v) :: makeG' s'
end.
We prove an analogous lemma to the one we proved connecting makeG and lookup. This time, we connect makeG' and hget.
Lemma In_makeG'_contra' : forall t v2 ts (s : hlist _ ts) n,
In (existT _ t (n, v2)) (makeG' s)
-> n >= length ts
-> False.
induction s; crush; eauto.
Qed.
Lemma In_makeG'_contra : forall t v2 ts (s : hlist _ ts),
In (existT _ t (length ts, v2)) (makeG' s)
-> False.
intros; eapply In_makeG'_contra'; eauto.
Qed.
Hint Resolve In_makeG'_contra.
Lemma In_makeG' : forall t v1 v2 ts s (w : ts ## v1 = Some t),
In (existT _ t (v1, v2)) (makeG' s)
-> hget s (makeVar w) = v2.
induction s; crush;
match goal with
| [ |- context[if ?E then _ else _] ] => destruct E; crush
end;
repeat match goal with
| [ |- context[match ?pf with refl_equal => _ end] ] =>
rewrite (UIP_refl _ _ pf)
end; crush; elimtype False; eauto.
Qed.
Hint Resolve In_makeG'.
Now the main inductive lemma can be stated and proved simply.
Lemma dbify_sound : forall G t (e1 : Phoas.exp _ t) (e2 : Phoas.exp _ t),
exp_equiv G e1 e2
-> forall ts (w : wf ts e1) s,
G = makeG' s
-> DeBruijn.expDenote (dbify e1 w) s = Phoas.expDenote e2.
induction 1; crush; (let x := fresh in extensionality x); crush.
Qed.
In the usual way, we wrap dbify_sound into the final soundness theorem, formally establishing the expressive equivalence of PHOAS and de Bruijn index terms.
Theorem Dbify_sound : forall t (E : Exp t) (W : Wf E),
DeBruijn.expDenote (Dbify W) HNil = Phoas.ExpDenote E.
unfold Dbify, Phoas.ExpDenote; intros; eapply dbify_sound; eauto.
Qed.