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.ProofTheory.BasicSequentCalculus.
Require Import Logic.GeneralLogic.KripkeModel.
Require Import Logic.GeneralLogic.Complete.ContextProperty.
Require Import Logic.GeneralLogic.Complete.ContextProperty_Kripke.
Require Import Logic.GeneralLogic.Complete.ContextProperty_Trivial.
Require Import Logic.MinimunLogic.Syntax.
Require Import Logic.MinimunLogic.ProofTheory.Minimun.
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.Complete.ContextProperty_Kripke.

Local Open Scope logic_base.
Local Open Scope syntax.
Import PropositionalLanguageNotation.

Section ContextProperties.

Context {L: Language}
        {minL: MinimunLanguage L}
        {pL: PropositionalLanguage L}
        {Gamma: ProofTheory L}
        {bSC: BasicSequentCalculus L Gamma}
        {minSC: MinimunSequentCalculus L Gamma}
        {ipSC: IntuitionisticPropositionalSequentCalculus L Gamma}
        {cpSC: ClassicalPropositionalSequentCalculus L Gamma}.

Lemma classical_derivable_spec: forall (Phi: context) (x: expr),
  Phi |-- x <-> ~ consistent (Union _ Phi (Singleton _ (~~ x))).
Proof.
(* Goal: forall (Phi : @context L) (_ : @maximal L (@consistent L Gamma) Phi) (x : @expr L), iff (Phi (@negp L minL pL x)) (not (Phi x)) *)
  intros.
(* Goal: iff (@derivable L Gamma Phi x) (not (@consistent L Gamma (Union (@expr L) Phi (Singleton (@expr L) (@negp L minL pL x))))) *)
  unfold consistent.
(* Goal: iff (@derivable L Gamma Phi x) (not (@ex (@expr L) (fun x0 : @expr L => not (@derivable L Gamma (Union (@expr L) Phi (Singleton (@expr L) (@negp L minL pL x))) x0)))) *)
  AddAxiomatization Gamma.
(* Goal: iff (@derivable L Gamma Phi x) (not (@ex (@expr L) (fun x0 : @expr L => not (@derivable L Gamma (Union (@expr L) Phi (Singleton (@expr L) (@negp L minL pL x))) x0)))) *)
  fold (@consistent L Gamma (Phi;; ~~ x)).
(* Goal: iff (@derivable L Gamma Phi x) (not (@consistent L Gamma (Union (@expr L) Phi (Singleton (@expr L) (@negp L minL pL x))))) *)
  rewrite <- (double_negp x) at 1.
(* Goal: iff (@derivable L Gamma Phi (@negp L minL pL (@negp L minL pL x))) (not (@consistent L Gamma (Union (@expr L) Phi (Singleton (@expr L) (@negp L minL pL x))))) *)
  unfold negp at 1.
(* Goal: iff (@derivable L Gamma Phi (@impp L minL (@negp L minL pL x) (@falsep L pL))) (not (@consistent L Gamma (Union (@expr L) Phi (Singleton (@expr L) (@negp L minL pL x))))) *)
  rewrite <- deduction_theorem.
(* Goal: iff (@derivable L Gamma (Union (@expr L) Phi (Singleton (@expr L) (@negp L minL pL x))) (@falsep L pL)) (not (@consistent L Gamma (Union (@expr L) Phi (Singleton (@expr L) (@negp L minL pL x))))) *)
  rewrite consistent_spec.
(* Goal: @derivable L Gamma Phi (@impp L minL x (@falsep L pL)) *)
  tauto.
Qed.

Lemma MCS_nonelement_inconsistent: forall (Phi: context),
  maximal consistent Phi ->
  (forall x: expr, ~ Phi x <-> Phi |-- x --> FF).
Proof.
(* Goal: forall (Phi : @context L) (_ : @maximal L (@consistent L Gamma) Phi) (x : @expr L), iff (Phi (@negp L minL pL x)) (not (Phi x)) *)
  intros.
(* Goal: forall (Phi : @context L) (_ : @maximal L (@consistent L Gamma) Phi) (x : @expr L), iff (Phi (@negp L minL pL x)) (not (Phi x)) *)
  split; intros.
  + destruct H.
(* Goal: @derivable L Gamma Phi (@impp L minL x (@falsep L pL)) *)
    specialize (H1 (Union _ Phi (Singleton _ x))).
(* Goal: @derivable L Gamma Phi (@impp L minL x (@falsep L pL)) *)
    rewrite consistent_spec in H1.
(* Goal: @derivable L Gamma Phi (@impp L minL x (@falsep L pL)) *)
    rewrite deduction_theorem in H1.
(* Goal: @derivable L Gamma Phi (@impp L minL x (@falsep L pL)) *)
    assert (Included expr Phi (Union expr Phi (Singleton expr x))) by (intros ? ?; left; auto).
(* Goal: @derivable L Gamma Phi (@impp L minL x (@falsep L pL)) *)
    assert (~ Included expr (Union expr Phi (Singleton expr x)) Phi) by (intros HH; specialize (HH x); apply H0, HH; right; constructor).
(* Goal: @derivable L Gamma Phi (@impp L minL x (@falsep L pL)) *)
    tauto.
  + intro.
(* Goal: False *)
    pose proof derivable_assum Phi x H1.
(* Goal: False *)
    pose proof deduction_modus_ponens _ _ _ H2 H0.
(* Goal: False *)
    destruct H as [? _].
(* Goal: False *)
    rewrite consistent_spec in H; auto.
Qed.

Lemma maximal_consistent_orp_witnessed: forall (Phi: context),
  maximal consistent Phi -> orp_witnessed Phi.
Proof.
(* Goal: forall (Phi : @context L) (_ : @maximal L (@consistent L Gamma) Phi) (x : @expr L), iff (Phi (@negp L minL pL x)) (not (Phi x)) *)
  intros.
(* Goal: forall (Phi : @context L) (_ : @maximal L (@consistent L Gamma) Phi) (x : @expr L), iff (Phi (@negp L minL pL x)) (not (Phi x)) *)
  hnf; intros.
(* Goal: or (Phi x) (Phi y) *)
  rewrite MCS_element_derivable in H0 by auto.
(* Goal: not (Phi x) *)
  apply NNPP; intro.
(* Goal: False *)
  apply not_or_and in H1.
(* Goal: False *)
  destruct H1.
(* Goal: False *)
  rewrite MCS_nonelement_inconsistent in H1, H2 by eauto.
(* Goal: False *)
  destruct H as [? _]; rewrite consistent_spec in H.
(* Goal: False *)
  apply H.
(* Goal: @derivable L Gamma Phi (@falsep L pL) *)
  eapply deduction_modus_ponens; [exact H0 |].
(* Goal: @derivable L Gamma Phi (@impp L minL (@orp L pL x y) (@falsep L pL)) *)
  apply deduction_orp_elim'; auto.
Qed.

Lemma MCS_andp_iff: forall (Phi: context),
  maximal consistent Phi ->
  (forall x y: expr, Phi (x && y) <-> (Phi x /\ Phi y)).
Proof.
(* Goal: forall (Phi : @context L) (_ : @maximal L (@consistent L Gamma) Phi) (x : @expr L), iff (Phi (@negp L minL pL x)) (not (Phi x)) *)
  intros.
(* Goal: iff (Phi (@andp L pL x y)) (and (Phi x) (Phi y)) *)
  apply maximal_consistent_derivable_closed in H.
(* Goal: iff (Phi (@andp L pL x y)) (and (Phi x) (Phi y)) *)
  apply DCS_andp_iff; auto.
Qed.

Lemma MCS_orp_iff: forall (Phi: context),
  maximal consistent Phi ->
  (forall x y: expr, Phi (x || y) <-> (Phi x \/ Phi y)).
Proof.
(* Goal: forall (Phi : @context L) (_ : @maximal L (@consistent L Gamma) Phi) (x : @expr L), iff (Phi (@negp L minL pL x)) (not (Phi x)) *)
  intros.
(* Goal: iff (Phi (@orp L pL x y)) (or (Phi x) (Phi y)) *)
  apply DCS_orp_iff; auto.
  + apply maximal_consistent_derivable_closed; auto.
  + apply maximal_consistent_orp_witnessed; auto.
Qed.

Lemma MCS_impp_iff: forall (Phi: context),
  maximal consistent Phi ->
  (forall x y: expr, Phi (x --> y) <-> (Phi x -> Phi y)).
Proof.
(* Goal: forall (Phi : @context L) (_ : @maximal L (@consistent L Gamma) Phi) (x : @expr L), iff (Phi (@negp L minL pL x)) (not (Phi x)) *)
  intros.
(* Goal: forall (Phi : @context L) (_ : @maximal L (@consistent L Gamma) Phi) (x : @expr L), iff (Phi (@negp L minL pL x)) (not (Phi x)) *)
  split; intros.
  + rewrite MCS_element_derivable in H0, H1 |- * by auto.
(* Goal: @derivable L Gamma Phi y *)
    apply (deduction_modus_ponens _ x y); auto.
  + pose proof derivable_excluded_middle Phi y.
(* Goal: Phi (@impp L minL x y) *)
    rewrite <- MCS_element_derivable in H1 by auto.
(* Goal: Phi (@impp L minL x y) *)
    rewrite MCS_orp_iff in H1 by auto.
(* Goal: Phi (@impp L minL x y) *)
    pose proof derivable_excluded_middle Phi x.
(* Goal: Phi (@impp L minL x y) *)
    rewrite <- MCS_element_derivable in H2 by auto.
(* Goal: Phi (@impp L minL x y) *)
    rewrite MCS_orp_iff in H2 by auto.
(* Goal: Phi (@impp L minL x y) *)
    destruct H1; [| destruct H2].
    - rewrite MCS_element_derivable in H1 |- * by auto.
(* Goal: @derivable L Gamma Phi (@impp L minL x y) *)
      apply deduction_left_impp_intros; auto.
    - exfalso.
(* Goal: False *)
      apply H0 in H2.
(* Goal: False *)
      rewrite MCS_element_derivable in H1, H2 by auto.
(* Goal: False *)
      pose proof deduction_modus_ponens _ _ _ H2 H1.
(* Goal: False *)
      destruct H as [? _].
(* Goal: False *)
      rewrite consistent_spec in H; auto.
    - rewrite MCS_element_derivable in H2 |- * by auto.
(* Goal: @derivable L Gamma Phi (@impp L minL x y) *)
      unfold negp in H2.
      rewrite <- deduction_theorem in H2 |- *.
(* Goal: @derivable L Gamma (Union (@expr L) Phi (Singleton (@expr L) x)) y *)
      pose proof deduction_falsep_elim _ y H2.
(* Goal: not (Phi (@falsep L pL)) *)
      auto.
Qed.

Lemma MCS_negp_iff: forall (Phi: context),
  maximal consistent Phi ->
  (forall x: expr, Phi (~~ x) <-> ~ Phi x).
Proof.
(* Goal: forall (Phi : @context L) (_ : @maximal L (@consistent L Gamma) Phi) (x : @expr L), iff (Phi (@negp L minL pL x)) (not (Phi x)) *)
  intros.
(* Goal: iff (Phi (@negp L minL pL x)) (not (Phi x)) *)
  unfold negp.
(* Goal: not (Phi (@falsep L pL)) *)
  rewrite MCS_impp_iff by auto.
(* Goal: iff (forall _ : Phi x, Phi (@falsep L pL)) (not (Phi x)) *)
  assert (~ Phi FF); [| tauto].
(* Goal: not (Phi (@falsep L pL)) *)
  pose proof proj1 H.
  rewrite consistent_spec, <- MCS_element_derivable in H0 by auto.
(* Goal: not (Phi (@falsep L pL)) *)
  auto.
Qed.

Lemma DDCS_MCS: forall (Phi: context),
  derivable_closed Phi ->
  orp_witnessed Phi ->
  consistent Phi ->
  maximal consistent Phi.
Proof.
(* Goal: forall (Phi : @context L) (_ : @maximal L (@consistent L Gamma) Phi) (x : @expr L), iff (Phi (@negp L minL pL x)) (not (Phi x)) *)
  intros.
(* Goal: not (Phi (@falsep L pL)) *)
  split; auto.
(* Goal: forall (Phi : @context L) (_ : @maximal L (@consistent L Gamma) Phi) (x : @expr L), iff (Phi (@negp L minL pL x)) (not (Phi x)) *)
  intros.
(* Goal: forall (Phi : @context L) (_ : @maximal L (@consistent L Gamma) Phi) (x : @expr L), iff (Phi (@negp L minL pL x)) (not (Phi x)) *)
  unfold Included, Ensembles.In; intros.
(* Goal: Phi (@impp L minL x y) *)
  pose proof derivable_excluded_middle Phi x.
  apply H in H5.
  apply H0 in H5.
(* Goal: not (Phi (@falsep L pL)) *)
  destruct H5; auto.
(* Goal: Phi (@impp L minL x y) *)
  exfalso.
  apply H3 in H5; unfold Ensembles.In in H5.
  rewrite consistent_spec in H2.
  apply H2; clear H2.
  apply derivable_assum in H4.
  apply derivable_assum in H5.
  eapply deduction_modus_ponens.
  - apply H4.
  - apply H5.
Qed.

End ContextProperties.
