iS4_GG_translation

Require Import Arith.
Require Import Lia.
Require Import Ensembles.
Require Import Init.Wf.

Require Import iS4_Syntax.
Require Import iS4H_export.
Require Import iS4_topol_export.

Section Failure_of_GG.

(* We could hope that iS4 validates the GG translation thanks to
    the following. *)


Lemma DNE_Box_Bot Γ : iS4H_prv (Γ, (¬ (Box Bot))) --> Box Bot).
Proof.
apply Strong_Completeness. intros M x .
intros y Rxy Hy.
intros u Hu.
exfalso. simpl in *.
apply Hy with y.
- apply reach_refl.
- intros. pose ( u Hu).
  pose (Hu v). apply i.
  unfold uset in *. apply i_T ; auto.
Qed.


(* But it does not. To show this, we create an interior
    preorder model with three points A, B and C such
    that A forces ¬ ¬ Box 0, but does not force Box ¬ ¬ 0. *)


(* We first construct the model. *)

Inductive ABC : Type :=
 | A : ABC
 | B : ABC
 | C : ABC.

Definition ABCreach (n m : ABC) : Prop :=
  match n with
   | A match m with
                   | A True
                   | B True
                   | C False
                  end
   | B match m with
                   | A False
                   | B True
                   | C False
                  end
   | C match m with
                   | A False
                   | B False
                   | C True
                  end
  end.

Lemma ABCreach_refl : n, ABCreach n n.
Proof.
intros. destruct n ; unfold ABCreach ; auto.
Qed.


Lemma ABCreach_trans : n m k, (ABCreach n m) (ABCreach m k) (ABCreach n k).
Proof.
intros. unfold ABCreach in * ; destruct n ; auto ; destruct m ; auto ; destruct k ; auto.
Qed.


(* We can create a preord_set of the following form (omitting reflexive arrows): 

                               (A) ==ABCreach==> (B)

                                (C)

    So, B can be reached by A, and C is an isolated point. *)


Instance P : preord_set :=
      {|
        nodes := ABC ;
        reachable := ABCreach ;
        reach_refl u := ABCreach_refl u ;
        reach_tran u v w := @ABCreach_trans u v w
      |}.

(* We manually define some upsets in P (the canonical ones). *)

  Lemma ABC_is_upset : w, ((Triple _ A B C) w)
             y, reachable w y ((Triple _ A B C) y).
  Proof.
  intros. destruct y ; firstorder.
  Qed.


  Instance ABC_upset : upset P :=
      {|
        uset := Triple _ A B C;
        is_upset := ABC_is_upset
      |}.

  Lemma AB_is_upset : w, ((Couple _ A B) w)
             y, reachable w y ((Couple _ A B) y).
  Proof.
  intros. inversion H ; simpl in * ; unfold reachable in ; destruct y ; subst ; firstorder.
  Qed.


  Instance AB_upset : upset P :=
      {|
        uset := Couple _ A B;
        is_upset := AB_is_upset
      |}.

  Lemma BC_is_upset : w, ((Couple _ B C) w)
             y, reachable w y ((Couple _ B C) y).
  Proof.
  intros. inversion H ; simpl in * ; unfold reachable in ; destruct y ; subst ; firstorder.
  Qed.


  Instance BC_upset : upset P :=
      {|
        uset := Couple _ B C;
        is_upset := BC_is_upset
      |}.

  Lemma B_is_upset : w, ((Singleton _ B) w)
             y, reachable w y ((Singleton _ B) y).
  Proof.
  intros. inversion H ; simpl in * ; unfold reachable in ; destruct y ; subst ; firstorder.
  Qed.


  Instance B_upset : upset P :=
      {|
        uset := Singleton _ B;
        is_upset := B_is_upset
      |}.

  Lemma C_is_upset : w, ((Singleton _ C) w)
             y, reachable w y ((Singleton _ C) y).
  Proof.
  intros. inversion H ; simpl in * ; unfold reachable in ; destruct y ; subst ; firstorder.
  Qed.


  Instance C_upset : upset P :=
      {|
        uset := Singleton _ C;
        is_upset := C_is_upset
      |}.

  Lemma Empty_is_upset : w, ((Empty_set _) w)
             y, reachable w y ((Empty_set _) y).
  Proof.
  intros. inversion H.
  Qed.


  Instance Empty_upset : upset P :=
      {|
        uset := Empty_set _;
        is_upset := Empty_is_upset
      |}.

(* Then we turn to the definition of our interior operator. *)

Definition i_P : (upset P) (upset P).
Proof.
intro. destruct X.
exists (fun x
  ((uset A uset B uset C)) (* For {A,B,C} *)
  (uset A uset B ( (uset C)) x = B) (* For {A,B} *)
  ( (uset A) uset B (uset C) x = B) (* For {B} *)
  (( (uset A)) ( (uset B)) uset C x = C) (* For {C} *)
  (( (uset A)) uset B uset C (x = B x = C)) (* For {B,C} *)
).
intros D . destruct as [ | [ | [ | [ | ]]]] ;
intros E reachDE.
destruct as ( & & ) ; auto.
all: destruct as ( & & & ) ; unfold reachable in reachDE ; subst.
- right ; left ; repeat split ; auto. destruct E ; auto ; subst ; try contradiction.
- right ; right ; left ; repeat split ; auto. destruct E ; auto ; subst ; try contradiction.
- right ; right ; right ; left ; repeat split ; auto. destruct E ; auto ; subst ; try contradiction.
- right ; right ; right ; right ; repeat split ; auto. destruct ; subst ; auto ; destruct E ; auto ; subst ; try contradiction.
Defined.


(* The next lemma shows that upset in our preord_set have a canonical representation. Note that in the
    proof of it, we use LEM: as Ensembles are functions to Prop in Coq, and thus our upsets are defined over
    these functions, to prove that two functions are equal we can assume LEM. We could get rid of this feature
    by requiring that our semantics accepts only upsets which are decidable. *)


Lemma canonical_form_upset_P : (u : upset P), (@uset _ u = Triple _ A B C)
                                                                                      (@uset _ u = Couple _ A B)
                                                                                      (@uset _ u = Couple _ B C)
                                                                                      (@uset _ u = Singleton _ B)
                                                                                      (@uset _ u = Singleton _ C)
                                                                                      (@uset _ u = Empty_set _).
Proof.
intros. destruct u. simpl in *.
destruct (LEM (uset A)).
- destruct (LEM (uset C)).
  + left. apply Extensionality_Ensembles. split ; intros D HD ; auto.
     destruct D ; firstorder. inversion HD ; firstorder.
  + right. left. apply Extensionality_Ensembles. split ; intros D HD ; auto.
     destruct D ; firstorder. inversion HD ; firstorder.
- destruct (LEM (uset B)).
  + destruct (LEM (uset C)).
    * right. right. left. apply Extensionality_Ensembles. split ; intros D HD ; auto.
      destruct D ; firstorder. inversion HD ; firstorder.
    * right. right. right. left. apply Extensionality_Ensembles. split ; intros D HD ; auto.
      destruct D ; firstorder. inversion HD ; firstorder.
  + destruct (LEM (uset C)).
    * right. right. right. right. left. apply Extensionality_Ensembles. split ; intros D HD ; auto.
      destruct D ; firstorder. inversion HD ; firstorder.
    * right. right. right. right. right. apply Extensionality_Ensembles. split ; intros D HD ; auto.
      destruct D ; firstorder. inversion HD ; firstorder.
Qed.


Lemma i_ABC : (u : upset P), (@uset _ u = Triple _ A B C) (@uset _ (i_P u) = Triple _ A B C).
Proof.
intros. unfold uset in *. destruct u ; simpl in *.
apply Extensionality_Ensembles. split ; intros D HD ; auto.
- destruct D ; firstorder.
- unfold In in *. left. rewrite H ; firstorder.
Qed.


Lemma i_AB : (u : upset P), (@uset _ u = Couple _ A B) (@uset _ (i_P u) = Singleton _ B).
Proof.
intros. unfold uset in *. destruct u ; simpl in *.
apply Extensionality_Ensembles. split ; intros D HD ; auto ; unfold In in *.
- subst. destruct HD as [ | [ | [ | [ | ]]]] ; subst ; firstorder.
  1,4,6: inversion .
  1-3: rewrite ; apply In_singleton.
- inversion HD ; subst. right. left ; firstorder. intro. inversion H.
Qed.


Lemma i_BC : (u : upset P), (@uset _ u = Couple _ B C) (@uset _ (i_P u) = Couple _ B C).
Proof.
intros. unfold uset in *. destruct u ; simpl in *.
apply Extensionality_Ensembles. split ; intros D HD ; auto ; unfold In in *.
- subst. destruct HD as [ | [ | [ | [ | ]]]] ; subst ; firstorder.
  1-2: inversion H.
  1-4: rewrite ; firstorder.
- right. right. subst. right. right. inversion HD ; subst ; firstorder. 1-2: intro ; inversion H.
Qed.


Lemma i_B : (u : upset P), (@uset _ u = Singleton _ B) (@uset _ (i_P u) = Singleton _ B).
Proof.
intros. unfold uset in *. destruct u ; simpl in *.
apply Extensionality_Ensembles. split ; intros D HD ; auto ; unfold In in *.
- subst. destruct HD as [ | [ | [ | [ | ]]]] ; subst ; firstorder.
  1-2: inversion H.
  1-3: rewrite ; firstorder.
- right. right. subst. left. inversion HD ; subst ; firstorder. 1-2: intro ; inversion H.
Qed.


Lemma i_C : (u : upset P), (@uset _ u = Singleton _ C) (@uset _ (i_P u) = Singleton _ C).
Proof.
intros. unfold uset in *. destruct u ; simpl in *.
apply Extensionality_Ensembles. split ; intros D HD ; auto ; unfold In in *.
- subst. destruct HD as [ | [ | [ | [ | ]]]] ; subst ; firstorder.
  1: inversion H.
  1-3: rewrite ; firstorder.
- right. right. subst. right ; left. inversion HD ; subst ; firstorder. 1-2: intro ; inversion H.
Qed.


Lemma i_Empty : (u : upset P), (@uset _ u = Empty_set _) (@uset _ (i_P u) = Empty_set _).
Proof.
intros. unfold uset in *. destruct u ; simpl in *.
apply Extensionality_Ensembles. split ; intros D HD ; auto.
- destruct HD as [ | [ | [ | [ | ]]]] ; subst ; firstorder.
- inversion HD.
Qed.


Lemma i_P_unit : i_P (unit_upset P) = (unit_upset P).
Proof.
apply upset_prf_irrel. rewrite i_ABC ; unfold uset ; unfold nodes in *.
all: unfold unit_upset ; apply Extensionality_Ensembles ; split ; intros D HD ;
destruct D ; subst ; firstorder.
Qed.


Lemma i_P_inter : u0 u1, @uset _ (i_P (inter_upset P )) = @uset _ (inter_upset P (i_P ) (i_P )).
Proof.
intros . unfold uset in *.
destruct (canonical_form_upset_P ) as [ | [ | [ | [ | [ | ]]]]].
- unfold uset in *. pose (i_ABC _ ). unfold uset in *.
  destruct (canonical_form_upset_P ) as [ | [ | [ | [ | [ | ]]]]] ; unfold uset in *.
  + pose (i_ABC _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; firstorder.
  + pose (i_AB _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; firstorder.
     1-2: rewrite in * ; simpl ; right ; left ; firstorder ; intro G ; inversion G.
  + pose (i_BC _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; firstorder.
     1-4: rewrite in * ; simpl ; right ; right ; right ; right ; firstorder ; intro G ; inversion G.
  + pose (i_B _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; firstorder.
     1-2,4: rewrite in * ; simpl ; right ; right ; left ; firstorder ; intro G ; inversion G.
     1-2: inversion .
  + pose (i_C _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; firstorder. inversion .
     1,3: rewrite in * ; simpl ; right ; right ; right ; left ; firstorder ; intro G ; inversion G. inversion .
  + pose (i_Empty _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; simpl ; firstorder.
- unfold uset in *. pose (i_AB _ ). unfold uset in *.
  destruct (canonical_form_upset_P ) as [ | [ | [ | [ | [ | ]]]]] ; unfold uset in *.
  + pose (i_ABC _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; firstorder.
     1-2: rewrite in * ; simpl ; right ; left ; firstorder ; intro G ; inversion G.
  + pose (i_AB _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; firstorder.
  + pose (i_BC _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; firstorder. inversion . 3-5: inversion .
     rewrite in * ; simpl ; right ; left ; firstorder ; intro G ; inversion G.
     rewrite in * ; simpl ; right ; right ; right ; right ; firstorder ; intro G ; inversion G.
  + pose (i_B _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; firstorder. inversion .
     1-2: rewrite in * ; simpl ; right ; left ; firstorder ; intro G ; inversion G.
     rewrite in * ; simpl ; right ; right ; left ; firstorder ; intro G ; inversion G.
     1-3: inversion .
  + pose (i_C _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; firstorder. inversion . 1-3: inversion .
     1-2: rewrite in ; inversion .
  + pose (i_Empty _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; simpl ; firstorder.
- unfold uset in *. pose (i_BC _ ). unfold uset in *.
  destruct (canonical_form_upset_P ) as [ | [ | [ | [ | [ | ]]]]] ; unfold uset in *.
  + pose (i_ABC _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; firstorder.
     1-4: rewrite in * ; simpl ; right ; right ; right ; right ; firstorder ; intro G ; inversion G.
  + pose (i_AB _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; firstorder. 4: inversion .
     1-3: rewrite in * ; simpl ; right ; right ; right ; right ; firstorder ; intro G ; inversion G. inversion H.
     rewrite in * ; simpl ; right ; left ; firstorder ; intro G ; inversion G.
  + pose (i_BC _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; firstorder.
  + pose (i_B _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; firstorder.
     1-4: rewrite in * ; simpl ; right ; right ; right ; right ; firstorder ; intro G ; inversion G.
     1-2: rewrite in * ; simpl ; right ; right ; left ; firstorder ; intro G ; inversion G.
     1-3: inversion .
  + pose (i_C _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; firstorder. inversion .
     1-4: rewrite in * ; simpl ; right ; right ; right ; right ; firstorder ; intro G ; inversion G.
     1: rewrite in * ; simpl ; right ; right ; right ; left ; firstorder ; intro G ; inversion G.
     1-2: inversion .
  + pose (i_Empty _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; simpl ; firstorder.
- unfold uset in *. pose (i_B _ ). unfold uset in *.
  destruct (canonical_form_upset_P ) as [ | [ | [ | [ | [ | ]]]]] ; unfold uset in *.
  + pose (i_ABC _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; firstorder. inversion H.
     1,3: rewrite in * ; simpl ; right ; right ; left ; firstorder ; intro G ; inversion G. all: inversion .
  + pose (i_AB _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; firstorder. 4: inversion . inversion H.
     rewrite in * ; simpl ; right ; right ; left ; firstorder ; intro G ; inversion G. 1-2: inversion . inversion H.
     rewrite in * ; simpl ; right ; left ; firstorder ; intro G ; inversion G.
  + pose (i_BC _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; firstorder.
     1-2,4: rewrite in * ; simpl ; right ; right ; left ; firstorder ; intro G ; inversion G. 1-2: inversion .
     1-2: rewrite in * ; simpl ; right ; right ; right ; right ; firstorder ; intro G ; inversion G. all: inversion .
  + pose (i_B _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; firstorder.
  + pose (i_C _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; firstorder. inversion . inversion .
     1-2: inversion . inversion . inversion . inversion . inversion . inversion H. rewrite in ; inversion .
  + pose (i_Empty _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; simpl ; firstorder.
- unfold uset in *. pose (i_C _ ). unfold uset in *.
  destruct (canonical_form_upset_P ) as [ | [ | [ | [ | [ | ]]]]] ; unfold uset in *.
  + pose (i_ABC _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; firstorder. inversion .
     1,3: rewrite in * ; simpl ; right ; right ; right ; left ; firstorder ; intro G ; inversion G. inversion .
  + pose (i_AB _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; firstorder. 4: inversion . inversion . 1-2: inversion .
     1-2: rewrite in ; inversion .
  + pose (i_BC _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; firstorder. inversion .
     1,3: rewrite in * ; simpl ; right ; right ; right ; left ; firstorder ; intro G ; inversion G. 1-2: inversion .
     1-2: rewrite in * ; simpl ; right ; right ; right ; right ; firstorder ; intro G ; inversion G. all: inversion .
  + pose (i_B _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; firstorder. 1,3-5,7-8: inversion . 1-2:inversion .
     1-2: rewrite in ; inversion .
  + pose (i_C _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; firstorder.
  + pose (i_Empty _ ). unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
     1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; simpl ; firstorder.
- unfold uset in *. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
   1-2: simpl in * ; unfold uset in * ; subst ; destruct ; destruct ; subst ; simpl ; firstorder.
Qed.


Lemma i_P_T : u, Included _ (@uset P (i_P u)) (@uset P u).
Proof.
intros. unfold uset. intros D HD. unfold In in *.
destruct (canonical_form_upset_P u) as [Hu | [Hu | [Hu | [Hu | [Hu | Hu]]]]] ; unfold uset in * ; rewrite Hu in *.
- destruct D ; firstorder.
- pose (i_AB _ Hu). unfold uset in * ; rewrite e in *. inversion HD ; firstorder.
- pose (i_BC _ Hu). unfold uset in * ; rewrite e in *. inversion HD ; firstorder.
- pose (i_B _ Hu). unfold uset in * ; rewrite e in *. inversion HD ; firstorder.
- pose (i_C _ Hu). unfold uset in * ; rewrite e in *. inversion HD ; firstorder.
- pose (i_Empty _ Hu). unfold uset in * ; rewrite e in *. inversion HD ; firstorder.
Qed.


Lemma i_P_4 : u, Included _ (@uset P (i_P u)) (@uset P (i_P (i_P u))).
Proof.
intros. unfold uset. intros D HD. unfold In in *.
destruct (canonical_form_upset_P u) as [Hu | [Hu | [Hu | [Hu | [Hu | Hu]]]]] ; unfold uset in *.
- pose (i_ABC _ Hu). unfold uset in * ; rewrite e in *.
  pose (i_ABC _ e). unfold uset in * ; rewrite in *. inversion HD ; firstorder.
- pose (i_AB _ Hu). unfold uset in * ; rewrite e in *.
  pose (i_B _ e). unfold uset in * ; rewrite in *. inversion HD ; firstorder.
- pose (i_BC _ Hu). unfold uset in * ; rewrite e in *.
  pose (i_BC _ e). unfold uset in * ; rewrite in *. inversion HD ; firstorder.
- pose (i_B _ Hu). unfold uset in * ; rewrite e in *.
  pose (i_B _ e). unfold uset in * ; rewrite in *. inversion HD ; firstorder.
- pose (i_C _ Hu). unfold uset in * ; rewrite e in *.
  pose (i_C _ e). unfold uset in * ; rewrite in *. inversion HD ; firstorder.
- pose (i_Empty _ Hu). unfold uset in * ; rewrite e in *.
  pose (i_Empty _ e). unfold uset in * ; rewrite in *. inversion HD ; firstorder.
Qed.


Definition val_P : (upset P) :=
fun n match n with
| 0 B_upset
| S n Empty_upset
end.

(* We finally can define our model. *)

Instance M : model :=
      {|
        pre := P ;

        i := i_P ;
        i_unit := i_P_unit ;
        i_inter := i_P_inter ;
        i_T := i_P_T ;
        i_4 := i_P_4 ;

        val := val_P ;
      |}.

(* We show that our model is indeed a countermodel
    to the formula mentioned initially. *)


Lemma Failure : (iS4H_prv (Empty_set _, (¬ (Box (# 0)))) --> Box (¬ (# 0))))) False.
Proof.
intro. apply Soundness in H. simpl in H.
epose (H M A).
assert (: ψ : form, In form (Empty_set form) ψ forces M A ψ).
intros Hpsi ; inversion Hpsi.

(* A forces the antecendent. *)
assert (: forces M A ((¬ Box # 0)))).
intros D reachAD HD. unfold reachable in reachAD. simpl in reachAD.
destruct D ; auto ; simpl.
1-2: apply HD with B ; auto ; intros ; unfold uset in * ; simpl in .
1-2: assert (J: (let (uset, _) := u in uset) = Singleton ABC B).
1,3: apply Extensionality_Ensembles ; split ; intros E HE ; firstorder.
1-2: pose (i_B u J) ; unfold uset in e ; unfold i ; simpl ; rewrite e in .
1-2: apply ; destruct u ; rewrite J ; firstorder.

(* But A forcing the consequent leads to a contradiction. *)
assert (F: forces M A (Box (¬ # 0)))).
pose (f A (reach_refl A)). simpl in . simpl. intros.
apply ; auto.
epose (force_Box_interior_truthset _ M A). destruct i.
clear . pose ( F). unfold uset in u.
assert ((let (uset, _) := (truthset_upset M (¬ # 0))) in uset) = Couple _ A B).
{ simpl. apply Extensionality_Ensembles. split ; intros D HD ; unfold In in *.
  - destruct D. 1-2: firstorder. exfalso. apply HD with C. apply I. intros. destruct v ; auto.
    inversion .
  - inversion HD ; subst. intros. destruct v ; auto. 1-2: apply with B ; auto ; apply In_singleton.
    intros. destruct v ; auto. apply with B ; auto ; apply In_singleton. }
apply i_AB in . unfold uset in .
unfold i in u. destruct (truthset_upset M (¬ # 0))). simpl in u. simpl in .
assert (Singleton ABC B A). rewrite .
destruct u as [( & & ) | [( & & & ) | [( & & & ) | [( & & & ) | ( & & & )]]]] ; subst ; auto.
1-4: inversion ; inversion . inversion .
Qed.


End Failure_of_GG.