Library typesystem
Require Import Omega.
Require Import List.
Require Import Equality.
Require Import ext.
Require Import list.
Inductive type : Set :=
| Var (x : nat)
| Arr (t : type) (s : type)
| Prod (t : type) (s : type)
| For (d : nat) (t12s : type) (t : type)
| Mu (t : type)
| Bot
| Top
| Snil
| Scons (t : type) (ts : type)
| Spair (d : nat) (t1 : type) (t2 : type)
.
Definition Var_a := Var.
Hint Unfold Var_a.
Definition traverse f := fix g i t :=
match t with
| Var a ⇒ f a i
| Arr t s ⇒ Arr (g i t) (g i s)
| Prod t s ⇒ Prod (g i t) (g i s)
| For d t12s r ⇒ For d (g (d + i) t12s) (g (d + i) r)
| Mu t ⇒ Mu (g (1 + i) t)
| Bot ⇒ Bot
| Top ⇒ Top
| Snil ⇒ Snil
| Scons t ts ⇒ Scons (g i t) (g i ts)
| Spair d t1 t2 ⇒ Spair d (g (d + i) t1) (g i t2)
end.
Definition lift_idx d a i := Var (if le_gt_dec i a then d + a else a).
Definition lift d := traverse (lift_idx d).
Definition shift := lift 1.
Hint Unfold lift_idx lift shift.
Definition subst_idx vecs a i :=
match le_gt_dec i a with
| right _ ⇒ Var a
| left _ ⇒
match le_gt_dec (i + length vecs) a with
| right _ ⇒ lift i 0 (nth (a - i) vecs Top)
| left _ ⇒ Var (a - length vecs)
end
end.
Definition subst vecs := traverse (subst_idx vecs).
Hint Unfold subst_idx subst.
Definition subst1 s i t := subst (s :: nil) i t.
Ltac subst_lift_var := repeat first
[ rewrite app_length in ×
| rewrite map_length in ×
| match goal with
| |- context[subst_idx] ⇒ unfold subst_idx
| |- context[lift_idx] ⇒ unfold lift_idx
| |- context[le_gt_dec ?x ?y] ⇒ destruct (le_gt_dec x y); try (exfalso; omega); simpl; auto
end ].
Notation type_env := nat.
Definition coer_env := list (type × type).
Definition pmap (f : type → type) xy :=
match xy with
| (x, y) ⇒ (f x, f y)
end.
Definition dmap (f : type → type) xs := map (pmap f) xs.
Hint Unfold pmap dmap.
Definition term_env := list type.
Inductive sort : Set :=
| Stype
| Sprod (e1 : sort) (e2 : sort)
| Slist (e : sort)
| Scoer (Y0 Y1 : coer_env) (dH : type_env) (dZ : coer_env)
.
Notation Sprodtype := (Sprod Stype Stype).
Notation Slistprodtype := (Slist Sprodtype).
Notation Slisttype := (Slist Stype).
Notation Slistcoer := (Slist (Scoer nil nil 0 nil)).
Fixpoint sort_type e :=
match e with
| Stype ⇒ type
| Sprod e1 e2 ⇒ prod (sort_type e1) (sort_type e2)
| Slist e ⇒ list (sort_type e)
| Scoer _ _ _ _ ⇒ prod type type
end.
Inductive extract : ∀ (e : sort), type → sort_type e → Prop :=
| Etype : ∀ t, extract Stype t t
| Enil : ∀ e, extract (Slist e) Snil nil
| Econs : ∀ e t ts x xs,
extract e t x →
extract (Slist e) ts xs →
extract (Slist e) (Scons t ts) (x :: xs)
| Epair : ∀ e1 e2 t1 t2 x1 x2,
extract e1 t1 x1 →
extract e2 t2 x2 →
extract (Sprod e1 e2) (Spair 0 t1 t2) (x1, x2)
| Ecoer : ∀ dH dZ Y0 Y1 t s,
extract (Scoer Y0 Y1 dH dZ) (Spair dH t s) (t, s)
.
Tactic Notation "dep" hyp(H) :=
do_depelim' ltac:(fun hyp ⇒ idtac) ltac:(fun hyp ⇒ do_case hyp) H.
Ltac destruct_extract := repeat
match goal with
| H : extract Stype _ _ |- _ ⇒ dep H
| H : extract _ ?x _ |- _ ⇒ (is_var x; fail 1) || dep H
| H : extract _ _ ?x |- _ ⇒ (is_var x; fail 1) || dep H
end.
Lemma extract_eq : ∀ {e t x y}, extract e t x → extract e t y → x = y.
Proof. induction 1; intros Hy; dep Hy; first [reflexivity|f_equal; auto]. Qed.
Lemma extract_inj : ∀ {e t x}, extract e t x → ∀ {s}, extract e s x → t = s.
Proof. induction 1; intros ? Hy; dep Hy; first [reflexivity|f_equal; auto]. Qed.
Definition inj_list A (inj : A → type) := fix f xs :=
match xs with
| nil ⇒ Snil
| cons x xs ⇒ Scons (inj x) (f xs)
end.
Fixpoint inject e (x : sort_type e) : type :=
match e return sort_type e → type with
| Stype ⇒ fun x ⇒ x
| Sprod e1 e2 ⇒ fun x ⇒
match x with
| (x1, x2) ⇒ Spair 0 (inject e1 x1) (inject e2 x2)
end
| Slist e ⇒ inj_list (sort_type e) (inject e)
| Scoer Y0 Y1 dH dZ ⇒ fun x ⇒
match x with
| (t, s) ⇒ Spair dH t s
end
end x.
Hint Unfold inj_list inject.
Lemma extract_inject : ∀ e x, extract e (inject e x) x.
Proof.
induction e; intros; simpl.
apply Etype.
destruct x as [x1 x2].
apply Epair; auto.
induction x as [|x xs]; [apply Enil|].
apply Econs; auto.
destruct x.
apply Ecoer.
Qed.
Lemma inject_extract : ∀ {e x t}, extract e t x → t = inject e x.
Proof.
intros.
apply (extract_inj H).
apply extract_inject.
Qed.
Inductive wfsort := WF | NE.
Inductive jwf : type_env → type → wfsort → Prop :=
| WFVar : ∀ a, jwf a (Var_a a) NE
| WFArr : ∀ a t s, jwf a t NE → jwf a s NE → jwf a (Arr t s) WF
| WFProd : ∀ a t s, jwf a t NE → jwf a s NE → jwf a (Prod t s) WF
| WFFor : ∀ wf a d t12s s12s t, t12s = shift (d + a) s12s →
jwf (d + a) t wf → jwf a (For d t12s t) wf
| WFMu : ∀ wf a t, jwf 0 t WF → jwf (1 + a) t wf → jwf a (Mu t) wf
| WFwf : ∀ a t s, t = shift a s → jwf a t WF
| WFne : ∀ a t, jwf a t WF → jwf a t NE
.
Inductive jerasable M : type_env → coer_env → type → sort → Prop :=
| JTVar : ∀ H Z n,
jerasable M H Z (Var n) Stype
| JTArr : ∀ H Z t s,
jerasable M H Z t Stype →
jerasable M H Z s Stype →
jerasable M H Z (Arr t s) Stype
| JTProd : ∀ H Z t s,
jerasable M H Z t Stype →
jerasable M H Z s Stype →
jerasable M H Z (Prod t s) Stype
| JTFor : ∀ H Z dH dZ t12s wits vecs t,
extract Slistprodtype t12s dZ →
extract Slisttype wits vecs →
length vecs = dH →
jerasable M (dH + H) (dmap (lift dH 0) Z) t12s Slistprodtype →
jerasable M (dH + H) (dZ ++ (dmap (lift dH 0) Z)) t Stype →
jerasable M H Z wits Slisttype →
jerasable M H Z (subst vecs 0 t12s) Slistcoer →
jerasable M H Z (For dH t12s t) Stype
| JTMu : ∀ H Z t,
jwf 0 t WF →
jerasable M (1 + H) (dmap (lift 1 0) Z) t Stype →
jerasable M H Z (Mu t) Stype
| JTBot : ∀ H Z,
jerasable M H Z Bot Stype
| JTTop : ∀ H Z,
jerasable M H Z Top Stype
| JSNil : ∀ H Z e,
jerasable M H Z Snil (Slist e)
| JSCons : ∀ H Z t ts e,
jerasable M H Z t e →
jerasable M H Z ts (Slist e) →
jerasable M H Z (Scons t ts) (Slist e)
| JSPair : ∀ H Z t1 t2 e1 e2,
jerasable M H Z t1 e1 →
jerasable M H Z t2 e2 →
jerasable M H Z (Spair 0 t1 t2) (Sprod e1 e2)
| JCRefl : ∀ H Z Y0 Y1 t,
(1 ≤ M → jerasable M H Z t Stype) →
jerasable M H Z (Spair 0 t t) (Scoer Y0 Y1 0 nil)
| JCTrans : ∀ dH1 dH2 H dZ1 dZ2 Z Y0 Y1 t1 t2 t3,
jerasable M (dH2 + H) (dZ2 ++ (dmap (lift dH2 0) Z)) (Spair dH1 t1 t2)
(Scoer (dmap (lift dH2 0) Y0) (dmap (lift dH2 0) Y1) dH1 dZ1) →
jerasable M H Z (Spair dH2 t2 t3) (Scoer Y0 Y1 dH2 dZ2) →
jerasable M H Z (Spair (dH1 + dH2) t1 t3) (Scoer Y0 Y1 (dH1 + dH2) (dZ1 ++ (dmap (lift dH1 0) dZ2)))
| JCWeak : ∀ dH H dZ Z Y0 Y1 t s,
(1 ≤ M → jerasable M H Z t Stype) →
jerasable M H Z (Spair dH (lift dH 0 t) s) (Scoer Y0 Y1 dH dZ) →
jerasable M H Z (Spair 0 t s) (Scoer Y0 Y1 0 nil)
| JCArr : ∀ dH H dZ Z Y0 Y1 t' s' t s,
(2 ≤ M → jerasable M (dH + H) (dZ ++ (dmap (lift dH 0) Z)) t' Stype) →
(2 ≤ M → jerasable M (dH + H) (dZ ++ (dmap (lift dH 0) Z)) s' Stype) →
jerasable M H Z t Stype →
jerasable M (dH + H) (dZ ++ (dmap (lift dH 0) Z)) (Spair 0 (lift dH 0 t) t')
(Scoer (dmap (lift dH 0) (Y1 ++ Y0)) nil 0 nil) →
jerasable M H Z (Spair dH s' s) (Scoer (Y1 ++ Y0) nil dH dZ) →
jerasable M H Z (Spair dH (Arr t' s') (Arr t s)) (Scoer Y0 Y1 dH dZ)
| JCProd : ∀ dH H dZ Z Y0 Y1 t' s' t s,
(2 ≤ M → jerasable M (dH + H) (dZ ++ (dmap (lift dH 0) Z)) t' Stype) →
(2 ≤ M → jerasable M (dH + H) (dZ ++ (dmap (lift dH 0) Z)) s' Stype) →
jerasable M H Z (Spair dH t' t) (Scoer (Y1 ++ Y0) nil dH dZ) →
jerasable M H Z (Spair dH s' s) (Scoer (Y1 ++ Y0) nil dH dZ) →
jerasable M H Z (Spair dH (Prod t' s') (Prod t s)) (Scoer Y0 Y1 dH dZ)
| JCVar : ∀ H Z Y0 Y1 c t s,
(1 ≤ M → jerasable M H Z t Stype) →
(1 ≤ M → jerasable M H Z s Stype) →
nth c (Y0 ++ Z) (Top, Top) = (t, s) →
jerasable M H Z (Spair 0 t s) (Scoer Y0 Y1 0 nil)
| JCGen : ∀ dH H dZ Z Y0 Y1 t12s wits vecs t,
(1 ≤ M → jerasable M H Z (For dH t12s t) Stype) →
extract Slistprodtype t12s dZ →
extract Slisttype wits vecs →
length vecs = dH →
jerasable M (dH + H) (dmap (lift dH 0) Z) t12s Slistprodtype →
jerasable M H Z wits Slisttype →
jerasable M H Z (subst vecs 0 t12s) Slistcoer →
jerasable M H Z (Spair dH t (For dH t12s t)) (Scoer Y0 Y1 dH dZ)
| JCInst : ∀ dH H Z Y0 Y1 t12s t insts vecs,
(1 ≤ M → jerasable M H Z (For dH t12s t) Stype) →
extract Slisttype insts vecs →
length vecs = dH →
jerasable M H Z insts Slisttype →
jerasable M H Z (subst vecs 0 t12s) Slistcoer →
jerasable M H Z (Spair 0 (For dH t12s t) (subst vecs 0 t)) (Scoer Y0 Y1 0 nil)
| JCUnfold : ∀ H Z Y0 Y1 t,
(1 ≤ M → jerasable M H Z (Mu t) Stype) →
(M ≠ 1 → jwf 0 t WF) →
jerasable M H Z (Spair 0 (Mu t) (subst1 (Mu t) 0 t)) (Scoer Y0 Y1 0 nil)
| JCFold : ∀ H Z Y0 Y1 t,
jerasable M H Z (Mu t) Stype →
jerasable M H Z (Spair 0 (subst1 (Mu t) 0 t) (Mu t)) (Scoer Y0 Y1 0 nil)
| JCFix : ∀ H Z Y0 Y1 t s,
(M ≠ 1 → jerasable M H Z s Stype) →
jerasable M H Z (Spair 0 t s) (Scoer Y0 ((t, s) :: Y1) 0 nil) →
jerasable M H Z (Spair 0 t s) (Scoer Y0 Y1 0 nil)
| JCBot : ∀ H Z Y0 Y1 t,
jerasable M H Z t Stype →
jerasable M H Z (Spair 0 Bot t) (Scoer Y0 Y1 0 nil)
| JCTop : ∀ H Z Y0 Y1 t,
(1 ≤ M → jerasable M H Z t Stype) →
jerasable M H Z (Spair 0 t Top) (Scoer Y0 Y1 0 nil)
.
Definition jtype M H Z t := jerasable M H Z t Stype.
Definition jcoer M H Z Y0 Y1 dH dZ t s := jerasable M H Z (Spair dH t s) (Scoer Y0 Y1 dH dZ).
Hint Unfold jtype jcoer.
Ltac jerasable_induction H :=
induction H; intros;
[ apply JTVar
| apply JTArr
| apply JTProd
| eapply JTFor
| apply JTMu
| apply JTBot
| apply JTTop
| apply JSNil
| apply JSCons
| apply JSPair
| apply JCRefl
| eapply JCTrans
| eapply JCWeak
| apply JCArr
| apply JCProd
| eapply JCVar
| eapply JCGen
| eapply JCInst
| apply JCUnfold
| apply JCFold
| apply JCFix
| apply JCBot
| apply JCTop].
Definition jerasable_bind M H Z dH dZ := ∃ vecs,
length vecs = dH ∧
jerasable M (dH + H) (dmap (lift dH 0) Z) (inject Slistprodtype dZ) Slistprodtype ∧
jerasable M H Z (inject Slisttype vecs) Slisttype ∧
jerasable M H Z (subst vecs 0 (inject Slistprodtype dZ)) Slistcoer.
Inductive jerasable_env M : type_env → coer_env → Prop :=
| JEnil : jerasable_env M 0 nil
| JEcons : ∀ H Z dH dZ dHH dZZ,
jerasable_env M H Z →
jerasable_bind M H Z dH dZ →
dHH = dH + H →
dZZ = dZ ++ dmap (lift dH 0) Z →
jerasable_env M dHH dZZ
.
Hint Unfold jerasable_bind.
Definition jterm_env M H Z G := (1 ≤ M → jerasable_env M H Z) ∧ Forall (jtype M H Z) G.
Hint Unfold jterm_env.
Lemma jterm_env_extract_jerasable_env : ∀ {M H Z G}, 1 ≤ M →
jterm_env M H Z G → jerasable_env M H Z.
Proof. intros ? ? ? ? I [H ?]; exact (H I). Qed.
Lemma lift_0 : ∀ t i, lift 0 i t = t.
Proof. induction t; intros i; simpl; [subst_lift_var|..]; f_equal; auto. Qed.
Lemma lift_fusion : ∀ t d l jl ij,
jl ≥ l → jl ≤ ij + l →
lift d jl (lift ij l t) = lift (d + ij) l t.
Proof.
induction t; intros; simpl; [|f_equal..];
try (first [reflexivity|rewrite IHt|rewrite IHt1|rewrite IHt2]; auto; omega).
subst_lift_var; f_equal; omega.
Qed.
Lemma lift_lift : ∀ t a b i ij, i ≤ ij →
lift a i (lift b ij t) = lift b (a + ij) (lift a i t).
Proof.
induction t; intros; simpl; [|f_equal..];
try (repeat rewrite plus_assoc;
first [reflexivity|rewrite IHt|rewrite IHt1|rewrite IHt2];
repeat rewrite <- plus_assoc;
f_equal; omega).
subst_lift_var; f_equal; omega.
Qed.
Lemma lift_subst1 : ∀ o vecs j t i,
lift o i (subst vecs (i + j) t) =
subst vecs (i + o + j) (lift o i t).
Proof.
induction t; intros; simpl; [|f_equal..];
try (repeat rewrite plus_assoc;
first [reflexivity|rewrite IHt|rewrite IHt1|rewrite IHt2];
repeat rewrite <- plus_assoc;
f_equal; omega).
subst_lift_var; [f_equal; omega|].
rewrite lift_fusion; [|omega..].
f_equal; [omega|].
f_equal; omega.
Qed.
Lemma lift_subst2 : ∀ off o vecs t i,
lift off (i + o) (subst vecs i t) =
subst (map (lift off o) vecs) i (lift off (i + length vecs + o) t).
Proof.
induction t; intros; simpl; [|f_equal..];
try (repeat rewrite plus_assoc;
first [reflexivity|rewrite <- IHt|rewrite <- IHt1|rewrite <- IHt2];
repeat rewrite <- plus_assoc;
f_equal; omega).
subst_lift_var; [f_equal; omega|].
replace Top with (lift off o Top) by reflexivity.
rewrite map_nth; simpl.
apply eq_sym.
apply lift_lift; omega.
Qed.
Lemma lift_subst1_0 : ∀ o vecs t j,
lift o 0 (subst vecs j t) =
subst vecs (o + j) (lift o 0 t).
Proof.
intros.
pose proof (lift_subst1 o vecs j t 0).
simpl in H; assumption.
Qed.
Lemma lift_subst2_0 : ∀ off o vecs t,
lift off o (subst vecs 0 t) =
subst (map (lift off o) vecs) 0 (lift off (length vecs + o) t).
Proof.
intros.
pose proof (lift_subst2 off o vecs t 0).
simpl in H; assumption.
Qed.
Lemma lift_subst2_0_1 : ∀ off o s t,
lift off o (subst1 s 0 t) =
subst1 (lift off o s) 0 (lift off (1 + o) t).
Proof.
intros.
pose proof (lift_subst2 off o (s :: nil) t 0).
simpl in H; assumption.
Qed.
Lemma subst_lift : ∀ t b i j h,
j ≥ i → j + length b ≤ i + h →
subst b j (lift h i t) = lift (h - length b) i t.
Proof.
induction t; intros; simpl; [|f_equal..];
try (first [reflexivity|rewrite IHt|rewrite IHt1|rewrite IHt2]; auto; omega).
subst_lift_var; f_equal; omega.
Qed.
Lemma subst_lift_0 : ∀ t b j h,
j + length b ≤ h →
subst b j (lift h 0 t) = lift (h - length b) 0 t.
Proof.
intros.
pose proof (subst_lift t b 0 j h).
simpl in H0.
rewrite H0; auto; omega.
Qed.
Lemma omega_shit_0 : ∀ a b c d, a + b - c - d - a = b - c - d.
Proof. intros; omega. Qed.
Lemma omega_shit_1 : ∀ a b c, a - b - c = a - c - b.
Proof. intros; omega. Qed.
Lemma subst_subst : ∀ t xs vecs i j,
subst xs (i + j) (subst vecs i t) =
subst (map (subst xs j) vecs) i (subst xs (i + length vecs + j) t).
Proof.
induction t; intros; simpl; [|f_equal..];
try (repeat rewrite plus_assoc;
first [reflexivity|rewrite IHt|rewrite IHt1|rewrite IHt2];
repeat rewrite <- plus_assoc;
repeat first [omega|f_equal]).
subst_lift_var.
f_equal; apply omega_shit_1.
rewrite subst_lift_0; repeat rewrite map_length; [|omega].
f_equal; [omega|].
f_equal; omega.
replace Top with (subst xs j Top) by reflexivity.
rewrite map_nth; simpl.
rewrite lift_subst1_0.
reflexivity.
replace (S (i + j)) with (1 + i + j) by reflexivity.
rewrite IHt; f_equal; f_equal; omega.
Qed.
Lemma subst_subst_0 : ∀ t xs vecs j,
subst xs j (subst vecs 0 t) =
subst (map (subst xs j) vecs) 0 (subst xs (length vecs + j) t).
Proof.
intros.
pose proof (subst_subst t xs vecs 0 j).
simpl in H; auto.
Qed.
Lemma subst_subst_0_1 : ∀ t xs s j,
subst xs j (subst1 s 0 t) =
subst1 (subst xs j s) 0 (subst xs (1 + j) t).
Proof.
intros.
pose proof (subst_subst t xs (s :: nil) 0 j).
simpl in H; auto.
Qed.
Lemma subst_app : ∀ x2s x1s t i,
subst (map (subst x2s 0) x1s ++ x2s) i t = subst x2s i (subst x1s i t).
Proof.
induction t; intros; simpl; [|f_equal..]; auto.
subst_lift_var.
f_equal; omega.
rewrite app_nth2; rewrite map_length; [|omega].
f_equal; f_equal; apply omega_shit_1.
rewrite app_nth1; repeat rewrite map_length; [|omega].
replace Top with (subst x2s 0 Top) by reflexivity.
rewrite map_nth; simpl.
rewrite lift_subst1_0.
f_equal; omega.
Qed.
Lemma subst_app_0 : ∀ x2s x1s t,
subst (map (subst x2s 0) x1s ++ x2s) 0 t = subst x2s 0 (subst x1s 0 t).
Proof. intros; pose proof (subst_app x2s x1s t 0); auto. Qed.
Ltac dmap_tac t :=
intros Z; induction Z as [|[? ?] Z]; intros; simpl; f_equal; auto;
simpl; f_equal; apply t; omega.
Lemma dmap_lift_0 : ∀ Z i, dmap (lift 0 i) Z = Z.
Proof. dmap_tac lift_0. Qed.
Lemma dmap_lift_fusion : ∀ Z d l jl ij,
jl ≥ l → jl ≤ ij + l → dmap (lift d jl) (dmap (lift ij l) Z) = dmap (lift (d + ij) l) Z.
Proof. dmap_tac lift_fusion. Qed.
Lemma dmap_lift_plus : ∀ d1 d2 Z i,
dmap (lift (d1 + d2) i) Z = dmap (lift d1 i) (dmap (lift d2 i) Z).
Proof. intros; rewrite dmap_lift_fusion; auto; omega. Qed.
Lemma dmap_lift_lift : ∀ Z a b i ij, i ≤ ij →
dmap (lift a i) (dmap (lift b ij) Z) = dmap (lift b (a + ij)) (dmap (lift a i) Z).
Proof. dmap_tac lift_lift. Qed.
Lemma dmap_lift_subst1 : ∀ Z o vecs j,
dmap (lift o 0) (dmap (subst vecs j) Z) =
dmap (subst vecs (o + j)) (dmap (lift o 0) Z).
Proof. dmap_tac lift_subst1_0. Qed.
Lemma dmap_lift_subst2 : ∀ Z off o vecs,
dmap (lift off o) (dmap (subst vecs 0) Z) =
dmap (subst (map (lift off o) vecs) 0) (dmap (lift off (length vecs + o)) Z).
Proof. dmap_tac lift_subst2_0. Qed.
Lemma dmap_subst_lift : ∀ t b j h,
j + length b ≤ h →
dmap (subst b j) (dmap (lift h 0) t) = dmap (lift (h - length b) 0) t.
Proof. dmap_tac subst_lift_0. Qed.
Lemma dmap_app : ∀ f Z1 Z2, dmap f Z1 ++ dmap f Z2 = dmap f (Z1 ++ Z2).
Proof. intros; unfold dmap; rewrite map_app; auto. Qed.
Definition etraverse f := fix g i e :=
match e with
| Stype ⇒ Stype
| Sprod e1 e2 ⇒ Sprod (g i e1) (g i e2)
| Slist e ⇒ Slist (g i e)
| Scoer Y0 Y1 dH dZ ⇒ Scoer (dmap (f i) Y0) (dmap (f i) Y1) dH (dmap (f (dH + i)) dZ)
end.
Definition elift d i := etraverse (lift d) i.
Definition esubst vecs i := etraverse (subst vecs) i.
Fixpoint slift e d i :=
match e return sort_type e → sort_type e with
| Stype ⇒ lift d i
| Sprod e1 e2 ⇒ fun x ⇒
match x with
| (x1, x2) ⇒ (slift e1 d i x1, slift e2 d i x2)
end
| Slist e ⇒ fix f xs :=
match xs with
| nil ⇒ nil
| cons x xs ⇒ cons (slift e d i x) (f xs)
end
| Scoer Y0 Y1 dH dZ ⇒ fun x ⇒
match x with
| (t, s) ⇒ (lift d (dH + i) t, lift d i s)
end
end.
Lemma extract_lift : ∀ d e x t i, extract e t x → extract e (lift d i t) (slift e d i x).
Proof.
induction e; [|induction x..]; intros; destruct_extract; simpl in *; auto using extract.
apply Econs; auto.
apply IHx; auto.
Qed.
Lemma lift_inject : ∀ d e i x,
lift d i (inject e x) = inject e (slift e d i x).
Proof. induction e; [|induction x..]; intros; simpl; f_equal; auto. Qed.
Fixpoint ssubst e vecs i :=
match e return sort_type e → sort_type e with
| Stype ⇒ subst vecs i
| Sprod e1 e2 ⇒ fun x ⇒
match x with
| (x1, x2) ⇒ (ssubst e1 vecs i x1, ssubst e2 vecs i x2)
end
| Slist e ⇒ fix f xs :=
match xs with
| nil ⇒ nil
| cons x xs ⇒ cons (ssubst e vecs i x) (f xs)
end
| Scoer Y0 Y1 dH dZ ⇒ fun x ⇒
match x with
| (t, s) ⇒ (subst vecs (dH + i) t, subst vecs i s)
end
end.
Lemma extract_subst : ∀ vecs e x t i, extract e t x →
extract e (subst vecs i t) (ssubst e vecs i x).
Proof.
induction e; [|induction x..]; intros; destruct_extract; simpl in *; auto using extract.
apply Econs; auto.
apply IHx; auto.
Qed.
Lemma subst_inject : ∀ xs e i x,
subst xs i (inject e x) = inject e (ssubst e xs i x).
Proof. induction e; [|induction x..]; intros; simpl; f_equal; auto. Qed.
Ltac dmap_lift_lift_tac :=
match goal with
| |- context[dmap (lift ?a (?b + ?c)) (dmap (lift ?b 0) ?Z)] ⇒
rewrite <- (dmap_lift_lift Z b a 0 c); [|omega]
| |- context[dmap (lift ?a ?b) (dmap (lift ?b 0) ?Z)] ⇒
rewrite (dmap_lift_fusion Z a 0 b b); [|omega..]
end.
Ltac S_plus_1 :=
match goal with
| |- context[S ?x] ⇒ is_var x; replace (S x) with (1 + x) by reflexivity
end.
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.
Ltac tryomega := subst; repeat first
[ assumption
| reflexivity
| omega
| unfold dmap; rewrite map_length
| rewrite <- dmap_app
| rewrite <- app_assoc
| repeat S_plus_1; rewrite dmap_lift_plus
| rewrite dmap_lift_0
| dmap_lift_lift_tac
| rewrite dmap_lift_subst1 ].
Lemma jwf_lift : ∀ wf off t a,
jwf a t wf →
∀ o,
jwf a (lift off (a + S o) t) wf.
Proof.
induction 1; simpl; intros; [subst_lift_var|..]; eauto using jwf.
apply WFFor with (lift off (d + a + o) s12s).
unfold shift; rewrite lift_lift; [|omega].
f_equal; auto; omega.
rewrite plus_assoc; eauto.
apply WFMu.
apply IHjwf1; tryomega.
apply IHjwf2; tryomega.
apply WFwf with (lift off (a + o) s).
unfold shift; rewrite lift_lift; [|omega].
f_equal; auto; omega.
Qed.
Lemma jwf_lift_0 : ∀ wf o off t,
jwf 0 t wf →
jwf 0 (lift off (S o) t) wf.
Proof.
intros wf o off t H0.
pose proof (jwf_lift wf off t 0 H0 o).
simpl in H; auto.
Qed.
Lemma jwf_subst : ∀ wf xs t a,
jwf a t wf →
∀ o,
jwf a (subst xs (a + S o) t) wf.
Proof.
induction 1; simpl; intros; [subst_lift_var|..]; eauto using jwf.
apply WFFor with (subst xs (d + a + o) s12s).
unfold shift; rewrite lift_subst1.
f_equal; auto; omega.
rewrite plus_assoc; eauto.
apply WFMu.
apply IHjwf1; tryomega.
apply IHjwf2; tryomega.
apply WFwf with (subst xs (a + o) s).
unfold shift; rewrite lift_subst1.
f_equal; auto; omega.
Qed.
Lemma jwf_subst_0 : ∀ wf i xs t,
jwf 0 t wf →
jwf 0 (subst xs (S i) t) wf.
Proof.
intros wf i xs t H.
pose proof (jwf_subst wf xs t 0 H).
simpl in H0; auto.
Qed.
Lemma jerasable_weak_coer : ∀ M H iHH iZZ dZ Z t e,
jerasable M iHH iZZ t e →
∀ iH iZ idZ,
iHH = iH + H →
iZZ = iZ ++ dmap (lift iH 0) Z →
idZ = iZ ++ dmap (lift iH 0) (dZ ++ Z) →
jerasable M iHH idZ t e.
Proof.
induction 1; simpl; intros; eauto using jerasable.
apply JTFor with dZ0 wits vecs; auto.
apply IHjerasable1 with (dH + iH) (dmap (lift dH 0) iZ); tryomega.
apply IHjerasable2 with (dH + iH) (dZ0 ++ dmap (lift dH 0) iZ); tryomega.
apply IHjerasable3 with iH iZ; tryomega.
apply IHjerasable4 with iH iZ; tryomega.
apply JTMu; auto.
apply IHjerasable with (1 + iH) (dmap (lift 1 0) iZ); tryomega.
apply JCTrans with t2; auto.
apply IHjerasable1 with (dH2 + iH) (dZ2 ++ dmap (lift dH2 0) iZ); tryomega.
apply IHjerasable2 with iH iZ; tryomega.
apply JCArr; try intro m; auto.
apply (H2 m) with (dH + iH) (dZ0 ++ dmap (lift dH 0) iZ); clear m; tryomega.
apply (H4 m) with (dH + iH) (dZ0 ++ dmap (lift dH 0) iZ); clear m; tryomega.
apply IHjerasable1 with iH iZ; tryomega.
apply IHjerasable2 with (dH + iH) (dZ0 ++ dmap (lift dH 0) iZ); tryomega.
apply IHjerasable3 with iH iZ; tryomega.
apply JCProd; try intro m; auto.
apply (H2 m) with (dH + iH) (dZ0 ++ dmap (lift dH 0) iZ); clear m; tryomega.
apply (H4 m) with (dH + iH) (dZ0 ++ dmap (lift dH 0) iZ); clear m; tryomega.
apply IHjerasable1 with iH iZ; tryomega.
apply IHjerasable2 with iH iZ; tryomega.
destruct (le_gt_dec (length Y0 + length iZ) c).
apply JCVar with (length dZ + c).
intros m; apply (H2 m) with iH iZ; clear m; tryomega.
intros m; apply (H4 m) with iH iZ; clear m; tryomega.
subst; rewrite <- dmap_app.
rewrite app_nth2 in × by omega.
rewrite app_nth2 in × by omega.
assert (length (dmap (lift iH 0) dZ) = length dZ) by tryomega.
rewrite app_nth2 by omega.
rewrite <- H5.
f_equal.
unfold dmap; rewrite map_length.
apply omega_shit_0.
apply JCVar with c.
intros m; apply (H2 m) with iH iZ; clear m; tryomega.
intros m; apply (H4 m) with iH iZ; clear m; tryomega.
subst.
rewrite app_assoc.
rewrite app_assoc in H5.
rewrite app_nth1; [|rewrite app_length; omega].
rewrite app_nth1 in H5; [assumption|rewrite app_length; omega].
apply JCGen with wits vecs; auto.
intros m. apply (H2 m) with iH iZ; clear m; tryomega.
apply IHjerasable1 with (dH + iH) (dmap (lift dH 0) iZ); tryomega.
apply IHjerasable2 with iH iZ; tryomega.
apply IHjerasable3 with iH iZ; tryomega.
Qed.
Lemma jerasable_weak_coer_0 : ∀ {M H dZ Z t e},
jerasable M H Z t e →
jerasable M H (dZ ++ Z) t e.
Proof. intros; apply jerasable_weak_coer with H Z dZ Z 0 nil; tryomega. Qed.
Definition Incf f Y Z :=
∀ c, nth c Y (Top, Top) = nth (f c) Z (Top, Top).
Hint Unfold Incf.
Lemma Incf_lift : ∀ f H Y Z,
Incf f Y Z → Incf f (dmap (lift H 0) Y) (dmap (lift H 0) Z).
Proof.
intros; intros c; pose proof (H0 c); unfold dmap.
replace (Top, Top) with (pmap (lift H 0) (Top, Top)) by reflexivity.
repeat rewrite map_nth.
rewrite H1; reflexivity.
Qed.
Lemma Incf_app : ∀ {f0 f1 Y0 Z0 Y1 Z1},
Incf f0 Y0 Z0 → Incf f1 Y1 Z1 → ∃ f, Incf f (Y0 ++ Y1) (Z0 ++ Z1).
Proof.
intros.
∃ (fun c ⇒ match le_gt_dec (length Y0) c with
| left _ ⇒ f1 (c - length Y0) + length Z0
| right _ ⇒
match le_gt_dec (length Z0) (f0 c) with
| left _ ⇒ f0 c + length Z1
| right _ ⇒ f0 c
end
end).
intros c.
destruct (le_gt_dec (length Y0) c).
repeat (rewrite app_nth2; [|omega]).
pose proof (H0 (c - length Y0)); rewrite H1.
f_equal; omega.
rewrite app_nth1; [|omega].
pose proof (H c); rewrite H1.
destruct (le_gt_dec (length Z0) (f0 c)).
rewrite app_nth2; [|omega].
repeat (rewrite nth_overflow; [|omega]).
reflexivity.
rewrite app_nth1; [|omega].
reflexivity.
Qed.
Lemma Incf_refl : ∀ Z, Incf (fun c ⇒ c) Z Z.
Proof. intros Z c; auto. Qed.
Lemma jcoer_weak_coerY : ∀ M H dH dZ Y0 Y1 Z t,
jerasable M H Z t (Scoer Y0 Y1 dH dZ) →
∀ f0 f1 Y0' Y1',
Incf f0 Y0 Y0' → Incf f1 Y1 Y1' →
jerasable M H Z t (Scoer Y0' Y1' dH dZ).
Proof.
intros M H dH dZ Y0 Y1 Z t HZt.
remember (Scoer Y0 Y1 dH dZ) as e.
generalize Y0 Y1 dH dZ Heqe; clear Y0 Y1 dH dZ Heqe;
induction HZt; intros ? ? ? ? Heqe; inversion Heqe; subst;
simpl; intros; eauto using jerasable.
apply JCTrans with t2; auto.
apply IHHZt1 with (dmap (lift dH2 0) Y2) (dmap (lift dH2 0) Y3) f0 f1; tryomega;
apply Incf_lift; auto.
apply IHHZt2 with Y2 Y3 f0 f1; tryomega.
destruct (Incf_app H5 H4) as [f ?].
pose proof (Incf_refl nil).
apply JCArr; auto.
apply IHHZt2 with (dmap (lift dH0 0) (Y3 ++ Y2)) nil f (fun c ⇒ c); tryomega.
repeat (rewrite dmap_app); apply Incf_lift; auto.
apply IHHZt3 with (Y3 ++ Y2) nil f (fun c ⇒ c); tryomega.
destruct (Incf_app H5 H4) as [f ?].
pose proof (Incf_refl nil).
apply JCProd; auto.
apply IHHZt1 with (Y3 ++ Y2) nil f (fun c ⇒ c); tryomega.
apply IHHZt2 with (Y3 ++ Y2) nil f (fun c ⇒ c); tryomega.
pose proof (Incf_refl Z).
destruct (Incf_app H5 H7) as [f ?].
apply JCVar with (f c); auto.
rewrite H8 in H4; auto.
apply JCGen with wits vecs; subst; auto.
apply JCFix.
intros m; apply (H0 m).
pose proof (Incf_refl ((t, s) :: nil)).
destruct (Incf_app H4 H3) as [f ?].
apply IHHZt with Y2 ((t, s) :: Y3) f0 f; tryomega.
Qed.
Lemma Incf_nil : ∀ Z, ∃ f, Incf f nil Z.
Proof.
intros.
∃ (fun c ⇒ length Z).
intros c.
repeat (rewrite nth_overflow; [|simpl; omega]).
reflexivity.
Qed.
Lemma jcoer_weak_coerY_0 : ∀ M H Z Y0 Y1 dH dZ t,
jerasable M H Z t (Scoer nil nil dH dZ) →
jerasable M H Z t (Scoer Y0 Y1 dH dZ).
Proof.
intros M H Z Y0 Y1 dH dZ t HZt.
destruct (Incf_nil Y0) as [f0 ?].
destruct (Incf_nil Y1) as [f1 ?].
pose proof (jcoer_weak_coerY M H dH dZ nil nil Z t HZt f0 f1 Y0 Y1); auto.
Qed.
Lemma jerasable_lift : ∀ M off iZZ iHH H Z t e,
jerasable M iHH iZZ t e →
∀ iH iZ ioH ioZ,
iHH = iH + H →
iZZ = iZ ++ dmap (lift iH 0) Z →
ioH = iH + off + H →
ioZ = dmap (lift off iH) iZZ →
jerasable M ioH ioZ (lift off iH t) (elift off iH e).
Proof.
induction 1; simpl; intros; eauto using jerasable.
apply JTFor with (dmap (lift off (dH + iH)) dZ)
(lift off iH wits) (map (lift off iH) vecs); tryomega;
try (apply extract_lift; auto).
apply IHjerasable1 with (dmap (lift (length vecs) 0) iZ); tryomega.
apply IHjerasable2 with (dZ ++ dmap (lift (length vecs) 0) iZ); tryomega.
apply IHjerasable3 with iZ; tryomega.
rewrite <- lift_subst2_0.
apply IHjerasable4 with iZ; tryomega.
apply JTMu.
subst; apply jwf_lift_0; assumption.
apply IHjerasable with (dmap (lift 1 0) iZ); tryomega.
rewrite <- dmap_app; rewrite <- plus_assoc; rewrite <- dmap_lift_lift; [|omega].
apply JCTrans with (lift off (dH2 + iH) t2).
rewrite (dmap_lift_lift Y0); [|omega].
rewrite (dmap_lift_lift Y1); [|omega].
apply IHjerasable1 with (dZ2 ++ dmap (lift dH2 0) iZ); tryomega.
apply IHjerasable2 with iZ; tryomega.
apply JCWeak with dH (dmap (lift off (dH + iH)) dZ).
intros m; apply (H2 m) with iZ; tryomega.
simpl in IHjerasable; rewrite lift_lift; [|omega].
apply IHjerasable with iZ; tryomega.
apply JCArr.
intros M2M; apply (H2 M2M) with (dZ ++ dmap (lift dH 0) iZ); tryomega.
intros M2M; apply (H4 M2M) with (dZ ++ dmap (lift dH 0) iZ); tryomega.
apply IHjerasable1 with iZ; tryomega.
simpl in IHjerasable2; trysimpl.
rewrite lift_lift; [|omega].
rewrite (dmap_lift_lift Y0); [|omega].
rewrite (dmap_lift_lift Y1); [|omega].
rewrite dmap_app.
apply IHjerasable2 with (dZ ++ dmap (lift dH 0) iZ); tryomega.
rewrite dmap_app.
apply IHjerasable3 with iZ; tryomega.
apply JCProd.
intros M2M; apply (H2 M2M) with (dZ ++ dmap (lift dH 0) iZ); tryomega.
intros M2M; apply (H4 M2M) with (dZ ++ dmap (lift dH 0) iZ); tryomega.
rewrite dmap_app; apply IHjerasable1 with iZ; tryomega.
rewrite dmap_app; apply IHjerasable2 with iZ; tryomega.
apply JCVar with c.
intros M1M; apply (H2 M1M) with iZ; tryomega.
intros M1M; apply (H4 M1M) with iZ; tryomega.
subst; rewrite dmap_app; unfold dmap in ×.
replace (Top, Top) with (pmap (lift off iH) (Top, Top)) by reflexivity.
rewrite map_nth.
rewrite H5; reflexivity.
apply JCGen with (lift off iH wits) (map (lift off iH) vecs); tryomega;
try (apply extract_lift; auto).
intros M1M; apply (H2 M1M) with iZ; tryomega.
apply IHjerasable1 with (dmap (lift (length vecs) 0) iZ); tryomega.
apply IHjerasable2 with iZ; tryomega.
rewrite <- lift_subst2_0.
apply IHjerasable3 with iZ; tryomega.
rewrite lift_subst2_0. subst dH.
apply JCInst with (lift off iH insts); try (apply extract_lift; auto); tryomega.
intros M1M; apply (H2 M1M) with iZ; tryomega.
apply IHjerasable1 with iZ; tryomega.
rewrite <- lift_subst2_0.
apply IHjerasable2 with iZ; tryomega.
unfold subst1 in *; rewrite lift_subst2_0.
apply JCUnfold.
intros M1M; apply (H2 M1M) with iZ; tryomega.
intros m; subst; apply jwf_lift_0; auto.
unfold subst1 in *; rewrite lift_subst2_0; simpl.
apply JCFold with (t := lift off (S iH) t).
apply IHjerasable with iZ; tryomega.
apply JCFix.
intros m; apply (H2 m) with iZ; tryomega.
apply IHjerasable with iZ; tryomega.
Qed.
Lemma jerasable_lift_0 : ∀ {M dH H Z t} e,
jerasable M H Z t e →
∀ ee, ee = elift dH 0 e →
jerasable M (dH + H) (dmap (lift dH 0) Z) (lift dH 0 t) ee.
Proof.
intros; subst.
apply jerasable_lift with Z H H Z nil; tryomega.
Qed.
Lemma jerasable_nth : ∀ M H Z e xs a,
a < length xs →
jerasable M H Z (inject Slisttype xs) (Slist e) →
jerasable M H Z (nth a xs Top) e.
Proof.
induction xs; intros; [inversion H0|].
destruct a0; simpl in *; inversion H1; auto.
apply IHxs; auto; omega.
Qed.
Lemma jerasable_nth_subst : ∀ M H Z xs dZ c t s,
jerasable M H Z (subst xs 0 (inject Slistprodtype dZ)) Slistcoer →
c < length dZ →
nth c dZ (Top, Top) = (t, s) →
jerasable M H Z (subst xs 0 (Spair 0 t s)) (Scoer nil nil 0 nil).
Proof.
induction dZ; intros; [inversion H1|].
destruct a as [t0 s0].
destruct c; inversion H2; subst; [inversion H0; auto|].
simpl in H1.
apply IHdZ with c; auto.
inversion H0; auto.
omega.
Qed.
Lemma jerasable_subst : ∀ M H Z xs dH dZ t e idH idZ,
dH = length xs →
jerasable M H Z (inject Slisttype xs) Slisttype →
jerasable M H Z (subst xs 0 (inject Slistprodtype dZ)) Slistcoer →
jerasable M idH idZ t e →
∀ iH iZ iHH iZZ,
idH = iH + dH + H →
idZ = iZ ++ dmap (lift iH 0) dZ ++ dmap (lift (iH + dH) 0) Z →
iHH = iH + H →
iZZ = dmap (subst xs iH) iZ ++ dmap (lift iH 0) Z →
jerasable M iHH iZZ (subst xs iH t) (esubst xs iH e).
Proof.
induction 4; simpl; intros; eauto using jerasable.
subst_lift_var; try apply JTVar; subst.
apply jerasable_weak_coer_0.
apply jerasable_lift_0 with Stype; auto.
apply jerasable_nth; auto; omega.
apply JTFor with (dZ := dmap (subst xs (dH0 + iH)) dZ0)
(wits := subst xs iH wits)
(vecs := map (subst xs iH) vecs); tryomega;
try (apply extract_subst; auto).
apply IHjerasable1 with (dmap (lift (length vecs) 0) iZ); tryomega.
apply IHjerasable2 with (dZ0 ++ dmap (lift (length vecs) 0) iZ); tryomega.
apply IHjerasable3 with iZ; tryomega.
rewrite <- subst_subst_0.
apply IHjerasable4 with iZ; tryomega.
apply JTMu.
subst; apply jwf_subst_0; assumption.
apply IHjerasable with (dmap (lift 1 0) iZ); tryomega.
rewrite <- dmap_app; rewrite <- plus_assoc; rewrite <- dmap_lift_subst1.
apply JCTrans with (subst xs (dH2 + iH) t2).
rewrite (dmap_lift_subst1 Y0).
rewrite (dmap_lift_subst1 Y1).
apply IHjerasable1 with (dZ2 ++ dmap (lift dH2 0) iZ); tryomega.
apply IHjerasable2 with iZ; tryomega.
apply JCWeak with dH0 (dmap (subst xs (dH0 + iH)) dZ0).
intros M1M; apply (H5 M1M) with iZ; tryomega.
simpl in IHjerasable; rewrite lift_subst1_0.
apply IHjerasable with iZ; tryomega.
apply JCArr.
intros M2M; apply (H5 M2M) with (dZ0 ++ dmap (lift dH0 0) iZ); tryomega.
intros M2M; apply (H7 M2M) with (dZ0 ++ dmap (lift dH0 0) iZ); tryomega.
apply IHjerasable1 with iZ; tryomega.
simpl in IHjerasable2; trysimpl.
rewrite lift_subst1_0.
rewrite (dmap_lift_subst1 Y0).
rewrite (dmap_lift_subst1 Y1).
rewrite dmap_app.
apply IHjerasable2 with (dZ0 ++ dmap (lift dH0 0) iZ); tryomega.
rewrite dmap_app.
apply IHjerasable3 with iZ; tryomega.
apply JCProd.
intros M2M; apply (H5 M2M) with (dZ0 ++ dmap (lift dH0 0) iZ); tryomega.
intros M2M; apply (H7 M2M) with (dZ0 ++ dmap (lift dH0 0) iZ); tryomega.
rewrite dmap_app; apply IHjerasable1 with iZ; tryomega.
rewrite dmap_app; apply IHjerasable2 with iZ; tryomega.
destruct (le_gt_dec (length (Y0 ++ iZ)) c);
[destruct (le_gt_dec (length (Y0 ++ iZ) + length dZ) c)|].
apply JCVar with (c - length dZ).
intros M1M; apply (H5 M1M) with iZ; tryomega.
intros M1M; apply (H7 M1M) with iZ; tryomega.
subst; rewrite app_assoc; rewrite dmap_app; unfold dmap in ×.
rewrite app_nth2; [|rewrite map_length; omega].
rewrite app_assoc in H8;
rewrite app_nth2 in H8; [|repeat rewrite map_length; omega].
rewrite app_nth2 in H8; [|repeat rewrite map_length; omega].
repeat rewrite map_length in ×.
replace (Top, Top) with (pmap (lift iH 0) (Top, Top)) by reflexivity.
rewrite map_nth.
replace (Top, Top) with (pmap (lift (iH + length xs) 0) (Top, Top)) in H8 by reflexivity.
rewrite map_nth in H8.
fold (pmap (subst xs iH) (t, s)).
rewrite <- H8.
rewrite omega_shit_1.
destruct (nth (c - length (Y0 ++ iZ) - length dZ)).
simpl.
repeat rewrite subst_lift; try omega.
replace (iH + length xs - length xs) with iH by omega.
reflexivity.
replace (Spair 0 (subst xs iH t) (subst xs iH s)) with (subst xs iH (Spair 0 t s)) by reflexivity.
clear H4 H5 H6 H7; subst.
rewrite app_assoc in H8; rewrite app_nth2 in H8; try omega.
unfold dmap in H8.
rewrite app_nth1 in H8; try (repeat rewrite map_length; omega).
replace (Top, Top) with (pmap (lift iH 0) (Top, Top)) in H8 by reflexivity.
rewrite map_nth in H8.
apply jerasable_weak_coer_0.
remember (nth (c - length (Y0 ++ iZ)) dZ (Top, Top)) as ts0.
destruct ts0 as [t0 s0].
simpl in H8; inversion H8; clear H8; subst.
replace (Spair 0 (lift iH 0 t0) (lift iH 0 s0)) with (lift iH 0 (Spair 0 t0 s0)) by reflexivity.
replace (subst xs iH (lift iH 0 (Spair 0 t0 s0))) with (lift iH 0 (subst xs 0 (Spair 0 t0 s0)))
by (rewrite lift_subst1_0; f_equal; omega).
apply jcoer_weak_coerY_0.
apply jerasable_lift_0 with (Scoer nil nil 0 nil); auto.
apply jerasable_nth_subst with dZ (c - length (Y0 ++ iZ)); auto.
omega.
apply JCVar with c.
intros M1M; apply (H5 M1M) with iZ; tryomega.
intros M1M; apply (H7 M1M) with iZ; tryomega.
clear H1 H2 H4 H5 H6 H7.
subst; rewrite app_assoc; rewrite dmap_app; unfold dmap in ×.
rewrite app_nth1; [|rewrite map_length; omega].
rewrite app_assoc in H8; rewrite app_nth1 in H8; [|repeat rewrite map_length; omega].
replace (Top, Top) with (pmap (subst xs iH) (Top, Top)) by reflexivity.
rewrite map_nth.
rewrite H8.
reflexivity.
apply JCGen with (subst xs iH wits) (map (subst xs iH) vecs); tryomega;
try (apply extract_subst; auto).
intros M1M; apply (H5 M1M) with iZ; tryomega.
apply IHjerasable1 with (dmap (lift (length vecs) 0) iZ); tryomega.
apply IHjerasable2 with iZ; tryomega.
rewrite <- subst_subst_0.
apply IHjerasable3 with iZ; tryomega.
rewrite subst_subst_0. subst dH0.
apply JCInst with (subst xs iH insts); try (apply extract_subst; auto); tryomega.
intros M1M; apply (H5 M1M) with iZ; tryomega.
apply IHjerasable1 with iZ; tryomega.
rewrite <- subst_subst_0.
apply IHjerasable2 with iZ; tryomega.
unfold subst1 in *; rewrite subst_subst_0.
apply JCUnfold.
intros M1M; apply (H5 M1M) with iZ; tryomega.
intros m; subst; apply jwf_subst_0; auto.
unfold subst1 in *; rewrite subst_subst_0.
apply JCFold with (t := subst xs (S iH) t).
apply IHjerasable with iZ; tryomega.
apply JCFix; auto.
intros m; apply (H5 m) with iZ; tryomega.
apply IHjerasable with iZ; tryomega.
Qed.
Lemma jerasable_subst_0 : ∀ {M H Z xs t} dH dZ e,
jerasable M (dH + H) (dZ ++ dmap (lift dH 0) Z) t e →
dH = length xs →
jerasable M H Z (inject Slisttype xs) Slisttype →
jerasable M H Z (subst xs 0 (inject Slistprodtype dZ)) Slistcoer →
∀ ee, ee = esubst xs 0 e →
jerasable M H Z (subst xs 0 t) ee.
Proof.
intros; subst ee.
apply jerasable_subst with H Z dH dZ (dH + H) (dZ ++ dmap (lift dH 0) Z) nil; tryomega.
Qed.
Lemma jcoer_extract_jerasable_env : ∀ M H Z Y0 Y1 dH dZ t s,
jerasable M H Z (Spair dH t s) (Scoer Y0 Y1 dH dZ) →
jerasable_env M H Z →
jerasable_env M (dH + H) (dZ ++ dmap (lift dH 0) Z).
Proof.
intros M H Z Y0 Y1 dH dZ t s jH.
remember (Spair dH t s) as ts.
remember (Scoer Y0 Y1 dH dZ) as e.
generalize t s Y0 Y1 dH dZ Heqts Heqe; clear t s Y0 Y1 dH dZ Heqts Heqe.
induction jH; intros; first [discriminate Heqts|discriminate Heqe|idtac];
inversion Heqts; inversion Heqe; clear Heqts Heqe; subst; trysimpl; eauto.
rewrite <- plus_assoc.
rewrite <- app_assoc.
rewrite dmap_app.
apply IHjH1 with t t2 (dmap (lift dH2 0) Y2) (dmap (lift dH2 0) Y3); tryomega.
apply IHjH2 with t2 s Y2 Y3; tryomega.
apply JEcons with H Z dH0 dZ0; tryomega.
∃ vecs; repeat split; auto.
rewrite <- (inject_extract H2); auto.
rewrite <- (inject_extract H3); auto.
rewrite <- (inject_extract H2); auto.
Qed.
Lemma jcoer_extract_right_type : ∀ {M H Z Y0 Y1 dH dZ t s}, 1 ≤ M →
jerasable M H Z (Spair dH t s) (Scoer Y0 Y1 dH dZ) →
jerasable M H Z s Stype.
Proof.
intros M H Z Y0 Y1 dH dZ t s M1M jH.
remember (Spair dH t s) as ts.
remember (Scoer Y0 Y1 dH dZ) as e.
generalize t s Y0 Y1 dH dZ Heqts Heqe; clear t s Y0 Y1 dH dZ Heqts Heqe.
induction jH; intros; first [discriminate Heqts|discriminate Heqe|idtac];
inversion Heqts; inversion Heqe; clear Heqts Heqe; subst;
repeat (trysimpl; match goal with
| H1 : 1 ≤ M → _ |- _ ⇒ pose proof (H1 M1M); clear H1
| _ : length ?vecs = ?dH |- _ ⇒ subst dH
| H : extract _ ?t ?x |- context[inject _ ?x]
⇒ rewrite <- (inject_extract H)
| |- jerasable _ _ _ (Arr _ _) _ ⇒ apply JTArr
| |- jerasable _ _ _ (Prod _ _) _ ⇒ apply JTProd
| H1 : jerasable _ _ _ (For _ _ _) _ |- _ ⇒ inversion H1; clear H1; subst
| _ : extract _ ?wits ?vecs
, _ : extract _ ?t12s ?dZ
|- jerasable _ _ _ (For (length ?vecs) ?t12s _) _ ⇒ apply JTFor with dZ wits vecs
| |- jerasable _ _ _ Top _ ⇒ apply JTTop
| H : jerasable _ (length ?vecs + _) (?dZ ++ _) ?t Stype
|- jerasable _ _ _ (subst ?vecs 0 ?t) Stype
⇒ apply jerasable_subst_0 with (length vecs) dZ Stype
end; auto); trysimpl; eauto.
inversion H1; subst.
apply jerasable_subst_0 with 1 nil Stype; simpl in *; eauto using jerasable.
Qed.
Lemma jcoer_extract_left_type : ∀ {M H Z Y0 Y1 dH dZ t s}, 1 ≤ M →
jerasable M H Z (Spair dH t s) (Scoer Y0 Y1 dH dZ) →
jerasable M (dH + H) (dZ ++ dmap (lift dH 0) Z) t Stype.
Proof.
intros M H Z Y0 Y1 dH dZ t s M1M jH.
remember (Spair dH t s) as ts.
remember (Scoer Y0 Y1 dH dZ) as e.
generalize t s Y0 Y1 dH dZ Heqts Heqe; clear t s Y0 Y1 dH dZ Heqts Heqe.
induction jH; intros; first [discriminate Heqts|discriminate Heqe|idtac];
inversion Heqts; inversion Heqe; clear Heqts Heqe; subst;
repeat (trysimpl; match goal with
| H1 : 2 ≤ M → _ |- _ ⇒ clear H1
| H1 : 1 ≤ M → _ |- _ ⇒ pose proof (H1 M1M); clear H1
| Hx : ∀ t0 s0 Y2 Y3 dH0 dZ0,
Spair ?dH ?t ?s = Spair dH0 t0 s0 →
Scoer ?Y0 ?Y1 ?dH ?dZ = Scoer Y2 Y3 dH0 dZ0 →
_ |- _ ⇒ pose proof (Hx t s Y0 Y1 dH dZ eq_refl eq_refl); clear Hx
| |- jerasable _ _ _ (Arr _ _) _ ⇒ apply JTArr
| |- jerasable _ _ _ (Prod _ _) _ ⇒ apply JTProd
| |- jerasable _ _ _ Bot _ ⇒ apply JTBot
| H1 : jerasable _ _ _ (For _ _ _) _ |- _ ⇒ inversion H1; clear H1; subst
| H1 : jerasable _ ?H ?Z (Spair _ _ ?t) (Scoer _ _ _ _)
|- jerasable _ ?H ?Z ?t Stype
⇒ apply (jcoer_extract_right_type M1M H1)
| H1 : extract _ ?t ?x , H2 : extract _ ?t ?y |- _
⇒ rewrite (extract_eq H1 H2); clear H1
end; auto); trysimpl; eauto.
inversion jH; subst.
apply jerasable_subst_0 with 1 nil Stype; simpl in *; eauto using jerasable.
Qed.
Require Import List.
Require Import Equality.
Require Import ext.
Require Import list.
Inductive type : Set :=
| Var (x : nat)
| Arr (t : type) (s : type)
| Prod (t : type) (s : type)
| For (d : nat) (t12s : type) (t : type)
| Mu (t : type)
| Bot
| Top
| Snil
| Scons (t : type) (ts : type)
| Spair (d : nat) (t1 : type) (t2 : type)
.
Definition Var_a := Var.
Hint Unfold Var_a.
Definition traverse f := fix g i t :=
match t with
| Var a ⇒ f a i
| Arr t s ⇒ Arr (g i t) (g i s)
| Prod t s ⇒ Prod (g i t) (g i s)
| For d t12s r ⇒ For d (g (d + i) t12s) (g (d + i) r)
| Mu t ⇒ Mu (g (1 + i) t)
| Bot ⇒ Bot
| Top ⇒ Top
| Snil ⇒ Snil
| Scons t ts ⇒ Scons (g i t) (g i ts)
| Spair d t1 t2 ⇒ Spair d (g (d + i) t1) (g i t2)
end.
Definition lift_idx d a i := Var (if le_gt_dec i a then d + a else a).
Definition lift d := traverse (lift_idx d).
Definition shift := lift 1.
Hint Unfold lift_idx lift shift.
Definition subst_idx vecs a i :=
match le_gt_dec i a with
| right _ ⇒ Var a
| left _ ⇒
match le_gt_dec (i + length vecs) a with
| right _ ⇒ lift i 0 (nth (a - i) vecs Top)
| left _ ⇒ Var (a - length vecs)
end
end.
Definition subst vecs := traverse (subst_idx vecs).
Hint Unfold subst_idx subst.
Definition subst1 s i t := subst (s :: nil) i t.
Ltac subst_lift_var := repeat first
[ rewrite app_length in ×
| rewrite map_length in ×
| match goal with
| |- context[subst_idx] ⇒ unfold subst_idx
| |- context[lift_idx] ⇒ unfold lift_idx
| |- context[le_gt_dec ?x ?y] ⇒ destruct (le_gt_dec x y); try (exfalso; omega); simpl; auto
end ].
Notation type_env := nat.
Definition coer_env := list (type × type).
Definition pmap (f : type → type) xy :=
match xy with
| (x, y) ⇒ (f x, f y)
end.
Definition dmap (f : type → type) xs := map (pmap f) xs.
Hint Unfold pmap dmap.
Definition term_env := list type.
Inductive sort : Set :=
| Stype
| Sprod (e1 : sort) (e2 : sort)
| Slist (e : sort)
| Scoer (Y0 Y1 : coer_env) (dH : type_env) (dZ : coer_env)
.
Notation Sprodtype := (Sprod Stype Stype).
Notation Slistprodtype := (Slist Sprodtype).
Notation Slisttype := (Slist Stype).
Notation Slistcoer := (Slist (Scoer nil nil 0 nil)).
Fixpoint sort_type e :=
match e with
| Stype ⇒ type
| Sprod e1 e2 ⇒ prod (sort_type e1) (sort_type e2)
| Slist e ⇒ list (sort_type e)
| Scoer _ _ _ _ ⇒ prod type type
end.
Inductive extract : ∀ (e : sort), type → sort_type e → Prop :=
| Etype : ∀ t, extract Stype t t
| Enil : ∀ e, extract (Slist e) Snil nil
| Econs : ∀ e t ts x xs,
extract e t x →
extract (Slist e) ts xs →
extract (Slist e) (Scons t ts) (x :: xs)
| Epair : ∀ e1 e2 t1 t2 x1 x2,
extract e1 t1 x1 →
extract e2 t2 x2 →
extract (Sprod e1 e2) (Spair 0 t1 t2) (x1, x2)
| Ecoer : ∀ dH dZ Y0 Y1 t s,
extract (Scoer Y0 Y1 dH dZ) (Spair dH t s) (t, s)
.
Tactic Notation "dep" hyp(H) :=
do_depelim' ltac:(fun hyp ⇒ idtac) ltac:(fun hyp ⇒ do_case hyp) H.
Ltac destruct_extract := repeat
match goal with
| H : extract Stype _ _ |- _ ⇒ dep H
| H : extract _ ?x _ |- _ ⇒ (is_var x; fail 1) || dep H
| H : extract _ _ ?x |- _ ⇒ (is_var x; fail 1) || dep H
end.
Lemma extract_eq : ∀ {e t x y}, extract e t x → extract e t y → x = y.
Proof. induction 1; intros Hy; dep Hy; first [reflexivity|f_equal; auto]. Qed.
Lemma extract_inj : ∀ {e t x}, extract e t x → ∀ {s}, extract e s x → t = s.
Proof. induction 1; intros ? Hy; dep Hy; first [reflexivity|f_equal; auto]. Qed.
Definition inj_list A (inj : A → type) := fix f xs :=
match xs with
| nil ⇒ Snil
| cons x xs ⇒ Scons (inj x) (f xs)
end.
Fixpoint inject e (x : sort_type e) : type :=
match e return sort_type e → type with
| Stype ⇒ fun x ⇒ x
| Sprod e1 e2 ⇒ fun x ⇒
match x with
| (x1, x2) ⇒ Spair 0 (inject e1 x1) (inject e2 x2)
end
| Slist e ⇒ inj_list (sort_type e) (inject e)
| Scoer Y0 Y1 dH dZ ⇒ fun x ⇒
match x with
| (t, s) ⇒ Spair dH t s
end
end x.
Hint Unfold inj_list inject.
Lemma extract_inject : ∀ e x, extract e (inject e x) x.
Proof.
induction e; intros; simpl.
apply Etype.
destruct x as [x1 x2].
apply Epair; auto.
induction x as [|x xs]; [apply Enil|].
apply Econs; auto.
destruct x.
apply Ecoer.
Qed.
Lemma inject_extract : ∀ {e x t}, extract e t x → t = inject e x.
Proof.
intros.
apply (extract_inj H).
apply extract_inject.
Qed.
Inductive wfsort := WF | NE.
Inductive jwf : type_env → type → wfsort → Prop :=
| WFVar : ∀ a, jwf a (Var_a a) NE
| WFArr : ∀ a t s, jwf a t NE → jwf a s NE → jwf a (Arr t s) WF
| WFProd : ∀ a t s, jwf a t NE → jwf a s NE → jwf a (Prod t s) WF
| WFFor : ∀ wf a d t12s s12s t, t12s = shift (d + a) s12s →
jwf (d + a) t wf → jwf a (For d t12s t) wf
| WFMu : ∀ wf a t, jwf 0 t WF → jwf (1 + a) t wf → jwf a (Mu t) wf
| WFwf : ∀ a t s, t = shift a s → jwf a t WF
| WFne : ∀ a t, jwf a t WF → jwf a t NE
.
Inductive jerasable M : type_env → coer_env → type → sort → Prop :=
| JTVar : ∀ H Z n,
jerasable M H Z (Var n) Stype
| JTArr : ∀ H Z t s,
jerasable M H Z t Stype →
jerasable M H Z s Stype →
jerasable M H Z (Arr t s) Stype
| JTProd : ∀ H Z t s,
jerasable M H Z t Stype →
jerasable M H Z s Stype →
jerasable M H Z (Prod t s) Stype
| JTFor : ∀ H Z dH dZ t12s wits vecs t,
extract Slistprodtype t12s dZ →
extract Slisttype wits vecs →
length vecs = dH →
jerasable M (dH + H) (dmap (lift dH 0) Z) t12s Slistprodtype →
jerasable M (dH + H) (dZ ++ (dmap (lift dH 0) Z)) t Stype →
jerasable M H Z wits Slisttype →
jerasable M H Z (subst vecs 0 t12s) Slistcoer →
jerasable M H Z (For dH t12s t) Stype
| JTMu : ∀ H Z t,
jwf 0 t WF →
jerasable M (1 + H) (dmap (lift 1 0) Z) t Stype →
jerasable M H Z (Mu t) Stype
| JTBot : ∀ H Z,
jerasable M H Z Bot Stype
| JTTop : ∀ H Z,
jerasable M H Z Top Stype
| JSNil : ∀ H Z e,
jerasable M H Z Snil (Slist e)
| JSCons : ∀ H Z t ts e,
jerasable M H Z t e →
jerasable M H Z ts (Slist e) →
jerasable M H Z (Scons t ts) (Slist e)
| JSPair : ∀ H Z t1 t2 e1 e2,
jerasable M H Z t1 e1 →
jerasable M H Z t2 e2 →
jerasable M H Z (Spair 0 t1 t2) (Sprod e1 e2)
| JCRefl : ∀ H Z Y0 Y1 t,
(1 ≤ M → jerasable M H Z t Stype) →
jerasable M H Z (Spair 0 t t) (Scoer Y0 Y1 0 nil)
| JCTrans : ∀ dH1 dH2 H dZ1 dZ2 Z Y0 Y1 t1 t2 t3,
jerasable M (dH2 + H) (dZ2 ++ (dmap (lift dH2 0) Z)) (Spair dH1 t1 t2)
(Scoer (dmap (lift dH2 0) Y0) (dmap (lift dH2 0) Y1) dH1 dZ1) →
jerasable M H Z (Spair dH2 t2 t3) (Scoer Y0 Y1 dH2 dZ2) →
jerasable M H Z (Spair (dH1 + dH2) t1 t3) (Scoer Y0 Y1 (dH1 + dH2) (dZ1 ++ (dmap (lift dH1 0) dZ2)))
| JCWeak : ∀ dH H dZ Z Y0 Y1 t s,
(1 ≤ M → jerasable M H Z t Stype) →
jerasable M H Z (Spair dH (lift dH 0 t) s) (Scoer Y0 Y1 dH dZ) →
jerasable M H Z (Spair 0 t s) (Scoer Y0 Y1 0 nil)
| JCArr : ∀ dH H dZ Z Y0 Y1 t' s' t s,
(2 ≤ M → jerasable M (dH + H) (dZ ++ (dmap (lift dH 0) Z)) t' Stype) →
(2 ≤ M → jerasable M (dH + H) (dZ ++ (dmap (lift dH 0) Z)) s' Stype) →
jerasable M H Z t Stype →
jerasable M (dH + H) (dZ ++ (dmap (lift dH 0) Z)) (Spair 0 (lift dH 0 t) t')
(Scoer (dmap (lift dH 0) (Y1 ++ Y0)) nil 0 nil) →
jerasable M H Z (Spair dH s' s) (Scoer (Y1 ++ Y0) nil dH dZ) →
jerasable M H Z (Spair dH (Arr t' s') (Arr t s)) (Scoer Y0 Y1 dH dZ)
| JCProd : ∀ dH H dZ Z Y0 Y1 t' s' t s,
(2 ≤ M → jerasable M (dH + H) (dZ ++ (dmap (lift dH 0) Z)) t' Stype) →
(2 ≤ M → jerasable M (dH + H) (dZ ++ (dmap (lift dH 0) Z)) s' Stype) →
jerasable M H Z (Spair dH t' t) (Scoer (Y1 ++ Y0) nil dH dZ) →
jerasable M H Z (Spair dH s' s) (Scoer (Y1 ++ Y0) nil dH dZ) →
jerasable M H Z (Spair dH (Prod t' s') (Prod t s)) (Scoer Y0 Y1 dH dZ)
| JCVar : ∀ H Z Y0 Y1 c t s,
(1 ≤ M → jerasable M H Z t Stype) →
(1 ≤ M → jerasable M H Z s Stype) →
nth c (Y0 ++ Z) (Top, Top) = (t, s) →
jerasable M H Z (Spair 0 t s) (Scoer Y0 Y1 0 nil)
| JCGen : ∀ dH H dZ Z Y0 Y1 t12s wits vecs t,
(1 ≤ M → jerasable M H Z (For dH t12s t) Stype) →
extract Slistprodtype t12s dZ →
extract Slisttype wits vecs →
length vecs = dH →
jerasable M (dH + H) (dmap (lift dH 0) Z) t12s Slistprodtype →
jerasable M H Z wits Slisttype →
jerasable M H Z (subst vecs 0 t12s) Slistcoer →
jerasable M H Z (Spair dH t (For dH t12s t)) (Scoer Y0 Y1 dH dZ)
| JCInst : ∀ dH H Z Y0 Y1 t12s t insts vecs,
(1 ≤ M → jerasable M H Z (For dH t12s t) Stype) →
extract Slisttype insts vecs →
length vecs = dH →
jerasable M H Z insts Slisttype →
jerasable M H Z (subst vecs 0 t12s) Slistcoer →
jerasable M H Z (Spair 0 (For dH t12s t) (subst vecs 0 t)) (Scoer Y0 Y1 0 nil)
| JCUnfold : ∀ H Z Y0 Y1 t,
(1 ≤ M → jerasable M H Z (Mu t) Stype) →
(M ≠ 1 → jwf 0 t WF) →
jerasable M H Z (Spair 0 (Mu t) (subst1 (Mu t) 0 t)) (Scoer Y0 Y1 0 nil)
| JCFold : ∀ H Z Y0 Y1 t,
jerasable M H Z (Mu t) Stype →
jerasable M H Z (Spair 0 (subst1 (Mu t) 0 t) (Mu t)) (Scoer Y0 Y1 0 nil)
| JCFix : ∀ H Z Y0 Y1 t s,
(M ≠ 1 → jerasable M H Z s Stype) →
jerasable M H Z (Spair 0 t s) (Scoer Y0 ((t, s) :: Y1) 0 nil) →
jerasable M H Z (Spair 0 t s) (Scoer Y0 Y1 0 nil)
| JCBot : ∀ H Z Y0 Y1 t,
jerasable M H Z t Stype →
jerasable M H Z (Spair 0 Bot t) (Scoer Y0 Y1 0 nil)
| JCTop : ∀ H Z Y0 Y1 t,
(1 ≤ M → jerasable M H Z t Stype) →
jerasable M H Z (Spair 0 t Top) (Scoer Y0 Y1 0 nil)
.
Definition jtype M H Z t := jerasable M H Z t Stype.
Definition jcoer M H Z Y0 Y1 dH dZ t s := jerasable M H Z (Spair dH t s) (Scoer Y0 Y1 dH dZ).
Hint Unfold jtype jcoer.
Ltac jerasable_induction H :=
induction H; intros;
[ apply JTVar
| apply JTArr
| apply JTProd
| eapply JTFor
| apply JTMu
| apply JTBot
| apply JTTop
| apply JSNil
| apply JSCons
| apply JSPair
| apply JCRefl
| eapply JCTrans
| eapply JCWeak
| apply JCArr
| apply JCProd
| eapply JCVar
| eapply JCGen
| eapply JCInst
| apply JCUnfold
| apply JCFold
| apply JCFix
| apply JCBot
| apply JCTop].
Definition jerasable_bind M H Z dH dZ := ∃ vecs,
length vecs = dH ∧
jerasable M (dH + H) (dmap (lift dH 0) Z) (inject Slistprodtype dZ) Slistprodtype ∧
jerasable M H Z (inject Slisttype vecs) Slisttype ∧
jerasable M H Z (subst vecs 0 (inject Slistprodtype dZ)) Slistcoer.
Inductive jerasable_env M : type_env → coer_env → Prop :=
| JEnil : jerasable_env M 0 nil
| JEcons : ∀ H Z dH dZ dHH dZZ,
jerasable_env M H Z →
jerasable_bind M H Z dH dZ →
dHH = dH + H →
dZZ = dZ ++ dmap (lift dH 0) Z →
jerasable_env M dHH dZZ
.
Hint Unfold jerasable_bind.
Definition jterm_env M H Z G := (1 ≤ M → jerasable_env M H Z) ∧ Forall (jtype M H Z) G.
Hint Unfold jterm_env.
Lemma jterm_env_extract_jerasable_env : ∀ {M H Z G}, 1 ≤ M →
jterm_env M H Z G → jerasable_env M H Z.
Proof. intros ? ? ? ? I [H ?]; exact (H I). Qed.
Lemma lift_0 : ∀ t i, lift 0 i t = t.
Proof. induction t; intros i; simpl; [subst_lift_var|..]; f_equal; auto. Qed.
Lemma lift_fusion : ∀ t d l jl ij,
jl ≥ l → jl ≤ ij + l →
lift d jl (lift ij l t) = lift (d + ij) l t.
Proof.
induction t; intros; simpl; [|f_equal..];
try (first [reflexivity|rewrite IHt|rewrite IHt1|rewrite IHt2]; auto; omega).
subst_lift_var; f_equal; omega.
Qed.
Lemma lift_lift : ∀ t a b i ij, i ≤ ij →
lift a i (lift b ij t) = lift b (a + ij) (lift a i t).
Proof.
induction t; intros; simpl; [|f_equal..];
try (repeat rewrite plus_assoc;
first [reflexivity|rewrite IHt|rewrite IHt1|rewrite IHt2];
repeat rewrite <- plus_assoc;
f_equal; omega).
subst_lift_var; f_equal; omega.
Qed.
Lemma lift_subst1 : ∀ o vecs j t i,
lift o i (subst vecs (i + j) t) =
subst vecs (i + o + j) (lift o i t).
Proof.
induction t; intros; simpl; [|f_equal..];
try (repeat rewrite plus_assoc;
first [reflexivity|rewrite IHt|rewrite IHt1|rewrite IHt2];
repeat rewrite <- plus_assoc;
f_equal; omega).
subst_lift_var; [f_equal; omega|].
rewrite lift_fusion; [|omega..].
f_equal; [omega|].
f_equal; omega.
Qed.
Lemma lift_subst2 : ∀ off o vecs t i,
lift off (i + o) (subst vecs i t) =
subst (map (lift off o) vecs) i (lift off (i + length vecs + o) t).
Proof.
induction t; intros; simpl; [|f_equal..];
try (repeat rewrite plus_assoc;
first [reflexivity|rewrite <- IHt|rewrite <- IHt1|rewrite <- IHt2];
repeat rewrite <- plus_assoc;
f_equal; omega).
subst_lift_var; [f_equal; omega|].
replace Top with (lift off o Top) by reflexivity.
rewrite map_nth; simpl.
apply eq_sym.
apply lift_lift; omega.
Qed.
Lemma lift_subst1_0 : ∀ o vecs t j,
lift o 0 (subst vecs j t) =
subst vecs (o + j) (lift o 0 t).
Proof.
intros.
pose proof (lift_subst1 o vecs j t 0).
simpl in H; assumption.
Qed.
Lemma lift_subst2_0 : ∀ off o vecs t,
lift off o (subst vecs 0 t) =
subst (map (lift off o) vecs) 0 (lift off (length vecs + o) t).
Proof.
intros.
pose proof (lift_subst2 off o vecs t 0).
simpl in H; assumption.
Qed.
Lemma lift_subst2_0_1 : ∀ off o s t,
lift off o (subst1 s 0 t) =
subst1 (lift off o s) 0 (lift off (1 + o) t).
Proof.
intros.
pose proof (lift_subst2 off o (s :: nil) t 0).
simpl in H; assumption.
Qed.
Lemma subst_lift : ∀ t b i j h,
j ≥ i → j + length b ≤ i + h →
subst b j (lift h i t) = lift (h - length b) i t.
Proof.
induction t; intros; simpl; [|f_equal..];
try (first [reflexivity|rewrite IHt|rewrite IHt1|rewrite IHt2]; auto; omega).
subst_lift_var; f_equal; omega.
Qed.
Lemma subst_lift_0 : ∀ t b j h,
j + length b ≤ h →
subst b j (lift h 0 t) = lift (h - length b) 0 t.
Proof.
intros.
pose proof (subst_lift t b 0 j h).
simpl in H0.
rewrite H0; auto; omega.
Qed.
Lemma omega_shit_0 : ∀ a b c d, a + b - c - d - a = b - c - d.
Proof. intros; omega. Qed.
Lemma omega_shit_1 : ∀ a b c, a - b - c = a - c - b.
Proof. intros; omega. Qed.
Lemma subst_subst : ∀ t xs vecs i j,
subst xs (i + j) (subst vecs i t) =
subst (map (subst xs j) vecs) i (subst xs (i + length vecs + j) t).
Proof.
induction t; intros; simpl; [|f_equal..];
try (repeat rewrite plus_assoc;
first [reflexivity|rewrite IHt|rewrite IHt1|rewrite IHt2];
repeat rewrite <- plus_assoc;
repeat first [omega|f_equal]).
subst_lift_var.
f_equal; apply omega_shit_1.
rewrite subst_lift_0; repeat rewrite map_length; [|omega].
f_equal; [omega|].
f_equal; omega.
replace Top with (subst xs j Top) by reflexivity.
rewrite map_nth; simpl.
rewrite lift_subst1_0.
reflexivity.
replace (S (i + j)) with (1 + i + j) by reflexivity.
rewrite IHt; f_equal; f_equal; omega.
Qed.
Lemma subst_subst_0 : ∀ t xs vecs j,
subst xs j (subst vecs 0 t) =
subst (map (subst xs j) vecs) 0 (subst xs (length vecs + j) t).
Proof.
intros.
pose proof (subst_subst t xs vecs 0 j).
simpl in H; auto.
Qed.
Lemma subst_subst_0_1 : ∀ t xs s j,
subst xs j (subst1 s 0 t) =
subst1 (subst xs j s) 0 (subst xs (1 + j) t).
Proof.
intros.
pose proof (subst_subst t xs (s :: nil) 0 j).
simpl in H; auto.
Qed.
Lemma subst_app : ∀ x2s x1s t i,
subst (map (subst x2s 0) x1s ++ x2s) i t = subst x2s i (subst x1s i t).
Proof.
induction t; intros; simpl; [|f_equal..]; auto.
subst_lift_var.
f_equal; omega.
rewrite app_nth2; rewrite map_length; [|omega].
f_equal; f_equal; apply omega_shit_1.
rewrite app_nth1; repeat rewrite map_length; [|omega].
replace Top with (subst x2s 0 Top) by reflexivity.
rewrite map_nth; simpl.
rewrite lift_subst1_0.
f_equal; omega.
Qed.
Lemma subst_app_0 : ∀ x2s x1s t,
subst (map (subst x2s 0) x1s ++ x2s) 0 t = subst x2s 0 (subst x1s 0 t).
Proof. intros; pose proof (subst_app x2s x1s t 0); auto. Qed.
Ltac dmap_tac t :=
intros Z; induction Z as [|[? ?] Z]; intros; simpl; f_equal; auto;
simpl; f_equal; apply t; omega.
Lemma dmap_lift_0 : ∀ Z i, dmap (lift 0 i) Z = Z.
Proof. dmap_tac lift_0. Qed.
Lemma dmap_lift_fusion : ∀ Z d l jl ij,
jl ≥ l → jl ≤ ij + l → dmap (lift d jl) (dmap (lift ij l) Z) = dmap (lift (d + ij) l) Z.
Proof. dmap_tac lift_fusion. Qed.
Lemma dmap_lift_plus : ∀ d1 d2 Z i,
dmap (lift (d1 + d2) i) Z = dmap (lift d1 i) (dmap (lift d2 i) Z).
Proof. intros; rewrite dmap_lift_fusion; auto; omega. Qed.
Lemma dmap_lift_lift : ∀ Z a b i ij, i ≤ ij →
dmap (lift a i) (dmap (lift b ij) Z) = dmap (lift b (a + ij)) (dmap (lift a i) Z).
Proof. dmap_tac lift_lift. Qed.
Lemma dmap_lift_subst1 : ∀ Z o vecs j,
dmap (lift o 0) (dmap (subst vecs j) Z) =
dmap (subst vecs (o + j)) (dmap (lift o 0) Z).
Proof. dmap_tac lift_subst1_0. Qed.
Lemma dmap_lift_subst2 : ∀ Z off o vecs,
dmap (lift off o) (dmap (subst vecs 0) Z) =
dmap (subst (map (lift off o) vecs) 0) (dmap (lift off (length vecs + o)) Z).
Proof. dmap_tac lift_subst2_0. Qed.
Lemma dmap_subst_lift : ∀ t b j h,
j + length b ≤ h →
dmap (subst b j) (dmap (lift h 0) t) = dmap (lift (h - length b) 0) t.
Proof. dmap_tac subst_lift_0. Qed.
Lemma dmap_app : ∀ f Z1 Z2, dmap f Z1 ++ dmap f Z2 = dmap f (Z1 ++ Z2).
Proof. intros; unfold dmap; rewrite map_app; auto. Qed.
Definition etraverse f := fix g i e :=
match e with
| Stype ⇒ Stype
| Sprod e1 e2 ⇒ Sprod (g i e1) (g i e2)
| Slist e ⇒ Slist (g i e)
| Scoer Y0 Y1 dH dZ ⇒ Scoer (dmap (f i) Y0) (dmap (f i) Y1) dH (dmap (f (dH + i)) dZ)
end.
Definition elift d i := etraverse (lift d) i.
Definition esubst vecs i := etraverse (subst vecs) i.
Fixpoint slift e d i :=
match e return sort_type e → sort_type e with
| Stype ⇒ lift d i
| Sprod e1 e2 ⇒ fun x ⇒
match x with
| (x1, x2) ⇒ (slift e1 d i x1, slift e2 d i x2)
end
| Slist e ⇒ fix f xs :=
match xs with
| nil ⇒ nil
| cons x xs ⇒ cons (slift e d i x) (f xs)
end
| Scoer Y0 Y1 dH dZ ⇒ fun x ⇒
match x with
| (t, s) ⇒ (lift d (dH + i) t, lift d i s)
end
end.
Lemma extract_lift : ∀ d e x t i, extract e t x → extract e (lift d i t) (slift e d i x).
Proof.
induction e; [|induction x..]; intros; destruct_extract; simpl in *; auto using extract.
apply Econs; auto.
apply IHx; auto.
Qed.
Lemma lift_inject : ∀ d e i x,
lift d i (inject e x) = inject e (slift e d i x).
Proof. induction e; [|induction x..]; intros; simpl; f_equal; auto. Qed.
Fixpoint ssubst e vecs i :=
match e return sort_type e → sort_type e with
| Stype ⇒ subst vecs i
| Sprod e1 e2 ⇒ fun x ⇒
match x with
| (x1, x2) ⇒ (ssubst e1 vecs i x1, ssubst e2 vecs i x2)
end
| Slist e ⇒ fix f xs :=
match xs with
| nil ⇒ nil
| cons x xs ⇒ cons (ssubst e vecs i x) (f xs)
end
| Scoer Y0 Y1 dH dZ ⇒ fun x ⇒
match x with
| (t, s) ⇒ (subst vecs (dH + i) t, subst vecs i s)
end
end.
Lemma extract_subst : ∀ vecs e x t i, extract e t x →
extract e (subst vecs i t) (ssubst e vecs i x).
Proof.
induction e; [|induction x..]; intros; destruct_extract; simpl in *; auto using extract.
apply Econs; auto.
apply IHx; auto.
Qed.
Lemma subst_inject : ∀ xs e i x,
subst xs i (inject e x) = inject e (ssubst e xs i x).
Proof. induction e; [|induction x..]; intros; simpl; f_equal; auto. Qed.
Ltac dmap_lift_lift_tac :=
match goal with
| |- context[dmap (lift ?a (?b + ?c)) (dmap (lift ?b 0) ?Z)] ⇒
rewrite <- (dmap_lift_lift Z b a 0 c); [|omega]
| |- context[dmap (lift ?a ?b) (dmap (lift ?b 0) ?Z)] ⇒
rewrite (dmap_lift_fusion Z a 0 b b); [|omega..]
end.
Ltac S_plus_1 :=
match goal with
| |- context[S ?x] ⇒ is_var x; replace (S x) with (1 + x) by reflexivity
end.
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.
Ltac tryomega := subst; repeat first
[ assumption
| reflexivity
| omega
| unfold dmap; rewrite map_length
| rewrite <- dmap_app
| rewrite <- app_assoc
| repeat S_plus_1; rewrite dmap_lift_plus
| rewrite dmap_lift_0
| dmap_lift_lift_tac
| rewrite dmap_lift_subst1 ].
Lemma jwf_lift : ∀ wf off t a,
jwf a t wf →
∀ o,
jwf a (lift off (a + S o) t) wf.
Proof.
induction 1; simpl; intros; [subst_lift_var|..]; eauto using jwf.
apply WFFor with (lift off (d + a + o) s12s).
unfold shift; rewrite lift_lift; [|omega].
f_equal; auto; omega.
rewrite plus_assoc; eauto.
apply WFMu.
apply IHjwf1; tryomega.
apply IHjwf2; tryomega.
apply WFwf with (lift off (a + o) s).
unfold shift; rewrite lift_lift; [|omega].
f_equal; auto; omega.
Qed.
Lemma jwf_lift_0 : ∀ wf o off t,
jwf 0 t wf →
jwf 0 (lift off (S o) t) wf.
Proof.
intros wf o off t H0.
pose proof (jwf_lift wf off t 0 H0 o).
simpl in H; auto.
Qed.
Lemma jwf_subst : ∀ wf xs t a,
jwf a t wf →
∀ o,
jwf a (subst xs (a + S o) t) wf.
Proof.
induction 1; simpl; intros; [subst_lift_var|..]; eauto using jwf.
apply WFFor with (subst xs (d + a + o) s12s).
unfold shift; rewrite lift_subst1.
f_equal; auto; omega.
rewrite plus_assoc; eauto.
apply WFMu.
apply IHjwf1; tryomega.
apply IHjwf2; tryomega.
apply WFwf with (subst xs (a + o) s).
unfold shift; rewrite lift_subst1.
f_equal; auto; omega.
Qed.
Lemma jwf_subst_0 : ∀ wf i xs t,
jwf 0 t wf →
jwf 0 (subst xs (S i) t) wf.
Proof.
intros wf i xs t H.
pose proof (jwf_subst wf xs t 0 H).
simpl in H0; auto.
Qed.
Lemma jerasable_weak_coer : ∀ M H iHH iZZ dZ Z t e,
jerasable M iHH iZZ t e →
∀ iH iZ idZ,
iHH = iH + H →
iZZ = iZ ++ dmap (lift iH 0) Z →
idZ = iZ ++ dmap (lift iH 0) (dZ ++ Z) →
jerasable M iHH idZ t e.
Proof.
induction 1; simpl; intros; eauto using jerasable.
apply JTFor with dZ0 wits vecs; auto.
apply IHjerasable1 with (dH + iH) (dmap (lift dH 0) iZ); tryomega.
apply IHjerasable2 with (dH + iH) (dZ0 ++ dmap (lift dH 0) iZ); tryomega.
apply IHjerasable3 with iH iZ; tryomega.
apply IHjerasable4 with iH iZ; tryomega.
apply JTMu; auto.
apply IHjerasable with (1 + iH) (dmap (lift 1 0) iZ); tryomega.
apply JCTrans with t2; auto.
apply IHjerasable1 with (dH2 + iH) (dZ2 ++ dmap (lift dH2 0) iZ); tryomega.
apply IHjerasable2 with iH iZ; tryomega.
apply JCArr; try intro m; auto.
apply (H2 m) with (dH + iH) (dZ0 ++ dmap (lift dH 0) iZ); clear m; tryomega.
apply (H4 m) with (dH + iH) (dZ0 ++ dmap (lift dH 0) iZ); clear m; tryomega.
apply IHjerasable1 with iH iZ; tryomega.
apply IHjerasable2 with (dH + iH) (dZ0 ++ dmap (lift dH 0) iZ); tryomega.
apply IHjerasable3 with iH iZ; tryomega.
apply JCProd; try intro m; auto.
apply (H2 m) with (dH + iH) (dZ0 ++ dmap (lift dH 0) iZ); clear m; tryomega.
apply (H4 m) with (dH + iH) (dZ0 ++ dmap (lift dH 0) iZ); clear m; tryomega.
apply IHjerasable1 with iH iZ; tryomega.
apply IHjerasable2 with iH iZ; tryomega.
destruct (le_gt_dec (length Y0 + length iZ) c).
apply JCVar with (length dZ + c).
intros m; apply (H2 m) with iH iZ; clear m; tryomega.
intros m; apply (H4 m) with iH iZ; clear m; tryomega.
subst; rewrite <- dmap_app.
rewrite app_nth2 in × by omega.
rewrite app_nth2 in × by omega.
assert (length (dmap (lift iH 0) dZ) = length dZ) by tryomega.
rewrite app_nth2 by omega.
rewrite <- H5.
f_equal.
unfold dmap; rewrite map_length.
apply omega_shit_0.
apply JCVar with c.
intros m; apply (H2 m) with iH iZ; clear m; tryomega.
intros m; apply (H4 m) with iH iZ; clear m; tryomega.
subst.
rewrite app_assoc.
rewrite app_assoc in H5.
rewrite app_nth1; [|rewrite app_length; omega].
rewrite app_nth1 in H5; [assumption|rewrite app_length; omega].
apply JCGen with wits vecs; auto.
intros m. apply (H2 m) with iH iZ; clear m; tryomega.
apply IHjerasable1 with (dH + iH) (dmap (lift dH 0) iZ); tryomega.
apply IHjerasable2 with iH iZ; tryomega.
apply IHjerasable3 with iH iZ; tryomega.
Qed.
Lemma jerasable_weak_coer_0 : ∀ {M H dZ Z t e},
jerasable M H Z t e →
jerasable M H (dZ ++ Z) t e.
Proof. intros; apply jerasable_weak_coer with H Z dZ Z 0 nil; tryomega. Qed.
Definition Incf f Y Z :=
∀ c, nth c Y (Top, Top) = nth (f c) Z (Top, Top).
Hint Unfold Incf.
Lemma Incf_lift : ∀ f H Y Z,
Incf f Y Z → Incf f (dmap (lift H 0) Y) (dmap (lift H 0) Z).
Proof.
intros; intros c; pose proof (H0 c); unfold dmap.
replace (Top, Top) with (pmap (lift H 0) (Top, Top)) by reflexivity.
repeat rewrite map_nth.
rewrite H1; reflexivity.
Qed.
Lemma Incf_app : ∀ {f0 f1 Y0 Z0 Y1 Z1},
Incf f0 Y0 Z0 → Incf f1 Y1 Z1 → ∃ f, Incf f (Y0 ++ Y1) (Z0 ++ Z1).
Proof.
intros.
∃ (fun c ⇒ match le_gt_dec (length Y0) c with
| left _ ⇒ f1 (c - length Y0) + length Z0
| right _ ⇒
match le_gt_dec (length Z0) (f0 c) with
| left _ ⇒ f0 c + length Z1
| right _ ⇒ f0 c
end
end).
intros c.
destruct (le_gt_dec (length Y0) c).
repeat (rewrite app_nth2; [|omega]).
pose proof (H0 (c - length Y0)); rewrite H1.
f_equal; omega.
rewrite app_nth1; [|omega].
pose proof (H c); rewrite H1.
destruct (le_gt_dec (length Z0) (f0 c)).
rewrite app_nth2; [|omega].
repeat (rewrite nth_overflow; [|omega]).
reflexivity.
rewrite app_nth1; [|omega].
reflexivity.
Qed.
Lemma Incf_refl : ∀ Z, Incf (fun c ⇒ c) Z Z.
Proof. intros Z c; auto. Qed.
Lemma jcoer_weak_coerY : ∀ M H dH dZ Y0 Y1 Z t,
jerasable M H Z t (Scoer Y0 Y1 dH dZ) →
∀ f0 f1 Y0' Y1',
Incf f0 Y0 Y0' → Incf f1 Y1 Y1' →
jerasable M H Z t (Scoer Y0' Y1' dH dZ).
Proof.
intros M H dH dZ Y0 Y1 Z t HZt.
remember (Scoer Y0 Y1 dH dZ) as e.
generalize Y0 Y1 dH dZ Heqe; clear Y0 Y1 dH dZ Heqe;
induction HZt; intros ? ? ? ? Heqe; inversion Heqe; subst;
simpl; intros; eauto using jerasable.
apply JCTrans with t2; auto.
apply IHHZt1 with (dmap (lift dH2 0) Y2) (dmap (lift dH2 0) Y3) f0 f1; tryomega;
apply Incf_lift; auto.
apply IHHZt2 with Y2 Y3 f0 f1; tryomega.
destruct (Incf_app H5 H4) as [f ?].
pose proof (Incf_refl nil).
apply JCArr; auto.
apply IHHZt2 with (dmap (lift dH0 0) (Y3 ++ Y2)) nil f (fun c ⇒ c); tryomega.
repeat (rewrite dmap_app); apply Incf_lift; auto.
apply IHHZt3 with (Y3 ++ Y2) nil f (fun c ⇒ c); tryomega.
destruct (Incf_app H5 H4) as [f ?].
pose proof (Incf_refl nil).
apply JCProd; auto.
apply IHHZt1 with (Y3 ++ Y2) nil f (fun c ⇒ c); tryomega.
apply IHHZt2 with (Y3 ++ Y2) nil f (fun c ⇒ c); tryomega.
pose proof (Incf_refl Z).
destruct (Incf_app H5 H7) as [f ?].
apply JCVar with (f c); auto.
rewrite H8 in H4; auto.
apply JCGen with wits vecs; subst; auto.
apply JCFix.
intros m; apply (H0 m).
pose proof (Incf_refl ((t, s) :: nil)).
destruct (Incf_app H4 H3) as [f ?].
apply IHHZt with Y2 ((t, s) :: Y3) f0 f; tryomega.
Qed.
Lemma Incf_nil : ∀ Z, ∃ f, Incf f nil Z.
Proof.
intros.
∃ (fun c ⇒ length Z).
intros c.
repeat (rewrite nth_overflow; [|simpl; omega]).
reflexivity.
Qed.
Lemma jcoer_weak_coerY_0 : ∀ M H Z Y0 Y1 dH dZ t,
jerasable M H Z t (Scoer nil nil dH dZ) →
jerasable M H Z t (Scoer Y0 Y1 dH dZ).
Proof.
intros M H Z Y0 Y1 dH dZ t HZt.
destruct (Incf_nil Y0) as [f0 ?].
destruct (Incf_nil Y1) as [f1 ?].
pose proof (jcoer_weak_coerY M H dH dZ nil nil Z t HZt f0 f1 Y0 Y1); auto.
Qed.
Lemma jerasable_lift : ∀ M off iZZ iHH H Z t e,
jerasable M iHH iZZ t e →
∀ iH iZ ioH ioZ,
iHH = iH + H →
iZZ = iZ ++ dmap (lift iH 0) Z →
ioH = iH + off + H →
ioZ = dmap (lift off iH) iZZ →
jerasable M ioH ioZ (lift off iH t) (elift off iH e).
Proof.
induction 1; simpl; intros; eauto using jerasable.
apply JTFor with (dmap (lift off (dH + iH)) dZ)
(lift off iH wits) (map (lift off iH) vecs); tryomega;
try (apply extract_lift; auto).
apply IHjerasable1 with (dmap (lift (length vecs) 0) iZ); tryomega.
apply IHjerasable2 with (dZ ++ dmap (lift (length vecs) 0) iZ); tryomega.
apply IHjerasable3 with iZ; tryomega.
rewrite <- lift_subst2_0.
apply IHjerasable4 with iZ; tryomega.
apply JTMu.
subst; apply jwf_lift_0; assumption.
apply IHjerasable with (dmap (lift 1 0) iZ); tryomega.
rewrite <- dmap_app; rewrite <- plus_assoc; rewrite <- dmap_lift_lift; [|omega].
apply JCTrans with (lift off (dH2 + iH) t2).
rewrite (dmap_lift_lift Y0); [|omega].
rewrite (dmap_lift_lift Y1); [|omega].
apply IHjerasable1 with (dZ2 ++ dmap (lift dH2 0) iZ); tryomega.
apply IHjerasable2 with iZ; tryomega.
apply JCWeak with dH (dmap (lift off (dH + iH)) dZ).
intros m; apply (H2 m) with iZ; tryomega.
simpl in IHjerasable; rewrite lift_lift; [|omega].
apply IHjerasable with iZ; tryomega.
apply JCArr.
intros M2M; apply (H2 M2M) with (dZ ++ dmap (lift dH 0) iZ); tryomega.
intros M2M; apply (H4 M2M) with (dZ ++ dmap (lift dH 0) iZ); tryomega.
apply IHjerasable1 with iZ; tryomega.
simpl in IHjerasable2; trysimpl.
rewrite lift_lift; [|omega].
rewrite (dmap_lift_lift Y0); [|omega].
rewrite (dmap_lift_lift Y1); [|omega].
rewrite dmap_app.
apply IHjerasable2 with (dZ ++ dmap (lift dH 0) iZ); tryomega.
rewrite dmap_app.
apply IHjerasable3 with iZ; tryomega.
apply JCProd.
intros M2M; apply (H2 M2M) with (dZ ++ dmap (lift dH 0) iZ); tryomega.
intros M2M; apply (H4 M2M) with (dZ ++ dmap (lift dH 0) iZ); tryomega.
rewrite dmap_app; apply IHjerasable1 with iZ; tryomega.
rewrite dmap_app; apply IHjerasable2 with iZ; tryomega.
apply JCVar with c.
intros M1M; apply (H2 M1M) with iZ; tryomega.
intros M1M; apply (H4 M1M) with iZ; tryomega.
subst; rewrite dmap_app; unfold dmap in ×.
replace (Top, Top) with (pmap (lift off iH) (Top, Top)) by reflexivity.
rewrite map_nth.
rewrite H5; reflexivity.
apply JCGen with (lift off iH wits) (map (lift off iH) vecs); tryomega;
try (apply extract_lift; auto).
intros M1M; apply (H2 M1M) with iZ; tryomega.
apply IHjerasable1 with (dmap (lift (length vecs) 0) iZ); tryomega.
apply IHjerasable2 with iZ; tryomega.
rewrite <- lift_subst2_0.
apply IHjerasable3 with iZ; tryomega.
rewrite lift_subst2_0. subst dH.
apply JCInst with (lift off iH insts); try (apply extract_lift; auto); tryomega.
intros M1M; apply (H2 M1M) with iZ; tryomega.
apply IHjerasable1 with iZ; tryomega.
rewrite <- lift_subst2_0.
apply IHjerasable2 with iZ; tryomega.
unfold subst1 in *; rewrite lift_subst2_0.
apply JCUnfold.
intros M1M; apply (H2 M1M) with iZ; tryomega.
intros m; subst; apply jwf_lift_0; auto.
unfold subst1 in *; rewrite lift_subst2_0; simpl.
apply JCFold with (t := lift off (S iH) t).
apply IHjerasable with iZ; tryomega.
apply JCFix.
intros m; apply (H2 m) with iZ; tryomega.
apply IHjerasable with iZ; tryomega.
Qed.
Lemma jerasable_lift_0 : ∀ {M dH H Z t} e,
jerasable M H Z t e →
∀ ee, ee = elift dH 0 e →
jerasable M (dH + H) (dmap (lift dH 0) Z) (lift dH 0 t) ee.
Proof.
intros; subst.
apply jerasable_lift with Z H H Z nil; tryomega.
Qed.
Lemma jerasable_nth : ∀ M H Z e xs a,
a < length xs →
jerasable M H Z (inject Slisttype xs) (Slist e) →
jerasable M H Z (nth a xs Top) e.
Proof.
induction xs; intros; [inversion H0|].
destruct a0; simpl in *; inversion H1; auto.
apply IHxs; auto; omega.
Qed.
Lemma jerasable_nth_subst : ∀ M H Z xs dZ c t s,
jerasable M H Z (subst xs 0 (inject Slistprodtype dZ)) Slistcoer →
c < length dZ →
nth c dZ (Top, Top) = (t, s) →
jerasable M H Z (subst xs 0 (Spair 0 t s)) (Scoer nil nil 0 nil).
Proof.
induction dZ; intros; [inversion H1|].
destruct a as [t0 s0].
destruct c; inversion H2; subst; [inversion H0; auto|].
simpl in H1.
apply IHdZ with c; auto.
inversion H0; auto.
omega.
Qed.
Lemma jerasable_subst : ∀ M H Z xs dH dZ t e idH idZ,
dH = length xs →
jerasable M H Z (inject Slisttype xs) Slisttype →
jerasable M H Z (subst xs 0 (inject Slistprodtype dZ)) Slistcoer →
jerasable M idH idZ t e →
∀ iH iZ iHH iZZ,
idH = iH + dH + H →
idZ = iZ ++ dmap (lift iH 0) dZ ++ dmap (lift (iH + dH) 0) Z →
iHH = iH + H →
iZZ = dmap (subst xs iH) iZ ++ dmap (lift iH 0) Z →
jerasable M iHH iZZ (subst xs iH t) (esubst xs iH e).
Proof.
induction 4; simpl; intros; eauto using jerasable.
subst_lift_var; try apply JTVar; subst.
apply jerasable_weak_coer_0.
apply jerasable_lift_0 with Stype; auto.
apply jerasable_nth; auto; omega.
apply JTFor with (dZ := dmap (subst xs (dH0 + iH)) dZ0)
(wits := subst xs iH wits)
(vecs := map (subst xs iH) vecs); tryomega;
try (apply extract_subst; auto).
apply IHjerasable1 with (dmap (lift (length vecs) 0) iZ); tryomega.
apply IHjerasable2 with (dZ0 ++ dmap (lift (length vecs) 0) iZ); tryomega.
apply IHjerasable3 with iZ; tryomega.
rewrite <- subst_subst_0.
apply IHjerasable4 with iZ; tryomega.
apply JTMu.
subst; apply jwf_subst_0; assumption.
apply IHjerasable with (dmap (lift 1 0) iZ); tryomega.
rewrite <- dmap_app; rewrite <- plus_assoc; rewrite <- dmap_lift_subst1.
apply JCTrans with (subst xs (dH2 + iH) t2).
rewrite (dmap_lift_subst1 Y0).
rewrite (dmap_lift_subst1 Y1).
apply IHjerasable1 with (dZ2 ++ dmap (lift dH2 0) iZ); tryomega.
apply IHjerasable2 with iZ; tryomega.
apply JCWeak with dH0 (dmap (subst xs (dH0 + iH)) dZ0).
intros M1M; apply (H5 M1M) with iZ; tryomega.
simpl in IHjerasable; rewrite lift_subst1_0.
apply IHjerasable with iZ; tryomega.
apply JCArr.
intros M2M; apply (H5 M2M) with (dZ0 ++ dmap (lift dH0 0) iZ); tryomega.
intros M2M; apply (H7 M2M) with (dZ0 ++ dmap (lift dH0 0) iZ); tryomega.
apply IHjerasable1 with iZ; tryomega.
simpl in IHjerasable2; trysimpl.
rewrite lift_subst1_0.
rewrite (dmap_lift_subst1 Y0).
rewrite (dmap_lift_subst1 Y1).
rewrite dmap_app.
apply IHjerasable2 with (dZ0 ++ dmap (lift dH0 0) iZ); tryomega.
rewrite dmap_app.
apply IHjerasable3 with iZ; tryomega.
apply JCProd.
intros M2M; apply (H5 M2M) with (dZ0 ++ dmap (lift dH0 0) iZ); tryomega.
intros M2M; apply (H7 M2M) with (dZ0 ++ dmap (lift dH0 0) iZ); tryomega.
rewrite dmap_app; apply IHjerasable1 with iZ; tryomega.
rewrite dmap_app; apply IHjerasable2 with iZ; tryomega.
destruct (le_gt_dec (length (Y0 ++ iZ)) c);
[destruct (le_gt_dec (length (Y0 ++ iZ) + length dZ) c)|].
apply JCVar with (c - length dZ).
intros M1M; apply (H5 M1M) with iZ; tryomega.
intros M1M; apply (H7 M1M) with iZ; tryomega.
subst; rewrite app_assoc; rewrite dmap_app; unfold dmap in ×.
rewrite app_nth2; [|rewrite map_length; omega].
rewrite app_assoc in H8;
rewrite app_nth2 in H8; [|repeat rewrite map_length; omega].
rewrite app_nth2 in H8; [|repeat rewrite map_length; omega].
repeat rewrite map_length in ×.
replace (Top, Top) with (pmap (lift iH 0) (Top, Top)) by reflexivity.
rewrite map_nth.
replace (Top, Top) with (pmap (lift (iH + length xs) 0) (Top, Top)) in H8 by reflexivity.
rewrite map_nth in H8.
fold (pmap (subst xs iH) (t, s)).
rewrite <- H8.
rewrite omega_shit_1.
destruct (nth (c - length (Y0 ++ iZ) - length dZ)).
simpl.
repeat rewrite subst_lift; try omega.
replace (iH + length xs - length xs) with iH by omega.
reflexivity.
replace (Spair 0 (subst xs iH t) (subst xs iH s)) with (subst xs iH (Spair 0 t s)) by reflexivity.
clear H4 H5 H6 H7; subst.
rewrite app_assoc in H8; rewrite app_nth2 in H8; try omega.
unfold dmap in H8.
rewrite app_nth1 in H8; try (repeat rewrite map_length; omega).
replace (Top, Top) with (pmap (lift iH 0) (Top, Top)) in H8 by reflexivity.
rewrite map_nth in H8.
apply jerasable_weak_coer_0.
remember (nth (c - length (Y0 ++ iZ)) dZ (Top, Top)) as ts0.
destruct ts0 as [t0 s0].
simpl in H8; inversion H8; clear H8; subst.
replace (Spair 0 (lift iH 0 t0) (lift iH 0 s0)) with (lift iH 0 (Spair 0 t0 s0)) by reflexivity.
replace (subst xs iH (lift iH 0 (Spair 0 t0 s0))) with (lift iH 0 (subst xs 0 (Spair 0 t0 s0)))
by (rewrite lift_subst1_0; f_equal; omega).
apply jcoer_weak_coerY_0.
apply jerasable_lift_0 with (Scoer nil nil 0 nil); auto.
apply jerasable_nth_subst with dZ (c - length (Y0 ++ iZ)); auto.
omega.
apply JCVar with c.
intros M1M; apply (H5 M1M) with iZ; tryomega.
intros M1M; apply (H7 M1M) with iZ; tryomega.
clear H1 H2 H4 H5 H6 H7.
subst; rewrite app_assoc; rewrite dmap_app; unfold dmap in ×.
rewrite app_nth1; [|rewrite map_length; omega].
rewrite app_assoc in H8; rewrite app_nth1 in H8; [|repeat rewrite map_length; omega].
replace (Top, Top) with (pmap (subst xs iH) (Top, Top)) by reflexivity.
rewrite map_nth.
rewrite H8.
reflexivity.
apply JCGen with (subst xs iH wits) (map (subst xs iH) vecs); tryomega;
try (apply extract_subst; auto).
intros M1M; apply (H5 M1M) with iZ; tryomega.
apply IHjerasable1 with (dmap (lift (length vecs) 0) iZ); tryomega.
apply IHjerasable2 with iZ; tryomega.
rewrite <- subst_subst_0.
apply IHjerasable3 with iZ; tryomega.
rewrite subst_subst_0. subst dH0.
apply JCInst with (subst xs iH insts); try (apply extract_subst; auto); tryomega.
intros M1M; apply (H5 M1M) with iZ; tryomega.
apply IHjerasable1 with iZ; tryomega.
rewrite <- subst_subst_0.
apply IHjerasable2 with iZ; tryomega.
unfold subst1 in *; rewrite subst_subst_0.
apply JCUnfold.
intros M1M; apply (H5 M1M) with iZ; tryomega.
intros m; subst; apply jwf_subst_0; auto.
unfold subst1 in *; rewrite subst_subst_0.
apply JCFold with (t := subst xs (S iH) t).
apply IHjerasable with iZ; tryomega.
apply JCFix; auto.
intros m; apply (H5 m) with iZ; tryomega.
apply IHjerasable with iZ; tryomega.
Qed.
Lemma jerasable_subst_0 : ∀ {M H Z xs t} dH dZ e,
jerasable M (dH + H) (dZ ++ dmap (lift dH 0) Z) t e →
dH = length xs →
jerasable M H Z (inject Slisttype xs) Slisttype →
jerasable M H Z (subst xs 0 (inject Slistprodtype dZ)) Slistcoer →
∀ ee, ee = esubst xs 0 e →
jerasable M H Z (subst xs 0 t) ee.
Proof.
intros; subst ee.
apply jerasable_subst with H Z dH dZ (dH + H) (dZ ++ dmap (lift dH 0) Z) nil; tryomega.
Qed.
Lemma jcoer_extract_jerasable_env : ∀ M H Z Y0 Y1 dH dZ t s,
jerasable M H Z (Spair dH t s) (Scoer Y0 Y1 dH dZ) →
jerasable_env M H Z →
jerasable_env M (dH + H) (dZ ++ dmap (lift dH 0) Z).
Proof.
intros M H Z Y0 Y1 dH dZ t s jH.
remember (Spair dH t s) as ts.
remember (Scoer Y0 Y1 dH dZ) as e.
generalize t s Y0 Y1 dH dZ Heqts Heqe; clear t s Y0 Y1 dH dZ Heqts Heqe.
induction jH; intros; first [discriminate Heqts|discriminate Heqe|idtac];
inversion Heqts; inversion Heqe; clear Heqts Heqe; subst; trysimpl; eauto.
rewrite <- plus_assoc.
rewrite <- app_assoc.
rewrite dmap_app.
apply IHjH1 with t t2 (dmap (lift dH2 0) Y2) (dmap (lift dH2 0) Y3); tryomega.
apply IHjH2 with t2 s Y2 Y3; tryomega.
apply JEcons with H Z dH0 dZ0; tryomega.
∃ vecs; repeat split; auto.
rewrite <- (inject_extract H2); auto.
rewrite <- (inject_extract H3); auto.
rewrite <- (inject_extract H2); auto.
Qed.
Lemma jcoer_extract_right_type : ∀ {M H Z Y0 Y1 dH dZ t s}, 1 ≤ M →
jerasable M H Z (Spair dH t s) (Scoer Y0 Y1 dH dZ) →
jerasable M H Z s Stype.
Proof.
intros M H Z Y0 Y1 dH dZ t s M1M jH.
remember (Spair dH t s) as ts.
remember (Scoer Y0 Y1 dH dZ) as e.
generalize t s Y0 Y1 dH dZ Heqts Heqe; clear t s Y0 Y1 dH dZ Heqts Heqe.
induction jH; intros; first [discriminate Heqts|discriminate Heqe|idtac];
inversion Heqts; inversion Heqe; clear Heqts Heqe; subst;
repeat (trysimpl; match goal with
| H1 : 1 ≤ M → _ |- _ ⇒ pose proof (H1 M1M); clear H1
| _ : length ?vecs = ?dH |- _ ⇒ subst dH
| H : extract _ ?t ?x |- context[inject _ ?x]
⇒ rewrite <- (inject_extract H)
| |- jerasable _ _ _ (Arr _ _) _ ⇒ apply JTArr
| |- jerasable _ _ _ (Prod _ _) _ ⇒ apply JTProd
| H1 : jerasable _ _ _ (For _ _ _) _ |- _ ⇒ inversion H1; clear H1; subst
| _ : extract _ ?wits ?vecs
, _ : extract _ ?t12s ?dZ
|- jerasable _ _ _ (For (length ?vecs) ?t12s _) _ ⇒ apply JTFor with dZ wits vecs
| |- jerasable _ _ _ Top _ ⇒ apply JTTop
| H : jerasable _ (length ?vecs + _) (?dZ ++ _) ?t Stype
|- jerasable _ _ _ (subst ?vecs 0 ?t) Stype
⇒ apply jerasable_subst_0 with (length vecs) dZ Stype
end; auto); trysimpl; eauto.
inversion H1; subst.
apply jerasable_subst_0 with 1 nil Stype; simpl in *; eauto using jerasable.
Qed.
Lemma jcoer_extract_left_type : ∀ {M H Z Y0 Y1 dH dZ t s}, 1 ≤ M →
jerasable M H Z (Spair dH t s) (Scoer Y0 Y1 dH dZ) →
jerasable M (dH + H) (dZ ++ dmap (lift dH 0) Z) t Stype.
Proof.
intros M H Z Y0 Y1 dH dZ t s M1M jH.
remember (Spair dH t s) as ts.
remember (Scoer Y0 Y1 dH dZ) as e.
generalize t s Y0 Y1 dH dZ Heqts Heqe; clear t s Y0 Y1 dH dZ Heqts Heqe.
induction jH; intros; first [discriminate Heqts|discriminate Heqe|idtac];
inversion Heqts; inversion Heqe; clear Heqts Heqe; subst;
repeat (trysimpl; match goal with
| H1 : 2 ≤ M → _ |- _ ⇒ clear H1
| H1 : 1 ≤ M → _ |- _ ⇒ pose proof (H1 M1M); clear H1
| Hx : ∀ t0 s0 Y2 Y3 dH0 dZ0,
Spair ?dH ?t ?s = Spair dH0 t0 s0 →
Scoer ?Y0 ?Y1 ?dH ?dZ = Scoer Y2 Y3 dH0 dZ0 →
_ |- _ ⇒ pose proof (Hx t s Y0 Y1 dH dZ eq_refl eq_refl); clear Hx
| |- jerasable _ _ _ (Arr _ _) _ ⇒ apply JTArr
| |- jerasable _ _ _ (Prod _ _) _ ⇒ apply JTProd
| |- jerasable _ _ _ Bot _ ⇒ apply JTBot
| H1 : jerasable _ _ _ (For _ _ _) _ |- _ ⇒ inversion H1; clear H1; subst
| H1 : jerasable _ ?H ?Z (Spair _ _ ?t) (Scoer _ _ _ _)
|- jerasable _ ?H ?Z ?t Stype
⇒ apply (jcoer_extract_right_type M1M H1)
| H1 : extract _ ?t ?x , H2 : extract _ ?t ?y |- _
⇒ rewrite (extract_eq H1 H2); clear H1
end; auto); trysimpl; eauto.
inversion jH; subst.
apply jerasable_subst_0 with 1 nil Stype; simpl in *; eauto using jerasable.
Qed.