(* Trying to get the constructive part of the note about resolutions of
 * closure and interior operators.
 * October 2004
 * Pierre Hyvernat
 *
 * I guess real coq hackers would find better ways to write the proofs, but
 * at least, it works...
 *)
Set Implicit Arguments.



Section Definitions.


(* The collection of subsets.
 * Since we will need to iterate it (as Pow(Pow X)), I define it directly
 * for Types. *)
Definition Pow (X:Type) : Type
 := X -> Prop.


(* inclusion *)
Definition subseteq (X:Type) (U V:Pow X) : Prop
 := forall x:X, (U x) -> (V x).

(* equality *)
Definition eqSubset (X:Type) (U V:Pow X) : Prop
 := (subseteq U V) /\ (subseteq V U).


(* "explicit" singleton subsets *)
Definition SING (X:Type) (x:X) : Pow X
 := eq x. (*fun x' => x=x'.*)
(* "implicit" singleton subsets *)
Definition SINGLE (X:Type) (U:Pow X) : Prop
 := exists2 x:X, U x & (forall x':X, U x' -> x=x').


(* relations *)
Definition Rel (X:Type) (Y:Type) : Type
 := X -> Y -> Prop.

(* converse of a relation *)
Definition CONV (X:Type) (Y:Type) (R:Rel X Y) : Rel Y X
 := fun (y:Y)(x:X) => R x y.


(* predicate transformers *)
Definition PT (X Y:Type) : Type
 := Pow(X) -> Pow(Y).

(* a predicate transformer is extensional if it is compatible with equality
 * on subsets *)
Definition EXT (X Y:Type) (F:PT X Y) : Prop
 := forall (U V:Pow X), (eqSubset U V) -> (eqSubset (F U) (F V)).

(* monotonicity *)
Definition monotonic (X Y:Type) (F:PT X Y) : Prop
  := forall (U V:Pow X), (subseteq U V) -> (subseteq (F U) (F V)).
(* antitonicity *)
Definition antitonic (X Y:Type) (F:PT X Y) : Prop
  := forall (U V:Pow X), (subseteq U V) -> (subseteq (F V) (F U)).


(* angelic update *)
Definition AngelU (X Y:Type) (r:Rel X Y) : PT Y X
 := fun V:Pow Y =>
    fun x:X     =>   exists2 y:Y, (r x y) & (V y).

(* demonic update *)
Definition DemonU (X Y:Type) (r:Rel X Y) : PT Y X
  := fun V:Pow Y =>
     fun x:X     =>   forall y:Y, (r x y) -> (V y).

(* "orthogonal" update (what's a good name for that???) *)
Definition BottomU (X Y:Type) (r:Rel X Y) : PT Y X
  := fun V:Pow Y =>
     fun x:X     =>   forall y:Y, (V y) -> (r x y).


(* unions of arbitrary collections of subsets *)
Definition BIGCUP (X:Type)(Y:Type)(F:PT X Y)(phi:Pow(Pow X)) : Pow Y
 := fun y:Y => exists U:Pow X, (phi U) /\ (F U y).
(* intersections of arbitrary collections of subsets *)
Definition BIGCAP (X:Type)(Y:Type)(F:PT X Y)(phi:Pow(Pow X)) : Pow Y
 := fun y:Y => forall U:Pow X, phi U -> F U y.


End Definitions.


(* some notations to make things a little easier to read *)
Notation "U :<: V" := (subseteq U V) (at level 70).
Notation "U :=: V" := (eqSubset U V) (at level 70).
Notation "'UNION' U :{ F | phi }:" := (BIGCUP (fun U => F) (fun U => phi)) (at level 0).
Notation "'INTER' U :{ F | phi }:" := (BIGCAP (fun U => F) (fun U => phi)) (at level 0).
Notation "r ~" := (CONV r) (at level 20).
Notation "<: r :>" := (AngelU r) (at level 0).
Notation "[: r :]" := (DemonU r) (at level 0).
Notation "\: r :/" := (BottomU r) (at level 0).



Section BasicProperties.

Variable X Y:Type.

(* Each subset is the union of the singletons it contains. *)
Lemma UnionSingle : forall (U:Pow X),
              U :=:  (UNION V :{ V | (SINGLE V) /\ (V :<: U)}:).
Proof.
 intros.
 split; unfold subseteq; intros.
  unfold BIGCUP.
  exists (SING x). repeat split.
   unfold SINGLE; unfold SING. exists x; auto.
   intros x' eq. rewrite <- eq. assumption.
   destruct H as [V [ [s f] v]]. auto.
Qed.

(* the angelic update is monotonic *)
Lemma AngelMonotonic : forall (r:Rel X Y), (monotonic <:r:>).
Proof.
 intros r U V i.
 unfold subseteq. intros.
 destruct H as [y r' u].
 exists y. assumption.
 apply i. assumption.
Qed.

(* the demonic update is monotonic *)
Lemma DemonMonotonic : forall (r:Rel X Y), (monotonic [:r:]).
Proof.
 intros r U V i.
 unfold subseteq. intros. intros y r'.
 apply i. apply H. assumption.
Qed.

(* bottom is antitonic *)
Lemma BottomAntitonic : forall (r:Rel X Y), (antitonic \:r:/).
Proof.
 intros r U V i.
 unfold subseteq. intros. intros y u.
 apply H. apply i. assumption.
Qed.

End BasicProperties.



(* Galois connection between the different PT defined from relations *)
Section Galois.

Variable X Y:Type.

Lemma AngelDemonGalois : forall (r:Rel X Y) (U:Pow X) (V:Pow Y),
  ((<:r:> V)  :<:  U) <->  (V  :<:  ([:r~:] U)).
Proof.
 intros. split.
  intros H y v x r'.
  apply H.
  exists y. unfold CONV in r'. assumption.
            assumption.
  intros H x [y r' v].
  apply H with y. assumption.
                  unfold CONV. assumption.
Qed.

Lemma BottomUSelfGalois : forall (r:Rel X Y) (U:Pow X) (V:Pow Y),
  (V  :<:  \:r~:/ U)  ->  (U  :<:  (\:r:/ V)).
Proof.
 intros R U V H x u y v. apply H; assumption.
Qed.

End Galois.



(*
 * the angelic update coresponds to sup-lattice morphisms, ie angelic updates
 * commute with arbitrary unions
 *)
Section AngelU.


Definition CommuteWithUnion (X Y:Type) (F:PT X Y) : Prop
 := forall phi:Pow(Pow X),
      (F ( UNION U :{ U | phi U}:)) :=:  (UNION U :{ F U | phi U }:).


Lemma AngelUCommuteWithUnion
  : forall (X Y:Type) (r:Rel X Y), (CommuteWithUnion <:r:>).
Proof.
 intros X Y R phi.
 split; intros x H.
  destruct H as [y r [U [fU u]]]. exists U. split. trivial.
                                                     exists y; auto.
  destruct H as [U [fU [y r u]]]. exists y. trivial.
                                              exists U. split; trivial.
Qed.


Lemma CommuteUnionMonotonic : forall (X Y:Type) (F:PT X Y) (e:EXT F),
  (CommuteWithUnion F) -> (monotonic F).
Proof.
 intros X Y F e C U V i y fu.
 set (phi := fun W => W=U \/ W=V).
 assert (H:(UNION W :{ (F W) | phi W }:) y).
 exists U. unfold phi. auto.
 assert ((F (UNION W :{ W | phi W }:) y)).
 destruct (C phi) as [_ H']. apply H'. exact H.
 clear C. rename H0 into H'.
 assert (V :=: UNION W :{ W | phi W }:).
 split; unfold subseteq; intros.
  clear F e i y fu H H'. rename H0 into v. exists V. unfold phi; auto.
  clear F e H fu H H'. rename H0 into H.
  destruct H as [W [H H']]. destruct H. apply i; rewrite <- H; trivial.
                                         rewrite <- H; trivial.
 destruct (e _ _ H0) as [_ H1]. apply H1. trivial.
Qed.


Lemma RepresentationAngelU : forall (X Y:Type) (F:PT Y X) (e:EXT F),
  (CommuteWithUnion F)
  ->
  exists r:Rel X Y, forall V:Pow Y, (F V) :=: (<:r:> V).
Proof.
 intros X Y F e C.
 set (R:=fun (x:X)(y:Y) => F (SING y) x).
 exists R.
 intros V. split; intros x H.

  (* 1 *)
  destruct (e _ _ (UnionSingle V)) as [H' _].
  destruct (C (fun W=>SINGLE W /\ W :<: V)) as [H'' _].
  destruct (H'' x (H' x H)) as [W [ [ [y w eq] i] H''']].
  exists y. unfold R.

   assert (SING y:=:W). clear X F e C R V x H H' H'' i H'''.
   split; intros y' H'. unfold SING in H'; rewrite <- H'; trivial.
                        unfold SING; apply eq; trivial.
   destruct (e _ _ H0) as [_ H1]. apply H1; trivial.

   apply i; trivial.

  (* 2*)
  destruct H as [y r H].
  assert (SING y :<: V). intros y' eq; rewrite <- eq; trivial.
  apply (CommuteUnionMonotonic e C H0). exact r.
Qed.

End AngelU.


(* Same thing for the demonic update *)
Section DemonU.

Definition CommuteWithInter (X Y:Type) (F:PT X Y) : Prop
 := forall phi:Pow(Pow X),
      (F ( INTER U :{ U | phi U}:)) :=:  (INTER U :{ F U | phi U }:).

Lemma DemonUCommuteWithInter
  : forall (X Y:Type) (r:Rel X Y), (CommuteWithInter [:r:]).
Proof.
 intros X Y R phi.
 split; intros x H.
  intros U fU y r. apply H; trivial.
  intros y r U fU. apply H; trivial.
Qed.

Lemma CommuteInterMonotonic : forall (X Y:Type) (F:PT X Y) (e:EXT F),
  (CommuteWithInter F) -> (monotonic F).
Proof.
 intros X Y F e C U V i y fu.
 set (phi := fun W => W=U \/ W=V).
 assert (H:(INTER W :{ (F W) | phi W }:) y).
 destruct (C phi) as [H _]. apply H. clear H.
 assert (INTER W :{W|phi W}: :=: U).
 split. intros x I. apply (I U). unfold phi; auto.
        intros x u W fW. destruct fW. rewrite H; trivial.
                                      rewrite H; apply i; trivial.
 destruct (e _ _ H) as [_ H']. apply H'; trivial.
 apply (H V). unfold phi; auto.
Qed.


Lemma RepresentationDemonU : forall (X Y:Type) (F:PT Y X) (e:EXT F),
  (CommuteWithInter F)
  ->
  exists r:Rel X Y, forall V:Pow Y, (F V) :=: ([:r:] V).
Proof.
 intros X Y F e C.
 set (R := fun (x:X) => INTER W :{ W | F W x}:).
 exists R.
 intros V. split; intros x H.

  (* 1 *)
  intros y r. apply r.
  assert (H' : V:=:fun y=>V y). split; intros xx HH; auto.
  destruct (e _ _ H') as [H1 _]. apply H1; trivial.

  (* 2 *)
  assert (INTER W :{ W|F W x}: :<: V).
  intros y Hy. apply H. exact Hy.
  apply (CommuteInterMonotonic e C H0).
  destruct (C (fun W=>F W x)) as [_ H1]. apply H1.
  intros U HU. trivial.
Qed.

End DemonU.


(* and finally for the "Bottom" operator *)
Section BottomU.

Definition TransformUnionInter (X Y:Type) (F:PT X Y) : Prop
 := forall phi:Pow(Pow X),
      (F ( UNION U :{ U | phi U}:)) :=:  (INTER U :{ F U | phi U }:).

Lemma BottomUTransformUnionInter
  : forall (X Y:Type) (r:Rel X Y), (TransformUnionInter \:r:/).
Proof.
 intros X Y R phi.
 split; intros x H.
  intros V fV y v. apply H. exists V. auto.
  intros y [V [fV v]]. apply H with V; trivial.
Qed.


Lemma TransformUnionInterAntitonic : forall (X Y:Type) (F:PT X Y) (e:EXT F),
  (TransformUnionInter F) -> (antitonic F).
Proof.
 intros X Y F e T U V i y fv.
 set (phi := fun W => W=U \/ W=V).
 assert (H:UNION W :{W|phi W}: :=: V).
 split; intros x H. destruct H as [W [fW w]]. destruct fW. apply i; rewrite <-H; trivial.
                                                            rewrite <- H; trivial.
                                               exists V. split. right; trivial. trivial.
 destruct (e _ _ H) as [_ H'].
 destruct (T phi) as [H'' _].
 generalize (H' y fv). intros. generalize (H'' y H0). intros. clear H H' H0 H'' i fv.
 apply H1. unfold phi. auto.
Qed.


(*
 * This proof doesn't use the fact that (BottomU R) is antitonic, while the
 * corresponding results for AngelU and DemonU use the fact that <R> and
 * [R] are monotonic...
 * Could I remove this intermediary lemmas from the proofs of
 * RepresentationAngelU and RepresentationDemonU?
 *)
Lemma RepresentationBottomU : forall (X Y:Type) (F:PT Y X) (e:EXT F),
  (TransformUnionInter F)
  ->
  exists r:Rel X Y, forall V:Pow Y, (F V) :=: (\:r:/ V).
Proof.
 intros X Y F e T.
 set (R := fun (x:X) (y:Y) => F (SING y) x).
 exists R.
 intros V. split; intros x H.

  (* 1 *)
  intros y v. unfold R.
  destruct (T (fun W=> SINGLE W /\ W :<: V)) as [H1 _]. apply H1. clear H1.
  destruct (e _ _ (UnionSingle V)) as [H2 _]. apply H2. trivial.

  split. exists y. unfold SING; auto.
                   intros; auto.
         intros y' eq. rewrite <- eq. trivial.

  (* 2 *)
  destruct (e _ _ (UnionSingle V)) as [_ H1]. apply H1. clear H1.
  destruct (T (fun W=> SINGLE W /\ W :<: V)) as [_ H2]. apply H2. clear H2.
  intros W [ [y w] eq] i.
  assert (W:=:SING y).
  split. intros y' w'. unfold SING. apply eq. trivial.
         intros y' eq'. unfold SING in eq'. rewrite <- eq'. trivial.
  destruct (e _ _ H0). apply H2. apply H. apply i. trivial.
Qed.

End BottomU.


(* Note, this doesn' require that F is extensional. *)
Theorem PTFactorize
  : forall (X Y:Type)(F:PT X Y), monotonic F ->
    exists Z:Type, exists R:Rel Z X, exists S:Rel Y Z,
    forall (U:Pow X), F U :=: <:S:> ([:R:] U).
Proof.
 intros X Y F m.
 set (Z:=Pow X); exists Z.
 set (R:=fun (U:Z)(x:X) => U x); exists R.
 set (S:=fun (y:Y)(U:Z) => F U y); exists S.
 intros U; split; intros y H.
  exists U. exact H. intros x r. exact r.
  destruct H as [U' s H]. unfold DemonU in H. unfold R in H. apply (m _ _  H). exact s.
Qed.



Section InteriorClosure.

Variable X:Type.
Variable F:PT X X.
Variable m:monotonic F.

Definition Closure : Prop
  := (forall U, U :<: F U)
      /\
     (forall U, F (F U) :<: F U).
Definition Interior : Prop
  := (forall U, F U :<: U)
      /\
     (forall U, F U :<: F (F U)).

Definition FIX : Pow(Pow X)
  := fun U => U :=: F U.


Lemma RepresentationInterior
 : Interior -> exists Y:Type, exists R:Rel X Y,
    forall U,  <:R:> ([:R~:] U) :=: F U.
Proof.
 intros C.
 set (PX:=Pow X). exists PX.
 set (R:=fun (x:X)(U:PX) => F U x). exists R.
 intros U; split.

 (* 1 *)
 intros x r.
 destruct r as [V r f]. unfold R in r. unfold R in f; unfold CONV in f; unfold DemonU in f.
 apply (m f). destruct C as [_ i]; apply i. trivial.

 (* 2 *)
 intros x H.
 exists (F U). unfold R. destruct C as [_ i]; apply i. trivial.
 intros x' r'.
 destruct C as [i _]; apply i; apply i. apply r'.
Qed.


Lemma RepresentationClosure
 : Closure -> exists Y:Type, exists R:Rel X Y,
    forall U,  \:R:/ (\:R~:/ U) :=: F U.
Proof.
 intros C.
 set (PX:=Pow X). exists PX.
 set (R:=fun (x:X)(U:PX) => F U x). exists R.
 intros U; split.

 (* 1 *)
 intros x r.
 destruct C as [i j]. apply j.
 apply r. intros x' u'. unfold R; unfold CONV.
 apply i; apply i. trivial.

 (* 2 *)
 intros x H V r. unfold R. unfold BottomU in r; unfold R in r; unfold CONV in r.
 assert (F U :<: F V).
 intros x' H'. destruct C as [_ i]; apply i; clear i. apply (m r). trivial.
 apply H0. trivial.
Qed.

End InteriorClosure.