Require Import Logic.lib.Ensembles_ext.
Require Import Logic.GeneralLogic.Base.
Require Import Logic.MinimunLogic.Syntax.
Require Import Logic.PropositionalLogic.Syntax.
Require Import Logic.ModalLogic.Syntax.
Require Import Logic.MinimunLogic.ProofTheory.Minimun.
Require Import Logic.PropositionalLogic.ProofTheory.Intuitionistic.
Require Import Logic.PropositionalLogic.ProofTheory.Classical.
Require Import Logic.ModalLogic.ProofTheory.ModalLogic.
Require Import Logic.ModalLogic.Model.KripkeModel.
Require Import Logic.ModalLogic.Semantics.Kripke.
Require Import Logic.ModalLogic.Sound.Sound_Kripke.
Require Import Logic.GeneralLogic.ShallowEmbedded.PredicateAsLang.
Require Import Logic.PropositionalLogic.ShallowEmbedded.PredicatePropositionalLogic.

Instance Pred_mL (A: Type) {R: KM.Relation A}: ModalLanguage (Pred_L A) :=
  Build_ModalLanguage (Pred_L A) Semantics.boxp.

Instance Pred_kmSM (A: Type) {R: KM.Relation A}: @KripkeModalSemantics (Pred_L A) (Pred_minL A) (Pred_mL A) (Build_Model A) (unit_kMD _) tt R (Pred_SM A).
Proof.
(* Goal: @SystemK (Pred_L A) (Pred_minL A) (Pred_pL A) (@Pred_mL A R) (Pred_Gamma A) (Pred_minAX A) (Pred_ipGamma A) *)
  constructor.
(* Goal: forall x : @expr (Pred_L A), Same_set (@Kworlds (Build_Model A) (unit_kMD (Build_Model A)) tt) (@Kdenotation (Pred_L A) (Build_Model A) (unit_kMD (Build_Model A)) tt (Pred_SM A) (@boxp (Pred_L A) (@Pred_mL A R) x)) (@Semantics.boxp (@Kworlds (Build_Model A) (unit_kMD (Build_Model A)) tt) R (@Kdenotation (Pred_L A) (Build_Model A) (unit_kMD (Build_Model A)) tt (Pred_SM A) x)) *)
  intros; apply Same_set_refl.
Qed.

Instance Pred_KmGamma (A: Type) {R: KM.Relation A}: SystemK (Pred_L A) (Pred_Gamma A).
Proof.
(* Goal: @SystemK (Pred_L A) (Pred_minL A) (Pred_pL A) (@Pred_mL A R) (Pred_Gamma A) (Pred_minAX A) (Pred_ipGamma A) *)
  constructor.
  + intros x y.
(* Goal: @provable (Pred_L A) (Pred_Gamma A) (@impp (Pred_L A) (Pred_minL A) (@boxp (Pred_L A) (@Pred_mL A R) (@impp (Pred_L A) (Pred_minL A) x y)) (@impp (Pred_L A) (Pred_minL A) (@boxp (Pred_L A) (@Pred_mL A R) x) (@boxp (Pred_L A) (@Pred_mL A R) y))) *)
    exact (@sound_axiom_K (Pred_L A) _ _ (Build_Model A) (unit_kMD _) tt R (Pred_SM A) (Pred_tminSM A) (Pred_kmSM A) x y).
  + intros x.
(* Goal: forall _ : @provable (Pred_L A) (Pred_Gamma A) x, @provable (Pred_L A) (Pred_Gamma A) (@boxp (Pred_L A) (@Pred_mL A R) x) *)
    exact (@sound_rule_N (Pred_L A) _ _ (Build_Model A) (unit_kMD _) tt R (Pred_SM A) (Pred_kmSM A) x).
Qed.
