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.
Require Import Logic.PropositionalLogic.Syntax.
Require Import Logic.PropositionalLogic.Semantics.Kripke.

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

Section Sound_Kripke.

Context {L: Language}
        {minL: MinimunLanguage L}
        {pL: PropositionalLanguage 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}
        {kpSM: KripkePropositionalSemantics L MD M SM}.

Lemma sound_andp_intros:
  forall x y: expr,
    forall m,
      KRIPKE: M, m |= x --> y --> x && y.
Proof.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@orp L pL (@negp L minL pL x) (@negp L minL pL (@negp L minL pL x))) *)
  intros.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@orp L pL (@negp L minL pL x) (@negp L minL pL (@negp L minL pL x))) *)
  rewrite sat_impp; intros.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@orp L pL (@negp L minL pL x) (@negp L minL pL (@negp L minL pL x))) *)
  rewrite sat_impp; intros.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n0) (@andp L pL x y) *)
  rewrite sat_andp.
(* Goal: and (@satisfies L MD SM (@build_model MD kMD M n0) x) (@satisfies L MD SM (@build_model MD kMD M n0) y) *)
  split.
  + eapply sat_mono; eauto.
  + auto.
Qed.

Lemma sound_andp_elim1:
  forall x y: expr,
    forall m,
      KRIPKE: M, m |= x && y --> x.
Proof.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@orp L pL (@negp L minL pL x) (@negp L minL pL (@negp L minL pL x))) *)
  intros.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@orp L pL (@negp L minL pL x) (@negp L minL pL (@negp L minL pL x))) *)
  rewrite sat_impp; intros.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) y *)
  rewrite sat_andp in H0.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n0) y *)
  tauto.
Qed.

Lemma sound_andp_elim2:
  forall x y: expr,
    forall m,
      KRIPKE: M, m |= x && y --> y.
Proof.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@orp L pL (@negp L minL pL x) (@negp L minL pL (@negp L minL pL x))) *)
  intros.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@orp L pL (@negp L minL pL x) (@negp L minL pL (@negp L minL pL x))) *)
  rewrite sat_impp; intros.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) y *)
  rewrite sat_andp in H0.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n0) y *)
  tauto.
Qed.

Lemma sound_orp_intros1:
  forall x y: expr,
    forall m,
      KRIPKE: M, m |= x --> x || y.
Proof.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@orp L pL (@negp L minL pL x) (@negp L minL pL (@negp L minL pL x))) *)
  intros.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@orp L pL (@negp L minL pL x) (@negp L minL pL (@negp L minL pL x))) *)
  rewrite sat_impp; intros.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) (@orp L pL x y) *)
  rewrite sat_orp.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n0) y *)
  tauto.
Qed.

Lemma sound_orp_intros2:
  forall x y: expr,
    forall m,
      KRIPKE: M, m |= y --> x || y.
Proof.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@orp L pL (@negp L minL pL x) (@negp L minL pL (@negp L minL pL x))) *)
  intros.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@orp L pL (@negp L minL pL x) (@negp L minL pL (@negp L minL pL x))) *)
  rewrite sat_impp; intros.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) (@orp L pL x y) *)
  rewrite sat_orp.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n0) y *)
  tauto.
Qed.

Lemma sound_orp_elim:
  forall x y z: expr,
    forall m,
      KRIPKE: M, m |= (x --> z) --> (y --> z) --> (x || y --> z).
Proof.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@orp L pL (@negp L minL pL x) (@negp L minL pL (@negp L minL pL x))) *)
  intros.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@orp L pL (@negp L minL pL x) (@negp L minL pL (@negp L minL pL x))) *)
  rewrite sat_impp; intros.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@orp L pL (@negp L minL pL x) (@negp L minL pL (@negp L minL pL x))) *)
  rewrite sat_impp; intros.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@orp L pL (@negp L minL pL x) (@negp L minL pL (@negp L minL pL x))) *)
  rewrite sat_impp; intros.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n1) z *)
  rewrite sat_orp in H4.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n1) z *)
  destruct H4.
  + rewrite sat_impp in H0.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n0) y *)
    apply H0; auto.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n0) y *)
    etransitivity; eauto.
  + rewrite sat_impp in H2.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n0) y *)
    apply H2; auto.
Qed.

Lemma sound_falsep_elim:
  forall x: expr,
    forall m,
      KRIPKE: M, m |= FF --> x.
Proof.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@orp L pL (@negp L minL pL x) (@negp L minL pL (@negp L minL pL x))) *)
  intros.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@orp L pL (@negp L minL pL x) (@negp L minL pL (@negp L minL pL x))) *)
  rewrite sat_impp; intros.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) x *)
  pose proof sat_falsep n.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n0) y *)
  tauto.
Qed.

Lemma sound_excluded_middle_ident {ikiM: IdentityKripkeIntuitionisticModel (Kworlds M)}:
  forall x: expr,
    forall m, KRIPKE: M, m |= x || ~~ x.
Proof.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@orp L pL (@negp L minL pL x) (@negp L minL pL (@negp L minL pL x))) *)
  intros.
(* Goal: @satisfies L MD SM (@build_model MD kMD M m) (@orp L pL (@negp L minL pL x) (@negp L minL pL (@negp L minL pL x))) *)
  unfold negp.
(* Goal: @satisfies L MD SM (@build_model MD kMD M m) (@orp L pL x (@impp L minL x (@falsep L pL))) *)
  rewrite sat_orp, sat_impp.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n0) y *)
  destruct (Classical_Prop.classic (KRIPKE: M, m |= x)); auto.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@orp L pL (@negp L minL pL x) (@negp L minL pL (@negp L minL pL x))) *)
  right; intros.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) (@falsep L pL) *)
  apply ikiM in H0; subst n.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n0) y *)
  tauto.
Qed.

Lemma sound_impp_choice_no_branch {nkiM: NoBranchKripkeIntuitionisticModel (Kworlds M)}:
  forall x y: expr,
    forall m, KRIPKE: M, m |= (x --> y) || (y --> x).
Proof.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@orp L pL (@negp L minL pL x) (@negp L minL pL (@negp L minL pL x))) *)
  intros.
(* Goal: @satisfies L MD SM (@build_model MD kMD M m) (@orp L pL (@impp L minL x (@falsep L pL)) (@impp L minL (@impp L minL x (@falsep L pL)) (@falsep L pL))) *)
  rewrite sat_orp, !sat_impp.
(* Goal: 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), @satisfies L MD SM (@build_model MD kMD M n) (@falsep L pL)) (forall (n : @Kworlds MD kMD M) (_ : @Krelation (@Kworlds MD kMD M) R m n) (_ : @satisfies L MD SM (@build_model MD kMD M n) (@impp L minL x (@falsep L pL))), @satisfies L MD SM (@build_model MD kMD M n) (@falsep L pL)) *)
  apply Classical_Prop.NNPP; intro.
(* Goal: False *)
  apply not_or_and in H; destruct H.
(* Goal: False *)
  apply not_all_ex_not in H.
(* Goal: False *)
  apply not_all_ex_not in H0.
(* Goal: False *)
  destruct H as [n1 ?], H0 as [n2 ?].
(* Goal: False *)
  apply imply_to_and in H.
(* Goal: False *)
  apply imply_to_and in H0.
(* Goal: False *)
  destruct H, H0.
(* Goal: False *)
  apply imply_to_and in H1.
(* Goal: False *)
  apply imply_to_and in H2.
(* Goal: False *)
  destruct H1, H2.
(* Goal: False *)
  destruct (Korder_no_branch n1 n2 m H H0).
  + pose proof (sat_mono _ _ x H5).
(* Goal: @satisfies L MD SM (@build_model MD kMD M n0) y *)
    tauto.
  + pose proof (sat_mono _ _ y H5).
(* Goal: @satisfies L MD SM (@build_model MD kMD M n0) y *)
    tauto.
Qed.

Lemma sound_weak_excluded_middle_branch_join {bkiM: BranchJoinKripkeIntuitionisticModel (Kworlds M)}:
  forall x: expr,
    forall m, KRIPKE: M, m |= ~~ x || ~~ ~~ x.
Proof.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@orp L pL (@negp L minL pL x) (@negp L minL pL (@negp L minL pL x))) *)
  intros.
(* Goal: @satisfies L MD SM (@build_model MD kMD M m) (@orp L pL (@negp L minL pL x) (@negp L minL pL (@negp L minL pL x))) *)
  unfold negp.
(* Goal: @satisfies L MD SM (@build_model MD kMD M m) (@orp L pL (@impp L minL x (@falsep L pL)) (@impp L minL (@impp L minL x (@falsep L pL)) (@falsep L pL))) *)
  rewrite sat_orp, !sat_impp.
(* Goal: 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), @satisfies L MD SM (@build_model MD kMD M n) (@falsep L pL)) (forall (n : @Kworlds MD kMD M) (_ : @Krelation (@Kworlds MD kMD M) R m n) (_ : @satisfies L MD SM (@build_model MD kMD M n) (@impp L minL x (@falsep L pL))), @satisfies L MD SM (@build_model MD kMD M n) (@falsep L pL)) *)
  apply Classical_Prop.NNPP; intro.
(* Goal: False *)
  apply not_or_and in H; destruct H.
(* Goal: False *)
  apply not_all_ex_not in H.
(* Goal: False *)
  apply not_all_ex_not in H0.
(* Goal: False *)
  destruct H as [n1 ?], H0 as [n2 ?].
(* Goal: False *)
  apply imply_to_and in H.
(* Goal: False *)
  apply imply_to_and in H0.
(* Goal: False *)
  destruct H, H0.
(* Goal: False *)
  apply imply_to_and in H1.
(* Goal: False *)
  apply imply_to_and in H2.
(* Goal: False *)
  destruct H1 as [? _], H2 as [? _].
(* Goal: False *)
  destruct (Korder_branch_join n1 n2 m H H0) as [n [? ?]].
(* Goal: False *)
  eapply sat_mono in H2; [| eassumption].
(* Goal: False *)
  eapply sat_mono in H1; [| eassumption].
(* Goal: False *)
  rewrite sat_impp in H2.
(* Goal: False *)
  apply (H2 n) in H1; [| reflexivity].
(* Goal: @satisfies L MD SM (@build_model MD kMD M n0) y *)
  apply sat_falsep in H1; auto.
Qed.

End Sound_Kripke.
