Global Set Implicit Arguments.
Global Unset Strict Implicit.
Global Unset Printing Implicit Defensive.
Global Set Universe Polymorphism.
Global Unset Universe Minimization ToSet.
Require Export Setoid Classes.Morphisms.
(* Some definitions for relations *)
Definition functional {X Y} (R : X -> Y -> Prop) :=
forall x y y', R x y -> R x y' -> y = y'.
Definition injective {X Y} (R : X -> Y -> Prop) :=
forall x x' y, R x y -> R x' y -> x = x'.
Definition total {X Y} (R : X -> Y -> Prop) :=
forall x, exists y, R x y.
Definition surjective {X Y} (R : X -> Y -> Prop) :=
forall y, exists x, R x y.
Definition cres {X} (equiv : X -> X -> Prop) (P : X -> Prop) :=
forall x x', equiv x x' -> P x -> P x'.
Definition fres {X} (equiv : X -> X -> Prop) (F : X -> X) :=
forall x x', equiv x x' -> equiv (F x) (F x').
Definition cequiv {X} (P P' : X -> Prop) :=
forall x, P x <-> P' x.
Instance cequiv_equiv {X} :
Equivalence (@cequiv X).
Proof.
firstorder.
Qed.
(* A set structure is a type together with a membership relation *)
Class SetStruct :=
{
set :> Type;
elem : set -> set -> Prop;
}.
Coercion set : SetStruct >-> Sortclass.
(* A Z-structure is a set structure with constants for emptyset,
unordered pair, union, power and separation *)
Class ZStruct :=
{
Zset :> SetStruct;
eset : Zset;
upair : Zset -> Zset -> Zset;
union : Zset -> Zset;
power : Zset -> Zset;
sep : (Zset -> Prop) -> Zset -> Zset;
}.
Coercion Zset : ZStruct >-> SetStruct.
(* A ZF'-structure is a Z-structure with a constant for functional replacement *)
Class ZFStruct' :=
{
ZFset' :> ZStruct;
frep : (ZFset' -> ZFset') -> ZFset' -> ZFset';
}.
Coercion ZFset' : ZFStruct' >-> ZStruct.
(* A ZF-structure is a ZF'-structure with a description operator *)
Class ZFStruct :=
{
ZFset :> ZFStruct';
delta : (ZFset -> Prop) -> ZFset;
}.
Coercion ZFset : ZFStruct >-> ZFStruct'.
(* Notation for subsets and subclasses and further shorthands *)
Definition sub {M : SetStruct} (x y : M) :=
forall z, elem z x -> elem z y.
Definition equiv {M : SetStruct} (x y : M) :=
sub x y /\ sub y x.
Notation "x 'el' y" := (elem x y) (at level 70).
Notation "x 'nel' y" := (~ elem x y) (at level 70).
Notation "x <<= y" := (sub x y) (at level 70).
Notation "x << y" := (x <<= y /\ x <> y) (at level 70).
Notation "x == y" := (equiv x y) (at level 70).
Notation "p '<=p' q" := (forall z, p z -> q z) (at level 70).
Notation "x '<=c' p" := (forall z, z el x -> p z) (at level 70).
Notation "p '<=s' x" := (forall z, p z -> z el x) (at level 70).
Notation "0" := eset.
Notation inhab x := (exists y, y el x).
Notation upbnd x u := (forall z, z el x -> z <<= u).
Notation gel x u := (u el x /\ upbnd x u).
Notation sing x := (upair x x).
Notation binunion x y := (union (upair x y)).
Notation cl x := (fun y => y el x).
Notation eqcl x := (fun y => y == x).
Definition least {M : SetStruct} P x :=
P x /\ forall y, P y -> x <<= y.
Definition unique {M : SetStruct} (P : M -> Prop) :=
forall x y, P x -> P y -> x = y.
Definition agree {M : SetStruct} P x :=
forall z, z el x <-> P z.
Definition small {M : SetStruct} P :=
exists x, agree P x.
Definition iseqcl {M : SetStruct} (P : M -> Prop) :=
exists x, forall y, P y <-> eqcl x y.
Inductive WF {M : SetStruct} x : Prop :=
WFI : (forall y, y el x -> WF y) -> WF x.
(* Intensional Z*, Z, ZF' and ZF (all without infinity) *)
Class iZS (M : ZStruct) : Prop :=
{
Morph : forall x x' y, x == x' -> x el y -> x' el y;
Eset : forall z, z nel 0;
Pair : forall x y z, z el (upair x y) <-> z == x \/ z == y;
Union : forall x z, z el union x <-> exists y, y el x /\ z el y;
Power : forall x y, y el power x <-> y <<= x;
Sep : forall P x y, cres equiv P -> y el (sep P x) <-> y el x /\ P y;
}.
Class iZ (M : ZStruct) : Prop :=
{
HiZ :> iZS M;
AxWF : forall x, WF x;
}.
Class iZF' (M : ZFStruct') : Prop :=
{
HiZF' :> iZ M;
Frep : forall F x z, fres equiv F -> z el (frep F x) <-> exists y, y el x /\ equiv z (F y);
}.
Class iZF (M : ZFStruct) : Prop :=
{
HiZF :> iZF' M;
Desc1 : forall P, iseqcl P -> P (delta P);
Desc2 : forall P P', (forall x, P x <-> P' x) -> delta P = delta P';
}.
(* Extensional Z, ZF', ZF, and ZF* *)
Class Z (M : ZStruct) : Prop :=
{
HZ :> iZ M;
ZExt : forall x y, x == y <-> x = y;
}.
Class ZF' (M : ZFStruct') : Prop :=
{
HZF' :> iZF' M;
ZFExt' : forall x y, x == y <-> x = y;
}.
Class ZF (M : ZFStruct) : Prop :=
{
HZF :> iZF M;
ZFExt : forall x y, x == y <-> x = y;
}.
Class ZFS (M : ZFStruct) : Prop :=
{
HZFS :> iZS M;
ZFSExt : forall x y, x == y <-> x = y;
ZFSFrep : forall F x z, fres equiv F -> z el (frep F x) <-> exists y, y el x /\ equiv z (F y);
ZFSDesc1 : forall P, iseqcl P -> P (delta P);
ZFSDesc2 : forall P P', (forall x, P x <-> P' x) -> delta P = delta P';
}.
Hint Extern 4 =>
match goal with
| [ H : _ el 0 |- _ ] => exfalso; apply (Eset H)
end.
(* Infinity *)
Fixpoint powit {M : ZStruct} n :=
match n with
| O => 0
| S n' => power (powit n')
end.
Definition finpow {M : ZStruct} x :=
exists n, x == powit n.
Definition Inf (M : ZStruct) :=
exists om, agree finpow om.
(* ZF-closed classes and universes *)
Definition ctrans {M : SetStruct} (P : M -> Prop) :=
forall x y, P x -> y el x -> P y.
Definition cswelled {M : SetStruct} (P : M -> Prop) :=
forall x y, P x -> y <<= x -> P y.
Definition trans {M : SetStruct} x :=
ctrans (cl x).
Definition swelled {M : SetStruct} x :=
cswelled (cl x).
Definition closed_upair {M : ZStruct} (U : M -> Prop) :=
forall x y, U x -> U y -> U (upair x y).
Definition closed_union {M : ZStruct} (U : M -> Prop) :=
forall x, U x -> U (union x).
Definition closed_power {M : ZStruct} (U : M -> Prop) :=
forall x, U x -> U (power x).
Definition closed_sep {M : ZStruct} (U : M -> Prop) :=
forall P x, cres equiv P -> U x -> U (sep P x).
Definition closed_frep {M : ZFStruct'} (U : M -> Prop) :=
forall F x, fres equiv F -> U x -> frep F x <=c U -> U (frep F x).
Structure closed_Z {M : ZStruct} U : Prop :=
{
U_trans : ctrans U;
U_eset : U 0;
U_upair : closed_upair U;
U_union : closed_union U;
U_power : closed_power U;
U_sep : closed_sep U;
}.
Structure closed_ZF {M : ZFStruct'} U : Prop :=
{
U_Z :> closed_Z U;
U_frep : closed_frep U;
}.
Definition universe {M : ZFStruct'} u :=
closed_ZF (cl u).
(* Universe strength and the axiomatisations ZFge, ZFn and ZFw *)
Fixpoint strength {M : ZFStruct'} n x :=
match n with
| O => True
| S n => exists u, u el x /\ universe u /\ strength n u
end.
(* ZFge n is ZF with at least n universes *)
Definition ZFge n (M : ZFStruct) :=
ZF M /\ (exists x, strength n x).
(* ZFn is ZF with exactly n universes *)
Definition ZFn n (M : ZFStruct) :=
ZFge n M /\ (~ exists x, strength (S n) x).
(* ZFw is ZF with infinitely many universes *)
Definition ZFw (M : ZFStruct) :=
ZF M /\ (forall n, exists x, strength n x).
(* Equiv is an equivalence relation and respects all set-theoretic notions *)
Section Proper.
Context { M : ZFStruct' }.
Context { MAX : iZF' M }.
Lemma eq_equiv x y :
x = y -> equiv x y.
Proof.
intros ->. firstorder.
Qed.
Global Instance equiv_equiv :
Equivalence equiv.
Proof.
firstorder.
Qed.
Lemma elem_proper' x x' y y' :
x == x' -> y == y' -> x el y -> x' el y'.
Proof.
intros H1 H2 H3. apply (Morph H1) in H3. now apply H2.
Qed.
Global Instance elem_proper :
Proper (equiv ==> equiv ==> iff) elem.
Proof.
intros x x' H1 y y' H2.
now split; apply elem_proper'.
Qed.
Global Instance sub_proper :
Proper (equiv ==> equiv ==> iff) sub.
Proof.
intros x x' H1 y y' H2. split; intros H u.
- rewrite <- H1, <- H2. apply H.
- rewrite H1, H2. apply H.
Qed.
Lemma upair_proper' x x' y y' :
x == x' -> y == y' -> upair x y <<= upair x' y'.
Proof.
intros H1 H2 z [-> | ->] % Pair; apply Pair; auto.
Qed.
Global Instance upair_proper :
Proper (equiv ==> equiv ==> equiv) upair.
Proof.
intros x x' H1 y y' H2.
split; now apply upair_proper'.
Qed.
Lemma union_proper' x x' :
x == x' -> union x <<= union x'.
Proof.
intros H z [y[H1 % H H2]] % Union.
apply Union. exists y. split; assumption.
Qed.
Global Instance union_proper :
Proper (equiv ==> equiv) union.
Proof.
intros x x' H. split; now apply union_proper'.
Qed.
Lemma power_proper' x x' :
x == x' -> power x <<= power x'.
Proof.
intros H z. repeat rewrite Power. now rewrite H.
Qed.
Global Instance power_proper :
Proper (equiv ==> equiv) power.
Proof.
intros x x' H. split; now apply power_proper'.
Qed.
Lemma ZF_proper' P P' :
closed_ZF P -> cequiv P P' -> closed_ZF P'.
Proof.
intros UU HU. unfold cequiv in HU. split. split.
- intros x y. repeat rewrite <- HU. apply UU.
- rewrite <- HU. apply UU.
- intros x y. repeat rewrite <- HU. apply UU.
- intros x. repeat rewrite <- HU. apply UU.
- intros x. repeat rewrite <- HU. apply UU.
- intros p x. repeat rewrite <- HU. apply UU.
- intros F x FR X FS. rewrite <- HU in *.
apply UU; trivial. intros y. rewrite HU. now apply FS.
Qed.
Global Instance ZF_proper :
Proper (cequiv ==> iff) closed_ZF.
Proof.
intros P P' HP. split; intros H; apply (ZF_proper' H); firstorder.
Qed.
Global Instance universe_proper :
Proper (equiv ==> iff) universe.
Proof.
intros u u' H. apply ZF_proper.
intros x. now rewrite H.
Qed.
Lemma strength_proper' n x x' :
x == x' -> strength n x -> strength n x'.
Proof.
intros H. destruct n; simpl; auto.
intros [u U]. exists u. now rewrite <- H.
Qed.
Global Instance strength_proper n :
Proper (equiv ==> iff) (strength n).
Proof.
intros x x' H. split; apply strength_proper'; now rewrite H.
Qed.
Lemma cres_cl x :
cres equiv (cl x).
Proof.
now intros y y' ->.
Qed.
Lemma sep_cswelled P :
cres equiv P -> closed_sep P -> cswelled P.
Proof with eauto using cres_cl.
intros PR H x y X1 X2.
assert (Y : y == (sep (cl y) x)).
- split; intros z Z.
+ apply Sep...
+ apply Sep in Z as [_ Z]...
- apply (PR (sep (cl y) x)).
+ now rewrite Y.
+ apply H...
Qed.
Lemma cswelled_sep P :
cswelled P -> closed_sep P.
Proof.
intros H p x PC X.
apply (H x); trivial.
intros y [Y _] % Sep; trivial.
Qed.
Lemma swelled_sep x :
swelled x <-> closed_sep (cl x).
Proof.
split.
+ apply cswelled_sep.
+ apply sep_cswelled, cres_cl.
Qed.
Definition const :=
fun (x : set) => True.
Fact const_ZF :
closed_ZF const.
Proof.
firstorder.
Qed.
End Proper.