CPPsiteProjPackage.CPP_BiInt_completeness_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_meta_interactions1.
Require Import CPP_BiInt_meta_interactions2.
Require Import CPP_BiInt_Kripke_sem_constr.
Require Import CPP_BiInt_Lindenbaum_lem.
Require Import CPP_BiInt_soundness_constr.

Section LEM_completeness.

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 ) (@prim ).

Definition Canon_val (P : Canon_worlds) (q : ) : 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 : u v, Canon_rel u v 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 LEM : P, P P.

Lemma LEM_prime Γ :
  quasi_prime Γ prime Γ.
Proof.
  intros A B .
  apply in . destruct (LEM (Γ A)) ; auto.
  destruct (LEM (Γ B)) ; auto. exfalso. apply .
  intro. destruct ; auto.
Qed.


Lemma LEM_Lindenbaum Γ Δ :
   pair_derrec (Γ, Δ)
   Γm, Included _ Γ Γm
            closed Γ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 LEM_prime. apply quasi_prime_Lind_pair ; auto.
- intro. apply Under_Lind_pair_init in ; auto.
Qed.


Lemma LEM_world Γ Δ :
   pair_derrec (Γ, Δ)
   w : Canon_worlds, Included _ Γ prim Included _ Δ (Complement _ prim).
Proof.
  intros (Γm & Γn & & & ) % LEM_Lindenbaum.
  unshelve eexists.
  - apply (Build_Canon_worlds Γm); intuition ; simpl.
    apply . exists [] ; repeat split ; auto. apply NoDup_nil.
    intros ; auto. inversion . intros A .
    destruct (LEM (Γm A)) ; intuition.
  - intuition. intros A . apply . exists [A].
    simpl ; repeat split ; auto. apply NoDup_cons. intro ; inversion .
    apply NoDup_nil. intros. destruct H ; try contradiction. subst ; auto.
    unfold In in . unfold prim in .
    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 ; subst. apply Id. apply IdRule_I ; auto. inversion .
Qed.


Lemma truth_lemma : 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 in H. simpl in H. apply in . simpl in .
  apply Closed.
  apply MP with (ps:=[(prim, --> (And ));(prim, )]).
  2: apply MPRule_I. intros. inversion . subst.
  apply MP with (ps:=[(prim, ( --> ) --> ( --> (And )));(prim, ( --> ))]).
  2: apply MPRule_I. intros. inversion . subst.
  apply MP with (ps:=[(prim, ( --> ) --> ( --> ) --> ( --> (And )));(prim, ( --> ))]).
  2: apply MPRule_I. intros. inversion . subst. apply Ax. apply AxRule_I.
  apply RA7_I. exists . exists . exists . auto. inversion .
  subst. 2: inversion . apply wimp_Id_gen. inversion . subst. 2: inversion .
  apply MP with (ps:=[(prim, --> ( --> ));(prim, )]).
  2: apply MPRule_I. intros. inversion . subst. apply wThm_irrel.
  inversion . subst. 2: inversion . apply Id. apply IdRule_I. assumption.
  inversion . subst. apply Id. apply IdRule_I. assumption. inversion .
- split. apply . simpl. apply Closed ; auto.
  apply MP with (ps:=[(prim, Imp (And ) );(prim, (And ))]).
  2: apply MPRule_I. intros. inversion . subst. apply Ax. apply AxRule_I.
  apply RA5_I. exists . exists . auto. inversion . 2: inversion .
  subst. apply Id. apply IdRule_I ; auto.
  apply . simpl. apply Closed ; auto.
  apply MP with (ps:=[(prim, Imp (And ) );(prim, (And ))]).
  2: apply MPRule_I. intros. inversion . subst. apply Ax. apply AxRule_I.
  apply RA6_I. exists . exists . auto. inversion . 2: inversion .
  subst. apply Id. apply IdRule_I ; auto.
(* Or A1 A2 *)
- destruct H.
  apply in H. simpl in H. apply Closed ; auto.
  apply MP with (ps:=[(prim, Imp (Or ));(prim, )]).
  2: apply MPRule_I. intros. inversion . subst. apply Ax. apply AxRule_I.
  apply RA2_I. exists . exists . auto. inversion . 2: inversion .
  subst. apply Id. apply IdRule_I ; auto.
  apply in H. simpl in H. apply Closed ; auto.
  apply MP with (ps:=[(prim, Imp (Or ));(prim, )]).
  2: apply MPRule_I. intros. inversion . subst. apply Ax. apply AxRule_I.
  apply RA3_I. exists . exists . auto. inversion . 2: inversion .
  subst. apply Id. apply IdRule_I ; auto.
- apply Prime in H ; auto. destruct H. left. apply ; auto.
  right. apply ; auto.
(* Imp A1 A2 *)
- apply Stable. intros .
  assert (pair_derrec (Union _ (prim) (Singleton _ ), Singleton _ ) False).
  intro. apply gen_BIH_Deduction_Theorem in . apply .
  { apply Closed. destruct .
    destruct . destruct . destruct x. simpl in . simpl in .
    apply MP with (ps:=[(prim, Imp (Bot) ( --> ));(prim, Bot)]). 2: apply MPRule_I.
    intros. inversion . subst. apply wEFQ. inversion . 2: inversion . subst.
    assumption. inversion . subst. pose ( b). assert (List.In b (b :: x)). apply in_eq.
    apply s in . inversion . subst. destruct x. simpl in .
    apply absorp_Or1 in . auto. pose ( b). assert (List.In b ( --> :: b :: x)).
    apply in_cons. apply in_eq. apply in . inversion . subst. inversion .
    subst. exfalso. apply . apply in_eq. }
  pose (LEM_world _ _ ). destruct e as [w [ ]].
  assert (: Canon_rel cp w). unfold Canon_rel. simpl.
  intro. intros. apply . apply Union_introl. auto. apply H in .
  apply in . assert (In BPropF (Complement _ prim) ). apply .
  apply In_singleton. apply ; auto.
  apply . simpl. apply . apply Union_intror. apply In_singleton.
- intros.
  apply in . simpl in . unfold Canon_rel in . simpl in .
  apply in H.
  apply . simpl.
  assert (pair_derrec (prim, Singleton _ )). exists []. repeat split.
  apply NoDup_cons ; auto ; apply NoDup_nil. intros. inversion . subst. apply In_singleton.
  inversion . simpl.
  apply MP with (ps:=[(prim, Imp (Or (Bot)));(prim, )]). 2: apply MPRule_I.
  intros. inversion . subst. apply Ax. apply AxRule_I. apply RA2_I. exists . exists (Bot).
  auto. inversion . subst.
  apply MP with (ps:=[(prim, Imp );(prim, )]). 2: apply MPRule_I.
  intros. inversion . subst. apply Id. apply IdRule_I. auto.
  inversion . 2: inversion . subst. apply Id. apply IdRule_I. auto.
  inversion .
  apply Closed. destruct . destruct .
  destruct . destruct x. simpl in . apply MP with (ps:=[(prim, Imp (Bot) );(prim, Bot)]).
  2: apply MPRule_I. intros. inversion . subst. apply wEFQ. inversion . 2: inversion .
  subst. auto. inversion . subst. pose ( b). assert (List.In b (b :: x)).
  apply in_eq. apply s in . inversion . subst. destruct x. simpl in .
  apply absorp_Or1 in . auto. exfalso. pose ( ). assert (List.In (b :: :: x)).
  apply in_cons. apply in_eq. apply in . inversion . subst. apply . apply in_eq.
(* Excl A1 A2 *)
- apply Stable. intros Hw. apply H. intros. apply in .
  assert (In (BPropF) (prim) (Or (Excl ))). {
  apply Closed.
  apply MP with (ps:=[(prim, Imp (Or (Excl )));(prim, )]). 2: apply MPRule_I.
  intros. inversion . subst. apply Ax. apply AxRule_I. apply RA11_I. exists .
  exists . auto. inversion . 2: inversion . subst. apply Id. apply IdRule_I. auto. }
  apply Prime in . destruct ; auto. apply ; auto. contradict Hw. apply , .
- assert (pair_derrec ((Singleton _ ), Union _ (Complement _ prim) (Singleton _ )) False).
  intro. destruct . destruct . destruct . simpl in . simpl in .
  pose (remove_disj x (Singleton (BPropF) )).
  assert (BIH_rules (Singleton (BPropF) , Or (list_disj (remove eq_dec_form x)))).
  apply MP with (ps:=[(Singleton (BPropF) , list_disj x --> Or
   (list_disj (remove eq_dec_form x)));(Singleton (BPropF) , list_disj x)]).
  2: apply MPRule_I. intros. inversion . subst. auto. inversion . subst.
  auto. inversion . clear b. clear .
  assert (Singleton (BPropF) = Union _ (Empty_set _) (Singleton (BPropF) )).
  apply Extensionality_Ensembles. split. intro. intros. inversion . subst.
  apply Union_intror. apply In_singleton. intro. intros. inversion .
  subst. inversion . inversion . subst. apply In_singleton. rewrite in .
  assert (: Union (BPropF) (Empty_set (BPropF)) (Singleton (BPropF) ) =
  Union (BPropF) (Empty_set (BPropF)) (Singleton (BPropF) )). auto.
  assert (: Or (list_disj (remove eq_dec_form x)) = Or (list_disj (remove eq_dec_form x))). auto.
  pose (BIH_Deduction_Theorem (Union (BPropF) (Empty_set (BPropF)) (Singleton (BPropF) ),
  Or (list_disj (remove eq_dec_form x))) (Or (list_disj (remove eq_dec_form x)))
  (Empty_set _) ). apply wdual_residuation in b. clear . clear . clear .
  assert (prim (list_disj (remove eq_dec_form x))). apply Closed.
  apply MP with (ps:=[(prim, Excl --> list_disj (remove eq_dec_form x));(prim, Excl )]).
  2: apply MPRule_I. intros. inversion . subst.
  pose (BIH_monot (Empty_set (BPropF), Excl --> list_disj (remove eq_dec_form x))
  b (prim)). apply . clear . simpl. intro. intros. inversion . inversion .
  subst. 2: inversion . clear . apply Id. apply IdRule_I. auto.
  apply list_disj_prime in . destruct . destruct .
  apply in_remove in ; destruct .
  apply in . inversion ; subst. auto. inversion ; subst ; auto.
  2: apply Prime. apply NotDer.
  intros Hv. apply LEM_world in . destruct as [w[ ]].
  enough ( v, Canon_rel v cp wforces CM v wforces CM v ) by firstorder.
  exists w. split; try apply . unfold Canon_rel.
  intro. intros. apply Stable. intros Hx. pose ( x). simpl in i.
  assert (In (BPropF) (Union (BPropF) (Complement _ (@prim cp)) (Singleton (BPropF) )) x).
  apply Union_introl. auto.
  apply i in . auto.
  split. apply . simpl. apply . apply In_singleton.
  intro. apply in .
  assert (In _ (Union BPropF (Complement BPropF (@prim cp)) (Singleton BPropF )) ).
  apply Union_intror ; apply In_singleton ; auto. pose ( ).
  auto.
Qed.


Theorem wQuasiCompleteness : s,
    (BIH_rules s False) ((loc_conseq (fst s) (snd s)) False).
Proof.
intros s WD H.
assert ((pair_derrec (fst s, Singleton _ (snd s))) False). intro. apply WD.
destruct . destruct . destruct . simpl in *. destruct x. simpl in . destruct s.
simpl in *.
apply MP with (ps:=[(e, Imp Bot b);(e, Bot)]). 2: apply MPRule_I.
intros. inversion . subst. Search Bot. apply wEFQ. inversion . subst.
2: inversion . auto.
simpl in . destruct x. simpl in . destruct s. simpl in *.
assert (=b). pose ( b). destruct s ; auto. subst. apply absorp_Or1 ; auto. simpl in *.
exfalso. pose ( b). pose ( ). destruct ; destruct ; auto. rewrite NoDup_cons_iff in .
destruct . apply ; apply in_eq.
apply LEM_world in . destruct as (w & & ).
assert (( A : BPropF, In (BPropF) (fst s) A wforces CM w A)). intros. apply truth_lemma. auto.
apply H in . apply truth_lemma in . simpl in .
pose ( (snd s)). destruct i. apply In_singleton. auto.
Qed.


Theorem wCompleteness : Γ A,
    (loc_conseq Γ A) BIH_rules (Γ, A).
Proof.
intros Γ A LC. pose (wQuasiCompleteness (Γ, A)).
destruct (LEM (BIH_rules (Γ, A))) ; auto. exfalso.
apply f ; assumption.
Qed.


End LEM_completeness.

Print Assumptions wCompleteness.

(* Reformulation of BIH_finite *)

Definition fromlist {X} (L : list X) : Ensemble X :=
  fun x List.In x L.

Lemma BIH_finite' T A :
  BIH_rules (T, A) L : list (BPropF), ( B, List.In B L T B) BIH_rules (fromlist L, A).
Proof.
  intros [T'[[[L HL]]]] % BIH_finite. cbn in *. exists L. split.
  - intros B HB. apply , HL, HB.
  - eapply (BIH_monot (T', A)); trivial. cbn. intros B HB. apply HL, HB.
Qed.


(* Consistency *)

#[export] Instance point_model :
  model.
Proof.
  unshelve econstructor.
  - exact unit.
  - exact (fun _ _ True).
  - exact (fun _ _ True).
  - split; auto.
  - cbn. trivial.
  - intuition.
Defined.


Lemma point_model_dec :
  model_dec point_model.
Proof.
  intros [] A. induction A; cbn; try now intuition.
  - destruct , .
    + left. now intros [].
    + right. firstorder.
    + left. now intros [].
    + left. now intros [].
    - destruct , .
      + right. intro. apply . intros. destruct v ; auto.
      + left. intro. auto.
      + right. intro. apply . intros. destruct v ; auto.
      + right. intro. apply . intros. destruct v ; auto. exfalso ; auto.
Qed.


Lemma consistency :
   BIH_rules (fromlist [], Bot).
Proof.
  intros H % wSoundness_dec. cbn in H. destruct (H point_model tt).
  - apply point_model_dec.
  - intros A [].
Qed.


(* Completeness implies LEM *)

Section Completeness_LEM.

  Variable P : Prop.

  Let TLEM (phi : BPropF) :=
    P P.

  Definition Completeness :=
     Γ A, loc_conseq Γ A BIH_rules (Γ, A).

  Theorem Completeness_LEM :
    Completeness P P.
  Proof.
    intros HC. assert (H : loc_conseq TLEM (Bot)).
    - intros M w H. cbn.
      assert (HP : (P P)) by intuition. apply HP. intros HP'.
      apply (H (Bot)). apply HP'.
    - apply HC in H. apply BIH_finite' in H as [L[ ]]. destruct L as [|A L].
      + now apply consistency in .
      + apply ( A). now left.
  Qed.


End Completeness_LEM.

Print Assumptions Completeness_LEM.