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.MinimunLogic.Syntax.
Require Import Logic.MinimunLogic.ProofTheory.Minimun.
Require Import Logic.MinimunLogic.Semantics.Trivial.
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.Trivial.
Require Import Logic.PropositionalLogic.Complete.ContextProperty_Kripke.
Require Import Logic.PropositionalLogic.Complete.ContextProperty_Trivial.
Require Import Logic.PropositionalLogic.Complete.ContextProperty_Kripke.
Require Import Logic.PropositionalLogic.Complete.ContextProperty_Trivial.

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

Section TruthLemma.

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}
        {MD: Model}
        {kMD: KripkeModel MD}
        {M: Kmodel}
        {SM: Semantics L MD}
        {tminSM: TrivialMinimunSemantics L MD SM}
        {tpSM: TrivialPropositionalSemantics L MD SM}.

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

Context (AL_MC: at_least (maximal consistent) cP).

Lemma truth_lemma_falsep:
  forall m Phi, rel m Phi -> (KRIPKE: M, m |= falsep <-> proj1_sig Phi falsep).
Proof.
(* Goal: forall (m : @Kworlds MD kMD M) (Phi : @sig (@context L) cP) (_ : bij_R (@Kworlds MD kMD M) (@sig (@context L) cP) rel m Phi), iff (@satisfies L MD SM (@build_model MD kMD M m) (@impp L minL x y)) (@proj1_sig (@context L) cP Phi (@impp L minL x y)) *)
  intros.
(* Goal: iff (@satisfies L MD SM (@build_model MD kMD M m) (@falsep L pL)) (@proj1_sig (@context L) cP Phi (@falsep L pL)) *)
  rewrite sat_falsep.
(* Goal: iff False (@proj1_sig (@context L) cP Phi (@falsep L pL)) *)
  pose proof proj2_sig Phi.
(* Goal: iff False (@proj1_sig (@context L) cP Phi (@falsep L pL)) *)
  pose proof proj1 (AL_MC _ H0).
(* Goal: iff False (@proj1_sig (@context L) cP Phi (@falsep L pL)) *)
  rewrite consistent_spec in H1.
(* Goal: iff False (@proj1_sig (@context L) cP Phi (@falsep L pL)) *)
  split; [intros [] |].
(* Goal: forall _ : @proj1_sig (@context L) cP Phi (@falsep L pL), False *)
  intro; apply H1.
(* Goal: @derivable L Gamma (@proj1_sig (@context L) cP Phi) (@falsep L pL) *)
  apply derivable_assum; auto.
Qed.

Lemma truth_lemma_andp
      (x y: expr)
      (IHx: forall m Phi, rel m Phi -> (KRIPKE: M, m |= x <-> proj1_sig Phi x))
      (IHy: forall m Phi, rel m Phi -> (KRIPKE: M, m |= y <-> proj1_sig Phi y)):
  forall m Phi, rel m Phi -> (KRIPKE: M, m |= x && y <-> proj1_sig Phi (x && y)).
Proof.
(* Goal: forall (m : @Kworlds MD kMD M) (Phi : @sig (@context L) cP) (_ : bij_R (@Kworlds MD kMD M) (@sig (@context L) cP) rel m Phi), iff (@satisfies L MD SM (@build_model MD kMD M m) (@impp L minL x y)) (@proj1_sig (@context L) cP Phi (@impp L minL x y)) *)
  intros.
(* Goal: iff (@satisfies L MD SM (@build_model MD kMD M m) (@andp L pL x y)) (@proj1_sig (@context L) cP Phi (@andp L pL x y)) *)
  rewrite sat_andp.
(* Goal: iff (and (@satisfies L MD SM (@build_model MD kMD M m) x) (@satisfies L MD SM (@build_model MD kMD M m) y)) (@proj1_sig (@context L) cP Phi (@andp L pL x y)) *)
  rewrite MCS_andp_iff by (apply AL_MC, (proj2_sig Phi)).
(* Goal: iff (and (@satisfies L MD SM (@build_model MD kMD M m) x) (@satisfies L MD SM (@build_model MD kMD M m) y)) (and (@proj1_sig (@context L) cP Phi x) (@proj1_sig (@context L) cP Phi y)) *)
  apply Morphisms_Prop.and_iff_morphism; auto.
Qed.

Lemma truth_lemma_orp
      (x y: expr)
      (IHx: forall m Phi, rel m Phi -> (KRIPKE: M, m |= x <-> proj1_sig Phi x))
      (IHy: forall m Phi, rel m Phi -> (KRIPKE: M, m |= y <-> proj1_sig Phi y)):
  forall m Phi, rel m Phi -> (KRIPKE: M, m |= x || y <-> proj1_sig Phi (x || y)).
Proof.
(* Goal: forall (m : @Kworlds MD kMD M) (Phi : @sig (@context L) cP) (_ : bij_R (@Kworlds MD kMD M) (@sig (@context L) cP) rel m Phi), iff (@satisfies L MD SM (@build_model MD kMD M m) (@impp L minL x y)) (@proj1_sig (@context L) cP Phi (@impp L minL x y)) *)
  intros.
(* Goal: iff (@satisfies L MD SM (@build_model MD kMD M m) (@orp L pL x y)) (@proj1_sig (@context L) cP Phi (@orp L pL x y)) *)
  rewrite sat_orp.
(* Goal: iff (or (@satisfies L MD SM (@build_model MD kMD M m) x) (@satisfies L MD SM (@build_model MD kMD M m) y)) (@proj1_sig (@context L) cP Phi (@orp L pL x y)) *)
  rewrite MCS_orp_iff by (apply AL_MC, (proj2_sig Phi)).
(* Goal: iff (or (@satisfies L MD SM (@build_model MD kMD M m) x) (@satisfies L MD SM (@build_model MD kMD M m) y)) (or (@proj1_sig (@context L) cP Phi x) (@proj1_sig (@context L) cP Phi y)) *)
  apply Morphisms_Prop.or_iff_morphism; auto.
Qed.

Lemma truth_lemma_impp
      (x y: expr)
      (IHx: forall m Phi, rel m Phi -> (KRIPKE: M, m |= x <-> proj1_sig Phi x))
      (IHy: forall m Phi, rel m Phi -> (KRIPKE: M, m |= y <-> proj1_sig Phi y)):
  forall m Phi, rel m Phi -> (KRIPKE: M, m |= x --> y <-> proj1_sig Phi (x --> y)).
Proof.
(* Goal: forall (m : @Kworlds MD kMD M) (Phi : @sig (@context L) cP) (_ : bij_R (@Kworlds MD kMD M) (@sig (@context L) cP) rel m Phi), iff (@satisfies L MD SM (@build_model MD kMD M m) (@impp L minL x y)) (@proj1_sig (@context L) cP Phi (@impp L minL x y)) *)
  intros.
(* Goal: iff (@satisfies L MD SM (@build_model MD kMD M m) (@impp L minL x y)) (@proj1_sig (@context L) cP Phi (@impp L minL x y)) *)
  rewrite sat_impp.
(* Goal: iff (forall _ : @satisfies L MD SM (@build_model MD kMD M m) x, @satisfies L MD SM (@build_model MD kMD M m) y) (@proj1_sig (@context L) cP Phi (@impp L minL x y)) *)
  rewrite MCS_impp_iff by (apply AL_MC, (proj2_sig Phi)).
(* Goal: iff (forall _ : @satisfies L MD SM (@build_model MD kMD M m) x, @satisfies L MD SM (@build_model MD kMD M m) y) (forall _ : @proj1_sig (@context L) cP Phi x, @proj1_sig (@context L) cP Phi y) *)
  apply Morphisms_Prop.iff_iff_iff_impl_morphism; auto.
Qed.

End TruthLemma.


