Require Import Coq.Logic.Classical_Prop.
Require Import Coq.Logic.Classical_Pred_Type.
Require Import Logic.lib.Ensembles_ext.
Require Import Logic.GeneralLogic.Base.
Require Import Logic.GeneralLogic.KripkeModel.
Require Import Logic.MinimunLogic.Syntax.
Require Import Logic.MinimunLogic.Semantics.Trivial.
Require Import Logic.PropositionalLogic.Syntax.
Require Import Logic.PropositionalLogic.Semantics.Trivial.
Require Import Logic.ModalLogic.Syntax.
Require Import Logic.ModalLogic.Model.KripkeModel.
Require Import Logic.ModalLogic.Model.OrderedKripkeModel.
Require Import Logic.ModalLogic.Semantics.Kripke.

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

Section Sound_Kripke.

Context {L: Language}
        {minL: MinimunLanguage L}
        {pL: PropositionalLanguage L}
        {mL: ModalLanguage L}
        {MD: Model}
        {kMD: KripkeModel MD}
        {M: Kmodel}
        {R: Relation (Kworlds M)}
        {SM: Semantics L MD}
        {tminSM: TrivialMinimunSemantics L MD SM}
        {tpSM: TrivialPropositionalSemantics L MD SM}
        {kmSM: KripkeModalSemantics L MD M SM}.

Lemma sound_axiom_K:
  forall x y (m: Kworlds M),
    KRIPKE: M, m |= boxp (x --> y) --> (boxp x --> boxp y).
Proof.
(* Goal: forall (x y : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@boxp L mL (@orp L pL x y)) (@orp L pL (@boxp L mL x) (@boxp L mL y))) *)
  intros.
(* Goal: @satisfies L MD SM (@build_model MD kMD M m) (@impp L minL (@boxp L mL (@impp L minL x y)) (@impp L minL (@boxp L mL x) (@boxp L mL y))) *)
  rewrite !sat_impp, !sat_boxp.
(* Goal: forall (x y : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@boxp L mL (@orp L pL x y)) (@orp L pL (@boxp L mL x) (@boxp L mL y))) *)
  intros.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) y *)
  specialize (H _ H1).
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) y *)
  specialize (H0 _ H1).
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) y *)
  rewrite sat_impp in H.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) y *)
  auto.
Qed.

Lemma sound_rule_N:
  forall x,
    (forall (m: Kworlds M), KRIPKE: M, m |= x) ->
    (forall (m: Kworlds M), KRIPKE: M, m |= boxp x).
Proof.
(* Goal: forall (x y : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@boxp L mL (@orp L pL x y)) (@orp L pL (@boxp L mL x) (@boxp L mL y))) *)
  intros.
(* Goal: @satisfies L MD SM (@build_model MD kMD M m) (@boxp L mL x) *)
  rewrite sat_boxp.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) y *)
  intros; apply H; auto.
Qed.

Lemma sound_boxp_orp {pf_R: PartialFunctional KM.Krelation}:
  forall x y (m: Kworlds M),
    KRIPKE: M, m |= boxp (x || y) <--> (boxp x || boxp y).
Proof.
(* Goal: forall (x y : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@boxp L mL (@orp L pL x y)) (@orp L pL (@boxp L mL x) (@boxp L mL y))) *)
  intros.
(* Goal: @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@boxp L mL (@orp L pL x y)) (@orp L pL (@boxp L mL x) (@boxp L mL y))) *)
  unfold iffp.
(* Goal: @satisfies L MD SM (@build_model MD kMD M m) (@andp L pL (@impp L minL (@boxp L mL (@orp L pL x y)) (@orp L pL (@boxp L mL x) (@boxp L mL y))) (@impp L minL (@orp L pL (@boxp L mL x) (@boxp L mL y)) (@boxp L mL (@orp L pL x y)))) *)
  rewrite sat_andp, !sat_impp, !sat_orp, !sat_boxp.
(* Goal: forall (x y : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@boxp L mL (@orp L pL x y)) (@orp L pL (@boxp L mL x) (@boxp L mL y))) *)
  split; intros.
  + apply NNPP.
(* Goal: not (not (or (forall (n : @Kworlds MD kMD M) (_ : @Krelation (@Kworlds MD kMD M) R m n), @satisfies L MD SM (@build_model MD kMD M n) x) (forall (n : @Kworlds MD kMD M) (_ : @Krelation (@Kworlds MD kMD M) R m n), @satisfies L MD SM (@build_model MD kMD M n) y))) *)
    intro.
(* Goal: False *)
    apply not_or_and in H0; destruct H0.
(* Goal: False *)
    apply not_all_ex_not in H0; destruct H0 as [n1 ?].
(* Goal: False *)
    apply not_all_ex_not in H1; destruct H1 as [n2 ?].
(* Goal: False *)
    apply imply_to_and in H0; destruct H0.
(* Goal: False *)
    apply imply_to_and in H1; destruct H1.
(* Goal: False *)
    pose proof partial_functionality _ _ _ H0 H1.
(* Goal: False *)
    subst n2; clear H1.
(* Goal: False *)
    specialize (H _ H0).
(* Goal: False *)
    rewrite sat_orp in H.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) y *)
    tauto.
  + rewrite sat_orp.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) y *)
    destruct H; [left | right]; auto.
Qed.

End Sound_Kripke.
