Library TranslValid

Application to translation validation


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

Require Import Uncurry.

A mutual induction principle for types and type lists.

Section TYPE_IND.

Variable P: type -> Prop.
Variable Q: list type -> Prop.

Hypothesis P_T: P T.
Hypothesis P_F: forall args res, Q args -> P res -> P (F args res).
Hypothesis Q_nil: Q nil.
Hypothesis Q_cons: forall t l, P t -> Q l -> Q (t::l).

Fixpoint type_ind2 (ty: type) : P ty :=
  match ty as t return P t with
  | T => P_T
  | F args res =>
      let fix type_list_ind2 (tl: list type) : Q tl :=
        match tl as l return Q l with
        | nil => Q_nil
        | ty1::tys => Q_cons ty1 tys (type_ind2 ty1) (type_list_ind2 tys)
        end
      in P_F args res (type_list_ind2 args) (type_ind2 res)
  end.

End TYPE_IND.

Decidable equality between types

Fixpoint beq_type (t1 t2: type) {struct t1} : bool :=
  match t1, t2 with
  | T, T => true
  | F targs1 tres1, F targs2 tres2 =>
      let fix beq_typelist (tl1 tl2: list type) {struct tl1} : bool :=
        match tl1, tl2 with
        | nil, nil => true
        | h1::l1, h2::l2 => beq_type h1 h2 && beq_typelist l1 l2
        | _, _ => false
        end in
      beq_typelist targs1 targs2 && beq_type tres1 tres2
  | _, _ => false
  end.

Fixpoint beq_typelist (tl1 tl2: list type) {struct tl1} : bool :=
  match tl1, tl2 with
  | nil, nil => true
  | h1::l1, h2::l2 => beq_type h1 h2 && beq_typelist l1 l2
  | _, _ => false
  end.

Lemma beq_type_correct:
  forall t1 t2, if beq_type t1 t2 then t1 = t2 else t1 <> t2.
Proof.
  apply (type_ind2
    (fun t1 => forall t2, if beq_type t1 t2 then t1 = t2 else t1 <> t2)
    (fun tl1 => forall tl2,
      if beq_typelist tl1 tl2 then tl1 = tl2 else tl1 <> tl2));
  intros.
  destruct t2; simpl; congruence.
  destruct t2; simpl. congruence.
  change (if beq_typelist args l && beq_type res t2
          then F args res = F l t2
          else F args res <> F l t2).
  generalize (H l). destruct (beq_typelist args l). intro.
  generalize (H0 t2). destruct (beq_type res t2); simpl; intros; congruence.
  simpl; congruence.
  destruct tl2; simpl; congruence.
  destruct tl2; simpl. congruence.
  generalize (H t0). destruct (beq_type t t0).
  generalize (H0 tl2). destruct (beq_typelist l tl2); simpl; congruence.
  simpl; congruence.
Qed.

Definition eq_type (t1 t2: type) : {t1=t2} + {t1<>t2}.
Proof.
  intros t1 t2. generalize (beq_type_correct t1 t2). case (beq_type t1 t2); intros.
  left; auto. right; auto.
Defined.

Checking the subtype relation


A syntax-directed variant of the subtype predicate.

Inductive sd_subtype: type -> type -> Prop :=
  | sd_subtype_top:
      sd_subtype T T
  | sd_subtype_inj: forall tres,
      sd_subtype tres T ->
      sd_subtype (F (T :: nil) tres) T
  | sd_subtype_fun: forall targs tres targs' tres',
      sd_subtype_list targs' targs ->
      sd_subtype tres tres' ->
      sd_subtype (F targs tres) (F targs' tres')

with sd_subtype_list: list type -> list type -> Prop :=
  | sd_subtype_nil:
      sd_subtype_list nil nil
  | sd_subtype_cons: forall t1 l1 t2 l2,
      sd_subtype t1 t2 -> sd_subtype_list l1 l2 ->
      sd_subtype_list (t1 :: l1) (t2 :: l2).

Scheme sd_subtype_ind2 := Minimality for sd_subtype Sort Prop
  with sd_subtype_list_ind2 := Minimality for sd_subtype_list Sort Prop.

Remark sd_subtype_list_length:
  forall l1 l2, sd_subtype_list l1 l2 -> length l2 = length l1.
Proof. induction 1; simpl; congruence. Qed.

Lemma sd_subtype_correct:
  forall t1 t2, sd_subtype t1 t2 -> subtype t1 t2.
Proof.
  apply (sd_subtype_ind2
    (fun t1 t2 => subtype t1 t2)
    (fun l1 l2 => subtype_list l1 l2)); intros.
  constructor.
  eapply subtype_trans with (F (T:: nil) T).
  apply subtype_fun. constructor. constructor. constructor. eauto.
  constructor.
  apply subtype_fun; auto.
  constructor.
  constructor; auto.
Qed.

Lemma sd_subtype_refl:
  forall t, sd_subtype t t.
Proof.
  apply (type_ind2 (fun t => sd_subtype t t)
                   (fun l => sd_subtype_list l l));
  intros; constructor; auto.
Qed.

Lemma sd_subtype_trans:
  forall t2 t1 t3,
  sd_subtype t1 t2 -> sd_subtype t2 t3 -> sd_subtype t1 t3.
Proof.
  apply (type_ind2
    (fun t2 => forall t1 t3,
     sd_subtype t1 t2 -> sd_subtype t2 t3 -> sd_subtype t1 t3)
    (fun t2 => forall t1 t3,
     sd_subtype_list t1 t2 -> sd_subtype_list t2 t3 -> sd_subtype_list t1 t3));
  intros.
  inv H0. auto.
  inv H1. inv H2. inv H6. inv H3. inv H8. constructor. eauto.
  constructor; eauto.
  inv H; inv H0; constructor.
  inv H1; inv H2; constructor; eauto.
Qed.

Lemma sd_subtype_complete:
  forall t1 t2, subtype t1 t2 -> sd_subtype t1 t2.
Proof.
  apply (subtype_ind2
    (fun t1 t2 => sd_subtype t1 t2)
    (fun l1 l2 => sd_subtype_list l1 l2)); intros.
  apply sd_subtype_refl.
  constructor. constructor.
  constructor; auto.
  eapply sd_subtype_trans; eauto.
  constructor.
  constructor; auto.
Qed.

Fixpoint size_type (t: type) : nat :=
  match t with
  | T => 0
  | F targs tres =>
      let fix size_typelist (tl: list type) : nat :=
        match tl with
        | nil => 0
        | t1 :: tl' => size_type t1 + size_typelist tl' + 1
        end
      in 1 + size_typelist targs + size_type tres
  end.

Fixpoint size_typelist (tl: list type) : nat :=
        match tl with
        | nil => 0
        | t1 :: tl' => size_type t1 + size_typelist tl' + 1
        end.

Fixpoint is_subtype_rec (n: nat) (t1 t2: type) {struct n} : bool :=
  match n with
  | 0 => false
  | S m =>
      match t2, t1 with
      | T, T => true
      | T, F (T :: nil) tres => is_subtype_rec m tres T
      | F targs2 tres2, F targs1 tres1 =>
          let fix is_subtype_list (tl1 tl2: list type) {struct tl1} : bool :=
            match tl1, tl2 with
            | nil, nil => true
            | t1::tl1', t2::tl2' =>
                is_subtype_rec m t1 t2 && is_subtype_list tl1' tl2'
            | _, _ => false
            end in
          is_subtype_list targs2 targs1 && is_subtype_rec m tres1 tres2
      | _, _ => false
      end
  end.

Definition is_subtype (t1 t2: type) : bool :=
  is_subtype_rec (S (size_type t1 + size_type t2)) t1 t2.

Lemma is_subtype_rec_correct:
  forall n t1 t2, is_subtype_rec n t1 t2 = true -> sd_subtype t1 t2.
Proof.
  induction n; simpl; intros.
  discriminate.
  destruct t2; destruct t1; try discriminate.
  constructor.
  destruct l; try discriminate.
  destruct t; try discriminate.
  destruct l; try discriminate.
  constructor; auto.
  destruct (andb_prop _ _ H); clear H.
  constructor.
  generalize l l0 H0. induction l1; intros.
  destruct l1. constructor. discriminate.
  destruct l2. discriminate.
  destruct (andb_prop _ _ H2); clear H2. constructor; auto.
  auto.
Qed.

Lemma is_subtype_correct:
  forall t1 t2, is_subtype t1 t2 = true -> sd_subtype t1 t2.
Proof.
  unfold is_subtype. intros. eapply is_subtype_rec_correct. eauto.
Qed.

Lemma is_subtype_rec_complete:
  forall t1 t2, sd_subtype t1 t2 ->
  forall n, n > size_type t1 + size_type t2 -> is_subtype_rec n t1 t2 = true.
Proof.
  apply (sd_subtype_ind2
    (fun t1 t2 => forall n, n > size_type t1 + size_type t2 -> is_subtype_rec n t1 t2 = true)
    (fun tl1 tl2 => forall n, n > size_typelist tl1 + size_typelist tl2 ->
      (fix is_subtype_list (tl1 tl2: list type) {struct tl1} : bool :=
            match tl1, tl2 with
            | nil, nil => true
            | t1::tl1', t2::tl2' =>
                is_subtype_rec n t1 t2 && is_subtype_list tl1' tl2'
            | _, _ => false
            end) tl1 tl2 = true));
  simpl; intros.
  destruct n. omegaContradiction. auto.
  destruct n. omegaContradiction. simpl. apply H0. simpl. omega.
  destruct n. omegaContradiction. simpl.
  change (S n > S (size_typelist targs + size_type tres) +
                S (size_typelist targs' + size_type tres')) in H3.
  apply andb_true_intro. split. apply (H0 n). omega. apply H2. omega.
  auto.
  apply andb_true_intro. split. apply H0. omega. apply (H2 n). omega.
Qed.

Lemma is_subtype_complete:
  forall t1 t2, sd_subtype t1 t2 -> is_subtype t1 t2 = true.
Proof.
  intros. unfold is_subtype. apply is_subtype_rec_complete. auto. omega.
Qed.

Lemma is_subtype_decision_procedure:
  forall t1 t2, is_subtype t1 t2 = true <-> subtype t1 t2.
Proof.
  intros; split; intros.
  apply sd_subtype_correct. apply is_subtype_correct; auto.
  apply is_subtype_complete. apply sd_subtype_complete. auto.
Qed.

Lemma sd_subtype_curry:
  forall tres1 tres2, sd_subtype tres1 tres2 ->
  forall targs2 targs1, sd_subtype_list targs2 targs1 ->
  sd_subtype (curry_type targs1 tres1) (curry_type targs2 tres2).
Proof.
  induction 2; simpl. auto.
  constructor. constructor. auto. constructor. auto.
Qed.

Lemma sd_subtype_curry_inv:
  forall tres1 tres2 targs1 targs2,
  length targs1 = length targs2 ->
  sd_subtype (curry_type targs1 tres1) (curry_type targs2 tres2) ->
  sd_subtype_list targs2 targs1 /\ sd_subtype tres1 tres2.
Proof.
  induction targs1; intros; destruct targs2; simpl in *; try discriminate.
  split. constructor. auto.
  inv H0. inv H4. inv H7.
  exploit (IHtargs1 targs2); eauto. intros [A B].
  split. constructor; auto. auto.
Qed.

Inference of coercions


Measures for coercions

Fixpoint sz_type (t: type) : nat :=
  match t with
  | T => 1
  | F targs tres =>
      let fix sz_typelist (tl: list type) : nat :=
        match tl with
        | nil => 1
        | t :: nil => sz_type t
        | t :: tl => sz_type t + sz_typelist tl + 2
        end in
      sz_typelist targs + sz_type tres + 1
  end.

Fixpoint sz_typelist (tl: list type) : nat :=
  match tl with
  | nil => 1
  | t :: nil => sz_type t
  | t :: tl => sz_type t + sz_typelist tl + 2
  end.

Remark sz_type_pos:
  forall t, sz_type t >= 1.
Proof.
  intro. destruct t; simpl; omega.
Qed.

Remark sz_typelist_pos:
  forall tl, sz_typelist tl >= 1.
Proof.
  intro. destruct tl; simpl. omega. destruct tl. apply sz_type_pos. omega.
Qed.

Remark sz_type_F:
  forall targs tres, sz_type (F targs tres) = sz_typelist targs + sz_type tres + 1.
Proof.
  intros; reflexivity.
Qed.

Lemma sz_curry_type:
  forall tres targs,
  length targs > 1 ->
  sz_type (curry_type targs tres) < sz_type (F targs tres).
Proof.
  induction targs; intros.
  simpl in H. omegaContradiction.
  destruct targs; simpl in H. omegaContradiction.
  destruct targs. simpl. omega.
  change (curry_type (a :: t :: t0 :: targs) tres)
    with (F (a :: nil) (curry_type (t :: t0 :: targs) tres)).
  repeat rewrite sz_type_F.
  change (sz_typelist (a :: nil)) with (sz_type a).
  apply lt_le_trans with
    (sz_type a + sz_type (F (t :: t0 :: targs) tres) + 1).
  exploit IHtargs. simpl; omega. omega.
  rewrite sz_type_F. simpl. omega.
Qed.

Definition sz_2 (t1 t2: type) :=
  sz_type t1 + sz_type t2 +
  match t2 with T => 3 | F _ _ => 0 end.

Definition sz_list_2 (tl1 tl2: list type) :=
  sz_typelist tl1 + sz_typelist tl2 + 3.

Remark sz_2_T:
  forall t, sz_2 t (F (T::nil) T) < sz_2 t T.
Proof.
  unfold sz_2; intros; simpl. omega.
Qed.

Remark sz_2_F_res:
  forall targs tres targs' tres',
  sz_2 tres tres' < sz_2 (F targs tres) (F targs' tres').
Proof.
  unfold sz_2; intros. repeat rewrite sz_type_F.
  apply le_lt_trans with
    (sz_type tres + sz_type tres' + 3).
  destruct tres'; omega.
  generalize (sz_typelist_pos targs) (sz_typelist_pos targs').
  omega.
Qed.

Remark sz_2_F_arglist:
  forall targs tres targs' tres',
  sz_list_2 targs' targs < sz_2 (F targs tres) (F targs' tres').
Proof.
  unfold sz_2, sz_list_2; intros. repeat rewrite sz_type_F.
  generalize (sz_type_pos tres) (sz_type_pos tres').
  omega.
Qed.

Remark sz_2_head:
  forall targ targs targ' targs',
  sz_2 targ targ' <= sz_list_2 (targ::targs) (targ'::targs').
Proof.
  intros. unfold sz_2, sz_list_2.
  apply le_trans with (sz_type targ + sz_type targ' + 3).
  destruct targ'; omega.
  simpl; destruct targs; destruct targs'; omega.
Qed.

Remark sz_2_tail:
  forall targ targs targ' targs',
  sz_list_2 targs targs' <= sz_list_2 (targ::targs) (targ'::targs').
Proof.
  intros. unfold sz_list_2. simpl.
  generalize (sz_type_pos targ) (sz_type_pos targ'); intros.
  destruct targs; destruct targs'.
  simpl. omega.
  simpl (sz_typelist nil). omega.
  simpl (sz_typelist nil). omega.
  omega.
Qed.

Remark sz_2_curry_left:
  forall targs tres targ' tres',
  length targs > 1 ->
  sz_2 (curry_type targs tres) (F (targ'::nil) tres') < sz_2 (F targs tres) (F (targ'::nil) tres').
Proof.
  intros; unfold sz_2. exploit (sz_curry_type tres targs); auto. omega.
Qed.

Remark sz_2_curry_right:
  forall targ tres targs' tres',
  length targs' > 1 ->
  sz_2 (F (targ::nil) tres) (curry_type targs' tres') <
  sz_2 (F (targ::nil) tres) (F targs' tres').
Proof.
  intros; unfold sz_2.
  apply le_lt_trans with (sz_type (F (targ :: nil) tres) + sz_type (curry_type targs' tres')).
  destruct targs'; simpl in H. omegaContradiction.
  simpl curry_type. omega.
  exploit (sz_curry_type tres' targs'); auto. omega.
Qed.

Remark sz_2_curry_both:
  forall targs tres targs' tres',
  length targs > 1 -> length targs' > 1 ->
  sz_2 (curry_type targs tres) (curry_type targs' tres') <
  sz_2 (F targs tres) (F targs' tres').
Proof.
  intros; unfold sz_2.
  apply le_lt_trans with (sz_type (curry_type targs tres) + sz_type (curry_type targs' tres')).
  destruct targs'; simpl in H0. omegaContradiction.
  simpl curry_type. omega.
  exploit (sz_curry_type tres targs); auto.
  exploit (sz_curry_type tres' targs'); auto. omega.
Qed.

Algorithm for coercions

Section DO_COERCE_ARGS.

Variable do_coerce: nterm -> type -> type -> option nterm.

Fixpoint do_coerce_args (v: nat) (tl1 tl2: list type) {struct tl1} : option (list nterm) :=
  match tl1, tl2 with
  | nil, nil => Some nil
  | t1::tl1', t2::tl2' =>
     do ba <- do_coerce (NVar v) t1 t2;
     do bal <- do_coerce_args (v - 1) tl1' tl2';
     Some (ba :: bal)
  | _, _ => None
  end.

End DO_COERCE_ARGS.

Fixpoint do_coerce_rec (n: nat) (b: nterm) (t1 t2: type) {struct n}: option nterm :=
  match n with
  | O => None
  | S m =>
      if is_subtype t1 t2 then Some b else
        match t2, t1 with
        | T, F targs1 tres1 =>
            do_coerce_rec m b t1 (F (T::nil) T)
        | F targs2 tres2, F targs1 tres1 =>
            if eq_nat_dec (length targs1) (length targs2) then
             (do bl <- do_coerce_args (do_coerce_rec m) (length targs1 - 1) targs2 targs1;
              do bres <- do_coerce_rec m (NApp (NVar (length targs1)) bl) tres1 tres2;
              Some (NLet b (NFun (length targs1) bres)))
            else match targs1, targs2 with
            | nil, _ => None
            | _, nil => None
            | targ1::nil, _ =>
                do b1 <- do_coerce_rec m b (F (targ1 :: nil) tres1) (curry_type targs2 tres2);
                Some(NApp (uncurry (length targs2)) (b1 :: nil))
            | _, targ2::nil =>
                do_coerce_rec m (NApp (curry (length targs1)) (b :: nil))
                                (curry_type targs1 tres1) (F (targ2 :: nil) tres2)
            | _, _ =>
                let t1' := curry_type targs1 tres1 in
                let t2' := curry_type targs2 tres2 in
                do b1 <- do_coerce_rec m (NApp (curry (length targs1)) (b :: nil)) t1' t2';
                Some(NApp (uncurry (length targs2)) (b1 :: nil))
            end
        | _, _ => None
        end
  end.

Definition do_coerce (b: nterm) (t1 t2: type) : option nterm :=
  do_coerce_rec (S (sz_2 t1 t2)) b t1 t2.

Lemma do_coerce_rec_correct:
  forall n b t1 t2 b', do_coerce_rec n b t1 t2 = Some b' -> coerce b t1 t2 b'.
Proof.
  induction n; intros until b'; simpl.
  congruence.
  caseEq (is_subtype t1 t2); intro ISUB.
  intro EQ; inv EQ. apply coerce_sub. rewrite <- is_subtype_decision_procedure. auto.

  destruct t2 as [ | targs2 tres2].
  destruct t1; intros. inv H.
  eapply coerce_trans. eauto. apply coerce_sub. constructor.

  destruct t1 as [ | targs1 tres1].
  congruence.
  case (eq_nat_dec (length targs1) (length targs2)); intro LENGTH.

  intro EQ. monadInv EQ.
  assert (forall l1 l2 bl, do_coerce_args (do_coerce_rec n) (length l1 - 1) l2 l1 = Some bl ->
          coerce_list (list_vars (length l1)) l2 l1 bl).
  induction l1; destruct l2; simpl; intros; monadInv H.
  constructor.
  constructor. replace (length l1) with (length l1 - 0) by omega. eauto.
  apply IHl1. replace (length l1 - 1) with (length l1 - 0 - 1) by omega. auto.
  apply coerce_fun with x. auto. eapply IHn. auto.

  destruct targs1 as [ | targ1 targs1 ]. congruence.
  destruct targs1 as [ | targ1' targs1 ].

  destruct targs2 as [ | targ2 targs2 ]. congruence.
  intro EQ. monadInv EQ.
  eapply coerce_trans. eauto. change (S (length targs2)) with (length (targ2 :: targs2)).
  apply coerce_uncurry. congruence.

  destruct targs2 as [ | targ2 targs2 ]. congruence.
  destruct targs2 as [ | targ2' targs2 ].

  intro. eapply coerce_trans. apply coerce_curry. congruence. eauto.

  intro EQ. monadInv EQ. eapply coerce_trans. apply coerce_curry. congruence.
  eapply coerce_trans. eauto.
  change (S (S (length targs2))) with (length (targ2 :: targ2' :: targs2)).
  apply coerce_uncurry. congruence.
Qed.

Lemma do_coerce_correct:
  forall b t1 t2 b', do_coerce b t1 t2 = Some b' -> coerce b t1 t2 b'.
Proof.
  unfold do_coerce. intros. eapply do_coerce_rec_correct; eauto.
Qed.

Inductive can_coerce: type -> type -> Prop :=
  | can_coerce_sub: forall t1 t2,
      sd_subtype t1 t2 ->
      can_coerce t1 t2
  | can_coerce_T: forall targs tres,
      can_coerce (F targs tres) (F (T::nil) T) ->
      can_coerce (F targs tres) T
  | can_coerce_NN: forall targs1 tres1 targs2 tres2,
      can_coerce_list targs2 targs1 -> can_coerce tres1 tres2 ->
      can_coerce (F targs1 tres1) (F targs2 tres2)
  | can_coerce_N1: forall targs1 tres1 targ2 tres2,
      length targs1 > 1 ->
      can_coerce (curry_type targs1 tres1) (F (targ2::nil) tres2) ->
      can_coerce (F targs1 tres1) (F (targ2::nil) tres2)
  | can_coerce_1N: forall targ1 tres1 targs2 tres2,
      length targs2 > 1 ->
      can_coerce (F (targ1::nil) tres1) (curry_type targs2 tres2) ->
      can_coerce (F (targ1::nil) tres1) (F targs2 tres2)
  | can_coerce_NM: forall targs1 tres1 targs2 tres2,
      length targs1 > 1 -> length targs2 > 1 ->
      length targs1 <> length targs2 ->
      can_coerce (curry_type targs1 tres1) (curry_type targs2 tres2) ->
      can_coerce (F targs1 tres1) (F targs2 tres2)

with can_coerce_list: list type -> list type -> Prop :=
  | can_coerce_nil:
      can_coerce_list nil nil
  | can_coerce_cons: forall t1 tl1 t2 tl2,
      can_coerce t1 t2 -> can_coerce_list tl1 tl2 ->
      can_coerce_list (t1::tl1) (t2 :: tl2).

Remark can_coerce_list_length:
  forall tl1 tl2, can_coerce_list tl1 tl2 -> length tl1 = length tl2.
Proof. induction 1; simpl; congruence. Qed.

Scheme can_coerce_ind2 := Minimality for can_coerce Sort Prop
  with can_coerce_list_ind2 := Minimality for can_coerce_list Sort Prop.

Lemma do_coerce_rec_complete:
  forall t1 t2, can_coerce t1 t2 ->
  forall n b, sz_2 t1 t2 < n -> exists b', do_coerce_rec n b t1 t2 = Some b'.
Proof.
Opaque eq_nat_dec.
  apply (can_coerce_ind2
    (fun t1 t2 => forall n b, sz_2 t1 t2 < n -> exists b', do_coerce_rec n b t1 t2 = Some b')
    (fun t1 t2 => forall n b, sz_list_2 t1 t2 < n -> exists b', do_coerce_args (do_coerce_rec n) b t1 t2 = Some b'));
  intros.

  destruct n; [omegaContradiction|simpl].
  rewrite (is_subtype_complete _ _ H). exists b; auto.

  destruct n; [omegaContradiction|simpl].
  destruct (is_subtype (F targs tres) T). exists b; auto.
  apply H0. generalize (sz_2_T (F targs tres)). omega.

  destruct n; [omegaContradiction|simpl].
  destruct (is_subtype (F targs1 tres1) (F targs2 tres2)). exists b; auto.
  exploit can_coerce_list_length; eauto. intro.
  destruct (eq_nat_dec (length targs1) (length targs2)); try congruence.
  exploit (H0 n (length targs1 - 1)).
  generalize (sz_2_F_arglist targs1 tres1 targs2 tres2). omega.
  intros [bargs C1]. rewrite C1. simpl.
  exploit (H2 n (NApp (NVar (length targs1)) bargs)).
  generalize (sz_2_F_res targs1 tres1 targs2 tres2). omega.
  intros [bres C2]. rewrite C2. simpl. econstructor; eauto.

  destruct n; [omegaContradiction|simpl].
  destruct (is_subtype (F targs1 tres1) (F (targ2 :: nil) tres2)). econstructor; eauto.
  destruct (eq_nat_dec (length targs1) 1). omegaContradiction.
  destruct targs1; simpl in H. omegaContradiction.
  destruct targs1; simpl in H. omegaContradiction.
  apply H1. exploit (sz_2_curry_left (t :: t0 :: targs1) tres1 targ2 tres2). simpl; omega.
  omega.

  destruct n; [omegaContradiction|simpl].
  destruct (is_subtype (F (targ1 :: nil) tres1) (F targs2 tres2)). econstructor; eauto.
  destruct (eq_nat_dec 1 (length targs2)). omegaContradiction.
  destruct targs2; simpl in H. omegaContradiction.
  exploit (H1 n b).
  exploit (sz_2_curry_right targ1 tres1 (t :: targs2) tres2). auto. omega.
  intros [b' C]. rewrite C. simpl. econstructor; eauto.

  destruct n; [omegaContradiction|simpl].
  destruct (is_subtype (F targs1 tres1) (F targs2 tres2)). econstructor; eauto.
  destruct (eq_nat_dec (length targs1) (length targs2)). congruence.
  destruct targs1; simpl in H. omegaContradiction.
  destruct targs1; simpl in H. omegaContradiction.
  destruct targs2; simpl in H0. omegaContradiction.
  destruct targs2; simpl in H0. omegaContradiction.
  exploit (H3 n (NApp (curry (length (t :: t0 :: targs1))) (b :: nil))).
  exploit (sz_2_curry_both (t :: t0 :: targs1) tres1 (t1 :: t2 :: targs2) tres2); auto.
  omega.
  intros [b' C]. rewrite C. simpl. econstructor; eauto.

  simpl. econstructor; eauto.

  simpl. exploit (H0 n (NVar b)).
  generalize (sz_2_head t1 tl1 t2 tl2). omega.
  intros [b1 C1].
  exploit (H2 n (b-1)).
  generalize (sz_2_tail t1 tl1 t2 tl2). omega.
  intros [bl CL].
  exists (b1::bl). rewrite C1; simpl. rewrite CL; simpl. auto.
Qed.

Lemma can_coerce_refl:
  forall t, can_coerce t t.
Proof.
  intros. apply can_coerce_sub. apply sd_subtype_complete. constructor.
Qed.

Lemma can_coerce_subtype_mix:
  forall t1 t2, can_coerce t1 t2 ->
  (forall t3, sd_subtype t2 t3 -> can_coerce t1 t3)
/\(forall t0, sd_subtype t0 t1 -> can_coerce t0 t2).
Proof.
  apply (can_coerce_ind2
    (fun t1 t2 =>
  (forall t3, sd_subtype t2 t3 -> can_coerce t1 t3)
/\(forall t0, sd_subtype t0 t1 -> can_coerce t0 t2))
    (fun t1 t2 =>
  (forall t3, sd_subtype_list t2 t3 -> can_coerce_list t1 t3)
/\(forall t0, sd_subtype_list t0 t1 -> can_coerce_list t0 t2)));
  intros; split; intros.
  apply can_coerce_sub. eapply sd_subtype_trans; eauto.
  apply can_coerce_sub. eapply sd_subtype_trans; eauto.

  inv H1. apply can_coerce_T; auto.
  destruct H0. inversion H1; subst.
  apply can_coerce_T. eapply H2. constructor; auto.

  destruct H0; destruct H2. inv H3.
  apply can_coerce_T. eapply can_coerce_NN; eauto.
  eapply can_coerce_NN; eauto.
  destruct H0; destruct H2. inv H3.
  eapply can_coerce_NN; eauto.

  destruct H1. inv H2. apply can_coerce_T. eapply can_coerce_N1; eauto.
  apply H1. repeat constructor. auto.
  inv H6. inv H9. apply can_coerce_N1. auto. apply H1. repeat constructor; auto.
  destruct H1. inv H2.
  exploit sd_subtype_list_length; eauto. intro.
  apply can_coerce_N1. congruence. apply H3.
  apply sd_subtype_curry; auto.

  destruct H1. inv H2. simpl in H. omegaContradiction.
  exploit sd_subtype_list_length; eauto. intro.
  apply can_coerce_1N. congruence. apply H1.
  apply sd_subtype_curry; auto.
  destruct H1. inv H2. inv H7. inv H9. apply can_coerce_1N; auto.
  apply H3. repeat constructor; auto.

  destruct H3. inv H4. simpl in H0; omegaContradiction.
  exploit sd_subtype_list_length; eauto. intro.
  apply can_coerce_NM; auto; try congruence. apply H3.
  apply sd_subtype_curry; auto.
  destruct H3. inv H4.
  exploit sd_subtype_list_length; eauto. intro.
  apply can_coerce_NM; auto; try congruence.
  apply H5. apply sd_subtype_curry; auto.

  inv H. constructor.
  inv H. constructor.

  destruct H0; destruct H2. inv H3. constructor; eauto.
  destruct H0; destruct H2. inv H3. constructor; eauto.
Qed.

Lemma can_coerce_subtype_trans:
  forall t1 t2 t3,
  can_coerce t1 t2 -> sd_subtype t2 t3 -> can_coerce t1 t3.
Proof.
  intros. exploit can_coerce_subtype_mix; eauto. firstorder.
Qed.

Lemma can_subtype_coerce_trans:
  forall t0 t1 t2,
  sd_subtype t0 t1 -> can_coerce t1 t2 -> can_coerce t0 t2.
Proof.
  intros. exploit can_coerce_subtype_mix; eauto. firstorder.
Qed.

Lemma can_coerce_curry:
  forall tres tres', can_coerce tres tres' ->
  forall targs' targs, can_coerce_list targs' targs ->
  can_coerce (curry_type targs tres) (curry_type targs' tres').
Proof.
  induction 2; simpl.
  auto.
  apply can_coerce_NN; auto. constructor; auto. constructor.
Qed.

Lemma sd_subtype_list_can_coerce_list:
  forall tl1 tl2,
  sd_subtype_list tl1 tl2 -> can_coerce_list tl1 tl2.
Proof.
  induction 1. constructor. constructor; auto. apply can_coerce_sub; auto.
Qed.

Lemma can_coerce_curry_inv:
  forall tres tres' targs targs',
  length targs = length targs' ->
  can_coerce (curry_type targs tres) (curry_type targs' tres') ->
  can_coerce_list targs' targs /\ can_coerce tres tres'.
Proof.
  induction targs; intros; destruct targs'; simpl in *; try discriminate.
  split. constructor. auto.
  inv H0.
  exploit (sd_subtype_curry_inv tres tres' (a::targs) (t::targs')). auto. auto.
  intros [A B]. split. apply sd_subtype_list_can_coerce_list; auto.
  apply can_coerce_sub; auto.
  inv H4. inv H7. exploit IHtargs. 2: eauto. congruence. intros [A B].
  split; auto. constructor; auto.
  simpl in H4. omegaContradiction.
  simpl in H4. omegaContradiction.
  simpl in H5. omegaContradiction.
Qed.

Lemma can_coerce_NM':
  forall targs tres targs' tres',
  length targs > 1 -> length targs' > 1 ->
  can_coerce (curry_type targs tres) (curry_type targs' tres') ->
  can_coerce (F targs tres) (F targs' tres').
Proof.
  intros. destruct (eq_nat_dec (length targs) (length targs')).
  exploit can_coerce_curry_inv; eauto. intros [A B].
  apply can_coerce_NN; auto.
  apply can_coerce_NM; auto.
Qed.

Lemma can_coerce_trans:
  forall t1 t2 t3, can_coerce t1 t2 -> can_coerce t2 t3 -> can_coerce t1 t3.
Proof.
  assert (forall N,
    (forall t1 t2 t3,
     sz_2 t1 t2 + sz_2 t2 t3 < N ->
     can_coerce t1 t2 -> can_coerce t2 t3 -> can_coerce t1 t3)
 /\ (forall t1 t2 t3,
     S (sz_list_2 t1 t2 + sz_list_2 t2 t3) < N ->
     can_coerce_list t1 t2 -> can_coerce_list t2 t3 -> can_coerce_list t1 t3)).
  induction N; split; intros.
  omegaContradiction. omegaContradiction.
  destruct IHN as [IHN1 IHN2].
  generalize (can_coerce_subtype_trans t1 t2 t3 H0); intro TRSUB.
  inversion H0; subst.

  eapply can_subtype_coerce_trans; eauto.

  inv H1. inv H3. auto.

  inversion H1; subst; auto.

  apply can_coerce_T. eapply IHN1; eauto.
  generalize (sz_2_T (F targs2 tres2)). omega.

  apply can_coerce_NN.
  eapply IHN2; eauto.
  generalize (sz_2_F_arglist targs1 tres1 targs2 tres2).
  generalize (sz_2_F_arglist targs2 tres2 targs3 tres3). omega.
  eapply IHN1; eauto.
  generalize (sz_2_F_res targs1 tres1 targs2 tres2).
  generalize (sz_2_F_res targs2 tres2 targs3 tres3). omega.

  assert (length targs1 > 1). exploit can_coerce_list_length; eauto. congruence.
  apply can_coerce_N1. auto.
  apply IHN1 with (t2 := curry_type targs2 tres2); auto.
  exploit (sz_2_curry_both targs1 tres1 targs2 tres2); auto.
  exploit (sz_2_curry_left targs2 tres2 targ2 tres3); auto. omega.
  apply can_coerce_curry; auto.

  inv H2. inv H10.
  apply can_coerce_1N. auto.
  apply IHN1 with (t2 := F (targ1 :: nil) tres2); auto.
  exploit (sz_2_curry_right targ1 tres2 targs0 tres3); auto. omega.

  exploit can_coerce_list_length; eauto. intro LEN.
  apply can_coerce_NM. congruence. auto. congruence.
  apply IHN1 with (t2 := curry_type targs2 tres2); auto.
  exploit (sz_2_curry_both targs1 tres1 targs2 tres2); auto. congruence.
  exploit (sz_2_curry_both targs2 tres2 targs3 tres3); auto. omega.
  apply can_coerce_curry; auto.

  inversion H1; subst; auto.

  apply can_coerce_T. apply IHN1 with (t2 := F (targ2::nil) tres2); auto.
  generalize (sz_2_T (F (targ2::nil) tres2)). omega.

  inv H6. inv H10.
  apply can_coerce_N1. auto. apply IHN1 with (t2 := F (targ2::nil) tres2); auto.
  exploit (sz_2_curry_left targs1 tres1 targ2 tres2); auto. omega.

  simpl in H6. omegaContradiction.

  apply can_coerce_NM'; auto.
  apply IHN1 with (t2 := (F (targ2 :: nil) tres2)); auto.
  exploit (sz_2_curry_left targs1 tres1 targ2 tres2); auto.
  exploit (sz_2_curry_right targ2 tres2 targs2 tres3); auto.
  omega.

  simpl in H6. omegaContradiction.


  inversion H1; subst. auto.

  apply can_coerce_T. apply IHN1 with (t2 := F targs2 tres2); auto.
  generalize (sz_2_T (F targs2 tres2)). omega.

  exploit can_coerce_list_length; eauto. intro LEN.
  apply can_coerce_1N. congruence.
  apply IHN1 with (t2 := curry_type targs2 tres2); auto.
  exploit (sz_2_curry_right targ1 tres1 targs2 tres2); auto.
  exploit (sz_2_curry_both targs2 tres2 targs0 tres3); auto. congruence.
  omega.
  apply can_coerce_curry; auto.

  apply IHN1 with (t2 := curry_type targs2 tres2); auto.
  exploit (sz_2_curry_right targ1 tres1 targs2 tres2); auto.
  exploit (sz_2_curry_left targs2 tres2 targ2 tres3); auto.
  omega.

  simpl in H2. omegaContradiction.

  apply can_coerce_1N. auto.
  apply IHN1 with (t2 := curry_type targs2 tres2); auto.
  exploit (sz_2_curry_right targ1 tres1 targs2 tres2); auto.
  exploit (sz_2_curry_both targs2 tres2 targs0 tres3); auto.
  omega.


  inversion H1; subst. auto.

  apply can_coerce_T. apply IHN1 with (t2 := F targs2 tres2); auto.
  generalize (sz_2_T (F targs2 tres2)). omega.

  exploit can_coerce_list_length; eauto. intro LEN.
  apply can_coerce_NM. auto. congruence. congruence.
  apply IHN1 with (t2 := curry_type targs2 tres2); auto.
  exploit (sz_2_curry_both targs1 tres1 targs2 tres2); auto.
  exploit (sz_2_curry_both targs2 tres2 targs3 tres3); auto. congruence.
  omega.
  apply can_coerce_curry; auto.

  apply can_coerce_N1. auto.
  apply IHN1 with (t2 := curry_type targs2 tres2); auto.
  exploit (sz_2_curry_both targs1 tres1 targs2 tres2); auto.
  exploit (sz_2_curry_left targs2 tres2 targ2 tres3); auto.
  omega.

  simpl in H3. omegaContradiction.

  apply can_coerce_NM'; auto.
  apply IHN1 with (t2 := curry_type targs2 tres2); auto.
  exploit (sz_2_curry_both targs1 tres1 targs2 tres2); auto.
  exploit (sz_2_curry_both targs2 tres2 targs3 tres3); auto.
  omega.


  destruct IHN as [IHN1 IHN2].
  generalize t1 t2 H0 t3 H1 H.
  induction 1; intros. inv H2. constructor.
  inv H4. constructor.
  apply IHN1 with (t2 := t4); auto.
  generalize (sz_2_head t0 tl1 t4 tl2).
  generalize (sz_2_head t4 tl2 t7 tl3).
  omega.
  apply IHcan_coerce_list. auto.
  generalize (sz_2_tail t0 tl1 t4 tl2).
  generalize (sz_2_tail t4 tl2 t7 tl3).
  omega.

  intros.
  destruct (H (S (sz_2 t1 t2 + sz_2 t2 t3))).
  apply H2 with t2; auto.
Qed.

Lemma coerce_can_coerce:
  forall b t1 t2 b', coerce b t1 t2 b' -> can_coerce t1 t2.
Proof.
  apply (coerce_ind2
    (fun b t1 t2 b' => can_coerce t1 t2)
    (fun b t1 t2 b' => can_coerce_list t1 t2));
  intros.
  apply can_coerce_sub. apply sd_subtype_complete. auto.

  destruct targs. congruence.
  destruct targs. simpl. apply can_coerce_refl.
  simpl. apply can_coerce_N1. simpl; omega. apply can_coerce_refl.

  destruct targs. congruence.
  destruct targs. simpl. apply can_coerce_refl.
  simpl. apply can_coerce_1N. simpl; omega. apply can_coerce_refl.

  apply can_coerce_NN; auto.

  eapply can_coerce_trans; eauto.

  constructor.

  constructor; auto.
Qed.

Lemma do_coerce_complete:
  forall b t1 t2 b', coerce b t1 t2 b' ->
  forall b1, exists b1', do_coerce b1 t1 t2 = Some b1'.
Proof.
  intros. unfold do_coerce. apply do_coerce_rec_complete.
  eapply coerce_can_coerce; eauto.
  omega.
Qed.

Some tests

Definition F1 (arg res: type) := F (arg::nil) res.

Eval vm_compute in (do_coerce (NVar 0) (F1 T T) T).
Eval vm_compute in (do_coerce (NVar 0) (F1 T (F1 T T)) T).
Eval vm_compute in (do_coerce (NVar 0) (F (T::T::nil) T) (F1 T (F1 T T))).
Eval vm_compute in (do_coerce (NVar 0) (F1 T (F1 T T)) (F (T::T::nil) T)).
Eval vm_compute in (do_coerce (NVar 0)
                       (F (T::T::T::nil) T)
                       (F1 T (F (T::T::nil) T))).
Eval vm_compute in (do_coerce (NVar 0)
                       (F (T::T::T::nil) T)
                       (F (T::T::nil) (F1 T T))).
Eval vm_compute in (do_coerce (NVar 0)
                       (F1 T T)
                       (F1 (F (T::T::nil) T) T)).

Type checking and production of uncurried term


Inductive aterm: Set :=
  | AVar: nat -> aterm
  | AConst: const -> aterm
  | AFun: type -> list type -> aterm -> aterm
  | AApp: aterm -> aterm -> aterm
  | ALet: aterm -> aterm -> aterm
  | ALetrec: type -> list type -> type -> aterm -> aterm -> aterm
  | ACoerce: aterm -> type -> aterm.

Fixpoint erasure (a: aterm) : uterm :=
  match a with
  | AVar n => UVar n
  | AConst c => UConst c
  | AFun ty tyl a1 => UFun_n (S (length tyl)) (erasure a1)
  | AApp a1 a2 => UApp (erasure a1) (erasure a2)
  | ALet a1 a2 => ULet (erasure a1) (erasure a2)
  | ALetrec ty tyl tyres a1 a2 => ULetrec (UFun_n (length tyl) (erasure a1)) (erasure a2)
  | ACoerce a1 ty => erasure a1
  end.

Definition types_of (args: list (type * nterm)) :=
  List.map (@fst type nterm) args.
Definition nterms_of (args: list (type * nterm)) :=
  List.map (@snd type nterm) args.

Section MATCH_APP.

Variable build_app: type * nterm -> list (type * nterm) -> option (type * nterm).
Variable tres: type.
Variable b: nterm.

Fixpoint match_app (tl: list type) (args: list (type * nterm))
                   (bargs: list nterm)
                   {struct args}: option (type * nterm) :=
  match tl, args with
  | nil, _ =>
      build_app (tres, NApp b (rev bargs)) args
  | t2' :: tl', nil =>
      None
  | t2' :: tl', (t2, b2) :: args' =>
      if eq_type t2 t2'
      then match_app tl' args' (b2 :: bargs)
      else None
  end.

Remark match_app_inv:
  forall t' b' args tl bargs,
  match_app tl args bargs = Some (t', b') ->
  exists args1, exists args2,
  args = args1 ++ args2 /\
  types_of args1 = tl /\
  build_app (tres, NApp b (rev bargs ++ nterms_of args1))
            args2 = Some (t', b').
Proof.
  unfold types_of, nterms_of.
  induction args; intros until bargs; simpl.
  destruct tl; try congruence.
  intros. exists (@nil (type * nterm)); exists (@nil (type * nterm)).
  split. auto. split. auto. simpl. rewrite <- app_nil_end. auto.

  destruct tl. intro.
  exists (@nil (type * nterm)); exists (a :: args).
  split. auto. split. auto. simpl. rewrite <- app_nil_end. auto.
  destruct a as [t2 b2]. destruct (eq_type t2 t); try congruence.
  intro. subst t. exploit IHargs; eauto.
  intros [args1 [args2 [A [B C]]]].
  exists ((t2, b2) :: args1); exists args2.
  split. simpl. congruence.
  split. simpl. congruence.
  simpl. simpl in C. rewrite app_ass in C. simpl in C. auto.
Qed.

End MATCH_APP.

Fixpoint build_app (tb: type * nterm) (args: list (type * nterm))
                   {struct args}: option (type * nterm) :=
  match args with
  | nil => Some tb
  | (t1, b1) :: args' =>
      match tb with
      | (T, b) =>
          if eq_type t1 T
          then build_app (T, NApp b (b1::nil)) args'
          else None
      | (F nil tres, b) =>
          None
      | (F (t1'::tl') tres, b) =>
          if eq_type t1 t1'
          then match_app build_app tres b tl' args' (b1::nil)
          else None
      end
  end.

Lemma transl_list_split:
  forall te args2 args1 al,
  transl_list te al (types_of (args1 ++ args2)) (nterms_of (args1 ++ args2)) ->
  exists al1, exists al2,
  al = al1 ++ al2 /\
  transl_list te al1 (types_of args1) (nterms_of args1) /\
  transl_list te al2 (types_of args2) (nterms_of args2).
Proof.
  unfold types_of, nterms_of; induction args1; simpl; intros.
  exists (@nil uterm); exists al.
  split. auto. split. constructor. auto.
  inv H. exploit IHargs1; eauto. intros [al1 [al2 [A [B C]]]]. subst al0.
  exists (a1 :: al1); exists al2.
  split. auto. split. constructor; auto. auto.
Qed.

Lemma build_app_correct:
  forall te args a t b al t' b',
  transl te a t b ->
  transl_list te al (types_of args) (nterms_of args) ->
  build_app (t, b) args = Some (t', b') ->
  transl te (UApp_n a al) t' b'.
Proof.
  intro te.
  assert (forall n args a t b al t' b',
    length args < n ->
    transl te a t b ->
    transl_list te al (map (@fst type nterm) args) (map (@snd type nterm) args) ->
    build_app (t, b) args = Some (t', b') ->
    transl te (UApp_n a al) t' b').
  induction n; intros until b'; intros LEN TR TRL. omegaContradiction.
  destruct args as [ | [t1 b1] args]; simpl.
  intros. inv H. simpl in TRL. inv TRL. simpl; auto.
  simpl in TRL. inv TRL. destruct t.

  destruct (eq_type t1 T); try congruence. intros.
  subst t1. simpl.
  eapply IHn with (args := args) (a := UApp a a1); eauto.
  simpl in LEN. omega.
  apply transl_appT; auto.

  destruct l as [ | t1' tl']. congruence.
  destruct (eq_type t1 t1'); try congruence. subst t1'.
  intro.
  exploit match_app_inv; eauto.
  intros [args1 [args2 [A [B C]]]]. subst args.
  exploit transl_list_split. unfold types_of, nterms_of; eauto.
  intros [al1 [al2 [D [E F]]]]. subst al0.
  change (a1 :: al1 ++ al2) with ((a1 :: al1) ++ al2).
  rewrite UApp_n_app.
  eapply IHn with (args := args2); eauto.
  simpl in LEN. rewrite app_length in LEN. omega.
  apply transl_app with (t1 :: tl'). congruence. auto.
  simpl. constructor; auto. congruence.

  intros. eapply H with (n := S (length args)); eauto.
Qed.

Fixpoint aterm_size (a: aterm) : nat :=
  match a with
  | AVar v => 0
  | AConst c => 0
  | AFun ty1 tyl a => aterm_size a + 1
  | AApp a1 a2 => aterm_size a1 + aterm_size a2 + 1
  | ALet a1 a2 => aterm_size a1 + aterm_size a2 + 1
  | ALetrec ty1 tyl tyres a1 a2 => aterm_size a1 + aterm_size a2 + 1
  | ACoerce a ty => aterm_size a + 1
  end.

Section DO_TRANSL_ARGS.

Variable do_transl: typenv -> aterm -> option (type * nterm).
Variable te: typenv.

Fixpoint do_transl_args (a: aterm) (args: list (type * nterm))
                        {struct a}: option (type * nterm) :=
  match a with
  | AApp a1 a2 =>
      do tb2 <- do_transl te a2; do_transl_args a1 (tb2 :: args)
  | _ =>
      do tb <- do_transl te a; build_app tb args
  end.

Lemma do_transl_args_correct:
  forall t b a args al,
  (forall a' ty b,
   aterm_size a' <= aterm_size a ->
   do_transl te a' = Some (ty, b) -> transl te (erasure a') ty b) ->
  do_transl_args a args = Some (t, b) ->
  transl_list te al (types_of args) (nterms_of args) ->
  transl te (UApp_n (erasure a) al) t b.
Proof.

  assert (BASE:
    forall t b a args al,
    (forall a' ty b,
     aterm_size a' <= aterm_size a ->
     do_transl te a' = Some (ty, b) -> transl te (erasure a') ty b) ->
    (do tb <- do_transl te a; build_app tb args) = Some (t, b) ->
    transl_list te al (types_of args) (nterms_of args) ->
    transl te (UApp_n (erasure a) al) t b).
  intros. monadInv H0. destruct x as [t' b'].
  eapply build_app_correct; eauto.

  induction a; simpl do_transl_args; intros; eauto.
  monadInv H0. destruct x as [t2 b2]. simpl.
  change (UApp_n (UApp (erasure a1) (erasure a2)) al)
    with (UApp_n (erasure a1) (erasure a2 :: al)).
  eapply IHa1; eauto. intros. apply H; auto. simpl; omega.
  simpl. constructor; auto. apply H; auto. simpl; omega.
Qed.

End DO_TRANSL_ARGS.

Fixpoint do_transl (te: typenv) (a: aterm) {struct a}: option (type * nterm) :=
  match a with
  | AVar n =>
      do ty <- nth_error te n;
      Some (ty, NVar n)
  | AConst c =>
      Some (T, NConst c)
  | AFun ty1 tyl a1 =>
      do (ty, b1) <- do_transl (rev (ty1::tyl) ++ te) a1;
      Some (F (ty1::tyl) ty, NFun (S (length tyl)) b1)
  | AApp a1 a2 =>
      do tb2 <- do_transl te a2; do_transl_args do_transl te a1 (tb2::nil)
  | ALet a1 a2 =>
      do (ty1, b1) <- do_transl te a1;
      do (ty2, b2) <- do_transl (ty1 :: te) a2;
      Some(ty2, NLet b1 b2)
  | ALetrec targ1 targs tres a1 a2 =>
      do (ty1, b1) <- do_transl (rev (targ1::targs) ++ F (targ1::targs) tres :: te) a1;
      do (ty2, b2) <- do_transl (F (targ1::targs) tres :: te) a2;
      if eq_type ty1 tres
      then Some(ty2, NLetrec (S (length targs)) b1 b2)
      else None
  | ACoerce a1 ty =>
      do (ty1, b1) <- do_transl te a1;
      do b2 <- do_coerce b1 ty1 ty;
      Some(ty, b2)
  end.

Theorem do_transl_correct:
  forall a te ty b,
  do_transl te a = Some (ty, b) -> transl te (erasure a) ty b.
Proof.
  assert (forall n a te ty b,
    aterm_size a < n ->
    do_transl te a = Some (ty, b) -> transl te (erasure a) ty b).
  induction n.
  intros. omegaContradiction.
  intros until b. destruct a; simpl; intros SZ TR; try (monadInv TR).

  constructor; auto.

  constructor.

  change (UFun (UFun_n (length l) (erasure a))) with (UFun_n (length (t :: l)) (erasure a)).
  change (S (length l)) with (length (t :: l)).
  constructor. congruence. apply IHn. omega. auto.

  destruct x as [tx bx].
  change (UApp (erasure a1) (erasure a2))
    with (UApp_n (erasure a1) (erasure a2 :: nil)).
  eapply do_transl_args_correct with (args := (tx,bx) :: nil); eauto.
  intros. apply IHn; auto. omega.
  simpl. constructor. apply IHn; auto. omega. constructor.

  eapply transl_let. apply IHn; eauto. omega. apply IHn; auto. omega.

  destruct (eq_type x t0); monadInv EQ2.
  econstructor.
  apply IHn. omega. simpl. eexact EQ.
  apply IHn. omega. auto.

  eapply transl_coerce.
  apply IHn; eauto. omega.
  eapply do_coerce_correct; eauto.

  intros. apply H with (n := S (aterm_size a)); auto.
Qed.

Fixpoint AApp_n (a: aterm) (bl: list aterm) {struct bl} : aterm :=
  match bl with
  | nil => a
  | b :: bs => AApp_n (AApp a b) bs
  end.

Remark erasure_AApp_n:
  forall Al A,
  erasure (AApp_n A Al) = UApp_n (erasure A) (map erasure Al).
Proof.
  induction Al; intro; simpl.
  auto.
  change (UApp (erasure A) (erasure a)) with (erasure (AApp A a)).
  apply IHAl.
Qed.

Remark AApp_n_app:
  forall Al1 Al2 A,
  AApp_n A (Al1 ++ Al2) = AApp_n (AApp_n A Al1) Al2.
Proof.
  induction Al1; intros; simpl. auto.
  rewrite IHAl1. auto.
Qed.

Remark match_app_complete:
  forall tres b targs bl bargs,
  length bl = length targs ->
  match_app build_app tres b targs (combine targs bl) bargs =
  Some (tres, NApp b (rev bargs ++ bl)).
Proof.
  induction targs; intros; simpl.
  destruct bl; simpl in H; try congruence. rewrite <- app_nil_end. auto.
  destruct bl; simpl in H; try congruence.
  simpl. rewrite dec_eq_true. rewrite IHtargs.
  simpl. rewrite app_ass. auto. congruence.
Qed.

Remark build_app_complete:
  forall tres targs b bl,
  targs <> nil -> length bl = length targs ->
  build_app (F targs tres, b) (List.combine targs bl) =
  Some (tres, NApp b bl).
Proof.
  intros. destruct targs. congruence. destruct bl; simpl in H0; try congruence.
  simpl. rewrite dec_eq_true. rewrite match_app_complete.
  simpl. auto. congruence.
Qed.

Remark do_transl_args_AApp_n:
  forall te Al targs bl,
  list_forall3
    (fun A ty b => do_transl te A = Some(ty, b))
    Al targs bl ->
  forall A tbl,
  do_transl_args do_transl te (AApp_n A Al) tbl =
  do_transl_args do_transl te A (List.combine targs bl ++ tbl).
Proof.
  induction 1; intros.
  simpl. auto.
  simpl. rewrite IHlist_forall3. simpl. rewrite H. simpl. auto.
Qed.

Theorem do_transl_complete:
  forall te a ty b,
  transl te a ty b ->
  exists A, exists b',
  a = erasure A /\ do_transl te A = Some(ty, b').
Proof.
  apply (transl_ind2
    (fun te a ty b =>
       exists A, exists b',
       a = erasure A /\ do_transl te A = Some(ty, b'))
    (fun te al tyl bl =>
       exists Al, exists bl',
       al = map erasure Al /\
       list_forall3
         (fun A ty b' => do_transl te A = Some(ty, b'))
         Al tyl bl'));
  intros.

  exists (AVar n); exists (NVar n); split.
  auto. simpl. rewrite H. simpl. auto.

  exists (AConst c); exists (NConst c); auto.

  destruct targs as [ | targ1 targs]. congruence.
  destruct H1 as [A [b' [P Q]]].
  exists (AFun targ1 targs A); econstructor; split.
  simpl. congruence.
  simpl. simpl in Q. rewrite Q. simpl. reflexivity.

  destruct H0 as [A1 [b1' [P1 Q1]]].
  destruct H2 as [A2 [b2' [P2 Q2]]].
  exists (AApp (ACoerce A1 T) A2); econstructor; split.
  subst a1 a2; auto.
  simpl. rewrite Q1. rewrite Q2. simpl. reflexivity.

  destruct H1 as [A1 [b1' [P1 Q1]]].
  destruct H3 as [Al [bl' [Pl Ql]]].
  exists (AApp_n (ACoerce A1 (F targs tres)) Al);
  exists (NApp b1' bl'); split.
  rewrite erasure_AApp_n. simpl. congruence.
  destruct (List.exists_last H) as [targs1 [targN EQ]].
  rewrite EQ in Ql. exploit list_forall3_app; eauto.
  intros [Al1 [Al2 [bl1' [bl2' [U [V [W X]]]]]]].
  inv X. inv H7. clear H2. clear Ql.
  rewrite AApp_n_app. simpl. rewrite H5. simpl.
  rewrite (do_transl_args_AApp_n te Al1 targs1 bl1'); auto.
  simpl. rewrite Q1. simpl.
  replace (do_coerce b1' (F (targs1 ++ targN :: nil) tres)
                         (F (targs1 ++ targN :: nil) tres))
  with (Some b1').
  simpl.
  assert (length bl1' = length targs1).
  exploit list_forall3_length2; eauto.
  exploit list_forall3_length3; eauto. congruence.
  replace (combine targs1 bl1' ++ (targN, c1) :: nil)
     with (combine (targs1 ++ targN :: nil) (bl1' ++ c1 :: nil)).
  rewrite build_app_complete. auto.
  destruct targs1; simpl; congruence.
  repeat rewrite app_length. simpl. omega.
  rewrite combine_app; auto.
  unfold do_coerce. simpl.
  rewrite (is_subtype_complete
            (F (targs1 ++ targN :: nil) tres)
            (F (targs1 ++ targN :: nil) tres)).
  auto. apply sd_subtype_refl.

  destruct H0 as [A1 [b1' [P1 Q1]]].
  destruct H2 as [A2 [b2' [P2 Q2]]].
  exists (ALet A1 A2); exists (NLet b1' b2'); split.
  simpl; congruence.
  simpl. rewrite Q1; simpl. rewrite Q2; simpl. auto.

  destruct H0 as [A1 [b1' [P1 Q1]]].
  destruct H2 as [A2 [b2' [P2 Q2]]].
  exists (ALetrec targ1 targs tres A1 A2); econstructor; split.
  simpl. congruence.
  simpl. simpl in Q1. rewrite Q1. simpl. rewrite Q2. simpl.
  rewrite dec_eq_true. reflexivity.

  destruct H0 as [A1 [b1' [P1 Q1]]].
  exploit do_coerce_complete; eauto. instantiate (1 := b1'). intros [b2 P2].
  exists (ACoerce A1 t'); exists b2; split.
  simpl. auto.
  simpl. rewrite Q1; simpl. rewrite P2; simpl. auto.


  exists (@nil aterm); exists (@nil nterm); split. auto. constructor.

  destruct H0 as [A1 [b1' [P1 Q1]]].
  destruct H2 as [A2 [b2' [P2 Q2]]].
  exists (A1 :: A2); exists (b1' :: b2'); split.
  simpl. congruence.
  constructor; auto.
Qed.