Library Uncurry
Require Omega.
Require Import Arith.
Require Import Setoid.
Require Import Wf.
Require Import Wf_nat.
Require Import Coqlib.
Open Scope nat_scope.
The source language
Parameter const: Set.
Parameters zero one: const.
Inductive uterm: Set :=
| UVar: nat -> uterm
| UConst: const -> uterm
| UFun: uterm -> uterm
| UApp: uterm -> uterm -> uterm
| ULet: uterm -> uterm -> uterm
| ULetrec: uterm -> uterm -> uterm.
CoInductive uvalue: Set :=
| UC: const -> uvalue
| UClos: uterm -> list uvalue -> uvalue.
Definition uenv := list uvalue.
Fixpoint UApp_n (a: uterm) (bl: list uterm) {struct bl} : uterm :=
match bl with
| nil => a
| b :: bs => UApp_n (UApp a b) bs
end.
Fixpoint UFun_n (n: nat) (a: uterm) {struct n} : uterm :=
match n with
| O => a
| S m => UFun (UFun_n m a)
end.
CoFixpoint uclos_rec (a: uterm) (e: uenv) : uvalue :=
UClos a (uclos_rec a e :: e).
Remark uclos_rec_unroll:
forall a e,
uclos_rec a e = UClos a (uclos_rec a e :: e).
Proof.
intros.
transitivity (match uclos_rec a e with UC c => UC c | UClos a' e' => UClos a' e' end).
generalize (uclos_rec a e). intro u. destruct u; auto.
auto.
Qed.
Remark UApp_n_app:
forall al1 al2 a,
UApp_n a (al1 ++ al2) = UApp_n (UApp_n a al1) al2.
Proof.
induction al1; intros; simpl. auto. rewrite IHal1. auto.
Qed.
Indexed big-step semantics
Inductive ueval: nat -> uenv -> uterm -> uvalue -> Prop :=
| ueval_var: forall e n v,
nth_error e n = Some v ->
ueval 0 e (UVar n) v
| ueval_const: forall e c,
ueval 0 e (UConst c) (UC c)
| ueval_fun: forall e a,
ueval 0 e (UFun a) (UClos a e)
| ueval_app: forall n1 n2 n3 n e a b c ce vb v,
ueval n1 e a (UClos c ce) ->
ueval n2 e b vb ->
ueval n3 (vb :: ce) c v ->
n = n1 + n2 + 1 + n3 ->
ueval n e (UApp a b) v
| ueval_let: forall n1 n2 n e a va b vb,
ueval n1 e a va ->
ueval n2 (va :: e) b vb ->
n = n1 + n2 + 1 ->
ueval n e (ULet a b) vb
| ueval_letrec: forall n e a b n1 vb,
ueval n1 (uclos_rec a e :: e) b vb ->
n = n1 + 1 ->
ueval n e (ULetrec a b) vb.
Inversion of curried applications
Inductive ueval_curried_app: nat -> uenv -> uterm -> uenv -> list uterm -> uvalue -> Prop :=
| ueval_curried_app_base: forall n e a1 e1 b1 v n1 n2 v1,
ueval n1 e b1 v1 ->
ueval n2 (v1 :: e1) a1 v ->
n = n1 + n2 + 1 ->
ueval_curried_app n e a1 e1 (b1 :: nil) v
| ueval_curried_app_cons: forall n e a1 e1 b1 bl v n1 v1 n2 a2 e2 n3,
ueval n1 e b1 v1 ->
ueval n2 (v1 :: e1) a1 (UClos a2 e2) ->
ueval_curried_app n3 e a2 e2 bl v ->
n = n1 + n2 + 1 + n3 ->
bl <> nil ->
ueval_curried_app n e a1 e1 (b1 :: bl) v.
Lemma ueval_UApp_n_inv:
forall e bl n a v,
ueval n e (UApp_n a bl) v ->
bl <> nil ->
exists n1, exists n2, exists a1, exists e1,
ueval n1 e a (UClos a1 e1) /\
ueval_curried_app n2 e a1 e1 bl v /\
n = n1 + n2.
Proof.
induction bl as [ | b1 bl IH]; intros.
congruence.
clear H0. simpl in H. destruct bl as [ | b2 bl ].
simpl in H. inv H.
exists n1; exists (n2 + n3 + 1); exists c; exists ce.
split. auto.
split. eapply ueval_curried_app_base; eauto.
omega.
exploit IH; eauto. congruence.
intros [n1 [n2 [a1 [e1 [A [B C]]]]]]. inv A.
exists n0; exists (n3 + 1 + n4 + n2); exists c; exists ce.
split. auto.
split. eapply ueval_curried_app_cons; eauto. omega.
congruence. omega.
Qed.
The target language: with N-ary functions
Inductive nterm: Set :=
| NVar: nat -> nterm
| NConst: const -> nterm
| NFun: nat -> nterm -> nterm
| NApp: nterm -> list nterm -> nterm
| NLet: nterm -> nterm -> nterm
| NLetrec: nat -> nterm -> nterm -> nterm.
CoInductive nvalue: Set :=
| NC: const -> nvalue
| NClos: nat -> nterm -> list nvalue -> nvalue.
Definition nenv := list nvalue.
CoFixpoint nclos_rec (n: nat) (b: nterm) (e: nenv) : nvalue :=
NClos n b (nclos_rec n b e :: e).
Remark nclos_rec_unroll:
forall n a e,
nclos_rec n a e = NClos n a (nclos_rec n a e :: e).
Proof.
intros.
transitivity (match nclos_rec n a e with NC c => NC c | NClos n' a' e' => NClos n' a' e' end).
generalize (nclos_rec n a e). intro w. destruct w; auto.
auto.
Qed.
Regular big-step semantics
Inductive neval: nenv -> nterm -> nvalue -> Prop :=
| neval_var: forall e n v,
nth_error e n = Some v ->
neval e (NVar n) v
| neval_const: forall e c,
neval e (NConst c) (NC c)
| neval_fun: forall n e a,
neval e (NFun n a) (NClos n a e)
| neval_app: forall e a bl n c ce vl v,
neval e a (NClos n c ce) ->
neval_list e bl vl ->
List.length bl = n ->
neval (List.rev vl ++ ce) c v ->
neval e (NApp a bl) v
| neval_let: forall e a va b vb,
neval e a va ->
neval (va :: e) b vb ->
neval e (NLet a b) vb
| neval_letrec: forall n e a b vb,
neval (nclos_rec n a e :: e) b vb ->
neval e (NLetrec n a b) vb
with neval_list: nenv -> list nterm -> list nvalue -> Prop :=
| neval_nil: forall e,
neval_list e nil nil
| neval_cons: forall e a al v vl,
neval e a v -> neval_list e al vl -> neval_list e (a :: al) (v :: vl).
Lemma neval_list_def:
forall e bl vl, neval_list e bl vl <-> list_forall2 (neval e) bl vl.
Proof.
intros; split.
generalize e bl vl. induction 1; constructor; auto.
generalize bl vl. induction 1; constructor; auto.
Qed.
Lemma neval_var':
forall f1 w f2 n,
n = length f1 ->
neval (f1 ++ w :: f2) (NVar n) w.
Proof.
intros. constructor. apply nth_error_app. auto.
Qed.
Approximation types
Inductive type : Set :=
| T: type
| F: list type -> type -> type.
Ahmad-Appel-McAllester step-indexed logical relations
Section REC.
Variable n: nat.
Variable rec: forall j: nat, j < n -> type -> uvalue -> nvalue -> Prop.
Lemma lt_rel_comp:
forall k j, k < n -> j <= k -> k - j < n.
Proof.
intros. omega.
Qed.
Definition rel_comp (k: nat) (P: k < n)
(t: type) (e: uenv) (a: uterm) (e': nenv) (a': nterm) : Prop :=
forall j v (Q: j <= k),
ueval j e a v ->
exists v', neval e' a' v' /\ rec (k - j) (lt_rel_comp k j P Q) t v v'.
Definition rel_comp_val (k: nat) (P: k < n)
(t: type) (e: uenv) (a: uterm) (v': nvalue) : Prop :=
forall j v (Q: j <= k),
ueval j e a v ->
rec (k - j) (lt_rel_comp k j P Q) t v v'.
Definition rel_val (t: type) (v: uvalue) (w: nvalue) : Prop :=
match t, v, w with
| T, UC i, NC j => i = j
| T, UClos a e, NClos 1 b f =>
forall j v w (P: j < n),
rec j P T v w -> rel_comp j P T (v :: e) a (w :: f) b
| F (targ :: nil) tres, UClos a e, NClos 1 b f =>
forall j v w (P: j < n),
rec j P targ v w -> rel_comp j P tres (v :: e) a (w :: f) b
| F (targ1 :: targ2 :: targs) tres, UClos a e, NClos ar b f =>
List.length (targ1 :: targ2 :: targs) = ar /\
forall j v w (P: j < n),
rec j P targ1 v w -> rel_comp_val j P (F (targ2 :: targs) tres) (v :: e) a (NClos (ar-1) b (w :: f))
| _, _, _ => False
end.
End REC.
Definition rval (k: nat) : type -> uvalue -> nvalue -> Prop :=
@Fix nat lt lt_wf (fun (n: nat) => type -> uvalue -> nvalue -> Prop) rel_val k.
Definition rcomp (k: nat) (t: type)
(e: uenv) (a: uterm) (e': nenv) (a': nterm) : Prop :=
forall j v,
j <= k ->
ueval j e a v ->
exists v', neval e' a' v' /\ rval (k - j) t v v'.
Definition rcompval (k: nat) (t: type)
(e: uenv) (a: uterm) (v': nvalue) : Prop :=
forall j v,
j <= k ->
ueval j e a v ->
rval (k - j) t v v'.
Axiom fun_extensionality:
forall (A B: Type) (f g: A -> B),
(forall x, f x = g x) -> f = g.
Axiom prop_extensionality:
forall (P Q: Prop), (P <-> Q) -> P = Q.
Inductive decomp_unary_fun: type -> type -> type -> Prop :=
| decomp_T:
decomp_unary_fun T T T
| decomp_F: forall targ tres,
decomp_unary_fun (F (targ :: nil) tres) targ tres.
Inductive rval_cases: nat -> type -> uvalue -> nvalue -> Prop :=
| rval_const: forall k n,
rval_cases k T (UC n) (NC n)
| rval_clos1: forall k t targ tres a e b f,
decomp_unary_fun t targ tres ->
(forall j v w,
j < k ->
rval j targ v w -> rcomp j tres (v :: e) a (w :: f) b) ->
rval_cases k t (UClos a e) (NClos 1 b f)
| rval_closN: forall k targ1 targ2 targs tres a e n b f,
List.length (targ1 :: targ2 :: targs) = n ->
(forall j v w,
j < k ->
rval j targ1 v w ->
rcompval j (F (targ2 :: targs) tres) (v :: e) a (NClos (n-1) b (w :: f))) ->
rval_cases k (F (targ1 :: targ2 :: targs) tres) (UClos a e) (NClos n b f).
Lemma rval_def:
forall k t v w,
rval k t v w <-> rval_cases k t v w.
Proof.
assert (forall k, rval k =
rel_val k (fun (j : nat) (P: j < k) => rval j)).
unfold rval. intro k.
apply (@Fix_eq nat lt lt_wf (fun (n: nat) => type -> uvalue -> nvalue -> Prop)).
intros.
apply fun_extensionality; intro t.
apply fun_extensionality; intro v.
apply fun_extensionality; intro w.
unfold rel_val. destruct t; destruct v; destruct w; auto.
destruct n; auto. destruct n; auto. apply prop_extensionality.
unfold rel_comp; split; intros.
rewrite <- H. eapply H0; eauto. rewrite H; auto.
rewrite H. eapply H0; eauto. rewrite <- H; auto.
destruct l; auto. destruct l; auto.
destruct n. auto. destruct n; auto. apply prop_extensionality.
unfold rel_comp; split; intros.
rewrite <- H. eapply H0; eauto. rewrite H; auto.
rewrite H. eapply H0; eauto. rewrite <- H; auto.
apply prop_extensionality.
unfold rel_comp_val; split; intros [A B]; split; auto; intros.
rewrite <- H. eapply B; eauto. rewrite H; auto.
rewrite H. eapply B; eauto. rewrite <- H; auto.
intros. rewrite H. unfold rel_val.
split; intros.
destruct t.
destruct v; destruct w; try contradiction.
subst c0. constructor.
destruct n; try contradiction. destruct n; try contradiction.
econstructor. constructor. auto.
destruct l. contradiction. destruct l; destruct v; destruct w; try contradiction.
destruct n. contradiction. destruct n. econstructor. constructor. auto. contradiction.
destruct H0. constructor; auto.
inv H0; auto. inv H1; auto.
Qed.
Monotonicity of
rval
Lemma rval_decr:
forall k1 k2 t v w,
rval k1 t v w -> k2 <= k1 -> rval k2 t v w.
Proof.
intros. rewrite rval_def in H. rewrite rval_def. inv H.
constructor.
econstructor. eauto. intros. apply H2; auto. omega.
constructor. auto. intros. apply H2; auto. omega.
Qed.
Lemma rval_fun_shape:
forall k targs tres v w,
rval k (F targs tres) v w ->
targs <> nil /\ exists b, exists f, w = NClos (length targs) b f.
Proof.
intros. rewrite rval_def in H. inv H. inv H0.
split. congruence. exists b; exists f; auto.
split. congruence. exists b; exists f; auto.
Qed.
Ltac minus0 := repeat rewrite <- minus_n_O in *.
Conditions for values to be related
Lemma rcomp_fun_rval:
forall k t e a f b n,
rcomp k t e (UFun a) f (NFun n b) <->
rval k t (UClos a e) (NClos n b f).
Proof.
intros; split; intros.
exploit (H 0). omega. constructor. intros [v' [A B]]. inv A. minus0. auto.
red; intros. inv H1. exists (NClos n b f); split.
constructor. minus0. auto.
Qed.
Lemma rcomp_const:
forall k t e f c c',
rcomp k t e (UConst c) f (NConst c') <-> t = T /\ c = c'.
Proof.
intros; split; intros.
exploit (H 0). omega. constructor. intros [v' [A B]]. inv A.
rewrite rval_def in B. inv B. auto.
destruct H. subst t c'. red; intros. inv H0. exists (NC c); split.
constructor. minus0. rewrite rval_def. constructor.
Qed.
Lemma rcomp_var:
forall k t e n f n' v w,
nth_error e n = Some v -> nth_error f n' = Some w ->
(rcomp k t e (UVar n) f (NVar n') <-> rval k t v w).
Proof.
intros; split; intros.
exploit (H1 0). omega. constructor. eauto. minus0. intros [w' [A B]].
inv A. congruence.
red; intros. inv H3. minus0. exists w; split. constructor; auto. congruence.
Qed.
Conditions for applications to be related
Lemma rcomp_appT:
forall k e1 a1 b1 e2 a2 b2,
rcomp k T e1 a1 e2 a2 -> rcomp k T e1 b1 e2 b2 ->
rcomp k T e1 (UApp a1 b1) e2 (NApp a2 (b2 :: nil)).
Proof.
intros; red; intros.
inv H2.
exploit (H n1); eauto. omega. intros [vf' [A B]].
exploit (H0 n2); eauto. omega. intros [vb' [D E]].
rewrite rval_def in B. inv B. inv H8.
assert (rcomp (k - (n1 + n2 + 1)) T (vb :: ce) c (vb' :: f) b).
apply H11. omega. eapply rval_decr; eauto. omega.
exploit (H2 n3); eauto. omega. intros [v' [P Q]].
exists v'; split.
eapply neval_app; eauto. constructor; eauto. constructor. simpl. auto.
replace (k - (n1 + n2 + 1 + n3))
with (k - (n1 + n2 + 1) - n3).
auto. omega.
Qed.
Definition rcomp_list (k: nat) (tl: list type)
(e: uenv) (al: list uterm)
(f: nenv) (bl: list nterm) : Prop :=
list_forall3 (fun t a b => rcomp k t e a f b) tl al bl.
Lemma rcomp_curried_app:
forall k n2 e1 a e bl1 v,
ueval_curried_app n2 e1 a e bl1 v ->
forall j n1 targs tres clos e2 bl2,
rval (j - n1) (F targs tres) (UClos a e) clos ->
rcomp_list k targs e1 bl1 e2 bl2 ->
j <= k -> n1 + n2 <= j ->
exists b, exists e', exists vl2, exists v',
clos = NClos (length targs) b e' /\
neval_list e2 bl2 vl2 /\
neval (List.rev vl2 ++ e') b v' /\
rval (j - (n1 + n2)) tres v v'.
Proof.
unfold rcomp_list; induction 1; intros.
inv H3. inv H11. rewrite rval_def in H2. inv H2. inv H8.
exploit (H9 n1); eauto. omega. intros [v1' [A B]].
assert (rcomp (j - (n0 + n1 + 1)) tres0 (v1 :: e1) a1 (v1' :: f) b).
apply H11. omega. eapply rval_decr; eauto. omega.
exploit (H1 n2); eauto. omega. intros [v' [C D]].
exists b; exists f; exists (v1' :: nil); exists v'.
split. auto.
split. constructor. auto. constructor.
split. simpl. auto.
replace (j - (n0 + (n1 + n2 + 1))) with (j - (n0 + n1 + 1) - n2) by omega.
auto.
inv H5. rewrite rval_def in H4. inv H4. inv H10. inv H13. congruence.
exploit (H11 n1); eauto. omega. intros [v1' [A B]].
assert (rcompval (j - (n0 + n1 + 1)) (F (targ2 :: targs) tres) (v1 :: e1) a1 (NClos (length (targ2 :: targs)) b (v1' :: f))).
apply H16. omega. eapply rval_decr; eauto. omega.
exploit (H2 n2); eauto. omega. intro C.
exploit IHueval_curried_app; eauto. omega. omega.
intros [cb [ce [vl2 [v' [P [Q [R S]]]]]]]. inv P.
exists cb; exists f; exists (v1' :: vl2); exists v'.
split. auto.
split. constructor; auto.
split. simpl. rewrite app_ass. simpl. auto.
replace (j - (n0 + (n1 + n2 + 1 + n3))) with (j - (n0 + n1 + 1) - (n2 + n3)) by omega.
auto.
Qed.
Lemma rcomp_appN:
forall k targs tres e1 a1 bl1 e2 a2 bl2,
bl1 <> nil ->
rcomp k (F targs tres) e1 a1 e2 a2 ->
rcomp_list k targs e1 bl1 e2 bl2 ->
rcomp k tres e1 (UApp_n a1 bl1) e2 (NApp a2 bl2).
Proof.
intros; red; intros.
exploit ueval_UApp_n_inv; eauto.
intros [n1 [n2 [a [e [A [B C]]]]]].
exploit (H0 n1); eauto. omega. intros [vf' [D E]].
exploit rcomp_curried_app; eauto. omega.
intros [b [e' [vl2 [v' [P [Q [R S]]]]]]].
exists v'; split.
subst vf'. econstructor; eauto.
red in H1. eapply list_forall3_length3; eauto.
subst j. auto.
Qed.
Typing environments for representation types
Definition typenv : Set := list type.
Inductive renv (k: nat): typenv -> uenv -> nenv -> Prop :=
| renv_nil:
renv k nil nil nil
| renv_cons: forall t te v e v' e',
rval k t v v' -> renv k te e e' ->
renv k (t :: te) (v :: e) (v' :: e').
Lemma renv_lookup:
forall k te e e', renv k te e e' ->
forall n t, nth_error te n = Some t ->
exists v, exists v', nth_error e n = Some v /\ nth_error e' n = Some v' /\ rval k t v v'.
Proof.
induction 1; intros.
destruct n; simpl in H; discriminate.
destruct n; simpl in H1.
inv H1. exists v; exists v'; auto.
simpl. auto.
Qed.
Lemma renv_decr:
forall k1 te e e', renv k1 te e e' ->
forall k2, k2 <= k1 -> renv k2 te e e'.
Proof.
induction 1; intros.
constructor.
constructor; auto. eapply rval_decr; eauto.
Qed.
Conditions for functions to be related
Lemma rcompval_fun:
forall tres targs k te e1 e2 a1 a2,
(forall k e1 e2,
renv k (List.rev targs ++ te) e1 e2 ->
rcomp k tres e1 a1 e2 a2) ->
renv k te e1 e2 ->
targs <> nil ->
rcompval k (F targs tres) e1 (UFun_n (length targs) a1) (NClos (length targs) a2 e2).
Proof.
induction targs; intros; simpl.
congruence.
red; intros. inv H3. minus0.
destruct targs. simpl.
rewrite rval_def. eapply rval_clos1. econstructor. intros.
apply H. simpl. constructor. auto. eapply renv_decr; eauto. omega.
rewrite rval_def. constructor. auto. intros.
apply IHtargs with (te := a :: te).
intros. apply H.
change (rev (a :: t :: targs)) with (rev (t :: targs) ++ (a :: nil)).
rewrite app_ass. auto.
constructor; auto. eapply renv_decr; eauto. omega.
congruence.
Qed.
Lemma rval_fun:
forall k te e f targs tres n a b,
(forall (k : nat) (e : uenv) (f : nenv),
renv k (rev targs ++ te) e f -> rcomp k tres e a f b) ->
renv k te e f ->
length targs = S n ->
rval k (F targs tres) (UClos (UFun_n n a) e) (NClos (length targs) b f).
Proof.
intros. destruct targs; simpl in H1. congruence. destruct targs; simpl in H1.
inv H1. rewrite rval_def. eapply rval_clos1. constructor. intros.
apply H. simpl. constructor. auto. eapply renv_decr; eauto. omega.
rewrite rval_def. apply rval_closN. auto. intros.
replace (length (t :: t0 :: targs) - 1) with (length (t0 :: targs)).
replace n with (length (t0 :: targs)).
apply rcompval_fun with (te := t :: te).
intros. apply H. simpl rev. repeat rewrite app_ass; simpl.
simpl in H4. rewrite app_ass in H4. simpl in H4. auto.
constructor; auto. eapply renv_decr; eauto. omega.
congruence. simpl; omega. simpl; omega.
Qed.
Lemma rval_fun_rec:
forall k targs tres n a e b f te,
(forall k e f,
renv k (rev targs ++ F targs tres :: te) e f ->
rcomp k tres e a f b) ->
renv k te e f ->
length targs = S n ->
rval k (F targs tres) (uclos_rec (UFun_n n a) e) (nclos_rec (S n) b f).
Proof.
intros.
assert (forall j, j <= k ->
rval j (F targs tres) (uclos_rec (UFun_n n a) e) (nclos_rec (S n) b f)).
intro j0. pattern j0. apply lt_wf_ind; intros.
rewrite uclos_rec_unroll. rewrite nclos_rec_unroll.
destruct targs; simpl in H1. discriminate. destruct targs; simpl in H1. inv H1.
simpl. rewrite rval_def. eapply rval_clos1. constructor. intros.
apply H. simpl. constructor. auto. constructor. apply H2. auto. omega.
eapply renv_decr; eauto. omega.
rewrite rval_def. apply rval_closN. simpl. auto. intros.
set (e1 := v :: uclos_rec (UFun_n n a) e :: e).
set (f1 := w :: nclos_rec (S n) b f :: f).
replace (S n - 1) with (length (t0 :: targs)).
replace n with (length (t0 :: targs)).
apply rcompval_fun with (te := t :: F (t :: t0 :: targs) tres :: te).
intros. apply H. simpl. rewrite app_ass. simpl. rewrite app_ass. simpl.
simpl in H6. rewrite app_ass in H6. auto.
unfold e1, f1. constructor. auto. constructor. apply H2. auto. omega.
eapply renv_decr; eauto. omega. congruence.
simpl. congruence. simpl. omega.
apply H2. omega.
Qed.
Alternate characterization of
rval on function types
Inductive rval_args: nat -> list type -> list uvalue -> list nvalue ->
uvalue -> uvalue -> nat -> Prop :=
| rval_args_nil: forall k v,
rval_args k nil nil nil v v k
| rval_args_cons: forall k targ1 targs v1 vl w1 wl a e res k' j j' clos,
rval j targ1 v1 w1 ->
ueval j' (v1 :: e) a clos ->
j < k -> j' <= j ->
rval_args (j - j') targs vl wl clos res k' ->
rval_args k (targ1 :: targs) (v1 :: vl) (w1 :: wl)
(UClos a e) res k'.
Remark rval_args_append:
forall k targs vl wl v v' k',
rval_args k targs vl wl v v' k' ->
forall targs' vl' wl' v'' k'',
rval_args k' targs' vl' wl' v' v'' k'' ->
rval_args k (targs ++ targs') (vl ++ vl') (wl ++ wl') v v'' k''.
Proof.
induction 1; intros.
simpl; auto.
simpl. eapply rval_args_cons; eauto.
Qed.
Inductive can_mult_apply: nat -> list type -> uvalue -> Prop :=
| can_mult_apply_nil: forall k v,
can_mult_apply k nil v
| can_mult_apply_cons: forall k targ1 targs a e,
(forall j v w j' v',
rval j targ1 v w ->
ueval j' (v :: e) a v' ->
j < k -> j' <= j ->
can_mult_apply (j - j') targs v') ->
can_mult_apply k (targ1 :: targs) (UClos a e).
Remark rval_fun_charact_1:
forall k targs vl wl v v' k',
rval_args k targs vl wl v v' k' ->
forall tres ar b f,
rval k (F targs tres) v (NClos ar b f) ->
exists w', neval (List.rev wl ++ f) b w' /\
rval k' tres v' w'.
Proof.
induction 1; intros.
rewrite rval_def in H. inv H. inv H5.
rewrite rval_def in H4. inv H4. inv H10.
clear IHrval_args. inv H3.
unfold rcomp in H13. simpl. eapply H13; eauto.
inversion H3; subst.
exploit H15; eauto. intro A. exploit IHrval_args; eauto.
simpl. intro B. rewrite app_ass. simpl. auto.
Qed.
Lemma rval_fun_charact_2:
forall tres targs k v b f,
can_mult_apply k targs v ->
(forall vl wl v' k',
rval_args k targs vl wl v v' k' ->
exists w', neval (List.rev wl ++ f) b w' /\ rval k' tres v' w') ->
targs <> nil ->
rval k (F targs tres) v (NClos (length targs) b f).
Proof.
induction targs; intros.
congruence.
destruct targs.
inv H. simpl. rewrite rval_def. eapply rval_clos1. econstructor.
intros; red; intros.
change (w :: f) with (rev (w :: nil) ++ f).
eapply H0. econstructor; eauto. constructor.
inv H. rewrite rval_def. apply rval_closN. auto.
intros; red; intros.
eapply IHtargs. eapply H6; eauto.
intros. replace (rev wl ++ w :: f) with (rev (w :: wl) ++ f).
eapply H0. econstructor; eauto.
simpl. rewrite app_ass. auto. congruence.
Qed.
Lemma rval_fun_charact_3:
forall tres targs k v w,
rval k (F targs tres) v w ->
can_mult_apply k targs v.
Proof.
induction targs; intros.
rewrite rval_def in H. inv H. inv H0.
rewrite rval_def in H. inv H. inv H0.
constructor. intros. constructor.
constructor. intros. eapply IHtargs.
unfold rcompval in H7. eauto.
Qed.
Lemma rval_fun_charact:
forall k targs tres v w,
rval k (F targs tres) v w <->
exists b, exists f,
w = NClos (length targs) b f /\
targs <> nil /\
can_mult_apply k targs v /\
(forall vl wl v' k',
rval_args k targs vl wl v v' k' ->
exists w', neval (List.rev wl ++ f) b w' /\ rval k' tres v' w').
Proof.
intros; split; intros.
exploit rval_fun_shape; eauto. intros [NOTNIL [b [f EQ]]].
exists b; exists f.
split. auto. split. auto.
split. eapply rval_fun_charact_3; eauto.
intros. subst w. eapply rval_fun_charact_1; eauto.
destruct H as [b [f [EQ [NOTNIL [A B]]]]].
subst w. eapply rval_fun_charact_2; eauto.
Qed.
Fixpoint NFun_n (n: nat) (a: nterm) {struct n} : nterm :=
match n with
| 0 => a
| S m => NFun 1 (NFun_n m a)
end.
Fixpoint list_vars (n: nat): list nterm :=
match n with
| 0 => nil
| S m => NVar m :: list_vars m
end.
Definition curry (n: nat): nterm :=
NFun 1 (NFun_n n (NApp (NVar n) (list_vars n))).
Fixpoint curry_type (targs: list type) (tres: type) {struct targs} : type :=
match targs with
| nil => tres
| t1 :: tl => F (t1 :: nil) (curry_type tl tres)
end.
Fixpoint NApp_n (a: nterm) (bl: list nterm) {struct bl} : nterm :=
match bl with
| nil => a
| b :: bs => NApp_n (NApp a (b :: nil)) bs
end.
Definition uncurry (n: nat): nterm :=
NFun 1 (NFun n (NApp_n (NVar n) (list_vars n))).
Subtyping without change of representation
Inductive subtype: type -> type -> Prop :=
| subtype_refl: forall t,
subtype t t
| subtype_inj:
subtype (F (T :: nil) T) T
| subtype_fun: forall targs tres targs' tres',
subtype_list targs' targs ->
subtype tres tres' ->
subtype (F targs tres) (F targs' tres')
| subtype_trans: forall t1 t2 t3,
subtype t1 t2 -> subtype t2 t3 -> subtype t1 t3
with subtype_list: list type -> list type -> Prop :=
| subtype_nil:
subtype_list nil nil
| subtype_cons: forall t1 l1 t2 l2,
subtype t1 t2 -> subtype_list l1 l2 ->
subtype_list (t1 :: l1) (t2 :: l2).
Scheme subtype_ind2 := Minimality for subtype Sort Prop
with subtype_list_ind2 := Minimality for subtype_list Sort Prop.
Coercions: subtyping with change of representation
Inductive coerce: nterm -> type -> type -> nterm -> Prop :=
| coerce_sub: forall b t1 t2,
subtype t1 t2 ->
coerce b t1 t2 b
| coerce_curry: forall b targs tres,
targs <> nil ->
coerce b (F targs tres)
(curry_type targs tres) (NApp (curry (length targs)) (b :: nil))
| coerce_uncurry: forall b targs tres,
targs <> nil ->
coerce b (curry_type targs tres)
(F targs tres) (NApp (uncurry (length targs)) (b :: nil))
| coerce_fun: forall b targs tres targs' tres' bargs bres,
coerce_list (list_vars (length targs)) targs' targs bargs ->
coerce (NApp (NVar (length targs)) bargs) tres tres' bres ->
coerce b (F targs tres)
(F targs' tres')
(NLet b (NFun (length targs) bres))
| coerce_trans: forall b1 t1 b2 t2 b3 t3,
coerce b1 t1 t2 b2 -> coerce b2 t2 t3 b3 ->
coerce b1 t1 t3 b3
with coerce_list: list nterm -> list type -> list type -> list nterm -> Prop :=
| coerce_nil:
coerce_list nil nil nil nil
| coerce_cons: forall t1 tl b1 bl b1' bl' t1' tl',
coerce t1 b1 b1' t1' -> coerce_list tl bl bl' tl' ->
coerce_list (t1 :: tl) (b1 :: bl) (b1' :: bl') (t1' :: tl').
Scheme coerce_ind2 := Minimality for coerce Sort Prop
with coerce_list_ind2 := Minimality for coerce_list Sort Prop.
Non-deterministic, type-directed translation of source terms to target terms
Inductive transl: typenv -> uterm -> type -> nterm -> Prop :=
| transl_var: forall te n t,
nth_error te n = Some t ->
transl te (UVar n) t (NVar n)
| transl_const: forall te c,
transl te (UConst c) T (NConst c)
| transl_fun: forall te a targs tres b,
targs <> nil ->
transl (List.rev targs ++ te) a tres b ->
transl te (UFun_n (length targs) a) (F targs tres) (NFun (length targs) b)
| transl_appT: forall te a1 a2 b1 b2,
transl te a1 T b1 ->
transl te a2 T b2 ->
transl te (UApp a1 a2) T (NApp b1 (b2 :: nil))
| transl_app: forall te a1 al2 targs tres b1 bl2,
targs <> nil ->
transl te a1 (F targs tres) b1 ->
transl_list te al2 targs bl2 ->
transl te (UApp_n a1 al2) tres (NApp b1 bl2)
| transl_let: forall te a1 a2 t1 t2 b1 b2,
transl te a1 t1 b1 ->
transl (t1 :: te) a2 t2 b2 ->
transl te (ULet a1 a2) t2 (NLet b1 b2)
| transl_letrec: forall te targ1 targs tres t2 a1 a2 b1 b2,
transl (List.rev (targ1 :: targs) ++ F (targ1 :: targs) tres :: te)
a1 tres b1 ->
transl (F (targ1 :: targs) tres :: te) a2 t2 b2 ->
transl te (ULetrec (UFun_n (length targs) a1) a2)
t2
(NLetrec (S (length targs)) b1 b2)
| transl_coerce: forall te a t b t' b',
transl te a t b -> coerce b t t' b' ->
transl te a t' b'
with transl_list: typenv -> list uterm -> list type -> list nterm -> Prop :=
| transl_nil: forall te,
transl_list te nil nil nil
| transl_cons: forall te a1 al t1 tl b1 bl,
transl te a1 t1 b1 -> transl_list te al tl bl ->
transl_list te (a1 :: al) (t1 :: tl) (b1 :: bl).
Scheme transl_ind2 := Minimality for transl Sort Prop
with transl_list_ind2 := Minimality for transl_list Sort Prop.
Definition sem_subtype_comp (t1 t2: type) : Prop :=
forall k e a f b, rcomp k t1 e a f b -> rcomp k t2 e a f b.
Definition sem_subtype_val (t1 t2: type) : Prop :=
forall k v w, rval k t1 v w -> rval k t2 v w.
Remark sem_subtype_val_comp:
forall t1 t2, sem_subtype_val t1 t2 -> sem_subtype_comp t1 t2.
Proof.
unfold sem_subtype_comp, sem_subtype_val; intros.
red; intros. exploit (H0 j); eauto. intros [v' [A B]].
exists v'; split. auto. apply H; auto.
Qed.
Semantic equivalence for the
subtype relation
Remark rval_subtype_list_fun:
forall tres tres',
sem_subtype_comp tres tres' ->
forall targs targs',
list_forall2 sem_subtype_val targs' targs ->
forall v v' n,
rval n (F targs tres) v v' ->
rval n (F targs' tres') v v'.
Proof.
induction 2; intros.
rewrite rval_def in H0. inv H0. inv H1.
rewrite rval_def in H2. inv H2. inv H3. inv H1.
rewrite rval_def. eapply rval_clos1. constructor. intros.
apply H. apply H4. auto. auto.
assert (exists a2, exists al', al = a2 :: al').
inv H1. exists a0; exists al0; auto.
destruct H2 as [a2 [al' EQ]]. subst al.
rewrite rval_def. apply rval_closN.
inv H1. symmetry. simpl. f_equal. f_equal. eapply list_forall2_length; eauto.
intros. red; intros.
apply IHlist_forall2. unfold rcompval in H10. eapply H10; eauto.
Qed.
Lemma rval_subtype:
forall t1 t2, subtype t1 t2 ->
forall k v w, rval k t1 v w -> rval k t2 v w.
Proof.
apply (subtype_ind2 sem_subtype_val (list_forall2 sem_subtype_val));
intros; hnf; intros.
auto.
rewrite rval_def in H. inv H. inv H0.
rewrite rval_def. econstructor; eauto. constructor.
eapply rval_subtype_list_fun; eauto. apply sem_subtype_val_comp; auto.
auto.
constructor.
constructor; auto.
Qed.
Lemma rcomp_subtype:
forall t1 t2, subtype t1 t2 ->
forall k e a f b, rcomp k t1 e a f b -> rcomp k t2 e a f b.
Proof.
intros t1 t2 SUB. change (sem_subtype_comp t1 t2).
apply sem_subtype_val_comp. red; intros; eapply rval_subtype; eauto.
Qed.
Semantic preservation for the
coerce relation
Definition sem_coerce_comp (b: nterm) (t: type) (t': type) (b': nterm) : Prop :=
forall k e a f, rcomp k t e a f b -> rcomp k t' e a f b'.
Lemma coerce_rcomp_var:
forall varno f k t' v w t b,
sem_coerce_comp (NVar varno) t' t b ->
rval k t' v w ->
nth_error f varno = Some w ->
exists w', neval f b w' /\ rval k t v w'.
Proof.
intros.
assert (rcomp k t (v :: nil) (UVar 0) f b).
apply H. red; intros. inv H3. simpl in H7. inv H7.
exists w. split. constructor. auto. replace (k - 0) with k by omega. auto.
replace k with (k - 0) by omega. eapply H2. omega. constructor. auto.
Qed.
Remark neval_list_vars:
forall vl e,
neval_list (vl ++ e) (list_vars (length vl)) (List.rev vl).
Proof.
intros vl0 e0.
assert(forall vl e,
neval_list (List.rev vl ++ e) (list_vars (length vl)) vl).
induction vl; intros; simpl. constructor.
rewrite app_ass. simpl. constructor; auto.
apply neval_var'. rewrite rev_length; auto.
generalize (H (List.rev vl0) e0).
rewrite rev_involutive. rewrite rev_length. auto.
Qed.
Remark length_list_vars:
forall n, List.length (list_vars n) = n.
Proof.
induction n; simpl; congruence.
Qed.
Lemma rval_curry_type:
forall targs tres k v ar b1 f1 b2 f2,
(forall args w,
length args = length targs ->
neval (args ++ f1) b1 w -> neval (args ++ f2) b2 w) ->
rval k (F targs tres) v (NClos ar b1 f1) ->
rval k (curry_type targs tres) v (NClos 1 (NFun_n (ar-1) b2) f2).
Proof.
induction targs; intros.
rewrite rval_def in H0. inv H0. inv H6.
rewrite rval_def in H0. inv H0. inv H6.
simpl. rewrite rval_def. eapply rval_clos1. econstructor. intros.
red; intros. exploit H8; eauto. intros [v' [A B]].
exists v'; split; auto. apply H with (args := w :: nil); auto.
change (curry_type (a :: targ2 :: targs0) tres)
with (F (a :: nil) (curry_type (targ2 :: targs0) tres)).
rewrite rval_def. eapply rval_clos1. econstructor. intros; red; intros.
exists (NClos 1 (NFun_n (length targs0) b2) (w :: f2)); split.
simpl. constructor.
replace (length targs0) with (length (targ2 :: targs0) - 1).
apply IHtargs with b1 (w :: f1).
intros. simpl in H4.
replace (args ++ w :: f2) with ((args ++ (w :: nil)) ++ f2).
apply H. simpl. rewrite app_length. simpl. omega.
rewrite app_ass. simpl. auto. rewrite app_ass. auto.
unfold rcompval in H10; eapply H10; eauto.
simpl; omega.
Qed.
Lemma rcomp_curry:
forall k targs tres e a f b,
targs <> nil ->
rcomp k (F targs tres) e a f b ->
rcomp k (curry_type targs tres) e a f (NApp (curry (length targs)) (b :: nil)).
Proof.
red; intros.
destruct (H0 _ _ H1 H2) as [v' [A B]].
set (body := NApp (NVar (length targs)) (list_vars (length targs))).
econstructor; split.
unfold curry. econstructor. constructor.
econstructor. eauto. constructor. auto.
simpl. fold body. replace (length targs) with (S (length targs - 1)).
simpl. constructor. destruct targs. congruence. simpl. omega.
exploit rval_fun_shape; eauto. intros [NOTNIL [b' [f' EQ]]].
subst v'. apply rval_curry_type with b' f'.
intros.
unfold body. econstructor. apply neval_var'. auto.
rewrite <- H3. apply neval_list_vars.
rewrite length_list_vars. auto. rewrite rev_involutive. auto.
auto.
Qed.
Inductive neval_multapp: nvalue -> list nvalue -> nvalue -> Prop :=
| neval_multapp_nil: forall v,
neval_multapp v nil v
| neval_multapp_cons: forall b f v1 vl v v',
neval (v1 :: f) b v' -> neval_multapp v' vl v ->
y" type_scope">neval_multapp (NClos 1 b f) (v1 :: vl) v.
Lemma rval_uncurry_type:
forall tres targs k v w body env,
targs <> nil ->
(forall args res,
List.length args = List.length targs ->
neval_multapp w args res -> neval (List.rev args ++ env) body res) ->
rval k (curry_type targs tres) v w ->
rval k (F targs tres) v (NClos (length targs) body env).
Proof.
induction targs; intros. congruence. destruct targs.
simpl in H1. simpl. rewrite rval_def in H1. inv H1. inv H2.
rewrite rval_def. eapply rval_clos1. constructor. intros; red; intros.
exploit H3; eauto. intros [v' [A B]]. exists v'; split; auto.
change (w :: env) with (List.rev (w :: nil) ++ env). apply H0. auto.
econstructor. eauto. constructor.
simpl in H1. rewrite rval_def in H1. inv H1. inv H2.
change (F (t :: nil) (curry_type targs tres))
with (curry_type (t :: targs) tres) in H3.
rewrite rval_def. eapply rval_closN. auto. intros; red; intros.
exploit H3; eauto. intros [v' [A B]].
apply IHtargs with v'; auto. congruence.
intros. replace (rev args ++ w :: env) with (rev (w :: args) ++ env).
apply H0. simpl in *. congruence. econstructor. eauto. auto.
simpl. rewrite app_ass. auto.
Qed.
Lemma neval_NApp_n:
forall v args res,
neval_multapp v args res ->
forall fn e,
neval (rev args ++ e) fn v ->
neval (rev args ++ e) (NApp_n fn (list_vars (length args))) res.
Proof.
induction 1; simpl; intros.
auto.
rewrite app_ass. simpl. apply IHneval_multapp.
econstructor. rewrite app_ass in H1. simpl in H1. eauto.
constructor. apply neval_var'. rewrite rev_length; auto. constructor. auto.
simpl. auto.
Qed.
Lemma rcomp_uncurry:
forall k targs tres e a f b,
targs <> nil ->
rcomp k (curry_type targs tres) e a f b ->
rcomp k (F targs tres) e a f (NApp (uncurry (length targs)) (b :: nil)).
Proof.
red; intros.
destruct (H0 _ _ H1 H2) as [v' [A B]].
econstructor; split.
unfold uncurry. econstructor. constructor. constructor. eauto. constructor. auto.
simpl. constructor.
apply rval_uncurry_type with v'; auto.
intros. rewrite <- H3. apply neval_NApp_n with v'; auto.
apply neval_var'. rewrite rev_length; auto.
Qed.
Lemma sem_coerce_comp_eval:
forall b t t' b' f v w k,
sem_coerce_comp b t t' b' ->
neval f b w -> rval k t v w ->
exists w', neval f b' w' /\ rval k t' v w'.
Proof.
intros. red in H.
assert (rcomp k t (v :: nil) (UVar 0) f b).
red. intros. inv H3. simpl in H7. inv H7.
replace (k - 0) with k by omega. exists w; auto.
exploit (H _ _ _ _ H2 0). omega. constructor. simpl; reflexivity.
replace (k - 0) with k by omega. auto.
Qed.
Lemma rcomp_recursive_coerce_can_mult_apply:
forall k targs v,
can_mult_apply k targs v ->
forall targs' bargs,
list_forall4 sem_coerce_comp (list_vars (length targs)) targs' targs bargs ->
can_mult_apply k targs' v.
Proof.
induction 1; intros; simpl in *.
inv H. constructor.
inv H1.
constructor; intros.
set (f := replicate (NC zero) (length targs) ++ w :: nil).
assert (exists w', neval f d1 w' /\ rval j targ1 v w').
eapply coerce_rcomp_var with (varno := length targs).
eassumption. eauto. unfold f. apply nth_error_app.
apply replicate_length.
destruct H5 as [w' [A B]].
eapply H0; eauto.
Qed.
Remark rval_args_length:
forall k targs vl wl v v' k',
rval_args k targs vl wl v v' k' -> length wl = length targs.
Proof.
induction 1; simpl; congruence.
Qed.
Lemma rcomp_recursive_coerce_rval_args:
forall k targs' vl wl v v' k',
rval_args k targs' vl wl v v' k' ->
forall targs bargs f,
list_forall4 sem_coerce_comp (list_vars (length targs)) targs' targs bargs ->
exists wl',
neval_list (rev wl ++ f) bargs wl' /\
rval_args k targs vl wl' v v' k'.
Proof.
induction 1; intros.
inv H. simpl. exists (@nil nvalue); split. constructor. constructor.
inv H4. simpl in H5; inv H5.
assert (exists w1', neval (rev (w1::wl) ++ f) d1 w1'
/\ rval j c1 v1 w1').
eapply coerce_rcomp_var with (varno := length cl).
eexact H8. eauto.
simpl. rewrite app_ass. simpl. apply nth_error_app.
rewrite rev_length. transitivity (length targs). eapply rval_args_length; eauto.
exploit list_forall4_length2; eauto. rewrite length_list_vars. auto.
destruct H4 as [w1' [A B]].
exploit IHrval_args; eauto. intros [wl' [C D]].
exists (w1' :: wl'); split.
constructor. auto. simpl. rewrite app_ass; simpl. eexact C.
econstructor; eauto.
Qed.
Lemma rcomp_recursive_coerce:
forall k targs tres targs' tres' bargs bres v clos f,
list_forall4 sem_coerce_comp (list_vars (length targs)) targs' targs bargs ->
sem_coerce_comp (NApp (NVar (length targs)) bargs) tres tres' bres ->
rval k (F targs tres) v clos ->
rval k (F targs' tres') v (NClos (length targs) bres (clos :: f)).
Proof.
intros.
rewrite rval_fun_charact in H1.
destruct H1 as [b' [f' [EQ [NOTNIL [A B]]]]].
assert (L: length targs' = length targs).
exploit list_forall4_length2; eauto.
exploit list_forall4_length3; eauto. congruence.
rewrite rval_fun_charact. exists bres; exists (clos :: f).
split. f_equal. auto.
split. inv H; congruence.
split. eapply rcomp_recursive_coerce_can_mult_apply; eauto.
intros. exploit rcomp_recursive_coerce_rval_args; eauto.
instantiate (1 := clos :: f). intros [wl' [D E]].
exploit B; eauto. intros [w [P Q]].
eapply sem_coerce_comp_eval; eauto.
econstructor.
rewrite EQ. apply neval_var'. rewrite rev_length. rewrite <- L.
symmetry; eapply rval_args_length; eauto.
eexact D.
rewrite <- (length_list_vars (length targs)). eapply list_forall4_length4; eauto.
exact P.
Qed.
Lemma coerce_rcomp:
forall b t t' b',
coerce b t t' b' ->
forall k e a f,
rcomp k t e a f b ->
rcomp k t' e a f b'.
Proof.
apply (coerce_ind2 sem_coerce_comp (list_forall4 sem_coerce_comp)); intros.
red; intros; eapply rcomp_subtype; eauto.
red; intros; eapply rcomp_curry; eauto.
red; intros; eapply rcomp_uncurry; eauto.
red; intros; red; intros. destruct (H3 _ _ H4 H5) as [v' [A B]].
econstructor; split.
econstructor. eauto. constructor.
eapply rcomp_recursive_coerce; eauto.
red; intros; auto.
constructor.
constructor; auto.
Qed.
The main semantic preservation result
Lemma transl_rcomp:
forall te a t b, transl te a t b ->
forall k e f, renv k te e f -> rcomp k t e a f b.
Proof.
apply (transl_ind2
(fun te a t b => forall k e f, renv k te e f -> rcomp k t e a f b)
(fun te al tl bl => forall k e f, renv k te e f -> rcomp_list k tl e al f bl));
intros.
exploit renv_lookup; eauto. intros [v [w [A [B C]]]].
rewrite (rcomp_var k t _ _ _ _ _ _ A B). auto.
rewrite rcomp_const. auto.
red; intros. exists (NClos (length targs) b f); split. constructor.
assert (exists n, length targs = S n).
destruct targs. congruence. exists (length targs); auto.
destruct H5 as [n EQ]. rewrite EQ in H4. inv H4. replace (k - 0) with k by omega.
eapply rval_fun; eauto.
eapply rcomp_appT; eauto.
eapply rcomp_appN; eauto. inv H2; congruence.
red; intros. inv H5.
generalize (H0 _ _ _ H3); intro.
exploit (H5 n1); eauto. omega. intros [va' [A B]].
assert (rcomp (k - n1) t2 (va :: e) a2 (va' :: f) b2).
apply H2. constructor. auto. eapply renv_decr; eauto. omega.
exploit (H6 n2); eauto. omega. intros [vb' [C D]].
exists vb'; split. econstructor; eauto.
eapply rval_decr; eauto. omega.
red; intros. inv H5.
assert (renv k (F (targ1 :: targs) tres :: te)
(uclos_rec (UFun_n (length targs) a1) e :: e)
(nclos_rec (S (length targs)) b1 f :: f)).
constructor. apply rval_fun_rec with te; auto. auto.
generalize (H2 _ _ _ H5); intro.
exploit (H6 n1); eauto. omega. intros [w [A B]].
exists w; split. econstructor; eauto. eapply rval_decr; eauto. omega.
eapply coerce_rcomp; eauto.
constructor.
constructor; auto. change (rcomp_list k tl e al f bl). auto.
Qed.
Correctness of translation follows as a corollary
Theorem transl_correct:
forall a b t n c,
transl nil a t b ->
ueval n nil a (UC c) ->
neval nil b (NC c).
Proof.
intros.
exploit transl_rcomp; eauto.
constructor.
intros [v' [A B]].
rewrite rval_def in B. inv B.
auto.
Qed.