Library Stlc.Connect
Connecting nominal and LN semantics
machine_step (h,t,s) ------> (h',t',s') nominal terms | | | decode | decode v v e - - -> e' locally nameless terms step e e' or e = e'
Require Import Metalib.Metatheory.
Require Import Stlc.Definitions.
Require Import Stlc.Lemmas.
Require Import Stlc.Nominal.
Import StlcNotations.
Translating nominal terms to LN terms
Fixpoint nom_to_exp (ne : n_exp) : exp :=
match ne with
| n_var x ⇒ var_f x
| n_app e1 e2 ⇒ app (nom_to_exp e1) (nom_to_exp e2)
| n_abs x e1 ⇒ abs (close_exp_wrt_exp x (nom_to_exp e1))
end.
We also define a translation from machine configurations to LN
terms. In this case we must substitute all definitions in the
heap through the terms and create all of the applications in
the stack.
Fixpoint apply_heap (h : heap) (e : exp) : exp :=
match h with
| nil ⇒ e
| (x , e') :: h' ⇒ apply_heap h' ([x ~> nom_to_exp e'] e)
end.
Fixpoint apply_stack h (s : list frame) (e :exp) : exp :=
match s with
| nil ⇒ e
| n_app2 e' :: s' ⇒ apply_stack h s' (app e (apply_heap h (nom_to_exp e')))
end.
The full decode function puts all of these parts together.
Definition decode (c:configuration) : exp :=
match c with
| (h,e,s) ⇒ apply_stack h s (apply_heap h (nom_to_exp e))
end.
Here's an example translation from the machine step demo.
Definition conf1 := ([(Y,n_var Z)], n_abs X (n_var X), [n_app2 (n_var Y)]).
Example decode1 : decode conf1 = (app (abs (var_b 0)) (var_f Z)).
Proof. default_simp.
unfold close_exp_wrt_exp.
default_simp.
Qed.
Connecting free variable functions.
Lemma fv_nom_fv_exp_eq : ∀ n,
fv_nom n [=] fv_exp (nom_to_exp n).
Proof.
induction n; intros; simpl; autorewrite with lngen; fsetdec.
Qed.
As we prove new lemmas, we can also extend the hint database with new
rewritings.
The Metatheory library contains two powerful tactics for simplifying
goals:
Below, we modify the behavior of these tactics by updating the following
two definitions, so that the lngen hint databases will be available.
- default_steps: repeat a bunch of simplifying steps, such as
simplifying the goal, inverting simple hypotheses, etc.
- default_simp: above plus case analysis for booleans and other sums
Ltac default_auto ::= auto with lngen.
Ltac default_autorewrite ::= autorewrite with lngen.
We also add a few more rewriting lemmas to the hint database to
automate our proofs.
Hint Rewrite subst_exp_open_exp_wrt_exp : lngen.
Hint Rewrite swap_size_eq : lngen.
Hint Resolve le_S_n : lngen.
Decoded terms are locally closed
Lemma nom_to_exp_lc : ∀ t, lc_exp (nom_to_exp t).
Proof.
induction t; default_steps.
Qed.
Hint Resolve nom_to_exp_lc : lngen.
Lemma apply_heap_lc : ∀ h e,
lc_exp e → lc_exp (apply_heap h e).
Proof.
alist induction h; default_simp.
Qed.
Hint Resolve apply_heap_lc : lngen.
Exercise: apply_stack_lc
Properties of apply_heap
Lemma apply_heap_abs : ∀ h e,
apply_heap h (abs e) = abs (apply_heap h e).
Proof.
alist induction h; default_simp.
Qed.
Hint Rewrite apply_heap_abs : lngen.
Lemma apply_heap_app : ∀ h e1 e2,
apply_heap h (app e1 e2) = app (apply_heap h e1) (apply_heap h e2).
Proof.
alist induction h; default_simp.
Qed.
Hint Rewrite apply_heap_app : lngen.
Exercise: apply_heap_open
Lemma apply_heap_open : ∀ h e e0,
lc_exp e0 →
apply_heap h (open e e0) =
open (apply_heap h e) (apply_heap h e0).
Proof.
Admitted.
Hint Rewrite apply_heap_open : lngen.
This last lemma "unsimpl"s the apply_heap function.
Lemma combine : ∀ h x e e',
apply_heap h ([x ~> nom_to_exp e] e') = (apply_heap ((x,e)::h) e').
Proof.
simpl. auto.
Qed.
Stacks as evaluation contexts
Lemma apply_stack_cong : ∀ s h e e',
step e e' →
step (apply_stack h s e) (apply_stack h s e').
Proof.
induction s; intros; try destruct a; default_simp.
Qed.
Connecting "freshening"
Lemma swap_spec : forall n w y, y `notin` fv_exp (nom_to_exp n) -> w <> y -> [w ~> var_f y] (nom_to_exp n) = nom_to_exp (swap w y n).
Exercise close_exp_wrt_exp_freshen
Lemma close_exp_wrt_exp_freshen : ∀ x y e,
y `notin` fv_exp e →
close_exp_wrt_exp x e =
close_exp_wrt_exp y ([x ~> var_f y] e).
Proof.
Admitted.
y `notin` fv_exp e →
close_exp_wrt_exp x e =
close_exp_wrt_exp y ([x ~> var_f y] e).
Proof.
Admitted.
One difficulty of swap_spec is that we need to use the induction
not on direct subterms, but on those that have had a swapping applied
to them. Swapping preserves the size of a nominal term, so we can
prove this result by induction on m, a bound on the size of the
term.
The difficulty in this proof comes from the n_abs case. In this
case, the term is is of the form n_abs x t for some binding
variable x. We don't know much about x; it could be w, or y
or some other variable. The first and last case are straightforward,
but the middle case causes difficulty: even though x is not free in
n_abs x t, it is free in t. Therefore, our induction hypothesis
doesn't apply.
To solve this problem, we need to generate a completely fresh
variable z for the binder, use the lemma above to replace y and
w with it, and then use the induction hypothesis.
Lemma swap_spec_aux : ∀ m t w y,
size t ≤ m →
y `notin` fv_exp (nom_to_exp t) →
w ≠ y →
[w ~> var_f y] (nom_to_exp t) =
nom_to_exp (swap w y t).
Proof.
induction m; intros t w y SZ;
destruct t; simpl in *; try omega;
intros.
+ unfold swap_var; default_simp.
+ unfold swap_var; default_simp.
{
rewrite subst_exp_fresh_eq; default_simp.
autorewrite with lngen in ×.
rewrite (close_exp_wrt_exp_freshen w y); try fsetdec.
rewrite IHm; default_simp. }
{
autorewrite with lngen in ×.
pick fresh z for (
fv_exp (nom_to_exp t) \u
fv_exp (nom_to_exp (swap w y t)) \u {{w}} \u {{y}}).
rewrite (close_exp_wrt_exp_freshen y z); auto.
rewrite (close_exp_wrt_exp_freshen w z); auto.
rewrite subst_exp_close_exp_wrt_exp; auto.
rewrite IHm with (y:=z); default_steps.
rewrite IHm with (y:=z); default_steps.
rewrite IHm with (y:=y); default_steps.
rewrite shuffle_swap; auto.
rewrite <- fv_nom_fv_exp_eq.
apply fv_nom_swap.
rewrite fv_nom_fv_exp_eq.
fsetdec.
}
{
rewrite <- IHm; default_steps.
autorewrite with lngen in ×.
fsetdec.
}
+ rewrite IHm; auto; try omega; try fsetdec.
rewrite IHm; auto; try omega; try fsetdec.
Qed.
Lemma swap_spec : ∀ t w y,
y `notin` fv_exp (nom_to_exp t) →
w ≠ y →
[w ~> var_f y] (nom_to_exp t) =
nom_to_exp (swap w y t).
Proof.
intros.
eapply swap_spec_aux with (t:=t)(m:=size t); auto.
Qed.
size t ≤ m →
y `notin` fv_exp (nom_to_exp t) →
w ≠ y →
[w ~> var_f y] (nom_to_exp t) =
nom_to_exp (swap w y t).
Proof.
induction m; intros t w y SZ;
destruct t; simpl in *; try omega;
intros.
+ unfold swap_var; default_simp.
+ unfold swap_var; default_simp.
{
rewrite subst_exp_fresh_eq; default_simp.
autorewrite with lngen in ×.
rewrite (close_exp_wrt_exp_freshen w y); try fsetdec.
rewrite IHm; default_simp. }
{
autorewrite with lngen in ×.
pick fresh z for (
fv_exp (nom_to_exp t) \u
fv_exp (nom_to_exp (swap w y t)) \u {{w}} \u {{y}}).
rewrite (close_exp_wrt_exp_freshen y z); auto.
rewrite (close_exp_wrt_exp_freshen w z); auto.
rewrite subst_exp_close_exp_wrt_exp; auto.
rewrite IHm with (y:=z); default_steps.
rewrite IHm with (y:=z); default_steps.
rewrite IHm with (y:=y); default_steps.
rewrite shuffle_swap; auto.
rewrite <- fv_nom_fv_exp_eq.
apply fv_nom_swap.
rewrite fv_nom_fv_exp_eq.
fsetdec.
}
{
rewrite <- IHm; default_steps.
autorewrite with lngen in ×.
fsetdec.
}
+ rewrite IHm; auto; try omega; try fsetdec.
rewrite IHm; auto; try omega; try fsetdec.
Qed.
Lemma swap_spec : ∀ t w y,
y `notin` fv_exp (nom_to_exp t) →
w ≠ y →
[w ~> var_f y] (nom_to_exp t) =
nom_to_exp (swap w y t).
Proof.
intros.
eapply swap_spec_aux with (t:=t)(m:=size t); auto.
Qed.
Connection for alpha-equivalence
Challenge Exercise: aeq_nom_to_exp
Lemma aeq_nom_to_exp : ∀ n1 n2, aeq n1 n2 → nom_to_exp n1 = nom_to_exp n2.
Proof.
Admitted.
Lemma nom_to_exp_eq_aeq : ∀ n1 n2, nom_to_exp n1 = nom_to_exp n2 → aeq n1 n2.
Proof.
Admitted.
Scoped configurations
Scoped heaps
Inductive scoped_heap (D : atoms) : heap → Prop :=
| scoped_nil : scoped_heap D nil
| scoped_cons : ∀ x e h,
x `notin` dom h \u D →
fv_exp (nom_to_exp e) [<=] dom h \u D →
scoped_heap D h →
scoped_heap D ((x,e)::h).
Recommended (Challenge) Exercise apply_heap_get
Lemma apply_heap_get : ∀ h D x e,
scoped_heap D h →
get x h = Some e →
apply_heap h (var_f x) = apply_heap h (nom_to_exp e).
Proof.
induction 1; intros; default_simp.
- Case "x is at the current heap location".
rewrite subst_exp_fresh_eq; auto. fsetdec.
- Case "x is later in the heap".
rewrite subst_exp_fresh_eq; auto.
Admitted.
Scoped stacks
Fixpoint fv_stack s :=
match s with
nil ⇒ {}
| n_app2 e :: s ⇒ fv_exp (nom_to_exp e) \u fv_stack s
end.
Stacks that are well-scoped can discard irrelevant bindings
from the heap.
Lemma apply_stack_fresh_eq : ∀ s x e1 h ,
x `notin` fv_stack s →
apply_stack ((x, e1) :: h) s = apply_stack h s.
Proof.
induction s; intros; try destruct a; default_simp.
rewrite IHs; auto.
Qed.
Simulation
Inductive scoped_conf : atoms → configuration → Prop :=
scoped_conf_witness : ∀ D h e s,
scoped_heap D h →
fv_exp (nom_to_exp e) [<=] dom h \u D →
fv_stack s [<=] dom h \u D →
scoped_conf D (h,e,s).
scoped_conf_witness : ∀ D h e s,
scoped_heap D h →
fv_exp (nom_to_exp e) [<=] dom h \u D →
fv_stack s [<=] dom h \u D →
scoped_conf D (h,e,s).
Lemma simulate_step : ∀ D h e s h' e' s' ,
machine_step D (h,e,s) = TakeStep _ (h',e',s') →
scoped_conf D (h,e,s) →
decode (h,e,s) = decode (h',e',s') ∨
step (decode (h,e,s)) (decode (h',e',s')).
Proof.
intros D h e s h' e' s' STEP SCOPE.
inversion SCOPE; subst; clear SCOPE.
simpl in ×.
destruct (isVal e) eqn:?.
destruct s.
- inversion STEP.
- destruct f eqn:?.
+ destruct e eqn:?; try solve [inversion STEP].
right.
destruct AtomSetProperties.In_dec.
×
destruct atom_fresh.
inversion STEP; subst; clear STEP.
simpl in *; autorewrite with lngen in ×.
rewrite combine.
rewrite apply_stack_fresh_eq; auto; try fsetdec.
apply apply_stack_cong.
simpl.
assert (x ≠ x0) by fsetdec.
rewrite <- swap_spec; auto; try fsetdec.
rewrite (subst_exp_spec _ _ x).
autorewrite with lngen; auto with lngen.
default_simp.
rewrite subst_exp_fresh_eq; autorewrite with lngen; auto.
apply step_beta; auto with lngen.
rewrite <- apply_heap_abs.
eapply apply_heap_lc.
auto with lngen.
rewrite H4. fsetdec.
×
admit.
- destruct e eqn:?; try solve [inversion STEP].
+
destruct (get x h) eqn:?; inversion STEP; subst; clear STEP.
left.
f_equal.
apply apply_heap_get with (D:= D); auto.
+
inversion STEP; subst; clear STEP.
left.
simpl.
rewrite apply_heap_app.
auto.
Admitted.
Lemma simulate_done : ∀ D h e s,
machine_step (dom h \u D) (h,e,s) = Done _ →
scoped_conf D (h,e,s) →
is_value (nom_to_exp e).
Proof. Admitted.
Challenge exercise simulate_error
Lemma simulate_error : ∀ D h e s,
machine_step (dom h \u D) (h,e,s) = Error _ →
scoped_conf D (h,e,s) →
not (∃ e0, step (decode (h,e,s)) e0).
Proof.
Admitted.