CPPsiteProjPackage.CPP_BiInt_soundness_constr
Require Import List.
Export ListNotations.
Require Import PeanoNat.
Require Import Lia.
Require Import Ensembles.
Require Import CPP_BiInt_GHC.
Require Import CPP_BiInt_Kripke_sem_constr.
Require Import CPP_BiInt_meta_interactions1.
Require Import CPP_BiInt_meta_interactions2.
Definition wSoundness := forall s, BIH_rules s -> loc_conseq (fst s) (snd s).
Section Soundness_LEM.
Axiom LEM : forall P, P \/ ~ P.
(* LEM implies soundness *)
Lemma wforces_dec : forall A M w,
(wforces M w A) \/ ((wforces M w A) -> False).
Proof.
intros. apply LEM.
Qed.
(* To get rid of the decidability of forcing we could change the semantics of the
disjunction, by adding a double negation. *)
Lemma Ax_valid : forall A, BIAxioms A ->
(forall M w, wforces M w A).
Proof.
intros A Ax. inversion Ax ; simpl ; intros ; auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. apply H2 ; auto. apply H0 ; auto. apply (@reach_tran M) with (v:=v0) ; auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto ; destruct H0 ; auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. destruct H4 ; auto. apply H0 ; auto.
apply (@reach_tran M) with (v:=v0) ; auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto. destruct H0. auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto. destruct H0. auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. split.
apply H0 ; auto. apply (@reach_tran M) with (v:=v0) ; auto. apply H2 ; auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto.
apply H0 with (v:=v0) ; auto. destruct H2. assumption. apply (@reach_refl M).
destruct H2. assumption.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto.
apply H0 ; auto. apply (@reach_tran M) with (v:=v0) ; auto. split. apply Persistence with (w:=v0) ; auto.
auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto.
apply H2 with (v:=v1) ; auto. apply H0 ; auto. apply (@reach_tran M) with (v:=v1) ; auto. apply (@reach_tran M) with (v:=v0) ; auto.
apply (@reach_refl M).
- destruct H ; destruct H ; subst ; simpl ; intros ; auto. pose (@wforces_dec x0 M v).
destruct o. auto. right. intro. apply H1, H2; trivial. apply reach_refl.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto. intro. apply H0. intros.
apply H1 with v0; trivial. apply reach_refl.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. intro. apply H0. intros.
pose (@wforces_dec x1 M v0). destruct o. auto. exfalso.
assert (~ ~ ((exists v, reachable v v0 /\ wforces M v x /\ ~ wforces M v x0) \/ ~ (exists v, reachable v v0 /\ wforces M v x /\ ~ wforces M v x0))) by tauto.
apply H5. intros [(v1 & H6 & H7 & H8)|H6].
+ apply H1 in H7 as [H7|H7]; try tauto.
* apply H4. now apply Persistence with v1.
* now apply reach_tran with v0.
+ apply H3. intros. pose (@wforces_dec x0 M v1).
destruct o. auto. contradict H6. now exists v1.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto.
pose (@H0 v0 H1). pose (@wforces_dec x0 M v0).
destruct o ; auto.
exfalso. apply f. intro. apply H3, H4; trivial. apply reach_refl.
- destruct H ; subst. simpl. intros. auto.
- destruct H ; subst ; simpl. intros. inversion H0.
Qed.
(* Actually stability of the model forcing is sufficient for soundness *)
Lemma Ax_valid_stable : forall A, BIAxioms A ->
(forall M, (forall w B, ~ ~ wforces M w B -> wforces M w B) -> forall w, wforces M w A).
Proof.
intros A Ax M stab. inversion Ax ; simpl ; intros ; auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. apply H2 ; auto. apply H0 ; auto. apply (@reach_tran M) with (v:=v0) ; auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto ; destruct H0 ; auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. destruct H4 ; auto. apply H0 ; auto.
apply (@reach_tran M) with (v:=v0) ; auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto. destruct H0. auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto. destruct H0. auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. split.
apply H0 ; auto. apply (@reach_tran M) with (v:=v0) ; auto. apply H2 ; auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto.
apply H0 with (v:=v0) ; auto. destruct H2. assumption. apply (@reach_refl M).
destruct H2. assumption.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto.
apply H0 ; auto. apply (@reach_tran M) with (v:=v0) ; auto. split. apply Persistence with (w:=v0) ; auto.
auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto.
apply H2 with (v:=v1) ; auto. apply H0 ; auto. apply (@reach_tran M) with (v:=v1) ; auto. apply (@reach_tran M) with (v:=v0) ; auto.
apply (@reach_refl M).
- destruct H ; destruct H ; subst ; intros v H H0. apply stab. intros H'.
assert (o' : ~ ~ (wforces M v x0 \/ ~ wforces M v x0)) by tauto. apply o'. intros o.
apply H'. cbn. destruct o. auto.
right. intro. apply H1, H2; trivial. apply reach_refl.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto. intro. apply H0. intros.
apply H1 with v0; trivial. apply reach_refl.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. intro. apply H0. intros.
apply stab. intros H4.
apply H3. intros. destruct (H1 v1); trivial.
+ now apply reach_tran with v0.
+ exfalso. apply H4. now apply Persistence with v1.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto.
pose (@H0 v0 H1). apply stab. intros H3.
apply f. intro. apply H3, H4; trivial. apply reach_refl.
- destruct H ; subst. simpl. intros. auto.
- destruct H ; subst ; simpl. intros. inversion H0.
Qed.
Theorem LEM_wSoundness : wSoundness.
Proof.
intros s D. induction D.
(* Id *)
- inversion H ; subst. intro. intros. apply H1. assumption.
(* Ax *)
- inversion H. subst. intro. intros. apply Ax_valid ; assumption.
(* MP *)
- inversion H1. subst. simpl. assert (J1: loc_conseq Γ (A --> B)).
apply H0 with (prem:=(Γ, A --> B)). apply in_eq. assert (J2: loc_conseq Γ A).
apply H0 with (prem:=(Γ, A)). apply in_cons. apply in_eq.
intro. intros. unfold loc_conseq in J1.
pose (J1 M w H2). pose (J2 M w H2). subst.
apply w0. apply (@reach_refl M). assumption.
(* wDN *)
- inversion H1. subst. simpl. assert (J1: loc_conseq (Empty_set BPropF) A).
apply H0 with (prem:=(Empty_set BPropF, A)) ; apply in_eq.
intro. intros. simpl in J1. simpl. intros. apply H4. intros.
assert (J2: (forall A : BPropF, In _ (Empty_set _) A -> wforces M v0 A)).
intros. inversion H7. pose (J1 M v0 J2). assumption.
Qed.
Print Assumptions LEM_wSoundness.
End Soundness_LEM.
Section Constr_Sound.
(* Constructivised Soundness *)
Definition model_dec M :=
forall w A, wforces M w A \/ (wforces M w A -> False).
Lemma Ax_valid_dec M :
model_dec M -> forall w A, BIAxioms A -> wforces M w A.
Proof.
intros dec w A Ax. inversion Ax ; simpl ; intros ; auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. apply H2 ; auto. apply H0 ; auto. apply (@reach_tran M) with (v:=v0) ; auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto ; destruct H0 ; auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. destruct H4 ; auto. apply H0 ; auto.
apply (@reach_tran M) with (v:=v0) ; auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto. destruct H0. auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto. destruct H0. auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. split.
apply H0 ; auto. apply (@reach_tran M) with (v:=v0) ; auto. apply H2 ; auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto.
apply H0 with (v:=v0) ; auto. destruct H2. assumption. apply (@reach_refl M).
destruct H2. assumption.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto.
apply H0 ; auto. apply (@reach_tran M) with (v:=v0) ; auto. split. apply Persistence with (w:=v0) ; auto.
auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto.
apply H2 with (v:=v1) ; auto. apply H0 ; auto. apply (@reach_tran M) with (v:=v1) ; auto. apply (@reach_tran M) with (v:=v0) ; auto.
apply (@reach_refl M).
- destruct H ; destruct H ; subst ; simpl ; intros ; auto. pose (@dec v x0).
destruct o. auto. right. intro. apply H1, H2; trivial. apply reach_refl.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto. intro. apply H0. intros.
apply H1 with v0; trivial. apply reach_refl.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. intro. apply H0. intros.
pose (@dec v0 x1). destruct o. auto. exfalso.
assert (~ ~ ((exists v, reachable v v0 /\ wforces M v x /\ ~ wforces M v x0) \/ ~ (exists v, reachable v v0 /\ wforces M v x /\ ~ wforces M v x0))) by tauto.
apply H5. intros [(v1 & H6 & H7 & H8)|H6].
+ apply H1 in H7 as [H7|H7]; try tauto.
* apply H4. now apply Persistence with v1.
* now apply reach_tran with v0.
+ apply H3. intros. pose (@wforces_dec x0 M v1).
destruct o. auto. contradict H6. now exists v1.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto.
pose (@H0 v0 H1). pose (@dec v0 x0).
destruct o ; auto.
exfalso. apply f. intro. apply H3, H4; trivial. apply reach_refl.
- destruct H ; subst. simpl. intros. auto.
- destruct H ; subst ; simpl. intros. inversion H0.
Qed.
Definition loc_conseq_dec Γ A :=
forall M w, model_dec M -> (forall B, (In _ Γ B) -> wforces M w B) -> (wforces M w A).
Theorem wSoundness_dec s :
BIH_rules s -> loc_conseq_dec (fst s) (snd s).
Proof.
intros D. induction D; intros M w HM.
(* Id *)
- inversion H. subst. simpl. intro. intros. apply H1. assumption.
(* Ax *)
- inversion H. subst. simpl. intro. intros. apply Ax_valid_dec ; intuition.
(* MP *)
- inversion H1. subst. simpl. assert (J1: loc_conseq_dec Γ (A --> B)).
apply H0 with (prem:=(Γ, A --> B)). apply in_eq. assert (J2: loc_conseq_dec Γ A).
apply H0 with (prem:=(Γ, A)). apply in_cons. apply in_eq.
intro. intros. unfold loc_conseq in J1.
pose (J1 M w HM H2). pose (J2 M w HM H2).
apply w0. apply (@reach_refl M). assumption.
(* DNw *)
- inversion H1. subst. simpl. assert (J1: loc_conseq_dec (Empty_set BPropF) A).
apply H0 with (prem:=(Empty_set BPropF, A)) ; apply in_eq.
intro. intros. simpl in J1. simpl. intros. apply H4. intros.
assert (J2: (forall A : BPropF, In _ (Empty_set _) A -> wforces M v0 A)).
intros. inversion H7.
pose (J1 M v0 HM J2). assumption.
Qed.
Print Assumptions wSoundness_dec.
End Constr_Sound.
Section BIH_model_Sound.
Lemma Ax_valid_BIH_model M w :
(forall B C, wforces M w (RA11 B C)) -> (forall B C D, wforces M w (RA13 B C D)) -> (forall B C, wforces M w (RA14 B C))
-> forall A, BIAxioms A -> wforces M w A.
Proof.
intros H11 H13 H14 A Ax. inversion Ax ; auto ; simpl ; intros ; auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. apply H2 ; auto. apply H0 ; auto. apply (@reach_tran M) with (v:=v0) ; auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto ; destruct H0 ; auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. destruct H4 ; auto. apply H0 ; auto.
apply (@reach_tran M) with (v:=v0) ; auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto. destruct H0. auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto. destruct H0. auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. split.
apply H0 ; auto. apply (@reach_tran M) with (v:=v0) ; auto. apply H2 ; auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto.
apply (H0 v0) with (v:=v0) ; auto. destruct H2. assumption. apply (@reach_refl M).
destruct H2. assumption.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto.
apply H0 ; auto. apply (@reach_tran M) with (v:=v0) ; auto. split. apply Persistence with (w:=v0) ; auto.
auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto.
apply H2 with (v:=v1) ; auto. apply H0 ; auto. apply (@reach_tran M) with (v:=v1) ; auto. apply (@reach_tran M) with (v:=v0) ; auto.
apply (@reach_refl M).
- destruct H ; destruct H ; subst ; simpl. now apply H11.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto ; intros. intro.
apply H0. intros. apply H1 with (v:=v0) ; auto. apply (@reach_refl M).
- destruct H ; destruct H ; destruct H ; subst ; simpl ; now apply H13.
- destruct H ; destruct H ; subst ; simpl. apply H14.
- destruct H ; subst. simpl. intros. auto.
- destruct H ; subst ; simpl. intros. inversion H0.
Qed.
Definition loc_conseq_BIH_model Γ A :=
forall M w, (forall B C w, wforces M w (RA11 B C)) -> (forall B C D w, wforces M w (RA13 B C D)) ->
(forall B C w, wforces M w (RA14 B C))
-> (forall B, (In _ Γ B) -> wforces M w B) -> (wforces M w A).
Theorem Soundness_BIH_model s :
BIH_rules s -> loc_conseq_BIH_model (fst s) (snd s).
Proof.
intros D. induction D; intros M w H11 H13 H14.
(* Id *)
- inversion H. subst. simpl. intro. apply H1. assumption.
(* Ax *)
- inversion H. subst. simpl. intro. intros. apply Ax_valid_BIH_model; intuition.
(* MP *)
- inversion H1. subst. simpl. assert (J1: loc_conseq_BIH_model Γ (A --> B)).
apply H0 with (prem:=(Γ, A --> B)). apply in_eq. assert (J2: loc_conseq_BIH_model Γ A).
apply H0 with (prem:=(Γ, A)). apply in_cons. apply in_eq.
intro. unfold loc_conseq in J1.
pose (J1 M w H11 H13 H14 H2). pose (J2 M w H11 H13 H14 H2).
apply w0 ; auto. apply (@reach_refl M).
(* DNw *)
- inversion H1. subst. simpl. assert (J1: loc_conseq_BIH_model (Empty_set (BPropF)) A).
apply H0 with (prem:=(Empty_set (BPropF), A)) ; apply in_eq.
intro. intros. apply H4. intros.
assert (J2: (forall A : BPropF, In _ (Empty_set _) A -> wforces M v0 A)).
intros. inversion H7.
pose (J1 M v0 H11 H13 H14 J2). auto.
Qed.
Print Assumptions Soundness_BIH_model.
End BIH_model_Sound.
Section LEM.
Variable P : Prop.
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.
Theorem wSoundness_LEM :
wSoundness -> ~ P \/ P.
Proof.
intro SD. unfold wSoundness in SD. pose (SD ((Empty_set _) , (Or (# 0) (wNeg (# 0))))).
assert (BIH_rules (Empty_set BPropF, Or # 0 (wNeg # 0))). apply wBiLEM.
pose (l H trivial_model tt).
assert (forall A : BPropF, In BPropF (Empty_set BPropF) A -> wforces trivial_model tt A).
intros. inversion H0. apply w in H0. simpl in H0. destruct H0 ; auto.
Qed.
Print Assumptions wSoundness_LEM.
End LEM.
Export ListNotations.
Require Import PeanoNat.
Require Import Lia.
Require Import Ensembles.
Require Import CPP_BiInt_GHC.
Require Import CPP_BiInt_Kripke_sem_constr.
Require Import CPP_BiInt_meta_interactions1.
Require Import CPP_BiInt_meta_interactions2.
Definition wSoundness := forall s, BIH_rules s -> loc_conseq (fst s) (snd s).
Section Soundness_LEM.
Axiom LEM : forall P, P \/ ~ P.
(* LEM implies soundness *)
Lemma wforces_dec : forall A M w,
(wforces M w A) \/ ((wforces M w A) -> False).
Proof.
intros. apply LEM.
Qed.
(* To get rid of the decidability of forcing we could change the semantics of the
disjunction, by adding a double negation. *)
Lemma Ax_valid : forall A, BIAxioms A ->
(forall M w, wforces M w A).
Proof.
intros A Ax. inversion Ax ; simpl ; intros ; auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. apply H2 ; auto. apply H0 ; auto. apply (@reach_tran M) with (v:=v0) ; auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto ; destruct H0 ; auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. destruct H4 ; auto. apply H0 ; auto.
apply (@reach_tran M) with (v:=v0) ; auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto. destruct H0. auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto. destruct H0. auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. split.
apply H0 ; auto. apply (@reach_tran M) with (v:=v0) ; auto. apply H2 ; auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto.
apply H0 with (v:=v0) ; auto. destruct H2. assumption. apply (@reach_refl M).
destruct H2. assumption.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto.
apply H0 ; auto. apply (@reach_tran M) with (v:=v0) ; auto. split. apply Persistence with (w:=v0) ; auto.
auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto.
apply H2 with (v:=v1) ; auto. apply H0 ; auto. apply (@reach_tran M) with (v:=v1) ; auto. apply (@reach_tran M) with (v:=v0) ; auto.
apply (@reach_refl M).
- destruct H ; destruct H ; subst ; simpl ; intros ; auto. pose (@wforces_dec x0 M v).
destruct o. auto. right. intro. apply H1, H2; trivial. apply reach_refl.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto. intro. apply H0. intros.
apply H1 with v0; trivial. apply reach_refl.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. intro. apply H0. intros.
pose (@wforces_dec x1 M v0). destruct o. auto. exfalso.
assert (~ ~ ((exists v, reachable v v0 /\ wforces M v x /\ ~ wforces M v x0) \/ ~ (exists v, reachable v v0 /\ wforces M v x /\ ~ wforces M v x0))) by tauto.
apply H5. intros [(v1 & H6 & H7 & H8)|H6].
+ apply H1 in H7 as [H7|H7]; try tauto.
* apply H4. now apply Persistence with v1.
* now apply reach_tran with v0.
+ apply H3. intros. pose (@wforces_dec x0 M v1).
destruct o. auto. contradict H6. now exists v1.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto.
pose (@H0 v0 H1). pose (@wforces_dec x0 M v0).
destruct o ; auto.
exfalso. apply f. intro. apply H3, H4; trivial. apply reach_refl.
- destruct H ; subst. simpl. intros. auto.
- destruct H ; subst ; simpl. intros. inversion H0.
Qed.
(* Actually stability of the model forcing is sufficient for soundness *)
Lemma Ax_valid_stable : forall A, BIAxioms A ->
(forall M, (forall w B, ~ ~ wforces M w B -> wforces M w B) -> forall w, wforces M w A).
Proof.
intros A Ax M stab. inversion Ax ; simpl ; intros ; auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. apply H2 ; auto. apply H0 ; auto. apply (@reach_tran M) with (v:=v0) ; auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto ; destruct H0 ; auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. destruct H4 ; auto. apply H0 ; auto.
apply (@reach_tran M) with (v:=v0) ; auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto. destruct H0. auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto. destruct H0. auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. split.
apply H0 ; auto. apply (@reach_tran M) with (v:=v0) ; auto. apply H2 ; auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto.
apply H0 with (v:=v0) ; auto. destruct H2. assumption. apply (@reach_refl M).
destruct H2. assumption.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto.
apply H0 ; auto. apply (@reach_tran M) with (v:=v0) ; auto. split. apply Persistence with (w:=v0) ; auto.
auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto.
apply H2 with (v:=v1) ; auto. apply H0 ; auto. apply (@reach_tran M) with (v:=v1) ; auto. apply (@reach_tran M) with (v:=v0) ; auto.
apply (@reach_refl M).
- destruct H ; destruct H ; subst ; intros v H H0. apply stab. intros H'.
assert (o' : ~ ~ (wforces M v x0 \/ ~ wforces M v x0)) by tauto. apply o'. intros o.
apply H'. cbn. destruct o. auto.
right. intro. apply H1, H2; trivial. apply reach_refl.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto. intro. apply H0. intros.
apply H1 with v0; trivial. apply reach_refl.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. intro. apply H0. intros.
apply stab. intros H4.
apply H3. intros. destruct (H1 v1); trivial.
+ now apply reach_tran with v0.
+ exfalso. apply H4. now apply Persistence with v1.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto.
pose (@H0 v0 H1). apply stab. intros H3.
apply f. intro. apply H3, H4; trivial. apply reach_refl.
- destruct H ; subst. simpl. intros. auto.
- destruct H ; subst ; simpl. intros. inversion H0.
Qed.
Theorem LEM_wSoundness : wSoundness.
Proof.
intros s D. induction D.
(* Id *)
- inversion H ; subst. intro. intros. apply H1. assumption.
(* Ax *)
- inversion H. subst. intro. intros. apply Ax_valid ; assumption.
(* MP *)
- inversion H1. subst. simpl. assert (J1: loc_conseq Γ (A --> B)).
apply H0 with (prem:=(Γ, A --> B)). apply in_eq. assert (J2: loc_conseq Γ A).
apply H0 with (prem:=(Γ, A)). apply in_cons. apply in_eq.
intro. intros. unfold loc_conseq in J1.
pose (J1 M w H2). pose (J2 M w H2). subst.
apply w0. apply (@reach_refl M). assumption.
(* wDN *)
- inversion H1. subst. simpl. assert (J1: loc_conseq (Empty_set BPropF) A).
apply H0 with (prem:=(Empty_set BPropF, A)) ; apply in_eq.
intro. intros. simpl in J1. simpl. intros. apply H4. intros.
assert (J2: (forall A : BPropF, In _ (Empty_set _) A -> wforces M v0 A)).
intros. inversion H7. pose (J1 M v0 J2). assumption.
Qed.
Print Assumptions LEM_wSoundness.
End Soundness_LEM.
Section Constr_Sound.
(* Constructivised Soundness *)
Definition model_dec M :=
forall w A, wforces M w A \/ (wforces M w A -> False).
Lemma Ax_valid_dec M :
model_dec M -> forall w A, BIAxioms A -> wforces M w A.
Proof.
intros dec w A Ax. inversion Ax ; simpl ; intros ; auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. apply H2 ; auto. apply H0 ; auto. apply (@reach_tran M) with (v:=v0) ; auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto ; destruct H0 ; auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. destruct H4 ; auto. apply H0 ; auto.
apply (@reach_tran M) with (v:=v0) ; auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto. destruct H0. auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto. destruct H0. auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. split.
apply H0 ; auto. apply (@reach_tran M) with (v:=v0) ; auto. apply H2 ; auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto.
apply H0 with (v:=v0) ; auto. destruct H2. assumption. apply (@reach_refl M).
destruct H2. assumption.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto.
apply H0 ; auto. apply (@reach_tran M) with (v:=v0) ; auto. split. apply Persistence with (w:=v0) ; auto.
auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto.
apply H2 with (v:=v1) ; auto. apply H0 ; auto. apply (@reach_tran M) with (v:=v1) ; auto. apply (@reach_tran M) with (v:=v0) ; auto.
apply (@reach_refl M).
- destruct H ; destruct H ; subst ; simpl ; intros ; auto. pose (@dec v x0).
destruct o. auto. right. intro. apply H1, H2; trivial. apply reach_refl.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto. intro. apply H0. intros.
apply H1 with v0; trivial. apply reach_refl.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. intro. apply H0. intros.
pose (@dec v0 x1). destruct o. auto. exfalso.
assert (~ ~ ((exists v, reachable v v0 /\ wforces M v x /\ ~ wforces M v x0) \/ ~ (exists v, reachable v v0 /\ wforces M v x /\ ~ wforces M v x0))) by tauto.
apply H5. intros [(v1 & H6 & H7 & H8)|H6].
+ apply H1 in H7 as [H7|H7]; try tauto.
* apply H4. now apply Persistence with v1.
* now apply reach_tran with v0.
+ apply H3. intros. pose (@wforces_dec x0 M v1).
destruct o. auto. contradict H6. now exists v1.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto.
pose (@H0 v0 H1). pose (@dec v0 x0).
destruct o ; auto.
exfalso. apply f. intro. apply H3, H4; trivial. apply reach_refl.
- destruct H ; subst. simpl. intros. auto.
- destruct H ; subst ; simpl. intros. inversion H0.
Qed.
Definition loc_conseq_dec Γ A :=
forall M w, model_dec M -> (forall B, (In _ Γ B) -> wforces M w B) -> (wforces M w A).
Theorem wSoundness_dec s :
BIH_rules s -> loc_conseq_dec (fst s) (snd s).
Proof.
intros D. induction D; intros M w HM.
(* Id *)
- inversion H. subst. simpl. intro. intros. apply H1. assumption.
(* Ax *)
- inversion H. subst. simpl. intro. intros. apply Ax_valid_dec ; intuition.
(* MP *)
- inversion H1. subst. simpl. assert (J1: loc_conseq_dec Γ (A --> B)).
apply H0 with (prem:=(Γ, A --> B)). apply in_eq. assert (J2: loc_conseq_dec Γ A).
apply H0 with (prem:=(Γ, A)). apply in_cons. apply in_eq.
intro. intros. unfold loc_conseq in J1.
pose (J1 M w HM H2). pose (J2 M w HM H2).
apply w0. apply (@reach_refl M). assumption.
(* DNw *)
- inversion H1. subst. simpl. assert (J1: loc_conseq_dec (Empty_set BPropF) A).
apply H0 with (prem:=(Empty_set BPropF, A)) ; apply in_eq.
intro. intros. simpl in J1. simpl. intros. apply H4. intros.
assert (J2: (forall A : BPropF, In _ (Empty_set _) A -> wforces M v0 A)).
intros. inversion H7.
pose (J1 M v0 HM J2). assumption.
Qed.
Print Assumptions wSoundness_dec.
End Constr_Sound.
Section BIH_model_Sound.
Lemma Ax_valid_BIH_model M w :
(forall B C, wforces M w (RA11 B C)) -> (forall B C D, wforces M w (RA13 B C D)) -> (forall B C, wforces M w (RA14 B C))
-> forall A, BIAxioms A -> wforces M w A.
Proof.
intros H11 H13 H14 A Ax. inversion Ax ; auto ; simpl ; intros ; auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. apply H2 ; auto. apply H0 ; auto. apply (@reach_tran M) with (v:=v0) ; auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto ; destruct H0 ; auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. destruct H4 ; auto. apply H0 ; auto.
apply (@reach_tran M) with (v:=v0) ; auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto. destruct H0. auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto. destruct H0. auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto. split.
apply H0 ; auto. apply (@reach_tran M) with (v:=v0) ; auto. apply H2 ; auto.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto.
apply (H0 v0) with (v:=v0) ; auto. destruct H2. assumption. apply (@reach_refl M).
destruct H2. assumption.
- destruct H ; destruct H ; destruct H ; subst ; simpl ; intros ; auto.
apply H0 ; auto. apply (@reach_tran M) with (v:=v0) ; auto. split. apply Persistence with (w:=v0) ; auto.
auto.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto.
apply H2 with (v:=v1) ; auto. apply H0 ; auto. apply (@reach_tran M) with (v:=v1) ; auto. apply (@reach_tran M) with (v:=v0) ; auto.
apply (@reach_refl M).
- destruct H ; destruct H ; subst ; simpl. now apply H11.
- destruct H ; destruct H ; subst ; simpl ; intros ; auto ; intros. intro.
apply H0. intros. apply H1 with (v:=v0) ; auto. apply (@reach_refl M).
- destruct H ; destruct H ; destruct H ; subst ; simpl ; now apply H13.
- destruct H ; destruct H ; subst ; simpl. apply H14.
- destruct H ; subst. simpl. intros. auto.
- destruct H ; subst ; simpl. intros. inversion H0.
Qed.
Definition loc_conseq_BIH_model Γ A :=
forall M w, (forall B C w, wforces M w (RA11 B C)) -> (forall B C D w, wforces M w (RA13 B C D)) ->
(forall B C w, wforces M w (RA14 B C))
-> (forall B, (In _ Γ B) -> wforces M w B) -> (wforces M w A).
Theorem Soundness_BIH_model s :
BIH_rules s -> loc_conseq_BIH_model (fst s) (snd s).
Proof.
intros D. induction D; intros M w H11 H13 H14.
(* Id *)
- inversion H. subst. simpl. intro. apply H1. assumption.
(* Ax *)
- inversion H. subst. simpl. intro. intros. apply Ax_valid_BIH_model; intuition.
(* MP *)
- inversion H1. subst. simpl. assert (J1: loc_conseq_BIH_model Γ (A --> B)).
apply H0 with (prem:=(Γ, A --> B)). apply in_eq. assert (J2: loc_conseq_BIH_model Γ A).
apply H0 with (prem:=(Γ, A)). apply in_cons. apply in_eq.
intro. unfold loc_conseq in J1.
pose (J1 M w H11 H13 H14 H2). pose (J2 M w H11 H13 H14 H2).
apply w0 ; auto. apply (@reach_refl M).
(* DNw *)
- inversion H1. subst. simpl. assert (J1: loc_conseq_BIH_model (Empty_set (BPropF)) A).
apply H0 with (prem:=(Empty_set (BPropF), A)) ; apply in_eq.
intro. intros. apply H4. intros.
assert (J2: (forall A : BPropF, In _ (Empty_set _) A -> wforces M v0 A)).
intros. inversion H7.
pose (J1 M v0 H11 H13 H14 J2). auto.
Qed.
Print Assumptions Soundness_BIH_model.
End BIH_model_Sound.
Section LEM.
Variable P : Prop.
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.
Theorem wSoundness_LEM :
wSoundness -> ~ P \/ P.
Proof.
intro SD. unfold wSoundness in SD. pose (SD ((Empty_set _) , (Or (# 0) (wNeg (# 0))))).
assert (BIH_rules (Empty_set BPropF, Or # 0 (wNeg # 0))). apply wBiLEM.
pose (l H trivial_model tt).
assert (forall A : BPropF, In BPropF (Empty_set BPropF) A -> wforces trivial_model tt A).
intros. inversion H0. apply w in H0. simpl in H0. destruct H0 ; auto.
Qed.
Print Assumptions wSoundness_LEM.
End LEM.