Require Import Coq.Logic.Classical_Prop.
Require Import Logic.lib.Coqlib.
Require Import Logic.GeneralLogic.Base.
Require Import Logic.GeneralLogic.Complete.ContextProperty.
Require Import Logic.GeneralLogic.ProofTheory.BasicSequentCalculus.
Require Import Logic.GeneralLogic.Complete.ContextProperty_Kripke.

Local Open Scope logic_base.

Section ContextProperty.

Context {L: Language}
        {Gamma: ProofTheory L}
        {bSC: BasicSequentCalculus L Gamma}.

Lemma maximal_consistent_spec :
  forall Phi, maximal consistent Phi <-> consistent Phi /\ forall x, consistent (Union _ Phi (Singleton _ x)) -> Phi x.
Proof.
(* Goal: forall (Phi : @context L) (_ : @maximal L (@consistent L Gamma) Phi) (x : @expr L), iff (Phi x) (@derivable L Gamma Phi x) *)
  intros.
(* Goal: iff (@maximal L (@consistent L Gamma) Phi) (and (@consistent L Gamma Phi) (forall (x : @expr L) (_ : @consistent L Gamma (Union (@expr L) Phi (Singleton (@expr L) x))), Phi x)) *)
  split; intros [? ?]; split; auto.
(* Goal: forall (Phi : @context L) (_ : @maximal L (@consistent L Gamma) Phi) (x : @expr L), iff (Phi x) (@derivable L Gamma Phi x) *)
  + intros.
(* Goal: Phi x *)
    specialize (H0 _ H1).
(* Goal: Phi x *)
    specialize (H0 (fun x H => Union_introl _ _ _ _ H)).
(* Goal: Phi x *)
    specialize (H0 x).
(* Goal: Phi x *)
    apply H0; right; constructor.
(* Goal: forall (Phi : @context L) (_ : @maximal L (@consistent L Gamma) Phi) (x : @expr L), iff (Phi x) (@derivable L Gamma Phi x) *)
  + intros.
(* Goal: forall (Phi : @context L) (_ : @maximal L (@consistent L Gamma) Phi) (x : @expr L), iff (Phi x) (@derivable L Gamma Phi x) *)
    hnf; intros.
(* Goal: Ensembles.In (@expr L) Phi x *)
    apply H0.
(* Goal: @consistent L Gamma (Union (@expr L) Phi (Singleton (@expr L) x)) *)
    unfold consistent in*.
(* Goal: @ex (@expr L) (fun x0 : @expr L => not (@derivable L Gamma (Union (@expr L) Phi (Singleton (@expr L) x)) x0)) *)
    destruct H1 as [y ?].
(* Goal: @ex (@expr L) (fun x0 : @expr L => not (@derivable L Gamma (Union (@expr L) Phi (Singleton (@expr L) x)) x0)) *)
    exists y.
(* Goal: not (@derivable L Gamma (Union (@expr L) Phi (Singleton (@expr L) x)) y) *)
    intro; apply H1.
(* Goal: @derivable L Gamma Psi y *)
    eapply deduction_weaken; [| exact H4].
(* Goal: Included (@expr L) (Union (@expr L) Phi (Singleton (@expr L) x)) Psi *)
    intros ? [? | ?]; auto.
(* Goal: Ensembles.In (@expr L) Psi x1 *)
    destruct H5; auto.
Qed.

Lemma maximal_consistent_derivable_closed:
  forall (Phi: context),
  maximal consistent Phi ->
  derivable_closed Phi.
Proof.
(* Goal: forall (Phi : @context L) (_ : @maximal L (@consistent L Gamma) Phi) (x : @expr L), iff (Phi x) (@derivable L Gamma Phi x) *)
  intros.
(* Goal: forall (Phi : @context L) (_ : @maximal L (@consistent L Gamma) Phi) (x : @expr L), iff (Phi x) (@derivable L Gamma Phi x) *)
  hnf; intros.
  assert (consistent (Union _ Phi (Singleton _ x))).
  Focus 1. {
    destruct H as [[y ?] _].
(* Goal: @ex (@expr L) (fun x0 : @expr L => not (@derivable L Gamma (Union (@expr L) Phi (Singleton (@expr L) x)) x0)) *)
    exists y.
    intro.
    pose proof deduction_subst1 _ _ _ H0 H1.
(* Goal: @maximal L (@consistent L Gamma) Phi *)
    auto.
  } Unfocus.
  destruct H.
  specialize (H2 _ H1).
  specialize (H2 (fun x H => Union_introl _ _ _ x H)).
  apply H2.
  right; constructor.
Qed.

Lemma MCS_element_derivable:
  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 x) (@derivable L Gamma Phi x) *)
  intros.
(* Goal: iff (Phi x) (@derivable L Gamma Phi x) *)
  apply derivable_closed_element_derivable, maximal_consistent_derivable_closed.
(* Goal: @maximal L (@consistent L Gamma) Phi *)
  auto.
Qed.

End ContextProperty.
