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.

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

Module Semantics.

Definition impp {worlds: Type} {R: Relation worlds} (X: Ensemble worlds) (Y: Ensemble worlds): Ensemble worlds :=
  fun m => forall n, m <= n -> X n -> Y n.

Lemma impp_closed {worlds: Type} {R: Relation worlds} {po_R: PreOrder Krelation}:
  forall (X: Ensemble worlds) (Y: Ensemble worlds),
    upwards_closed_Kdenote X ->
    upwards_closed_Kdenote Y ->
    upwards_closed_Kdenote (impp X Y).
Proof.
(* Goal: forall (X Y : Ensemble worlds) (_ : @upwards_closed_Kdenote worlds R X) (_ : @upwards_closed_Kdenote worlds R Y), @upwards_closed_Kdenote worlds R (@impp worlds R X Y) *)
  intros.
(* Goal: forall (X Y : Ensemble worlds) (_ : @upwards_closed_Kdenote worlds R X) (_ : @upwards_closed_Kdenote worlds R Y), @upwards_closed_Kdenote worlds R (@impp worlds R X Y) *)
  hnf; intros.
(* Goal: @impp worlds R X Y m *)
  hnf in H2 |- *.
(* Goal: forall (n : worlds) (_ : @Krelation worlds R m n) (_ : X n), Y n *)
  intros ? ?; apply H2.
(* Goal: @Krelation worlds R n n0 *)
  etransitivity; eauto.
Qed.

End Semantics.

Module SemanticsMono.

Program Definition impp {worlds: Type} {R: Relation worlds} {po_R: PreOrder Krelation} (X Y: MonoEnsemble worlds): MonoEnsemble worlds :=
  Semantics.impp X Y.
Next Obligation.
  apply (@Semantics.impp_closed worlds R po_R);
  apply (proj2_sig _).
Defined.

End SemanticsMono.

Class KripkeMinimunSemantics (L: Language) {minL: MinimunLanguage L} (MD: Model) {kMD: KripkeModel MD} (M: Kmodel) {R: Relation (Kworlds M)} (SM: Semantics L MD) : Type := {
  denote_impp: forall x y, Same_set _ (Kdenotation M (x --> y)) (Semantics.impp (Kdenotation M x) (Kdenotation M y))
}.

Lemma sat_impp {L: Language} {minL: MinimunLanguage L} {MD: Model} {kMD: KripkeModel MD} {M: Kmodel} {R: Relation (Kworlds M)} {SM: Semantics L MD} {kminSM: KripkeMinimunSemantics L MD M SM}: forall m x y, KRIPKE: M , m |= x --> y <-> (forall n, m <= n -> KRIPKE: M , n |= x -> KRIPKE: M , n |= y).
Proof.
(* Goal: forall (m : @Kworlds MD kMD M) (x y : @expr L), iff (@satisfies L MD SM (@build_model MD kMD M m) (@impp L minL x y)) (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) y) *)
  intros; simpl.
(* Goal: iff (@satisfies L MD SM (@build_model MD kMD M m) (@impp L minL x y)) (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) y) *)
  unfold satisfies.
(* Goal: iff (@denotation L MD SM (@impp L minL x y) (@build_model MD kMD M m)) (forall (n : @Kworlds MD kMD M) (_ : @Krelation (@Kworlds MD kMD M) R m n) (_ : @denotation L MD SM x (@build_model MD kMD M n)), @denotation L MD SM y (@build_model MD kMD M n)) *)
  destruct (denote_impp x y).
(* Goal: iff (@denotation L MD SM (@impp L minL x y) (@build_model MD kMD M m)) (forall (n : @Kworlds MD kMD M) (_ : @Krelation (@Kworlds MD kMD M) R m n) (_ : @denotation L MD SM x (@build_model MD kMD M n)), @denotation L MD SM y (@build_model MD kMD M n)) *)
  split; [apply H | apply H0].
Qed.

