Require Import Coq.Logic.Classical_Prop.
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Relations.Relation_Definitions.
Require Import Logic.lib.Ensembles_ext.
Require Import Logic.GeneralLogic.Base.
Require Import Logic.GeneralLogic.KripkeModel.
Require Import Logic.MinimunLogic.Syntax.
Require Logic.MinimunLogic.Semantics.Kripke.
Require Logic.MinimunLogic.Semantics.Trivial.

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

Section SemanticEquiv.

Context {L: Language}
        {minL: MinimunLanguage L}
        {MD: Model}
        {SM: Semantics L MD}.

Lemma eqR_KripkeIntuitionistic: @Kripke.KripkeIntuitionisticSemantics L MD (unit_kMD _) tt eq SM.
Proof.
(* Goal: @Kripke.KripkeMinimunSemantics L minL MD (unit_kMD MD) tt (@eq (@Kworlds MD (unit_kMD MD) tt)) SM *)
  constructor.
(* Goal: forall x : @expr L, @upwards_closed_Kdenote (@Kworlds MD (unit_kMD MD) tt) (@eq (@Kworlds MD (unit_kMD MD) tt)) (@Kdenotation L MD (unit_kMD MD) tt SM x) *)
  intros; hnf; intros.
(* Goal: @Kdenotation L MD (unit_kMD MD) tt SM x m *)
  hnf in H; subst.
(* Goal: @Kdenotation L MD (unit_kMD MD) tt SM x m *)
  auto.
Qed.

Lemma Trivial2Kripke {tpSM: Trivial.TrivialMinimunSemantics L MD SM}: 
  @Kripke.KripkeMinimunSemantics L minL MD (unit_kMD _) tt eq SM.
Proof.
(* Goal: @Kripke.KripkeMinimunSemantics L minL MD (unit_kMD MD) tt (@eq (@Kworlds MD (unit_kMD MD) tt)) SM *)
  constructor.
(* Goal: forall x y : @expr L, Same_set (@Kworlds MD (unit_kMD MD) tt) (@Kdenotation L MD (unit_kMD MD) tt SM (@impp L minL x y)) (@Kripke.Semantics.impp (@Kworlds MD (unit_kMD MD) tt) (@eq (@Kworlds MD (unit_kMD MD) tt)) (@Kdenotation L MD (unit_kMD MD) tt SM x) (@Kdenotation L MD (unit_kMD MD) tt SM y)) *)
  + intros.
(* Goal: Same_set (@Kworlds MD (unit_kMD MD) tt) (@Kdenotation L MD (unit_kMD MD) tt SM (@impp L minL x y)) (@Kripke.Semantics.impp (@Kworlds MD (unit_kMD MD) tt) (@eq (@Kworlds MD (unit_kMD MD) tt)) (@Kdenotation L MD (unit_kMD MD) tt SM x) (@Kdenotation L MD (unit_kMD MD) tt SM y)) *)
    change (@Kdenotation L MD (unit_kMD _) tt SM) with denotation.
(* Goal: Same_set (@Kworlds MD (unit_kMD MD) tt) (@denotation L MD SM (@impp L minL x y)) (@Kripke.Semantics.impp (@Kworlds MD (unit_kMD MD) tt) (@eq (@Kworlds MD (unit_kMD MD) tt)) (@denotation L MD SM x) (@denotation L MD SM y)) *)
    rewrite Trivial.denote_impp.
(* Goal: forall x y : @expr L, Same_set (@Kworlds MD (unit_kMD MD) tt) (@Kdenotation L MD (unit_kMD MD) tt SM (@impp L minL x y)) (@Kripke.Semantics.impp (@Kworlds MD (unit_kMD MD) tt) (@eq (@Kworlds MD (unit_kMD MD) tt)) (@Kdenotation L MD (unit_kMD MD) tt SM x) (@Kdenotation L MD (unit_kMD MD) tt SM y)) *)
    split; unfold Included, Ensembles.In; intros.
(* Goal: forall x y : @expr L, Same_set (@Kworlds MD (unit_kMD MD) tt) (@Kdenotation L MD (unit_kMD MD) tt SM (@impp L minL x y)) (@Kripke.Semantics.impp (@Kworlds MD (unit_kMD MD) tt) (@eq (@Kworlds MD (unit_kMD MD) tt)) (@Kdenotation L MD (unit_kMD MD) tt SM x) (@Kdenotation L MD (unit_kMD MD) tt SM y)) *)
    - hnf; intros.
(* Goal: @denotation L MD SM y n *)
      hnf in H0; subst.
(* Goal: @denotation L MD SM y n *)
      apply H, H1.
(* Goal: @Kdenotation L MD (unit_kMD MD) tt SM x m *)
    - hnf; intros; apply (H x0); auto.
(* Goal: @Krelation (@Kworlds MD (unit_kMD MD) tt) (@eq (@Kworlds MD (unit_kMD MD) tt)) x0 x0 *)
      reflexivity.
Qed.

End SemanticEquiv.
