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.ProofTheory.BasicSequentCalculus.
Require Import Logic.GeneralLogic.KripkeModel.
Require Import Logic.GeneralLogic.Semantics.Kripke.
Require Import Logic.GeneralLogic.Complete.ContextProperty.
Require Import Logic.GeneralLogic.Complete.ContextProperty_Kripke.
Require Import Logic.GeneralLogic.Complete.Lindenbaum.
Require Import Logic.MinimunLogic.Syntax.
Require Import Logic.MinimunLogic.ProofTheory.Minimun.
Require Import Logic.MinimunLogic.Semantics.Kripke.

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

Section TruthLemma.

Context {L: Language}
        {minL: MinimunLanguage L}
        {Gamma: ProofTheory L}
        {bSC: BasicSequentCalculus L Gamma}
        {minSC: MinimunSequentCalculus L Gamma}
        {MD: Model}
        {kMD: KripkeModel MD}
        {M: Kmodel}
        {R: Relation (Kworlds M)}
        {SM: Semantics L MD}
        {kminSM: KripkeMinimunSemantics L MD M SM}.

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

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_impp
      (AL_DC: at_least derivable_closed cP)
      (LIN_CD: forall x, Lindenbaum_constructable (cannot_derive x) cP)
      (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: 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)) *)
  split; intros.
  + rewrite derivable_closed_element_derivable by (apply AL_DC, (proj2_sig Phi)).
(* Goal: @derivable L Gamma (@proj1_sig (@context L) cP Phi) (@impp L minL x y) *)
    rewrite <- deduction_theorem.
(* Goal: @derivable L Gamma (Union (@expr L) (@proj1_sig (@context L) cP Phi) (Singleton (@expr L) x)) y *)
    apply NNPP; intro.
(* Goal: False *)
    apply LIN_CD in H1.
(* Goal: False *)
    destruct H1 as [Psi [? ?]].
(* Goal: False *)
    apply H2; clear H2.
(* Goal: @derivable L Gamma (@proj1_sig (Ensemble (@expr L)) cP Psi) y *)
    assert (Included _ (proj1_sig Phi) (proj1_sig Psi)) by (intros ? ?; apply H1; left; auto).
(* Goal: @derivable L Gamma (@proj1_sig (Ensemble (@expr L)) cP Psi) y *)
    assert (proj1_sig Psi x) by (apply H1; right; constructor; auto).
(* Goal: @derivable L Gamma (@proj1_sig (Ensemble (@expr L)) cP Psi) y *)
    clear H1.
(* Goal: @derivable L Gamma (@proj1_sig (Ensemble (@expr L)) cP Psi) y *)
    destruct (su_bij _ _ rel Psi) as [n ?].
(* Goal: @derivable L Gamma (@proj1_sig (@context L) cP Psi) (@impp L minL x y) *)
    rewrite <- derivable_closed_element_derivable by (apply AL_DC, (proj2_sig Psi)).
(* Goal: @proj1_sig (Ensemble (@expr L)) cP Psi y *)
    rewrite <- (IHx _ _ H1) in H3.
(* Goal: @proj1_sig (Ensemble (@expr L)) cP Psi y *)
    rewrite <- (IHy _ _ H1).
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) y *)
    apply H0; auto.
(* Goal: @Krelation (@Kworlds MD kMD M) R m n *)
    erewrite H_R by eauto.
(* Goal: Included (@expr L) (@proj1_sig (@context L) cP Phi) (@proj1_sig (@context L) cP Psi) *)
    auto.
  + destruct (im_bij _ _ rel n) as [Psi ?].
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) y *)
    rewrite (IHx _ _ H3) in H2.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) y *)
    rewrite (IHy _ _ H3).
(* Goal: @proj1_sig (@context L) cP Psi y *)
    rewrite derivable_closed_element_derivable in H2 |- * by (apply AL_DC, (proj2_sig Psi)).
(* Goal: @derivable L Gamma (@proj1_sig (@context L) cP Psi) y *)
    eapply deduction_modus_ponens; [exact H2 |].
(* Goal: @derivable L Gamma (@proj1_sig (@context L) cP Psi) (@impp L minL x y) *)
    rewrite <- derivable_closed_element_derivable by (apply AL_DC, (proj2_sig Psi)).
(* Goal: Included (@expr L) (@proj1_sig (@context L) cP Phi) (@proj1_sig (@context L) cP Psi) *)
    erewrite H_R in H1 by eauto.
(* Goal: Included (@expr L) (@proj1_sig (@context L) cP Phi) (@proj1_sig (@context L) cP Psi) *)
    apply H1; auto.
Qed.

End TruthLemma.


