(* 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 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.