Lemma stuck_not_closed s :
stuck s -> closedL s -> False.
Proof.
induction 1;inversion 1;eauto;omega.
Qed.
Lemma closed_cases s :
closedL s -> exactlyOneHolds [reducible (≻L) s;abstraction s].
Proof.
intros ?. specialize stuck_not_closed with (s:=s). specialize L_trichotomy with (s:=s). cbn. tauto.
Qed.
stuck s -> closedL s -> False.
Proof.
induction 1;inversion 1;eauto;omega.
Qed.
Lemma closed_cases s :
closedL s -> exactlyOneHolds [reducible (≻L) s;abstraction s].
Proof.
intros ?. specialize stuck_not_closed with (s:=s). specialize L_trichotomy with (s:=s). cbn. tauto.
Qed.
Inductive star X (R:X->X->Prop) : X -> X -> Prop :=
| starR x : star R x x
| starC x y z : R x y -> star R y z -> star R x z.
Lemma counterexample_closed_needed:
let s := (lam (lam 1)) (lam 1) (lam 0)in
star (≻L) s (lam (lam 0)) /\
star (≻C) ([γ s retT/[]],[]) ([],[varT 1 retT / []]).
Proof.
split.
-repeat (eapply starC;[now eauto|cbn]). apply starR.
-cbn. repeat (eapply starC;[do 2 econstructor;now constructor|cbn]). apply starR.
Qed.
Lemma boundL_mono k k' s : k <= k' -> s <L k -> s <L k'.
Proof.
intros HMk. induction 1 in HMk,k'|-*; econstructor; eauto.
- omega.
- eapply IHboundL. omega.
Qed.
Lemma boundL_subst s t k : s <L S k -> t <L k -> subst s k t <L k.
Proof.
revert k t; induction s; intros k t cls_s cls_t; simpl; inv cls_s; eauto 6 using boundL_mono.
decide (n = k); eauto. econstructor. omega.
Qed.
Lemma subst_boundL_inv s k u : s <L k -> subst s k u = s.
Proof with eauto.
intros H; revert u; induction H; intros u; simpl.
- decide (n = k)... omega.
- rewrite IHboundL1, IHboundL2...
- f_equal...
Qed.
Lemma closed_subst s k u : closedL s -> subst s k u = s.
Proof.
intros H. eapply subst_boundL_inv. eapply boundL_mono. 2:eassumption. omega.
Qed.
Lemma closed_stepL s t : s ≻L t -> closedL s -> closedL t.
Proof.
unfold closedL;induction 1; intros cls_s; inv cls_s; eauto using boundL.
inv H1. eauto using boundL_subst.
Qed.
Section heap_decomp.
Variable codeImpl:code.
Variable heapImpl:heap PA.
Variable C: Code.
Notation "(≫C_ H )" := (representsClos C H) (at level 0, format "'(≫C_' H ')'").
Notation "g ≫C_ H e" := (representsClos C H g e) (at level 70,H at level 0, format "g '≫C_' H e").
Notation "a ≫E_ H E" := (representsEnv C H a E) (at level 70,H at level 0, format "a '≫E_' H E").
Notation "(≫HC)" := (repsHC) (at level 0).
Notation "ψ '≫HC' π" := (repsHC ψ π) (at level 70).
Section unlinPro.
Fixpoint unlinPro (i:nat) (p:PA) : option Pro :=
match i,C p with
| S i, Some (appC) => match unlinPro i (inc p) with
Some P => Some (appT P)
| _ => None
end
| S i, Some (varC x) => match unlinPro i (inc p) with
Some P => Some (varT x P)
| _ => None
end
| S i, Some (retC) => Some retT
| S i, Some (lamC q) => match unlinPro i (inc p),unlinPro i q with
Some P,Some Q => Some (lamT Q P)
| _,_ => None
end
| _,_ => None
end.
Lemma unlinPro_mono i j p P: i <= j -> unlinPro i p = Some P -> unlinPro j p = Some P.
Proof.
induction j in i,p,P|-*.
-destruct i. all:easy.
-destruct i. easy.
+intros H%le_S_n eq.
specialize IHj with (1:=H).
cbn in eq|-*.
destruct (C p) as [[]|] eqn:eq'.
1,5:congruence.
all:repeat (let eq := fresh "eq" in destruct (unlinPro i _) eqn:eq;[apply IHj in eq;try eassumption;rewrite eq in *|congruence]).
all:congruence.
Qed.
Lemma unlinPro_fuel p P: p ≫p_C P -> exists i, unlinPro i p = Some P.
Proof.
induction 1 as [? eq| ? ? ? eq ? (i1&IH)| ? ? ? ? eq ? (i1&IH1) ? (i2&IH2)| ? ? ? eq (i1&IH)].
-exists 1. cbn. now rewrite eq.
-exists (1+i1). cbn. now rewrite eq,IH.
-exists (1+i1+i2). cbn. rewrite eq. do 2 (erewrite unlinPro_mono;[| |eassumption];[|omega]). reflexivity.
-exists (1+i1). cbn. now rewrite H,IH.
Qed.
End unlinPro.
Section unlinEnv.
Variable H:Heap.
Fixpoint unlinClos (i:nat) (p:HC) : option Clo :=
match i,p with
0,_ => None
| S i,(p,a) =>
match unlinPro i p, unlinEnv i a with
Some P, Some E => Some (P/E)
| _,_ => None
end
end
with
unlinEnv (i:nat) (a:HA) : option (list Clo) :=
match i with
0 => None
| S i => match get H a with
None => None
| Some None => Some []
| Some (Some (p,b)) =>
match unlinClos i p,unlinEnv i b with
| Some C, Some A => Some (C::A)
| _,_ => None
end
end
end.
Lemma unlinEnv_mono i j: i <= j -> (forall g e, unlinClos i g = Some e -> unlinClos j g = Some e)
/\ forall a E, (unlinEnv i a = Some E -> unlinEnv j a = Some E).
Proof.
induction j in i|-*.
-destruct i. all:easy.
-destruct i. easy. intros H1%le_S_n. specialize IHj with (1:=H1) as [IHc ILEnv].
split;cbn.
+intros [? ?] ?.
destruct unlinPro eqn:eq. 2:easy. rewrite unlinPro_mono with (1:=H1) (2:=eq).
destruct unlinEnv eqn:eq1. 2:easy. rewrite ILEnv with (1:=eq1). easy.
+intros ? ?. destruct (H a) as [[[]|]|]. 2,3:easy.
destruct unlinClos eqn: eq. 2:easy. rewrite IHc with (1:=eq).
destruct unlinEnv eqn:eq2. 2:easy. rewrite ILEnv with (1:=eq2). easy.
Qed.
Lemma unlinEnv_fuel: (forall a E, a ≫E_H E -> exists n, unlinEnv n a = Some E).
Proof.
induction 1 as [? eq|? ? ? ? ? ? ? eq Rp ? [n1 eq1] ? [n2 eq2]].
-exists 1. cbn. now rewrite eq.
-apply unlinPro_fuel in Rp as [n3 eq3].
eexists (2 + n1 + n2 + n3). cbn. rewrite eq.
eapply unlinEnv_mono in eq1 as ->. 2:omega.
eapply unlinPro_mono in eq3 as ->. 2:omega.
eapply unlinEnv_mono with (j:= S (n1+n2+n3)) in eq2. 2:omega. cbn in eq2. rewrite eq2. tauto.
Qed.
(*
Lemma unlinEnv_fuel: (forall a E, a ≫E_H E -> exists n, unlinEnv n a = Some E)
/\ (forall g e, g ≫C_H e -> exists n, unlinClos n g = Some e).
Proof.
apply unheaped_mutual_ind.
-intros ? ? ? ? ? eq ? n1 eq1 ? n2 eq2.
exists (1+n1+n2). cbn in *. rewrite eq.
eapply unlinEnv_mono in eq1. rewrite eq1. 2:omega.
eapply unlinEnv_mono in eq2. rewrite eq2. 2:omega.
easy.
-intros ? eq. exists 1. cbn in *. now rewrite eq.
-intros ? ? ? ? ? n1 eq1 Rep.
eapply unlinPro_fuel in Rep as n2 eq2.
exists (1+n1+n2). cbn. erewrite unlinPro_mono with (2:=eq2). 2:omega. eapply unlinEnv_mono in eq1. rewrite eq1. 2:omega. tauto.
Qed.
*)
End unlinEnv.
End heap_decomp.
Fixpoint unlinPro (i:nat) (p:PA) : option Pro :=
match i,C p with
| S i, Some (appC) => match unlinPro i (inc p) with
Some P => Some (appT P)
| _ => None
end
| S i, Some (varC x) => match unlinPro i (inc p) with
Some P => Some (varT x P)
| _ => None
end
| S i, Some (retC) => Some retT
| S i, Some (lamC q) => match unlinPro i (inc p),unlinPro i q with
Some P,Some Q => Some (lamT Q P)
| _,_ => None
end
| _,_ => None
end.
Lemma unlinPro_mono i j p P: i <= j -> unlinPro i p = Some P -> unlinPro j p = Some P.
Proof.
induction j in i,p,P|-*.
-destruct i. all:easy.
-destruct i. easy.
+intros H%le_S_n eq.
specialize IHj with (1:=H).
cbn in eq|-*.
destruct (C p) as [[]|] eqn:eq'.
1,5:congruence.
all:repeat (let eq := fresh "eq" in destruct (unlinPro i _) eqn:eq;[apply IHj in eq;try eassumption;rewrite eq in *|congruence]).
all:congruence.
Qed.
Lemma unlinPro_fuel p P: p ≫p_C P -> exists i, unlinPro i p = Some P.
Proof.
induction 1 as [? eq| ? ? ? eq ? (i1&IH)| ? ? ? ? eq ? (i1&IH1) ? (i2&IH2)| ? ? ? eq (i1&IH)].
-exists 1. cbn. now rewrite eq.
-exists (1+i1). cbn. now rewrite eq,IH.
-exists (1+i1+i2). cbn. rewrite eq. do 2 (erewrite unlinPro_mono;[| |eassumption];[|omega]). reflexivity.
-exists (1+i1). cbn. now rewrite H,IH.
Qed.
End unlinPro.
Section unlinEnv.
Variable H:Heap.
Fixpoint unlinClos (i:nat) (p:HC) : option Clo :=
match i,p with
0,_ => None
| S i,(p,a) =>
match unlinPro i p, unlinEnv i a with
Some P, Some E => Some (P/E)
| _,_ => None
end
end
with
unlinEnv (i:nat) (a:HA) : option (list Clo) :=
match i with
0 => None
| S i => match get H a with
None => None
| Some None => Some []
| Some (Some (p,b)) =>
match unlinClos i p,unlinEnv i b with
| Some C, Some A => Some (C::A)
| _,_ => None
end
end
end.
Lemma unlinEnv_mono i j: i <= j -> (forall g e, unlinClos i g = Some e -> unlinClos j g = Some e)
/\ forall a E, (unlinEnv i a = Some E -> unlinEnv j a = Some E).
Proof.
induction j in i|-*.
-destruct i. all:easy.
-destruct i. easy. intros H1%le_S_n. specialize IHj with (1:=H1) as [IHc ILEnv].
split;cbn.
+intros [? ?] ?.
destruct unlinPro eqn:eq. 2:easy. rewrite unlinPro_mono with (1:=H1) (2:=eq).
destruct unlinEnv eqn:eq1. 2:easy. rewrite ILEnv with (1:=eq1). easy.
+intros ? ?. destruct (H a) as [[[]|]|]. 2,3:easy.
destruct unlinClos eqn: eq. 2:easy. rewrite IHc with (1:=eq).
destruct unlinEnv eqn:eq2. 2:easy. rewrite ILEnv with (1:=eq2). easy.
Qed.
Lemma unlinEnv_fuel: (forall a E, a ≫E_H E -> exists n, unlinEnv n a = Some E).
Proof.
induction 1 as [? eq|? ? ? ? ? ? ? eq Rp ? [n1 eq1] ? [n2 eq2]].
-exists 1. cbn. now rewrite eq.
-apply unlinPro_fuel in Rp as [n3 eq3].
eexists (2 + n1 + n2 + n3). cbn. rewrite eq.
eapply unlinEnv_mono in eq1 as ->. 2:omega.
eapply unlinPro_mono in eq3 as ->. 2:omega.
eapply unlinEnv_mono with (j:= S (n1+n2+n3)) in eq2. 2:omega. cbn in eq2. rewrite eq2. tauto.
Qed.
(*
Lemma unlinEnv_fuel: (forall a E, a ≫E_H E -> exists n, unlinEnv n a = Some E)
/\ (forall g e, g ≫C_H e -> exists n, unlinClos n g = Some e).
Proof.
apply unheaped_mutual_ind.
-intros ? ? ? ? ? eq ? n1 eq1 ? n2 eq2.
exists (1+n1+n2). cbn in *. rewrite eq.
eapply unlinEnv_mono in eq1. rewrite eq1. 2:omega.
eapply unlinEnv_mono in eq2. rewrite eq2. 2:omega.
easy.
-intros ? eq. exists 1. cbn in *. now rewrite eq.
-intros ? ? ? ? ? n1 eq1 Rep.
eapply unlinPro_fuel in Rep as n2 eq2.
exists (1+n1+n2). cbn. erewrite unlinPro_mono with (2:=eq2). 2:omega. eapply unlinEnv_mono in eq1. rewrite eq1. 2:omega. tauto.
Qed.
*)
End unlinEnv.
End heap_decomp.