Require Import Logic.lib.Bijection.
Require Import Logic.lib.Countable.
Require Import Logic.lib.EnsemblesProperties.
Require Import Logic.GeneralLogic.Base.
Require Import Logic.GeneralLogic.ProofTheory.BasicSequentCalculus.
Require Import Logic.GeneralLogic.Complete.Lindenbaum.
Require Import Logic.GeneralLogic.Complete.Lindenbaum_Kripke.
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.MinimunLogic.Complete.Lindenbaum_Kripke.
Require Import Logic.PropositionalLogic.Syntax.
Require Import Logic.PropositionalLogic.ProofTheory.Intuitionistic.
Require Import Logic.PropositionalLogic.Complete.ContextProperty_Kripke.

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

Section Lindenbaum_Kripke.

Context {L: Language}
        {minL: MinimunLanguage L}
        {pL: PropositionalLanguage L}
        {Gamma: ProofTheory L}
        {SC: NormalSequentCalculus L Gamma}
        {bSC: BasicSequentCalculus L Gamma}
        {fwSC: FiniteWitnessedSequentCalculus L Gamma}
        {minSC: MinimunSequentCalculus L Gamma}
        {ipSC: IntuitionisticPropositionalSequentCalculus L Gamma}
        {minAX: MinimunAxiomatization L Gamma}
        {ipGamma: IntuitionisticPropositionalLogic L Gamma}.

Lemma Lindenbaum_for_orp_witnessed: forall P,
  Lindenbaum_preserves P ->
  subset_preserved P ->
  context_orp_captured P ->
  Lindenbaum_ensures P derivable_closed ->
  Lindenbaum_ensures P orp_witnessed.
Proof.
(* Goal: forall (P : forall _ : Ensemble (@expr L), Prop) (_ : @Lindenbaum_preserves (@expr L) P) (_ : @subset_preserved (@expr L) P) (_ : @context_orp_captured L pL Gamma P) (_ : @Lindenbaum_ensures (@expr L) P (@derivable_closed L Gamma)), @Lindenbaum_ensures (@expr L) P (@orp_witnessed L pL) *)
  intros; hnf; intros.
(* Goal: @orp_witnessed L pL (@LindenbaumConstruction (@expr L) CA init P) *)
  specialize (H2 CA init H3).
(* Goal: @orp_witnessed L pL (@LindenbaumConstruction (@expr L) CA init P) *)
  rename H2 into DC.
(* Goal: @at_least L (@consistent L Gamma) (fun Phi : @context L => not (@derivable L Gamma Phi x)) *)
  hnf; intros.
(* Goal: or (@LindenbaumConstruction (@expr L) CA init P x) (@LindenbaumConstruction (@expr L) CA init P y) *)
  pose proof H0.
(* Goal: or (@LindenbaumConstruction (@expr L) CA init P x) (@LindenbaumConstruction (@expr L) CA init P y) *)
  apply subset_preserved_same_set_preserved in H4.
(* Goal: or (@LindenbaumConstruction (@expr L) CA init P x) (@LindenbaumConstruction (@expr L) CA init P y) *)
  pose proof H CA _ H3.
(* Goal: or (@LindenbaumConstruction (@expr L) CA init P x) (@LindenbaumConstruction (@expr L) CA init P y) *)
  destruct (im_inj _ _ CA x) as [n ?].
(* Goal: or (@LindenbaumConstruction (@expr L) CA init P x) (@LindenbaumConstruction (@expr L) CA init P y) *)
  destruct (im_inj _ _ CA y) as [m ?].
(* Goal: or (@LindenbaumConstruction (@expr L) CA init P x) (@LindenbaumConstruction (@expr L) CA init P y) *)
  rewrite <- !Lindenbaum_pointwise_finite_decided' by eauto.
(* Goal: or (P (Union (@expr L) (@LindenbaumChain (@expr L) CA init P n) (Singleton (@expr L) x))) (P (Union (@expr L) (@LindenbaumChain (@expr L) CA init P m) (Singleton (@expr L) y))) *)
  apply H1.
(* Goal: P (@context_orp L pL Gamma (Union (@expr L) (@LindenbaumChain (@expr L) CA init P n) (Singleton (@expr L) x)) (Union (@expr L) (@LindenbaumChain (@expr L) CA init P m) (Singleton (@expr L) y))) *)
  eapply H0; [| exact H5].
(* Goal: Included (@expr L) (@context_orp L pL Gamma (Union (@expr L) (@LindenbaumChain (@expr L) CA init P n) (Singleton (@expr L) x)) (Union (@expr L) (@LindenbaumChain (@expr L) CA init P m) (Singleton (@expr L) y))) (@LindenbaumConstruction (@expr L) CA init P) *)
  unfold Included, Ensembles.In; intros z ?.
(* Goal: @LindenbaumConstruction (@expr L) CA init P z *)
  destruct H8 as [x0 [y0 [? [? ?]]]]; subst z.
(* Goal: @LindenbaumConstruction (@expr L) CA init P (@orp L pL x0 y0) *)
  apply deduction_orp_intros1 with (y1 := y0) in H9.
(* Goal: @LindenbaumConstruction (@expr L) CA init P (@orp L pL x0 y0) *)
  apply deduction_orp_intros2 with (x1 := x0) in H10.
(* Goal: @LindenbaumConstruction (@expr L) CA init P (@orp L pL x0 y0) *)
  rewrite deduction_theorem in H9, H10.
(* Goal: @LindenbaumConstruction (@expr L) CA init P (@orp L pL x0 y0) *)
  eapply deduction_weaken in H9; [| apply Lindenbaum_included_n_omega].
(* Goal: @LindenbaumConstruction (@expr L) CA init P (@orp L pL x0 y0) *)
  eapply deduction_weaken in H10; [| apply Lindenbaum_included_n_omega].
(* Goal: @LindenbaumConstruction (@expr L) CA init P (@orp L pL x0 y0) *)
  pose proof deduction_orp_elim' _ _ _ _ H9 H10.
(* Goal: @LindenbaumConstruction (@expr L) CA init P (@orp L pL x0 y0) *)
  apply derivable_assum in H2.
(* Goal: @LindenbaumConstruction (@expr L) CA init P (@orp L pL x0 y0) *)
  pose proof deduction_modus_ponens _ _ _ H2 H8.
(* Goal: @LindenbaumConstruction (@expr L) CA init P (@orp L pL x0 y0) *)
  apply DC; auto.
Qed.

Lemma Lindenbaum_cannot_derive_ensures_orp_witnessed {AX: NormalAxiomatization L Gamma}: forall x, Lindenbaum_ensures (cannot_derive x) orp_witnessed.
Proof.
(* Goal: forall x : @expr L, @Lindenbaum_ensures (@expr L) (@cannot_derive L Gamma x) (@consistent L Gamma) *)
  intros.
(* Goal: @Lindenbaum_ensures (@expr L) (@cannot_derive L Gamma x) (@orp_witnessed L pL) *)
  apply Lindenbaum_for_orp_witnessed.
  - apply Lindenbaum_preserves_cannot_derive.
  - apply cannot_derive_subset_preserved.
  - apply cannot_derive_context_orp_captured.
  - apply Lindenbaum_cannot_derive_ensures_derivable_closed.
Qed.

Lemma Lindenbaum_for_consistent: forall P,
  Lindenbaum_preserves P ->
  at_least consistent P ->
  Lindenbaum_ensures P consistent.
Proof.
(* Goal: forall x : @expr L, @Lindenbaum_ensures (@expr L) (@cannot_derive L Gamma x) (@consistent L Gamma) *)
  intros.
(* Goal: @at_least L (@consistent L Gamma) (fun Phi : @context L => not (@derivable L Gamma Phi x)) *)
  hnf; intros.
(* Goal: @consistent L Gamma (@LindenbaumConstruction (@expr L) CA init P) *)
  apply H0.
(* Goal: P (@LindenbaumConstruction (@expr L) CA init P) *)
  apply H; auto.
Qed.

Lemma Lindenbaum_cannot_derive_ensures_consistent {AX: NormalAxiomatization L Gamma}: forall x, Lindenbaum_ensures (cannot_derive x) consistent.
Proof.
(* Goal: forall x : @expr L, @Lindenbaum_ensures (@expr L) (@cannot_derive L Gamma x) (@consistent L Gamma) *)
  intros.
(* Goal: @Lindenbaum_ensures (@expr L) (@cannot_derive L Gamma x) (@consistent L Gamma) *)
  apply Lindenbaum_for_consistent.
  - apply Lindenbaum_preserves_cannot_derive.
  - unfold cannot_derive.
(* Goal: @at_least L (@consistent L Gamma) (fun Phi : @context L => not (@derivable L Gamma Phi x)) *)
    hnf; intros.
(* Goal: @consistent L Gamma Phi *)
    exists x; auto.
Qed.

End Lindenbaum_Kripke.
