Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Logic.Classical_Prop.
Require Import Coq.Logic.Classical_Pred_Type.
Require Import Logic.lib.Bijection.
Require Import Logic.lib.Countable.
Require Import Logic.GeneralLogic.Base.
Require Import Logic.GeneralLogic.KripkeModel.
Require Import Logic.GeneralLogic.ProofTheory.BasicSequentCalculus.
Require Import Logic.GeneralLogic.Semantics.Kripke.
Require Import Logic.GeneralLogic.Complete.ContextProperty.
Require Import Logic.GeneralLogic.Complete.ContextProperty_Kripke.
Require Import Logic.GeneralLogic.Complete.Lindenbaum.
Require Import Logic.MinimunLogic.Syntax.
Require Import Logic.MinimunLogic.ProofTheory.Minimun.
Require Import Logic.MinimunLogic.Semantics.Kripke.
Require Import Logic.MinimunLogic.Complete.ContextProperty_Kripke.
Require Import Logic.PropositionalLogic.Syntax.
Require Import Logic.PropositionalLogic.ProofTheory.Intuitionistic.
Require Import Logic.PropositionalLogic.ProofTheory.DeMorgan.
Require Import Logic.PropositionalLogic.ProofTheory.GodelDummett.
Require Import Logic.PropositionalLogic.ProofTheory.Classical.
Require Import Logic.PropositionalLogic.Semantics.Kripke.
Require Import Logic.PropositionalLogic.Complete.ContextProperty_Kripke.

Local Open Scope logic_base.
Local Open Scope syntax.
Local Open Scope kripke_model.
Import PropositionalLanguageNotation.
Import KripkeModelFamilyNotation.
Import KripkeModelNotation_Intuitionistic.

Section Canonical.

Context {L: Language}
        {minL: MinimunLanguage L}
        {pL: PropositionalLanguage L}
        {Gamma: ProofTheory L}
        {bSC: BasicSequentCalculus L Gamma}
        {minSC: MinimunSequentCalculus L Gamma}
        {ipSC: IntuitionisticPropositionalSequentCalculus L Gamma}
        {MD: Model}
        {kMD: KripkeModel MD}
        {M: Kmodel}
        {R: Relation (Kworlds M)}
        {SM: Semantics L MD}
        {kminSM: KripkeMinimunSemantics L MD M SM}
        {kpSM: KripkePropositionalSemantics L MD M SM}.

Context (cP: context -> Prop)
        (rel: bijection (Kworlds M) (sig cP)).

Hypothesis H_R: forall m n Phi Psi, rel m Phi -> rel n Psi -> (m <= n <-> Included _ (proj1_sig Phi) (proj1_sig Psi)).

Lemma classical_canonical_ident
      {cpSC: ClassicalPropositionalSequentCalculus L Gamma}
      (AL_DC: at_least derivable_closed cP)
      (AL_OW: at_least orp_witnessed cP)
      (AL_CONSI: at_least consistent cP):
  IdentityKripkeIntuitionisticModel (Kworlds M).
Proof.
(* Goal: @NoBranchKripkeIntuitionisticModel (@Kworlds MD kMD M) R *)
  constructor.
(* Goal: forall (m1 m2 n : @Kworlds MD kMD M) (_ : @Krelation (@Kworlds MD kMD M) R n m1) (_ : @Krelation (@Kworlds MD kMD M) R n m2), or (@Krelation (@Kworlds MD kMD M) R m1 m2) (@Krelation (@Kworlds MD kMD M) R m2 m1) *)
  intros.
(* Goal: @eq (@Kworlds MD kMD M) m n *)
  destruct (im_bij _ _ rel m) as [Phi ?].
(* Goal: @eq (@Kworlds MD kMD M) m n *)
  destruct (im_bij _ _ rel n) as [Psi ?].
(* Goal: @eq (@Kworlds MD kMD M) m n *)
  erewrite H_R in H by eauto.
(* Goal: @eq (@Kworlds MD kMD M) m n *)
  assert (Phi = Psi); [| subst; eapply (in_bij _ _ rel); eauto].
(* Goal: @eq (@sig (@context L) cP) Phi Psi *)
  clear rel H_R m n H0 H1.

(* Goal: @eq (@sig (@context L) cP) Phi Psi *)
  apply sig_context_ext.
(* Goal: forall x : @expr L, iff (@proj1_sig (@context L) cP Phi x) (@proj1_sig (@context L) cP Psi x) *)
  intros; split; [apply H; auto |].
(* Goal: forall (m1 m2 n : @Kworlds MD kMD M) (_ : @Krelation (@Kworlds MD kMD M) R n m1) (_ : @Krelation (@Kworlds MD kMD M) R n m2), or (@Krelation (@Kworlds MD kMD M) R m1 m2) (@Krelation (@Kworlds MD kMD M) R m2 m1) *)
  intros.
(* Goal: @proj1_sig (@context L) cP Phi x *)
  pose proof derivable_excluded_middle (proj1_sig Phi) x.
(* Goal: @proj1_sig (@context L) cP Phi x *)
  rewrite <- derivable_closed_element_derivable in H1 by (apply AL_DC, (proj2_sig Phi)).
(* Goal: @proj1_sig (@context L) cP Phi x *)
  apply AL_OW in H1; [| apply (proj2_sig Phi)].
(* Goal: @proj1_sig (@context L) cP Phi x *)
  destruct H1; auto.
(* Goal: @proj1_sig (@context L) cP Phi x *)
  exfalso.
(* Goal: False *)
  apply H in H1; unfold Ensembles.In in H1.
(* Goal: False *)
  rewrite derivable_closed_element_derivable in H0, H1 by (apply AL_DC, (proj2_sig Psi)).
(* Goal: False *)
  pose proof deduction_modus_ponens _ _ _ H0 H1.
(* Goal: False *)
  revert H2; change (~ proj1_sig Psi |-- FF).
(* Goal: not (@derivable L Gamma (@proj1_sig (@context L) cP Psi) (@falsep L pL)) *)
  rewrite <- consistent_spec.
(* Goal: @consistent L Gamma (@proj1_sig (@context L) cP Psi) *)
  apply AL_CONSI, (proj2_sig Psi).
Qed.

Lemma GodelDummett_canonical_no_branch
      {SC: NormalSequentCalculus L Gamma}
      {minAX: MinimunAxiomatization L Gamma}
      {ipGamma: IntuitionisticPropositionalLogic L Gamma}
      {gdpGamma: GodelDummettPropositionalLogic L Gamma}
      (AL_DC: at_least derivable_closed cP)
      (AL_OW: at_least orp_witnessed cP):
  NoBranchKripkeIntuitionisticModel (Kworlds M).
Proof.
(* Goal: @NoBranchKripkeIntuitionisticModel (@Kworlds MD kMD M) R *)
  constructor.
(* Goal: forall (m1 m2 n : @Kworlds MD kMD M) (_ : @Krelation (@Kworlds MD kMD M) R n m1) (_ : @Krelation (@Kworlds MD kMD M) R n m2), or (@Krelation (@Kworlds MD kMD M) R m1 m2) (@Krelation (@Kworlds MD kMD M) R m2 m1) *)
  intros.
(* Goal: or (@Krelation (@Kworlds MD kMD M) R m1 m2) (@Krelation (@Kworlds MD kMD M) R m2 m1) *)
  destruct (im_bij _ _ rel n) as [Phi ?].
(* Goal: or (@Krelation (@Kworlds MD kMD M) R m1 m2) (@Krelation (@Kworlds MD kMD M) R m2 m1) *)
  destruct (im_bij _ _ rel m1) as [Psi1 ?].
(* Goal: or (@Krelation (@Kworlds MD kMD M) R m1 m2) (@Krelation (@Kworlds MD kMD M) R m2 m1) *)
  destruct (im_bij _ _ rel m2) as [Psi2 ?].
(* Goal: or (@Krelation (@Kworlds MD kMD M) R m1 m2) (@Krelation (@Kworlds MD kMD M) R m2 m1) *)
  erewrite !H_R in H, H0 by eauto.
(* Goal: or (@Krelation (@Kworlds MD kMD M) R m1 m2) (@Krelation (@Kworlds MD kMD M) R m2 m1) *)
  do 2 erewrite H_R by eauto.
(* Goal: or (Included (@expr L) (@proj1_sig (@context L) cP Psi1) (@proj1_sig (@context L) cP Psi2)) (Included (@expr L) (@proj1_sig (@context L) cP Psi2) (@proj1_sig (@context L) cP Psi1)) *)
  clear rel H_R m1 m2 n H1 H2 H3.

(* Goal: or (Included (@expr L) (@proj1_sig (@context L) cP Psi1) (@proj1_sig (@context L) cP Psi2)) (Included (@expr L) (@proj1_sig (@context L) cP Psi2) (@proj1_sig (@context L) cP Psi1)) *)
  apply NNPP; intro.
(* Goal: False *)
  apply not_or_and in H1; destruct H1.
(* Goal: False *)
  apply not_all_ex_not in H1.
(* Goal: False *)
  apply not_all_ex_not in H2.
(* Goal: False *)
  destruct H1 as [x1 ?], H2 as [x2 ?].
(* Goal: False *)
  pose proof deduction_weaken0 (proj1_sig Phi) _ (impp_choice x1 x2).
(* Goal: False *)
  rewrite <- derivable_closed_element_derivable in H3 by (apply AL_DC, (proj2_sig Phi)).
(* Goal: False *)
  apply AL_OW in H3; [| apply (proj2_sig Phi)].
(* Goal: False *)
  destruct H3; pose proof H3; apply H in H3; apply H0 in H4.
  + rewrite derivable_closed_element_derivable in H3 by (apply AL_DC, (proj2_sig Psi1)).
(* Goal: False *)
    rewrite derivable_closed_element_derivable in H4 by (apply AL_DC, (proj2_sig Psi2)).
(* Goal: False *)
    pose proof (fun HH => deduction_modus_ponens _ _ _ HH H3).
(* Goal: False *)
    pose proof (fun HH => deduction_modus_ponens _ _ _ HH H4).
(* Goal: False *)
    rewrite <- !derivable_closed_element_derivable in H5 by (apply AL_DC, (proj2_sig Psi1)).
(* Goal: False *)
    rewrite <- !derivable_closed_element_derivable in H6 by (apply AL_DC, (proj2_sig Psi2)).
(* Goal: False *)
    clear - H1 H2 H5 H6.
(* Goal: False *)
    tauto.
  + rewrite derivable_closed_element_derivable in H3 by (apply AL_DC, (proj2_sig Psi1)).
(* Goal: False *)
    rewrite derivable_closed_element_derivable in H4 by (apply AL_DC, (proj2_sig Psi2)).
(* Goal: False *)
    pose proof (fun HH => deduction_modus_ponens _ _ _ HH H3).
(* Goal: False *)
    pose proof (fun HH => deduction_modus_ponens _ _ _ HH H4).
(* Goal: False *)
    rewrite <- !derivable_closed_element_derivable in H5 by (apply AL_DC, (proj2_sig Psi1)).
(* Goal: False *)
    rewrite <- !derivable_closed_element_derivable in H6 by (apply AL_DC, (proj2_sig Psi2)).
(* Goal: False *)
    clear - H1 H2 H5 H6.
(* Goal: False *)
    tauto.
Qed.

Lemma DeMorgan_canonical_branch_join
      {SC: NormalSequentCalculus L Gamma}
      {AX: NormalAxiomatization L Gamma}
      {minAX: MinimunAxiomatization L Gamma}
      {ipGamma: IntuitionisticPropositionalLogic L Gamma}
      {dmpGamma: DeMorganPropositionalLogic L Gamma}
      (AL_DC: at_least derivable_closed cP)
      (AL_OW: at_least orp_witnessed cP)
      (AL_CONSI: at_least consistent cP)
      (LIN_CD: forall x, Lindenbaum_constructable (cannot_derive x) cP):
  BranchJoinKripkeIntuitionisticModel (Kworlds M).
Proof.
(* Goal: @NoBranchKripkeIntuitionisticModel (@Kworlds MD kMD M) R *)
  constructor.
(* Goal: forall (m1 m2 n : @Kworlds MD kMD M) (_ : @Krelation (@Kworlds MD kMD M) R n m1) (_ : @Krelation (@Kworlds MD kMD M) R n m2), or (@Krelation (@Kworlds MD kMD M) R m1 m2) (@Krelation (@Kworlds MD kMD M) R m2 m1) *)
  intros.
(* Goal: or (@Krelation (@Kworlds MD kMD M) R m1 m2) (@Krelation (@Kworlds MD kMD M) R m2 m1) *)
  destruct (im_bij _ _ rel n) as [Phi ?].
(* Goal: or (@Krelation (@Kworlds MD kMD M) R m1 m2) (@Krelation (@Kworlds MD kMD M) R m2 m1) *)
  destruct (im_bij _ _ rel m1) as [Psi1 ?].
(* Goal: or (@Krelation (@Kworlds MD kMD M) R m1 m2) (@Krelation (@Kworlds MD kMD M) R m2 m1) *)
  destruct (im_bij _ _ rel m2) as [Psi2 ?].
(* Goal: or (@Krelation (@Kworlds MD kMD M) R m1 m2) (@Krelation (@Kworlds MD kMD M) R m2 m1) *)
  erewrite !H_R in H, H0 by eauto.
  assert (exists Psi: sig cP, Included _ (proj1_sig Psi1) (proj1_sig Psi) /\
                              Included _ (proj1_sig Psi2) (proj1_sig Psi)).
  Focus 2. {
    destruct H4 as [Psi [? ?]].
    destruct (su_bij _ _ rel Psi) as [m ?].
    exists m.
    erewrite !H_R by eauto; auto.
  } Unfocus.
(* Goal: or (Included (@expr L) (@proj1_sig (@context L) cP Psi1) (@proj1_sig (@context L) cP Psi2)) (Included (@expr L) (@proj1_sig (@context L) cP Psi2) (@proj1_sig (@context L) cP Psi1)) *)
  clear rel H_R m1 m2 n H1 H2 H3.

  assert (~ (Union _ (proj1_sig Psi1) (proj1_sig Psi2)) |-- FF).
  + intro.
    apply derivable_closed_union_derivable in H1; [| apply AL_DC, (proj2_sig Psi2)].
    destruct H1 as [x [? ?]].
    rewrite derivable_closed_element_derivable in H1 by (apply AL_DC, (proj2_sig Psi2)).
    pose proof deduction_weaken0 (proj1_sig Phi) _ (weak_excluded_middle x).
(* Goal: False *)
    rewrite <- derivable_closed_element_derivable in H3 by (apply AL_DC, (proj2_sig Phi)).
(* Goal: False *)
    apply AL_OW in H3; [| apply (proj2_sig Phi)].
    destruct H3.
    - apply H0 in H3; unfold Ensembles.In in H3.
      rewrite derivable_closed_element_derivable in H3 by (apply AL_DC, (proj2_sig Psi2)).
      pose proof deduction_modus_ponens _ _ _ H1 H3.
      revert H4; change (~ proj1_sig Psi2 |-- FF).
(* Goal: not (@derivable L Gamma (@proj1_sig (@context L) cP Psi) (@falsep L pL)) *)
      rewrite <- consistent_spec.
      apply AL_CONSI, (proj2_sig Psi2).
    - apply H in H3; unfold Ensembles.In in H3.
(* Goal: False *)
      rewrite derivable_closed_element_derivable in H3 by (apply AL_DC, (proj2_sig Psi1)).
      pose proof deduction_modus_ponens _ _ _ H2 H3.
      revert H4; change (~ proj1_sig Psi1 |-- FF).
(* Goal: not (@derivable L Gamma (@proj1_sig (@context L) cP Psi) (@falsep L pL)) *)
      rewrite <- consistent_spec.
      apply AL_CONSI, (proj2_sig Psi1).
  + apply LIN_CD in H1.
    destruct H1 as [Psi [? ?]]; exists Psi.
    split; intros ? ?; apply H1; [left | right]; auto.
Qed.

End Canonical.
