Require Import Coq.Logic.Classical_Prop.
Require Import Logic.lib.Coqlib.
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.Complete.ContextProperty.
Require Import Logic.GeneralLogic.Complete.ContextProperty_Kripke.
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.RewriteClass.
Require Import Logic.PropositionalLogic.ProofTheory.ProofTheoryPatterns.

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

Section ContextProperties.

Context {L: Language}
        {minL: MinimunLanguage L}
        {pL: PropositionalLanguage L}.

Definition orp_witnessed: context -> Prop :=
  fun Phi => forall x y, Phi (orp x y) -> Phi x \/ Phi y.

Context {Gamma: ProofTheory L}.

Definition context_orp (Phi Psi: context): context :=
  fun z => exists x y, z = x || y /\ Phi |-- x /\ Psi |-- y.

Definition context_orp_captured (P: context -> Prop): Prop :=
  forall Phi Psi, P (context_orp Phi Psi) -> P Phi \/ P Psi.

Context {SC: NormalSequentCalculus L Gamma}
        {bSC: BasicSequentCalculus L Gamma}
        {minSC: MinimunSequentCalculus L Gamma}
        {ipSC: IntuitionisticPropositionalSequentCalculus L Gamma}
        {minAX: MinimunAxiomatization L Gamma}
        {ipGamma: IntuitionisticPropositionalLogic L Gamma}.

Lemma context_orp_mono: forall Phi Psi Phi' Psi',
  Included _ (derivable Phi) (derivable Phi') ->
  Included _ (derivable Psi) (derivable Psi') ->
  Included _ (context_orp Phi Psi) (context_orp Phi' Psi').
Proof.
(* Goal: forall Phi : @context L, iff (@consistent L Gamma Phi) (not (@derivable L Gamma Phi (@falsep L pL))) *)
  intros.
(* Goal: forall Phi : @context L, iff (@consistent L Gamma Phi) (not (@derivable L Gamma Phi (@falsep L pL))) *)
  hnf; unfold Ensembles.In; intros.
(* Goal: context_orp Phi' Psi' x *)
  hnf in H1 |- *.
(* Goal: @ex (@expr L) (fun x0 : @expr L => @ex (@expr L) (fun y : @expr L => and (@eq (@expr L) x (@orp L pL x0 y)) (and (@derivable L Gamma Phi' x0) (@derivable L Gamma Psi' y)))) *)
  destruct H1 as [y [z [? [? ?]]]]; subst.
(* Goal: @ex (@expr L) (fun x : @expr L => @ex (@expr L) (fun y0 : @expr L => and (@eq (@expr L) (@orp L pL y z) (@orp L pL x y0)) (and (@derivable L Gamma Phi' x) (@derivable L Gamma Psi' y0)))) *)
  exists y, z.
(* Goal: and (@eq (@expr L) (@orp L pL x x) (@orp L pL x x)) (and (@derivable L Gamma Phi x) (@derivable L Gamma Psi x)) *)
  split; [| split]; auto.
  + apply H; auto.
  + apply H0; auto.
Qed.

Lemma context_orp_mono': forall Phi Psi Phi' Psi',
  Included _ Phi Phi' ->
  Included _ Psi Psi' ->
  Included _ (context_orp Phi Psi) (context_orp Phi' Psi').
Proof.
(* Goal: forall Phi : @context L, iff (@consistent L Gamma Phi) (not (@derivable L Gamma Phi (@falsep L pL))) *)
  intros.
(* Goal: Included (@expr L) (context_orp Phi Psi) (context_orp Phi' Psi') *)
  apply context_orp_mono; hnf; intros; eapply deduction_weaken; eauto.
Qed.

Lemma cannot_derive_context_orp_captured: forall (x: expr),
  context_orp_captured (cannot_derive x).
Proof.
(* Goal: forall Phi : @context L, iff (@consistent L Gamma Phi) (not (@derivable L Gamma Phi (@falsep L pL))) *)
  intros.
(* Goal: context_orp_captured (@cannot_derive L Gamma x) *)
  unfold cannot_derive.
(* Goal: forall Phi : @context L, iff (@consistent L Gamma Phi) (not (@derivable L Gamma Phi (@falsep L pL))) *)
  hnf; intros.
(* Goal: or (not (@derivable L Gamma Phi x)) (not (@derivable L Gamma Psi x)) *)
  apply not_and_or.
(* Goal: not (and (@derivable L Gamma Phi x) (@derivable L Gamma Psi x)) *)
  intros [? ?]; apply H; clear H.
(* Goal: @derivable L Gamma (context_orp Phi Psi) x *)
  rewrite <- (orp_dup x).
(* Goal: @derivable L Gamma (context_orp Phi Psi) (@orp L pL x x) *)
  apply derivable_assum.
(* Goal: Ensembles.In (@expr L) (context_orp Phi Psi) (@orp L pL x x) *)
  exists x, x.
(* Goal: and (@eq (@expr L) (@orp L pL x x) (@orp L pL x x)) (and (@derivable L Gamma Phi x) (@derivable L Gamma Psi x)) *)
  split; [| split]; auto.
Qed.

Lemma DCS_truep: forall (Phi: context),
  derivable_closed Phi ->
  Phi TT.
Proof.
(* Goal: forall Phi : @context L, iff (@consistent L Gamma Phi) (not (@derivable L Gamma Phi (@falsep L pL))) *)
  intros.
(* Goal: Phi x *)
  apply H.
(* Goal: @derivable L Gamma Phi (@truep L minL pL) *)
  apply derivable_impp_refl.
Qed.

Lemma DCS_andp_iff: forall (Phi: context),
  derivable_closed Phi ->
  (forall x y: expr, Phi (x && y) <-> (Phi x /\ Phi y)).
Proof.
(* Goal: forall Phi : @context L, iff (@consistent L Gamma Phi) (not (@derivable L Gamma Phi (@falsep L pL))) *)
  intros.
(* Goal: iff (Phi (@orp L pL x y)) (or (Phi x) (Phi y)) *)
  pose proof derivable_closed_element_derivable _ H; clear H.
(* Goal: forall Phi : @context L, iff (@consistent L Gamma Phi) (not (@derivable L Gamma Phi (@falsep L pL))) *)
  rewrite !H0; clear H0; split; intros.
  + pose proof deduction_andp_elim1 Phi x y H.
(* Goal: and (@derivable L Gamma Phi x) (@derivable L Gamma Phi y) *)
    pose proof deduction_andp_elim2 Phi x y H.
(* Goal: @derivable L Gamma Phi (@falsep L pL) *)
    auto.
  + destruct H.
(* Goal: @derivable L Gamma Phi (@andp L pL x y) *)
    pose proof deduction_andp_intros Phi x y H H0.
(* Goal: @derivable L Gamma Phi (@falsep L pL) *)
    auto.
Qed.

Lemma DCS_iffp: forall (Phi: context) (x y: expr),
  derivable_closed Phi ->
  |-- x <--> y ->
  (Phi x <-> Phi y).
Proof.
(* Goal: forall Phi : @context L, iff (@consistent L Gamma Phi) (not (@derivable L Gamma Phi (@falsep L pL))) *)
  intros.
(* Goal: forall Phi : @context L, iff (@consistent L Gamma Phi) (not (@derivable L Gamma Phi (@falsep L pL))) *)
  split; intros.
  + apply H.
(* Goal: @derivable L Gamma Phi y *)
    rewrite <- H0.
(* Goal: @derivable L Gamma Phi (@falsep L pL) *)
    apply derivable_assum; auto.
  + apply H.
(* Goal: @derivable L Gamma Phi x *)
    rewrite H0.
(* Goal: @derivable L Gamma Phi (@falsep L pL) *)
    apply derivable_assum; auto.
Qed.

Lemma DCS_multi_and_iff: forall (Phi: context),
  derivable_closed Phi ->
  (forall xs: list expr, Phi (multi_and xs) <-> Forall Phi xs).
Proof.
(* Goal: forall Phi : @context L, iff (@consistent L Gamma Phi) (not (@derivable L Gamma Phi (@falsep L pL))) *)
  intros.
  rewrite (DCS_iffp Phi (multi_and xs) (fold_right andp TT xs)).
(* Goal: @derivable L Gamma Phi (@falsep L pL) *)
  2: auto.
  2: apply multi_and_spec.

  induction xs.
(* Goal: forall Phi : @context L, iff (@consistent L Gamma Phi) (not (@derivable L Gamma Phi (@falsep L pL))) *)
  + split; intros.
    - constructor.
    - simpl.
(* Goal: @derivable L Gamma Phi (@falsep L pL) *)
      apply DCS_truep; auto.
  + simpl.
(* Goal: @derivable L Gamma Phi (@falsep L pL) *)
    rewrite DCS_andp_iff by auto.
    rewrite IHxs.
    clear.
(* Goal: forall Phi : @context L, iff (@consistent L Gamma Phi) (not (@derivable L Gamma Phi (@falsep L pL))) *)
    split; intros.
(* Goal: @derivable L Gamma Phi (@falsep L pL) *)
    - constructor; tauto.
(* Goal: @derivable L Gamma Phi (@falsep L pL) *)
    - inversion H; auto.
Qed.

Lemma DCS_orp_iff: forall (Phi: context),
  derivable_closed Phi ->
  orp_witnessed Phi ->
  (forall x y: expr, Phi (x || y) <-> (Phi x \/ Phi y)).
Proof.
(* Goal: forall Phi : @context L, iff (@consistent L Gamma Phi) (not (@derivable L Gamma Phi (@falsep L pL))) *)
  intros.
(* Goal: iff (Phi (@orp L pL x y)) (or (Phi x) (Phi y)) *)
  pose proof derivable_closed_element_derivable _ H; clear H.
(* Goal: forall Phi : @context L, iff (@consistent L Gamma Phi) (not (@derivable L Gamma Phi (@falsep L pL))) *)
  split; intros.
  + apply H0; auto.
  + rewrite !H1 in *.
(* Goal: @derivable L Gamma Phi (@orp L pL x y) *)
    destruct H.
(* Goal: @derivable L Gamma Phi (@falsep L pL) *)
    - pose proof deduction_orp_intros1 Phi x y H; auto.
(* Goal: @derivable L Gamma Phi (@falsep L pL) *)
    - pose proof deduction_orp_intros2 Phi x y H; auto.
Qed.

Lemma derivable_closed_union_derivable {AX: NormalAxiomatization L Gamma}: forall (Phi Psi: context) (x: expr),
  derivable_closed Psi ->
  Union _ Phi Psi |-- x ->
  exists y, Psi y /\ Phi |-- y --> x.
Proof.
(* Goal: forall Phi : @context L, iff (@consistent L Gamma Phi) (not (@derivable L Gamma Phi (@falsep L pL))) *)
  intros.
  rewrite derivable_provable in H0.
  destruct H0 as [xs [? ?]].
  pose proof provable_multi_imp_split _ _ _ _ H0 H1 as [xs1 [xs2 [? [? ?]]]].
  pose proof H4.
  rewrite <- multi_and_multi_imp in H4.
  eapply modus_ponens in H4; [| apply provable_multi_imp_arg_switch1].
  exists (multi_and xs2).
  split.
  + apply DCS_multi_and_iff; auto.
  + rewrite derivable_provable.
    exists xs1.
(* Goal: @derivable L Gamma Phi (@falsep L pL) *)
    split; auto.
    eapply modus_ponens.
    - apply provable_multi_imp_weaken.
      rewrite (multi_and_multi_imp xs2 x).
      apply provable_impp_refl.
    - exact H5.
Qed.

Lemma consistent_spec:
  forall (Phi: context), consistent Phi <-> ~ Phi |-- FF.
Proof.
(* Goal: forall Phi : @context L, iff (@consistent L Gamma Phi) (not (@derivable L Gamma Phi (@falsep L pL))) *)
  intros.
(* Goal: forall Phi : @context L, iff (@consistent L Gamma Phi) (not (@derivable L Gamma Phi (@falsep L pL))) *)
  split; intros.
  + intro.
(* Goal: False *)
    destruct H as [x H]; apply H; clear H.
(* Goal: @derivable L Gamma Phi x *)
    apply deduction_falsep_elim.
(* Goal: @derivable L Gamma Phi (@falsep L pL) *)
    auto.
  + exists FF; auto.
Qed.

End ContextProperties.
