Require Import Coq.Sets.Ensembles.
Require Import Coq.Logic.Classical_Prop.
Require Import Coq.Logic.ChoiceFacts.
Require Import Coq.Logic.ClassicalChoice.
Require Export Coq.Classes.RelationClasses.
Require Import Coq.Relations.Relations.
Require Export Coq.Classes.Morphisms.
Require Export Logic.lib.Relation_ext.
Require Export Logic.lib.RelationPairs_ext.

Module KI.

Class Relation (worlds: Type): Type :=
  Krelation: worlds -> Ensemble worlds (* <= *).

End KI.

Export KI.

Module KripkeModelNotation_Intuitionistic.

Infix "<=" := Krelation: kripke_model.

End KripkeModelNotation_Intuitionistic.

Import KripkeModelNotation_Intuitionistic.

Local Open Scope kripke_model.

Definition upwards_closed_Kdenote {worlds: Type} {R: Relation worlds} (d: Ensemble worlds): Prop :=
  forall n m, n <= m -> d n -> d m.

Definition Krelation_stable_Kdenote {worlds: Type} {R: Relation worlds} (d: Ensemble worlds): Prop :=
  forall w1 w2, w1 <= w2 -> (d w1 <-> d w2).

Definition MonoEnsemble (A: Type) {R: Relation A}: Type := @sig (_ -> Prop) (@upwards_closed_Kdenote A R).

Class IdentityKripkeIntuitionisticModel (worlds: Type) {R: Relation worlds} : Prop := {
  Korder_identity: forall m n: worlds, m <= n -> m = n
}.

Class NoBranchKripkeIntuitionisticModel (worlds: Type) {R: Relation worlds} : Prop := {
  Korder_no_branch: forall m1 m2 n: worlds, n <= m1 -> n <= m2 -> m1 <= m2 \/ m2 <= m1
}.

Class BranchJoinKripkeIntuitionisticModel (worlds: Type) {R: Relation worlds} : Prop := {
  Korder_branch_join: forall m1 m2 n: worlds, n <= m1 -> n <= m2 -> exists m, m1 <= m /\ m2 <= m
}.

Instance prod_BranchJoinKripkeIntuitionisticModel (A B: Type) {RA: Relation A} {RB: Relation B} {bkiMA: BranchJoinKripkeIntuitionisticModel A} {bkiMB: BranchJoinKripkeIntuitionisticModel B}: @BranchJoinKripkeIntuitionisticModel (A * B) (RelProd RA RB).
Proof.
(* Goal: @IdentityKripkeIntuitionisticModel worlds (@eq worlds) *)
  constructor.
(* Goal: forall (m1 m2 n : prod A B) (_ : @Krelation (prod A B) (@RelProd A B RA RB) n m1) (_ : @Krelation (prod A B) (@RelProd A B RA RB) n m2), @ex (prod A B) (fun m : prod A B => and (@Krelation (prod A B) (@RelProd A B RA RB) m1 m) (@Krelation (prod A B) (@RelProd A B RA RB) m2 m)) *)
  intros [m11 m12] [m21 m22] [n1 n2] [? ?] [? ?].
(* Goal: @ex (prod A B) (fun m : prod A B => and (@Krelation (prod A B) (@RelProd A B RA RB) (@pair A B m11 m12) m) (@Krelation (prod A B) (@RelProd A B RA RB) (@pair A B m21 m22) m)) *)
  hnf in H, H0, H1, H2; simpl in *.
(* Goal: @ex (prod A B) (fun m : prod A B => and (@Krelation (prod A B) (@RelProd A B RA RB) (@pair A B m11 m12) m) (@Krelation (prod A B) (@RelProd A B RA RB) (@pair A B m21 m22) m)) *)
  destruct (@Korder_branch_join _ _ bkiMA m11 m21 n1 H H1) as [m1 [? ?]].
(* Goal: @ex (prod A B) (fun m : prod A B => and (@Krelation (prod A B) (@RelProd A B RA RB) (@pair A B m11 m12) m) (@Krelation (prod A B) (@RelProd A B RA RB) (@pair A B m21 m22) m)) *)
  destruct (@Korder_branch_join _ _ bkiMB m12 m22 n2 H0 H2) as [m2 [? ?]].
(* Goal: @ex (prod A B) (fun m : prod A B => and (@Krelation (prod A B) (@RelProd A B RA RB) (@pair A B m11 m12) m) (@Krelation (prod A B) (@RelProd A B RA RB) (@pair A B m21 m22) m)) *)
  exists (m1, m2); split; split; auto.
Qed.

Instance fun_BranchJoinKripkeIntuitionisticModel (A B: Type) {RB: Relation B} {bkiMB: BranchJoinKripkeIntuitionisticModel B}: @BranchJoinKripkeIntuitionisticModel (A -> B) (pointwise_relation A RB).
Proof.
(* Goal: @IdentityKripkeIntuitionisticModel worlds (@eq worlds) *)
  constructor.
(* Goal: forall (m1 m2 n : A) (_ : @Krelation A R n m1) (_ : @Krelation A R n m2), @ex A (fun m : A => and (@Krelation A R m1 m) (@Krelation A R m2 m)) *)
  intros.
(* Goal: @ex (forall _ : A, B) (fun m : forall _ : A, B => and (@Krelation (forall _ : A, B) (@pointwise_relation A B RB) m1 m) (@Krelation (forall _ : A, B) (@pointwise_relation A B RB) m2 m)) *)
  destruct (choice (fun x fx => m1 x <= fx /\ m2 x <= fx)) as [m ?].
(* Goal: forall (m1 m2 n : A) (_ : @Krelation A R n m1) (_ : @Krelation A R n m2), @ex A (fun m : A => and (@Krelation A R m1 m) (@Krelation A R m2 m)) *)
  + intros.
(* Goal: @ex B (fun y : B => and (@Krelation B RB (m1 x) y) (@Krelation B RB (m2 x) y)) *)
    specialize (H x).
(* Goal: @ex B (fun y : B => and (@Krelation B RB (m1 x) y) (@Krelation B RB (m2 x) y)) *)
    specialize (H0 x).
(* Goal: @ex B (fun y : B => and (@Krelation B RB (m1 x) y) (@Krelation B RB (m2 x) y)) *)
    destruct (Korder_branch_join _ _ _ H H0) as [y [? ?]].
(* Goal: @ex B (fun y : B => and (@Krelation B RB (m1 x) y) (@Krelation B RB (m2 x) y)) *)
    exists y; auto.
  + exists m.
(* Goal: and (@Krelation (forall _ : A, B) (@pointwise_relation A B RB) m1 m) (@Krelation (forall _ : A, B) (@pointwise_relation A B RB) m2 m) *)
    split; intros x; specialize (H1 x); tauto.
Qed.

Instance option00_BranchJoinKripkeIntuitionisticModel (A: Type) {R: Relation A} {bkiM: BranchJoinKripkeIntuitionisticModel A}: @BranchJoinKripkeIntuitionisticModel (option A) (option00_relation R).
Proof.
(* Goal: @IdentityKripkeIntuitionisticModel worlds (@eq worlds) *)
  constructor.
(* Goal: forall (m1 m2 n : A) (_ : @Krelation A R n m1) (_ : @Krelation A R n m2), @ex A (fun m : A => and (@Krelation A R m1 m) (@Krelation A R m2 m)) *)
  intros.
(* Goal: @ex (option A) (fun m : option A => and (@Krelation (option A) (@option00_relation A R) m1 m) (@Krelation (option A) (@option00_relation A R) m2 m)) *)
  inversion H; inversion H0; try congruence; subst.
  + exists None; split; auto.
  + inversion H5; subst.
(* Goal: @ex (option A) (fun m : option A => and (@Krelation (option A) (@option00_relation A R) (@Some A b) m) (@Krelation (option A) (@option00_relation A R) (@Some A b0) m)) *)
    clear H0 H H5.
(* Goal: @ex (option A) (fun m : option A => and (@Krelation (option A) (@option00_relation A R) (@Some A b) m) (@Krelation (option A) (@option00_relation A R) (@Some A b0) m)) *)
    destruct (Korder_branch_join _ _ _ H1 H4) as [b' [? ?]].
(* Goal: @ex (option A) (fun m : option A => and (@Krelation (option A) (@option00_relation A R) (@Some A b) m) (@Krelation (option A) (@option00_relation A R) (@Some A b0) m)) *)
    exists (Some b').
(* Goal: and (@Krelation (option A) (@option00_relation A R) (@Some A b) (@Some A b')) (@Krelation (option A) (@option00_relation A R) (@Some A b0) (@Some A b')) *)
    split; constructor; auto.
Qed.

Instance NoBranch2BranchJoin (A: Type) {R: Relation A} {po_R: PreOrder Krelation} {nkiM: NoBranchKripkeIntuitionisticModel A}: BranchJoinKripkeIntuitionisticModel A.
Proof.
(* Goal: @IdentityKripkeIntuitionisticModel worlds (@eq worlds) *)
  constructor.
(* Goal: forall (m1 m2 n : A) (_ : @Krelation A R n m1) (_ : @Krelation A R n m2), @ex A (fun m : A => and (@Krelation A R m1 m) (@Krelation A R m2 m)) *)
  intros.
(* Goal: @ex A (fun m : A => and (@Krelation A R m1 m) (@Krelation A R m2 m)) *)
  pose proof Korder_no_branch _ _ _ H H0.
(* Goal: @ex A (fun m : A => and (@Krelation A R m1 m) (@Krelation A R m2 m)) *)
  destruct H1.
  + exists m2; split; auto.
(* Goal: @Krelation A R m1 m1 *)
    reflexivity.
  + exists m1; split; auto.
(* Goal: @Krelation A R m1 m1 *)
    reflexivity.
Qed.

Instance eq_ikiM {worlds: Type}: @IdentityKripkeIntuitionisticModel worlds eq.
Proof.
(* Goal: @IdentityKripkeIntuitionisticModel worlds (@eq worlds) *)
  constructor.
(* Goal: forall (m n : worlds) (_ : @Krelation worlds (@eq worlds) m n), @eq worlds m n *)
  intros; auto.
Qed.

