Library TranslValid
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.
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.
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)).
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.