Ltac contra A :=
match goal with
|[ |- ?t] => destruct (classic t) as [A|A]; [exact A|exfalso]
end.
Section Stage.
Context { set : ZFStruct }.
Context { ZFS : ZF set }.
Implicit Types x y z a b c u v : set.
Implicit Types p q : set -> Prop.
Fact class_not_sub p q :
~ p <=p q -> exists x, p x /\ ~ q x.
Proof.
intros H1. contra H2. apply H1.
intros x X. contra H3. apply H2. now exists x.
Qed.
Fact set_not_sub x y :
~ x <<= y -> exists z, z el x /\ z nel y.
Proof.
intros H1. contra H2. apply H1.
intros z Z. contra H3. apply H2. now exists z.
Qed.
Inductive Stage : set -> Prop :=
| StageS x : Stage x -> Stage (power x)
| StageU x : x <=c Stage -> Stage (union x).
Fact Stage_eset :
Stage eset.
Proof.
rewrite <- union_eset. constructor. auto.
Qed.
Fact Stage_trans :
Stage <=p trans.
Proof.
intros x H. induction H.
- now apply power_trans.
- now apply union_trans.
Qed.
Fact Stage_swelled :
Stage <=p swelled.
Proof.
induction 1 as [x _ _ | x _ IH]; intros a b.
- intros H1 % Power H2. apply Power. auto.
- intros (c&H1&H2) % Union H3. apply Union.
exists c. split. exact H1. now apply (IH c H1 a b).
Qed.
Fact Stage_union x y :
Stage x -> y el x -> union y el x.
Proof.
intros H. revert y. induction H.
- intros y Y % Power. apply Power.
intros z [u[U1 % Y U2]] % Union.
now apply (Stage_trans H U1).
- intros y [z[Z1 Z2]] % Union.
specialize (H0 z Z1 y Z2).
apply Union. now exists z.
Qed.
Fact Stage_power x a :
Stage x -> a el x -> power a el power x.
Proof.
intros H. revert a. induction H; intros a A; apply Power; intros b B % Power.
- apply Power. apply (sub_trans B). now apply Power.
- apply Union in A as [c[C1 C2]]. apply Union.
exists c. split; trivial. specialize (H0 c C1 a C2).
apply Power in H0. apply H0. now apply Power.
Qed.
Fact Stage_upair x a b :
Stage x -> a el x -> b el x -> (upair a b) el (power x).
Proof.
intros _ A B. apply Power.
intros c [C|C] % pair_el; now subst.
Qed.
Fact Stage_sep x a p :
Stage x -> a el x -> sep p a el x.
Proof.
intros H1 H2. apply (Stage_swelled H1 H2). apply sep_sub.
Qed.
(* Linearity *)
Fact Stage_inc x :
Stage x -> x <<= power x.
Proof.
intros H % Stage_trans y Y. apply Power. intros z. now apply H.
Qed.
Fact xm_upbnd x y :
upbnd x y \/ exists z, z el x /\ ~ z <<= y.
Proof.
destruct (classic (exists z, z el x /\ ~ z <<= y)) as [H|H].
- right. exact H.
- left. intros z H1. contra H2. contradict H. now exists z.
Qed.
Lemma Stage_double_ind (R: set -> set -> Prop) :
(forall x y, Stage x -> R x y -> R y x -> R (power x) y) ->
(forall x y, (forall z, z el x -> R z y) -> R (union x) y) ->
forall x y, Stage x -> Stage y -> R x y.
Proof.
intros H1 H2 x y Hx. revert y.
induction Hx as [x Hx IHx|x _ IHx]; intros y Hy.
- apply (H1 x y Hx (IHx y Hy)).
induction Hy as [y Hy IHy|y _ IHy].
+ apply (H1 y x Hy). exact IHy. exact (IHx _ Hy).
+ apply (H2 y x IHy).
- apply (H2 x y). intros z H. now apply IHx.
Qed.
Lemma Stage_lin_succ x y :
Stage x -> Stage y -> x <<= y \/ power y <<= x.
Proof.
revert x y. apply Stage_double_ind.
- intros x y Hx [H1|H1] [H2|H2]; auto.
+ destruct (Ext H1 H2). auto.
+ right. apply (sub_trans H1). apply Stage_inc, Hx.
- intros x y H.
destruct (xm_upbnd x y) as [H1|(z&H1&H2)].
+ left. apply union_sub, H1.
+ right. destruct (H z H1) as [H3|H3].
* exfalso; tauto.
* apply (sub_trans H3). cbn. apply union_el_sub, H1.
Qed.
Fact Stage_lin x y :
Stage x -> Stage y -> x <<= y \/ y <<= x.
Proof.
intros Hx Hy.
destruct (Stage_lin_succ Hx Hy) as [H|H]; auto.
right. revert H. apply sub_trans, Stage_inc, Hy.
Qed.
Fact Stage_lin_el x y :
Stage x -> Stage y -> x <<= y \/ y el x.
Proof.
intros H I. destruct (Stage_lin_succ H I) as [J|J]; auto.
right. apply J. apply power_eager.
Qed.
Fact Stage_tricho x y :
Stage x -> Stage y -> x el y \/ x = y \/ y el x.
Proof.
intros H I. destruct (Stage_lin_el H I) as [H1|H1].
- destruct (Stage_lin_el I H) as [H2|H2].
+ right. left. now apply Ext.
+ now left.
- now repeat right.
Qed.
(* Least Elements *)
Lemma Stage_least x p :
Stage x -> p x -> ex (least (fun z => Stage z /\ p z)).
Proof.
intros H1 H2. induction (AxWF x) as [x _ IH].
destruct (classic (exists y, Stage y /\ p y /\ y el x)) as [(y&H3&H4&H5)|H3].
- now apply (IH y).
- exists x. repeat split; trivial. intros y [Y1 Y2].
destruct (Stage_lin_el H1 Y1) as [H|H]; trivial.
contradict H3. now exists y.
Qed.
(* Rank Function *)
Definition rank x a := Stage a /\ x <<= a /\ x nel a.
Fact rank_fun :
functional rank.
Proof.
intros x a b [H1[H2 H3]] [I1[I2 I3]].
destruct (Stage_tricho H1 I1) as [H|[H|H]]; trivial.
- exfalso. apply I3. now apply (Stage_swelled I1 H).
- exfalso. apply H3. now apply (Stage_swelled H1 H).
Qed.
Definition rho a :=
delta (rank a).
Definition rho' a :=
(union (frep power (frep rho a))).
Fact rho_rank_ex a b :
rank a b -> rank a (rho a).
Proof.
intros H. unfold rho.
now rewrite (delta_eq (@rank_fun a) H).
Qed.
Lemma rho'_rank a :
rank a (rho' a).
Proof.
induction (AxWF a) as [a _ IH]. repeat split.
- constructor. intros x [y[Y ->]] % frep_el.
constructor. apply frep_el in Y as [b [B ->]].
apply (rho_rank_ex (IH b B)).
- intros b B. apply Union. exists (power (rho b)). split.
+ apply frep_el. exists (rho b). split; trivial.
apply frep_el. now exists b.
+ apply Power. apply (rho_rank_ex (IH b B)).
- intros [x[X1 X2]] % Union. apply frep_el in X1 as [y[Y ->]].
apply (frep_el) in Y as [b[B1 B2]]. subst.
apply (rho_rank_ex (IH b B1)).
apply Power in X2. now apply X2.
Qed.
Fact rho_rho' x :
rho x = rho' x.
Proof.
apply (delta_eq (@rank_fun x)), rho'_rank.
Qed.
Fact ex_rank a :
ex (rank a).
Proof.
exists (rho' a). apply rho'_rank.
Qed.
Fact rho_rank a :
rank a (rho a).
Proof.
apply (rho_rank_ex (rho'_rank a)).
Qed.
Definition reachable x := exists y, Stage y /\ x el y.
Fact WF_reachable x :
reachable x.
Proof.
destruct (ex_rank x) as [y Y].
exists (power y). split.
- constructor. apply Y.
- apply Power, Y.
Qed.
Definition succ x := exists y, x = power y /\ Stage y.
Definition limit x := Stage x /\ x <<= union x.
Definition closed_stage x := forall a, a el x -> exists y, Stage y /\ y el x /\ a el y.
Fact Stage_dicho x :
x <=c Stage -> union x el x \/ x <<= union x.
Proof.
intros H. destruct (classic (x <<= union x)) as [J|J]; auto.
apply set_not_sub in J as [y[Y1 Y2]]. left.
cutrewrite (union x = y); trivial.
apply union_gel_eq. split; trivial.
intros z I. destruct (Stage_lin_el (H z I) (H y Y1)) as [J|J]; trivial.
exfalso. apply Y2. apply Union. now exists z.
Qed.
Lemma Stage_succ_limit x :
Stage x -> succ x \/ limit x.
Proof.
induction 1 as [x H _ | y H IH].
- left. exists x. auto.
- destruct (Stage_dicho H) as [H1|H1].
+ apply IH, H1.
+ right. split; try now constructor.
intros a (z&H2&H3) % Union.
apply Union. exists z. auto.
Qed.
Fact limit_closed_stage :
limit <=p closed_stage.
Proof.
intros x [H1 H2]. induction H1 as [x _ _ | y H1 IH].
- rewrite union_power_eq in H2. now apply power_above in H2.
- destruct (Stage_dicho H1) as [H3|H3]; try now apply IH.
intros b (a&H4&H5) % Union. exists a. auto.
Qed.
Lemma Stage_inhab x :
Stage x -> inhab x -> 0 el x.
Proof.
intros H1 (a&H2).
destruct (Stage_lin_el H1 Stage_eset) as [H3|H3].
- apply H3 in H2. auto.
- exact H3.
Qed.
Lemma limit_union x :
limit x -> closed_union (cl x).
Proof.
intros [H _] a I. now apply (Stage_union H).
Qed.
Lemma limit_power x :
limit x -> closed_power (cl x).
Proof.
intros H a I.
destruct (limit_closed_stage H I) as (y&Y1&Y2&Y3).
apply (Stage_power Y1) in Y3. destruct H as [H _].
destruct (Stage_lin_el (StageS Y1) H) as [J|J]; auto.
exfalso. apply Power in J. specialize (J y Y2).
now apply WF_no_loop in J.
Qed.
Lemma limit_upair x :
limit x -> closed_upair (cl x).
Proof.
intros H a b H1 H2.
destruct (limit_closed_stage H H1) as (y&Y1&Y2&Y3).
destruct (limit_closed_stage H H2) as (z&Z1&Z2&Z3).
destruct (Stage_lin Y1 Z1) as [I|I].
- apply Stage_trans with (x:=power z); try apply H.
+ now apply limit_power.
+ apply Stage_upair; auto.
- apply Stage_trans with (x:=power y); try apply H.
+ now apply limit_power.
+ apply Stage_upair; auto.
Qed.
Lemma limit_sep x :
limit x -> closed_sep (cl x).
Proof.
intros [H _] p a _ I. now apply (Stage_sep p H).
Qed.
Fact limit_Z x :
limit x -> inhab x -> closed_Z (cl x).
Proof.
intros H1 H2. split.
- apply Stage_trans, H1.
- destruct H1 as [H1 _], H2 as [y Y].
apply (Stage_swelled H1 Y). auto.
- now apply limit_upair.
- now apply limit_union.
- now apply limit_power.
- now apply limit_sep.
Qed.
Fact universe_trans :
universe <=p trans.
Proof.
intros u H. apply H.
Qed.
Fact universe_swelled :
universe <=p swelled.
Proof.
intros u H1 a b H2 H3.
apply (universe_trans H1) with (x:= power a).
- apply H1, H2.
- apply Power, H3.
Qed.
Lemma universe_rank a u :
universe u -> a el u -> rho a el u.
Proof.
intros H1 H2. induction (AxWF a) as [a _ IH].
rewrite rho_rho'. repeat apply H1; eauto using fres_eq.
- intros y [b[B ->]] % frep_el. apply IH; trivial.
now apply (universe_trans H1) with (x:=a).
- intros y [b[[c[C ->]] % frep_el ->]] % frep_el.
apply H1. apply IH; trivial.
now apply (universe_trans H1) with (x:=a).
Qed.
Fact universe_stage u :
universe u -> Stage u.
Proof.
intros H1. enough (union (sep Stage u) = u) as <-.
{ constructor. intros x H2 % sep_el. apply H2. }
apply Ext.
- intros a (b & (H2 & _) % sep_el &H3) % Union.
now apply (universe_trans H1) with (x:=b).
- intros a H2. apply Union. exists (power (rho a)). split.
+ apply sep_el. split.
* now apply H1, universe_rank.
* constructor. apply rho_rank.
+ apply Power, rho_rank.
Qed.
Fact universe_limit' u :
universe u -> limit u.
Proof.
intros H. split; try now apply universe_stage.
intros x I % universe_rank; trivial.
apply Union. exists (power (rho x)). split.
- now apply H.
- apply Power, rho_rank.
Qed.
Fact universe_limit_frep u :
universe u <-> (limit u /\ inhab u /\ closed_frep (cl u)).
Proof.
split; intros H.
- split; try now apply universe_limit'.
split; try apply H. exists 0. apply H.
- destruct H as [H1[H2 H3]].
split; trivial. now apply limit_Z.
Qed.
Lemma universe_limit u :
universe u <-> (limit u /\ inhab u /\ closed_rep (cl u)).
Proof.
split; intros H.
- split; try now apply universe_limit'. split.
+ exists 0. apply H.
+ unfold universe in H. now rewrite ZF_rep in H.
- destruct H as [H1[H2 H3]].
apply ZF_rep. repeat split; trivial.
+ apply Stage_trans, H1.
+ apply Stage_inhab; trivial; apply H1.
+ now apply limit_union.
+ now apply limit_power.
Qed.
Lemma universe_least u p :
universe u /\ p u -> exists v, least (fun v => universe v /\ p v) v.
Proof.
intros H. assert (SU : Stage u) by apply universe_stage, H.
pattern u in H. destruct (Stage_least SU H) as [v VL].
exists v. split; try apply VL. intros u' HU. apply VL.
split; try apply universe_stage; apply HU.
Qed.
End Stage.