Library typesystemequiv
Require Import List.
Require Import Omega.
Require Import list.
Require Import mxx.
Require Import typesystem.
Require Import Ltypesystem.
Lemma jerasable_down : ∀ M H Z t e,
jerasable 2 H Z t e → jerasable M H Z t e.
Proof. intros M H Z t e HZte; jerasable_induction HZte; eauto. Qed.
Lemma jerasable_bind_down : ∀ M H Z dH dZ,
jerasable_bind 2 H Z dH dZ → jerasable_bind M H Z dH dZ.
Proof.
intros M H Z dH dZ [? [? [? [? ?]]]].
∃ x; repeat split; auto; apply jerasable_down; auto.
Qed.
Lemma jerasable_env_down : ∀ M H Z,
jerasable_env 2 H Z → jerasable_env M H Z.
Proof.
intros M H Z HZ.
induction HZ; [apply JEnil|eapply JEcons]; eauto.
apply jerasable_bind_down; auto.
Qed.
Lemma jterm_env_down : ∀ M H Z G,
jterm_env 2 H Z G → jterm_env M H Z G.
Proof.
intros M H Z G [? ?].
split.
intros m; apply jerasable_env_down; auto.
eapply Forall_impl; [|apply H1].
unfold jtype; intros.
apply jerasable_down; auto.
Qed.
Lemma jterm_down : ∀ M H Z G a t,
jterm 2 H Z G a t → jterm M H Z G a t.
Proof.
intros M H Z G a t HZGat; jterm_induction HZGat; eauto; unfold jtype, jcoer in *;
repeat (match goal with
| |- _ ≤ M → _ ⇒ intros m
| |- jterm_env M _ _ _ ⇒ apply jterm_env_down
| |- jerasable M _ _ _ _ ⇒ apply jerasable_down
end; auto).
intros m; apply jerasable_down; auto.
Qed.
Lemma jerasable_up_2 : ∀ H Z t e,
jerasable 1 H Z t e → jerasable 2 H Z t e.
Proof.
intros H Z t e HZte; jerasable_induction HZte; eauto;
repeat (match goal with
| H1 : 2 ≤ 1 → _ |- _ ⇒ clear H1
| |- 2 ≤ 2 → _ ⇒ intros _
| |- 2 ≠ 1 → _ ⇒ intros _
| H1 : jerasable 2 ?H ?Z (Spair ?dH ?t ?s) (Scoer _ _ ?dH ?dZ)
|- jerasable 2 (?dH + ?H) (?dZ ++ dmap (lift ?dH 0) ?Z) ?t Stype
⇒ apply (jcoer_extract_left_type M12 H1)
| H1 : jerasable 2 ?H ?Z (Spair ?dH ?t ?s) (Scoer _ _ ?dH ?dZ)
|- jerasable 2 ?H ?Z ?s Stype
⇒ apply (jcoer_extract_right_type M12 H1)
| H1 : jerasable 2 ?H ?Z (Mu ?t) Stype
|- jerasable 2 (1 + ?H) (dmap (lift 1 0) ?Z) ?t Stype
⇒ inversion H1; assumption
end; auto); pose proof (H1 M11) as Hmu; inversion Hmu; assumption.
Qed.
Lemma jerasable_bind_up_2 : ∀ H Z dH dZ,
jerasable_bind 1 H Z dH dZ → jerasable_bind 2 H Z dH dZ.
Proof.
intros H Z dH dZ [? [? [? [? ?]]]].
∃ x; repeat split; auto; apply jerasable_up_2; auto.
Qed.
Lemma jerasable_env_up_2 : ∀ H Z,
jerasable_env 1 H Z → jerasable_env 2 H Z.
Proof.
intros H Z HZ.
induction HZ; [apply JEnil|eapply JEcons]; eauto.
apply jerasable_bind_up_2; auto.
Qed.
Lemma jterm_env_up_2 : ∀ H Z G,
jterm_env 1 H Z G → jterm_env 2 H Z G.
Proof.
intros H Z G [? ?].
split.
intros.
apply jerasable_env_up_2; auto.
eapply Forall_impl; [|apply H1].
unfold jtype; intros.
apply jerasable_up_2; auto.
Qed.
Lemma jterm_up_2 : ∀ H Z G a t,
jterm 1 H Z G a t → jterm 2 H Z G a t.
Proof.
intros H Z G a t HZGat; jterm_induction HZGat; eauto; unfold jtype, jcoer in *;
repeat (match goal with
| |- _ ≤ _ → _ ⇒ intros _
| |- jterm_env 2 _ _ _ ⇒ apply jterm_env_up_2
| |- jerasable 2 _ _ _ _ ⇒ apply jerasable_up_2
end; auto).
intros _.
pose proof (jterm_extract_jterm_env M12 IHHZGat) as [_ ?].
inversion H1; auto.
Qed.
Lemma jerasable_list_app : ∀ M e e' H Z x2s x1s,
jerasable M H Z (inject (Slist e') x1s) (Slist e) →
jerasable M H Z (inject (Slist e') x2s) (Slist e) →
jerasable M H Z (inject (Slist e') (x1s ++ x2s)) (Slist e).
Proof.
induction x1s; simpl; intros; auto.
inversion H0; subst.
constructor; auto.
Qed.
Ltac from_slift :=
match goal with
| |- context[slift Slisttype ?d ?i ?vecs] ⇒
replace (slift Slisttype d i vecs) with (map (lift d i) vecs) by reflexivity
| |- context[slift Slistcoer ?d ?i ?Z] ⇒
replace (slift Slistcoer d i Z) with (dmap (lift d i) Z) by reflexivity
| |- context[slift Slistprodtype ?d ?i ?Z] ⇒
replace (slift Slistprodtype d i Z) with (dmap (lift d i) Z) by reflexivity
end.
Ltac to_slift s :=
match goal with
| |- context[dmap (lift ?d ?i) ?Z] ⇒
replace (dmap (lift d i) Z) with (slift s d i Z) by reflexivity
| |- context[map (lift ?d ?i) ?vecs] ⇒
replace (map (lift d i) vecs) with (slift Slisttype d i vecs) by reflexivity
end.
Lemma jerasable_bind_only_type : ∀ M H Z dH, jerasable_bind M H Z dH nil.
Proof.
intros; induction dH.
∃ nil.
repeat split; simpl; constructor.
destruct IHdH as [xs [? [? [? ?]]]].
∃ (Top :: xs).
repeat split; simpl; repeat constructor; auto.
Qed.
Ltac trysimpl := repeat
match goal with
| |- context[0 + ?x] ⇒ replace (0 + x) with x by reflexivity
| H : context[0 + ?x] |- _ ⇒ replace (0 + x) with x in H by reflexivity
| |- context[nil ++ ?xs] ⇒ replace (nil ++ xs) with xs by reflexivity
| H : context[nil ++ ?xs] |- _ ⇒ replace (nil ++ xs) with xs in H by reflexivity
| |- context[_ + 0] ⇒ rewrite <- plus_n_O
| H : context[_ + 0] |- _ ⇒ rewrite <- plus_n_O in H
| |- context[_ ++ nil] ⇒ rewrite app_nil_r
| H : context[_ ++ nil] |- _ ⇒ rewrite app_nil_r in H
| |- context[dmap (lift 0 _) _] ⇒ rewrite dmap_lift_0
| H : context[dmap (lift 0 _) _] |- _ ⇒ rewrite dmap_lift_0 in H
| |- context[dmap ?f nil] ⇒ replace (dmap f nil) with (@nil (type × type)) by reflexivity
| H : context[dmap ?f nil] |- _ ⇒
replace (dmap f nil) with (@nil (type × type)) in H by reflexivity
| |- context[_ + (_ + _)] ⇒ rewrite plus_assoc
| H : context[_ + (_ + _)] |- _ ⇒ rewrite plus_assoc in H
| |- context[dmap _ (_ ++ _)] ⇒ rewrite <- dmap_app
| H : context[dmap _ (_ ++ _)] |- _ ⇒ rewrite <- dmap_app in H
| |- context[_ ++ _ ++ _] ⇒ rewrite app_assoc
| H : context[_ ++ _ ++ _] |- _ ⇒ rewrite app_assoc in H
| |- context[dmap (lift (_ + _) ?i) _] ⇒ rewrite dmap_lift_plus
| H : context[dmap (lift (_ + _) ?i) _] |- _ ⇒ rewrite dmap_lift_plus in H
| |- context[length (_ ++ _)] ⇒ rewrite app_length
| H : context[length (_ ++ _)] |- _ ⇒ rewrite app_length in H
end.
Lemma jerasable_bind_lift : ∀ {M H Z dH dZ dH0},
jerasable_bind M H Z dH dZ →
jerasable_bind M H Z (dH0 + dH) (dmap (lift dH0 0) dZ).
Proof.
intros.
destruct H0 as [? [? [? [? ?]]]].
destruct (replicate _ Top dH0) as [? [? ?]].
∃ (map (subst x 0) x0 ++ x).
repeat split; trysimpl; tryomega.
repeat to_slift (Slist Sprodtype); rewrite <- lift_inject; from_slift.
rewrite <- plus_assoc.
apply jerasable_lift_0 with Slistprodtype; auto.
apply jerasable_list_app; auto.
clear H2 H3 H1 dZ.
induction x0; simpl; [apply JSNil|apply JSCons].
pose proof (H5 0); simpl in H0; subst; simpl; apply JTTop.
apply IHx0; intros i.
pose proof (H5 (1 + i)); simpl in H0; auto.
rewrite subst_app.
repeat to_slift (Slist Sprodtype); rewrite <- lift_inject.
rewrite subst_lift; auto.
replace (length x0 - length x0) with 0 by omega.
rewrite lift_0; auto.
Qed.
Lemma jerasable_env_lift : ∀ {M H Z} dH,
jerasable_env M H Z →
jerasable_env M (dH + H) (dmap (lift dH 0) Z).
Proof.
induction 1; simpl.
apply JEcons with 0 nil (dH + 0) nil; simpl; auto; [apply JEnil|].
apply jerasable_bind_only_type.
subst; trysimpl.
apply JEcons with H Z (dH + dH0) (dmap (lift dH 0) dZ); tryomega.
apply jerasable_bind_lift; auto.
Qed.
Lemma jerasable_env_bind : ∀ {H Z dH t12s wits vecs dZ},
jerasable_env 1 H Z →
length vecs = dH →
extract Slistprodtype t12s dZ →
extract Slisttype wits vecs →
jerasable 1 H Z wits Slisttype →
jerasable 1 (dH + H) (dmap (lift dH 0) Z) t12s Slistprodtype →
jerasable 1 H Z (subst vecs 0 t12s) Slistcoer →
jerasable_env 1 (dH + H) (dZ ++ dmap (lift dH 0) Z).
Proof.
intros.
apply JEcons with H Z dH dZ; auto.
∃ vecs.
repeat split; auto;
match goal with
| H1 : extract _ _ _ |- _ ⇒ rewrite <- (inject_extract H1)
end; auto.
Qed.
Inductive coer_left_type : type_env → coer_env → type → sort → Prop :=
| CRcoer : ∀ H Z dH dZ Y0 Y1 t1 t2,
jerasable 1 (dH + H) (dZ ++ dmap (lift dH 0) Z) t1 Stype →
coer_left_type H Z (Spair dH t1 t2) (Scoer Y0 Y1 dH dZ)
| CRtype : ∀ H Z t,
coer_left_type H Z t Stype
| CRpair : ∀ H Z t1 t2 e1 e2,
coer_left_type H Z t1 e1 →
coer_left_type H Z t2 e2 →
coer_left_type H Z (Spair 0 t1 t2) (Sprod e1 e2)
| CRnil : ∀ H Z e,
coer_left_type H Z Snil (Slist e)
| CRcons : ∀ H Z t ts e,
coer_left_type H Z t e →
coer_left_type H Z ts (Slist e) →
coer_left_type H Z (Scons t ts) (Slist e)
.
Lemma coer_left_type_type : ∀ H Z t, coer_left_type H Z t Stype.
Proof. intros; apply CRtype. Qed.
Lemma coer_left_type_listtype : ∀ H Z xs wits,
extract Slisttype wits xs →
coer_left_type H Z wits Slisttype.
Proof.
induction xs; intros; destruct_extract.
apply CRnil.
apply CRcons; auto.
apply coer_left_type_type.
Qed.
Lemma coer_left_type_listprodtype : ∀ H Z dZ t12s,
extract Slistprodtype t12s dZ →
coer_left_type H Z t12s Slistprodtype.
Proof.
induction dZ as [|[t1 t2] dZ]; intros; destruct_extract.
apply CRnil.
apply CRcons; auto.
apply CRpair; apply coer_left_type_type.
Qed.
Lemma coer_left_type_listcoer : ∀ H Z dZ t12s,
extract Slistcoer t12s dZ →
jerasable 1 H Z (inject Slistcoer dZ) Slistcoer →
coer_left_type H Z t12s Slistcoer.
Proof.
induction dZ as [|[t1 t2] dZ]; intros; destruct_extract.
apply CRnil.
inversion H1; subst.
apply CRcons; auto.
apply CRcoer.
apply (jcoer_extract_left_type M11 H7).
Qed.
Lemma coer_left_type_listcoer_subst : ∀ H Z wits vecs,
extract Slisttype wits vecs →
jerasable 1 H Z wits Slisttype →
∀ dZ t12s,
extract Slistprodtype t12s dZ →
jerasable 1 (length vecs + H) (dmap (lift (length vecs) 0) Z) t12s Slistprodtype →
coer_left_type H Z (subst vecs 0 t12s) Slistcoer.
Proof.
induction dZ as [|[t1 t2] dZ]; intros; destruct_extract.
simpl; apply CRnil.
inversion H3; subst.
inversion H9; subst.
simpl; apply CRcons; auto.
apply CRcoer; trysimpl.
apply jerasable_subst_0 with (length vecs) nil Stype; auto.
rewrite <- (inject_extract H0); auto.
simpl; apply JSNil.
Qed.
Inductive coer_ext_env : type_env → coer_env → type → sort → Prop :=
| CEcoer : ∀ H Z dH dZ Y0 Y1 t1 t2,
jerasable_env 1 (dH + H) (dZ ++ dmap (lift dH 0) Z) →
coer_ext_env H Z (Spair dH t1 t2) (Scoer Y0 Y1 dH dZ)
| CEtype : ∀ H Z t, coer_ext_env H Z t Stype
| CEprod : ∀ H Z t e1 e2, coer_ext_env H Z t (Sprod e1 e2)
| CElist : ∀ H Z t e, coer_ext_env H Z t (Slist e)
.
Definition jcoer_env H Z :=
Forall (fun ts ⇒ match ts with (t, s) ⇒ jerasable 1 H Z t Stype ∧ jerasable 1 H Z s Stype end).
Lemma jcoer_env_lift : ∀ H Z dH dZ Y,
jcoer_env H Z Y →
jcoer_env (dH + H) (dZ ++ dmap (lift dH 0) Z) (dmap (lift dH 0) Y).
Proof.
induction Y as [|[t s] Y]; simpl; intros; constructor.
inversion H0; subst; destruct H3.
split; apply jerasable_weak_coer_0; apply jerasable_lift_0 with Stype; auto.
inversion H0; subst; destruct H3.
apply IHY; auto.
Qed.
Inductive coer_coer_env : type_env → coer_env → type → sort → Prop :=
| CCcoer : ∀ H Z dH dZ Y0 Y1 t1 t2,
jcoer_env H Z Y0 → jcoer_env H Z Y1 →
coer_coer_env H Z (Spair dH t1 t2) (Scoer Y0 Y1 dH dZ)
| CCtype : ∀ H Z t,
coer_coer_env H Z t Stype
| CCpair : ∀ H Z t1 t2 e1 e2,
coer_coer_env H Z t1 e1 →
coer_coer_env H Z t2 e2 →
coer_coer_env H Z (Spair 0 t1 t2) (Sprod e1 e2)
| CCnil : ∀ H Z e,
coer_coer_env H Z Snil (Slist e)
| CCcons : ∀ H Z t ts e,
coer_coer_env H Z t e →
coer_coer_env H Z ts (Slist e) →
coer_coer_env H Z (Scons t ts) (Slist e)
.
Lemma coer_coer_env_type : ∀ H Z t, coer_coer_env H Z t Stype.
Proof. intros; apply CCtype. Qed.
Lemma coer_coer_env_listtype : ∀ H Z xs wits,
extract Slisttype wits xs →
coer_coer_env H Z wits Slisttype.
Proof.
induction xs; intros; destruct_extract.
apply CCnil.
apply CCcons; auto.
apply coer_coer_env_type.
Qed.
Lemma coer_coer_env_listprodtype : ∀ H Z dZ t12s,
extract Slistprodtype t12s dZ →
coer_coer_env H Z t12s Slistprodtype.
Proof.
induction dZ as [|[t1 t2] dZ]; intros; destruct_extract.
apply CCnil.
apply CCcons; auto.
apply CCpair; apply coer_coer_env_type.
Qed.
Lemma coer_coer_env_listcoer : ∀ H Z dZ t12s,
extract Slistcoer t12s dZ →
coer_coer_env H Z t12s Slistcoer.
Proof.
induction dZ as [|[t1 t2] dZ]; intros; destruct_extract.
apply CCnil.
apply CCcons; auto.
apply CCcoer; constructor.
Qed.
Lemma coer_coer_env_listcoer_subst : ∀ H Z vecs dZ t12s,
extract Slistprodtype t12s dZ →
coer_coer_env H Z (subst vecs 0 t12s) Slistcoer.
Proof.
induction dZ as [|[t1 t2] dZ]; intros; destruct_extract.
apply CCnil.
apply CCcons; auto.
apply CCcoer; constructor.
Qed.
Lemma coer_coer_env_lift : ∀ dH2 H dZ2 Z dH t s Y0 Y1 dZ,
jcoer_env H Z Y0 → jcoer_env H Z Y1 →
coer_coer_env (dH2 + H) (dZ2 ++ dmap (lift dH2 0) Z)
(Spair dH t s) (Scoer (dmap (lift dH2 0) Y0) (dmap (lift dH2 0) Y1) dH dZ).
Proof. intros; apply CCcoer; apply jcoer_env_lift; auto. Qed.
Lemma coer_coer_env_app : ∀ H Z Y0 Y1 dH t s dZ,
jcoer_env H Z Y0 → jcoer_env H Z Y1 →
coer_coer_env H Z (Spair dH t s) (Scoer (Y1 ++ Y0) nil dH dZ).
Proof. intros; apply CCcoer; [apply Forall_app; auto|constructor]. Qed.
Lemma coer_coer_env_lift_app : ∀ H Z Y0 Y1 dH dZ t s,
jcoer_env H Z Y0 → jcoer_env H Z Y1 →
coer_coer_env (dH + H) (dZ ++ dmap (lift dH 0) Z)
(Spair 0 t s) (Scoer (dmap (lift dH 0) Y1 ++ dmap (lift dH 0) Y0) nil 0 nil).
Proof.
intros; apply CCcoer; [|constructor].
rewrite dmap_app.
apply jcoer_env_lift.
apply Forall_app; auto.
Qed.
Lemma jerasable_env_jerasable_Z : ∀ M H Z,
jerasable_env M H Z →
jerasable M H Z (inject Slistprodtype Z) Slistprodtype.
Proof.
induction 1; intros; [apply JSNil|subst].
apply jerasable_list_app.
destruct H1 as [? [? [? [? ?]]]].
apply jerasable_weak_coer_0; auto.
apply jerasable_weak_coer_0.
repeat to_slift (Slist Sprodtype); rewrite <- lift_inject; from_slift.
apply jerasable_lift_0 with Slistprodtype; auto.
Qed.
Lemma jcoer_env_jerasable_Z : ∀ H Z Y,
jcoer_env H Z Y →
jerasable 1 H Z (inject Slistprodtype Y) Slistprodtype.
Proof.
induction Y as [|[t s] Y]; simpl; intros; [apply JSNil|apply JSCons].
inversion H0; subst; destruct H3; apply JSPair; auto.
inversion H0; subst; destruct H3.
apply IHY; auto.
Qed.
Lemma nth_jerasable_env_aux : ∀ M H t s Z c dZ,
jerasable M H Z (inject Slistprodtype dZ) Slistprodtype →
nth c dZ (Top, Top) = (t, s) →
jerasable M H Z s Stype.
Proof.
induction c; intros;
(destruct dZ as [|[t0 s0] dZ]; [inversion H1; subst; apply JTTop|]);
inversion H1; subst; inversion H0; subst;
[inversion H8; subst|apply IHc with dZ]; auto.
Qed.
Lemma nth_jerasable_env : ∀ H t s Y0 Z c,
jerasable_env 1 H Z →
jcoer_env H Z Y0 →
nth c (Y0 ++ Z) (Top, Top) = (t, s) →
jerasable 1 H Z s Stype.
Proof.
intros.
apply nth_jerasable_env_aux with t c (Y0 ++ Z); auto.
apply jerasable_list_app; [|apply jerasable_env_jerasable_Z; auto].
apply jcoer_env_jerasable_Z; auto.
Qed.
Lemma jerasable_up_1 : ∀ H Z t e,
jerasable 0 H Z t e → jerasable_env 1 H Z → coer_coer_env H Z t e →
(coer_ext_env H Z t e ∧ (coer_left_type H Z t e → jerasable 1 H Z t e)).
Proof.
Ltac induction_up_1 H := induction H; intros;
[ split; [|intros; apply JTVar]
| split; [|intros; apply JTArr]
| split; [|intros; apply JTProd]
| split; [|intros; eapply JTFor]
| split; [|intros; apply JTMu]
| split; [|intros; apply JTBot]
| split; [|intros; apply JTTop]
| split; [|intros; apply JSNil]
| split; [|intros; apply JSCons]
| split; [|intros; apply JSPair]
| split; [|intros; apply JCRefl]
| split; [|intros; eapply JCTrans]
| split; [|intros; eapply JCWeak]
| split; [|intros; apply JCArr]
| split; [|intros; apply JCProd]
| split; [|intros; eapply JCVar]
| split; [|intros; eapply JCGen]
| split; [|intros; eapply JCInst]
| split; [|intros; apply JCUnfold]
| split; [|intros; apply JCFold]
| split; [|intros; apply JCFix]
| split; [|intros; apply JCBot]
| split; [|intros; apply JCTop]].
Ltac clear_stuff :=
match goal with
| H1 : 1 ≤ 0 → _ |- _ ⇒ clear H1
| H1 : 2 ≤ 0 → _ |- _ ⇒ clear H1
| H1 : jerasable 0 _ _ _ _ |- _ ⇒ clear H1
| H1 : coer_ext_env _ _ _ Stype |- _ ⇒ clear H1
| H1 : coer_ext_env _ _ _ (Sprod _ _) |- _ ⇒ clear H1
| H1 : coer_ext_env _ _ _ (Slist _) |- _ ⇒ clear H1
| H1 : coer_left_type _ _ _ Stype |- _ ⇒ clear H1
| H1 : coer_left_type _ _ Snil (Slist _) |- _ ⇒ clear H1
| H1 : coer_coer_env _ _ _ Stype |- _ ⇒ clear H1
| H1 : coer_coer_env _ _ Snil (Slist _) |- _ ⇒ clear H1
end.
Ltac do_stuff := first [clear_stuff|
match goal with
| |- coer_ext_env _ _ _ (Scoer _ _ _ _) ⇒ apply CEcoer
| |- coer_ext_env _ _ _ Stype ⇒ apply CEtype
| |- coer_ext_env _ _ _ (Sprod _ _) ⇒ apply CEprod
| |- coer_ext_env _ _ _ (Slist _) ⇒ apply CElist
| |- 2 ≤ 1 → _ ⇒ let H1 := fresh "H" in intros H1; inversion H1
| H1 : jerasable_env 1 ?H ?Z
, H2 : extract Slistprodtype ?t12s ?dZ
, H3 : extract Slisttype ?wits ?vecs
, H4 : jerasable 1 ?H ?Z ?wits Slisttype
, H5 : jerasable 1 (length ?vecs + ?H) (dmap (lift (length ?vecs) 0) ?Z) ?t12s Slistprodtype
, H6 : jerasable 1 ?H ?Z (subst ?vecs 0 ?t12s) Slistcoer
|- jerasable_env 1 (length ?vecs + ?H) (?dZ ++ ?dmap (lift (length ?vecs) 0) ?Z)
⇒ apply (jerasable_env_bind H1 eq_refl H2 H3 H4 H5 H6)
end].
Ltac hyp_stuff := first [do_stuff|
match goal with
| _ : length ?vecs = ?dH |- _ ⇒ subst dH
| H1 : _ ∧ _ |- _ ⇒ destruct H1
| |- 1 ≤ 1 → _ ⇒ intros _
| Hx : 0 ≠ 1 → _ |- _ ⇒ pose proof (Hx M01); clear Hx
| H1 : jerasable_env 1 ?H ?Z , Hx : jerasable_env 1 ?H ?Z → _ |- _ ⇒ pose proof (Hx H1); clear Hx
| H1 : jerasable_env 1 ?H ?Z
, Hx : jerasable_env 1 (?dH + ?H) (?dmap (lift ?dH 0) ?Z) → _
|- _ ⇒ pose proof (Hx (jerasable_env_lift dH H1)); clear Hx
| H1 : jerasable_env 1 ?H ?Z
, H2 : extract Slistprodtype ?t12s ?dZ
, H3 : extract Slisttype ?wits ?vecs
, H4 : jerasable 1 ?H ?Z ?wits Slisttype
, H5 : jerasable 1 (length ?vecs + ?H) (dmap (lift (length ?vecs) 0) ?Z) ?t12s Slistprodtype
, H6 : jerasable 1 ?H ?Z (subst ?vecs 0 ?t12s) Slistcoer
, Hx : jerasable_env 1 (length ?vecs + ?H) (?dZ ++ ?dmap (lift (length ?vecs) 0) ?Z) → _
|- _ ⇒ pose proof (Hx (jerasable_env_bind H1 eq_refl H2 H3 H4 H5 H6)); clear Hx
| H1 : coer_coer_env ?H ?Z ?t ?e
, Hx : coer_coer_env ?H ?Z ?t ?e → _
|- _ ⇒ pose proof (Hx H1); clear Hx
| Hx : coer_coer_env ?H ?Z ?t Stype → _
|- _ ⇒ pose proof (Hx (coer_coer_env_type H Z t)); clear Hx
| H1 : extract Slisttype ?wits ?vecs
, Hx : coer_coer_env ?H ?Z ?wits Slisttype → _
|- _ ⇒ pose proof (Hx (coer_coer_env_listtype H Z vecs wits H1)); clear Hx
| H1 : extract Slistprodtype ?t12s ?dZ
, Hx : coer_coer_env ?H ?Z ?t12s Slistprodtype → _
|- _ ⇒ pose proof (Hx (coer_coer_env_listprodtype H Z dZ t12s H1)); clear Hx
| H1 : extract Slistprodtype ?t12s ?dZ
, Hx : coer_coer_env ?H ?Z (subst ?vecs 0 ?t12s) Slistcoer → _
|- _ ⇒ pose proof (Hx (coer_coer_env_listcoer_subst H Z vecs dZ t12s H1)); clear Hx
| H1 : jcoer_env ?H ?Z ?Y0
, H2 : jcoer_env ?H ?Z ?Y1
, Hx : coer_coer_env ?H ?Z (Spair ?dH ?t ?s) (Scoer ?Y0 ?Y1 ?dH ?dZ) → _
|- _ ⇒ pose proof (Hx (CCcoer H Z dH dZ Y0 Y1 t s H1 H2)); clear Hx
| H1 : jcoer_env ?H ?Z ?Y0
, H2 : jcoer_env ?H ?Z ?Y1
, Hx : coer_coer_env (?dH2 + ?H) (?dZ2 ++ dmap (lift ?dH2 0) ?Z)
(Spair ?dH ?t ?s) (Scoer (dmap (lift ?dH2 0) ?Y0) (dmap (lift ?dH2 0) ?Y1) ?dH ?dZ) → _
|- _ ⇒ pose proof (Hx (coer_coer_env_lift dH2 H dZ2 Z dH t s Y0 Y1 dZ H1 H2)); clear Hx
| H1 : jcoer_env ?H ?Z ?Y0
, H2 : jcoer_env ?H ?Z ?Y1
, Hx : coer_coer_env ?H ?Z (Spair ?dH ?t ?s) (Scoer (?Y1 ++ ?Y0) nil ?dH ?dZ) → _
|- _ ⇒ pose proof (Hx (coer_coer_env_app H Z Y0 Y1 dH t s dZ H1 H2)); clear Hx
| H1 : jcoer_env ?H ?Z ?Y0
, H2 : jcoer_env ?H ?Z ?Y1
, Hx : coer_coer_env (?dH + ?H) (?dZ ++ dmap (lift ?dH 0) ?Z)
(Spair 0 ?t ?s) (Scoer (dmap (lift ?dH 0) ?Y1 ++ dmap (lift ?dH 0) ?Y0) nil 0 nil) → _
|- _ ⇒ pose proof (Hx (coer_coer_env_lift_app H Z Y0 Y1 dH dZ t s H1 H2)); clear Hx
| Hx : coer_left_type ?H ?Z ?t Stype → _
|- _ ⇒ pose proof (Hx (coer_left_type_type H Z t)); clear Hx
| H1 : extract Slisttype ?wits ?vecs
, Hx : coer_left_type ?H ?Z ?wits Slisttype → _
|- _ ⇒ pose proof (Hx (coer_left_type_listtype H Z vecs wits H1)); clear Hx
| H1 : extract Slistprodtype ?t12s ?dZ
, Hx : coer_left_type ?H ?Z ?t12s Slistprodtype → _
|- _ ⇒ pose proof (Hx (coer_left_type_listprodtype H Z dZ t12s H1)); clear Hx
| H1 : extract Slistprodtype ?t12s ?dZ
, H2 : extract Slisttype ?wits ?vecs
, H3 : jerasable 1 ?H ?Z ?wits Slisttype
, H4 : jerasable 1 (length ?vecs + ?H) (dmap (lift (length ?vecs) 0) ?Z) ?t12s Slistprodtype
, Hx : coer_left_type ?H ?Z (subst ?vecs 0 ?t12s) Slistcoer → _
|- _ ⇒ pose proof (Hx (coer_left_type_listcoer_subst H Z wits vecs H2 H3 dZ t12s H1 H4)); clear Hx
end].
Ltac inv_stuff := first [hyp_stuff|
match goal with
| H1 : coer_ext_env _ _ _ (Scoer _ _ _ _) |- _ ⇒ inversion H1; clear H1; subst
| H1 : coer_left_type _ _ _ (Scoer _ _ _ _) |- _ ⇒ inversion H1; clear H1; subst
| H1 : coer_left_type _ _ _ (Sprod _ _) |- _ ⇒ inversion H1; clear H1; subst
| H1 : coer_left_type _ _ (Scons _ _) (Slist _) |- _ ⇒ inversion H1; clear H1; subst
| H1 : coer_coer_env _ _ _ (Scoer _ _ _ _) |- _ ⇒ inversion H1; clear H1; subst
| H1 : coer_coer_env _ _ _ (Sprod _ _) |- _ ⇒ inversion H1; clear H1; subst
| H1 : coer_coer_env _ _ (Scons _ _) (Slist _) |- _ ⇒ inversion H1; clear H1; subst
end].
Ltac step := first [inv_stuff|
match goal with
| H1 : jerasable 1 _ _ (Arr _ _) _ |- _ ⇒ inversion H1; clear H1; subst
| H1 : jerasable 1 _ _ (Prod _ _) _ |- _ ⇒ inversion H1; clear H1; subst
| H1 : jerasable 1 ?H ?Z (Spair ?dH ?t ?s) (Scoer _ _ ?dH ?dZ)
|- jerasable 1 ?H ?Z ?s Stype ⇒ apply (jcoer_extract_right_type M11 H1)
| H1 : jerasable 1 ?H ?Z ?t Stype
|- jerasable 1 (?dH + ?H) (_ ++ dmap (lift ?dH 0) ?Z) (lift ?dH 0 ?t) Stype
⇒ apply jerasable_weak_coer_0
| H1 : jerasable 1 ?H ?Z ?t Stype
|- jerasable 1 (?dH + ?H) (dmap (lift ?dH 0) ?Z) (lift ?dH 0 ?t) Stype
⇒ apply jerasable_lift_0 with Stype
| Hx : coer_left_type ?H ?Z (Spair ?dH ?t ?s) (Scoer ?Y0 ?Y1 ?dH ?dZ) → _
|- _ ⇒ let H1 := fresh "H" in assert (coer_left_type H Z (Spair dH t s) (Scoer Y0 Y1 dH dZ)) as H1;
[clear Hx; apply CRcoer|pose proof (Hx H1); clear Hx]
end].
intros H Z t e HZte; induction_up_1 HZte; repeat (step; trysimpl; eauto).
apply nth_jerasable_env with t Y0 c; auto.
apply JTFor with dZ wits vecs; auto.
inversion H10; subst; apply H0;
[apply coer_coer_env_listcoer_subst with dZ|apply coer_left_type_listcoer_subst with insts dZ]; auto.
apply H1; repeat constructor; tryomega.
Qed.
Lemma jerasable_bind_up_1 : ∀ H Z dH dZ, jerasable_bind 0 H Z dH dZ →
jerasable_env 1 H Z → jerasable_bind 1 H Z dH dZ.
Proof.
intros H Z dH dZ [? [? [? [? ?]]]]; intros HZ.
∃ x; repeat split; auto; apply jerasable_up_1; auto.
apply JEcons with H Z dH nil; auto; apply jerasable_bind_only_type.
apply coer_coer_env_listprodtype with dZ; apply extract_inject.
apply coer_left_type_listprodtype with dZ; apply extract_inject.
apply coer_coer_env_listtype with x; apply extract_inject.
apply coer_left_type_listtype with x; apply extract_inject.
apply coer_coer_env_listcoer_subst with dZ; apply extract_inject.
apply coer_left_type_listcoer_subst with (inject Slisttype x) dZ; auto;
try apply extract_inject.
apply jerasable_up_1; auto.
apply coer_coer_env_listtype with x; apply extract_inject.
apply coer_left_type_listtype with x; apply extract_inject.
subst.
apply jerasable_up_1; auto.
apply JEcons with H Z (length x) nil; auto.
apply jerasable_bind_only_type.
apply coer_coer_env_listprodtype with dZ; apply extract_inject.
apply coer_left_type_listprodtype with dZ; apply extract_inject.
Qed.
Lemma jerasable_env_up_1 : ∀ H Z,
jerasable_env 0 H Z → jerasable_env 1 H Z.
Proof.
intros H Z HZ.
induction HZ; [apply JEnil|eapply JEcons]; eauto.
apply jerasable_bind_up_1; auto.
Qed.
Lemma jterm_env_up_1 : ∀ H Z G,
jterm_env 0 H Z G → jerasable_env 1 H Z → jterm_env 1 H Z G.
Proof.
intros H Z G [_ ?] ?.
split; auto.
eapply Forall_impl; [|apply H0].
unfold jtype; intros.
apply jerasable_up_1; auto.
apply coer_coer_env_type.
apply coer_left_type_type.
Qed.
Lemma jcoer_rebuild_jterm_env : ∀ H Z G dH dZ Y0 Y1 t s,
jerasable 0 H Z (Spair dH t s) (Scoer Y0 Y1 dH dZ) →
jterm_env 1 H Z G →
jterm_env 1 (dH + H) (dZ ++ dmap (lift dH 0) Z) (map (lift dH 0) G).
Proof.
split; destruct H1.
intros _.
apply jerasable_env_up_1; auto.
apply jcoer_extract_jerasable_env with Y0 Y1 t s; auto.
apply jerasable_env_down.
apply jerasable_env_up_2; auto.
eapply Forall_map_impl; [|apply H2].
unfold jtype; intros ? ?.
apply jerasable_weak_coer_0.
apply jerasable_lift_0 with Stype; auto.
Qed.
Lemma jterm_up_1 : ∀ H Z G a t, jterm 0 H Z G a t →
jterm_env 1 H Z G → jterm 1 H Z G a t.
Proof.
intros H Z G a t HZGat; jterm_induction HZGat; eauto; unfold jtype, jcoer in *;
repeat (match goal with
| H1 : 1 ≤ 0 → _ |- _ ⇒ clear H1
| |- _ ≤ _ → _ ⇒ intros _
end; eauto).
intros Heq; exfalso; omega.
apply IHHZGat.
destruct H1; split; auto.
constructor; auto.
apply jerasable_up_1; auto.
apply coer_coer_env_type.
apply coer_left_type_type.
destruct H2; apply jerasable_up_1; eauto.
apply CCcoer; constructor.
apply CRcoer.
apply @jterm_extract_jtype with (map (lift dH 0) G) a; auto.
apply IHHZGat.
apply jcoer_rebuild_jterm_env with nil nil t s; auto.
apply IHHZGat.
apply jcoer_rebuild_jterm_env with nil nil t s; auto.
Qed.
Print Assumptions jterm_down.
Print Assumptions jterm_up_2.
Print Assumptions jterm_up_1.
Require Import Omega.
Require Import list.
Require Import mxx.
Require Import typesystem.
Require Import Ltypesystem.
Lemma jerasable_down : ∀ M H Z t e,
jerasable 2 H Z t e → jerasable M H Z t e.
Proof. intros M H Z t e HZte; jerasable_induction HZte; eauto. Qed.
Lemma jerasable_bind_down : ∀ M H Z dH dZ,
jerasable_bind 2 H Z dH dZ → jerasable_bind M H Z dH dZ.
Proof.
intros M H Z dH dZ [? [? [? [? ?]]]].
∃ x; repeat split; auto; apply jerasable_down; auto.
Qed.
Lemma jerasable_env_down : ∀ M H Z,
jerasable_env 2 H Z → jerasable_env M H Z.
Proof.
intros M H Z HZ.
induction HZ; [apply JEnil|eapply JEcons]; eauto.
apply jerasable_bind_down; auto.
Qed.
Lemma jterm_env_down : ∀ M H Z G,
jterm_env 2 H Z G → jterm_env M H Z G.
Proof.
intros M H Z G [? ?].
split.
intros m; apply jerasable_env_down; auto.
eapply Forall_impl; [|apply H1].
unfold jtype; intros.
apply jerasable_down; auto.
Qed.
Lemma jterm_down : ∀ M H Z G a t,
jterm 2 H Z G a t → jterm M H Z G a t.
Proof.
intros M H Z G a t HZGat; jterm_induction HZGat; eauto; unfold jtype, jcoer in *;
repeat (match goal with
| |- _ ≤ M → _ ⇒ intros m
| |- jterm_env M _ _ _ ⇒ apply jterm_env_down
| |- jerasable M _ _ _ _ ⇒ apply jerasable_down
end; auto).
intros m; apply jerasable_down; auto.
Qed.
Lemma jerasable_up_2 : ∀ H Z t e,
jerasable 1 H Z t e → jerasable 2 H Z t e.
Proof.
intros H Z t e HZte; jerasable_induction HZte; eauto;
repeat (match goal with
| H1 : 2 ≤ 1 → _ |- _ ⇒ clear H1
| |- 2 ≤ 2 → _ ⇒ intros _
| |- 2 ≠ 1 → _ ⇒ intros _
| H1 : jerasable 2 ?H ?Z (Spair ?dH ?t ?s) (Scoer _ _ ?dH ?dZ)
|- jerasable 2 (?dH + ?H) (?dZ ++ dmap (lift ?dH 0) ?Z) ?t Stype
⇒ apply (jcoer_extract_left_type M12 H1)
| H1 : jerasable 2 ?H ?Z (Spair ?dH ?t ?s) (Scoer _ _ ?dH ?dZ)
|- jerasable 2 ?H ?Z ?s Stype
⇒ apply (jcoer_extract_right_type M12 H1)
| H1 : jerasable 2 ?H ?Z (Mu ?t) Stype
|- jerasable 2 (1 + ?H) (dmap (lift 1 0) ?Z) ?t Stype
⇒ inversion H1; assumption
end; auto); pose proof (H1 M11) as Hmu; inversion Hmu; assumption.
Qed.
Lemma jerasable_bind_up_2 : ∀ H Z dH dZ,
jerasable_bind 1 H Z dH dZ → jerasable_bind 2 H Z dH dZ.
Proof.
intros H Z dH dZ [? [? [? [? ?]]]].
∃ x; repeat split; auto; apply jerasable_up_2; auto.
Qed.
Lemma jerasable_env_up_2 : ∀ H Z,
jerasable_env 1 H Z → jerasable_env 2 H Z.
Proof.
intros H Z HZ.
induction HZ; [apply JEnil|eapply JEcons]; eauto.
apply jerasable_bind_up_2; auto.
Qed.
Lemma jterm_env_up_2 : ∀ H Z G,
jterm_env 1 H Z G → jterm_env 2 H Z G.
Proof.
intros H Z G [? ?].
split.
intros.
apply jerasable_env_up_2; auto.
eapply Forall_impl; [|apply H1].
unfold jtype; intros.
apply jerasable_up_2; auto.
Qed.
Lemma jterm_up_2 : ∀ H Z G a t,
jterm 1 H Z G a t → jterm 2 H Z G a t.
Proof.
intros H Z G a t HZGat; jterm_induction HZGat; eauto; unfold jtype, jcoer in *;
repeat (match goal with
| |- _ ≤ _ → _ ⇒ intros _
| |- jterm_env 2 _ _ _ ⇒ apply jterm_env_up_2
| |- jerasable 2 _ _ _ _ ⇒ apply jerasable_up_2
end; auto).
intros _.
pose proof (jterm_extract_jterm_env M12 IHHZGat) as [_ ?].
inversion H1; auto.
Qed.
Lemma jerasable_list_app : ∀ M e e' H Z x2s x1s,
jerasable M H Z (inject (Slist e') x1s) (Slist e) →
jerasable M H Z (inject (Slist e') x2s) (Slist e) →
jerasable M H Z (inject (Slist e') (x1s ++ x2s)) (Slist e).
Proof.
induction x1s; simpl; intros; auto.
inversion H0; subst.
constructor; auto.
Qed.
Ltac from_slift :=
match goal with
| |- context[slift Slisttype ?d ?i ?vecs] ⇒
replace (slift Slisttype d i vecs) with (map (lift d i) vecs) by reflexivity
| |- context[slift Slistcoer ?d ?i ?Z] ⇒
replace (slift Slistcoer d i Z) with (dmap (lift d i) Z) by reflexivity
| |- context[slift Slistprodtype ?d ?i ?Z] ⇒
replace (slift Slistprodtype d i Z) with (dmap (lift d i) Z) by reflexivity
end.
Ltac to_slift s :=
match goal with
| |- context[dmap (lift ?d ?i) ?Z] ⇒
replace (dmap (lift d i) Z) with (slift s d i Z) by reflexivity
| |- context[map (lift ?d ?i) ?vecs] ⇒
replace (map (lift d i) vecs) with (slift Slisttype d i vecs) by reflexivity
end.
Lemma jerasable_bind_only_type : ∀ M H Z dH, jerasable_bind M H Z dH nil.
Proof.
intros; induction dH.
∃ nil.
repeat split; simpl; constructor.
destruct IHdH as [xs [? [? [? ?]]]].
∃ (Top :: xs).
repeat split; simpl; repeat constructor; auto.
Qed.
Ltac trysimpl := repeat
match goal with
| |- context[0 + ?x] ⇒ replace (0 + x) with x by reflexivity
| H : context[0 + ?x] |- _ ⇒ replace (0 + x) with x in H by reflexivity
| |- context[nil ++ ?xs] ⇒ replace (nil ++ xs) with xs by reflexivity
| H : context[nil ++ ?xs] |- _ ⇒ replace (nil ++ xs) with xs in H by reflexivity
| |- context[_ + 0] ⇒ rewrite <- plus_n_O
| H : context[_ + 0] |- _ ⇒ rewrite <- plus_n_O in H
| |- context[_ ++ nil] ⇒ rewrite app_nil_r
| H : context[_ ++ nil] |- _ ⇒ rewrite app_nil_r in H
| |- context[dmap (lift 0 _) _] ⇒ rewrite dmap_lift_0
| H : context[dmap (lift 0 _) _] |- _ ⇒ rewrite dmap_lift_0 in H
| |- context[dmap ?f nil] ⇒ replace (dmap f nil) with (@nil (type × type)) by reflexivity
| H : context[dmap ?f nil] |- _ ⇒
replace (dmap f nil) with (@nil (type × type)) in H by reflexivity
| |- context[_ + (_ + _)] ⇒ rewrite plus_assoc
| H : context[_ + (_ + _)] |- _ ⇒ rewrite plus_assoc in H
| |- context[dmap _ (_ ++ _)] ⇒ rewrite <- dmap_app
| H : context[dmap _ (_ ++ _)] |- _ ⇒ rewrite <- dmap_app in H
| |- context[_ ++ _ ++ _] ⇒ rewrite app_assoc
| H : context[_ ++ _ ++ _] |- _ ⇒ rewrite app_assoc in H
| |- context[dmap (lift (_ + _) ?i) _] ⇒ rewrite dmap_lift_plus
| H : context[dmap (lift (_ + _) ?i) _] |- _ ⇒ rewrite dmap_lift_plus in H
| |- context[length (_ ++ _)] ⇒ rewrite app_length
| H : context[length (_ ++ _)] |- _ ⇒ rewrite app_length in H
end.
Lemma jerasable_bind_lift : ∀ {M H Z dH dZ dH0},
jerasable_bind M H Z dH dZ →
jerasable_bind M H Z (dH0 + dH) (dmap (lift dH0 0) dZ).
Proof.
intros.
destruct H0 as [? [? [? [? ?]]]].
destruct (replicate _ Top dH0) as [? [? ?]].
∃ (map (subst x 0) x0 ++ x).
repeat split; trysimpl; tryomega.
repeat to_slift (Slist Sprodtype); rewrite <- lift_inject; from_slift.
rewrite <- plus_assoc.
apply jerasable_lift_0 with Slistprodtype; auto.
apply jerasable_list_app; auto.
clear H2 H3 H1 dZ.
induction x0; simpl; [apply JSNil|apply JSCons].
pose proof (H5 0); simpl in H0; subst; simpl; apply JTTop.
apply IHx0; intros i.
pose proof (H5 (1 + i)); simpl in H0; auto.
rewrite subst_app.
repeat to_slift (Slist Sprodtype); rewrite <- lift_inject.
rewrite subst_lift; auto.
replace (length x0 - length x0) with 0 by omega.
rewrite lift_0; auto.
Qed.
Lemma jerasable_env_lift : ∀ {M H Z} dH,
jerasable_env M H Z →
jerasable_env M (dH + H) (dmap (lift dH 0) Z).
Proof.
induction 1; simpl.
apply JEcons with 0 nil (dH + 0) nil; simpl; auto; [apply JEnil|].
apply jerasable_bind_only_type.
subst; trysimpl.
apply JEcons with H Z (dH + dH0) (dmap (lift dH 0) dZ); tryomega.
apply jerasable_bind_lift; auto.
Qed.
Lemma jerasable_env_bind : ∀ {H Z dH t12s wits vecs dZ},
jerasable_env 1 H Z →
length vecs = dH →
extract Slistprodtype t12s dZ →
extract Slisttype wits vecs →
jerasable 1 H Z wits Slisttype →
jerasable 1 (dH + H) (dmap (lift dH 0) Z) t12s Slistprodtype →
jerasable 1 H Z (subst vecs 0 t12s) Slistcoer →
jerasable_env 1 (dH + H) (dZ ++ dmap (lift dH 0) Z).
Proof.
intros.
apply JEcons with H Z dH dZ; auto.
∃ vecs.
repeat split; auto;
match goal with
| H1 : extract _ _ _ |- _ ⇒ rewrite <- (inject_extract H1)
end; auto.
Qed.
Inductive coer_left_type : type_env → coer_env → type → sort → Prop :=
| CRcoer : ∀ H Z dH dZ Y0 Y1 t1 t2,
jerasable 1 (dH + H) (dZ ++ dmap (lift dH 0) Z) t1 Stype →
coer_left_type H Z (Spair dH t1 t2) (Scoer Y0 Y1 dH dZ)
| CRtype : ∀ H Z t,
coer_left_type H Z t Stype
| CRpair : ∀ H Z t1 t2 e1 e2,
coer_left_type H Z t1 e1 →
coer_left_type H Z t2 e2 →
coer_left_type H Z (Spair 0 t1 t2) (Sprod e1 e2)
| CRnil : ∀ H Z e,
coer_left_type H Z Snil (Slist e)
| CRcons : ∀ H Z t ts e,
coer_left_type H Z t e →
coer_left_type H Z ts (Slist e) →
coer_left_type H Z (Scons t ts) (Slist e)
.
Lemma coer_left_type_type : ∀ H Z t, coer_left_type H Z t Stype.
Proof. intros; apply CRtype. Qed.
Lemma coer_left_type_listtype : ∀ H Z xs wits,
extract Slisttype wits xs →
coer_left_type H Z wits Slisttype.
Proof.
induction xs; intros; destruct_extract.
apply CRnil.
apply CRcons; auto.
apply coer_left_type_type.
Qed.
Lemma coer_left_type_listprodtype : ∀ H Z dZ t12s,
extract Slistprodtype t12s dZ →
coer_left_type H Z t12s Slistprodtype.
Proof.
induction dZ as [|[t1 t2] dZ]; intros; destruct_extract.
apply CRnil.
apply CRcons; auto.
apply CRpair; apply coer_left_type_type.
Qed.
Lemma coer_left_type_listcoer : ∀ H Z dZ t12s,
extract Slistcoer t12s dZ →
jerasable 1 H Z (inject Slistcoer dZ) Slistcoer →
coer_left_type H Z t12s Slistcoer.
Proof.
induction dZ as [|[t1 t2] dZ]; intros; destruct_extract.
apply CRnil.
inversion H1; subst.
apply CRcons; auto.
apply CRcoer.
apply (jcoer_extract_left_type M11 H7).
Qed.
Lemma coer_left_type_listcoer_subst : ∀ H Z wits vecs,
extract Slisttype wits vecs →
jerasable 1 H Z wits Slisttype →
∀ dZ t12s,
extract Slistprodtype t12s dZ →
jerasable 1 (length vecs + H) (dmap (lift (length vecs) 0) Z) t12s Slistprodtype →
coer_left_type H Z (subst vecs 0 t12s) Slistcoer.
Proof.
induction dZ as [|[t1 t2] dZ]; intros; destruct_extract.
simpl; apply CRnil.
inversion H3; subst.
inversion H9; subst.
simpl; apply CRcons; auto.
apply CRcoer; trysimpl.
apply jerasable_subst_0 with (length vecs) nil Stype; auto.
rewrite <- (inject_extract H0); auto.
simpl; apply JSNil.
Qed.
Inductive coer_ext_env : type_env → coer_env → type → sort → Prop :=
| CEcoer : ∀ H Z dH dZ Y0 Y1 t1 t2,
jerasable_env 1 (dH + H) (dZ ++ dmap (lift dH 0) Z) →
coer_ext_env H Z (Spair dH t1 t2) (Scoer Y0 Y1 dH dZ)
| CEtype : ∀ H Z t, coer_ext_env H Z t Stype
| CEprod : ∀ H Z t e1 e2, coer_ext_env H Z t (Sprod e1 e2)
| CElist : ∀ H Z t e, coer_ext_env H Z t (Slist e)
.
Definition jcoer_env H Z :=
Forall (fun ts ⇒ match ts with (t, s) ⇒ jerasable 1 H Z t Stype ∧ jerasable 1 H Z s Stype end).
Lemma jcoer_env_lift : ∀ H Z dH dZ Y,
jcoer_env H Z Y →
jcoer_env (dH + H) (dZ ++ dmap (lift dH 0) Z) (dmap (lift dH 0) Y).
Proof.
induction Y as [|[t s] Y]; simpl; intros; constructor.
inversion H0; subst; destruct H3.
split; apply jerasable_weak_coer_0; apply jerasable_lift_0 with Stype; auto.
inversion H0; subst; destruct H3.
apply IHY; auto.
Qed.
Inductive coer_coer_env : type_env → coer_env → type → sort → Prop :=
| CCcoer : ∀ H Z dH dZ Y0 Y1 t1 t2,
jcoer_env H Z Y0 → jcoer_env H Z Y1 →
coer_coer_env H Z (Spair dH t1 t2) (Scoer Y0 Y1 dH dZ)
| CCtype : ∀ H Z t,
coer_coer_env H Z t Stype
| CCpair : ∀ H Z t1 t2 e1 e2,
coer_coer_env H Z t1 e1 →
coer_coer_env H Z t2 e2 →
coer_coer_env H Z (Spair 0 t1 t2) (Sprod e1 e2)
| CCnil : ∀ H Z e,
coer_coer_env H Z Snil (Slist e)
| CCcons : ∀ H Z t ts e,
coer_coer_env H Z t e →
coer_coer_env H Z ts (Slist e) →
coer_coer_env H Z (Scons t ts) (Slist e)
.
Lemma coer_coer_env_type : ∀ H Z t, coer_coer_env H Z t Stype.
Proof. intros; apply CCtype. Qed.
Lemma coer_coer_env_listtype : ∀ H Z xs wits,
extract Slisttype wits xs →
coer_coer_env H Z wits Slisttype.
Proof.
induction xs; intros; destruct_extract.
apply CCnil.
apply CCcons; auto.
apply coer_coer_env_type.
Qed.
Lemma coer_coer_env_listprodtype : ∀ H Z dZ t12s,
extract Slistprodtype t12s dZ →
coer_coer_env H Z t12s Slistprodtype.
Proof.
induction dZ as [|[t1 t2] dZ]; intros; destruct_extract.
apply CCnil.
apply CCcons; auto.
apply CCpair; apply coer_coer_env_type.
Qed.
Lemma coer_coer_env_listcoer : ∀ H Z dZ t12s,
extract Slistcoer t12s dZ →
coer_coer_env H Z t12s Slistcoer.
Proof.
induction dZ as [|[t1 t2] dZ]; intros; destruct_extract.
apply CCnil.
apply CCcons; auto.
apply CCcoer; constructor.
Qed.
Lemma coer_coer_env_listcoer_subst : ∀ H Z vecs dZ t12s,
extract Slistprodtype t12s dZ →
coer_coer_env H Z (subst vecs 0 t12s) Slistcoer.
Proof.
induction dZ as [|[t1 t2] dZ]; intros; destruct_extract.
apply CCnil.
apply CCcons; auto.
apply CCcoer; constructor.
Qed.
Lemma coer_coer_env_lift : ∀ dH2 H dZ2 Z dH t s Y0 Y1 dZ,
jcoer_env H Z Y0 → jcoer_env H Z Y1 →
coer_coer_env (dH2 + H) (dZ2 ++ dmap (lift dH2 0) Z)
(Spair dH t s) (Scoer (dmap (lift dH2 0) Y0) (dmap (lift dH2 0) Y1) dH dZ).
Proof. intros; apply CCcoer; apply jcoer_env_lift; auto. Qed.
Lemma coer_coer_env_app : ∀ H Z Y0 Y1 dH t s dZ,
jcoer_env H Z Y0 → jcoer_env H Z Y1 →
coer_coer_env H Z (Spair dH t s) (Scoer (Y1 ++ Y0) nil dH dZ).
Proof. intros; apply CCcoer; [apply Forall_app; auto|constructor]. Qed.
Lemma coer_coer_env_lift_app : ∀ H Z Y0 Y1 dH dZ t s,
jcoer_env H Z Y0 → jcoer_env H Z Y1 →
coer_coer_env (dH + H) (dZ ++ dmap (lift dH 0) Z)
(Spair 0 t s) (Scoer (dmap (lift dH 0) Y1 ++ dmap (lift dH 0) Y0) nil 0 nil).
Proof.
intros; apply CCcoer; [|constructor].
rewrite dmap_app.
apply jcoer_env_lift.
apply Forall_app; auto.
Qed.
Lemma jerasable_env_jerasable_Z : ∀ M H Z,
jerasable_env M H Z →
jerasable M H Z (inject Slistprodtype Z) Slistprodtype.
Proof.
induction 1; intros; [apply JSNil|subst].
apply jerasable_list_app.
destruct H1 as [? [? [? [? ?]]]].
apply jerasable_weak_coer_0; auto.
apply jerasable_weak_coer_0.
repeat to_slift (Slist Sprodtype); rewrite <- lift_inject; from_slift.
apply jerasable_lift_0 with Slistprodtype; auto.
Qed.
Lemma jcoer_env_jerasable_Z : ∀ H Z Y,
jcoer_env H Z Y →
jerasable 1 H Z (inject Slistprodtype Y) Slistprodtype.
Proof.
induction Y as [|[t s] Y]; simpl; intros; [apply JSNil|apply JSCons].
inversion H0; subst; destruct H3; apply JSPair; auto.
inversion H0; subst; destruct H3.
apply IHY; auto.
Qed.
Lemma nth_jerasable_env_aux : ∀ M H t s Z c dZ,
jerasable M H Z (inject Slistprodtype dZ) Slistprodtype →
nth c dZ (Top, Top) = (t, s) →
jerasable M H Z s Stype.
Proof.
induction c; intros;
(destruct dZ as [|[t0 s0] dZ]; [inversion H1; subst; apply JTTop|]);
inversion H1; subst; inversion H0; subst;
[inversion H8; subst|apply IHc with dZ]; auto.
Qed.
Lemma nth_jerasable_env : ∀ H t s Y0 Z c,
jerasable_env 1 H Z →
jcoer_env H Z Y0 →
nth c (Y0 ++ Z) (Top, Top) = (t, s) →
jerasable 1 H Z s Stype.
Proof.
intros.
apply nth_jerasable_env_aux with t c (Y0 ++ Z); auto.
apply jerasable_list_app; [|apply jerasable_env_jerasable_Z; auto].
apply jcoer_env_jerasable_Z; auto.
Qed.
Lemma jerasable_up_1 : ∀ H Z t e,
jerasable 0 H Z t e → jerasable_env 1 H Z → coer_coer_env H Z t e →
(coer_ext_env H Z t e ∧ (coer_left_type H Z t e → jerasable 1 H Z t e)).
Proof.
Ltac induction_up_1 H := induction H; intros;
[ split; [|intros; apply JTVar]
| split; [|intros; apply JTArr]
| split; [|intros; apply JTProd]
| split; [|intros; eapply JTFor]
| split; [|intros; apply JTMu]
| split; [|intros; apply JTBot]
| split; [|intros; apply JTTop]
| split; [|intros; apply JSNil]
| split; [|intros; apply JSCons]
| split; [|intros; apply JSPair]
| split; [|intros; apply JCRefl]
| split; [|intros; eapply JCTrans]
| split; [|intros; eapply JCWeak]
| split; [|intros; apply JCArr]
| split; [|intros; apply JCProd]
| split; [|intros; eapply JCVar]
| split; [|intros; eapply JCGen]
| split; [|intros; eapply JCInst]
| split; [|intros; apply JCUnfold]
| split; [|intros; apply JCFold]
| split; [|intros; apply JCFix]
| split; [|intros; apply JCBot]
| split; [|intros; apply JCTop]].
Ltac clear_stuff :=
match goal with
| H1 : 1 ≤ 0 → _ |- _ ⇒ clear H1
| H1 : 2 ≤ 0 → _ |- _ ⇒ clear H1
| H1 : jerasable 0 _ _ _ _ |- _ ⇒ clear H1
| H1 : coer_ext_env _ _ _ Stype |- _ ⇒ clear H1
| H1 : coer_ext_env _ _ _ (Sprod _ _) |- _ ⇒ clear H1
| H1 : coer_ext_env _ _ _ (Slist _) |- _ ⇒ clear H1
| H1 : coer_left_type _ _ _ Stype |- _ ⇒ clear H1
| H1 : coer_left_type _ _ Snil (Slist _) |- _ ⇒ clear H1
| H1 : coer_coer_env _ _ _ Stype |- _ ⇒ clear H1
| H1 : coer_coer_env _ _ Snil (Slist _) |- _ ⇒ clear H1
end.
Ltac do_stuff := first [clear_stuff|
match goal with
| |- coer_ext_env _ _ _ (Scoer _ _ _ _) ⇒ apply CEcoer
| |- coer_ext_env _ _ _ Stype ⇒ apply CEtype
| |- coer_ext_env _ _ _ (Sprod _ _) ⇒ apply CEprod
| |- coer_ext_env _ _ _ (Slist _) ⇒ apply CElist
| |- 2 ≤ 1 → _ ⇒ let H1 := fresh "H" in intros H1; inversion H1
| H1 : jerasable_env 1 ?H ?Z
, H2 : extract Slistprodtype ?t12s ?dZ
, H3 : extract Slisttype ?wits ?vecs
, H4 : jerasable 1 ?H ?Z ?wits Slisttype
, H5 : jerasable 1 (length ?vecs + ?H) (dmap (lift (length ?vecs) 0) ?Z) ?t12s Slistprodtype
, H6 : jerasable 1 ?H ?Z (subst ?vecs 0 ?t12s) Slistcoer
|- jerasable_env 1 (length ?vecs + ?H) (?dZ ++ ?dmap (lift (length ?vecs) 0) ?Z)
⇒ apply (jerasable_env_bind H1 eq_refl H2 H3 H4 H5 H6)
end].
Ltac hyp_stuff := first [do_stuff|
match goal with
| _ : length ?vecs = ?dH |- _ ⇒ subst dH
| H1 : _ ∧ _ |- _ ⇒ destruct H1
| |- 1 ≤ 1 → _ ⇒ intros _
| Hx : 0 ≠ 1 → _ |- _ ⇒ pose proof (Hx M01); clear Hx
| H1 : jerasable_env 1 ?H ?Z , Hx : jerasable_env 1 ?H ?Z → _ |- _ ⇒ pose proof (Hx H1); clear Hx
| H1 : jerasable_env 1 ?H ?Z
, Hx : jerasable_env 1 (?dH + ?H) (?dmap (lift ?dH 0) ?Z) → _
|- _ ⇒ pose proof (Hx (jerasable_env_lift dH H1)); clear Hx
| H1 : jerasable_env 1 ?H ?Z
, H2 : extract Slistprodtype ?t12s ?dZ
, H3 : extract Slisttype ?wits ?vecs
, H4 : jerasable 1 ?H ?Z ?wits Slisttype
, H5 : jerasable 1 (length ?vecs + ?H) (dmap (lift (length ?vecs) 0) ?Z) ?t12s Slistprodtype
, H6 : jerasable 1 ?H ?Z (subst ?vecs 0 ?t12s) Slistcoer
, Hx : jerasable_env 1 (length ?vecs + ?H) (?dZ ++ ?dmap (lift (length ?vecs) 0) ?Z) → _
|- _ ⇒ pose proof (Hx (jerasable_env_bind H1 eq_refl H2 H3 H4 H5 H6)); clear Hx
| H1 : coer_coer_env ?H ?Z ?t ?e
, Hx : coer_coer_env ?H ?Z ?t ?e → _
|- _ ⇒ pose proof (Hx H1); clear Hx
| Hx : coer_coer_env ?H ?Z ?t Stype → _
|- _ ⇒ pose proof (Hx (coer_coer_env_type H Z t)); clear Hx
| H1 : extract Slisttype ?wits ?vecs
, Hx : coer_coer_env ?H ?Z ?wits Slisttype → _
|- _ ⇒ pose proof (Hx (coer_coer_env_listtype H Z vecs wits H1)); clear Hx
| H1 : extract Slistprodtype ?t12s ?dZ
, Hx : coer_coer_env ?H ?Z ?t12s Slistprodtype → _
|- _ ⇒ pose proof (Hx (coer_coer_env_listprodtype H Z dZ t12s H1)); clear Hx
| H1 : extract Slistprodtype ?t12s ?dZ
, Hx : coer_coer_env ?H ?Z (subst ?vecs 0 ?t12s) Slistcoer → _
|- _ ⇒ pose proof (Hx (coer_coer_env_listcoer_subst H Z vecs dZ t12s H1)); clear Hx
| H1 : jcoer_env ?H ?Z ?Y0
, H2 : jcoer_env ?H ?Z ?Y1
, Hx : coer_coer_env ?H ?Z (Spair ?dH ?t ?s) (Scoer ?Y0 ?Y1 ?dH ?dZ) → _
|- _ ⇒ pose proof (Hx (CCcoer H Z dH dZ Y0 Y1 t s H1 H2)); clear Hx
| H1 : jcoer_env ?H ?Z ?Y0
, H2 : jcoer_env ?H ?Z ?Y1
, Hx : coer_coer_env (?dH2 + ?H) (?dZ2 ++ dmap (lift ?dH2 0) ?Z)
(Spair ?dH ?t ?s) (Scoer (dmap (lift ?dH2 0) ?Y0) (dmap (lift ?dH2 0) ?Y1) ?dH ?dZ) → _
|- _ ⇒ pose proof (Hx (coer_coer_env_lift dH2 H dZ2 Z dH t s Y0 Y1 dZ H1 H2)); clear Hx
| H1 : jcoer_env ?H ?Z ?Y0
, H2 : jcoer_env ?H ?Z ?Y1
, Hx : coer_coer_env ?H ?Z (Spair ?dH ?t ?s) (Scoer (?Y1 ++ ?Y0) nil ?dH ?dZ) → _
|- _ ⇒ pose proof (Hx (coer_coer_env_app H Z Y0 Y1 dH t s dZ H1 H2)); clear Hx
| H1 : jcoer_env ?H ?Z ?Y0
, H2 : jcoer_env ?H ?Z ?Y1
, Hx : coer_coer_env (?dH + ?H) (?dZ ++ dmap (lift ?dH 0) ?Z)
(Spair 0 ?t ?s) (Scoer (dmap (lift ?dH 0) ?Y1 ++ dmap (lift ?dH 0) ?Y0) nil 0 nil) → _
|- _ ⇒ pose proof (Hx (coer_coer_env_lift_app H Z Y0 Y1 dH dZ t s H1 H2)); clear Hx
| Hx : coer_left_type ?H ?Z ?t Stype → _
|- _ ⇒ pose proof (Hx (coer_left_type_type H Z t)); clear Hx
| H1 : extract Slisttype ?wits ?vecs
, Hx : coer_left_type ?H ?Z ?wits Slisttype → _
|- _ ⇒ pose proof (Hx (coer_left_type_listtype H Z vecs wits H1)); clear Hx
| H1 : extract Slistprodtype ?t12s ?dZ
, Hx : coer_left_type ?H ?Z ?t12s Slistprodtype → _
|- _ ⇒ pose proof (Hx (coer_left_type_listprodtype H Z dZ t12s H1)); clear Hx
| H1 : extract Slistprodtype ?t12s ?dZ
, H2 : extract Slisttype ?wits ?vecs
, H3 : jerasable 1 ?H ?Z ?wits Slisttype
, H4 : jerasable 1 (length ?vecs + ?H) (dmap (lift (length ?vecs) 0) ?Z) ?t12s Slistprodtype
, Hx : coer_left_type ?H ?Z (subst ?vecs 0 ?t12s) Slistcoer → _
|- _ ⇒ pose proof (Hx (coer_left_type_listcoer_subst H Z wits vecs H2 H3 dZ t12s H1 H4)); clear Hx
end].
Ltac inv_stuff := first [hyp_stuff|
match goal with
| H1 : coer_ext_env _ _ _ (Scoer _ _ _ _) |- _ ⇒ inversion H1; clear H1; subst
| H1 : coer_left_type _ _ _ (Scoer _ _ _ _) |- _ ⇒ inversion H1; clear H1; subst
| H1 : coer_left_type _ _ _ (Sprod _ _) |- _ ⇒ inversion H1; clear H1; subst
| H1 : coer_left_type _ _ (Scons _ _) (Slist _) |- _ ⇒ inversion H1; clear H1; subst
| H1 : coer_coer_env _ _ _ (Scoer _ _ _ _) |- _ ⇒ inversion H1; clear H1; subst
| H1 : coer_coer_env _ _ _ (Sprod _ _) |- _ ⇒ inversion H1; clear H1; subst
| H1 : coer_coer_env _ _ (Scons _ _) (Slist _) |- _ ⇒ inversion H1; clear H1; subst
end].
Ltac step := first [inv_stuff|
match goal with
| H1 : jerasable 1 _ _ (Arr _ _) _ |- _ ⇒ inversion H1; clear H1; subst
| H1 : jerasable 1 _ _ (Prod _ _) _ |- _ ⇒ inversion H1; clear H1; subst
| H1 : jerasable 1 ?H ?Z (Spair ?dH ?t ?s) (Scoer _ _ ?dH ?dZ)
|- jerasable 1 ?H ?Z ?s Stype ⇒ apply (jcoer_extract_right_type M11 H1)
| H1 : jerasable 1 ?H ?Z ?t Stype
|- jerasable 1 (?dH + ?H) (_ ++ dmap (lift ?dH 0) ?Z) (lift ?dH 0 ?t) Stype
⇒ apply jerasable_weak_coer_0
| H1 : jerasable 1 ?H ?Z ?t Stype
|- jerasable 1 (?dH + ?H) (dmap (lift ?dH 0) ?Z) (lift ?dH 0 ?t) Stype
⇒ apply jerasable_lift_0 with Stype
| Hx : coer_left_type ?H ?Z (Spair ?dH ?t ?s) (Scoer ?Y0 ?Y1 ?dH ?dZ) → _
|- _ ⇒ let H1 := fresh "H" in assert (coer_left_type H Z (Spair dH t s) (Scoer Y0 Y1 dH dZ)) as H1;
[clear Hx; apply CRcoer|pose proof (Hx H1); clear Hx]
end].
intros H Z t e HZte; induction_up_1 HZte; repeat (step; trysimpl; eauto).
apply nth_jerasable_env with t Y0 c; auto.
apply JTFor with dZ wits vecs; auto.
inversion H10; subst; apply H0;
[apply coer_coer_env_listcoer_subst with dZ|apply coer_left_type_listcoer_subst with insts dZ]; auto.
apply H1; repeat constructor; tryomega.
Qed.
Lemma jerasable_bind_up_1 : ∀ H Z dH dZ, jerasable_bind 0 H Z dH dZ →
jerasable_env 1 H Z → jerasable_bind 1 H Z dH dZ.
Proof.
intros H Z dH dZ [? [? [? [? ?]]]]; intros HZ.
∃ x; repeat split; auto; apply jerasable_up_1; auto.
apply JEcons with H Z dH nil; auto; apply jerasable_bind_only_type.
apply coer_coer_env_listprodtype with dZ; apply extract_inject.
apply coer_left_type_listprodtype with dZ; apply extract_inject.
apply coer_coer_env_listtype with x; apply extract_inject.
apply coer_left_type_listtype with x; apply extract_inject.
apply coer_coer_env_listcoer_subst with dZ; apply extract_inject.
apply coer_left_type_listcoer_subst with (inject Slisttype x) dZ; auto;
try apply extract_inject.
apply jerasable_up_1; auto.
apply coer_coer_env_listtype with x; apply extract_inject.
apply coer_left_type_listtype with x; apply extract_inject.
subst.
apply jerasable_up_1; auto.
apply JEcons with H Z (length x) nil; auto.
apply jerasable_bind_only_type.
apply coer_coer_env_listprodtype with dZ; apply extract_inject.
apply coer_left_type_listprodtype with dZ; apply extract_inject.
Qed.
Lemma jerasable_env_up_1 : ∀ H Z,
jerasable_env 0 H Z → jerasable_env 1 H Z.
Proof.
intros H Z HZ.
induction HZ; [apply JEnil|eapply JEcons]; eauto.
apply jerasable_bind_up_1; auto.
Qed.
Lemma jterm_env_up_1 : ∀ H Z G,
jterm_env 0 H Z G → jerasable_env 1 H Z → jterm_env 1 H Z G.
Proof.
intros H Z G [_ ?] ?.
split; auto.
eapply Forall_impl; [|apply H0].
unfold jtype; intros.
apply jerasable_up_1; auto.
apply coer_coer_env_type.
apply coer_left_type_type.
Qed.
Lemma jcoer_rebuild_jterm_env : ∀ H Z G dH dZ Y0 Y1 t s,
jerasable 0 H Z (Spair dH t s) (Scoer Y0 Y1 dH dZ) →
jterm_env 1 H Z G →
jterm_env 1 (dH + H) (dZ ++ dmap (lift dH 0) Z) (map (lift dH 0) G).
Proof.
split; destruct H1.
intros _.
apply jerasable_env_up_1; auto.
apply jcoer_extract_jerasable_env with Y0 Y1 t s; auto.
apply jerasable_env_down.
apply jerasable_env_up_2; auto.
eapply Forall_map_impl; [|apply H2].
unfold jtype; intros ? ?.
apply jerasable_weak_coer_0.
apply jerasable_lift_0 with Stype; auto.
Qed.
Lemma jterm_up_1 : ∀ H Z G a t, jterm 0 H Z G a t →
jterm_env 1 H Z G → jterm 1 H Z G a t.
Proof.
intros H Z G a t HZGat; jterm_induction HZGat; eauto; unfold jtype, jcoer in *;
repeat (match goal with
| H1 : 1 ≤ 0 → _ |- _ ⇒ clear H1
| |- _ ≤ _ → _ ⇒ intros _
end; eauto).
intros Heq; exfalso; omega.
apply IHHZGat.
destruct H1; split; auto.
constructor; auto.
apply jerasable_up_1; auto.
apply coer_coer_env_type.
apply coer_left_type_type.
destruct H2; apply jerasable_up_1; eauto.
apply CCcoer; constructor.
apply CRcoer.
apply @jterm_extract_jtype with (map (lift dH 0) G) a; auto.
apply IHHZGat.
apply jcoer_rebuild_jterm_env with nil nil t s; auto.
apply IHHZGat.
apply jcoer_rebuild_jterm_env with nil nil t s; auto.
Qed.
Print Assumptions jterm_down.
Print Assumptions jterm_up_2.
Print Assumptions jterm_up_1.