Library Lsemantics
Require Import Omega.
Require Import Min.
Require Import List.
Require Import ext.
Require Import set.
Require Import minmax.
Require Import Llanguage.
Definition Red (R : set) : set := fun b ⇒ ∃ a, R a ∧ red a b.
Hint Unfold Red.
Definition Exp (P : set) (R : set) : set := fun a ⇒ P a ∧ ∀ b, red a b → R b.
Hint Unfold Exp.
Ltac Exp := let Hred := fresh "Hred" in split; [|intros ? Hred; inversion Hred].
Lemma RedCN : Inc (Red CN) CN.
Proof.
intros b [a [CNa Hred]].
inversion Hred; subst; inversion CNa; auto.
Qed.
Inductive Cl (R : set) : set :=
| ClR : ∀ a, R a → Cl R a
| ClExp : ∀ a, N a → (∀ b, red a b → Cl R b) → Cl R a.
Lemma Cl_def : ∀ R, Cl R = Union R (Exp N (Cl R)).
Proof.
intros R; apply extEq; split; intros a Ha.
inversion Ha; subst; [left|right]; auto.
destruct Ha as [?|[? ?]]; [apply ClR|apply ClExp]; auto.
Qed.
Lemma fold_Cl : ∀ R a, (R a ∨ Exp N (Cl R) a) → Cl R a.
Proof. intros; rewrite Cl_def; auto. Qed.
Lemma unfold_Cl : ∀ R a, Cl R a → (R a ∨ Exp N (Cl R) a).
Proof. intros; rewrite Cl_def in H; auto. Qed.
Lemma Cl_monotone : ∀ (R S : set), (∀ a, R a → S a) → ∀ a, Cl R a → Cl S a.
Proof. intros R S RS a Ha; induction Ha; [apply ClR|apply ClExp]; auto. Qed.
Definition Pcn R := Inc R CN.
Definition Psn R := Inc R SN.
Definition Pred R := Inc (Red R) R.
Definition Pexp R := Inc (Exp N R) R.
Hint Unfold Pcn Psn Pred Pexp.
Record C (R : set) : Prop := C_ {
Csn : Psn R ;
Cred : Pred R }.
Arguments Csn [R] _ _ _.
Arguments Cred [R] _ _ _.
Record CT (R : set) : Prop := CT_ {
CTcn : Pcn R ;
CTsn : Psn R ;
CTred : Pred R }.
Arguments CTcn [R] _ _ _.
Arguments CTsn [R] _ _ _.
Arguments CTred [R] _ _ _.
Record CE (R : set) : Prop := CE_ {
CEsn : Psn R ;
CEred : Pred R ;
CEexp : Pexp R }.
Arguments CEsn [R] _ _ _.
Arguments CEred [R] _ _ _.
Arguments CEexp [R] _ _ _.
Lemma CT_CPcn : ∀ R, Pcn R → C R → CT R.
Proof.
intros R PR CR; apply CT_.
apply PR.
apply (Csn CR).
apply (Cred CR).
Qed.
Lemma CE_CPexp : ∀ R, Pexp R → C R → CE R.
Proof.
intros R PR CR; apply CE_.
apply (Csn CR).
apply (Cred CR).
apply PR.
Qed.
Lemma C_CT : ∀ {R}, CT R → C R.
Proof. intros ? [? ? ?]; apply C_; auto. Qed.
Lemma C_CE : ∀ {R}, CE R → C R.
Proof. intros ? [? ? ?]; apply C_; auto. Qed.
Lemma Pred_SN : Pred SN.
Proof. intros b [_ [[a Expa] Hred]]; auto. Qed.
Lemma Pexp_SN : Pexp SN.
Proof. intros a [_ Expa]; apply SN_; auto. Qed.
Lemma Pexp_Cl : ∀ R, Pexp (Cl R).
Proof. intros R a [Na Ha]; rewrite Cl_def; right; auto. Qed.
Lemma Psn_Cl : ∀ R, Psn R → Psn (Cl R).
Proof. intros R CR a Cla. induction Cla; auto using SN. Qed.
Lemma C_Cl : ∀ {R}, C R → C (Cl R).
Proof.
intros R CR; apply C_.
apply Psn_Cl; apply (Csn CR).
intros b [a [Cla Hred]]; rewrite Cl_def in Cla.
destruct Cla as [Pa|[Na Expa]]; auto.
rewrite Cl_def; left; apply (Cred CR); ∃ a; auto.
Qed.
Lemma CE_Cl : ∀ {R}, C R → CE (Cl R).
Proof.
intros R CR.
pose proof (C_Cl CR) as [? ?].
apply CE_; auto.
apply Pexp_Cl.
Qed.
Lemma destruct_Cl_CN : ∀ R a, CN a → Cl R a → R a.
Proof.
intros R a CNa Ha; apply unfold_Cl in Ha as [Ha|[Na _]]; auto.
exfalso; apply (CN_N a); auto.
Qed.
Lemma destruct_Cl_N : ∀ R a, Pcn R → N a → Cl R a → Exp N (Cl R) a.
Proof.
intros R a PR Na Ha; apply unfold_Cl in Ha as [Ha|Expa]; auto.
exfalso; apply (CN_N a); auto.
Qed.
Lemma split_Cl : ∀ (R : set) a, (CN a → R a) → (N a → Exp N (Cl R) a) → Cl R a.
Proof. intros R a H1 H2; destruct (N_dec a); apply fold_Cl; [left|right]; auto. Qed.
Definition Lc R := Inter CN R.
Hint Unfold Lc.
Lemma CT_Lc : ∀ {Q}, C Q → CT (Lc Q).
Proof.
intros Q CQ; apply CT_.
intros a [? ?]; auto.
intros a [? ?]; apply (Csn CQ); auto.
intros b [a [[? ?] ?]].
split; [apply RedCN|apply (Cred CQ)]; ∃ a; auto.
Qed.
Lemma Lc_Cl : ∀ R, CT R → Lc (Cl R) = R.
Proof.
intros R CR; apply extEq; split; intros a Ha.
destruct Ha; apply destruct_Cl_CN; auto.
split; [apply (CTcn CR); auto|].
apply fold_Cl; left; auto.
Qed.
Lemma Cl_Lc : ∀ Q, CE Q → Cl (Lc Q) = Q.
Proof.
intros Q CQ; apply extEq; split; intros a Ha.
induction Ha as [? [? ?]|? ?]; auto.
apply (CEexp CQ); auto.
pose proof (CEsn CQ a Ha).
induction H.
apply split_Cl; intros; auto.
repeat split; auto.
intros b Hred.
apply H0; auto.
apply (CEred CQ); ∃ a; auto.
Qed.
Definition PArr (R S : set) : set := fun lam ⇒
∃ a, lam = Lam a ∧ ∀ b, R b → S (subst b 0 a).
Definition Arr (R S : set) : set := Cl (PArr R S).
Hint Unfold PArr Arr.
Definition PProd (R S : set) : set := fun pair ⇒
∃ a b, pair = Pair a b ∧ R a ∧ S b.
Definition Prod (R S : set) : set := Cl (PProd R S).
Hint Unfold PProd Prod.
Lemma SN_Var : ∀ n, SN (Var n).
Proof. intros n; apply SN_; intros b Hred; inversion Hred. Qed.
Lemma R_Var : ∀ {R n}, Pexp R → R (Var n).
Proof. intros R n CR; apply CR; Exp; simpl; auto. Qed.
Lemma SN_Lam : ∀ {a}, SN a → SN (Lam a).
Proof.
intros a Ha; induction Ha.
apply SN_; intros b Hred; inversion Hred; subst.
apply H0; auto.
Qed.
Lemma SN_Pair : ∀ {a b}, SN a → SN b → SN (Pair a b).
Proof.
intros a b SNa.
generalize b; clear b; induction SNa; intros b SNb; induction SNb.
apply SN_; intros b Hred; inversion Hred; subst.
apply H0; auto using SN.
apply H2; auto.
Qed.
Lemma SN_subst_Var : ∀ a i x, SN (subst (Var x) i a) → SN a.
Proof.
intros a i x SNa.
remember (subst (Var x) i a) as a'.
generalize a i x Heqa'; clear a i x Heqa'; induction SNa; intros; subst.
rename a0 into a.
apply SN_; intros b Hred.
eapply H0; [apply red_subst; apply Hred|reflexivity].
Qed.
Lemma C_PArr : ∀ {R S}, CE R → C S → C (PArr R S).
Proof.
intros R S CR CS.
apply C_.
intros lam [a [Heq Hsub]]; subst.
apply SN_Lam; apply SN_subst_Var with 0 0.
apply (Csn CS); apply Hsub; apply R_Var; apply (CEexp CR).
intros a' [lam [[a [Heq Hsub]] Hred]]; subst.
inversion Hred; subst; rename a'0 into a'.
∃ a'; repeat split; auto.
intros b Rb.
pose proof (red_subst _ _ b H0 0).
apply (Cred CS).
eexists; eauto.
Qed.
Lemma Pcn_PArr : ∀ R S, Pcn (PArr R S).
Proof. intros R S lam [a [Heq _]]; subst; exact I. Qed.
Lemma CT_PArr : ∀ {R S}, CE R → C S → CT (PArr R S).
Proof.
intros; apply CT_CPcn.
apply Pcn_PArr.
apply C_PArr; auto.
Qed.
Lemma CE_Arr : ∀ {R S}, CE R → C S → CE (Arr R S).
Proof.
intros; apply CE_Cl.
apply C_PArr; auto.
Qed.
Lemma C_PProd : ∀ {R S}, C R → C S → C (PProd R S).
Proof.
intros R S CR CS.
apply C_.
intros pair [a [b [Heq [? ?]]]]; subst.
apply SN_Pair; [apply (Csn CR)|apply (Csn CS)]; auto.
intros a' [pair [[a [b [Heq [? ?]]]] Hred]]; subst.
inversion Hred; subst; [rename a'0 into a'|];
[∃ a', b|∃ a, b']; repeat split; auto;
[apply (Cred CR); ∃ a|apply (Cred CS); ∃ b]; auto.
Qed.
Lemma Pcn_PProd : ∀ R S, Pcn (PProd R S).
Proof. intros R S pair [a [b [Heq _]]]; subst; exact I. Qed.
Lemma CT_PProd : ∀ {R S}, C R → C S → CT (PProd R S).
Proof.
intros; apply CT_CPcn.
apply Pcn_PProd.
apply C_PProd; auto.
Qed.
Lemma CE_Prod : ∀ {R S}, C R → C S → CE (Prod R S).
Proof.
intros; apply CE_Cl.
apply C_PProd; auto.
Qed.
Definition For I (cond : I → Prop) (func : ∀ i, cond i → set) : set := fun a ⇒
∀ i H, func i H a.
Definition For_preserve P := ∀ Ix cond func, (∃ i, cond i) →
(∀ i H, P (func i H)) → P (For Ix cond func).
Hint Unfold For For_preserve.
Lemma C_For : For_preserve C.
Proof.
intros Ix cond func [wit cwit] Hfor; apply C_.
intros a Ha; apply (Csn (Hfor wit cwit)); apply Ha; apply cwit.
intros b [a [Ha Hred]] i ci; apply (Cred (Hfor i ci)); ∃ a;
split; [apply Ha; apply ci|apply Hred].
Qed.
Lemma Pcn_For : For_preserve Pcn.
Proof.
intros Ix cond func [wit cwit] Hfor a Ha.
apply (Hfor wit cwit a (Ha wit cwit)).
Qed.
Lemma CT_For : For_preserve CT.
Proof.
intros Ix cond func wit Hfor.
apply CT_CPcn.
apply Pcn_For; auto; intros; apply CTcn; auto.
apply C_For; auto; intros; apply C_CT; auto.
Qed.
Lemma Pexp_For : For_preserve Pexp.
Proof.
intros Ix cond func [wit cwit] Hfor a [NVa Expa] i ci.
apply (Hfor i ci); split; auto; intros b Hred.
apply (Expa b Hred i ci).
Qed.
Lemma CE_For : For_preserve CE.
Proof.
intros Ix cond func wit Hfor.
apply CE_CPexp.
apply Pexp_For; auto; intros; apply CEexp; auto.
apply C_For; auto; intros; apply C_CE; auto.
Qed.
Definition PExi I (cond : I → Prop) (func : ∀ i, cond i → set) : set :=
fun a ⇒ ∃ i H, func i H a.
Definition PExi_preserve P := ∀ Ix cond func,
(∀ i H, P (func i H)) → P (PExi Ix cond func).
Definition Exi I cond func := Cl (PExi I cond func).
Definition Exi_preserve P Q := ∀ Ix cond func,
(∀ i H, P (func i H)) → Q (Exi Ix cond func).
Hint Unfold PExi Exi PExi_preserve Exi_preserve.
Lemma C_PExi : PExi_preserve C.
Proof.
intros Ix cond func Hfor; apply C_.
intros a [i [Ci Ha]]; apply (Csn (Hfor i Ci)); apply Ha.
intros b [a [[i [Ci Hb]] ba]]; ∃ i, Ci.
apply (Cred (Hfor i Ci)); ∃ a; auto.
Qed.
Lemma Pcn_PExi : PExi_preserve Pcn.
Proof.
intros Ix cond func Hexi a [i [Ci Ha]].
apply (Hexi i Ci a Ha).
Qed.
Lemma CT_PExi : PExi_preserve CT.
Proof.
intros Ix cond func Hexi.
apply CT_CPcn.
apply Pcn_PExi; auto; intros; apply CTcn; auto.
apply C_PExi; auto; intros; apply C_CT; auto.
Qed.
Lemma Pexp_Exi : Exi_preserve (fun _ ⇒ True) Pexp.
Proof.
intros Ix cond func Hexi a [NVa Expa].
apply fold_Cl; right; auto.
Qed.
Lemma CE_Exi : Exi_preserve C CE.
Proof.
intros Ix cond func Hexi.
apply CE_CPexp.
apply Pexp_Exi; auto.
apply C_Cl; apply C_PExi; auto.
Qed.
Definition Top : set := Exi set CE (fun R _ ⇒ R).
Lemma CE_Top : CE Top.
Proof. apply CE_Exi; intros i H; apply C_CE; auto. Qed.
Lemma C_Top : C Top.
Proof. apply C_CE; apply CE_Top. Qed.
Definition Bot : set := For set CE (fun R _ ⇒ R).
Lemma CE_Bot : CE Bot.
Proof.
apply CE_For.
∃ Top; apply CE_Top.
intros i H; exact H.
Qed.
Lemma C_Bot : C Bot.
Proof. apply C_CE; apply CE_Bot. Qed.
Definition Subst (R S : set) : set := fun a ⇒ ∀ b, R b → S (subst b 0 a).
Hint Unfold Subst.
Fixpoint Judg (G : list set) (S : set) : set :=
match G with
| nil ⇒ S
| cons R G ⇒ Subst (Judg G R) (Judg G S)
end.
Lemma Pred_Judg : ∀ G S, C S → Pred (Judg G S).
Proof.
induction G as [|R G]; intros S CS a' [a [Ha ba]]; simpl in ×.
apply (Cred CS); ∃ a; auto.
intros b Hb; apply IHG; auto.
∃ (subst b 0 a); split; auto.
apply red_subst; auto.
Qed.
Lemma Judg_Var : ∀ G S, Pexp S → Judg G S (Var (length G + 1)).
Proof.
intros G S CS; induction G; simpl.
apply R_Var; auto.
intros b Hb.
simpl; subst_lift_var.
rewrite <- minus_n_O.
apply IHG.
Qed.
Lemma Psn_Judg : ∀ G S, Forall Pexp G → C S → Psn (Judg G S).
Proof.
induction G as [|R G]; intros S CG CS a Ha; simpl in ×.
apply (Csn CS); auto.
apply SN_subst_Var with (x := (length G + 1)) (i := 0).
inversion CG; subst.
apply (IHG S H2 CS _).
apply Ha; apply Judg_Var; auto.
Qed.
Lemma C_Judg : ∀ G S, Forall Pexp G → C S → C (Judg G S).
Proof.
intros G S CG CS; apply C_.
apply Psn_Judg; auto.
apply Pred_Judg; auto.
Qed.
Lemma Var_sem : ∀ R x G, Forall C G →
nth x G Top = R →
Judg G R (Var x).
Proof.
induction x; intros G CG Hx;
(destruct G as [|R0 G]; simpl in *; subst; [apply R_Var; apply Pexp_Cl|]).
intros b Rb; simpl; subst_lift_var; rewrite lift_0.
inversion CG; auto.
inversion CG; subst.
intros b0 Rb0.
simpl; subst_lift_var; rewrite <- minus_n_O.
apply IHx; auto.
Qed.
Lemma Lam_sem : ∀ G R S a, Pexp R → C S →
Judg (R :: G) S a →
Judg G (Arr R S) (Lam a).
Proof.
induction G as [|R0 G]; intros R S a CR CS Ha; simpl in ×.
apply fold_Cl; left.
∃ a; repeat split.
intros b Rb; auto.
intros b0 Rb0; subst; simpl.
apply IHG; auto.
intros b Rb.
replace b with (subst b0 0 (shift 0 b)); [|apply subst_lift_0].
rewrite <- subst_subst_0; apply Ha; auto.
intros ? ?; rewrite subst_lift_0; auto.
Qed.
Lemma App_sem : ∀ G R S a b, CE R → CE S →
Judg G (Arr R S) a →
Judg G R b →
Judg G S (App a b).
Proof.
induction G as [|R0 G]; intros R S a b CR CS Ha Hb; simpl in ×.
pose proof (CE_Arr CR (C_CE CS)) as CRS.
pose proof (CEsn CRS a Ha) as SNa.
pose proof (CEsn CR b Hb) as SNb.
generalize Ha Hb; clear Ha Hb; induction SNa; induction SNb; intros Ha Hb.
rename a0 into b.
apply (CEexp CS); repeat split; auto.
intros b0 Hred; inversion Hred; subst.
apply H0; auto; apply (CEred CRS); ∃ a; auto.
apply H2; auto; [|apply (CEred CR); ∃ b; auto].
intros.
apply (CEred CS); ∃ (App b0 b); split; auto.
apply RedCtxApp2; auto.
clear H1 H H0 H2 Hred.
apply (destruct_Cl_CN (PArr R S) (Lam a0)) in Ha; simpl; auto.
destruct Ha as [a [Heq Hsub]].
inversion Heq; clear Heq; subst; auto.
intros b0 Rb0; simpl.
apply (IHG R S); auto.
Qed.
Lemma Pair_sem : ∀ G R S a b, C R → C S →
Judg G R a →
Judg G S b →
Judg G (Prod R S) (Pair a b).
Proof.
induction G as [|R0 G]; intros R S a b CR CS Ha Hb; simpl in ×.
apply fold_Cl; left.
∃ a, b; repeat split; auto.
intros b0 Rb0; simpl; apply IHG; auto.
Qed.
Lemma Fst_sem : ∀ G R S a, CE R → C S →
Judg G (Prod R S) a →
Judg G R (Fst a).
Proof.
induction G as [|R0 G]; intros R S a CR CS Ha; simpl in ×.
pose proof (CE_Prod (C_CE CR) CS) as CRS.
pose proof (CEsn CRS a Ha) as SNa.
generalize Ha; induction SNa; intros.
apply (CEexp CR); repeat split; simpl; auto.
intros b0 Hred; inversion Hred; subst.
apply H0; auto; apply (CEred CRS); ∃ a; auto.
clear H H0 Ha0.
apply (destruct_Cl_CN (PProd R S) (Pair b0 b)) in Ha; simpl; auto.
destruct Ha as [a [b' [Heq [? ?]]]].
inversion Heq; clear Heq; subst; auto.
intros b0 Rb0; simpl.
apply (IHG R S); auto.
Qed.
Lemma Snd_sem : ∀ G R S a, C R → CE S →
Judg G (Prod R S) a →
Judg G S (Snd a).
Proof.
induction G as [|R0 G]; intros R S a CR CS Ha; simpl in ×.
pose proof (CE_Prod CR (C_CE CS)) as CRS.
pose proof (CEsn CRS a Ha) as SNa.
generalize Ha; induction SNa; intros.
apply (CEexp CS); repeat split; simpl; auto.
intros b0 Hred; inversion Hred; subst.
apply H0; auto; apply (CEred CRS); ∃ a; auto.
clear H H0 Ha0.
apply (destruct_Cl_CN (PProd R S) (Pair a0 b0)) in Ha; simpl; auto.
destruct Ha as [a [b' [Heq [? ?]]]].
inversion Heq; clear Heq; subst; auto.
intros b0 Rb0; simpl.
apply (IHG R S); auto.
Qed.
Lemma Coer_sem : ∀ G R S, Inc R S → ∀ a, Judg G R a → Judg G S a.
Proof.
induction G as [|R0 G]; intros R S RS a Ha; simpl in *; auto.
intros b0 Rb0.
apply (IHG R S); auto.
Qed.
Lemma distrib : ∀ I cond func G a,
(∃ i, cond i) → (∀ i H, CE (func i H)) →
For I cond (fun i H ⇒ Judg G (func i H)) a →
Judg G (For I cond func) a.
Proof.
induction G as [|R G]; intros a Hexi CEfunc H; auto; simpl.
intros b0 Rb0; match goal with | |- ?J _ _ _ ⇒ replace J with Judg by reflexivity end.
apply IHG; auto; intros i Hi; apply H; auto.
Qed.
Require Import Min.
Require Import List.
Require Import ext.
Require Import set.
Require Import minmax.
Require Import Llanguage.
Definition Red (R : set) : set := fun b ⇒ ∃ a, R a ∧ red a b.
Hint Unfold Red.
Definition Exp (P : set) (R : set) : set := fun a ⇒ P a ∧ ∀ b, red a b → R b.
Hint Unfold Exp.
Ltac Exp := let Hred := fresh "Hred" in split; [|intros ? Hred; inversion Hred].
Lemma RedCN : Inc (Red CN) CN.
Proof.
intros b [a [CNa Hred]].
inversion Hred; subst; inversion CNa; auto.
Qed.
Inductive Cl (R : set) : set :=
| ClR : ∀ a, R a → Cl R a
| ClExp : ∀ a, N a → (∀ b, red a b → Cl R b) → Cl R a.
Lemma Cl_def : ∀ R, Cl R = Union R (Exp N (Cl R)).
Proof.
intros R; apply extEq; split; intros a Ha.
inversion Ha; subst; [left|right]; auto.
destruct Ha as [?|[? ?]]; [apply ClR|apply ClExp]; auto.
Qed.
Lemma fold_Cl : ∀ R a, (R a ∨ Exp N (Cl R) a) → Cl R a.
Proof. intros; rewrite Cl_def; auto. Qed.
Lemma unfold_Cl : ∀ R a, Cl R a → (R a ∨ Exp N (Cl R) a).
Proof. intros; rewrite Cl_def in H; auto. Qed.
Lemma Cl_monotone : ∀ (R S : set), (∀ a, R a → S a) → ∀ a, Cl R a → Cl S a.
Proof. intros R S RS a Ha; induction Ha; [apply ClR|apply ClExp]; auto. Qed.
Definition Pcn R := Inc R CN.
Definition Psn R := Inc R SN.
Definition Pred R := Inc (Red R) R.
Definition Pexp R := Inc (Exp N R) R.
Hint Unfold Pcn Psn Pred Pexp.
Record C (R : set) : Prop := C_ {
Csn : Psn R ;
Cred : Pred R }.
Arguments Csn [R] _ _ _.
Arguments Cred [R] _ _ _.
Record CT (R : set) : Prop := CT_ {
CTcn : Pcn R ;
CTsn : Psn R ;
CTred : Pred R }.
Arguments CTcn [R] _ _ _.
Arguments CTsn [R] _ _ _.
Arguments CTred [R] _ _ _.
Record CE (R : set) : Prop := CE_ {
CEsn : Psn R ;
CEred : Pred R ;
CEexp : Pexp R }.
Arguments CEsn [R] _ _ _.
Arguments CEred [R] _ _ _.
Arguments CEexp [R] _ _ _.
Lemma CT_CPcn : ∀ R, Pcn R → C R → CT R.
Proof.
intros R PR CR; apply CT_.
apply PR.
apply (Csn CR).
apply (Cred CR).
Qed.
Lemma CE_CPexp : ∀ R, Pexp R → C R → CE R.
Proof.
intros R PR CR; apply CE_.
apply (Csn CR).
apply (Cred CR).
apply PR.
Qed.
Lemma C_CT : ∀ {R}, CT R → C R.
Proof. intros ? [? ? ?]; apply C_; auto. Qed.
Lemma C_CE : ∀ {R}, CE R → C R.
Proof. intros ? [? ? ?]; apply C_; auto. Qed.
Lemma Pred_SN : Pred SN.
Proof. intros b [_ [[a Expa] Hred]]; auto. Qed.
Lemma Pexp_SN : Pexp SN.
Proof. intros a [_ Expa]; apply SN_; auto. Qed.
Lemma Pexp_Cl : ∀ R, Pexp (Cl R).
Proof. intros R a [Na Ha]; rewrite Cl_def; right; auto. Qed.
Lemma Psn_Cl : ∀ R, Psn R → Psn (Cl R).
Proof. intros R CR a Cla. induction Cla; auto using SN. Qed.
Lemma C_Cl : ∀ {R}, C R → C (Cl R).
Proof.
intros R CR; apply C_.
apply Psn_Cl; apply (Csn CR).
intros b [a [Cla Hred]]; rewrite Cl_def in Cla.
destruct Cla as [Pa|[Na Expa]]; auto.
rewrite Cl_def; left; apply (Cred CR); ∃ a; auto.
Qed.
Lemma CE_Cl : ∀ {R}, C R → CE (Cl R).
Proof.
intros R CR.
pose proof (C_Cl CR) as [? ?].
apply CE_; auto.
apply Pexp_Cl.
Qed.
Lemma destruct_Cl_CN : ∀ R a, CN a → Cl R a → R a.
Proof.
intros R a CNa Ha; apply unfold_Cl in Ha as [Ha|[Na _]]; auto.
exfalso; apply (CN_N a); auto.
Qed.
Lemma destruct_Cl_N : ∀ R a, Pcn R → N a → Cl R a → Exp N (Cl R) a.
Proof.
intros R a PR Na Ha; apply unfold_Cl in Ha as [Ha|Expa]; auto.
exfalso; apply (CN_N a); auto.
Qed.
Lemma split_Cl : ∀ (R : set) a, (CN a → R a) → (N a → Exp N (Cl R) a) → Cl R a.
Proof. intros R a H1 H2; destruct (N_dec a); apply fold_Cl; [left|right]; auto. Qed.
Definition Lc R := Inter CN R.
Hint Unfold Lc.
Lemma CT_Lc : ∀ {Q}, C Q → CT (Lc Q).
Proof.
intros Q CQ; apply CT_.
intros a [? ?]; auto.
intros a [? ?]; apply (Csn CQ); auto.
intros b [a [[? ?] ?]].
split; [apply RedCN|apply (Cred CQ)]; ∃ a; auto.
Qed.
Lemma Lc_Cl : ∀ R, CT R → Lc (Cl R) = R.
Proof.
intros R CR; apply extEq; split; intros a Ha.
destruct Ha; apply destruct_Cl_CN; auto.
split; [apply (CTcn CR); auto|].
apply fold_Cl; left; auto.
Qed.
Lemma Cl_Lc : ∀ Q, CE Q → Cl (Lc Q) = Q.
Proof.
intros Q CQ; apply extEq; split; intros a Ha.
induction Ha as [? [? ?]|? ?]; auto.
apply (CEexp CQ); auto.
pose proof (CEsn CQ a Ha).
induction H.
apply split_Cl; intros; auto.
repeat split; auto.
intros b Hred.
apply H0; auto.
apply (CEred CQ); ∃ a; auto.
Qed.
Definition PArr (R S : set) : set := fun lam ⇒
∃ a, lam = Lam a ∧ ∀ b, R b → S (subst b 0 a).
Definition Arr (R S : set) : set := Cl (PArr R S).
Hint Unfold PArr Arr.
Definition PProd (R S : set) : set := fun pair ⇒
∃ a b, pair = Pair a b ∧ R a ∧ S b.
Definition Prod (R S : set) : set := Cl (PProd R S).
Hint Unfold PProd Prod.
Lemma SN_Var : ∀ n, SN (Var n).
Proof. intros n; apply SN_; intros b Hred; inversion Hred. Qed.
Lemma R_Var : ∀ {R n}, Pexp R → R (Var n).
Proof. intros R n CR; apply CR; Exp; simpl; auto. Qed.
Lemma SN_Lam : ∀ {a}, SN a → SN (Lam a).
Proof.
intros a Ha; induction Ha.
apply SN_; intros b Hred; inversion Hred; subst.
apply H0; auto.
Qed.
Lemma SN_Pair : ∀ {a b}, SN a → SN b → SN (Pair a b).
Proof.
intros a b SNa.
generalize b; clear b; induction SNa; intros b SNb; induction SNb.
apply SN_; intros b Hred; inversion Hred; subst.
apply H0; auto using SN.
apply H2; auto.
Qed.
Lemma SN_subst_Var : ∀ a i x, SN (subst (Var x) i a) → SN a.
Proof.
intros a i x SNa.
remember (subst (Var x) i a) as a'.
generalize a i x Heqa'; clear a i x Heqa'; induction SNa; intros; subst.
rename a0 into a.
apply SN_; intros b Hred.
eapply H0; [apply red_subst; apply Hred|reflexivity].
Qed.
Lemma C_PArr : ∀ {R S}, CE R → C S → C (PArr R S).
Proof.
intros R S CR CS.
apply C_.
intros lam [a [Heq Hsub]]; subst.
apply SN_Lam; apply SN_subst_Var with 0 0.
apply (Csn CS); apply Hsub; apply R_Var; apply (CEexp CR).
intros a' [lam [[a [Heq Hsub]] Hred]]; subst.
inversion Hred; subst; rename a'0 into a'.
∃ a'; repeat split; auto.
intros b Rb.
pose proof (red_subst _ _ b H0 0).
apply (Cred CS).
eexists; eauto.
Qed.
Lemma Pcn_PArr : ∀ R S, Pcn (PArr R S).
Proof. intros R S lam [a [Heq _]]; subst; exact I. Qed.
Lemma CT_PArr : ∀ {R S}, CE R → C S → CT (PArr R S).
Proof.
intros; apply CT_CPcn.
apply Pcn_PArr.
apply C_PArr; auto.
Qed.
Lemma CE_Arr : ∀ {R S}, CE R → C S → CE (Arr R S).
Proof.
intros; apply CE_Cl.
apply C_PArr; auto.
Qed.
Lemma C_PProd : ∀ {R S}, C R → C S → C (PProd R S).
Proof.
intros R S CR CS.
apply C_.
intros pair [a [b [Heq [? ?]]]]; subst.
apply SN_Pair; [apply (Csn CR)|apply (Csn CS)]; auto.
intros a' [pair [[a [b [Heq [? ?]]]] Hred]]; subst.
inversion Hred; subst; [rename a'0 into a'|];
[∃ a', b|∃ a, b']; repeat split; auto;
[apply (Cred CR); ∃ a|apply (Cred CS); ∃ b]; auto.
Qed.
Lemma Pcn_PProd : ∀ R S, Pcn (PProd R S).
Proof. intros R S pair [a [b [Heq _]]]; subst; exact I. Qed.
Lemma CT_PProd : ∀ {R S}, C R → C S → CT (PProd R S).
Proof.
intros; apply CT_CPcn.
apply Pcn_PProd.
apply C_PProd; auto.
Qed.
Lemma CE_Prod : ∀ {R S}, C R → C S → CE (Prod R S).
Proof.
intros; apply CE_Cl.
apply C_PProd; auto.
Qed.
Definition For I (cond : I → Prop) (func : ∀ i, cond i → set) : set := fun a ⇒
∀ i H, func i H a.
Definition For_preserve P := ∀ Ix cond func, (∃ i, cond i) →
(∀ i H, P (func i H)) → P (For Ix cond func).
Hint Unfold For For_preserve.
Lemma C_For : For_preserve C.
Proof.
intros Ix cond func [wit cwit] Hfor; apply C_.
intros a Ha; apply (Csn (Hfor wit cwit)); apply Ha; apply cwit.
intros b [a [Ha Hred]] i ci; apply (Cred (Hfor i ci)); ∃ a;
split; [apply Ha; apply ci|apply Hred].
Qed.
Lemma Pcn_For : For_preserve Pcn.
Proof.
intros Ix cond func [wit cwit] Hfor a Ha.
apply (Hfor wit cwit a (Ha wit cwit)).
Qed.
Lemma CT_For : For_preserve CT.
Proof.
intros Ix cond func wit Hfor.
apply CT_CPcn.
apply Pcn_For; auto; intros; apply CTcn; auto.
apply C_For; auto; intros; apply C_CT; auto.
Qed.
Lemma Pexp_For : For_preserve Pexp.
Proof.
intros Ix cond func [wit cwit] Hfor a [NVa Expa] i ci.
apply (Hfor i ci); split; auto; intros b Hred.
apply (Expa b Hred i ci).
Qed.
Lemma CE_For : For_preserve CE.
Proof.
intros Ix cond func wit Hfor.
apply CE_CPexp.
apply Pexp_For; auto; intros; apply CEexp; auto.
apply C_For; auto; intros; apply C_CE; auto.
Qed.
Definition PExi I (cond : I → Prop) (func : ∀ i, cond i → set) : set :=
fun a ⇒ ∃ i H, func i H a.
Definition PExi_preserve P := ∀ Ix cond func,
(∀ i H, P (func i H)) → P (PExi Ix cond func).
Definition Exi I cond func := Cl (PExi I cond func).
Definition Exi_preserve P Q := ∀ Ix cond func,
(∀ i H, P (func i H)) → Q (Exi Ix cond func).
Hint Unfold PExi Exi PExi_preserve Exi_preserve.
Lemma C_PExi : PExi_preserve C.
Proof.
intros Ix cond func Hfor; apply C_.
intros a [i [Ci Ha]]; apply (Csn (Hfor i Ci)); apply Ha.
intros b [a [[i [Ci Hb]] ba]]; ∃ i, Ci.
apply (Cred (Hfor i Ci)); ∃ a; auto.
Qed.
Lemma Pcn_PExi : PExi_preserve Pcn.
Proof.
intros Ix cond func Hexi a [i [Ci Ha]].
apply (Hexi i Ci a Ha).
Qed.
Lemma CT_PExi : PExi_preserve CT.
Proof.
intros Ix cond func Hexi.
apply CT_CPcn.
apply Pcn_PExi; auto; intros; apply CTcn; auto.
apply C_PExi; auto; intros; apply C_CT; auto.
Qed.
Lemma Pexp_Exi : Exi_preserve (fun _ ⇒ True) Pexp.
Proof.
intros Ix cond func Hexi a [NVa Expa].
apply fold_Cl; right; auto.
Qed.
Lemma CE_Exi : Exi_preserve C CE.
Proof.
intros Ix cond func Hexi.
apply CE_CPexp.
apply Pexp_Exi; auto.
apply C_Cl; apply C_PExi; auto.
Qed.
Definition Top : set := Exi set CE (fun R _ ⇒ R).
Lemma CE_Top : CE Top.
Proof. apply CE_Exi; intros i H; apply C_CE; auto. Qed.
Lemma C_Top : C Top.
Proof. apply C_CE; apply CE_Top. Qed.
Definition Bot : set := For set CE (fun R _ ⇒ R).
Lemma CE_Bot : CE Bot.
Proof.
apply CE_For.
∃ Top; apply CE_Top.
intros i H; exact H.
Qed.
Lemma C_Bot : C Bot.
Proof. apply C_CE; apply CE_Bot. Qed.
Definition Subst (R S : set) : set := fun a ⇒ ∀ b, R b → S (subst b 0 a).
Hint Unfold Subst.
Fixpoint Judg (G : list set) (S : set) : set :=
match G with
| nil ⇒ S
| cons R G ⇒ Subst (Judg G R) (Judg G S)
end.
Lemma Pred_Judg : ∀ G S, C S → Pred (Judg G S).
Proof.
induction G as [|R G]; intros S CS a' [a [Ha ba]]; simpl in ×.
apply (Cred CS); ∃ a; auto.
intros b Hb; apply IHG; auto.
∃ (subst b 0 a); split; auto.
apply red_subst; auto.
Qed.
Lemma Judg_Var : ∀ G S, Pexp S → Judg G S (Var (length G + 1)).
Proof.
intros G S CS; induction G; simpl.
apply R_Var; auto.
intros b Hb.
simpl; subst_lift_var.
rewrite <- minus_n_O.
apply IHG.
Qed.
Lemma Psn_Judg : ∀ G S, Forall Pexp G → C S → Psn (Judg G S).
Proof.
induction G as [|R G]; intros S CG CS a Ha; simpl in ×.
apply (Csn CS); auto.
apply SN_subst_Var with (x := (length G + 1)) (i := 0).
inversion CG; subst.
apply (IHG S H2 CS _).
apply Ha; apply Judg_Var; auto.
Qed.
Lemma C_Judg : ∀ G S, Forall Pexp G → C S → C (Judg G S).
Proof.
intros G S CG CS; apply C_.
apply Psn_Judg; auto.
apply Pred_Judg; auto.
Qed.
Lemma Var_sem : ∀ R x G, Forall C G →
nth x G Top = R →
Judg G R (Var x).
Proof.
induction x; intros G CG Hx;
(destruct G as [|R0 G]; simpl in *; subst; [apply R_Var; apply Pexp_Cl|]).
intros b Rb; simpl; subst_lift_var; rewrite lift_0.
inversion CG; auto.
inversion CG; subst.
intros b0 Rb0.
simpl; subst_lift_var; rewrite <- minus_n_O.
apply IHx; auto.
Qed.
Lemma Lam_sem : ∀ G R S a, Pexp R → C S →
Judg (R :: G) S a →
Judg G (Arr R S) (Lam a).
Proof.
induction G as [|R0 G]; intros R S a CR CS Ha; simpl in ×.
apply fold_Cl; left.
∃ a; repeat split.
intros b Rb; auto.
intros b0 Rb0; subst; simpl.
apply IHG; auto.
intros b Rb.
replace b with (subst b0 0 (shift 0 b)); [|apply subst_lift_0].
rewrite <- subst_subst_0; apply Ha; auto.
intros ? ?; rewrite subst_lift_0; auto.
Qed.
Lemma App_sem : ∀ G R S a b, CE R → CE S →
Judg G (Arr R S) a →
Judg G R b →
Judg G S (App a b).
Proof.
induction G as [|R0 G]; intros R S a b CR CS Ha Hb; simpl in ×.
pose proof (CE_Arr CR (C_CE CS)) as CRS.
pose proof (CEsn CRS a Ha) as SNa.
pose proof (CEsn CR b Hb) as SNb.
generalize Ha Hb; clear Ha Hb; induction SNa; induction SNb; intros Ha Hb.
rename a0 into b.
apply (CEexp CS); repeat split; auto.
intros b0 Hred; inversion Hred; subst.
apply H0; auto; apply (CEred CRS); ∃ a; auto.
apply H2; auto; [|apply (CEred CR); ∃ b; auto].
intros.
apply (CEred CS); ∃ (App b0 b); split; auto.
apply RedCtxApp2; auto.
clear H1 H H0 H2 Hred.
apply (destruct_Cl_CN (PArr R S) (Lam a0)) in Ha; simpl; auto.
destruct Ha as [a [Heq Hsub]].
inversion Heq; clear Heq; subst; auto.
intros b0 Rb0; simpl.
apply (IHG R S); auto.
Qed.
Lemma Pair_sem : ∀ G R S a b, C R → C S →
Judg G R a →
Judg G S b →
Judg G (Prod R S) (Pair a b).
Proof.
induction G as [|R0 G]; intros R S a b CR CS Ha Hb; simpl in ×.
apply fold_Cl; left.
∃ a, b; repeat split; auto.
intros b0 Rb0; simpl; apply IHG; auto.
Qed.
Lemma Fst_sem : ∀ G R S a, CE R → C S →
Judg G (Prod R S) a →
Judg G R (Fst a).
Proof.
induction G as [|R0 G]; intros R S a CR CS Ha; simpl in ×.
pose proof (CE_Prod (C_CE CR) CS) as CRS.
pose proof (CEsn CRS a Ha) as SNa.
generalize Ha; induction SNa; intros.
apply (CEexp CR); repeat split; simpl; auto.
intros b0 Hred; inversion Hred; subst.
apply H0; auto; apply (CEred CRS); ∃ a; auto.
clear H H0 Ha0.
apply (destruct_Cl_CN (PProd R S) (Pair b0 b)) in Ha; simpl; auto.
destruct Ha as [a [b' [Heq [? ?]]]].
inversion Heq; clear Heq; subst; auto.
intros b0 Rb0; simpl.
apply (IHG R S); auto.
Qed.
Lemma Snd_sem : ∀ G R S a, C R → CE S →
Judg G (Prod R S) a →
Judg G S (Snd a).
Proof.
induction G as [|R0 G]; intros R S a CR CS Ha; simpl in ×.
pose proof (CE_Prod CR (C_CE CS)) as CRS.
pose proof (CEsn CRS a Ha) as SNa.
generalize Ha; induction SNa; intros.
apply (CEexp CS); repeat split; simpl; auto.
intros b0 Hred; inversion Hred; subst.
apply H0; auto; apply (CEred CRS); ∃ a; auto.
clear H H0 Ha0.
apply (destruct_Cl_CN (PProd R S) (Pair a0 b0)) in Ha; simpl; auto.
destruct Ha as [a [b' [Heq [? ?]]]].
inversion Heq; clear Heq; subst; auto.
intros b0 Rb0; simpl.
apply (IHG R S); auto.
Qed.
Lemma Coer_sem : ∀ G R S, Inc R S → ∀ a, Judg G R a → Judg G S a.
Proof.
induction G as [|R0 G]; intros R S RS a Ha; simpl in *; auto.
intros b0 Rb0.
apply (IHG R S); auto.
Qed.
Lemma distrib : ∀ I cond func G a,
(∃ i, cond i) → (∀ i H, CE (func i H)) →
For I cond (fun i H ⇒ Judg G (func i H)) a →
Judg G (For I cond func) a.
Proof.
induction G as [|R G]; intros a Hexi CEfunc H; auto; simpl.
intros b0 Rb0; match goal with | |- ?J _ _ _ ⇒ replace J with Judg by reflexivity end.
apply IHG; auto; intros i Hi; apply H; auto.
Qed.