Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Logic.Classical_Prop.
Require Import Coq.Logic.Classical_Pred_Type.
Require Import Logic.lib.Bijection.
Require Import Logic.lib.Countable.
Require Import Logic.GeneralLogic.Base.
Require Import Logic.GeneralLogic.KripkeModel.
Require Import Logic.GeneralLogic.ProofTheory.BasicSequentCalculus.
Require Import Logic.GeneralLogic.Semantics.Kripke.
Require Import Logic.GeneralLogic.Complete.ContextProperty_Kripke.

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

Section Canonical.

Context {L: Language}
        {Gamma: ProofTheory L}
        {bSC: BasicSequentCalculus L Gamma}
        {MD: Model}
        {kMD: KripkeModel MD}
        {M: Kmodel}
        {R: Relation (Kworlds M)}
        {SM: Semantics L MD}.

Context (cP: context -> Prop)
        (rel: bijection (Kworlds M) (sig cP)).

Hypothesis H_R: forall m n Phi Psi, rel m Phi -> rel n Psi -> (m <= n <-> Included _ (proj1_sig Phi) (proj1_sig Psi)).

Lemma denote_monotonic (x: expr):
  (forall m Phi, rel m Phi -> (KRIPKE: M, m |= x <-> proj1_sig Phi x)) ->
  upwards_closed_Kdenote (Kdenotation M x).
Proof.
(* Goal: forall _ : forall (m : @Kworlds MD kMD M) (Phi : @sig (@context L) cP) (_ : bij_R (@Kworlds MD kMD M) (@sig (@context L) cP) rel m Phi), iff (@satisfies L MD SM (@build_model MD kMD M m) x) (@proj1_sig (@context L) cP Phi x), @upwards_closed_Kdenote (@Kworlds MD kMD M) R (@Kdenotation L MD kMD M SM x) *)
  intros.
(* Goal: forall _ : forall (m : @Kworlds MD kMD M) (Phi : @sig (@context L) cP) (_ : bij_R (@Kworlds MD kMD M) (@sig (@context L) cP) rel m Phi), iff (@satisfies L MD SM (@build_model MD kMD M m) x) (@proj1_sig (@context L) cP Phi x), @upwards_closed_Kdenote (@Kworlds MD kMD M) R (@Kdenotation L MD kMD M SM x) *)
  hnf; intros.
(* Goal: @Kdenotation L MD kMD M SM x m *)
  change (KRIPKE: M, m |= x).
(* Goal: @satisfies L MD SM (@build_model MD kMD M m) x *)
  change (KRIPKE: M, n |= x) in H1.
(* Goal: @satisfies L MD SM (@build_model MD kMD M m) x *)
  destruct (im_bij _ _ rel n) as [Phi ?].
(* Goal: @satisfies L MD SM (@build_model MD kMD M m) x *)
  destruct (im_bij _ _ rel m) as [Psi ?].
(* Goal: @satisfies L MD SM (@build_model MD kMD M m) x *)
  erewrite H in H1 |- * by eauto.
(* Goal: @proj1_sig (@context L) cP Psi x *)
  eapply H_R in H0; eauto.
(* Goal: @proj1_sig (@context L) cP Psi x *)
  apply H0; auto.
Qed.

Instance po_R: PreOrder (@KI.Krelation _ R).
Proof.
(* Goal: @PreOrder (@Kworlds MD kMD M) (@Krelation (@Kworlds MD kMD M) R) *)
  constructor.
  + hnf; intros m.
(* Goal: @Krelation (@Kworlds MD kMD M) R m m *)
    destruct (im_bij _ _ rel m) as [Phi ?].
(* Goal: @Krelation (@Kworlds MD kMD M) R m m *)
    apply (H_R _ _ _ _ H H).
(* Goal: Included (@expr L) (@proj1_sig (@context L) cP Phi) (@proj1_sig (@context L) cP Phi) *)
    hnf; intros; auto.
  + hnf; intros m1 m2 m3.
(* Goal: forall (_ : @Krelation (@Kworlds MD kMD M) R m1 m2) (_ : @Krelation (@Kworlds MD kMD M) R m2 m3), @Krelation (@Kworlds MD kMD M) R m1 m3 *)
    destruct (im_bij _ _ rel m1) as [Phi1 ?].
(* Goal: forall (_ : @Krelation (@Kworlds MD kMD M) R m1 m2) (_ : @Krelation (@Kworlds MD kMD M) R m2 m3), @Krelation (@Kworlds MD kMD M) R m1 m3 *)
    destruct (im_bij _ _ rel m2) as [Phi2 ?].
(* Goal: forall (_ : @Krelation (@Kworlds MD kMD M) R m1 m2) (_ : @Krelation (@Kworlds MD kMD M) R m2 m3), @Krelation (@Kworlds MD kMD M) R m1 m3 *)
    destruct (im_bij _ _ rel m3) as [Phi3 ?].
(* Goal: forall (_ : @Krelation (@Kworlds MD kMD M) R m1 m2) (_ : @Krelation (@Kworlds MD kMD M) R m2 m3), @Krelation (@Kworlds MD kMD M) R m1 m3 *)
    rewrite (H_R _ _ _ _ H H0).
(* Goal: forall (_ : Included (@expr L) (@proj1_sig (@context L) cP Phi1) (@proj1_sig (@context L) cP Phi2)) (_ : @Krelation (@Kworlds MD kMD M) R m2 m3), @Krelation (@Kworlds MD kMD M) R m1 m3 *)
    rewrite (H_R _ _ _ _ H0 H1).
(* Goal: forall (_ : Included (@expr L) (@proj1_sig (@context L) cP Phi1) (@proj1_sig (@context L) cP Phi2)) (_ : Included (@expr L) (@proj1_sig (@context L) cP Phi2) (@proj1_sig (@context L) cP Phi3)), @Krelation (@Kworlds MD kMD M) R m1 m3 *)
    rewrite (H_R _ _ _ _ H H1).
(* Goal: forall (_ : Included (@expr L) (@proj1_sig (@context L) cP Phi1) (@proj1_sig (@context L) cP Phi2)) (_ : Included (@expr L) (@proj1_sig (@context L) cP Phi2) (@proj1_sig (@context L) cP Phi3)), Included (@expr L) (@proj1_sig (@context L) cP Phi1) (@proj1_sig (@context L) cP Phi3) *)
    clear; unfold Included, Ensembles.In; firstorder.
Qed.

End Canonical.
