Library Uncurry

Higher-order uncurrying and step-indexed logical relations


Require Omega.
Require Import Arith.
Require Import Setoid.
Require Import Wf.
Require Import Wf_nat.
Require Import Coqlib.
Open Scope nat_scope.

Source and target languages


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.

Relating source and target terms


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.

Currying, uncurrying, and coercions


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.

Proof of semantic preservation


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.