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.Kripke.
Require Import Logic.MinimunLogic.Complete.ContextProperty_Kripke.
Require Import Logic.PropositionalLogic.Syntax.
Require Import Logic.PropositionalLogic.ProofTheory.Intuitionistic.
Require Import Logic.PropositionalLogic.Semantics.Kripke.
Require Import Logic.PropositionalLogic.Complete.ContextProperty_Kripke.

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}
        {MD: Model}
        {kMD: KripkeModel MD}
        {M: Kmodel}
        {R: Relation (Kworlds M)}
        {SM: Semantics L MD}
        {kminSM: KripkeMinimunSemantics L MD M SM}
        {kpSM: KripkePropositionalSemantics L MD M SM}.

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

Hypothesis H_R: forall m n Phi Psi, rel m Phi -> rel n Psi -> (m <= n <-> Included _ (proj1_sig Phi) (proj1_sig Psi)).

Lemma truth_lemma_falsep (AL_CONSI: at_least consistent P):
  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) P) (_ : bij_R (@Kworlds MD kMD M) (@sig (@context L) P) rel m Phi), iff (@satisfies L MD SM (@build_model MD kMD M m) (@andp L pL x y)) (@proj1_sig (@context L) P Phi (@andp L pL x y)) *)
  intros.
(* Goal: iff (@satisfies L MD SM (@build_model MD kMD M m) (@falsep L pL)) (@proj1_sig (@context L) P Phi (@falsep L pL)) *)
  rewrite sat_falsep.
(* Goal: iff False (@proj1_sig (@context L) P Phi (@falsep L pL)) *)
  pose proof proj2_sig Phi.
(* Goal: iff False (@proj1_sig (@context L) P Phi (@falsep L pL)) *)
  pose proof AL_CONSI _ H0.
(* Goal: iff False (@proj1_sig (@context L) P Phi (@falsep L pL)) *)
  rewrite consistent_spec in H1.
(* Goal: iff False (@proj1_sig (@context L) P Phi (@falsep L pL)) *)
  split; [intros [] |].
(* Goal: forall _ : @proj1_sig (@context L) P Phi (@falsep L pL), False *)
  intro; apply H1.
(* Goal: @derivable L Gamma (@proj1_sig (@context L) P Phi) (@falsep L pL) *)
  apply derivable_assum; auto.
Qed.

Lemma truth_lemma_andp
      (AL_DC: at_least derivable_closed P)
      (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) P) (_ : bij_R (@Kworlds MD kMD M) (@sig (@context L) P) rel m Phi), iff (@satisfies L MD SM (@build_model MD kMD M m) (@andp L pL x y)) (@proj1_sig (@context L) P Phi (@andp L pL x y)) *)
  intros.
(* Goal: iff (@satisfies L MD SM (@build_model MD kMD M m) (@andp L pL x y)) (@proj1_sig (@context L) P 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) P Phi (@andp L pL x y)) *)
  rewrite DCS_andp_iff by (apply AL_DC, (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) P Phi x) (@proj1_sig (@context L) P Phi y)) *)
  apply Morphisms_Prop.and_iff_morphism; auto.
Qed.

Lemma truth_lemma_orp
      (AL_DC: at_least derivable_closed P)
      (AL_OW: at_least orp_witnessed P)
      (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) P) (_ : bij_R (@Kworlds MD kMD M) (@sig (@context L) P) rel m Phi), iff (@satisfies L MD SM (@build_model MD kMD M m) (@andp L pL x y)) (@proj1_sig (@context L) P Phi (@andp L pL x y)) *)
  intros.
  rewrite sat_orp.
  rewrite DCS_orp_iff.
    2: apply AL_DC, (proj2_sig Phi).
    2: apply AL_OW, (proj2_sig Phi).
  apply Morphisms_Prop.or_iff_morphism; auto.
Qed.

End TruthLemma.


