Require Import Logic.GeneralLogic.KripkeModel.
Require Import Logic.ModalLogic.Model.KripkeModel.

Local Open Scope kripke_model.
Import KripkeModelNotation_Intuitionistic.

Class UpwardsClosedOrderedKripkeModel (worlds: Type) {R1: KI.Relation worlds} {R2: KM.Relation worlds} := {
  KM_relation_up: forall m m' n', m <= m' -> KM.Krelation m' n' -> exists n, n <= n' /\ KM.Krelation m n
}.

(* Generator *)

Instance prod_ukmM {A B: Type} (RA1: KI.Relation A) (RB1: KI.Relation B) (RA2: KM.Relation A) (RB2: KM.Relation B) {ukmM_A: UpwardsClosedOrderedKripkeModel A} {ukmM_B: UpwardsClosedOrderedKripkeModel B}: @UpwardsClosedOrderedKripkeModel (A * B) (RelProd RA1 RB1) (RelProd RA2 RB2).
Proof.
(* Goal: @UpwardsClosedOrderedKripkeModel (prod A B) (@RelProd A B RA1 RB1) (@RelProd A B RA2 RB2) *)
  constructor.
(* Goal: forall (m m' n' : prod A B) (_ : @KI.Krelation (prod A B) (@RelProd A B RA1 RB1) m m') (_ : @Krelation (prod A B) (@RelProd A B RA2 RB2) m' n'), @ex (prod A B) (fun n : prod A B => and (@KI.Krelation (prod A B) (@RelProd A B RA1 RB1) n n') (@Krelation (prod A B) (@RelProd A B RA2 RB2) m n)) *)
  intros [m1 m2] [m1' m2'] [n1 n2] [? ?] [? ?].
(* Goal: @ex (prod A B) (fun n : prod A B => and (@KI.Krelation (prod A B) (@RelProd A B RA1 RB1) n (@pair A B n1 n2)) (@Krelation (prod A B) (@RelProd A B RA2 RB2) (@pair A B m1 m2) n)) *)
  hnf in H, H0, H1, H2; simpl in *.
(* Goal: @ex (prod A B) (fun n : prod A B => and (@KI.Krelation (prod A B) (@RelProd A B RA1 RB1) n (@pair A B n1 n2)) (@Krelation (prod A B) (@RelProd A B RA2 RB2) (@pair A B m1 m2) n)) *)
  destruct (KM_relation_up _ _ _ H H1) as [n1' [? ?]].
(* Goal: @ex (prod A B) (fun n : prod A B => and (@KI.Krelation (prod A B) (@RelProd A B RA1 RB1) n (@pair A B n1 n2)) (@Krelation (prod A B) (@RelProd A B RA2 RB2) (@pair A B m1 m2) n)) *)
  destruct (KM_relation_up _ _ _ H0 H2) as [n2' [? ?]].
(* Goal: @ex (prod A B) (fun n : prod A B => and (@KI.Krelation (prod A B) (@RelProd A B RA1 RB1) n (@pair A B n1 n2)) (@Krelation (prod A B) (@RelProd A B RA2 RB2) (@pair A B m1 m2) n)) *)
  exists (n1', n2').
(* Goal: and (@KI.Krelation (prod A B) (@RelProd A B RA1 RB1) (@pair A B n1' n2') (@pair A B n1 n2)) (@Krelation (prod A B) (@RelProd A B RA2 RB2) (@pair A B m1 m2) (@pair A B n1' n2')) *)
  split; split; auto.
Qed.

Instance eq1_ukmM (worlds: Type) {R: KM.Relation worlds}: @UpwardsClosedOrderedKripkeModel worlds eq R.
Proof.
(* Goal: @UpwardsClosedOrderedKripkeModel worlds R (@eq worlds) *)
  constructor; intros.
(* Goal: @ex worlds (fun n : worlds => and (@KI.Krelation worlds (@eq worlds) n n') (@Krelation worlds R m n)) *)
  exists n'; simpl in *.
(* Goal: and (@KI.Krelation worlds R m n') (@Krelation worlds (@eq worlds) m m) *)
  split.
  + reflexivity.
  + hnf in H; subst; auto.
Qed.

Instance eq2_ukmM (worlds: Type) {R: KI.Relation worlds}: @UpwardsClosedOrderedKripkeModel worlds R eq.
Proof.
(* Goal: @UpwardsClosedOrderedKripkeModel worlds R (@eq worlds) *)
  constructor; intros.
(* Goal: @ex worlds (fun n : worlds => and (@KI.Krelation worlds R n n') (@Krelation worlds (@eq worlds) m n)) *)
  exists m; simpl in *.
(* Goal: and (@KI.Krelation worlds R m n') (@Krelation worlds (@eq worlds) m m) *)
  split.
  + hnf in H0; subst; auto.
  + reflexivity.
Qed.
