Require Import Coq.Logic.Classical_Prop.
Require Import Coq.Logic.Classical_Pred_Type.
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Relations.Relation_Definitions.
Require Import Logic.GeneralLogic.Base.
Require Import Logic.GeneralLogic.KripkeModel.
Require Import Logic.GeneralLogic.Semantics.Kripke.
Require Import Logic.MinimunLogic.Syntax.
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 Sound_Kripke.

Context {L: Language}
        {minL: MinimunLanguage L}
        {MD: Model}
        {kMD: KripkeModel MD}
        {M: Kmodel}
        {R: Relation (Kworlds M)}
        {po_R: PreOrder Krelation}
        {SM: Semantics L MD}
        {kiSM: KripkeIntuitionisticSemantics L MD M SM}
        {kminSM: KripkeMinimunSemantics L MD M SM}.

Lemma sound_modus_ponens:
  forall x y: expr,
    forall m,
      KRIPKE: M, m |= (x --> y) -> KRIPKE: M, m |= x -> KRIPKE: M, m |= y.
Proof.
(* Goal: forall (x y z : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@impp L minL (@impp L minL x (@impp L minL y z)) (@impp L minL (@impp L minL x y) (@impp L minL x z))) *)
  intros.
(* Goal: @satisfies L MD SM (@build_model MD kMD M m) y *)
  rewrite sat_impp in H.
(* Goal: @satisfies L MD SM (@build_model MD kMD M m) y *)
  specialize (H m).
(* Goal: @satisfies L MD SM (@build_model MD kMD M m) y *)
  apply H; auto.
(* Goal: @Krelation (@Kworlds MD kMD M) R m m *)
  reflexivity.
Qed.

Lemma sound_axiom1:
  forall x y: expr,
    forall m,
      KRIPKE: M, m |= x --> y --> x.
Proof.
(* Goal: forall (x y z : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@impp L minL (@impp L minL x (@impp L minL y z)) (@impp L minL (@impp L minL x y) (@impp L minL x z))) *)
  intros.
(* Goal: forall (x y z : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@impp L minL (@impp L minL x (@impp L minL y z)) (@impp L minL (@impp L minL x y) (@impp L minL x z))) *)
  rewrite sat_impp; intros.
(* Goal: forall (x y z : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@impp L minL (@impp L minL x (@impp L minL y z)) (@impp L minL (@impp L minL x y) (@impp L minL x z))) *)
  rewrite sat_impp; intros.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n0) x *)
  eapply sat_mono; eauto.
Qed.

Lemma sound_axiom2:
  forall x y z: expr,
    forall m,
      KRIPKE: M, m |= (x --> y --> z) --> (x --> y) --> (x --> z).
Proof.
(* Goal: forall (x y z : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@impp L minL (@impp L minL x (@impp L minL y z)) (@impp L minL (@impp L minL x y) (@impp L minL x z))) *)
  intros.
(* Goal: forall (x y z : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@impp L minL (@impp L minL x (@impp L minL y z)) (@impp L minL (@impp L minL x y) (@impp L minL x z))) *)
  rewrite sat_impp; intros.
(* Goal: forall (x y z : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@impp L minL (@impp L minL x (@impp L minL y z)) (@impp L minL (@impp L minL x y) (@impp L minL x z))) *)
  rewrite sat_impp; intros.
(* Goal: forall (x y z : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@impp L minL (@impp L minL x (@impp L minL y z)) (@impp L minL (@impp L minL x y) (@impp L minL x z))) *)
  rewrite sat_impp; intros.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n1) z *)
  assert (n <= n1) by (etransitivity; eauto).

(* Goal: @satisfies L MD SM (@build_model MD kMD M n1) z *)
  rewrite sat_impp in H0.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n1) z *)
  specialize (H0 n1 H5 H4).
(* Goal: @satisfies L MD SM (@build_model MD kMD M n1) z *)
  rewrite sat_impp in H2.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n1) z *)
  specialize (H2 n1 H3 H4).

(* Goal: @satisfies L MD SM (@build_model MD kMD M n1) z *)
  rewrite sat_impp in H0.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n1) z *)
  specialize (H0 n1 ltac:(reflexivity) H2).
(* Goal: @satisfies L MD SM (@build_model MD kMD M n1) z *)
  auto.
Qed.

End Sound_Kripke.
