Library Fsoundness
Require Import Omega.
Require Import List.
Require Import Equality.
Require Import mxx.
Require Import minmax.
Require Import ext.
Require Import set.
Require Import list.
Require Import Flanguage.
Require Import Fnormalization.
Require Import Fsemantics.
Require Import Ftypesystem.
Require Import typesystem.
Definition Fake := Var_x 0 0. Fixpoint sem_type (h : list set) (t : type) {struct t} : set :=
match t with
| Var a ⇒ nth a h ETop
| Arr t s ⇒ EArr (sem_type h t) (sem_type h s)
| Prod t s ⇒ EProd (sem_type h t) (sem_type h s)
| For dH t12s t ⇒ Fsemantics.For (list set)
(fun dh ⇒ length dh = dH ∧ Forall CE dh ∧ sem_type (dh ++ h) t12s Fake)
(fun dh _ ⇒ sem_type (dh ++ h) t)
| Mu t ⇒ EMu (fun X ⇒ sem_type (X :: h) t)
| Bot ⇒ EBot
| Top ⇒ ETop
| Snil ⇒ fun _ ⇒ True
| Scons t ts ⇒ fun _ ⇒ sem_type h t Fake ∧ sem_type h ts Fake
| Spair d t1 t2 ⇒ fun _ ⇒ d = 0 ∧ Inc (sem_type h t1) (sem_type h t2)
end.
Lemma sem_type_lift : ∀ h dH dh, length dh = dH → ∀ t i di, length di = i →
sem_type (di ++ dh ++ h) (lift dH i t) = sem_type (di ++ h) t.
Proof.
induction t; intros i di dii; [|simpl..];
[repeat first [rewrite IHt|rewrite IHt1|rewrite IHt2]; auto..|].
simpl; subst.
destruct (le_gt_dec (length di) x).
rewrite 3 app_nth2; try omega.
f_equal; omega.
rewrite 2 app_nth1; try omega; reflexivity.
apply functional_extensionality; intros.
unfold Fsemantics.For.
apply forall_extensionality.
apply functional_extensionality; intros dh'.
match goal with | |- (?P → _) = (?Q → _) ⇒ assert (P = Q) end.
apply and_extensionality; intros.
replace (dh' ++ di ++ h) with ((dh' ++ di) ++ h) by (rewrite app_assoc; auto).
rewrite <- (IHt1 (d + i) (dh' ++ di)); [|rewrite app_length; omega].
rewrite <- app_assoc; reflexivity.
rewrite H0.
apply forall_extensionality.
apply functional_extensionality; intros [? [? ?]].
replace (dh' ++ di ++ h) with ((dh' ++ di) ++ h) by (rewrite app_assoc; auto).
rewrite <- (IHt2 (d + i) (dh' ++ di)); [|rewrite app_length; omega].
rewrite <- app_assoc; reflexivity.
f_equal.
apply functional_extensionality; intros R.
replace (R :: di ++ h) with ((R :: di) ++ h) by reflexivity.
rewrite <- (IHt (1 + i) (R :: di)); subst; simpl; reflexivity.
apply functional_extensionality; intros.
apply and_extensionality; intros.
rewrite IHt1; [|omega].
rewrite IHt2; [|omega].
reflexivity.
Qed.
Lemma sem_type_shift : ∀ h dH dh R t, length dh = dH →
sem_type (dh ++ R :: h) (shift dH t) = sem_type (dh ++ h) t.
Proof.
intros.
replace (R :: h) with ((R :: nil) ++ h) by reflexivity.
apply sem_type_lift; auto.
Qed.
Lemma sem_type_lift_0 : ∀ t h dH dh, length dh = dH →
sem_type (dh ++ h) (lift dH 0 t) = sem_type h t.
Proof.
intros t h dH dh dHh.
apply sem_type_lift with (di := nil) (i := 0); auto.
Qed.
Lemma sem_type_subst : ∀ h vecs t i dh, length dh = i →
sem_type (dh ++ h) (subst vecs i t) = sem_type (dh ++ map (sem_type h) vecs ++ h) t.
Proof.
induction t; intros i dh dhi; simpl;
[repeat first [rewrite IHt|rewrite IHt1|rewrite IHt2]..|]; auto.
subst_lift_var; subst.
rewrite 3 app_nth2; [rewrite map_length..| |]; try omega.
f_equal; omega.
rewrite app_nth2; auto.
rewrite app_nth1; [|rewrite map_length; omega].
replace ETop with (sem_type h Top) by reflexivity.
rewrite map_nth.
apply sem_type_lift_0; auto.
rewrite 2 app_nth1; auto; omega.
apply functional_extensionality; intros.
unfold Fsemantics.For.
apply forall_extensionality.
apply functional_extensionality; intros dh'.
match goal with | |- (?P → _) = (?Q → _) ⇒ assert (P = Q) end.
apply and_extensionality; intros.
replace (dh' ++ dh ++ h) with ((dh' ++ dh) ++ h) by (rewrite app_assoc; auto).
rewrite (IHt1 (d + i) (dh' ++ dh)); [|rewrite app_length; omega].
rewrite <- app_assoc; reflexivity.
rewrite H.
apply forall_extensionality.
apply functional_extensionality; intros [? [? ?]].
replace (dh' ++ dh ++ h) with ((dh' ++ dh) ++ h) by (rewrite app_assoc; auto).
rewrite (IHt2 (d + i) (dh' ++ dh)); [|rewrite app_length; omega].
rewrite <- app_assoc; reflexivity.
f_equal.
apply functional_extensionality; intros R.
replace (R :: dh ++ h) with ((R :: dh) ++ h) by reflexivity.
rewrite (IHt (S i) (R :: dh)); subst; simpl; reflexivity.
apply functional_extensionality; intros.
apply and_extensionality; intros.
rewrite IHt1; [|omega].
rewrite IHt2; [|omega].
reflexivity.
Qed.
Lemma sem_type_subst_0 : ∀ h vecs t,
sem_type h (subst vecs 0 t) = sem_type (map (sem_type h) vecs ++ h) t.
Proof. intros h vecs t; apply (sem_type_subst h vecs t 0 nil); auto. Qed.
Lemma sem_type_subst1_0 : ∀ h s t,
sem_type h (subst1 s 0 t) = sem_type (sem_type h s :: h) t.
Proof. intros h s t; apply (sem_type_subst h (s :: nil) t 0 nil); auto. Qed.
Definition sem_type_env h := Forall CE h.
Definition sem_coer_env h :=
Forall (fun ts ⇒ match ts with (t, s) ⇒ Inc (sem_type h t) (sem_type h s) end).
Definition sem_coer_env_k h k :=
Forall (fun ts ⇒ match ts with (t, s) ⇒
Inc (approx (sem_type h t) k) (approx (sem_type h s) k) end).
Definition sem_erasable_env h dH dZ dh :=
length dh = dH ∧ sem_type_env dh ∧ sem_coer_env (dh ++ h) dZ.
Definition sem_term_env h G := map (sem_type h) G.
Hint Unfold sem_type_env sem_coer_env sem_coer_env_k sem_erasable_env sem_term_env.
Lemma sem_coer_env_k_dec : ∀ Z h j k,
j ≤ k → sem_coer_env_k h k Z → sem_coer_env_k h j Z.
Proof.
induction Z; intros; auto.
destruct a as [t s].
inversion H0; clear H0; subst.
constructor; [|apply IHZ with k; auto].
intros a [aj Ha].
split; auto.
apply approx_unfold with k.
apply H3.
split; auto.
apply lt_term_le with j; auto; omega.
Qed.
Lemma sem_coer_env_to_k : ∀ Z h k,
sem_coer_env h Z → sem_coer_env_k h k Z.
Proof.
induction Z; intros; auto.
destruct a as [t s].
inversion H; clear H; subst.
constructor; [|apply IHZ; auto].
intros a [ak Ha]; auto.
Qed.
Lemma sem_coer_env_lift : ∀ Z h dH dh, length dh = dH →
sem_coer_env (dh ++ h) (dmap (lift dH 0) Z) = sem_coer_env h Z.
Proof.
intros; apply Forall_map; intros; destruct x; simpl.
rewrite 2 sem_type_lift_0; auto.
Qed.
Lemma sem_coer_env_k_lift : ∀ Z h k dH dh, length dh = dH →
sem_coer_env_k (dh ++ h) k (dmap (lift dH 0) Z) = sem_coer_env_k h k Z.
Proof.
intros; apply Forall_map; intros; destruct x; simpl.
rewrite 2 sem_type_lift_0; auto.
Qed.
Lemma sem_coer_env_shift : ∀ Z h R,
sem_coer_env (R :: h) (dmap (lift 1 0) Z) = sem_coer_env h Z.
Proof. intros; apply (sem_coer_env_lift Z h 1 (R :: nil)); auto. Qed.
Lemma sem_coer_env_app : ∀ h Z2 Z1,
sem_coer_env h (Z1 ++ Z2) ↔ (sem_coer_env h Z1 ∧ sem_coer_env h Z2).
Proof.
induction Z1; intros; simpl; split; first [intros [? ?]|intros]; auto;
destruct a; inversion H; subst.
split; [constructor; auto; apply IHZ1; auto|].
destruct (proj1 IHZ1); auto.
constructor; auto; apply IHZ1; auto.
Qed.
Lemma sem_coer_env_k_app : ∀ h k Z2 Z1,
sem_coer_env_k h k (Z1 ++ Z2) ↔ (sem_coer_env_k h k Z1 ∧ sem_coer_env_k h k Z2).
Proof.
induction Z1; intros; simpl; split; first [intros [? ?]|intros]; auto;
destruct a; inversion H; subst.
split; [constructor; auto; apply IHZ1; auto|].
destruct (proj1 IHZ1); auto.
constructor; auto; apply IHZ1; auto.
Qed.
Lemma sem_type2sem_coer_env : ∀ dZ t12s h,
extract Slistprodtype t12s dZ →
sem_type h t12s Fake →
sem_coer_env h dZ.
Proof.
induction dZ; intros; auto.
destruct a.
destruct_extract.
destruct H2 as [[_ ?] ?].
constructor; auto.
apply (IHdZ ts); auto.
Qed.
Lemma sem_coer_env2sem_type : ∀ dZ t12s h,
extract Slistprodtype t12s dZ →
sem_coer_env h dZ →
sem_type h t12s Fake.
Proof.
induction dZ; intros; destruct_extract; [exact I|].
destruct a; destruct_extract.
inversion H2; subst.
constructor; auto.
split; auto.
Qed.
Lemma sem_erasable_env_app : ∀ h dH2 dZ2 dh2 dH1 dZ1 dh1,
sem_erasable_env h dH2 dZ2 dh2 →
sem_erasable_env (dh2 ++ h) dH1 dZ1 dh1 →
sem_erasable_env h (dH1 + dH2) (dZ1 ++ dmap (lift dH1 0) dZ2) (dh1 ++ dh2).
Proof.
intros h dH2 dZ2 dh2 dH1 dZ1 dh1 [? [? ?]] [? [? ?]].
split; [|split].
rewrite app_length; auto.
apply Forall_app; auto.
rewrite <- app_assoc.
apply sem_coer_env_app; auto.
rewrite sem_coer_env_lift; auto.
Qed.
Lemma sem_erasable_env_lift : ∀ h' H Z dH dh h,
length dh = dH → Forall CE dh →
sem_erasable_env h' H Z h →
sem_erasable_env h' (dH + H) (dmap (lift dH 0) Z) (dh ++ h).
Proof.
intros; destruct H2 as [? [? ?]]; split; [|split].
rewrite app_length; auto.
apply Forall_app; auto.
rewrite <- app_assoc.
rewrite sem_coer_env_lift; auto.
Qed.
Definition swfsort wf :=
match wf with
| WF ⇒ 1
| NE ⇒ 0
end.
Definition swf dH t wf :=
∀ dh h, length dh = dH →
WFj (swfsort wf) (fun X ⇒ sem_type (dh ++ X :: h) t).
Hint Unfold swfsort swf.
Lemma jwf_sound : ∀ {a t wf}, jwf a t wf → swf a t wf.
Proof.
induction 1; intros dh h Hdh; simpl.
apply NE_id; intros R.
rewrite app_nth2 by omega.
replace (a - length dh) with 0 by omega.
reflexivity.
apply WFj_WF.
intros R k.
rewrite WF_EArr.
replace k with (0 + k) by (simpl; omega).
rewrite IHjwf1; auto.
rewrite IHjwf2; auto.
rewrite <- WF_EArr.
simpl; replace (k - 0) with k by omega.
reflexivity.
apply WFj_WF.
intros R k.
rewrite WF_EProd.
replace k with (0 + k) by omega.
rewrite IHjwf1; auto.
rewrite IHjwf2; auto.
rewrite <- WF_EProd.
simpl; replace (k - 0) with k by omega.
reflexivity.
subst t12s.
apply WFj_For with (Ix := list set)
(cond := fun dh0 ⇒ length dh0 = d ∧ Forall CE dh0 ∧ sem_type (dh0 ++ dh ++ h) s12s Fake)
(func := fun X dh0 _ ⇒ sem_type (dh0 ++ dh ++ X :: h) t).
intros dh0 [? [? ?]].
replace (fun X ⇒ sem_type (dh0 ++ dh ++ X :: h) t) with (fun X ⇒ sem_type ((dh0 ++ dh) ++ X :: h) t).
apply IHjwf; auto.
rewrite app_length; omega.
apply functional_extensionality; intros x.
rewrite app_assoc; reflexivity.
intros X.
apply functional_extensionality_dep; intros b.
apply forall_extensionality.
apply functional_extensionality_dep; intros dh0.
match goal with
| |- (?R → _) = (?S → _) ⇒ replace R with S; [reflexivity|]
end.
apply and_extensionality; intros.
repeat rewrite app_assoc.
rewrite sem_type_shift; auto.
rewrite app_length; auto.
apply WFj_Mu.
intros X.
apply WFj_WF.
apply (IHjwf1 nil (dh ++ X :: h)); auto.
intros Y.
pose proof (IHjwf2 (Y :: dh) h).
simpl in H1; auto.
subst t.
apply WF_CST; ∃ (sem_type (dh ++ h) s); intros R.
apply sem_type_shift; auto.
apply WFj_dec with (ij := 1); auto.
Qed.
Definition serasable_sem h := fix aux e t :=
match e with
| Stype ⇒ CE (sem_type h t)
| Sprod e1 e2 ⇒ ∃ t1 t2, extract Sprodtype t (t1, t2) ∧ aux e1 t1 ∧ aux e2 t2
| Slist e ⇒ ∃ ts, extract Slisttype t ts ∧ Forall (aux e) ts
| Scoer Y0 Y1 dH dZ ⇒ ∃ t1 t2, extract (Scoer Y0 Y1 dH dZ) t (t1, t2) ∧
(∃ dh, sem_erasable_env h dH dZ dh) ∧
(∀ k, sem_coer_env_k h k Y0 → sem_coer_env_k h (k - 1) Y1 →
∀ a, term_lt a k →
(∀ dh, sem_erasable_env h dH dZ dh → sem_type (dh ++ h) t1 a) →
sem_type h t2 a)
end.
Definition serasable H Z t e := ∀ h, sem_erasable_env nil H Z h → serasable_sem h e t.
Definition stype H Z t := serasable H Z t Stype.
Definition scoer H Z Y0 Y1 dH dZ t s := serasable H Z (Spair dH t s) (Scoer Y0 Y1 dH dZ).
Hint Unfold serasable_sem serasable stype scoer.
Lemma Forall_coer2sem_type : ∀ x h t12s,
Forall (serasable_sem h (Scoer nil nil 0 nil)) x →
extract Slisttype t12s x →
sem_type h t12s Fake.
Proof.
induction x; intros h t12s H1 H2; simpl.
destruct_extract; exact I.
destruct_extract.
inversion H1; clear H1; subst.
destruct H2 as [? [? [? [? ?]]]].
destruct_extract; simpl.
split; [split|]; auto.
intros a Ha.
destruct (term_lt_exists a) as [k ak].
apply H1 with k; auto.
intros dh [ldh [? ?]].
destruct dh; inversion ldh; subst; auto.
Qed.
Lemma serasable_sem2Forall_type : ∀ h vecs wits,
extract Slisttype wits vecs →
serasable_sem h (Slist Stype) wits →
Forall CE (map (sem_type h) vecs).
Proof.
induction vecs; intros; destruct_extract; constructor.
destruct H1 as [? [? ?]]; destruct_extract.
inversion H2; auto.
destruct H1 as [? [? ?]]; destruct_extract.
pose proof (extract_eq H0 H1); subst.
apply (IHvecs ts); auto.
inversion H2; subst.
∃ xs; auto.
Qed.
Lemma CVar_sound : ∀ c Z k t s h a,
term_lt a k →
nth c Z (Top, Top) = (t, s) →
sem_coer_env_k h k Z →
sem_type h t a →
sem_type h s a.
Proof.
induction c; intros.
destruct Z; simpl in H0; [inversion H0|]; subst; auto.
inversion H1; subst.
apply approx_unfold with k.
apply H4; auto.
destruct Z; simpl in H0; [inversion H0|]; subst; auto.
apply (IHc Z k t s); auto.
inversion H1; subst; auto.
Qed.
Lemma jerasable_sound : ∀ {H Z t e}, jerasable 2 H Z t e → serasable H Z t e.
Proof.
intros H Z t e HZte; induction HZte; intros h HZh; simpl.
generalize h H Z HZh; clear h H Z HZh; induction n; intros h H Z [? [? ?]];
(destruct H; destruct h; inversion H0; simpl; [apply CE_ETop|]);
inversion H1; subst; auto.
apply IHn with (H := length h) (Z := nil); repeat split; auto; omega.
apply CE_EArr.
apply C_CE; apply IHHZte1; auto.
apply C_CE; apply IHHZte2; auto.
apply CE_EProd.
apply C_CE; apply IHHZte1; auto.
apply C_CE; apply IHHZte2; auto.
apply CE_For.
∃ (map (sem_type h) vecs); repeat split.
rewrite map_length; auto.
destruct (IHHZte3 h HZh) as [? [? ?]].
pose proof (extract_eq H1 H3); subst x.
rewrite Forall_map with (h := serasable_sem h Stype); auto.
pose proof (IHHZte4 h HZh) as [? [? ?]].
rewrite <- sem_type_subst_0.
apply Forall_coer2sem_type with (x := x); auto.
destruct HZh as [? [? ?]].
intros i [? [? ?]].
apply IHHZte2.
split; [rewrite app_length; omega|].
split; [apply Forall_app; auto|].
rewrite app_nil_r in ×.
apply sem_coer_env_app; split.
apply sem_type2sem_coer_env with (t12s := t12s); auto.
rewrite sem_coer_env_lift; auto.
apply CE_EMu.
intros R CTR; destruct HZh as [? [? ?]]; apply IHHZte; split; [|split]; simpl; auto.
rewrite sem_coer_env_shift; auto.
destruct HZh as [Hh [? ?]].
apply WFj_WF.
apply (jwf_sound H0 nil h); auto.
apply CE_EBot.
apply CE_ETop.
∃ nil; split; constructor.
destruct (IHHZte2 h HZh) as [? [? ?]].
∃ (t :: x); split; repeat constructor; auto.
∃ t1, t2; repeat split; repeat constructor; auto.
∃ t, t; split; [repeat constructor|split; [∃ nil; auto|intros k HY0 HY1 a ak Ha]].
apply (Ha nil); auto.
∃ t1, t3; split; [repeat constructor|split; [|intros k HY0 HY1 a ak Ha]].
destruct (IHHZte2 h HZh) as [? [? [? [[dh2 ?] ?]]]].
destruct (IHHZte1 (dh2 ++ h)) as [? [? [? [[dh1 ?] ?]]]];
[apply sem_erasable_env_app; auto; rewrite app_nil_r; auto|].
∃ (dh1 ++ dh2).
apply sem_erasable_env_app; auto.
destruct (IHHZte2 h HZh) as [? [? [? [? ?]]]]; destruct_extract.
apply H2 with k; auto; intros dh2 dHh2.
destruct (IHHZte1 (dh2 ++ h)) as [? [? [? [? ?]]]]; destruct_extract.
apply sem_erasable_env_app; auto.
rewrite app_nil_r; auto.
apply H4 with k; auto.
destruct dHh2 as [? [? ?]]; rewrite sem_coer_env_k_lift; auto.
destruct dHh2 as [? [? ?]]; rewrite sem_coer_env_k_lift; auto.
intros dh1 dHh1; rewrite app_assoc.
apply Ha.
apply sem_erasable_env_app; auto.
∃ t, s; split; [repeat constructor|split; [∃ nil; auto|intros k HY0 HY1 a ak Ha]].
destruct (IHHZte h HZh) as [? [? [? [? ?]]]]; destruct_extract.
apply H4 with k; auto; intros dh [? [? ?]].
rewrite sem_type_lift_0; auto.
apply (Ha nil); auto.
destruct (IHHZte3 h HZh) as [? [? [? [Hexi ?]]]].
destruct_extract; rename x into s', x0 into s.
pose proof Hexi as [wdh wHdh].
∃ (Arr t' s'), (Arr t s); split; [repeat constructor|split; [∃ wdh; auto|]].
intros k HY0 HY1.
apply Cl_approx_For; auto.
intros dh Hdh;
match goal with
|- C (PArr (?x _ _) _) ⇒ replace x with sem_type by reflexivity
end.
apply C_PArr; apply C_CE; [apply (H1 M22)|apply (H3 M22)];
apply sem_erasable_env_app; auto; rewrite app_nil_r; auto.
intros a ak;
match goal with
|- _ → PArr (?x _ _) _ _ ⇒ replace x with sem_type by reflexivity
end; intros Ha.
destruct (Ha wdh wHdh) as [j [a' [Heq [Hok _]]]].
∃ j, a'; repeat split; auto.
intros Hj b Rb.
apply H5 with (k - 1).
apply sem_coer_env_k_app; split; auto.
apply sem_coer_env_k_dec with k; auto; omega.
constructor.
subst a; destruct ak.
apply unary_fuel_map_trivial.
intros.
destruct j; [inversion Hj|]; simpl.
rewrite <- minus_n_O.
apply le_trans with (S j).
minmax.
omega.
intros dh Hdh.
destruct (Ha dh Hdh) as [k2 [a2' [Heq2 [_ Hsub]]]].
rewrite Heq in Heq2; inversion Heq2; subst k2 a2'.
apply Hsub; auto; clear Hsub.
destruct (IHHZte2 (dh ++ h)) as [? [? [? [? ?]]]];
[apply sem_erasable_env_app; auto; rewrite app_nil_r; auto|].
destruct_extract; rename x0 into t'.
apply H7 with (k - 1).
destruct Hdh as [? [? ?]].
rewrite sem_coer_env_k_lift; auto.
apply sem_coer_env_k_app; split; auto.
apply sem_coer_env_k_dec with k; auto; omega.
constructor.
destruct ak.
apply unary_fuel_map_trivial.
intros.
destruct j; [inversion Hj|]; simpl.
rewrite <- minus_n_O.
apply le_trans with (S j).
minmax.
omega.
intros dh0 [d0h0 _]; destruct dh0; inversion d0h0; simpl.
destruct Hdh as [? [? ?]].
rewrite sem_type_lift_0; auto.
destruct (IHHZte1 h HZh) as [? [? [? [Hexi ?]]]].
pose proof Hexi as [wdh1 wHdh1].
destruct (IHHZte2 h HZh) as [? [? [? [[wdh2 wHdh2] ?]]]].
destruct_extract; rename x into t', x0 into t, x1 into s', x2 into s.
∃ (Prod t' s'), (Prod t s); split; [repeat constructor|split; [∃ wdh1; auto|]].
intros k HY0 HY1.
apply Cl_approx_For; auto.
intros dh Hdh;
match goal with
|- C (PProd (?x _ _) _) ⇒ replace x with sem_type by reflexivity
end.
apply C_PProd; apply C_CE; [apply (H1 M22)|apply (H3 M22)];
apply sem_erasable_env_app; auto; rewrite app_nil_r; auto.
intros a ak;
match goal with
|- _ → PProd (?x _ _) _ _ ⇒ replace x with sem_type by reflexivity
end; intros Ha.
destruct (Ha wdh1 wHdh1) as [j [a' [b' [Heq [[Hoka Hokb] _]]]]].
∃ j, a', b'; repeat split; auto; rename H4 into Hj.
apply H5 with (k - 1).
apply sem_coer_env_k_app; split; auto.
apply sem_coer_env_k_dec with k; auto; omega.
constructor.
subst a; destruct ak.
apply unary_fuel_map_trivial.
intros.
destruct j; [inversion Hj|]; simpl.
rewrite <- minus_n_O.
apply le_trans with (S j).
minmax.
omega.
intros dh Hdh.
destruct (Ha dh Hdh) as [k2 [a2' [b2' [Heq2 [_ Hproj]]]]].
rewrite Heq in Heq2; inversion Heq2; subst k2 a2'.
apply Hproj; auto.
apply H7 with (k - 1).
apply sem_coer_env_k_app; split; auto.
apply sem_coer_env_k_dec with k; auto; omega.
constructor.
subst a; destruct ak.
apply unary_fuel_map_trivial.
intros.
destruct j; [inversion Hj|]; simpl.
rewrite <- minus_n_O.
apply le_trans with (S j).
minmax.
omega.
intros dh Hdh.
destruct (Ha dh Hdh) as [k2 [a2' [b2' [Heq2 [_ Hproj]]]]].
rewrite Heq in Heq2; inversion Heq2; subst k2 a2'.
apply Hproj; auto.
∃ t, s; split; [repeat constructor|split; [∃ nil; auto|intros k HY0 HY1 a ak Ha]].
assert (sem_type h t a) by (apply (Ha nil); auto); clear Ha.
apply CVar_sound with (c := c) (k := k) (Z := Y0 ++ Z) (t := t); auto.
apply sem_coer_env_k_app; split; auto.
destruct HZh as [_ [_ ?]]; rewrite app_nil_r in H6.
apply sem_coer_env_to_k; auto.
∃ t, (For dH t12s t); split; [repeat constructor|split; [|intros k HY0 HY1 a ak Ha]].
∃ (map (sem_type h) vecs).
split; [|split].
rewrite map_length; auto.
apply serasable_sem2Forall_type with (wits := wits); auto.
apply sem_type2sem_coer_env with (t12s := t12s); auto.
pose proof (IHHZte3 h HZh) as [? [? ?]].
rewrite <- sem_type_subst_0.
apply Forall_coer2sem_type with (x := x); auto.
intros dh [? [? ?]].
match goal with
| |- ?R _ _ _ ⇒
replace R with sem_type in × by reflexivity
end.
apply Ha.
split; [|split]; auto.
apply sem_type2sem_coer_env with (t12s := t12s); auto.
∃ (For dH t12s t), (subst vecs 0 t);
split; [repeat constructor|split; [∃ nil; auto|intros k HY0 HY1 a ak Ha]].
assert (sem_erasable_env h 0 nil nil) as nil0 by auto.
pose proof (Ha nil nil0) as Ha0; simpl app in Ha0.
rewrite sem_type_subst_0.
apply Ha0; split; [|split].
rewrite map_length; auto.
apply serasable_sem2Forall_type with (wits := insts); auto.
match goal with
| |- ?R _ _ _ ⇒
replace R with sem_type in × by reflexivity
end.
pose proof (IHHZte2 h HZh) as [? [? ?]].
rewrite <- sem_type_subst_0.
apply Forall_coer2sem_type with (x := x); auto.
∃ (Mu t), (subst1 (Mu t) 0 t);
split; [repeat constructor|split; [∃ nil; auto|intros k HY0 HY1 a ak Ha]].
unfold subst1; rewrite sem_type_subst_0; simpl.
assert (sem_erasable_env h 0 nil nil) as nil0 by auto.
pose proof (Ha nil nil0) as Ha0; simpl in Ha0.
pose proof (H0 M12).
inversion H3; clear H3; subst.
pose proof (jwf_sound H6 nil h).
simpl in H3.
remember (fun X ⇒ sem_type (X :: h) t) as F.
replace (sem_type (EMu F :: h) t) with (F (EMu F)) by (subst F; reflexivity).
destruct HZh as [? [? ?]].
apply (Mu_unfold F); auto.
apply WFj_WF; auto.
∃ (subst1 (Mu t) 0 t), (Mu t);
split; [repeat constructor|split; [∃ nil; auto|intros k HY0 HY1 a ak Ha]].
assert (sem_erasable_env h 0 nil nil) as nil0 by auto.
pose proof (Ha nil nil0) as Ha0.
unfold subst1 in Ha0; rewrite sem_type_subst_0 in Ha0; simpl in Ha0.
inversion HZte; subst.
pose proof (jwf_sound H2 nil h).
simpl in H0.
simpl; remember (fun X ⇒ sem_type (X :: h) t) as F.
replace (sem_type (EMu F :: h) t) with (F (EMu F)) in Ha0 by (subst F; reflexivity).
destruct HZh as [? [? ?]].
apply (Mu_fold F); auto.
apply WFj_WF; auto.
∃ t, s; split; [repeat constructor|split; [∃ nil; auto|]].
induction k; intros HY0 HY1 a ak Ha; [exfalso; apply term_lt_0 with a; auto|].
simpl in *; rewrite <- minus_n_O in ×.
destruct (IHHZte h HZh) as [? [? [? [? ?]]]]; destruct_extract.
rename x into t, x0 into s.
apply H4 with (S k); auto.
simpl; rewrite <- minus_n_O; constructor; auto.
clear a ak Ha; intros a [ak Ha]; split; auto.
apply IHk; auto.
apply sem_coer_env_k_dec with (S k); auto; omega.
apply sem_coer_env_k_dec with k; auto; omega.
intros dh0 [d0h0 _]; destruct dh0; inversion d0h0; simpl; auto.
∃ Bot, t; split; [repeat constructor|split; [∃ nil; auto|intros k HY0 HY1 a ak Ha]].
apply (Ha nil); auto.
apply IHHZte; auto.
∃ t, Top; split; [repeat constructor|split; [∃ nil; auto|intros k HY0 HY1 a ak Ha]].
apply fold_Cl; left.
∃ (sem_type h t); split; [apply (H1 M12)|apply (Ha nil)]; auto.
Qed.
Lemma jtype_sound : ∀ {H Z t}, jtype 2 H Z t → stype H Z t.
Proof. intros; apply jerasable_sound; auto. Qed.
Lemma jcoer_sound : ∀ {H Z Y0 Y1 dH dZ t s},
jcoer 2 H Z Y0 Y1 dH dZ t s → scoer H Z Y0 Y1 dH dZ t s.
Proof. intros; apply jerasable_sound; auto. Qed.
Definition sterm_env H Z G :=
∀ h, sem_erasable_env nil H Z h → Forall CE (sem_term_env h G).
Hint Unfold sterm_env.
Definition sterm H Z G a t :=
∀ h, sem_erasable_env nil H Z h → EJudg (sem_term_env h G) (sem_type h t) a.
Hint Unfold sterm.
Lemma jterm_env_sound : ∀ {H Z G}, jterm_env 2 H Z G → sterm_env H Z G.
Proof.
intros H Z G [_ HZG]; induction G; inversion HZG; clear HZG; subst; constructor.
apply (jtype_sound H2 h H0).
apply (IHG H3 h H0).
Qed.
Lemma sem_term_env_lift : ∀ G h dH dh, length dh = dH →
sem_term_env (dh ++ h) (map (lift dH 0) G) = sem_term_env h G.
Proof.
induction G; intros h dH dh dHh; simpl; auto.
rewrite sem_type_lift_0; auto.
rewrite IHG; auto.
Qed.
Definition serasable_env H Z := ∃ h, sem_erasable_env nil H Z h.
Lemma jerasable_env_sound : ∀ {H Z},
jerasable_env 2 H Z → serasable_env H Z.
Proof.
intros H Z jenv.
induction jenv; [∃ nil; repeat split; auto|].
destruct H0 as [xs [? [? [? ?]]]].
destruct IHjenv as [h [? [? ?]]].
∃ (map (sem_type h) xs ++ h).
subst dHH dZZ.
repeat split.
rewrite app_length; rewrite map_length; auto.
apply Forall_app.
split; auto.
pose proof (extract_inject Slisttype xs).
apply serasable_sem2Forall_type with (wits := (inject Slisttype xs)); auto.
apply (jerasable_sound H4 h); auto.
rewrite app_nil_r.
apply sem_coer_env_app.
split.
pose proof (extract_inject Slistprodtype dZ).
pose proof (jerasable_sound H5 h) as [? [? ?]]; auto.
apply sem_type2sem_coer_env with (t12s := inject Slistprodtype dZ); auto.
rewrite <- sem_type_subst_0.
apply Forall_coer2sem_type with (x := x); auto.
rewrite app_nil_r in H8.
rewrite sem_coer_env_lift; auto.
rewrite map_length; auto.
Qed.
Lemma nth_sem : ∀ x G t h, nth x G Top = t →
nth x (sem_term_env h G) ETop = sem_type h t.
Proof. induction x; intros G t h Gx; destruct G as [|s G]; simpl in *; subst; auto. Qed.
Lemma jterm_sound : ∀ {H Z G a t}, jterm 2 H Z G a t → sterm H Z G a t.
Proof.
intros H Z G a t HZGat; induction HZGat; intros h Hh; simpl.
apply EVar_sem; [|apply nth_sem]; auto.
apply (Forall_impl _ (@C_CE) ((jterm_env_sound (H0 M12)) h Hh)).
pose proof (jterm_extract_jterm_env M12 HZGat) as [_ ?].
inversion H1; subst.
pose proof (jtype_sound H4) as HZt.
pose proof (jtype_sound (jterm_extract_jtype M12 HZGat)) as HZs.
apply ELam_sem; [apply CEexp; apply HZt|apply (C_CE (HZs h Hh))|]; auto.
apply IHHZGat; auto.
pose proof (jterm_extract_jtype M12 HZGat1) as Hts.
inversion Hts; subst.
pose proof (C_CE (jtype_sound H5 h Hh)).
pose proof (jtype_sound H6 h Hh).
apply EApp_sem with (R := sem_type h t); auto.
apply IHHZGat1; auto.
pose proof (C_CE (jtype_sound (jterm_extract_jtype M12 HZGat1) h Hh)).
pose proof (C_CE (jtype_sound (jterm_extract_jtype M12 HZGat2) h Hh)).
apply EPair_sem; auto.
pose proof (jterm_extract_jtype M12 HZGat) as Hts.
inversion Hts; subst.
pose proof (jtype_sound H5 h Hh).
pose proof (C_CE (jtype_sound H6 h Hh)).
apply EFst_sem with (S := sem_type h s); auto.
apply IHHZGat; auto.
pose proof (jterm_extract_jtype M12 HZGat) as Hts.
inversion Hts; subst.
pose proof (C_CE (jtype_sound H5 h Hh)).
pose proof (jtype_sound H6 h Hh).
apply ESnd_sem with (R := sem_type h t); auto.
apply IHHZGat; auto.
pose proof (jtype_sound (jterm_extract_jtype M12 HZGat)).
pose proof (jcoer_sound H1 h Hh) as [? [? [? [? ?]]]].
assert (sterm_env (dH + H) (dZ ++ dmap (lift dH 0) Z) (map (lift dH 0) G)).
intros dhh [? [? ?]].
destruct (cut_length _ _ _ _ H6) as [dh [h' [? [? ?]]]]; subst dhh; clear H6.
rewrite sem_term_env_lift; auto.
apply (jterm_env_sound (H0 M12)).
apply Forall_app in H7 as [? ?].
repeat split; auto.
rewrite app_nil_r in ×.
apply sem_coer_env_app in H8 as [? ?].
rewrite <- sem_coer_env_lift with (dH := dH) (dh := dh); auto.
apply ECoer_sem with (R := sem_type h (For dH (inject Slistprodtype dZ) t)); auto;
destruct_extract; rename x into t, x0 into s.
intros b Hb.
destruct (term_lt_exists b) as [k bk].
apply H5 with k; try constructor; auto.
intros dh [? [? ?]].
apply Hb; split; [|split]; auto.
match goal with
| |- ?R _ _ _ ⇒ replace R with sem_type by reflexivity
end.
apply sem_coer_env2sem_type with (dZ := dZ); auto.
apply (extract_inject Slistprodtype).
apply Edistrib;
match goal with
| |- context[?R _ _ _] ⇒ replace R with sem_type by reflexivity
end.
destruct H4 as [wdh [? [? ?]]].
∃ wdh; repeat split; auto.
apply sem_coer_env2sem_type with (dZ := dZ); auto.
apply extract_inject.
intros dh [? [? ?]]; apply H2.
apply sem_erasable_env_app; auto; rewrite app_nil_r; auto.
repeat split; auto.
apply sem_type2sem_coer_env with (t12s := inject Slistprodtype dZ); auto.
apply extract_inject.
intros dh [? [? ?]].
rewrite <- sem_term_env_lift with (dH := dH) (dh := dh); auto.
apply IHHZGat.
apply sem_erasable_env_app; auto.
rewrite app_nil_r; auto.
repeat split; auto.
apply sem_type2sem_coer_env with (t12s := inject Slistprodtype dZ); auto.
apply (extract_inject Slistprodtype).
Qed.
Require Import List.
Require Import Equality.
Require Import mxx.
Require Import minmax.
Require Import ext.
Require Import set.
Require Import list.
Require Import Flanguage.
Require Import Fnormalization.
Require Import Fsemantics.
Require Import Ftypesystem.
Require Import typesystem.
Definition Fake := Var_x 0 0. Fixpoint sem_type (h : list set) (t : type) {struct t} : set :=
match t with
| Var a ⇒ nth a h ETop
| Arr t s ⇒ EArr (sem_type h t) (sem_type h s)
| Prod t s ⇒ EProd (sem_type h t) (sem_type h s)
| For dH t12s t ⇒ Fsemantics.For (list set)
(fun dh ⇒ length dh = dH ∧ Forall CE dh ∧ sem_type (dh ++ h) t12s Fake)
(fun dh _ ⇒ sem_type (dh ++ h) t)
| Mu t ⇒ EMu (fun X ⇒ sem_type (X :: h) t)
| Bot ⇒ EBot
| Top ⇒ ETop
| Snil ⇒ fun _ ⇒ True
| Scons t ts ⇒ fun _ ⇒ sem_type h t Fake ∧ sem_type h ts Fake
| Spair d t1 t2 ⇒ fun _ ⇒ d = 0 ∧ Inc (sem_type h t1) (sem_type h t2)
end.
Lemma sem_type_lift : ∀ h dH dh, length dh = dH → ∀ t i di, length di = i →
sem_type (di ++ dh ++ h) (lift dH i t) = sem_type (di ++ h) t.
Proof.
induction t; intros i di dii; [|simpl..];
[repeat first [rewrite IHt|rewrite IHt1|rewrite IHt2]; auto..|].
simpl; subst.
destruct (le_gt_dec (length di) x).
rewrite 3 app_nth2; try omega.
f_equal; omega.
rewrite 2 app_nth1; try omega; reflexivity.
apply functional_extensionality; intros.
unfold Fsemantics.For.
apply forall_extensionality.
apply functional_extensionality; intros dh'.
match goal with | |- (?P → _) = (?Q → _) ⇒ assert (P = Q) end.
apply and_extensionality; intros.
replace (dh' ++ di ++ h) with ((dh' ++ di) ++ h) by (rewrite app_assoc; auto).
rewrite <- (IHt1 (d + i) (dh' ++ di)); [|rewrite app_length; omega].
rewrite <- app_assoc; reflexivity.
rewrite H0.
apply forall_extensionality.
apply functional_extensionality; intros [? [? ?]].
replace (dh' ++ di ++ h) with ((dh' ++ di) ++ h) by (rewrite app_assoc; auto).
rewrite <- (IHt2 (d + i) (dh' ++ di)); [|rewrite app_length; omega].
rewrite <- app_assoc; reflexivity.
f_equal.
apply functional_extensionality; intros R.
replace (R :: di ++ h) with ((R :: di) ++ h) by reflexivity.
rewrite <- (IHt (1 + i) (R :: di)); subst; simpl; reflexivity.
apply functional_extensionality; intros.
apply and_extensionality; intros.
rewrite IHt1; [|omega].
rewrite IHt2; [|omega].
reflexivity.
Qed.
Lemma sem_type_shift : ∀ h dH dh R t, length dh = dH →
sem_type (dh ++ R :: h) (shift dH t) = sem_type (dh ++ h) t.
Proof.
intros.
replace (R :: h) with ((R :: nil) ++ h) by reflexivity.
apply sem_type_lift; auto.
Qed.
Lemma sem_type_lift_0 : ∀ t h dH dh, length dh = dH →
sem_type (dh ++ h) (lift dH 0 t) = sem_type h t.
Proof.
intros t h dH dh dHh.
apply sem_type_lift with (di := nil) (i := 0); auto.
Qed.
Lemma sem_type_subst : ∀ h vecs t i dh, length dh = i →
sem_type (dh ++ h) (subst vecs i t) = sem_type (dh ++ map (sem_type h) vecs ++ h) t.
Proof.
induction t; intros i dh dhi; simpl;
[repeat first [rewrite IHt|rewrite IHt1|rewrite IHt2]..|]; auto.
subst_lift_var; subst.
rewrite 3 app_nth2; [rewrite map_length..| |]; try omega.
f_equal; omega.
rewrite app_nth2; auto.
rewrite app_nth1; [|rewrite map_length; omega].
replace ETop with (sem_type h Top) by reflexivity.
rewrite map_nth.
apply sem_type_lift_0; auto.
rewrite 2 app_nth1; auto; omega.
apply functional_extensionality; intros.
unfold Fsemantics.For.
apply forall_extensionality.
apply functional_extensionality; intros dh'.
match goal with | |- (?P → _) = (?Q → _) ⇒ assert (P = Q) end.
apply and_extensionality; intros.
replace (dh' ++ dh ++ h) with ((dh' ++ dh) ++ h) by (rewrite app_assoc; auto).
rewrite (IHt1 (d + i) (dh' ++ dh)); [|rewrite app_length; omega].
rewrite <- app_assoc; reflexivity.
rewrite H.
apply forall_extensionality.
apply functional_extensionality; intros [? [? ?]].
replace (dh' ++ dh ++ h) with ((dh' ++ dh) ++ h) by (rewrite app_assoc; auto).
rewrite (IHt2 (d + i) (dh' ++ dh)); [|rewrite app_length; omega].
rewrite <- app_assoc; reflexivity.
f_equal.
apply functional_extensionality; intros R.
replace (R :: dh ++ h) with ((R :: dh) ++ h) by reflexivity.
rewrite (IHt (S i) (R :: dh)); subst; simpl; reflexivity.
apply functional_extensionality; intros.
apply and_extensionality; intros.
rewrite IHt1; [|omega].
rewrite IHt2; [|omega].
reflexivity.
Qed.
Lemma sem_type_subst_0 : ∀ h vecs t,
sem_type h (subst vecs 0 t) = sem_type (map (sem_type h) vecs ++ h) t.
Proof. intros h vecs t; apply (sem_type_subst h vecs t 0 nil); auto. Qed.
Lemma sem_type_subst1_0 : ∀ h s t,
sem_type h (subst1 s 0 t) = sem_type (sem_type h s :: h) t.
Proof. intros h s t; apply (sem_type_subst h (s :: nil) t 0 nil); auto. Qed.
Definition sem_type_env h := Forall CE h.
Definition sem_coer_env h :=
Forall (fun ts ⇒ match ts with (t, s) ⇒ Inc (sem_type h t) (sem_type h s) end).
Definition sem_coer_env_k h k :=
Forall (fun ts ⇒ match ts with (t, s) ⇒
Inc (approx (sem_type h t) k) (approx (sem_type h s) k) end).
Definition sem_erasable_env h dH dZ dh :=
length dh = dH ∧ sem_type_env dh ∧ sem_coer_env (dh ++ h) dZ.
Definition sem_term_env h G := map (sem_type h) G.
Hint Unfold sem_type_env sem_coer_env sem_coer_env_k sem_erasable_env sem_term_env.
Lemma sem_coer_env_k_dec : ∀ Z h j k,
j ≤ k → sem_coer_env_k h k Z → sem_coer_env_k h j Z.
Proof.
induction Z; intros; auto.
destruct a as [t s].
inversion H0; clear H0; subst.
constructor; [|apply IHZ with k; auto].
intros a [aj Ha].
split; auto.
apply approx_unfold with k.
apply H3.
split; auto.
apply lt_term_le with j; auto; omega.
Qed.
Lemma sem_coer_env_to_k : ∀ Z h k,
sem_coer_env h Z → sem_coer_env_k h k Z.
Proof.
induction Z; intros; auto.
destruct a as [t s].
inversion H; clear H; subst.
constructor; [|apply IHZ; auto].
intros a [ak Ha]; auto.
Qed.
Lemma sem_coer_env_lift : ∀ Z h dH dh, length dh = dH →
sem_coer_env (dh ++ h) (dmap (lift dH 0) Z) = sem_coer_env h Z.
Proof.
intros; apply Forall_map; intros; destruct x; simpl.
rewrite 2 sem_type_lift_0; auto.
Qed.
Lemma sem_coer_env_k_lift : ∀ Z h k dH dh, length dh = dH →
sem_coer_env_k (dh ++ h) k (dmap (lift dH 0) Z) = sem_coer_env_k h k Z.
Proof.
intros; apply Forall_map; intros; destruct x; simpl.
rewrite 2 sem_type_lift_0; auto.
Qed.
Lemma sem_coer_env_shift : ∀ Z h R,
sem_coer_env (R :: h) (dmap (lift 1 0) Z) = sem_coer_env h Z.
Proof. intros; apply (sem_coer_env_lift Z h 1 (R :: nil)); auto. Qed.
Lemma sem_coer_env_app : ∀ h Z2 Z1,
sem_coer_env h (Z1 ++ Z2) ↔ (sem_coer_env h Z1 ∧ sem_coer_env h Z2).
Proof.
induction Z1; intros; simpl; split; first [intros [? ?]|intros]; auto;
destruct a; inversion H; subst.
split; [constructor; auto; apply IHZ1; auto|].
destruct (proj1 IHZ1); auto.
constructor; auto; apply IHZ1; auto.
Qed.
Lemma sem_coer_env_k_app : ∀ h k Z2 Z1,
sem_coer_env_k h k (Z1 ++ Z2) ↔ (sem_coer_env_k h k Z1 ∧ sem_coer_env_k h k Z2).
Proof.
induction Z1; intros; simpl; split; first [intros [? ?]|intros]; auto;
destruct a; inversion H; subst.
split; [constructor; auto; apply IHZ1; auto|].
destruct (proj1 IHZ1); auto.
constructor; auto; apply IHZ1; auto.
Qed.
Lemma sem_type2sem_coer_env : ∀ dZ t12s h,
extract Slistprodtype t12s dZ →
sem_type h t12s Fake →
sem_coer_env h dZ.
Proof.
induction dZ; intros; auto.
destruct a.
destruct_extract.
destruct H2 as [[_ ?] ?].
constructor; auto.
apply (IHdZ ts); auto.
Qed.
Lemma sem_coer_env2sem_type : ∀ dZ t12s h,
extract Slistprodtype t12s dZ →
sem_coer_env h dZ →
sem_type h t12s Fake.
Proof.
induction dZ; intros; destruct_extract; [exact I|].
destruct a; destruct_extract.
inversion H2; subst.
constructor; auto.
split; auto.
Qed.
Lemma sem_erasable_env_app : ∀ h dH2 dZ2 dh2 dH1 dZ1 dh1,
sem_erasable_env h dH2 dZ2 dh2 →
sem_erasable_env (dh2 ++ h) dH1 dZ1 dh1 →
sem_erasable_env h (dH1 + dH2) (dZ1 ++ dmap (lift dH1 0) dZ2) (dh1 ++ dh2).
Proof.
intros h dH2 dZ2 dh2 dH1 dZ1 dh1 [? [? ?]] [? [? ?]].
split; [|split].
rewrite app_length; auto.
apply Forall_app; auto.
rewrite <- app_assoc.
apply sem_coer_env_app; auto.
rewrite sem_coer_env_lift; auto.
Qed.
Lemma sem_erasable_env_lift : ∀ h' H Z dH dh h,
length dh = dH → Forall CE dh →
sem_erasable_env h' H Z h →
sem_erasable_env h' (dH + H) (dmap (lift dH 0) Z) (dh ++ h).
Proof.
intros; destruct H2 as [? [? ?]]; split; [|split].
rewrite app_length; auto.
apply Forall_app; auto.
rewrite <- app_assoc.
rewrite sem_coer_env_lift; auto.
Qed.
Definition swfsort wf :=
match wf with
| WF ⇒ 1
| NE ⇒ 0
end.
Definition swf dH t wf :=
∀ dh h, length dh = dH →
WFj (swfsort wf) (fun X ⇒ sem_type (dh ++ X :: h) t).
Hint Unfold swfsort swf.
Lemma jwf_sound : ∀ {a t wf}, jwf a t wf → swf a t wf.
Proof.
induction 1; intros dh h Hdh; simpl.
apply NE_id; intros R.
rewrite app_nth2 by omega.
replace (a - length dh) with 0 by omega.
reflexivity.
apply WFj_WF.
intros R k.
rewrite WF_EArr.
replace k with (0 + k) by (simpl; omega).
rewrite IHjwf1; auto.
rewrite IHjwf2; auto.
rewrite <- WF_EArr.
simpl; replace (k - 0) with k by omega.
reflexivity.
apply WFj_WF.
intros R k.
rewrite WF_EProd.
replace k with (0 + k) by omega.
rewrite IHjwf1; auto.
rewrite IHjwf2; auto.
rewrite <- WF_EProd.
simpl; replace (k - 0) with k by omega.
reflexivity.
subst t12s.
apply WFj_For with (Ix := list set)
(cond := fun dh0 ⇒ length dh0 = d ∧ Forall CE dh0 ∧ sem_type (dh0 ++ dh ++ h) s12s Fake)
(func := fun X dh0 _ ⇒ sem_type (dh0 ++ dh ++ X :: h) t).
intros dh0 [? [? ?]].
replace (fun X ⇒ sem_type (dh0 ++ dh ++ X :: h) t) with (fun X ⇒ sem_type ((dh0 ++ dh) ++ X :: h) t).
apply IHjwf; auto.
rewrite app_length; omega.
apply functional_extensionality; intros x.
rewrite app_assoc; reflexivity.
intros X.
apply functional_extensionality_dep; intros b.
apply forall_extensionality.
apply functional_extensionality_dep; intros dh0.
match goal with
| |- (?R → _) = (?S → _) ⇒ replace R with S; [reflexivity|]
end.
apply and_extensionality; intros.
repeat rewrite app_assoc.
rewrite sem_type_shift; auto.
rewrite app_length; auto.
apply WFj_Mu.
intros X.
apply WFj_WF.
apply (IHjwf1 nil (dh ++ X :: h)); auto.
intros Y.
pose proof (IHjwf2 (Y :: dh) h).
simpl in H1; auto.
subst t.
apply WF_CST; ∃ (sem_type (dh ++ h) s); intros R.
apply sem_type_shift; auto.
apply WFj_dec with (ij := 1); auto.
Qed.
Definition serasable_sem h := fix aux e t :=
match e with
| Stype ⇒ CE (sem_type h t)
| Sprod e1 e2 ⇒ ∃ t1 t2, extract Sprodtype t (t1, t2) ∧ aux e1 t1 ∧ aux e2 t2
| Slist e ⇒ ∃ ts, extract Slisttype t ts ∧ Forall (aux e) ts
| Scoer Y0 Y1 dH dZ ⇒ ∃ t1 t2, extract (Scoer Y0 Y1 dH dZ) t (t1, t2) ∧
(∃ dh, sem_erasable_env h dH dZ dh) ∧
(∀ k, sem_coer_env_k h k Y0 → sem_coer_env_k h (k - 1) Y1 →
∀ a, term_lt a k →
(∀ dh, sem_erasable_env h dH dZ dh → sem_type (dh ++ h) t1 a) →
sem_type h t2 a)
end.
Definition serasable H Z t e := ∀ h, sem_erasable_env nil H Z h → serasable_sem h e t.
Definition stype H Z t := serasable H Z t Stype.
Definition scoer H Z Y0 Y1 dH dZ t s := serasable H Z (Spair dH t s) (Scoer Y0 Y1 dH dZ).
Hint Unfold serasable_sem serasable stype scoer.
Lemma Forall_coer2sem_type : ∀ x h t12s,
Forall (serasable_sem h (Scoer nil nil 0 nil)) x →
extract Slisttype t12s x →
sem_type h t12s Fake.
Proof.
induction x; intros h t12s H1 H2; simpl.
destruct_extract; exact I.
destruct_extract.
inversion H1; clear H1; subst.
destruct H2 as [? [? [? [? ?]]]].
destruct_extract; simpl.
split; [split|]; auto.
intros a Ha.
destruct (term_lt_exists a) as [k ak].
apply H1 with k; auto.
intros dh [ldh [? ?]].
destruct dh; inversion ldh; subst; auto.
Qed.
Lemma serasable_sem2Forall_type : ∀ h vecs wits,
extract Slisttype wits vecs →
serasable_sem h (Slist Stype) wits →
Forall CE (map (sem_type h) vecs).
Proof.
induction vecs; intros; destruct_extract; constructor.
destruct H1 as [? [? ?]]; destruct_extract.
inversion H2; auto.
destruct H1 as [? [? ?]]; destruct_extract.
pose proof (extract_eq H0 H1); subst.
apply (IHvecs ts); auto.
inversion H2; subst.
∃ xs; auto.
Qed.
Lemma CVar_sound : ∀ c Z k t s h a,
term_lt a k →
nth c Z (Top, Top) = (t, s) →
sem_coer_env_k h k Z →
sem_type h t a →
sem_type h s a.
Proof.
induction c; intros.
destruct Z; simpl in H0; [inversion H0|]; subst; auto.
inversion H1; subst.
apply approx_unfold with k.
apply H4; auto.
destruct Z; simpl in H0; [inversion H0|]; subst; auto.
apply (IHc Z k t s); auto.
inversion H1; subst; auto.
Qed.
Lemma jerasable_sound : ∀ {H Z t e}, jerasable 2 H Z t e → serasable H Z t e.
Proof.
intros H Z t e HZte; induction HZte; intros h HZh; simpl.
generalize h H Z HZh; clear h H Z HZh; induction n; intros h H Z [? [? ?]];
(destruct H; destruct h; inversion H0; simpl; [apply CE_ETop|]);
inversion H1; subst; auto.
apply IHn with (H := length h) (Z := nil); repeat split; auto; omega.
apply CE_EArr.
apply C_CE; apply IHHZte1; auto.
apply C_CE; apply IHHZte2; auto.
apply CE_EProd.
apply C_CE; apply IHHZte1; auto.
apply C_CE; apply IHHZte2; auto.
apply CE_For.
∃ (map (sem_type h) vecs); repeat split.
rewrite map_length; auto.
destruct (IHHZte3 h HZh) as [? [? ?]].
pose proof (extract_eq H1 H3); subst x.
rewrite Forall_map with (h := serasable_sem h Stype); auto.
pose proof (IHHZte4 h HZh) as [? [? ?]].
rewrite <- sem_type_subst_0.
apply Forall_coer2sem_type with (x := x); auto.
destruct HZh as [? [? ?]].
intros i [? [? ?]].
apply IHHZte2.
split; [rewrite app_length; omega|].
split; [apply Forall_app; auto|].
rewrite app_nil_r in ×.
apply sem_coer_env_app; split.
apply sem_type2sem_coer_env with (t12s := t12s); auto.
rewrite sem_coer_env_lift; auto.
apply CE_EMu.
intros R CTR; destruct HZh as [? [? ?]]; apply IHHZte; split; [|split]; simpl; auto.
rewrite sem_coer_env_shift; auto.
destruct HZh as [Hh [? ?]].
apply WFj_WF.
apply (jwf_sound H0 nil h); auto.
apply CE_EBot.
apply CE_ETop.
∃ nil; split; constructor.
destruct (IHHZte2 h HZh) as [? [? ?]].
∃ (t :: x); split; repeat constructor; auto.
∃ t1, t2; repeat split; repeat constructor; auto.
∃ t, t; split; [repeat constructor|split; [∃ nil; auto|intros k HY0 HY1 a ak Ha]].
apply (Ha nil); auto.
∃ t1, t3; split; [repeat constructor|split; [|intros k HY0 HY1 a ak Ha]].
destruct (IHHZte2 h HZh) as [? [? [? [[dh2 ?] ?]]]].
destruct (IHHZte1 (dh2 ++ h)) as [? [? [? [[dh1 ?] ?]]]];
[apply sem_erasable_env_app; auto; rewrite app_nil_r; auto|].
∃ (dh1 ++ dh2).
apply sem_erasable_env_app; auto.
destruct (IHHZte2 h HZh) as [? [? [? [? ?]]]]; destruct_extract.
apply H2 with k; auto; intros dh2 dHh2.
destruct (IHHZte1 (dh2 ++ h)) as [? [? [? [? ?]]]]; destruct_extract.
apply sem_erasable_env_app; auto.
rewrite app_nil_r; auto.
apply H4 with k; auto.
destruct dHh2 as [? [? ?]]; rewrite sem_coer_env_k_lift; auto.
destruct dHh2 as [? [? ?]]; rewrite sem_coer_env_k_lift; auto.
intros dh1 dHh1; rewrite app_assoc.
apply Ha.
apply sem_erasable_env_app; auto.
∃ t, s; split; [repeat constructor|split; [∃ nil; auto|intros k HY0 HY1 a ak Ha]].
destruct (IHHZte h HZh) as [? [? [? [? ?]]]]; destruct_extract.
apply H4 with k; auto; intros dh [? [? ?]].
rewrite sem_type_lift_0; auto.
apply (Ha nil); auto.
destruct (IHHZte3 h HZh) as [? [? [? [Hexi ?]]]].
destruct_extract; rename x into s', x0 into s.
pose proof Hexi as [wdh wHdh].
∃ (Arr t' s'), (Arr t s); split; [repeat constructor|split; [∃ wdh; auto|]].
intros k HY0 HY1.
apply Cl_approx_For; auto.
intros dh Hdh;
match goal with
|- C (PArr (?x _ _) _) ⇒ replace x with sem_type by reflexivity
end.
apply C_PArr; apply C_CE; [apply (H1 M22)|apply (H3 M22)];
apply sem_erasable_env_app; auto; rewrite app_nil_r; auto.
intros a ak;
match goal with
|- _ → PArr (?x _ _) _ _ ⇒ replace x with sem_type by reflexivity
end; intros Ha.
destruct (Ha wdh wHdh) as [j [a' [Heq [Hok _]]]].
∃ j, a'; repeat split; auto.
intros Hj b Rb.
apply H5 with (k - 1).
apply sem_coer_env_k_app; split; auto.
apply sem_coer_env_k_dec with k; auto; omega.
constructor.
subst a; destruct ak.
apply unary_fuel_map_trivial.
intros.
destruct j; [inversion Hj|]; simpl.
rewrite <- minus_n_O.
apply le_trans with (S j).
minmax.
omega.
intros dh Hdh.
destruct (Ha dh Hdh) as [k2 [a2' [Heq2 [_ Hsub]]]].
rewrite Heq in Heq2; inversion Heq2; subst k2 a2'.
apply Hsub; auto; clear Hsub.
destruct (IHHZte2 (dh ++ h)) as [? [? [? [? ?]]]];
[apply sem_erasable_env_app; auto; rewrite app_nil_r; auto|].
destruct_extract; rename x0 into t'.
apply H7 with (k - 1).
destruct Hdh as [? [? ?]].
rewrite sem_coer_env_k_lift; auto.
apply sem_coer_env_k_app; split; auto.
apply sem_coer_env_k_dec with k; auto; omega.
constructor.
destruct ak.
apply unary_fuel_map_trivial.
intros.
destruct j; [inversion Hj|]; simpl.
rewrite <- minus_n_O.
apply le_trans with (S j).
minmax.
omega.
intros dh0 [d0h0 _]; destruct dh0; inversion d0h0; simpl.
destruct Hdh as [? [? ?]].
rewrite sem_type_lift_0; auto.
destruct (IHHZte1 h HZh) as [? [? [? [Hexi ?]]]].
pose proof Hexi as [wdh1 wHdh1].
destruct (IHHZte2 h HZh) as [? [? [? [[wdh2 wHdh2] ?]]]].
destruct_extract; rename x into t', x0 into t, x1 into s', x2 into s.
∃ (Prod t' s'), (Prod t s); split; [repeat constructor|split; [∃ wdh1; auto|]].
intros k HY0 HY1.
apply Cl_approx_For; auto.
intros dh Hdh;
match goal with
|- C (PProd (?x _ _) _) ⇒ replace x with sem_type by reflexivity
end.
apply C_PProd; apply C_CE; [apply (H1 M22)|apply (H3 M22)];
apply sem_erasable_env_app; auto; rewrite app_nil_r; auto.
intros a ak;
match goal with
|- _ → PProd (?x _ _) _ _ ⇒ replace x with sem_type by reflexivity
end; intros Ha.
destruct (Ha wdh1 wHdh1) as [j [a' [b' [Heq [[Hoka Hokb] _]]]]].
∃ j, a', b'; repeat split; auto; rename H4 into Hj.
apply H5 with (k - 1).
apply sem_coer_env_k_app; split; auto.
apply sem_coer_env_k_dec with k; auto; omega.
constructor.
subst a; destruct ak.
apply unary_fuel_map_trivial.
intros.
destruct j; [inversion Hj|]; simpl.
rewrite <- minus_n_O.
apply le_trans with (S j).
minmax.
omega.
intros dh Hdh.
destruct (Ha dh Hdh) as [k2 [a2' [b2' [Heq2 [_ Hproj]]]]].
rewrite Heq in Heq2; inversion Heq2; subst k2 a2'.
apply Hproj; auto.
apply H7 with (k - 1).
apply sem_coer_env_k_app; split; auto.
apply sem_coer_env_k_dec with k; auto; omega.
constructor.
subst a; destruct ak.
apply unary_fuel_map_trivial.
intros.
destruct j; [inversion Hj|]; simpl.
rewrite <- minus_n_O.
apply le_trans with (S j).
minmax.
omega.
intros dh Hdh.
destruct (Ha dh Hdh) as [k2 [a2' [b2' [Heq2 [_ Hproj]]]]].
rewrite Heq in Heq2; inversion Heq2; subst k2 a2'.
apply Hproj; auto.
∃ t, s; split; [repeat constructor|split; [∃ nil; auto|intros k HY0 HY1 a ak Ha]].
assert (sem_type h t a) by (apply (Ha nil); auto); clear Ha.
apply CVar_sound with (c := c) (k := k) (Z := Y0 ++ Z) (t := t); auto.
apply sem_coer_env_k_app; split; auto.
destruct HZh as [_ [_ ?]]; rewrite app_nil_r in H6.
apply sem_coer_env_to_k; auto.
∃ t, (For dH t12s t); split; [repeat constructor|split; [|intros k HY0 HY1 a ak Ha]].
∃ (map (sem_type h) vecs).
split; [|split].
rewrite map_length; auto.
apply serasable_sem2Forall_type with (wits := wits); auto.
apply sem_type2sem_coer_env with (t12s := t12s); auto.
pose proof (IHHZte3 h HZh) as [? [? ?]].
rewrite <- sem_type_subst_0.
apply Forall_coer2sem_type with (x := x); auto.
intros dh [? [? ?]].
match goal with
| |- ?R _ _ _ ⇒
replace R with sem_type in × by reflexivity
end.
apply Ha.
split; [|split]; auto.
apply sem_type2sem_coer_env with (t12s := t12s); auto.
∃ (For dH t12s t), (subst vecs 0 t);
split; [repeat constructor|split; [∃ nil; auto|intros k HY0 HY1 a ak Ha]].
assert (sem_erasable_env h 0 nil nil) as nil0 by auto.
pose proof (Ha nil nil0) as Ha0; simpl app in Ha0.
rewrite sem_type_subst_0.
apply Ha0; split; [|split].
rewrite map_length; auto.
apply serasable_sem2Forall_type with (wits := insts); auto.
match goal with
| |- ?R _ _ _ ⇒
replace R with sem_type in × by reflexivity
end.
pose proof (IHHZte2 h HZh) as [? [? ?]].
rewrite <- sem_type_subst_0.
apply Forall_coer2sem_type with (x := x); auto.
∃ (Mu t), (subst1 (Mu t) 0 t);
split; [repeat constructor|split; [∃ nil; auto|intros k HY0 HY1 a ak Ha]].
unfold subst1; rewrite sem_type_subst_0; simpl.
assert (sem_erasable_env h 0 nil nil) as nil0 by auto.
pose proof (Ha nil nil0) as Ha0; simpl in Ha0.
pose proof (H0 M12).
inversion H3; clear H3; subst.
pose proof (jwf_sound H6 nil h).
simpl in H3.
remember (fun X ⇒ sem_type (X :: h) t) as F.
replace (sem_type (EMu F :: h) t) with (F (EMu F)) by (subst F; reflexivity).
destruct HZh as [? [? ?]].
apply (Mu_unfold F); auto.
apply WFj_WF; auto.
∃ (subst1 (Mu t) 0 t), (Mu t);
split; [repeat constructor|split; [∃ nil; auto|intros k HY0 HY1 a ak Ha]].
assert (sem_erasable_env h 0 nil nil) as nil0 by auto.
pose proof (Ha nil nil0) as Ha0.
unfold subst1 in Ha0; rewrite sem_type_subst_0 in Ha0; simpl in Ha0.
inversion HZte; subst.
pose proof (jwf_sound H2 nil h).
simpl in H0.
simpl; remember (fun X ⇒ sem_type (X :: h) t) as F.
replace (sem_type (EMu F :: h) t) with (F (EMu F)) in Ha0 by (subst F; reflexivity).
destruct HZh as [? [? ?]].
apply (Mu_fold F); auto.
apply WFj_WF; auto.
∃ t, s; split; [repeat constructor|split; [∃ nil; auto|]].
induction k; intros HY0 HY1 a ak Ha; [exfalso; apply term_lt_0 with a; auto|].
simpl in *; rewrite <- minus_n_O in ×.
destruct (IHHZte h HZh) as [? [? [? [? ?]]]]; destruct_extract.
rename x into t, x0 into s.
apply H4 with (S k); auto.
simpl; rewrite <- minus_n_O; constructor; auto.
clear a ak Ha; intros a [ak Ha]; split; auto.
apply IHk; auto.
apply sem_coer_env_k_dec with (S k); auto; omega.
apply sem_coer_env_k_dec with k; auto; omega.
intros dh0 [d0h0 _]; destruct dh0; inversion d0h0; simpl; auto.
∃ Bot, t; split; [repeat constructor|split; [∃ nil; auto|intros k HY0 HY1 a ak Ha]].
apply (Ha nil); auto.
apply IHHZte; auto.
∃ t, Top; split; [repeat constructor|split; [∃ nil; auto|intros k HY0 HY1 a ak Ha]].
apply fold_Cl; left.
∃ (sem_type h t); split; [apply (H1 M12)|apply (Ha nil)]; auto.
Qed.
Lemma jtype_sound : ∀ {H Z t}, jtype 2 H Z t → stype H Z t.
Proof. intros; apply jerasable_sound; auto. Qed.
Lemma jcoer_sound : ∀ {H Z Y0 Y1 dH dZ t s},
jcoer 2 H Z Y0 Y1 dH dZ t s → scoer H Z Y0 Y1 dH dZ t s.
Proof. intros; apply jerasable_sound; auto. Qed.
Definition sterm_env H Z G :=
∀ h, sem_erasable_env nil H Z h → Forall CE (sem_term_env h G).
Hint Unfold sterm_env.
Definition sterm H Z G a t :=
∀ h, sem_erasable_env nil H Z h → EJudg (sem_term_env h G) (sem_type h t) a.
Hint Unfold sterm.
Lemma jterm_env_sound : ∀ {H Z G}, jterm_env 2 H Z G → sterm_env H Z G.
Proof.
intros H Z G [_ HZG]; induction G; inversion HZG; clear HZG; subst; constructor.
apply (jtype_sound H2 h H0).
apply (IHG H3 h H0).
Qed.
Lemma sem_term_env_lift : ∀ G h dH dh, length dh = dH →
sem_term_env (dh ++ h) (map (lift dH 0) G) = sem_term_env h G.
Proof.
induction G; intros h dH dh dHh; simpl; auto.
rewrite sem_type_lift_0; auto.
rewrite IHG; auto.
Qed.
Definition serasable_env H Z := ∃ h, sem_erasable_env nil H Z h.
Lemma jerasable_env_sound : ∀ {H Z},
jerasable_env 2 H Z → serasable_env H Z.
Proof.
intros H Z jenv.
induction jenv; [∃ nil; repeat split; auto|].
destruct H0 as [xs [? [? [? ?]]]].
destruct IHjenv as [h [? [? ?]]].
∃ (map (sem_type h) xs ++ h).
subst dHH dZZ.
repeat split.
rewrite app_length; rewrite map_length; auto.
apply Forall_app.
split; auto.
pose proof (extract_inject Slisttype xs).
apply serasable_sem2Forall_type with (wits := (inject Slisttype xs)); auto.
apply (jerasable_sound H4 h); auto.
rewrite app_nil_r.
apply sem_coer_env_app.
split.
pose proof (extract_inject Slistprodtype dZ).
pose proof (jerasable_sound H5 h) as [? [? ?]]; auto.
apply sem_type2sem_coer_env with (t12s := inject Slistprodtype dZ); auto.
rewrite <- sem_type_subst_0.
apply Forall_coer2sem_type with (x := x); auto.
rewrite app_nil_r in H8.
rewrite sem_coer_env_lift; auto.
rewrite map_length; auto.
Qed.
Lemma nth_sem : ∀ x G t h, nth x G Top = t →
nth x (sem_term_env h G) ETop = sem_type h t.
Proof. induction x; intros G t h Gx; destruct G as [|s G]; simpl in *; subst; auto. Qed.
Lemma jterm_sound : ∀ {H Z G a t}, jterm 2 H Z G a t → sterm H Z G a t.
Proof.
intros H Z G a t HZGat; induction HZGat; intros h Hh; simpl.
apply EVar_sem; [|apply nth_sem]; auto.
apply (Forall_impl _ (@C_CE) ((jterm_env_sound (H0 M12)) h Hh)).
pose proof (jterm_extract_jterm_env M12 HZGat) as [_ ?].
inversion H1; subst.
pose proof (jtype_sound H4) as HZt.
pose proof (jtype_sound (jterm_extract_jtype M12 HZGat)) as HZs.
apply ELam_sem; [apply CEexp; apply HZt|apply (C_CE (HZs h Hh))|]; auto.
apply IHHZGat; auto.
pose proof (jterm_extract_jtype M12 HZGat1) as Hts.
inversion Hts; subst.
pose proof (C_CE (jtype_sound H5 h Hh)).
pose proof (jtype_sound H6 h Hh).
apply EApp_sem with (R := sem_type h t); auto.
apply IHHZGat1; auto.
pose proof (C_CE (jtype_sound (jterm_extract_jtype M12 HZGat1) h Hh)).
pose proof (C_CE (jtype_sound (jterm_extract_jtype M12 HZGat2) h Hh)).
apply EPair_sem; auto.
pose proof (jterm_extract_jtype M12 HZGat) as Hts.
inversion Hts; subst.
pose proof (jtype_sound H5 h Hh).
pose proof (C_CE (jtype_sound H6 h Hh)).
apply EFst_sem with (S := sem_type h s); auto.
apply IHHZGat; auto.
pose proof (jterm_extract_jtype M12 HZGat) as Hts.
inversion Hts; subst.
pose proof (C_CE (jtype_sound H5 h Hh)).
pose proof (jtype_sound H6 h Hh).
apply ESnd_sem with (R := sem_type h t); auto.
apply IHHZGat; auto.
pose proof (jtype_sound (jterm_extract_jtype M12 HZGat)).
pose proof (jcoer_sound H1 h Hh) as [? [? [? [? ?]]]].
assert (sterm_env (dH + H) (dZ ++ dmap (lift dH 0) Z) (map (lift dH 0) G)).
intros dhh [? [? ?]].
destruct (cut_length _ _ _ _ H6) as [dh [h' [? [? ?]]]]; subst dhh; clear H6.
rewrite sem_term_env_lift; auto.
apply (jterm_env_sound (H0 M12)).
apply Forall_app in H7 as [? ?].
repeat split; auto.
rewrite app_nil_r in ×.
apply sem_coer_env_app in H8 as [? ?].
rewrite <- sem_coer_env_lift with (dH := dH) (dh := dh); auto.
apply ECoer_sem with (R := sem_type h (For dH (inject Slistprodtype dZ) t)); auto;
destruct_extract; rename x into t, x0 into s.
intros b Hb.
destruct (term_lt_exists b) as [k bk].
apply H5 with k; try constructor; auto.
intros dh [? [? ?]].
apply Hb; split; [|split]; auto.
match goal with
| |- ?R _ _ _ ⇒ replace R with sem_type by reflexivity
end.
apply sem_coer_env2sem_type with (dZ := dZ); auto.
apply (extract_inject Slistprodtype).
apply Edistrib;
match goal with
| |- context[?R _ _ _] ⇒ replace R with sem_type by reflexivity
end.
destruct H4 as [wdh [? [? ?]]].
∃ wdh; repeat split; auto.
apply sem_coer_env2sem_type with (dZ := dZ); auto.
apply extract_inject.
intros dh [? [? ?]]; apply H2.
apply sem_erasable_env_app; auto; rewrite app_nil_r; auto.
repeat split; auto.
apply sem_type2sem_coer_env with (t12s := inject Slistprodtype dZ); auto.
apply extract_inject.
intros dh [? [? ?]].
rewrite <- sem_term_env_lift with (dH := dH) (dh := dh); auto.
apply IHHZGat.
apply sem_erasable_env_app; auto.
rewrite app_nil_r; auto.
repeat split; auto.
apply sem_type2sem_coer_env with (t12s := inject Slistprodtype dZ); auto.
apply (extract_inject Slistprodtype).
Qed.