Require Export Instances.

Section Stage.

Context { set : SetStruct }.
Context { ZFS : ZF set }.

Implicit Types x y z a b c u v : set.
Implicit Types p q : set -> Prop.

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] % upair_el; now subst.
Qed.

Fact Stage_sep x a p :
  Stage x -> a el x -> a ! p 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. 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 closed_union x := forall a, a el x -> union a el x.
Definition closed_power x := forall a, a el x -> power a el x.
Definition closed_upair x := forall a b, a el x -> b el x -> (upair a b) el x.
Definition closed_sep x := forall a p, a el x -> a ! p el x.

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 :
  limit <=p closed_union.
Proof.
  intros x [H _] a I. now apply (Stage_union H).
Qed.

Lemma limit_power :
  limit <=p closed_power.
Proof.
  intros x 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 :
  limit <=p closed_upair.
Proof.
  intros x 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 (y:=power z); try apply H.
    + now apply limit_power.
    + apply Stage_upair; auto.
  - apply Stage_trans with (y:=power y); try apply H.
    + now apply limit_power.
    + apply Stage_upair; auto.
Qed.

Lemma limit_sep :
  limit <=p closed_sep.
Proof.
  intros x [H _] a p I. now apply (Stage_sep p H).
Qed.

Definition closed_rep x :=
  forall R a, functional R -> (forall y z, R y z -> y el a -> z el x) -> a el x -> rep R a el x.

Definition closed_rep' x :=
  forall R a, functional R -> rep R a <<= x -> a el x -> rep R a el x.

Fact rep_closed_equiv x :
  closed_rep x <-> closed_rep' x.
Proof.
  split; intros H R a FR H1 H2; apply H; auto.
  - intros y z I1 I2. apply H1.
    apply Rep; trivial. now exists y.
  - intros z [y[Y1 Y2]] % Rep; trivial.
    now apply (H1 y).
Qed.

Definition universe u :=
  trans u /\ 0 el u /\ closed_union u /\ closed_power u /\ closed_rep u.

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 (y:= power a).
  - apply H1, H2.
  - apply Power, H3.
Qed.

Fact universe_ZF_closed u :
  universe u -> ZF_closed (fun x => x el u).
Proof.
  intros H. repeat split; try apply H.
  intros x y Y X. now apply H with (y:=x).
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; trivial.
  - congruence.
  - intros y z <- [b[B <-]] % frep_el. apply H1.
    apply IH; trivial. now apply H1 with (y:=a).
  - congruence.
  - intros y z <- H. apply IH; trivial.
    now apply H1 with (y:=a).
Qed.

Fact universe_stage u :
  universe u -> Stage u.
Proof.
  intros H1. enough (union (u ! Stage) = u) as <-.
  { constructor. intros x H2 % sep_el. apply H2. }
  apply Ext.
  - intros a (b & (H2 & _) % sep_el &H3) % Union.
    now apply H1 with (y:=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.

Lemma universe_limit u :
  universe u <-> (limit u /\ inhab u /\ closed_rep u).
Proof.
  split; intros H.
  - repeat split; try apply H.
    + now apply universe_stage.
    + intros x I % universe_rank; trivial.
      apply Union. exists (power (rho x)). split.
      * now apply H.
      * apply Power, rho_rank.
    + exists 0. apply H.
  - destruct H as [H1[H2 H3]]. repeat split; trivial.
    + apply Stage_trans, H1.
    + apply Stage_inhab; trivial; apply H1.
    + now apply limit_union.
    + now apply limit_power.
Qed.

End Stage.