CPPsiteProjPackage.CPP_BiInt_ModEx_constr
Require Import List.
Export ListNotations.
Require Import PeanoNat.
Require Import Lia.
Require Import Ensembles.
Require Import CPP_BiInt_GHC.
Require Import CPP_BiInt_logic.
Require Import CPP_BiInt_Kripke_sem_constr.
Require Import CPP_BiInt_soundness_constr.
Require Import CPP_BiInt_meta_interactions1.
Require Import CPP_BiInt_meta_interactions2.
Require Import CPP_BiInt_Lindenbaum_lem.
(* Assume enough variables in V *)
Variable i : nat -> nat.
Definition Var' n := Var (i n).
(* Model Existence implies WLEM *)
Section WLEM.
Variable P : Prop.
Let TP phi :=
phi = Or (Var' 0) (Neg (Var' 0)) \/ P /\ phi = Var' 0 \/ ~ P /\ phi = Neg (Var' 0).
Instance trivial_model :
model.
Proof.
unshelve econstructor.
- exact unit.
- exact (fun _ _ => True).
- exact (fun _ _ => P).
- split; auto.
- cbn. trivial.
- intuition.
Defined.
Lemma trivial_model_dec :
~ ~ model_dec trivial_model.
Proof.
intros H. assert (HP : ~ ~ (P \/ ~ P)) by tauto. apply HP. intros HP'.
apply H. intros [] A. induction A; cbn; try now intuition.
- destruct IHA1, IHA2.
+ left. now intros [].
+ right. firstorder.
+ left. now intros [].
+ left. now intros [].
- destruct IHA1, IHA2.
+ right. intro. apply H2. intros. destruct v ; auto.
+ left. intro. auto.
+ right. intro. apply H2. intros. destruct v ; auto.
+ right. intro. apply H2. intros. destruct v ; auto. exfalso ; auto.
Qed.
Lemma TP_consistent :
~ BIH_rules (TP, Bot).
Proof.
intros H. apply trivial_model_dec. intros HM.
assert (HP : ~ ~ (P \/ ~ P)) by tauto. apply HP. intros HP'.
apply (wSoundness_dec) in H. destruct (H trivial_model tt).
- apply HM.
- intros A [->|[[HA ->]|[HA ->]]]; cbn; intuition.
Qed.
Definition ModEx :=
forall T, ~ BIH_rules (T, Bot) -> exists M (w: @nodes M), forall A, In _ T A -> wforces M w A.
Theorem ModEx_WLEM :
ModEx -> ~ P \/ ~ ~ P.
Proof.
intros HME. destruct (@HME TP TP_consistent) as [M[w HM]].
destruct (HM (Or (Var' 0) (Neg (Var' 0)))) as [H|H].
- now left.
- right. intros HP. assert (HTP : TP (Neg (Var' 0))) by (unfold TP; intuition).
apply (HM (Neg (Var' 0)) HTP w); try apply reach_refl. apply H.
- left. intros HP. apply (H w); try apply reach_refl.
assert (HTP : TP (Var' 0)) by (unfold TP; intuition). apply (HM (Var' 0) HTP).
Qed.
Print Assumptions ModEx_WLEM.
End WLEM.
Section ModEx.
Class Canon_worlds : Type :=
{ prim : @Ensemble (BPropF) ;
NotDer : ~ (BIH_rules (prim, Bot)) ;
Closed : closed prim ;
Stable : stable prim ;
Prime : prime prim
}.
Definition Canon_rel (P0 P1 : Canon_worlds) : Prop :=
Included _ (@prim P0) (@prim P1).
Definition Canon_val (P : Canon_worlds) (q : nat) : Prop :=
In _ prim (# q).
Lemma C_R_refl u : Canon_rel u u.
Proof.
unfold Canon_rel. intro. auto.
Qed.
Lemma C_R_trans u v w: Canon_rel u v -> Canon_rel v w -> Canon_rel u w.
Proof.
intros. intro. intros. auto.
Qed.
Lemma C_val_persist : forall u v, Canon_rel u v -> forall p, Canon_val u p -> Canon_val v p.
Proof.
intros. apply H. auto.
Qed.
Instance CM : model :=
{|
nodes := Canon_worlds ;
reachable := Canon_rel ;
val := Canon_val ;
reach_refl := C_R_refl ;
reach_tran := C_R_trans ;
persist := C_val_persist ;
|}.
Axiom WLEM : forall P, ~ P \/ ~~ P.
Lemma WLEM_prime Γ :
stable Γ -> quasi_prime Γ -> prime Γ.
Proof.
intros H1 H2 A B H3. pose (WLEM (Γ A)).
destruct o. pose (WLEM (Γ B)). destruct o.
apply H2 in H3. exfalso. apply H3. intro. destruct H4 ; auto.
apply H1 in H0 ; auto. apply H1 in H ; auto.
Qed.
Lemma WLEM_Lindenbaum Γ Δ :
~ pair_derrec (Γ, Δ) ->
exists Γm, Included _ Γ Γm
/\ closed Γm
/\ stable Γm
/\ prime Γm
/\ ~ pair_derrec (Γm, Δ).
Proof.
intros.
exists (prime_theory Γ Δ).
repeat split.
- intro. apply prime_theory_extens.
- apply closeder_fst_Lind_pair ; auto.
- apply stable_Lind_pair ; auto.
- apply WLEM_prime. 2: apply quasi_prime_Lind_pair ; auto.
apply stable_Lind_pair ; auto.
- intro. apply Under_Lind_pair_init in H0 ; auto.
Qed.
Lemma WLEM_world Γ Δ :
~ pair_derrec (Γ, Δ) ->
exists w : Canon_worlds, Included _ Γ prim /\ Included _ Δ (Complement _ prim).
Proof.
intros (Γm & Γn & H1 & H2 & H3 & H4) % WLEM_Lindenbaum.
unshelve eexists.
- apply (Build_Canon_worlds Γm); intuition.
apply H4. exists [] ; repeat split ; auto. apply NoDup_nil.
intros ; auto. inversion H0.
- intuition. intros A HA0 HA1. apply H4. exists [A].
simpl ; repeat split ; auto. apply NoDup_cons. intro H8 ; inversion H8.
apply NoDup_nil. intros. destruct H ; try contradiction. subst ; auto.
unfold In in HA1. unfold prim in HA1.
apply MP with (ps:=[(Γm, A --> (Or A Bot));(Γm, A)]).
2: apply MPRule_I. intros. inversion H. subst. apply Ax.
apply AxRule_I. apply RA2_I. exists A. exists Bot ; auto.
inversion H0 ; subst. apply Id. apply IdRule_I ; auto. inversion H5.
Qed.
Lemma truth_lemma : forall A (cp : Canon_worlds),
(wforces CM cp A) <-> (In _ (@prim cp) A).
Proof.
induction A ; intro ; split ; intros ; simpl ; try simpl in H ; auto.
(* Bot *)
- inversion H.
- apply NotDer. apply Id. apply IdRule_I. auto.
(* Top *)
- apply Closed. apply wTop.
(* And A1 A2 *)
- destruct H. apply IHA1 in H. simpl in H. apply IHA2 in H0. simpl in H0.
apply Closed.
apply MP with (ps:=[(prim, A1 --> (And A1 A2));(prim, A1)]).
2: apply MPRule_I. intros. inversion H1. subst.
apply MP with (ps:=[(prim, (A1 --> A2) --> (A1 --> (And A1 A2)));(prim, (A1 --> A2))]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(prim, (A1 --> A1) --> (A1 --> A2) --> (A1 --> (And A1 A2)));(prim, (A1 --> A1))]).
2: apply MPRule_I. intros. inversion H3. subst. apply Ax. apply AxRule_I.
apply RA7_I. exists A1. exists A1. exists A2. auto. inversion H4.
subst. 2: inversion H5. apply wimp_Id_gen. inversion H3. subst. 2: inversion H4.
apply MP with (ps:=[(prim, A2 --> (A1 --> A2));(prim, A2)]).
2: apply MPRule_I. intros. inversion H4. subst. apply wThm_irrel.
inversion H5. subst. 2: inversion H6. apply Id. apply IdRule_I. assumption.
inversion H2. subst. apply Id. apply IdRule_I. assumption. inversion H3.
- split. apply IHA1. simpl. apply Closed ; auto.
apply MP with (ps:=[(prim, Imp (And A1 A2) A1);(prim, (And A1 A2))]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA5_I. exists A1. exists A2. auto. inversion H1. 2: inversion H2.
subst. apply Id. apply IdRule_I ; auto.
apply IHA2. simpl. apply Closed ; auto.
apply MP with (ps:=[(prim, Imp (And A1 A2) A2);(prim, (And A1 A2))]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA6_I. exists A1. exists A2. auto. inversion H1. 2: inversion H2.
subst. apply Id. apply IdRule_I ; auto.
(* Or A1 A2 *)
- destruct H.
apply IHA1 in H. simpl in H. apply Closed ; auto.
apply MP with (ps:=[(prim, Imp A1 (Or A1 A2));(prim, A1)]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA2_I. exists A1. exists A2. auto. inversion H1. 2: inversion H2.
subst. apply Id. apply IdRule_I ; auto.
apply IHA2 in H. simpl in H. apply Closed ; auto.
apply MP with (ps:=[(prim, Imp A2 (Or A1 A2));(prim, A2)]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA3_I. exists A1. exists A2. auto. inversion H1. 2: inversion H2.
subst. apply Id. apply IdRule_I ; auto.
- apply Prime in H ; auto. destruct H. left. apply IHA1 ; auto.
right. apply IHA2 ; auto.
(* Imp A1 A2 *)
- apply Stable. intros H0.
assert (pair_derrec (Union _ (prim) (Singleton _ A1), Singleton _ A2) -> False).
intro. apply gen_BIH_Deduction_Theorem in H1. apply H0.
{ apply Closed. destruct H1.
destruct H1. destruct H2. destruct x. simpl in H3. simpl in H2.
apply MP with (ps:=[(prim, Imp (Bot) (A1 --> A2));(prim, Bot)]). 2: apply MPRule_I.
intros. inversion H4. subst. apply wEFQ. inversion H5. 2: inversion H6. subst.
assumption. inversion H1. subst. pose (H2 b). assert (List.In b (b :: x)). apply in_eq.
apply s in H4. inversion H4. subst. destruct x. simpl in H3.
apply absorp_Or1 in H3. auto. pose (H2 b). assert (List.In b (A1 --> A2 :: b :: x)).
apply in_cons. apply in_eq. apply s0 in H5. inversion H5. subst. inversion H1.
subst. exfalso. apply H10. apply in_eq. }
pose (WLEM_world _ _ H1). destruct e as [w [Hw1 Hw2]].
assert (J2: Canon_rel cp w). unfold Canon_rel. simpl.
intro. intros. apply Hw1. apply Union_introl. auto. apply H in J2.
apply IHA2 in J2. assert (In BPropF (Complement _ prim) A2). apply Hw2.
apply In_singleton. apply H2 ; auto.
apply IHA1. simpl. apply Hw1. apply Union_intror. apply In_singleton.
- intros.
apply IHA1 in H1. simpl in H1. unfold Canon_rel in H0. simpl in H0.
apply H0 in H.
apply IHA2. simpl.
assert (pair_derrec (prim, Singleton _ A2)). exists [A2]. repeat split.
apply NoDup_cons ; auto ; apply NoDup_nil. intros. inversion H2. subst. apply In_singleton.
inversion H3. simpl.
apply MP with (ps:=[(prim, Imp A2 (Or A2 (Bot)));(prim, A2)]). 2: apply MPRule_I.
intros. inversion H2. subst. apply Ax. apply AxRule_I. apply RA2_I. exists A2. exists (Bot).
auto. inversion H3. subst.
apply MP with (ps:=[(prim, Imp A1 A2);(prim, A1)]). 2: apply MPRule_I.
intros. inversion H4. subst. apply Id. apply IdRule_I. auto.
inversion H5. 2: inversion H6. subst. apply Id. apply IdRule_I. auto.
inversion H4.
apply Closed. destruct H2. destruct H2.
destruct H3. destruct x. simpl in H4. apply MP with (ps:=[(prim, Imp (Bot) A2);(prim, Bot)]).
2: apply MPRule_I. intros. inversion H5. subst. apply wEFQ. inversion H6. 2: inversion H7.
subst. auto. inversion H2. subst. pose (H3 b). assert (List.In b (b :: x)).
apply in_eq. apply s in H5. inversion H5. subst. destruct x. simpl in H4.
apply absorp_Or1 in H4. auto. exfalso. pose (H3 b0). assert (List.In b0 (b :: b0 :: x)).
apply in_cons. apply in_eq. apply s0 in H6. inversion H6. subst. apply H7. apply in_eq.
(* Excl A1 A2 *)
- apply Stable. intros Hw. apply H. intros. apply IHA1 in H1.
assert (In (BPropF) (prim) (Or A2 (Excl A1 A2))). {
apply Closed.
apply MP with (ps:=[(prim, Imp A1 (Or A2 (Excl A1 A2)));(prim, A1)]). 2: apply MPRule_I.
intros. inversion H2. subst. apply Ax. apply AxRule_I. apply RA11_I. exists A1.
exists A2. auto. inversion H3. 2: inversion H4. subst. apply Id. apply IdRule_I. auto. }
apply Prime in H2. destruct H2 ; auto. apply IHA2 ; auto. contradict Hw. apply H0, H2.
- assert (pair_derrec ((Singleton _ A1), Union _ (Complement _ prim) (Singleton _ A2)) -> False).
intro. destruct H0. destruct H0. destruct H1. simpl in H2. simpl in H1.
pose (remove_disj x A2 (Singleton (BPropF) A1)).
assert (BIH_rules (Singleton (BPropF) A1, Or A2 (list_disj (remove eq_dec_form A2 x)))).
apply MP with (ps:=[(Singleton (BPropF) A1, list_disj x --> Or A2
(list_disj (remove eq_dec_form A2 x)));(Singleton (BPropF) A1, list_disj x)]).
2: apply MPRule_I. intros. inversion H3. subst. auto. inversion H4. subst.
auto. inversion H5. clear b. clear H2.
assert (Singleton (BPropF) A1 = Union _ (Empty_set _) (Singleton (BPropF) A1)).
apply Extensionality_Ensembles. split. intro. intros. inversion H2. subst.
apply Union_intror. apply In_singleton. intro. intros. inversion H2.
subst. inversion H4. inversion H4. subst. apply In_singleton. rewrite H2 in H3.
assert (J1: Union (BPropF) (Empty_set (BPropF)) (Singleton (BPropF) A1) =
Union (BPropF) (Empty_set (BPropF)) (Singleton (BPropF) A1)). auto.
assert (J2: Or A2 (list_disj (remove eq_dec_form A2 x)) = Or A2 (list_disj (remove eq_dec_form A2 x))). auto.
pose (BIH_Deduction_Theorem (Union (BPropF) (Empty_set (BPropF)) (Singleton (BPropF) A1),
Or A2 (list_disj (remove eq_dec_form A2 x))) H3 A1 (Or A2 (list_disj (remove eq_dec_form A2 x)))
(Empty_set _) J1 J2). apply wdual_residuation in b. clear J2. clear J1. clear H2.
assert (prim (list_disj (remove eq_dec_form A2 x))). apply Closed.
apply MP with (ps:=[(prim, Excl A1 A2 --> list_disj (remove eq_dec_form A2 x));(prim, Excl A1 A2)]).
2: apply MPRule_I. intros. inversion H2. subst.
pose (BIH_monot (Empty_set (BPropF), Excl A1 A2 --> list_disj (remove eq_dec_form A2 x))
b (prim)). apply b0. clear b0. simpl. intro. intros. inversion H4. inversion H4.
subst. 2: inversion H5. clear H2. apply Id. apply IdRule_I. auto.
apply list_disj_prime in H2. destruct H2. destruct H2.
apply in_remove in H2 ; destruct H2.
apply H1 in H2. inversion H2 ; subst. auto. inversion H6 ; subst ; auto.
2: apply Prime. apply NotDer.
intros Hv. apply WLEM_world in H0. destruct H0 as [w[Hw1 Hw2]].
enough (exists v, Canon_rel v cp /\ wforces CM v A1 /\ ~ wforces CM v A2) by firstorder.
exists w. split; try apply Hw1. unfold Canon_rel.
intro. intros. apply Stable. intros Hx. pose (Hw2 x). simpl in i0.
assert (In (BPropF) (Union (BPropF) (Complement _ (@prim cp)) (Singleton (BPropF) A2)) x).
apply Union_introl. auto.
apply i0 in H1. auto.
split. apply IHA1. simpl. apply Hw1. apply In_singleton.
intro. apply IHA2 in H0.
assert (In _ (Union BPropF (Complement BPropF (@prim cp)) (Singleton BPropF A2)) A2).
apply Union_intror ; apply In_singleton ; auto. pose (Hw2 A2 H1).
auto.
Qed.
Theorem WLEM_ModEx : ModEx.
Proof.
intros Γ D.
assert (~ pair_derrec (Γ, Singleton _ Bot)).
intro. apply D. destruct H. destruct H. destruct H0. simpl in H1.
destruct x. simpl in H1 ; auto. destruct x ; simpl in H1. apply absorp_Or1 in H1.
simpl in *. pose (H0 b). destruct s ; auto. exfalso.
pose (H0 b). destruct s. apply in_eq. simpl in *. pose (H0 b0).
destruct s ; auto. inversion H ; subst. apply H4 ; apply in_eq.
apply WLEM_world in H. destruct H. destruct H. exists CM. exists x.
intros. apply truth_lemma. auto.
Qed.
End ModEx.
Export ListNotations.
Require Import PeanoNat.
Require Import Lia.
Require Import Ensembles.
Require Import CPP_BiInt_GHC.
Require Import CPP_BiInt_logic.
Require Import CPP_BiInt_Kripke_sem_constr.
Require Import CPP_BiInt_soundness_constr.
Require Import CPP_BiInt_meta_interactions1.
Require Import CPP_BiInt_meta_interactions2.
Require Import CPP_BiInt_Lindenbaum_lem.
(* Assume enough variables in V *)
Variable i : nat -> nat.
Definition Var' n := Var (i n).
(* Model Existence implies WLEM *)
Section WLEM.
Variable P : Prop.
Let TP phi :=
phi = Or (Var' 0) (Neg (Var' 0)) \/ P /\ phi = Var' 0 \/ ~ P /\ phi = Neg (Var' 0).
Instance trivial_model :
model.
Proof.
unshelve econstructor.
- exact unit.
- exact (fun _ _ => True).
- exact (fun _ _ => P).
- split; auto.
- cbn. trivial.
- intuition.
Defined.
Lemma trivial_model_dec :
~ ~ model_dec trivial_model.
Proof.
intros H. assert (HP : ~ ~ (P \/ ~ P)) by tauto. apply HP. intros HP'.
apply H. intros [] A. induction A; cbn; try now intuition.
- destruct IHA1, IHA2.
+ left. now intros [].
+ right. firstorder.
+ left. now intros [].
+ left. now intros [].
- destruct IHA1, IHA2.
+ right. intro. apply H2. intros. destruct v ; auto.
+ left. intro. auto.
+ right. intro. apply H2. intros. destruct v ; auto.
+ right. intro. apply H2. intros. destruct v ; auto. exfalso ; auto.
Qed.
Lemma TP_consistent :
~ BIH_rules (TP, Bot).
Proof.
intros H. apply trivial_model_dec. intros HM.
assert (HP : ~ ~ (P \/ ~ P)) by tauto. apply HP. intros HP'.
apply (wSoundness_dec) in H. destruct (H trivial_model tt).
- apply HM.
- intros A [->|[[HA ->]|[HA ->]]]; cbn; intuition.
Qed.
Definition ModEx :=
forall T, ~ BIH_rules (T, Bot) -> exists M (w: @nodes M), forall A, In _ T A -> wforces M w A.
Theorem ModEx_WLEM :
ModEx -> ~ P \/ ~ ~ P.
Proof.
intros HME. destruct (@HME TP TP_consistent) as [M[w HM]].
destruct (HM (Or (Var' 0) (Neg (Var' 0)))) as [H|H].
- now left.
- right. intros HP. assert (HTP : TP (Neg (Var' 0))) by (unfold TP; intuition).
apply (HM (Neg (Var' 0)) HTP w); try apply reach_refl. apply H.
- left. intros HP. apply (H w); try apply reach_refl.
assert (HTP : TP (Var' 0)) by (unfold TP; intuition). apply (HM (Var' 0) HTP).
Qed.
Print Assumptions ModEx_WLEM.
End WLEM.
Section ModEx.
Class Canon_worlds : Type :=
{ prim : @Ensemble (BPropF) ;
NotDer : ~ (BIH_rules (prim, Bot)) ;
Closed : closed prim ;
Stable : stable prim ;
Prime : prime prim
}.
Definition Canon_rel (P0 P1 : Canon_worlds) : Prop :=
Included _ (@prim P0) (@prim P1).
Definition Canon_val (P : Canon_worlds) (q : nat) : Prop :=
In _ prim (# q).
Lemma C_R_refl u : Canon_rel u u.
Proof.
unfold Canon_rel. intro. auto.
Qed.
Lemma C_R_trans u v w: Canon_rel u v -> Canon_rel v w -> Canon_rel u w.
Proof.
intros. intro. intros. auto.
Qed.
Lemma C_val_persist : forall u v, Canon_rel u v -> forall p, Canon_val u p -> Canon_val v p.
Proof.
intros. apply H. auto.
Qed.
Instance CM : model :=
{|
nodes := Canon_worlds ;
reachable := Canon_rel ;
val := Canon_val ;
reach_refl := C_R_refl ;
reach_tran := C_R_trans ;
persist := C_val_persist ;
|}.
Axiom WLEM : forall P, ~ P \/ ~~ P.
Lemma WLEM_prime Γ :
stable Γ -> quasi_prime Γ -> prime Γ.
Proof.
intros H1 H2 A B H3. pose (WLEM (Γ A)).
destruct o. pose (WLEM (Γ B)). destruct o.
apply H2 in H3. exfalso. apply H3. intro. destruct H4 ; auto.
apply H1 in H0 ; auto. apply H1 in H ; auto.
Qed.
Lemma WLEM_Lindenbaum Γ Δ :
~ pair_derrec (Γ, Δ) ->
exists Γm, Included _ Γ Γm
/\ closed Γm
/\ stable Γm
/\ prime Γm
/\ ~ pair_derrec (Γm, Δ).
Proof.
intros.
exists (prime_theory Γ Δ).
repeat split.
- intro. apply prime_theory_extens.
- apply closeder_fst_Lind_pair ; auto.
- apply stable_Lind_pair ; auto.
- apply WLEM_prime. 2: apply quasi_prime_Lind_pair ; auto.
apply stable_Lind_pair ; auto.
- intro. apply Under_Lind_pair_init in H0 ; auto.
Qed.
Lemma WLEM_world Γ Δ :
~ pair_derrec (Γ, Δ) ->
exists w : Canon_worlds, Included _ Γ prim /\ Included _ Δ (Complement _ prim).
Proof.
intros (Γm & Γn & H1 & H2 & H3 & H4) % WLEM_Lindenbaum.
unshelve eexists.
- apply (Build_Canon_worlds Γm); intuition.
apply H4. exists [] ; repeat split ; auto. apply NoDup_nil.
intros ; auto. inversion H0.
- intuition. intros A HA0 HA1. apply H4. exists [A].
simpl ; repeat split ; auto. apply NoDup_cons. intro H8 ; inversion H8.
apply NoDup_nil. intros. destruct H ; try contradiction. subst ; auto.
unfold In in HA1. unfold prim in HA1.
apply MP with (ps:=[(Γm, A --> (Or A Bot));(Γm, A)]).
2: apply MPRule_I. intros. inversion H. subst. apply Ax.
apply AxRule_I. apply RA2_I. exists A. exists Bot ; auto.
inversion H0 ; subst. apply Id. apply IdRule_I ; auto. inversion H5.
Qed.
Lemma truth_lemma : forall A (cp : Canon_worlds),
(wforces CM cp A) <-> (In _ (@prim cp) A).
Proof.
induction A ; intro ; split ; intros ; simpl ; try simpl in H ; auto.
(* Bot *)
- inversion H.
- apply NotDer. apply Id. apply IdRule_I. auto.
(* Top *)
- apply Closed. apply wTop.
(* And A1 A2 *)
- destruct H. apply IHA1 in H. simpl in H. apply IHA2 in H0. simpl in H0.
apply Closed.
apply MP with (ps:=[(prim, A1 --> (And A1 A2));(prim, A1)]).
2: apply MPRule_I. intros. inversion H1. subst.
apply MP with (ps:=[(prim, (A1 --> A2) --> (A1 --> (And A1 A2)));(prim, (A1 --> A2))]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(prim, (A1 --> A1) --> (A1 --> A2) --> (A1 --> (And A1 A2)));(prim, (A1 --> A1))]).
2: apply MPRule_I. intros. inversion H3. subst. apply Ax. apply AxRule_I.
apply RA7_I. exists A1. exists A1. exists A2. auto. inversion H4.
subst. 2: inversion H5. apply wimp_Id_gen. inversion H3. subst. 2: inversion H4.
apply MP with (ps:=[(prim, A2 --> (A1 --> A2));(prim, A2)]).
2: apply MPRule_I. intros. inversion H4. subst. apply wThm_irrel.
inversion H5. subst. 2: inversion H6. apply Id. apply IdRule_I. assumption.
inversion H2. subst. apply Id. apply IdRule_I. assumption. inversion H3.
- split. apply IHA1. simpl. apply Closed ; auto.
apply MP with (ps:=[(prim, Imp (And A1 A2) A1);(prim, (And A1 A2))]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA5_I. exists A1. exists A2. auto. inversion H1. 2: inversion H2.
subst. apply Id. apply IdRule_I ; auto.
apply IHA2. simpl. apply Closed ; auto.
apply MP with (ps:=[(prim, Imp (And A1 A2) A2);(prim, (And A1 A2))]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA6_I. exists A1. exists A2. auto. inversion H1. 2: inversion H2.
subst. apply Id. apply IdRule_I ; auto.
(* Or A1 A2 *)
- destruct H.
apply IHA1 in H. simpl in H. apply Closed ; auto.
apply MP with (ps:=[(prim, Imp A1 (Or A1 A2));(prim, A1)]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA2_I. exists A1. exists A2. auto. inversion H1. 2: inversion H2.
subst. apply Id. apply IdRule_I ; auto.
apply IHA2 in H. simpl in H. apply Closed ; auto.
apply MP with (ps:=[(prim, Imp A2 (Or A1 A2));(prim, A2)]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA3_I. exists A1. exists A2. auto. inversion H1. 2: inversion H2.
subst. apply Id. apply IdRule_I ; auto.
- apply Prime in H ; auto. destruct H. left. apply IHA1 ; auto.
right. apply IHA2 ; auto.
(* Imp A1 A2 *)
- apply Stable. intros H0.
assert (pair_derrec (Union _ (prim) (Singleton _ A1), Singleton _ A2) -> False).
intro. apply gen_BIH_Deduction_Theorem in H1. apply H0.
{ apply Closed. destruct H1.
destruct H1. destruct H2. destruct x. simpl in H3. simpl in H2.
apply MP with (ps:=[(prim, Imp (Bot) (A1 --> A2));(prim, Bot)]). 2: apply MPRule_I.
intros. inversion H4. subst. apply wEFQ. inversion H5. 2: inversion H6. subst.
assumption. inversion H1. subst. pose (H2 b). assert (List.In b (b :: x)). apply in_eq.
apply s in H4. inversion H4. subst. destruct x. simpl in H3.
apply absorp_Or1 in H3. auto. pose (H2 b). assert (List.In b (A1 --> A2 :: b :: x)).
apply in_cons. apply in_eq. apply s0 in H5. inversion H5. subst. inversion H1.
subst. exfalso. apply H10. apply in_eq. }
pose (WLEM_world _ _ H1). destruct e as [w [Hw1 Hw2]].
assert (J2: Canon_rel cp w). unfold Canon_rel. simpl.
intro. intros. apply Hw1. apply Union_introl. auto. apply H in J2.
apply IHA2 in J2. assert (In BPropF (Complement _ prim) A2). apply Hw2.
apply In_singleton. apply H2 ; auto.
apply IHA1. simpl. apply Hw1. apply Union_intror. apply In_singleton.
- intros.
apply IHA1 in H1. simpl in H1. unfold Canon_rel in H0. simpl in H0.
apply H0 in H.
apply IHA2. simpl.
assert (pair_derrec (prim, Singleton _ A2)). exists [A2]. repeat split.
apply NoDup_cons ; auto ; apply NoDup_nil. intros. inversion H2. subst. apply In_singleton.
inversion H3. simpl.
apply MP with (ps:=[(prim, Imp A2 (Or A2 (Bot)));(prim, A2)]). 2: apply MPRule_I.
intros. inversion H2. subst. apply Ax. apply AxRule_I. apply RA2_I. exists A2. exists (Bot).
auto. inversion H3. subst.
apply MP with (ps:=[(prim, Imp A1 A2);(prim, A1)]). 2: apply MPRule_I.
intros. inversion H4. subst. apply Id. apply IdRule_I. auto.
inversion H5. 2: inversion H6. subst. apply Id. apply IdRule_I. auto.
inversion H4.
apply Closed. destruct H2. destruct H2.
destruct H3. destruct x. simpl in H4. apply MP with (ps:=[(prim, Imp (Bot) A2);(prim, Bot)]).
2: apply MPRule_I. intros. inversion H5. subst. apply wEFQ. inversion H6. 2: inversion H7.
subst. auto. inversion H2. subst. pose (H3 b). assert (List.In b (b :: x)).
apply in_eq. apply s in H5. inversion H5. subst. destruct x. simpl in H4.
apply absorp_Or1 in H4. auto. exfalso. pose (H3 b0). assert (List.In b0 (b :: b0 :: x)).
apply in_cons. apply in_eq. apply s0 in H6. inversion H6. subst. apply H7. apply in_eq.
(* Excl A1 A2 *)
- apply Stable. intros Hw. apply H. intros. apply IHA1 in H1.
assert (In (BPropF) (prim) (Or A2 (Excl A1 A2))). {
apply Closed.
apply MP with (ps:=[(prim, Imp A1 (Or A2 (Excl A1 A2)));(prim, A1)]). 2: apply MPRule_I.
intros. inversion H2. subst. apply Ax. apply AxRule_I. apply RA11_I. exists A1.
exists A2. auto. inversion H3. 2: inversion H4. subst. apply Id. apply IdRule_I. auto. }
apply Prime in H2. destruct H2 ; auto. apply IHA2 ; auto. contradict Hw. apply H0, H2.
- assert (pair_derrec ((Singleton _ A1), Union _ (Complement _ prim) (Singleton _ A2)) -> False).
intro. destruct H0. destruct H0. destruct H1. simpl in H2. simpl in H1.
pose (remove_disj x A2 (Singleton (BPropF) A1)).
assert (BIH_rules (Singleton (BPropF) A1, Or A2 (list_disj (remove eq_dec_form A2 x)))).
apply MP with (ps:=[(Singleton (BPropF) A1, list_disj x --> Or A2
(list_disj (remove eq_dec_form A2 x)));(Singleton (BPropF) A1, list_disj x)]).
2: apply MPRule_I. intros. inversion H3. subst. auto. inversion H4. subst.
auto. inversion H5. clear b. clear H2.
assert (Singleton (BPropF) A1 = Union _ (Empty_set _) (Singleton (BPropF) A1)).
apply Extensionality_Ensembles. split. intro. intros. inversion H2. subst.
apply Union_intror. apply In_singleton. intro. intros. inversion H2.
subst. inversion H4. inversion H4. subst. apply In_singleton. rewrite H2 in H3.
assert (J1: Union (BPropF) (Empty_set (BPropF)) (Singleton (BPropF) A1) =
Union (BPropF) (Empty_set (BPropF)) (Singleton (BPropF) A1)). auto.
assert (J2: Or A2 (list_disj (remove eq_dec_form A2 x)) = Or A2 (list_disj (remove eq_dec_form A2 x))). auto.
pose (BIH_Deduction_Theorem (Union (BPropF) (Empty_set (BPropF)) (Singleton (BPropF) A1),
Or A2 (list_disj (remove eq_dec_form A2 x))) H3 A1 (Or A2 (list_disj (remove eq_dec_form A2 x)))
(Empty_set _) J1 J2). apply wdual_residuation in b. clear J2. clear J1. clear H2.
assert (prim (list_disj (remove eq_dec_form A2 x))). apply Closed.
apply MP with (ps:=[(prim, Excl A1 A2 --> list_disj (remove eq_dec_form A2 x));(prim, Excl A1 A2)]).
2: apply MPRule_I. intros. inversion H2. subst.
pose (BIH_monot (Empty_set (BPropF), Excl A1 A2 --> list_disj (remove eq_dec_form A2 x))
b (prim)). apply b0. clear b0. simpl. intro. intros. inversion H4. inversion H4.
subst. 2: inversion H5. clear H2. apply Id. apply IdRule_I. auto.
apply list_disj_prime in H2. destruct H2. destruct H2.
apply in_remove in H2 ; destruct H2.
apply H1 in H2. inversion H2 ; subst. auto. inversion H6 ; subst ; auto.
2: apply Prime. apply NotDer.
intros Hv. apply WLEM_world in H0. destruct H0 as [w[Hw1 Hw2]].
enough (exists v, Canon_rel v cp /\ wforces CM v A1 /\ ~ wforces CM v A2) by firstorder.
exists w. split; try apply Hw1. unfold Canon_rel.
intro. intros. apply Stable. intros Hx. pose (Hw2 x). simpl in i0.
assert (In (BPropF) (Union (BPropF) (Complement _ (@prim cp)) (Singleton (BPropF) A2)) x).
apply Union_introl. auto.
apply i0 in H1. auto.
split. apply IHA1. simpl. apply Hw1. apply In_singleton.
intro. apply IHA2 in H0.
assert (In _ (Union BPropF (Complement BPropF (@prim cp)) (Singleton BPropF A2)) A2).
apply Union_intror ; apply In_singleton ; auto. pose (Hw2 A2 H1).
auto.
Qed.
Theorem WLEM_ModEx : ModEx.
Proof.
intros Γ D.
assert (~ pair_derrec (Γ, Singleton _ Bot)).
intro. apply D. destruct H. destruct H. destruct H0. simpl in H1.
destruct x. simpl in H1 ; auto. destruct x ; simpl in H1. apply absorp_Or1 in H1.
simpl in *. pose (H0 b). destruct s ; auto. exfalso.
pose (H0 b). destruct s. apply in_eq. simpl in *. pose (H0 b0).
destruct s ; auto. inversion H ; subst. apply H4 ; apply in_eq.
apply WLEM_world in H. destruct H. destruct H. exists CM. exists x.
intros. apply truth_lemma. auto.
Qed.
End ModEx.