Require Export Stage.

Section Infinity.

(* We assume a model of ZF and define binary union and adjunction *)

Context { M : ZFStruct }.
Context { MZF : ZF M }.

Lemma binunion_el x y z :
  z el binunion x y <-> z el x \/ z el y.
Proof.
  split; intros H.
  - apply Union in H as [y'[Y1 Y2]].
    apply pair_el in Y1 as [->| ->]; auto.
  - destruct H as [H|H]; apply Union.
    * exists x. split; trivial. apply Pair. now left.
    * exists y. split; trivial. apply Pair. now right.
Qed.

Definition adj x y :=
  binunion y (sing x).

Lemma adj_el x y z :
  z el adj x y <-> z el y \/ z = x.
Proof.
  split; intros H.
  - apply binunion_el in H as [H|H]; auto.
    apply sing_el in H as ->. now right.
  - destruct H as [H| ->]; apply binunion_el; auto.
    right. apply sing_el. reflexivity.
Qed.

Hypothesis MI :
  Inf M.

Definition om :=
  delta (fun om' => agree finpow om').

Lemma Infinity' :
  agree finpow om.
Proof.
  unfold om. destruct MI as [om' H].
  apply (delta_spec H). apply agree_unique.
Qed.

Lemma Infinity :
  forall x, x el om <-> exists n, x = powit n.
Proof.
  intros x. rewrite (Infinity' x).
  split; intros [n H]; exists n; now apply ZFExt.
Qed.

Definition OM :=
  union om.

(* OM is a limit stage *)

Lemma OM_powit n :
  powit n el OM.
Proof.
  apply Union. exists (powit (S n)). split.
  - apply Infinity. now exists (S n).
  - now apply Power.
Qed.

Lemma OM_ex_powit x :
  x el OM -> exists n, x el powit n.
Proof.
  intros [y[Y1 Y2]] % Union.
  apply Infinity in Y1 as [n ->].
  now exists n.
Qed.

Lemma OM_eset :
  0 el OM.
Proof.
  assert (H : eset = powit 0) by trivial.
  rewrite H. apply OM_powit.
Qed.

Lemma powit_stage n :
  Stage (powit n).
Proof.
  induction n.
  - apply Stage_eset.
  - now constructor.
Qed.

Lemma OM_stage :
  Stage OM.
Proof.
  constructor. intros y H.
  apply Infinity in H as [n ->].
  apply powit_stage.
Qed.

Lemma OM_limit :
  OM <<= union OM.
Proof.
  intros x [X[H1 H2]] % Union.
  apply Infinity in H1 as [n ->].
  apply Union. exists (powit n). split; trivial.
  apply OM_powit.
Qed.

Lemma limit_OM :
  limit OM.
Proof.
  split; auto using OM_stage, OM_limit.
Qed.

Inductive Fin : M -> Prop :=
| FinE : Fin 0
| FinA x y : Fin y -> Fin (adj x y).

Inductive HF x : Prop :=
HFI : (forall y, y el x -> HF y) -> Fin x -> HF x.

Fact HF_Fin x :
  HF x -> Fin x.
Proof.
  intros [_ H]. assumption.
Qed.

Lemma adj_sep x y :
  x el y -> y = adj x (sep (fun a => a <> x) y).
Proof.
  intros H. apply Ext; intros z Z.
  - destruct (classic (z = x)) as [-> | N]; apply adj_el; auto.
    left. apply sep_el. now split.
  - apply adj_el in Z as [Z| ->]; trivial.
    now apply sep_el in Z as [Z1 Z2].
Qed.

Lemma Fin_subset x y :
  Fin x -> y <<= x -> Fin y.
Proof.
  intros H. revert y. induction H as [|x z H IH].
  - intros y -> % sub_eset. constructor.
  - intros y HY. destruct (classic (x el y)) as [X|X].
    + rewrite -> (adj_sep X). constructor.
      apply IH. intros a [A1 A2] % sep_el.
      specialize (HY a A1). apply adj_el in HY as [A|A]; tauto.
    + apply IH. intros a A. specialize (HY a A).
      apply adj_el in HY as [I|I]; subst; tauto.
Qed.

(* Fin and HF are closed under replacement *)

Lemma rep_eset R :
  functional R -> rep R 0 = 0.
Proof.
  intros H. apply sub_eset.
  intros x [y[Y1 Y2]] % Rep; trivial.
  contradict (Eset Y1).
Qed.

Lemma rep_sing R x y :
  functional R -> R x y -> y = union (rep R (sing x)).
Proof.
  intros FR H. apply Ext; intros z Z.
  - apply Union. exists y. split; trivial.
    apply Rep; trivial. exists x. split; trivial.
    apply Pair. now left.
  - apply Union in Z as [b[B1 B2]].
    apply Rep in B1 as [a[A1 A2]]; trivial.
    apply pair_el in A1 as [A1|A1]; subst a; now rewrite (FR x y b H A2).
Qed.

Lemma rep_adj R x y :
  functional R -> rep R (adj x y) <<= adj (union (rep R (sing x))) (rep R y).
Proof.
  intros FR b [a[A1 A2]] % Rep; trivial.
  apply adj_el in A1 as [A1|A1].
  - apply adj_el. left. apply Rep; trivial. now exists a.
  - subst x. apply adj_el. right. now apply rep_sing.
Qed.

Lemma Fin_rep R x :
  functional R -> Fin x -> Fin (rep R x).
Proof.
  intros FR H. induction H as [|x y H IH].
  - rewrite rep_eset; trivial. constructor.
  - apply Fin_subset with (x:=adj (union (rep R (sing x))) (rep R y)).
    + now constructor.
    + now apply rep_adj.
Qed.

Lemma Fin_frep F x :
  Fin x -> Fin (frep F x).
Proof.
  intros H. rewrite rep_frep.
  apply Fin_rep; trivial. congruence.
Qed.

Lemma HF_rep :
  closed_rep HF.
Proof.
  intros R x FR H RR. split.
  - intros y [z[Z1 Z2]] % Rep; trivial.
    apply RR, Rep; trivial. now exists z.
  - apply Fin_rep; trivial. apply H.
Qed.

(* Fin and HF are closed under power *)

Lemma binunion_eset x :
  binunion 0 x = x.
Proof.
  apply Ext; intros y Y.
  - apply binunion_el in Y as [Y|Y]; auto.
  - apply binunion_el. now right.
Qed.

Lemma binunion_adj x y z :
  binunion (adj x z) y = adj x (binunion z y).
Proof.
  apply Ext; intros a A.
  - apply adj_el. apply binunion_el in A as [A|A].
    + apply adj_el in A as [A| ->]; auto.
      left. apply binunion_el. now left.
    + left. apply binunion_el. now right.
  - apply binunion_el. apply adj_el in A as [A | ->].
    + apply binunion_el in A as [A|A]; auto.
      left. apply adj_el. now left.
    + left. apply adj_el. now right.
Qed.

Lemma Fin_binunion x y :
  Fin x -> Fin y -> Fin (binunion x y).
Proof.
  intros H. revert y. induction H as [|x z H IH].
  - intros y FY. now rewrite binunion_eset.
  - intros y FY. rewrite binunion_adj.
    constructor. now apply IH.
Qed.

Lemma adj_power x y :
  power (adj x y) = binunion (power y) (frep (adj x) (power y)).
Proof.
  apply Ext; intros z Z.
  - apply Power in Z. destruct (classic (x el z)) as [H|H].
    + apply binunion_el. right. apply frep_el.
      exists (sep (fun a => a <> x) z). split; try now apply adj_sep.
      apply Power. intros a [A1 A2] % sep_el.
      specialize (Z a A1). apply adj_el in Z as [Z|Z]; tauto.
    + apply binunion_el. left. apply Power.
      intros a A. specialize (Z a A).
      apply adj_el in Z as [Z|Z]; trivial.
      subst. contradiction.
  - apply Power. intros a A. apply binunion_el in Z as [Z|Z].
    + apply Power in Z. apply adj_el. left. now apply Z.
    + apply frep_el in Z as [y'[Y1 % Power Y2]]. subst.
      apply adj_el. apply adj_el in A as [A | ->]; auto.
Qed.

Lemma pow_eset :
  power 0 = adj 0 0.
Proof.
  apply Ext; intros x X.
  - apply Power in X. apply sub_eset in X as <-.
    apply adj_el. now right.
  - apply adj_el in X as [X| ->].
    + contradict (Eset X).
    + apply Power. auto.
Qed.

Lemma power_Fin :
  closed_power Fin.
Proof.
  intros x. induction 1 as [|x y H IH].
  - rewrite pow_eset. repeat constructor.
  - rewrite adj_power. apply Fin_binunion; trivial.
    rewrite rep_frep. apply Fin_rep; trivial. congruence.
Qed.

Lemma HF_power :
  closed_power HF.
Proof.
  intros x [H1 H2]. split.
  - intros y Y % Power. constructor; auto.
    now apply (Fin_subset H2).
  - now apply power_Fin.
Qed.

(* HF is ZF-closed *)

Lemma HF_ctrans :
  ctrans HF.
Proof.
  intros x y [H]. apply H.
Qed.

Lemma HF_eset :
  HF 0.
Proof.
  constructor; auto using Fin.
Qed.

Lemma adj_union x y :
  union (adj x y) = binunion x (union y).
Proof.
  apply Ext; intros z H.
  - apply binunion_el.
    apply Union in H as [z'[H1 H2]].
    apply adj_el in H1 as [H1| ->]; auto.
    right. apply Union. now exists z'.
  - apply Union.
    apply binunion_el in H as [H|H].
    + exists x. split; trivial. apply adj_el; auto.
    + apply Union in H as [z'[H1 H2]].
      exists z'. split; trivial. apply adj_el; auto.
Qed.

Lemma HF_union :
  closed_union HF.
Proof.
  intros x [H1 H2]. constructor.
  - intros z [y[Y1 Y2]] % Union.
    apply H1 in Y1 as [Y1]. now apply Y1.
  - induction H2.
    + rewrite union_eset. constructor.
    + rewrite adj_union. apply Fin_binunion.
      * apply HF_Fin, H1, adj_el. now right.
      * apply IHFin. intros z H.
        apply H1, adj_el. now left.
Qed.

Fact HF_ZF :
  closed_ZF HF.
Proof.
  apply ZF_rep.
  split; try apply HF_ctrans.
  split; try apply HF_eset.
  split; try apply HF_union.
  split; try apply HF_power.
  apply HF_rep.
Qed.

Lemma eset_HF :
  HF 0.
Proof.
  split; auto using FinE.
Qed.

Lemma powit_HF n :
  HF (powit n).
Proof.
  induction n as [| n IH].
  - apply eset_HF.
  - now apply HF_power.
Qed.

Lemma powit_Fin n :
  Fin (powit n).
Proof.
  induction n.
  - constructor.
  - now apply power_Fin.
Qed.

Lemma OM_Fin x :
  x el OM -> Fin x.
Proof.
  intros [n H] % OM_ex_powit.
  destruct n.
  - contradiction (Eset H).
  - apply (Fin_subset (powit_Fin n)).
    now apply Power.
Qed.

Lemma OM_rho_el x :
  x el OM -> rho x el OM.
Proof.
  intros [X[X1 X2]] % Union.
  apply Infinity in X1 as [n ->].
  apply (Stage_swelled OM_stage (x:=powit n)).
  - apply OM_powit.
  - destruct (@Stage_lin _ _ (rho x) (powit n)) as [H|H].
    + apply rho_rank.
    + apply powit_stage.
    + assumption.
    + exfalso. apply H in X2. now apply rho_rank in X2.
Qed.

Definition chain x :=
  forall y z, y el x -> z el x -> y <<= z \/ z <<= y.

Lemma chain_sub x y :
  x <<= y -> chain y -> chain x.
Proof.
  intros H1 H2 a b A B. apply H2; auto.
Qed.

Lemma adj_sub x y :
  y <<= adj x y.
Proof.
  intros z Z. apply adj_el. now left.
Qed.

Lemma Fin_chain_max x :
  Fin x -> inhab x -> chain x -> union x el x.
Proof.
  induction 1 as [|x y H IH]; intros H1 H2.
  - now contradiction (inhab_neq H1).
  - destruct (classic (inhab y)) as [H3|H3].
    + specialize (IH H3 (chain_sub (@adj_sub x y) H2)).
      assert (XA : x el adj x y) by (apply adj_el; auto).
      assert (YA : (union y) el adj x y) by (apply adj_el; auto).
      destruct (H2 x (union y) XA YA) as [XY|YX]; apply adj_el.
      * left. cutrewrite (union (adj x y) = union y); trivial. apply Ext.
        -- apply union_sub. intros a [A| ->] % adj_el; trivial.
           now apply union_el_sub.
        -- apply union_el_sub. apply adj_el. now left.
      * right. apply Ext.
        -- apply union_sub. intros a [A| ->] % adj_el; trivial.
           intros b B. apply YX. apply Union. now exists a.
        -- apply union_el_sub. apply adj_el. now right.
    + apply adj_el. right. apply Ext.
      * apply union_sub. intros a [A| ->] % adj_el; trivial.
        contradict H3. now exists a.
      * apply union_el_sub. apply adj_el. now right.
Qed.

Lemma HF_rho x :
  HF x -> rho x el OM.
Proof.
  induction 1 as [x _ IH H].
  pose (X := (frep power (frep rho x))).
  destruct (classic (inhab x)) as [[z Z]| -> % inhab_not].
  - assert (H3 : chain X).
    + intros a b [a'[A ->]] % frep_el [b'[B ->]] % frep_el.
      apply frep_el in A as [a[A ->]]. apply frep_el in B as [b[B ->]].
      apply Stage_lin; constructor; apply rho_rank.
    + assert (IR : inhab X).
      { exists (power (rho z)). apply frep_el. exists (rho z).
        split; trivial. apply frep_el. now exists z. }
      apply Fin_chain_max in H3; try (repeat apply Fin_frep; trivial).
      apply frep_el in H3 as [Y[[y [Y1 Y2]] % frep_el Y3]]; subst.
      rewrite rho_rho'. unfold rho'. fold X. rewrite Y3.
      apply (limit_power limit_OM). now apply IH.
  - cutrewrite (rho 0 = 0); try apply OM_eset.
    apply (rank_fun (rho_rank 0)).
    repeat split; auto using Stage_eset, Eset.
Qed.

Lemma HF_OM :
  agree HF OM.
Proof.
  intros x. split; intros H.
  - apply Union in H as [y [[n ->] % Infinity Y2]].
    destruct (powit_HF n) as [H _]. now apply H.
  - apply (Stage_swelled OM_stage (x:=rho x)).
    + now apply HF_rho.
    + apply rho_rank.
Qed.

(* OM is closed under replacement and hence a universe *)

Lemma OM_repclosed :
  closed_rep (cl OM).
Proof.
  intros R x FR X XR. apply HF_OM.
  apply HF_rep; trivial.
  - now apply HF_OM.
  - intros z [y[H1 H2]] % Rep; trivial.
    apply HF_OM, XR, Rep; trivial. now exists y.
Qed.

Theorem OM_universe :
  universe OM.
Proof.
  apply universe_limit. repeat split.
  - apply OM_stage.
  - apply OM_limit.
  - exists eset. now apply OM_eset.
  - apply OM_repclosed.
Qed.

Theorem OM_ZF1 :
  ZFge 1 M.
Proof.
  split; trivial.
  exists (power OM), OM. simpl.
  split; auto using power_eager.
  split; auto using OM_universe.
Qed.

(* OM is in fact the least limit and universe *)

Lemma om_limit x :
  limit x -> inhab x -> om <<= x.
Proof.
  intros H1 H2 y Y.
  apply Infinity in Y as [n ->].
  induction n as [|n IH].
  - apply Stage_inhab; firstorder.
  - now apply limit_power.
Qed.

Lemma om_infinite :
  ~ Fin om.
Proof.
  intros H. apply Fin_chain_max in H.
  - apply Infinity in H as [n H].
    apply (WF_no_loop (x:=powit n)).
    rewrite <- H at 2. apply OM_powit.
  - exists 0. apply Infinity. now exists O.
  - intros x y [n ->] % Infinity [n' ->] % Infinity.
    apply Stage_lin; apply powit_stage.
Qed.

Lemma limit_infinite x :
  limit x -> inhab x -> ~ Fin x.
Proof.
  intros H1 H2 H3. apply om_infinite.
  now apply (Fin_subset H3), om_limit.
Qed.

Fact OM_least_limit x :
  limit x -> inhab x -> OM <<= x.
Proof.
  intros H1 H2. assert (S1 : Stage x) by apply H1.
  assert (S2 : Stage OM) by apply universe_stage, OM_universe.
  destruct (Stage_lin_el S2 S1) as [I|I]; trivial.
  exfalso. apply (limit_infinite H1 H2). now apply OM_Fin.
Qed.

Corollary OM_least u :
  universe u -> OM <<= u.
Proof.
  intros H % universe_limit.
  apply OM_least_limit; apply H.
Qed.

End Infinity.

Section Inf.

  Context { M : ZFStruct }.
  Context { MZF1 : ZFge 1 M }.

  Instance MZF : ZF M :=
    proj1 MZF1.

  Fact MI :
    Inf M.
  Proof.
    destruct MZF1 as [MZF[X[U[_[HU _]]]]].
    pose (om := sep finpow U).
    exists om. intros x. split; intros H.
    - now apply sep_el in H.
    - destruct H as [n ->]. apply sep_el.
      split; try now exists n.
      induction n; simpl; now apply HU.
  Qed.

End Inf.