Set Theory

Require Import Prelude.

Notation "p '<=p' q" := (forall z, p z -> q z) (at level 70).

We assume a type of sets with a membership relation

Axiom set : Type.
Axiom elem : set -> set -> Prop.

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

Notation "x 'el' y" := (elem x y) (at level 70).
Notation "x 'nel' y" := (~ elem x y) (at level 70).

Russell's class agrees with no set

Definition agree p x := forall z, z el x <-> p z.

Definition small p := exists x, agree p x.

Lemma Russell :
~ small (fun z => z nel z).
Proof.
intros [x A]. specialize (A x). simpl in *. tauto.
Qed.

Inclusion ordering

Definition sub x y := forall z, z el x -> z el y.
Notation "x '<<=' y" := (sub x y) (at level 70).
Notation "x << y" := (x <<= y /\ x <> y) (at level 70).

Lemma sub_refl x :
  x <<= x.
Proof.
  unfold sub. auto.
Qed.

Lemma sub_trans x y z :
  x <<= y -> y <<= z -> x <<= z.
Proof.
  unfold sub. auto.
Qed.

Hint Unfold sub.
Hint Resolve sub_refl.

Extensionality axiom

Axiom Ext :
  forall x y, x <<= y -> y <<= x -> x = y.

Definition least p x := p x /\ forall y, p y -> x <<= y.
Definition unique p := forall x y, p x -> p y -> x = y.

Fact least_unique p :
  unique (least p).
Proof.
  intros x y [H1 H2] [H3 H4]. apply Ext; auto.
Qed.

Fact agree_unique p :
  unique (agree p).
Proof.
  intros a b H1 H2. apply Ext; intros x.
  - intros H3 % H1 % H2. exact H3.
  - intros H3 % H2 % H1. exact H3.
Qed.

Empty set and adjunction

Axiom eset : set.
Notation "0" := eset.

Axiom Eset :
  forall z, z nel 0.

Lemma eset_sub x :
  0 <<= x.
Proof.
  intros z H. exfalso. eapply Eset, H.
Qed.

Lemma eset_unique x :
  (forall z, z nel x ) -> x = 0.
Proof.
  intros H. apply Ext.
  - intros z H1. contradiction (H z H1).
  - apply eset_sub.
Qed.

Lemma sub_eset x :
  x <<= 0 -> x = 0.
Proof.
  intros H. apply eset_unique. intros z H1 % H.
  contradiction (Eset H1).
Qed.

Hint Resolve eset_sub sub_eset.

Hint Extern 4 =>
match goal with
  | [ H : _ el 0 |- _ ] => exfalso; apply (Eset H)
end.

Notation inhab x := (exists z, z el x).

Lemma inhab_not x :
  ~ inhab x <-> x = 0.
Proof.
  split.
  - intros H. apply eset_unique. intros z H1. eauto.
  - intros -> [z H]. eauto.
Qed.

Lemma inhab_neq x :
  inhab x -> x <> 0.
Proof.
  intros [z H] ->. eauto.
Qed.

Hint Resolve inhab_neq.

Hint Extern 4 =>
match goal with
  | [ H : inhab 0 |- _ ] => exfalso; now apply (inhab_neq H)
end.

Axiom adj : set -> set -> set.
Notation "x @ y" := (adj x y) (at level 65, right associativity).

Axiom Adj : forall x y z, z el x @ y <-> z = x \/ z el y.

Lemma Adj' x y z :
  z = x \/ z el y -> z el x @ y.
Proof.
  apply Adj.
Qed.

Hint Resolve Adj'.

Lemma adj_sub' a x y :
  a el y -> x <<= y -> a @ x <<= y.
Proof.
  intros H1 H2 z [->|H3] % Adj; auto.
Qed.

Lemma adj_sub x y z :
  x @ y <<= z <-> x el z /\ y <<= z.
Proof.
  split.
  - unfold sub. auto.
  - intros [H1 H2]. now apply adj_sub'.
Qed.

Lemma adj_eset x y :
  x @ y <> 0.
Proof.
  apply inhab_neq. eauto.
Qed.

Lemma adj_inhab x y :
  inhab (x @ y).
Proof.
  exists x. auto.
Qed.

Lemma adj_inj a x b y :
  a @ x = b @ y -> a = b \/ a el y.
Proof.
  intros H. apply Adj. rewrite <- H. auto.
Qed.

Lemma adj_sub_eset a x :
  ~ a @ x <<= 0.
Proof.
  intros H. eapply Eset; auto.
Qed.

Fact adj_el_eq x y :
  x el y -> x @ y = y.
Proof.
  intros H. apply Ext.
  - apply adj_sub; auto.
  - auto.
Qed.

Hint Resolve adj_sub' adj_eset adj_inhab.

Hint Extern 4 =>
match goal with
| [ H : _ @ _ = 0 |- _ ] => contradiction (adj_eset H)
| [ H : 0 = _ @ _ |- _ ] => symmetry in H; contradiction (adj_eset H)
| [ H : _ @ _ <<= 0 |- _ ] => contradiction (adj_sub_eset H)
end.

Singletons

Notation sing x := (x@0).

Lemma sing_el x y :
  x el sing y <-> x =y.
Proof.
  rewrite Adj. intuition.
Qed.

Hint Extern 4 =>
match goal with
| [ H : _ el sing _ |- _ ] => apply sing_el in H as ->
end.

Lemma sing_inj x y :
  sing x = sing y -> x = y.
Proof.
  cbn.
  intros H % adj_inj. intuition.
Qed.

Lemma sing_eq x y :
  x = sing y -> y el x.
Proof.
  intros ->. auto.
Qed.

Unordered pairs

Notation upair x y := (x@y@0).

Lemma upair_sing x y z :
  upair x y = sing z -> x = z /\ y = z.
Proof.
  intros H. split; apply sing_el; rewrite <- H; auto.
Qed.

Lemma upair_el z x y :
  z el upair x y <-> z = x \/ z = y.
Proof.
  split.
  - intros [->|[->|H1] % Adj] % Adj; auto.
  - intros [->| ->]; auto.
Qed.

Lemma upair_inj x y a b :
  upair x y = upair a b -> x =a /\ y =b \/ x =b /\ y =a.
Proof.
  intros H1.
  assert (H2: x=a \/ x=b).
  { apply upair_el. rewrite <-H1. auto. }
  assert (H3: y=a \/ y=b).
  { apply upair_el. rewrite <-H1. auto. }
  assert (H4: a=x \/ a=y).
  { apply upair_el. rewrite H1. auto. }
  assert (H5: b=x \/ b=y).
  { apply upair_el. rewrite H1. auto. }
  intuition.
Qed.

Ordered pairs

Definition opair x y := upair (sing x) (upair x y).

Lemma opair_inj x y a b :
  opair x y = opair a b -> x =a /\ y =b.
Proof.
  intros [[H1 H2]|[H1 H2]] % upair_inj.
  - apply sing_inj in H1 as <-.
    apply upair_inj in H2. intuition congruence.
  - apply upair_sing in H2 as [-> ->].
    symmetry in H1. apply upair_sing in H1 as [_ ->].
    auto.
Qed.

Numerals

Definition sigma x := x@x.
Arguments sigma / x.

Fact sigma_auto z x :
z = x \/ z el x -> z el sigma x.
Proof.
cbn. auto.
Qed.

Hint Resolve sigma_auto.

Technical remark. Defining sigma as a function has the consequence that we loose the automation we have registered for adjunction. Defining sigma x as notation for x@x preserves the automation but later on it will be essential to have sigma as a function.

Inductive Num : set -> Prop :=
| NumO : Num 0
| NumS x : Num x -> Num (sigma x).

Definition trans x := forall y, y el x -> y <<= x.

Lemma eset_trans :
  trans 0.
Proof.
  hnf. auto.
Qed.

Lemma sigma_trans x :
  trans x -> trans (sigma x).
Proof.
  intros H1 a [->|H2] % Adj b H3.
  - auto.
  - apply H1 in H2. auto.
Qed.

Fact Num_trans x :
  Num x -> trans x.
Proof.
  induction 1 as [|x _ IH].
  - unfold trans. auto.
  - auto using sigma_trans.
Qed.

Lemma sigma_inj_sub x y :
  trans y -> sigma x <<= sigma y -> x <<= y.
Proof.
  intros H1 H2 z H3.
  assert (x el sigma y) as [->|H4] % Adj by auto.
  - exact H3.
  - apply H1 in H4. auto.
Qed.

Lemma sigma_inj x y :
  trans x -> trans y -> sigma x = sigma y -> x = y.
Proof.
  intros Hx Hy H.
  apply Ext; apply sigma_inj_sub; try rewrite H; auto.
Qed.

Fact Num_eset x :
  Num x -> x = 0 \/ 0 el x.
Proof.
  induction 1 as [|x _ [->|IH]]; auto.
Qed.

Fact Num_mono_el x y :
  Num y -> x el y -> sigma x el sigma y.
Proof.
  induction 1 as [|y _ IH].
  - auto.
  - intros [<-|H] % Adj; auto.
Qed.

Theorem Num_tricho x y :
  Num x -> Num y -> x el y \/ x = y \/ y el x.
Proof.
  intros Hx. revert y.
  induction Hx as [|x Hx IH]; intros y Hy.
  - apply Num_eset in Hy. intuition.
  - destruct Hy as [|y Hy].
    + apply Num_eset in Hx. intuition.
    + destruct (IH y Hy) as [H|[<-|H]];
        auto using Num_mono_el.
Qed.

Fact Num_lin_sigma x y :
  Num x -> Num y -> x <<= y \/ sigma y <<= x.
Proof.
  intros Hx Hy.
  destruct (Num_tricho Hx Hy) as [H|[<-|H]].
  - apply (Num_trans Hy) in H. auto.
  - auto.
  - right. intros z [->|H1] % Adj. exact H.
    apply (Num_trans Hx H H1).
Qed.

Fact Num_lin_el x y :
  Num x -> Num y -> x <<= y \/ y el x.
Proof.
  intros Hx Hy.
  destruct (Num_lin_sigma Hx Hy) as [H|H].
  - auto.
  - right. apply H. cbn; auto.
Qed.

Fact Num_lin x y :
  Num x -> Num y -> x <<= y \/ y <<= x.
Proof.
  intros Hx Hy.
  destruct (Num_lin_el Hx Hy) as [H|H].
  - auto.
  - right. now apply Num_trans.
Qed.

Fact Num_strict x :
  Num x -> x nel x.
Proof.
  induction 1 as [|x H IH].
  - auto.
  - intros [H1|H1] % Adj.
    + apply IH. rewrite <-H1 at 2. cbn. auto.
    + apply IH. apply (Num_trans H H1). cbn. auto.
Qed.

Fact Num_cum x y :
  Num x -> Num y -> x el y <-> x << y.
Proof.
  intros Hx Hy. split.
  - intros H. split. now apply Num_trans.
    intros <-. now apply (Num_strict Hx).
  - intros [H1 H2].
    destruct (Num_lin_el Hy Hx) as [H3|H3].
   + contradiction H2. now apply Ext.
    + exact H3.
Qed.

Fact Num_mono x y :
  Num x -> Num y -> x <<= y -> sigma x <<= sigma y.
Proof.
  intros Hx Hy H z [->|H1] % Adj.
  - apply Num_cum. exact Hx. now constructor.
    split. now auto. intros ->.
    apply (Num_strict Hy). auto.
  - auto.
Qed.

Fact Num_closed x y :
  Num x -> y el x -> Num y.
Proof.
  induction 1 as [|x H IH].
  - auto.
  - intros [->|H1] % Adj; auto.
Qed.

Fact Num_no_loop2 x y :
  Num x -> x el y -> y nel x.
Proof.
  intros H1 H2 H3.
  apply (Num_strict H1).
  apply (Num_trans H1) in H3. auto.
Qed.

Exercise: Propostional decidability of numerals

Notation xm P := (P \/ ~ P).

Lemma ext_xm x y :
  xm (x <<= y) -> xm (y <<= x) -> xm (x = y).
Proof.
  intros [H1|H1].
  - intros [H2|H2].
    + left. now apply Ext.
    + right. intros <-. auto.
  - intros _. right. intros <-. auto.
Qed.

Fact Num_el_xm x y :
  Num x -> Num y -> xm (x el y).
Proof.
  intros Hx Hy.
    destruct (Num_tricho Hx Hy) as [H|[<-|H]].
    + auto.
    + auto using Num_strict.
    + auto using Num_no_loop2.
Qed.

Fact Num_sub_xm x y :
  Num x -> Num y -> xm (x <<= y).
Proof.
  intros Hx Hy.
    destruct (Num_tricho Hx Hy) as [H|[<-|H]].
    + auto using (Num_trans Hy).
    + auto.
    + right. intros H1. apply H1 in H.
      apply (Num_strict Hy H).
Qed.

Fact Num_eq_xm x y :
  Num x -> Num y -> xm (x = y).
Proof.
  intros. apply ext_xm; apply Num_sub_xm; auto.
Qed.

Exercise: Numerals and numbers

Fixpoint num n : set :=
  match n with
    | 0 => 0
    | S n' => sigma (num n')
  end.

Lemma num_Num n :
  Num (num n).
Proof.
  induction n; now constructor.
Qed.

Fact Num_num x :
  Num x <-> exists n, x = num n.
Proof.
  split.
  - induction 1 as [|x _ [n IH]].
    + now exists O.
    + exists (S n). cbn. now f_equal.
- intros [n ->]. apply num_Num.
Qed.

Lemma num_le m n :
  m < n -> num m el num n.
Proof.
  revert m; induction n as [|n IH]; cbn; intros m H.
  - exfalso ; omega.
  - assert (m = n \/ m < n) as [->|H1] by omega; auto.
Qed.

Lemma num_el x n :
  x el num n -> exists m, m < n /\ x = num m.
Proof.
  induction n as [|n IH]; cbn.
  - auto.
  - intros [->|H] % Adj.
    + exists n. intuition; omega.
    + apply IH in H as [m [H ->]].
      exists m. intuition; omega.
Qed.

Lemma num_inj m n :
  num m = num n -> m = n.
Proof.
  revert n; induction m as [|m IH]; intros [|n] H; cbn in H.
  - auto.
  - auto.
  - auto.
  - f_equal. apply IH.
    apply sigma_inj; auto using num_Num, Num_trans.
Qed.

Lemma num_el_num m n :
  num m el num n <-> m < n.
Proof.
  split.
  - intros [k [H H']] % num_el.
    apply num_inj in H' as ->. exact H.
  - apply num_le.
Qed.

Lemma num_sub_num m n :
  num m <<= num n <-> m <= n.
Proof.
  assert (m<n \/ m=n \/ n<m) as [H|[->|H]] by omega.
  - split. omega. intros _.
    apply Num_trans; auto using num_Num, Num_trans, num_le.
  - intuition.
  - split; [|omega]. intros H1. exfalso.
    revert H. intros H % num_le % H1 % num_el_num. omega.
Qed.

Finite sets

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

Fact Fin_eset_inhab x :
  Fin x -> x = 0 \/ inhab x.
Proof.
  intros H. destruct H as [|a x _]; auto.
Qed.

Definition chain x := forall a b, a el x -> b el x -> a <<= b \/ b <<= a.
Definition gel x u := u el x /\ forall z, z el x -> z <<= u.

Fact chain_adj a x :
  chain (a@x) -> chain x.
Proof.
  intros H b c Ha Hb. apply H; auto.
Qed.

Fact Fin_chain_gel x :
  Fin x -> inhab x -> chain x -> exists u, gel x u.
Proof.
  induction 1 as [|a x H IH]; intros H1 H2.
  - exfalso. auto.
  - apply Fin_eset_inhab in H as [->|H].
    + exists a. split. now auto. intros z [-> |H3] % Adj; auto.
    + destruct (IH H (chain_adj H2)) as (u&H3&H4).
      assert (a <<= u \/ u <<= a) as [H5|H5].
      * apply H2; auto.
      * exists u. split. now auto. intros z [->|H6] % Adj; auto.
      * exists a. split. now auto.
        intros y [->|H6] % Adj. now auto.
        specialize (H4 y H6). auto.
Qed.

Hereditarily finite sets

Inductive HF : set -> Prop :=
| HFE : HF 0
| HFA x y : HF x -> HF y -> HF (x @ y).

Fact HF_fin x :
  HF x -> Fin x.
Proof.
  induction 1; now constructor.
Qed.

Fact Num_HF x :
  Num x -> HF x.
Proof.
  induction 1; now constructor.
Qed.

Fact HF_closed x y :
  HF x -> y el x -> HF y.
Proof.
  induction 1 as [|x1 x2 H1 _ _ IH2]; intros H.
  - auto.
  - apply Adj in H as [->|H]; auto.
Qed.

Lemma adj_el_xm z a x :
  xm (z = a) -> xm (z el x) -> xm (z el a @ x).
Proof.
  intros [->|H1]. now auto.
  intros [H2|H2]. now auto.
  right. intros [->|H3] % Adj; auto.
Qed.

Lemma adj_sub_xm a x y :
  xm (a el y) -> xm (x <<= y) -> xm (a @ x <<= y).
Proof.
  intros [H1|H1].
  - intros [H2|H2].
    + auto.
    + right. intros H3 % adj_sub. tauto.
  - intros _. right. contradict H1. auto.
Qed.

Lemma HF_xm_eset_el x :
  HF x -> xm (0 el x).
Proof.
  induction 1 as [|a x Ha _ _ IHx].
  - auto.
  - apply adj_el_xm.
    + destruct Ha; auto.
    + auto.
Qed.

Lemma HF_xm x y :
  HF x -> HF y ->
  xm (x el y) /\ xm (y el x) /\ xm (x <<= y) /\ xm (y <<= x).
Proof.
  intros Hx. revert y.
  induction Hx as [|a x Ha IHa Hx IHx]; intros y Hy.
  - repeat split.
    + apply HF_xm_eset_el, Hy.
    + auto.
    + auto.
    + destruct Hy; auto.
  - induction Hy as [|b y Hb IHb Hy IHy]; repeat split.
    + auto.
    + apply HF_xm_eset_el. now constructor.
    + auto.
    + auto.
    + apply adj_el_xm.
      * apply ext_xm; apply IHb.
      * apply IHy.
    + apply adj_el_xm.
      * apply ext_xm; apply IHa; now constructor.
      * apply IHx. now constructor.
    + apply adj_sub_xm.
      * apply IHa. now constructor.
      * apply IHx. now constructor.
    + apply adj_sub_xm.
      * apply IHb.
      * apply IHy.
Qed.

Fact HF_list x :
  HF x -> exists A, (forall z, z el x <-> In z A ) /\ (forall z, In z A -> HF z ).
Proof.
  induction 1 as [|a x Ha _ Hx IH].
  - exists nil. firstorder.
  - destruct IH as (A&H1&H2).
    exists (a::A). split; intros z; cbn.
    + split.
      * intros [->|H3] % Adj. now auto.
        right; apply H1, H3.
      * intros [<-|H3]. now auto.
        apply H1 in H3. auto.
    + intros [<-|H3]; auto.
Qed.

Fact HF_list' A :
  (forall z, In z A -> HF z ) -> exists x, forall z, z el x <-> In z A.
Proof.
  intros H.
  induction A as [|a A IH].
  - exists 0. firstorder.
  - destruct IH as (x&H1). firstorder.
    exists (a@x). intros z. cbn. rewrite Adj, <- H1.
    intuition.
Qed.

Well-founded sets

Notation "x '<=c' p" := (forall z, z el x -> p z) (at level 70, only parsing).

Inductive WF : set -> Prop :=
| WFI x : x <=c WF -> WF x.

Lemma WF_closed x y :
  WF x -> y el x -> WF y.
Proof.
  intros [z H] H1. auto.
Qed.

Hint Resolve WF_closed.

Lemma WF_sub_closed x y :
  WF x -> y <<= x -> WF y.
Proof.
  intros [z H] H1. constructor. auto.
Qed.

Lemma WF_eset :
  WF 0.
Proof.
  constructor. auto.
Qed.

Lemma WF_adj x y :
  WF x -> WF y -> WF (x @ y).
Proof.
  intros H1 H2. constructor. intros z [->|H3] % Adj.
  - exact H1.
  - revert H2 H3. apply WF_closed.
Qed.

Lemma HF_WF x :
  HF x -> WF x.
Proof.
  induction 1; auto using WF_eset, WF_adj.
Qed.

Lemma WF_no_loop x :
  WF x -> x el x -> False.
Proof.
  induction 1 as [x _ IH]. eauto.
Qed.

Lemma WF_no_loop2 x y :
  WF x -> y el x -> x el y -> False.
Proof.
  intros H; revert y. induction H as [x _ IH]. eauto.
Qed.

Lemma WF_no_loop3 x y z :
  WF x -> z el y -> y el x -> x el z -> False.
Proof.
  intros H; revert y z. induction H as [x _ IH]. eauto.
Qed.

Lemma WF_unrealizable :
  ~ small WF.
Proof.
  intros [x H].
  assert (WF x) as H1.
  { constructor. apply H. }
  apply (WF_no_loop H1). apply H, H1.
Qed.

Lemma WF_sigma_inj x y :
  WF x -> sigma x = sigma y -> x = y.
Proof.
  intros H1 H2.
  destruct (adj_inj H2) as [->|H3]. reflexivity.
  symmetry in H2. apply adj_inj in H2 as [->|H2]. reflexivity.
  exfalso. revert H3. now apply WF_no_loop2.
Qed.

Lemma WF_sigma_notin x :
  WF x -> sigma x nel x.
Proof.
  intros H1 H2. apply (WF_no_loop2 H1 H2). auto.
Qed.

Lemma WF_sigma_neq x :
  WF x -> sigma x <> x.
Proof.
  intros H1 H2.
  apply WF_no_loop with (x:= x).
  - auto.
  - rewrite <- H2 at 2. auto.
Qed.

Fact WF_min p (XM: forall P, xm P) :
  ex p -> p <=p WF -> exists x, p x /\ forall y, p y -> y nel x.
Proof.
  intros (x&H2) H1.
  induction (H1 x H2) as [x H IH].
  destruct (XM (exists y, y el x /\ p y)) as [(y&H3&H4)|H3].
  - now apply (IH y).
  - exists x. split. exact H2.
    intros y H4. contradict H3. eauto.
Qed.

HFT characterisation of numerals

Definition HFT x := HF x /\ trans x /\ x <=c trans.

Fact HFT_closed x :
  HFT x -> x <=c HFT.
Proof.
  intros (H1&H2&H3) y H4. repeat split.
  - apply (HF_closed H1 H4).
  - apply H3, H4.
  - intros z H5 % (H2 y H4). auto.
Qed.

Fact Num_trans_gel x u :
  trans x -> x <=c Num -> gel x u -> x = sigma u.
Proof.
  intros H1 H2 [H3 H4]. apply Ext; intros y.
  - intros H5.
    destruct (Num_tricho (H2 y H5) (H2 u H3)) as [H6|[->|H6]].
    + auto.
    + auto.
    + contradiction (Num_strict (H2 _ H3)).
      apply (H4 y H5), H6.
  - intros [->|H5] % Adj. exact H3.
    apply H1 in H3. auto.
Qed.

Fact Fin_trans_Num x :
  Fin x -> trans x -> x <=c Num -> Num x.
Proof.
  intros H1 H2 H3.
  destruct (Fin_eset_inhab H1) as [->|H4]. now constructor.
  destruct (Fin_chain_gel H1 H4 ) as [u H5].
  { intros a b Ha Hb. apply Num_lin; auto. }
  rewrite (Num_trans_gel H2 H3 H5).
  constructor. apply H3, H5.
Qed.

Theorem HFT_Num x :
  HFT x <-> Num x.
Proof.
  split; intros H.
  - assert (WF x) as H1 by apply HF_WF, H.
    induction H1 as [x _ IH].
    apply Fin_trans_Num.
    + apply HF_fin, H.
    + destruct H as (_&H&_). exact H.
    + intros y H1. apply (IH y H1).
      revert H1. apply HFT_closed, H.
  - split. now apply Num_HF.
    split. now apply Num_trans.
    intros y H1. eapply Num_trans, Num_closed; eauto.
Qed.

Union

Axiom union : set -> set.

Axiom Union :
  forall x z, z el union x <-> exists y, y el x /\ z el y.

Notation upbnd x u := (forall z, z el x -> z <<= u).

Fact union_el_sub x y :
  x el y -> x <<= union y.
Proof.
  intros H z H1. apply Union. eauto.
Qed.

Lemma union_sub x u :
  upbnd x u -> union x <<= u.
Proof.
  intros H z [y [H1 H2]] % Union.
  now apply (H y).
Qed.

Hint Resolve union_el_sub union_sub.

Fact union_trans_sub x :
  trans x <-> union x <<= x.
Proof.
  split.
  - intros H z (y&H1&H2) % Union. apply H in H1. auto.
  - intros H y H1 % union_el_sub. auto.
Qed.

Lemma union_mono x y :
  x <<= y -> union x <<= union y.
Proof.
  auto.
Qed.

Lemma union_lub u x :
  union x = u <-> upbnd x u /\ forall v, upbnd x v -> u <<= v.
Proof.
   split.
  - intros <-. split.
    + intros z. apply union_el_sub.
    + apply union_sub.
  - intros [H1 H2]. apply Ext.
    + apply union_sub, H1.
    + apply H2. intros z. apply union_el_sub.
Qed.

Fact union_gel x :
  union x el x -> gel x (union x).
Proof.
  unfold gel. auto.
Qed.

Fact union_gel_eq x u :
  gel x u -> union x = u.
Proof.
  intros [H1 H2]. apply union_lub; auto.
Qed.

Lemma union_eset :
  union 0 = 0.
Proof.
  apply union_lub. auto.
Qed.

Lemma union_sing x :
  union (sing x) = x.
Proof.
  apply union_lub. auto.
Qed.

Fact union_sigma x :
  trans x -> union (sigma x) = x.
Proof.
  intros H. apply union_lub. split.
  - intros z [->|H1] % Adj; auto.
  - auto.
Qed.

Fact Num_pred x :
  Num x -> union (sigma x) = x.
Proof.
  intros H % Num_trans % union_sigma. exact H.
Qed.

Fact Num_either x :
  Num x -> x = 0 \/ x = sigma (union x).
Proof.
  intros H. destruct H as [|x H].
  - auto.
  - right. now rewrite Num_pred.
Qed.

Fact union_trans x :
  x <=c trans -> trans (union x).
Proof.
  intros H1 z (y&H2&H3) % Union u H4. apply Union.
  exists y. split. exact H2. revert u H4. apply (H1 y H2), H3.
Qed.

Fact union_WF x :
  WF x -> WF (union x).
Proof.
  intros H. constructor. intros z (y&H1&H2) % Union.
  apply (WF_closed (WF_closed H H1) H2).
Qed.

Fact union_WFc x :
  x <=c WF -> WF (union x).
Proof.
  intros H. constructor. intros z (y&H1&H2) % Union.
  apply H in H1. apply (WF_closed H1 H2).
Qed.

HF closed under union

Fact union_adj_eset x :
  union (0 @ x) = union x.
Proof.
  apply union_lub. split.
  - intros y [->|H] % Adj; auto.
  - auto.
Qed.

Fact union_adj_adj a x y :
  union ((a @ x ) @ y) = a @ union (x @ y).
Proof.
  apply union_lub. split.
  - intros z [->|H] % Adj.
    + intros z [->|H] % Adj. now auto.
      apply Adj. right. apply Union. eauto.
    + intros b H1.
      apply Adj. right. apply Union. eauto.
  - intros u H z [->|H1] % Adj.
    + enough (a @ x <<= u); auto.
    + apply Union in H1 as (b&H1&H2).
      apply Adj in H1 as [->|H1].
      * enough (a @ x <<= u); auto.
      * enough (b <<= u); auto.
Qed.

Fact union_HF x :
  HF x -> HF (union x).
Proof.
  induction 1 as [|a x Ha _ _ IH].
  - rewrite union_eset. constructor.
  - induction Ha as [|a y Ha _ _ IHa].
    + now rewrite union_adj_eset.
    + rewrite union_adj_adj. now constructor.
Qed.

Absorption

Fact union_abs x u :
  union x <<= u -> union (u @ x) = u.
Proof.
  intros H. apply union_lub. split.
  - intros z [-> |H1] % Adj. now auto.
    apply union_el_sub in H1. auto.
  - auto.
Qed.

Fact union_abs' u x :
  u <<= union x -> union (u @ x) = union x.
Proof.
  intros H. apply union_lub. split.
  - intros y [->|H1] % Adj. exact H. apply union_el_sub, H1.
  - intros v H1. apply union_sub. auto.
Qed.

Replacement and Separation

Definition functional R := forall x, unique (R x).

Axiom rep : (set -> set -> Prop) -> set -> set.
Axiom Rep : forall R, functional R -> forall x z, z el rep R x <-> exists y, y el x /\ R y z.

Definition frep f x := rep (fun a b => f a = b) x.

Lemma frep_el f x z :
  z el frep f x <-> exists y, y el x /\ f y = z.
Proof.
  unfold frep. rewrite Rep. reflexivity.
  clear x z. intros x a b. congruence.
Qed.

Definition sep x p := rep (fun z y => p z /\ z = y) x.
Notation "x ! p" := (sep x p) (at level 59, left associativity).

Fact sep_el x p z :
  z el x !p <-> z el x /\ p z.
Proof.
  unfold sep. rewrite Rep.
  - split.
    + intros (y&H1&H2&<-). auto.
    + intros (H1&H2); eauto.
  - cbv. intuition congruence.
Qed.

Fact sep_sub x p :
  x !p <<= x.
Proof.
  intros y (H&_) % sep_el. exact H.
Qed.

Fact small_red p q :
  p <=p q -> small q -> small p.
Proof.
  intros H [x H1]. exists (x!p). intros z.
  rewrite sep_el. split. tauto.
  intros H2. split. apply H1, H, H2. exact H2.
Qed.

Fact small_HF_Num :
  small HF -> small Num.
Proof.
  apply small_red, Num_HF.
Qed.

Fact subset_outside x :
  exists u, u <<= x /\ u nel x.
Proof.
  pose (u:= x ! (fun z => z nel z )).
  assert (u <<= x) as H by apply sep_sub.
  exists u. split. exact H. intros H1.
  enough (u el u <-> u nel u) by tauto.
  split.
  + intros H2 % sep_el. tauto.
  + intros H2. apply sep_el. auto.
Qed.

Fact Cantor f x :
  exists u, u <<= x /\ u nel frep f x.
Proof.
  pose (u:= x ! (fun z => z nel f z )).
  exists u. split. now apply sep_sub.
  intros (y&H1&H2) % frep_el.
  enough (y el u <-> y nel u) by tauto.
  split.
  - intros [H3 H4] % sep_el. congruence.
  - intros H3. apply sep_el.
    split. exact H1. congruence.
Qed.

Description

Definition delta p := union (rep (fun x y => p y) (sing 0)).

Fact delta_eq p x :
  unique p -> p x -> delta p = x.
Proof.
  intros H1 H2. apply union_lub. split.
  - intros y (z&H3&H4) % Rep.
    + rewrite (H1 y x); auto.
    + intros z. exact H1.
  - intros u H3. apply H3. apply Rep; hnf; eauto.
Qed.

Fact small_HF_delta_Num :
  small HF -> agree Num (delta (agree Num)).
Proof.
  intros [u H].
  pose (omega:= u ! Num).
  assert (H1: agree Num omega).
  { intros y. split.
    - intros [_ H1] % sep_el. exact H1.
    - intros H1. apply sep_el. split; [|exact H1].
      apply H, Num_HF, H1. }
  assert (H2: delta (agree Num) = omega).
  { apply delta_eq. apply agree_unique. exact H1. }
  intros x. rewrite H2. apply H1.
Qed.

Fact frep_delta_sep R x :
  functional R ->
  rep R x = frep (fun a => delta (R a)) (x ! (fun a => ex (R a))).
Proof.
  intros H. apply Ext; intros z; rewrite (Rep H), frep_el.
  - intros (a&H1&H2). exists a. split.
    + apply sep_el. eauto.
    + apply delta_eq; auto.
  - intros (a & (H1&b&H2)% sep_el & H3).
    exists a. split. exact H1.
    generalize (delta_eq (H a) H2). congruence.
Qed.

Projections

Definition pi1 u := delta (fun z => sing z el u).
Definition pi2 u := delta (fun z => u = opair (pi1 u) z).

Fact pi1_eq x y :
  pi1 (opair x y) = x.
Proof.
  apply delta_eq.
  - intros a b [H1|H1] % upair_el [H2|H2] % upair_el.
    + apply sing_inj in H1 as ->.
      apply sing_inj in H2 as ->.
      reflexivity.
    + apply sing_inj in H1 as ->.
      symmetry in H2. apply upair_sing in H2 as [<- _].
      reflexivity.
    + apply sing_inj in H2 as ->.
      symmetry in H1. apply upair_sing in H1 as [<- _].
      reflexivity.
    + symmetry in H1. apply upair_sing in H1 as [<- _].
      symmetry in H2. apply upair_sing in H2 as [<- _].
      reflexivity.
  - unfold opair. auto.
Qed.

Fact pi2_eq x y :
  pi2 (opair x y) = y.
Proof.
  apply delta_eq.
  - intros a b [_ <-] % opair_inj [_ <-] % opair_inj.
    reflexivity.
  - now rewrite pi1_eq.
Qed.

Cartesian products

Definition cprod x y := union (frep (fun a => frep (opair a) y) x).

Lemma el_cprod z x y :
  z el cprod x y <-> exists a b, a el x /\ b el y /\ z = opair a b.
Proof.
  unfold cprod. rewrite Union. split.
  - intros (b & H1 & H2).
    apply frep_el in H1 as (a&H1&<-).
    apply frep_el in H2 as (b&H2&H3). eauto.
  - intros (a&b&H1&H2&->).
    exists (frep (opair a) y).
    rewrite !frep_el. eauto 6.
Qed.

Functions as sets

Definition toset f u := frep (fun x => opair x (f x)) u.
Definition apply u x := pi2 (union (u ! (fun z => pi1 z = x ))).

Fact apply_toset x u f :
  x el u -> apply (toset f u) x = f x.
Proof.
  intros H.
  assert ((toset f u ! fun z => pi1 z = x) = sing (opair x (f x))) as H1.
  { apply Ext.
    - intros z [H1 <-] % sep_el. apply sing_el.
      apply frep_el in H1 as (y&H2&<-). now rewrite pi1_eq.
    - intros ? -> % sing_el. apply sep_el. split.
      + apply frep_el. eauto.
      + apply pi1_eq. }
  unfold apply. rewrite H1, union_sing. apply pi2_eq.
Qed.

Subsets and XM

Definition tau P := sigma 0 ! (fun _ => P ).

Lemma tau_inhab P :
  inhab (tau P) <-> P.
Proof.
  split.
  - intros [x H % sep_el]. tauto.
  - intros. exists 0. apply sep_el. auto.
Qed.

Fact Fin_sigma0_xm :
  (forall x, x <<= sigma 0 -> Fin x ) -> forall P, xm P.
Proof.
  intros H P.
  assert (Fin (tau P)) as H1 by apply H, sep_sub.
  apply Fin_eset_inhab in H1 as [H1|H1].
  + right. intros H2 % tau_inhab.
    apply inhab_not in H1. auto.
  + left. apply tau_inhab, H1.
Qed.

Diaconescu's Theorem

Section Diaconescu.
  Variable gamma : set -> set.
  Variable choice : forall x, inhab x -> gamma x el x.

  Fact Diaconescu :
    forall P, P \/ ~ P.
  Proof.
    intros P.
    pose (f x := sigma (sigma 0) ! fun z => z = x \/ P).
    assert (H1: gamma (f 0) el f 0).
    { apply choice. exists 0. apply sep_el. auto 6. }
    assert (H2: gamma (f (sigma 0)) el f (sigma 0)).
    { apply choice. exists (sigma 0). apply sep_el. auto 6. }
    apply sep_el in H1 as [H1 [H3|H3]]; [|auto].
    apply sep_el in H2 as [H2 [H4|H4]]; [|auto].
    right. intros H5.
    enough (0 = sigma 0) by (unfold sigma in *; auto).
    enough (f 0 = f (sigma 0)) by congruence.
    apply Ext; intros z H6 % sep_el; apply sep_el; tauto.
  Qed.

End Diaconescu.

Power

Axiom power : set -> set.
Axiom Power : forall x z, z el power x <-> z <<= x.

Fact power_eager x :
  x el power x.
Proof.
  apply Power; auto.
Qed.

Fact power_trans x :
  trans x -> trans (power x).
Proof.
  intros H y H1 % Power z H2.
  apply Power. apply H. auto.
Qed.

Fact power_WF x :
  WF x -> WF (power x).
Proof.
  intros [H]. constructor. intros y H1 % Power.
  constructor. auto.
Qed.

Fact power_mono x y :
  x <<= y -> power x <<= power y.
Proof.
  intros H1 z H2 % Power. apply Power. auto.
Qed.

Fact union_power_eq x :
  union (power x) = x.
Proof.
  apply union_lub. split.
  - intros y H % Power. exact H.
  - intros y H. apply H, power_eager.
Qed.

Fact power_inj x y :
  power x = power y -> x = y.
Proof.
  intros H.
  rewrite <- (union_power_eq x), H.
  apply union_power_eq.
Qed.

Fact trans_power x :
  trans x <-> x <<= power x.
Proof.
  split.
  - intros H1 y H2. apply Power, H1, H2.
  - intros H1 y H2. apply Power. auto.
Qed.

Fact trans_power_eq x :
  trans x -> power x = union (x @ power x @ 0).
Proof.
  intros H. symmetry. apply union_lub. split.
  - intros y [->| ->] % upair_el.
    + apply power_trans. exact H. apply power_eager.
    + auto.
  - intros y H1. apply H1, upair_el. auto.
Qed.

Fact power_above x :
  ~ power x <<= x.
Proof.
  intros H.
  destruct (subset_outside x) as (u&H1&H2).
  apply H2, H. apply Power, H1.
Qed.

Subsets of Finite Sets

Axiom XM : forall P, xm P.

Fact adj_incl_xm_or x a y :
  x <<= a @ y ->
  x <<= y \/ exists x', x' <<= y /\ x = a @ x'.
Proof.
  intros H.
  destruct (XM (a el y)) as [H1|H1].
  - left. now rewrite (adj_el_eq H1) in H.
  - destruct (XM (a el x)) as [H2|H2].
    + right.
      pose (x' := x ! (fun z => z <> a)). exists x'. split.
      * intros b [H3 H4] % sep_el.
        apply H in H3 as [->|H3] % Adj; tauto.
      * apply Ext.
        -- intros z H3. apply Adj.
           destruct (XM (z=a)). now auto.
           right. apply sep_el. auto.
        -- intros z [->|H3] % Adj. now auto.
           now apply sep_sub in H3.
    + left. intros z H3. specialize (H z H3).
      apply Adj in H as [->|H]; tauto.
Qed.

Fact Fin_sub x y :
  Fin x -> y <<= x -> Fin y.
Proof.
  intros H. revert y.
  induction H as [|a x _ IH]; intros y.
  - intros -> % sub_eset. constructor.
  - intros [H|(x'&H&->)] % adj_incl_xm_or.
    + apply IH, H.
    + constructor. apply IH, H.
Qed.

Notation bun x y := (union (upair x y)).

Fact bun_el z x y :
  z el bun x y <-> z el x \/ z el y.
Proof.
  split.
  - intros (a&H1&H2) % Union.
    apply upair_el in H1 as [->| ->]; auto.
  - intros [H|H]; apply Union.
    + exists x. rewrite upair_el. auto.
    + exists y. rewrite upair_el. auto.
Qed.

Fact bun_0_eq y :
  bun 0 y = y.
Proof.
  apply Ext.
  - intros z [H|H] % bun_el; auto.
  - intros z H. apply bun_el. auto.
Qed.

Fact bun_adj_eq a x y :
  bun (a@x) y = a @ bun x y.
Proof.
  apply Ext.
  - intros z [[->|H] % Adj|H] % bun_el.
    + auto.
    + apply Adj. right. apply bun_el. auto.
    + apply Adj. right. apply bun_el. auto.
  - intros z [->|[H|H] % bun_el] % Adj;
      apply bun_el; auto.
Qed.

Fact frep_0_eq f :
  frep f 0 = 0.
Proof.
  apply Ext.
  - intros z (a&H&_) % frep_el. auto.
  - auto.
Qed.

Fact frep_adj_eq f a x :
  frep f (a@x) = f a @ frep f x.
Proof.
  apply Ext.
  - intros z (y&H1&<-) % frep_el.
    apply Adj in H1 as [->|H1]. now auto.
    apply Adj. right. apply frep_el. eauto.
  - intros z [->|(y&H1&<-) % frep_el] % Adj;
      apply frep_el; eauto.
Qed.

Fact power_0_eq :
  power 0 = sing 0.
Proof.
  apply Ext.
  - intros x H % Power. auto.
  - intros x [->|H] % Adj; apply Power; auto.
Qed.

Fact power_adj_eq a x :
  power (a@x) = bun (power x) (frep (adj a) (power x)).
Proof.
  apply Ext; intros y; rewrite bun_el, frep_el, !Power.
  - intros [H|(x'&H&->)] % adj_incl_xm_or.
    + left. exact H.
    + right. exists x'. split; [|reflexivity].
      apply Power. exact H.
  - intros [H|(z&H&<-)].
    + auto.
    + apply Power in H. intros b [->|?] % Adj; auto.
Qed.

Fact HF_closed_bun x y :
  HF x -> HF y -> HF (bun x y).
Proof.
  intros Hx Hy.
  induction Hx as [|a x Ha _ _ IHx].
  - rewrite bun_0_eq. exact Hy.
  - rewrite bun_adj_eq. now constructor.
Qed.

Fact HF_closed_frep a x :
  HF a -> HF x -> HF (frep (adj a) x).
Proof.
  intros Ha Hx.
  induction Hx as [|b x Hb _ Hx IHx].
  - rewrite frep_0_eq. constructor.
  - rewrite frep_adj_eq. now repeat constructor.
Qed.

Fact HF_closed_power x :
  HF x -> HF (power x).
Proof.
  induction 1 as [|a x Ha _ Hx IHx].
  - rewrite power_0_eq. now repeat constructor.
  - rewrite power_adj_eq.
    apply HF_closed_bun. exact IHx.
    now apply HF_closed_frep.
Qed.

Towers

Section Tower.
  Variable g : set -> set.

  Inductive tow : set -> Prop :=
  | towS x : tow x -> tow (g x)
  | towU x : x <=c tow -> tow (union x).

  Fact tow_eset :
    tow 0.
  Proof.
    rewrite <-union_eset. constructor. auto.
  Qed.

Successor linearity

  Inductive towD : set -> set -> Prop :=
  | towDS x y : tow x -> towD x y -> towD y x -> towD (g x) y
  | towDU x y : (forall z, z el x -> towD z y ) -> towD (union x) y.

  Lemma tow_di x y :
    tow x -> tow y -> towD x y.
  Proof.
    intros Hx. revert y.
    induction Hx as [x Hx IHx|x _ IHx]; intros y Hy.
    - constructor. exact Hx.
      + apply IHx, Hy.
      + induction Hy as [y Hy IHy|y _ IHy].
        * constructor. exact Hy. exact IHy. exact (IHx _ Hy).
        * constructor. exact IHy.
    - constructor. intros z H. now apply IHx.
  Qed.

  Fact xm_upbnd x y :
    upbnd x y \/ exists z, z el x /\ ~ z <<= y.
  Proof.
    destruct (XM (exists z, z el x /\ ~ z <<= y)) as [H|H].
    - right. exact H.
    - left. intros z H1. contra XM H2. contradict H. now exists z.
  Qed.

  Variable g_inc : forall x, tow x -> x <<= g x.

  Theorem tow_lin_succ x y :
    tow x -> tow y -> x <<= y \/ g y <<= x.
  Proof.
    intros Hx. intros H % (tow_di Hx). clear Hx.
    induction H as [x y Hx _ IH1 _ IH2 | x y _ IH].
    - destruct IH1 as [IH1|IH1].
      + destruct IH2 as [IH2|IH2]; [|now auto].
        destruct (Ext IH1 IH2) as []. auto.
      + right. apply (sub_trans IH1). apply g_inc, Hx.
    - destruct (xm_upbnd x y) as [H1|(z&H1&H2)].
      + left. apply union_sub, H1.
      + right. destruct (IH z H1) as [H3|H3].
        * exfalso; tauto.
        * apply (sub_trans H3). cbn. apply union_el_sub, H1.
  Qed.

  Fact tow_lin x y :
    tow x -> tow y -> x <<= y \/ y <<= x.
  Proof.
    intros Hx Hy.
    destruct (tow_lin_succ Hx Hy) as [H|H].
    - auto.
    - right. revert H. apply sub_trans, g_inc, Hy.
  Qed.

  Fact tow_not_sub x y :
    tow x -> tow y -> ~ x <<= y -> y << x.
  Proof.
    intros H1 H2 H3.
    destruct (tow_lin_succ H1 H2) as [H4|H4].
    - now contradict H3.
    - split.
      + revert H4. apply sub_trans. apply g_inc, H2.
      + intros ->. auto.
  Qed.

  Fact tow_mono x y :
    tow x -> tow y -> x <<= y -> g x <<= g y.
  Proof.
    intros Hx Hy H.
    destruct (tow_lin_succ Hy Hx) as [H1|H1].
    - destruct (Ext H H1). auto.
    - apply (sub_trans H1). apply (g_inc Hy).
  Qed.

Complete induction and least elements

  Inductive towA : set -> Prop :=
  | towAI x : (forall y, tow y -> y << x -> towA y ) -> towA x.

  Fact tow_acc :
    tow <=p towA.
  Proof.
    intros x H.
    enough (forall y, y <<= x -> towA y) by auto.
    induction H as [x H IH|x H IH];
      intros y H1; constructor; intros z H2 [H3 H4].
    - apply IH.
      destruct (tow_lin_succ H2 H) as [H5|H5]. exact H5.
      contradict H4. apply Ext; auto.
    - destruct (xm_upbnd x z) as [H5|(a&H5&H6)].
      + contradict H4. apply Ext. exact H3.
        apply (sub_trans H1), union_sub, H5.
      + apply (IH a H5). apply tow_not_sub; auto.
  Qed.

  Fact tow_least x p :
    tow x -> p x -> ex (least (fun z => tow z /\ p z)).
  Proof.
    intros H1 H2.
    induction (tow_acc H1) as [x _ IH].
    destruct (XM (exists y, tow y /\ p y /\ y << x)) as [(y&H3&H4&H5)|H3].
    - now apply (IH y).
    - exists x. repeat split. exact H1. exact H2.
      intros y [H4 H5]. contra XM H6. apply H3. exists y.
      now apply (tow_not_sub H1 H4) in H6.
   Qed.

Basic towers

  Inductive btow : set -> Prop :=
  | btowO : btow 0
  | btowS x : btow x -> btow (g x).

  Fact btow_tow :
    btow <=p tow.
  Proof.
    intros x. induction 1 as [|x _ IH].
    - apply tow_eset.
    - now constructor.
  Qed.

  Fact btow_tight x y :
    tow x -> btow y -> x <<= y -> btow x.
  Proof.
    intros H.
    induction 1 as [|y H1 IH].
    - intros -> % sub_eset. constructor.
    - intros H2.
      destruct (tow_lin_succ H (btow_tow H1)) as [H3|H3].
      + now apply IH.
      + assert (g y = x) as <- by now apply Ext.
        now constructor.
  Qed.

Successor linearity and complete induction can be shown constructively for basic towers

  Inductive btowD : set -> set -> Prop :=
  | btowDO y : btowD 0 y
  | btowDS x y : btow x -> btowD x y -> btowD y x -> btowD (g x) y.

  Fact btow_di x y :
    btow x -> btow y -> btowD x y.
  Proof.
    intros Hx. revert y.
    induction Hx as [|x Hx IHx]; intros y Hy.
    - constructor.
    - constructor.
      + exact Hx.
      + apply IHx, Hy.
      + induction Hy as [|y Hy IHy].
        * constructor.
        * constructor. exact Hy. exact IHy. apply IHx, Hy.
  Qed.

  Fact btow_lin_succ x y :
    btow x -> btow y -> x <<= y \/ g y <<= x.
  Proof.
    intros Hx. intros H % (btow_di Hx). clear Hx.
    induction H as [y|x y Hx _ IH1 _ IH2].
    - auto.
    - destruct IH2 as [IH2|IH2]; [|now auto].
      right.
      destruct IH1 as [IH1|IH1].
      + destruct (Ext IH1 IH2). auto.
      + apply (sub_trans IH1). apply g_inc, btow_tow, Hx.
  Qed.

  Inductive btowA : set -> Prop :=
  | btowAI x : (forall y, btow y -> y << x -> btowA y ) -> btowA x.

  Fact btow_acc :
    btow <=p btowA.
  Proof.
    intros x H.
    enough (forall y, y <<= x -> btowA y) by auto.
  induction H as [|x H IH];
    intros y H1; constructor; intros z H2 [H3 H4].
  - exfalso.
    apply sub_eset in H1 as ->.
    apply sub_eset in H3 as ->.
    auto.
  - apply IH.
    destruct (btow_lin_succ H2 H) as [H5|H5]. exact H5.
    exfalso. apply H4, Ext; auto.
Qed.

WF-preserving and eager generator

  Variable g_WF : forall x, WF x -> WF (g x).
  Variable g_eager : forall x, x el g x.

  Fact tow_WF x :
    tow x -> WF x.
  Proof.
    induction 1 as [x H IH|x _ IH].
    - now apply g_WF.
    - apply union_WF. constructor. exact IH.
  Qed.

  Fact tow_strict x :
    tow x -> x nel x.
  Proof.
    intros H % tow_WF. exact (WF_no_loop H).
  Qed.

  Fact tow_inj_sub x y :
    tow x -> tow y -> g x <<= g y -> x <<= y.
  Proof.
    intros Hx Hy H.
    destruct (tow_lin_succ Hx Hy) as [H1|H1]. exact H1.
    contradiction (tow_strict Hx). auto.
  Qed.

  Fact tow_inj x y :
    tow x -> tow y -> g x = g y -> x = y.
  Proof.
    intros Hx Hy H.
    apply Ext; apply tow_inj_sub; auto; rewrite H; auto.
  Qed.

  Fact tow_lin_el x y :
    tow x -> tow y -> x <<= y \/ y el x.
  Proof.
    intros Hx Hy.
    destruct (tow_lin_succ Hx Hy) as [H|H]; auto.
  Qed.

  Fact tow_tricho x y :
    tow x -> tow y -> x el y \/ x = y \/ y el x.
  Proof.
    intros Hx Hy.
    destruct (tow_lin_el Hx Hy) as [H1|H1].
    - destruct (tow_lin_el Hy Hx) as [H2|H2].
      + destruct (Ext H1 H2). auto.
      + auto.
    - auto.
  Qed.

  Fact tow_lt_el x y :
    tow x -> tow y -> x << y -> x el y.
  Proof.
    intros Hx Hy [H1 H2].
    destruct (tow_lin_succ Hy Hx) as [H3|H3].
    + contradiction H2. now apply Ext.
    + auto.
  Qed.

  Fact tow_mono_el x y :
    tow x -> tow y -> x el y -> g x el g y.
  Proof.
    intros Hx Hy H.
    destruct (tow_lin_el (towS Hy) (towS Hx)) as [H1|H1].
    - contradiction (tow_strict Hx).
      apply (tow_inj_sub Hy Hx) in H1. auto.
    - exact H1.
  Qed.

  Fact tow_new x :
    x <=c tow -> g (union x) nel x.
  Proof.
    intros H1 H2.
    apply (@WF_no_loop (union x)).
    - apply tow_WF. constructor. apply H1.
    - apply Union. exists (g (union x)).
      split. exact H2. apply g_eager.
  Qed.

  Fact tow_large :
    ~ small tow.
  Proof.
    intros (u&H).
    assert (tow (union u)) as H1.
    { constructor. intros z H1. apply H, H1. }
    enough (g (union u) <<= union u) as H2.
    { apply (WF_no_loop (tow_WF H1)). apply H2, g_eager. }
    apply union_el_sub. apply H. constructor. exact H1.
  Qed.

  Fact btow_inf x :
    (forall z, btow z -> z el x ) -> ~ Fin x.
  Proof.
    intros H1 H2.
    assert (H3: Fin (x ! btow)).
    { apply (Fin_sub H2), sep_sub. }
    destruct (Fin_chain_gel H3) as (a & [H4 H5] % sep_el &H6).
    - exists 0. apply sep_el. split; [apply H1|]; now constructor.
    - intros a b [_ Ha] % sep_el [_ Hb] % sep_el.
      destruct (tow_lin (btow_tow Ha) (btow_tow Hb)); auto.
    - assert (H7: g a el x).
      { apply H1. now constructor. }
      assert (H8: g a <<= a).
      { apply H6, sep_el. split. exact H7. now constructor. }
      apply WF_no_loop with (x:= a).
      + apply tow_WF, btow_tow, H5.
      + apply H8, g_eager.
  Qed.

  Fact tow_btow x :
    Fin x -> tow x -> btow x.
  Proof.
    intros H1 H2.
    assert (H3: ~ forall z, btow z -> z el x).
    { intros H3. apply (btow_inf H3 H1). }
    assert (exists a, btow a /\ a nel x) as (a&H4&H5).
    { contra XM H4. contradict H3. intros z H5.
      contra XM H6. contradict H4. now exists z. }
    apply (btow_tight H2 H4).
    destruct (tow_lin_el H2 (btow_tow H4)) as [H6|H6].
    exact H6. exfalso. auto.
  Qed.

Transitivity preserving generator

  Variable g_trans : forall x, trans x -> trans (g x).

  Fact tow_trans x :
    tow x -> trans x.
  Proof.
    induction 1 as [x H IH|x _ IH].
    - now apply g_trans.
    - apply union_trans, IH.
  Qed.

  Fact tow_cum x y :
    tow x -> tow y -> x el y <-> x << y.
  Proof.
    intros Hx Hy. split.
    - intros H. split. now apply tow_trans.
      intros <-. apply (tow_strict Hx H).
    - now apply tow_lt_el.
  Qed.

End Tower.

Ordinals

Notation Ord := (tow sigma).

Fact Ord_eset :
  Ord 0.
Proof.
  apply tow_eset.
Qed.

Fact Num_Ord x :
  Num x -> Ord x.
Proof.
  induction 1 as [|x _ IH].
  - apply Ord_eset.
  - constructor. exact IH.
Qed.

Fact Ord_closed x y :
  Ord x -> y el x -> Ord y.
Proof.
  induction 1 as [x H IH|x _ IH].
  - intros [->|H1] % Adj. exact H. apply IH, H1.
  - intros (z&H1&H2) % Union. eauto.
Qed.

Fact sigma_WF x :
  WF x -> WF (sigma x).
Proof.
  intros H. now apply WF_adj.
Qed.

Fact sigma_eager x :
  x el sigma x.
Proof.
  auto.
Qed.

Fact Ord_WF x :
  Ord x -> WF x.
Proof.
  apply tow_WF, sigma_WF.
Qed.

Fact Ord_trans x :
  Ord x -> trans x.
Proof.
  apply tow_trans, sigma_trans.
Qed.

Fact Ord_strict x :
  Ord x -> x nel x.
Proof.
  apply tow_strict, sigma_WF.
Qed.

Fact Ord_new x :
  x <=c Ord -> sigma (union x) nel x.
Proof.
  apply tow_new. exact sigma_WF. exact sigma_eager.
Qed.

Fact Ord_large :
  ~ small Ord.
Proof.
  apply tow_large. exact sigma_WF. exact sigma_eager.
Qed.

Section Ord_omega.
  Variable omega : set.
  Variable omega_Num : agree Num omega.

  Fact omega_no_num :
    ~ Num omega.
  Proof.
    intros H % omega_Num.
    assert (Num omega) as H1 by apply omega_Num, H.
    apply (Num_strict H1 H).
  Qed.

  Fact union_omega :
    union omega = omega.
  Proof.
    apply Ext.
    - intros z (y & H1 % omega_Num & H2) % Union.
      apply omega_Num. revert H1 H2. apply Num_closed.
    - intros z H % omega_Num. apply Union. exists (sigma z).
      split; [|now auto]. apply omega_Num. now constructor.
  Qed.

  Fact Ord_omega :
    Ord omega.
  Proof.
    rewrite <-union_omega. constructor.
    intros x H % omega_Num % Num_Ord. exact H.
  Qed.

End Ord_omega.

Theorem Ord_lin_succ x y :
  Ord x -> Ord y -> x <<= y \/ sigma y <<= x.
Proof.
  apply tow_lin_succ. cbn. auto.
Qed.

Fact Ord_lin_el x y :
  Ord x -> Ord y -> x <<= y \/ y el x.
Proof.
  intros Hx Hy.
  destruct (Ord_lin_succ Hx Hy); auto.
Qed.

Fact Ord_lin x y :
  Ord x -> Ord y -> x <<= y \/ y <<= x.
Proof.
  intros Hx Hy.
  destruct (Ord_lin_succ Hx Hy) as [H|H].
  - auto.
  - right. revert H. apply sub_trans. auto.
Qed.

Fact Ord_tricho x y :
  Ord x -> Ord y -> x el y \/ x = y \/ y el x.
Proof.
  intros Hx Hy.
  destruct (Ord_lin_el Hx Hy) as [H1|H1].
  - destruct (Ord_lin_el Hy Hx) as [H2|H2].
    + destruct (Ext H1 H2). auto.
    + auto.
  - auto.
Qed.

Fact Ord_cum x y :
  Ord x -> Ord y -> x el y <-> x << y.
Proof.
  intros Hx Hy. split.
  - intros H. split. now apply Ord_trans.
    intros <-. apply (Ord_strict Hx H).
  - intros [H1 H2].
    destruct (Ord_lin_el Hy Hx) as [H|H].
    + contradiction H2. now apply Ext.
    + exact H.
Qed.

Fact Ord_union x :
  Ord x -> Ord (union x).
Proof.
  intros H. constructor. intros y. apply Ord_closed, H.
Qed.

Fact Ord_succ_limit x :
  Ord x -> x = union x \/ x = sigma (union x).
Proof.
  intros Hx.
  assert (Ord (union x)) as Hu by apply Ord_union, Hx.
  assert (Ord (sigma (union x))) as Hs.
  { do 2 constructor. intros y. apply Ord_closed, Hx. }
  destruct (Ord_tricho Hx Hs) as [H|[H|H]].
  - pose proof H as [H1|H1] % Adj.
    + left. exact H1.
    + contradiction (Ord_strict Hx).
      enough (union x <<= x) by auto.
      rewrite <-union_trans_sub. apply Ord_trans, Hx.
  - right. exact H.
  - contradiction (Ord_strict Hu).
    apply (union_el_sub H). auto.
Qed.

Fact Ord_least x p :
  Ord x -> p x -> ex (least (fun z => Ord z /\ p z)).
Proof.
  intros H1 H2.
  induction (Ord_WF H1) as [x H IH].
  destruct (XM (exists y, y el x /\ p y)) as [(y&H3&H4)|H3].
  - pose proof (Ord_closed H1 H3) as H5. now apply (IH y).
  - exists x. repeat split. exact H1. exact H2.
    intros y [H4 H5].
    destruct (Ord_lin_succ H1 H4) as [H6|H6]. exact H6.
    contradiction H3. exists y. eauto.
Qed.

Alternatively, we could reuse the more general proof for towers based on subset induction.

WFT Characterisation of Ordinals

Fact Ord_trans_Ord x :
  trans x -> x <=c Ord -> Ord x.
Proof.
  intros H1 H2.
  assert (Ord (sigma (union x))) as H3.
  { do 2 constructor. auto. }
  destruct (Ord_least (p:= fun z => z nel x) H3) as (y&(H4&H5)&H6).
  - cbn. apply Ord_new, H2.
  - enough (x = y) as <- by exact H4.
    apply Ext.
    + intros z H7.
      destruct (@Ord_tricho y z) as [H8|[->|H8]]; auto.
      * contradiction H5. apply H1 in H7. auto.
      * contradiction H5.
    + intros z H7.
      assert (Ord z) as H8 by apply (Ord_closed H4 H7).
      contra XM H9. contradiction (Ord_strict H8).
      now apply (H6 z).
Qed.

Definition WFT x := WF x /\ trans x /\ x <=c trans.

Theorem Ord_WFT x :
  Ord x <-> WFT x.
Proof.
  split.
  - intros H.
    split. exact (Ord_WF H).
    split. exact (Ord_trans H).
    intros y H1 % (Ord_closed H). exact (Ord_trans H1).
  - intros (H1&H2&H3).
    induction H1 as [x H IH].
    apply (Ord_trans_Ord H2).
    intros y H4. apply (IH y H4).
    + auto.
    + intros z H5. apply H3. apply (H2 y H4), H5.
Qed.

Fact WFT_closed x :
  WFT x -> x <=c WFT.
Proof.
  intros (H1&H2&H3) y H4.
  split. exact (WF_closed H1 H4).
  split. now apply H3, H4.
  intros z H5. apply H2 in H4. auto.
Qed.

Finite Ordinals

The following 3 results all hold in general for the basic stages of a tower. We don't reuse the proofs since Num has not been defined with the predicate btow

Fact Num_inf x :
  (forall z, Num z -> z el x ) -> ~ Fin x.
Proof.
  intros H1 H2.
  assert (H3: Fin (x ! Num)).
  { apply (Fin_sub H2), sep_sub. }
  destruct (Fin_chain_gel H3) as (a & [H4 H5] % sep_el &H6).
  - exists 0. apply sep_el. split; [apply H1|]; now constructor.
  - intros a b [_ Ha] % sep_el [_ Hb] % sep_el.
    destruct (Ord_lin (Num_Ord Ha) (Num_Ord Hb)); auto.
  - assert (H7: sigma a el x).
    { apply H1. now constructor. }
    assert (H8: sigma a <<= a).
    { apply H6, sep_el. split. exact H7. now constructor. }
    apply WF_no_loop with (x:= a).
    + apply Ord_WF, Num_Ord, H5.
    + auto.
Qed.

Fact Num_tight x y :
  Ord x -> Num y -> x <<= y -> Num x.
Proof.
  intros H.
  induction 1 as [|y H1 IH].
  - intros -> % sub_eset. constructor.
  - intros H2.
    destruct (Ord_lin_succ H (Num_Ord H1)) as [H3|H3].
    + now apply IH.
    + assert (sigma y = x) as <- by now apply Ext.
      now constructor.
Qed.

Fact Ord_Num x :
  Fin x -> Ord x -> Num x.
Proof.
  intros H1 H2.
  assert (H3: ~ forall z, Num z -> z el x).
  { intros H3. apply (Num_inf H3 H1). }
  assert (exists a, Num a /\ a nel x) as (a&H4&H5).
  { contra XM H4. contradict H3. intros z H5.
    contra XM H6. contradict H4. now exists z. }
  apply (Num_tight H2 H4).
  destruct (Ord_lin_el H2 (Num_Ord H4)) as [H6|H6].
  exact H6. exfalso. auto.
Qed.

Cumulative Hierarchy

Notation Stage := (tow power).

Fact Stage_eset :
  Stage 0.
Proof.
  apply tow_eset.
Qed.

Fact Stage_WF :
  Stage <=p WF.
Proof.
  apply tow_WF, power_WF.
Qed.

Fact Stage_trans :
  Stage <=p trans.
Proof.
  apply tow_trans, power_trans.
Qed.

Fact Stage_strict x :
  Stage x -> x nel x.
Proof.
  apply tow_strict, power_WF.
Qed.

Fact Stage_large :
  ~ small Stage.
Proof.
  apply tow_large. exact power_WF. exact power_eager.
Qed.

Fact Stage_inc x :
  Stage x -> x <<= power x.
Proof.
  intros H % Stage_trans % power_trans.
  apply H, power_eager.
Qed.

Theorem Stage_lin_succ x y :
  Stage x -> Stage y -> x <<= y \/ power y <<= x.
Proof.
  apply tow_lin_succ, Stage_inc.
Qed.

Fact Stage_lin_el x y :
  Stage x -> Stage y -> x <<= y \/ y el x.
Proof.
  apply tow_lin_el. exact Stage_inc. exact power_eager.
Qed.

Fact Stage_lin x y :
  Stage x -> Stage y -> x <<= y \/ y <<= x.
Proof.
  apply tow_lin, Stage_inc.
Qed.

Definition reachable x := exists y, Stage y /\ x el y.
Definition rank a x := Stage x /\ a <<= x /\ a nel x.

Fact rank_least a x :
  rank a x -> least (fun z => Stage z /\ a <<= z) x.
Proof.
  intros H. split.
  - split; apply H.
  - intros y (H1&H2).
    destruct H as (H4&H5&H6).
    destruct (Stage_lin_succ H4 H1) as [H|H]. exact H.
    contradict H6. apply H. apply Power, H2.
Qed.

Fact rank_fun :
  functional rank.
Proof.
  intros x a b H1 % rank_least H2 % rank_least.
  revert H1 H2. apply least_unique.
Qed.

Theorem reachable_rank a :
  reachable a -> ex (rank a).
Proof.
  intros (x&H1&H2).
  induction H1 as [x Hx IHx|x _ IHx].
  - apply Power in H2.
    destruct (XM (a el x)) as [H|H].
    + apply IHx, H.
    + exists x. now hnf.
  - apply Union in H2 as (y&H2&H3).
    now apply (IHx y).
Qed.

Lemma reachable_reachable x :
  x <=c reachable -> reachable x.
Proof.
  exists (power (power (union (rep rank x)))). split.
  - do 3 constructor.
    intros y (z&H1&H2&H3) % (Rep rank_fun). exact H2.
  - apply Power. intros y H1. apply Power.
    destruct (reachable_rank (H y H1)) as (a&H2).
    apply sub_trans with (y:=a).
    + apply H2.
    + apply union_el_sub. apply (Rep rank_fun).
      now exists y.
Qed.

Theorem WF_reachable :
  WF <=p reachable.
Proof.
  intros x. induction 1 as [x _ IH].
  apply reachable_reachable, IH.
Qed.

Fact rank_WF x :
  ex (rank x) -> WF x.
Proof.
  intros (y&H1&H2&_). apply Power in H2.
    revert H2. apply WF_closed.
    apply power_WF, Stage_WF, H1.
Qed.

Fact Stage_least x p :
  Stage x -> p x -> ex (least (fun z => Stage z /\ p z)).
Proof.
  apply tow_least, Stage_inc.
Qed.

Finite Stages

Notation BS := (btow power).

Fact BS_Stage :
  BS <=p Stage.
Proof.
  apply btow_tow.
Qed.

Fact BS_trans :
  BS <=p trans.
Proof.
  intros x H % BS_Stage % Stage_trans. exact H.
Qed.

Fact BS_lin_succ x y :
  BS x -> BS y -> x <<= y \/ power y <<= x.
Proof.
  intros Hx % BS_Stage Hy % BS_Stage.
  now apply Stage_lin_succ.
Qed.

Fact BS_inf x :
  (forall z, BS z -> z el x ) -> ~ Fin x.
Proof.
  apply btow_inf.
  - exact Stage_inc.
  - exact power_WF.
  - exact power_eager.
Qed.

Fact BS_tight x y :
  Stage x -> BS y -> x <<= y -> BS x.
Proof.
  apply btow_tight, Stage_inc.
Qed.

Fact Stage_BS x :
  Fin x -> Stage x -> BS x.
Proof.
  intros H1 H2.
  assert (H3: ~ forall z, BS z -> z el x).
  { intros H3. apply (BS_inf H3 H1). }
  assert (exists a, BS a /\ a nel x) as (a&H4&H5).
  { contra XM H4. contradict H3. intros z H5.
    contra XM H6. contradict H4. now exists z. }
  apply (BS_tight H2 H4).
  destruct (Stage_lin_el H2 (BS_Stage H4)) as [H6|H6].
  exact H6. exfalso. auto.
Qed.

Fact HF_BS x :
  HF x -> exists y, BS y /\ x el y.
Proof.
  induction 1 as [|a x _ (u&IHu1&IHu2) _ (v&IHv1&IHv2)].
  - exists (power 0). split.
    + repeat constructor.
    + apply Power. auto.
  - destruct (BS_lin_succ IHv1 IHu1) as [H|H].
    + exists (power u). split. now constructor.
      apply Power. apply (BS_trans IHv1) in IHv2. auto.
    + exists (power v). split. now constructor.
      apply Power. apply (BS_trans IHv1) in IHv2.
      enough (a el v) by auto.
      apply H. revert IHu2. apply BS_trans.
      * now constructor.
      * apply power_eager.
Qed.

Fact BS_HF :
  BS <=p HF.
Proof.
  intros x. induction 1 as [|x _ IH].
  - constructor.
  - apply HF_closed_power, IH.
Qed.

Fact HF_BS_agree x :
  HF x <-> exists y, BS y /\ x el y.
Proof.
  split.
  - apply HF_BS.
  - intros (y&H1&H2).
    revert H2. apply HF_closed, BS_HF, H1.
Qed.

Fact HF_inf x :
  (forall z, HF z -> z el x ) -> ~ Fin x.
Proof.
  intros H. apply BS_inf.
  intros z H1 % BS_HF. auto.
Qed.

Closures and Infinity

Section Closure.
  Variable o : set.
  Variable f : set -> set.

  Definition closed x := o el x /\ forall y, y el x -> f y el x.
  Definition closure := delta (least closed).

  Lemma closure_eq x :
    least closed x -> closure = x.
  Proof.
    intros H. unfold closure.
    apply delta_eq. apply least_unique. exact H.
  Qed.

  Lemma least_closed_ex :
    ex closed -> ex (least closed).
  Proof.
    intros (u&H).
    pose (w := u ! (fun x => forall y, closed y -> x el y )).
    exists w. split.
    - split.
      + apply sep_el. firstorder.
      + intros y [H1 H2] % sep_el. apply sep_el. split.
        * apply H, H1.
        * intros v H3. apply H3. auto.
    - intros v H1 x [H2 H3] % sep_el. auto.
  Qed.

  Lemma closure_least' :
    ex closed -> least closed closure.
  Proof.
    intros [u H] % least_closed_ex.
    now rewrite (closure_eq H).
  Qed.

  Lemma closure_o' :
    ex closed -> o el closure.
  Proof.
    intros [u H] % least_closed_ex.
    rewrite (closure_eq H).
    destruct H as [H _]. apply H.
  Qed.

  Lemma closure_f' x :
    ex closed -> x el closure -> f x el closure.
  Proof.
    intros [u H] % least_closed_ex.
    rewrite (closure_eq H).
    destruct H as [H _]. apply H.
  Qed.

  Lemma closure_ind' p :
    ex closed ->
    p o ->
    (forall x, x el closure -> p x -> p (f x)) ->
    closure <=c p.
  Proof.
    intros [u H] % least_closed_ex.
    rewrite (closure_eq H).
    intros H1 H2.
    destruct H as [H3 H4]. specialize (H4 (u ! p)).
    intros x [H5 H6] % H4 % sep_el. exact H6. split.
    - apply sep_el. split. apply H3. exact H1.
    - intros y [H5 H6] % sep_el. apply sep_el. split.
      + apply H3. exact H5.
      + now apply H2.
  Qed.

End Closure.

Notation omega := (closure 0 sigma).

Axiom Inf : ex (closed 0 sigma).

Fact omega_Num :
  agree Num omega.
Proof.
  intros x. split.
  - revert x. apply (closure_ind' Inf).
    + constructor.
    + intros x _ H. now constructor.
  - induction 1 as [|x H IH].
    + apply (closure_o' Inf).
    + apply (closure_f' Inf), IH.
Qed.

Fact omega_inf :
  ~ Fin omega.
Proof.
  apply Num_inf.
  intros z H. now apply omega_Num.
Qed.

Fact omega_O :
  0 el omega.
Proof.
  apply omega_Num. constructor.
Qed.

Fact omega_sigma x :
  x el omega -> sigma x el omega.
Proof.
  intros H % omega_Num.
  apply omega_Num. now constructor.
Qed.

Section ClosureExists.
  Variable o : set.
  Variable f : set -> set.

  Inductive Rec : set -> set -> Prop :=
  | RecO : Rec 0 o
  | RecS x a : Rec x a -> Rec (sigma x) (f a).

  Lemma Rec_Num x a :
    Rec x a -> Num x.
  Proof.
    induction 1 as [|x a _ IH]; now constructor.
  Qed.

  Lemma Rec_fun :
    functional Rec.
  Proof.
    intros x a b H. revert b.
    induction H as [|x a H IH].
    - intros a H. remember 0 as x eqn:E.
      destruct H as [|x a H]; cbn in E; auto.
    - intros b H1. remember (sigma x) as y eqn:E.
      destruct H1 as [|y b H3]; cbn in E.
      + auto.
      + apply sigma_inj in E as ->.
        * f_equal. apply IH, H3.
        * apply Num_trans, (Rec_Num H3).
        * apply Num_trans, (Rec_Num H).
  Qed.

  Lemma closed_ex :
    ex (closed o f).
  Proof.
    exists (rep Rec omega). split.
    - apply (Rep Rec_fun). exists 0. split.
      + apply omega_O.
      + constructor.
    - intros x (y&H1&H2) % (Rep Rec_fun).
      apply (Rep Rec_fun). exists (sigma y). split.
      + now apply omega_sigma.
      + now constructor.
  Qed.

  Theorem closure_least :
    least (closed o f) (closure o f).
  Proof.
    apply closure_least', closed_ex.
  Qed.

  Fact closure_o :
    o el closure o f.
  Proof.
    apply closure_o', closed_ex.
  Qed.

  Fact closure_f x :
    x el closure o f -> f x el closure o f.
  Proof.
   apply closure_f', closed_ex.
  Qed.

  Fact closure_ind p :
    p o ->
    (forall x, x el closure o f -> p x -> p (f x)) ->
    closure o f <=c p.
  Proof.
    apply closure_ind', closed_ex.
  Qed.

End ClosureExists.

Fact agree_BS :
  agree BS (closure 0 power).
Proof.
  intros x. split.
  - revert x. apply closure_ind.
    + constructor.
    + intros x _ H. now constructor.
  - induction 1 as [|x H IH].
    + apply closure_o.
    + apply closure_f, IH.
Qed.

Fact agree_HF :
  agree HF (union (closure 0 power)).
Proof.
  intros x. split.
  - intros (y & H1 % agree_BS & H2) % Union.
    revert H2. apply HF_closed. apply BS_HF, H1.
  - intros (y&H1&H2) % HF_BS. apply Union.
    exists y. split. now apply agree_BS. exact H2.
Qed.

Transitive Closure

Definition tc x := union (closure x union).

Fact trans_closure x :
  least (fun y => trans y /\ x <<= y) (tc x).
Proof.
  repeat split.
  - intros z (y&H1&H2) % Union.
    apply (sub_trans (union_el_sub H2)).
    apply union_el_sub, closure_f, H1.
  - apply union_el_sub, closure_o.
  - intros y [H1 H2]. apply union_sub.
    apply closure_ind. exact H2.
    intros z _ IH. apply union_sub. auto.
Qed.

Well-Ordering Theorem

Section Wellordering.
  Variable u : set.
  Variable gamma : set -> set.

  Notation comp x := (u ! fun y => y nel x).
  Definition pi x := u ! fun z => z el x \/ z = gamma (comp x).
  Notation Zer := (tow pi).

  Fact Zer_u x :
    Zer x -> x <<= u.
  Proof.
    induction 1 as [x _ _|x _ IH].
    - intros z [H _] % sep_el. exact H.
    - apply union_sub, IH.
  Qed.

  Fact Zer_inc x :
    Zer x -> x <<= pi x.
  Proof.
    intros H1 % Zer_u z H2. apply sep_el. auto.
  Qed.

  Fact Zer_lin_succ x y :
    Zer x -> Zer y -> x <<= y \/ pi y <<= x.
  Proof.
    apply tow_lin_succ, Zer_inc.
  Qed.

  Fact Zer_not_sub x y :
    Zer x -> Zer y -> ~ x <<= y -> y << x.
  Proof.
    apply tow_not_sub, Zer_inc.
  Qed.

  Fact Zer_least x p :
    Zer x -> p x -> ex (least (fun z => Zer z /\ p z)).
  Proof.
    apply tow_least, Zer_inc.
  Qed.

  Definition sta a := union (power u ! fun x => Zer x /\ a nel x).
  Notation "a <= b" := (sta a <<= sta b).

  Fact sta_Zer a :
    Zer (sta a).
  Proof.
    constructor. intros x H % sep_el. apply H.
  Qed.

  Fact wo_trans a b c :
    a <= b -> b <= c -> a <= c.
  Proof.
    auto.
  Qed.

  Fact wo_lin a b :
    a <= b \/ b <= a.
  Proof.
    destruct (Zer_lin_succ (sta_Zer a) (sta_Zer b)) as [H|H].
    - auto.
    - right. revert H. apply sub_trans. apply Zer_inc, sta_Zer.
  Qed.

  Fact wo_least a p :
    a el u -> p a ->
    exists b, b el u /\ p b /\ forall c, c el u -> p c -> b <= c.
  Proof.
    intros H1 H2.
    pose (q x := exists a, a el u /\ p a /\ sta a = x).
    destruct (Zer_least (p:= q) (sta_Zer a)) as (x&(H3&H4)&H5).
    - exists a. auto.
    - destruct H4 as (b&H6&H7&<-).
      exists b. repeat split.
      + exact H6.
      + exact H7.
      + intros c H8 H9. apply H5. split.
        * apply sta_Zer.
        * exists c. auto.
  Qed.

Antisymmetry requires choice

  Variable choice : forall x, inhab x -> x <<= u -> gamma x el x.

  Fact sta_inv a :
    a el u -> gamma (comp (sta a)) = a.
  Proof.
    intros H. contra XM H1.
    assert (a nel sta a) as H0.
    { intros (x & H2 % sep_el & H3) % Union. apply H2, H3. }
    assert (gamma (comp (sta a)) el comp (sta a)) as [H2 H3] % sep_el.
    { apply choice. (* This is the only use of choice *)
      - exists a. apply sep_el. auto.
      - intros b H4 % sep_el. apply H4. }
    assert (gamma (comp (sta a)) el pi (sta a)) as H4.
    { apply sep_el. auto. }
    enough (pi (sta a) <<= sta a) by auto.
    assert (Zer (pi (sta a))) as H5.
    { constructor. apply sta_Zer. }
    apply union_el_sub, sep_el. repeat split.
    - apply Power, Zer_u, H5.
    - exact H5.
    - intros [H6 [H7|H7]] % sep_el; congruence.
  Qed.

  Fact wo_anti a b c :
    a el u -> b el u -> a <= b -> b <= a -> a = b.
  Proof.
    intros H1 % sta_inv H2 % sta_inv H3 H4.
    assert (sta a = sta b) as E by now apply Ext.
    rewrite E in H1. congruence.
  Qed.

End Wellordering.

Regularity

Definition regular x := inhab x -> exists y, y el x /\ forall z, z el y -> z nel x.
Definition serial x := inhab x /\ forall y, y el x -> exists z, z el y /\ z el x.

Fact WF_regular x :
  WF x -> regular x.
Proof.
  intros H1 H2.
  destruct (WF_min (p:= fun z => z el x) XM) as (y&H3&H4).
  - exact H2.
  - destruct H1 as [x H1]. exact H1.
  - exists y. split. exact H3.
    intros z H5 H6. now apply (H4 z).
Qed.

Fact serial_not_regular x :
  serial x <-> ~ regular x.
Proof.
  split.
  - intros [H1 H2] H3.
    destruct (H3 H1) as (y&H4&H5).
    destruct (H2 y H4) as (z&H6&H7).
    apply (H5 z H6 H7).
  - intros H1.
    enough (inhab x /\ forall y, y el x -> exists z, z el y /\ z el x) as [H2 H3].
    { split. exact H2. exact H3. }
    split.
    + contra XM H2. apply H1. intros H3. now contradict H2.
    + intros y H2. contra XM H3. contradict H1. intros H4.
      exists y. split. exact H2. intros z H5. contradict H3.
      now exists z.
Qed.

Fact WF_not x :
  ~ WF x <-> exists y, y el x /\ ~ WF y.
Proof.
  split.
  - intros H1. contra XM H2. apply H1. constructor.
    intros y H3. contra XM H4. apply H2. exists y. auto.
  - intros (y&H1&H2) H3. contradict H2.
    apply (WF_closed H3 H1).
Qed.

Fact serial_ex_trans x :
  trans x -> ~ WF x -> serial (x ! (fun y => ~ WF y )).
Proof.
  intros H1 H2. split.
  - apply WF_not in H2 as (y&H2&H3).
    exists y. now apply sep_el.
  - intros y (H3&H4) % sep_el.
    apply WF_not in H4 as (z&H4&H5).
    exists z. split. exact H4.
    apply sep_el. apply H1 in H3. auto.
Qed.

Fact serial_ex x :
  ~ WF x -> ex serial.
Proof.
  intros H.
  destruct (trans_closure x) as [[H1 H2] _].
  exists (tc x ! (fun y => ~ WF y )).
  apply serial_ex_trans. exact H1.
  contradict H. apply (WF_sub_closed H H2).
Qed.

Fact regularity_all_WF :
  all WF <-> all regular.
Proof.
  split; intros H x.
  - apply WF_regular, H.
  - contra XM H1.
    apply serial_ex in H1 as [y H1].
    generalize (H y). apply serial_not_regular, H1.
Qed.