Parameter set : Type. Parameter IN : set -> set -> Prop. Infix ":e" := IN (at level 70). Definition Subq (X Y:set) : Prop := forall z, z :e X -> z :e Y. Infix "c=" := Subq (at level 70). (** * Axioms **) (** Extensionality ***) Axiom set_ext : forall X Y, X c= Y -> Y c= X -> X = Y. (** Empty ***) Parameter empty : set. Axiom emptyE : forall (x:set), ~ x :e empty. (** Unions ***) Parameter union : set -> set. Axiom unionAx : forall (x z:set), z :e union x <-> exists y, y :e x /\ z :e y. (** Power Sets ***) Parameter power : set -> set. Axiom powerAx : forall (X:set), forall Y:set, Y c= X <-> Y :e power X. (** * Specifications **) (** Description Specification ***) Record DescrSpec : Type := mkDescr { descr : (set -> Prop) -> set; descrAx : forall P:set -> Prop, (exists! y, P y) -> P (descr P) }. (** Separation Specification ***) Record SepSpec : Type := mkSep { sep : set -> (set -> Prop) -> set; sepAx : forall X P z, z :e sep X P <-> z :e X /\ P z }. (** Total Replacement Specification ***) Record TotReplSpec : Type := mkTotRepl { repS : set -> (set -> set -> Prop) -> set; repSAx : forall X:set, forall P:set -> set -> Prop, (forall x, x :e X -> exists! y, P x y) -> forall y, y :e repS X P <-> exists x, x :e X /\ P x y }. (** Map Replacement Specification ***) Record MapReplSpec : Type := mkMapRepl { repM : set -> (set -> set) -> set; repMAx : forall X:set, forall F:set -> set, forall y, y :e repM X F <-> exists x, x :e X /\ F x = y }. (** Partial Replacement Specification (No requirement that P is a *total* functional relation on X). This is the version Barras uses. ***) Record PartReplSpec : Type := mkPartRepl { repP : set -> (set -> set -> Prop) -> set; repPAx : forall X:set, forall P:set -> set -> Prop, (forall x, x :e X -> forall y z, P x y -> P x z -> y = z) -> forall y, y :e repP X P <-> exists x, x :e X /\ P x y }. (** * TotRepl <-> Descr /\ MapRepl ***) Definition TotRepl_Descr : TotReplSpec -> DescrSpec. intros sr. set (d := (fun P => union (repS sr (power empty) (fun _ y => P y)))). apply (mkDescr d). intros P H1. assert (L1:forall x, x :e power empty -> exists! y, P y). { intros x _. exact H1. } destruct H1 as [y [H1 H2]]. assert (L2:d P = y). { apply set_ext. - intros z H3. destruct (unionAx (repS sr (power empty) (fun _ y => P y)) z) as [H4 _]. destruct (H4 H3) as [w [H5 H6]]. destruct (repSAx sr (power empty) (fun _ y => P y) L1 w) as [H7 _]. destruct (H7 H5) as [_ [_ H8]]. rewrite (H2 w H8). exact H6. - intros z H3. destruct (unionAx (repS sr (power empty) (fun _ y => P y)) z) as [_ H4]. apply H4. exists y. split. + destruct (repSAx sr (power empty) (fun _ y => P y) L1 y) as [_ H5]. apply H5. exists empty. split. * destruct (powerAx empty empty) as [H6 _]. apply H6. intros w H7. exact H7. * exact H1. + exact H3. } rewrite L2. exact H1. Defined. Definition TotRepl_MapRepl : TotReplSpec -> MapReplSpec. intros sr. set (r := fun (X:set) (F:set -> set) => repS sr X (fun x y => F x = y)). apply (mkMapRepl r). intros X F y. apply (repSAx sr). intros x _. exists (F x). split. - reflexivity. - intros z H. exact H. Defined. Definition Descr_MapRepl_TotRepl : DescrSpec -> MapReplSpec -> TotReplSpec. intros d mr. set (r := fun (X:set) (P:set -> set -> Prop) => repM mr X (fun x => descr d (P x))). apply (mkTotRepl r). intros X P H1 y. destruct (repMAx mr X (fun x => descr d (P x)) y) as [H2 H3]. split. - intros H4. destruct (H2 H4) as [x [H5 H6]]. exists x. split. + exact H5. + rewrite <- H6. apply (descrAx d (P x)). apply H1. exact H5. - intros [x [H4 H5]]. apply H3. exists x. split. + exact H4. + destruct (H1 x H4) as [z [H6 H7]]. generalize (descrAx d (P x) (H1 x H4)). intros H8. rewrite <- (H7 _ H8). exact (H7 _ H5). Defined. (** * PartRepl <-> Sep /\ TotRepl ***) Definition PartRepl_Sep : PartReplSpec -> SepSpec. intros pr. set (s := fun (X:set) (P:set -> Prop) => repP pr X (fun x y => P x /\ x = y)). apply (mkSep s). intros X P. assert (L1:forall x, x :e X -> forall y z, P x /\ x = y -> P x /\ x = z -> y = z). { intros x _ y z [_ H1] [_ H2]. rewrite <- H1. exact H2. } intros z. destruct (repPAx pr X (fun x y => P x /\ x = y) L1 z) as [H1 H2]. split. - intros H3. destruct (H1 H3) as [x [H4 [H5 H6]]]. rewrite <- H6. split; assumption. - intros [H3 H4]. apply H2. exists z. tauto. Defined. Definition PartRepl_TotRepl : PartReplSpec -> TotReplSpec. intros pr. set (r := repP pr). apply (mkTotRepl r). intros X P H1. apply (repPAx pr). intros x H2 y z H3 H4. destruct (H1 x H2) as [w [_ H5]]. rewrite <- (H5 y H3). exact (H5 z H4). Defined. Definition Sep_TotRepl_PartRepl : SepSpec -> TotReplSpec -> PartReplSpec. intros s sr. set (r := fun (X:set) (P:set -> set -> Prop) => repS sr (sep s X (fun x => exists y, P x y)) P). apply (mkPartRepl r). intros X P H1. assert (L1:forall x, x :e sep s X (fun x => exists y, P x y) -> exists! y, P x y). { intros x H2. destruct (sepAx s X (fun x => exists y, P x y) x) as [H3 _]. destruct (H3 H2) as [H4 [y H5]]. exists y. split. - exact H5. - intros z. apply (H1 x H4). exact H5. } intros y. destruct (repSAx sr (sep s X (fun x => exists y, P x y)) P L1 y) as [H2 H3]. split. - intros H4. destruct (H2 H4) as [x [H5 H6]]. destruct (sepAx s X (fun x => exists y, P x y) x) as [H7 _]. destruct (H7 H5) as [H8 _]. exists x. split. + exact H8. + exact H6. - intros [x [H4 H5]]. apply H3. exists x. split. + destruct (sepAx s X (fun x => exists y, P x y) x) as [_ H6]. apply H6. split. * exact H4. * exists y. exact H5. + exact H5. Defined.