Require Export HFS.Operations.

Section Ordinals.
  Variable X: HF.
  Implicit Types x y z alpha beta : X.

  Inductive ord : X -> Prop :=
  | Ord0 : ord 0
  | OrdS x : ord x -> ord (x@x).

  Fact ord_trans alpha (A : ord alpha) :
    trans alpha.
  Proof.
    induction A; hfs.
  Qed.

  Fact ord_ord alpha z (A : ord alpha) :
    z el alpha -> ord z.
  Proof.
    induction A; hfs.
  Qed.

  Fact ord_eset' alpha (A : ord alpha) :
    alpha <> 0 -> 0 el alpha.
  Proof.
    intros B. induction A as [|alpha A IH].
    - exfalso; auto.
    - decide (alpha=0) as [-> |C]; hfs.
  Qed.

  Fact ord_eset alpha (A : ord alpha) :
    (alpha = 0) + (0 el alpha).
  Proof.
    decide (alpha=0) as [-> |B]; auto using ord_eset'.
  Qed.

  Fact ord_pred alpha (A : ord alpha) :
    alpha <> 0 -> alpha = union alpha @ union alpha.
  Proof.
    intros B. induction A as [|alpha A IH].
    - exfalso; auto.
    - rewrite succ_inv; auto using ord_trans.
  Qed.

  Fact ord_pred' alpha (A : ord alpha) :
    ord (union alpha).
  Proof.
    induction A as [|alpha A IH].
    - rewrite unionE_eq. constructor.
    - rewrite succ_inv; auto using ord_trans.
  Qed.

  Fact ord_inv alpha (A : ord alpha) :
    (alpha = 0) + Sigma gamma, ord gamma /\ alpha = gamma @ gamma.
  Proof.
    decide (alpha = 0) as [-> |B]. now left.
    right. exists (union alpha). auto using ord_pred, ord_pred'.
  Qed.

  Fact ord_sip (p : X -> Type) :
    p 0 -> (forall alpha, ord alpha -> p alpha -> p (alpha @ alpha)) ->
    forall alpha, ord alpha -> p alpha.
  Proof.
    intros A B alpha. epsilon_induction alpha.
    intros alpha IH [-> |(gamma&C&->)] % ord_inv.
    - exact A.
    - apply (B gamma C), IH; hfs.
  Qed.

  Fact ord_mono alpha beta (B : ord beta) :
    alpha el beta -> alpha @ alpha el beta @ beta.
  Proof.
    induction B; hfs.
  Qed.

  Fact ord_tricho alpha beta (A : ord alpha) (B : ord beta) :
    (alpha el beta) + (alpha = beta) + (beta el alpha).
  Proof.
    revert beta B. pattern alpha. revert alpha A. apply ord_sip.
    - intros beta [B|B] % ord_eset; eauto.
    - intros alpha A IH beta B.
      destruct (ord_inv B) as [->|(gamma&C&->)].
      + right. apply ord_eset in A as [-> |A]; hfs.
      + destruct (IH gamma C) as [[D| -> ]|D]; auto using ord_mono.
  Qed.

  Fact ord_incl alpha beta (A : ord alpha) (B : ord beta) :
    alpha el beta <-> alpha <<= beta /\ alpha <> beta.
  Proof.
    split.
    - intros C. split.
      + now apply ord_trans.
      + intros <-. contradiction (el_irrefl C).
    - intros [C D].
      destruct (ord_tricho A B) as [[E|<- ]|E].
      + exact E.
      + exfalso. auto.
      + exfalso. pose proof (ord_trans A E) as F.
        apply D. extensio as z. hfs.
  Qed.

  Fact ord_chain x :
    (forall z, z el x -> ord z) -> chain x.
  Proof.
    intros C alpha beta A B.
    destruct (ord_tricho (C _ A) (C _ B)) as [[D| <-]|D].
    - left. apply ord_incl; auto.
    - auto.
    - right. apply ord_incl; auto.
  Qed.

  Fact ord_chain' alpha (A : ord alpha) :
    chain alpha.
  Proof.
    apply ord_chain. eauto using ord_ord.
  Qed.

  Definition HT x := trans x /\ forall z, z el x -> trans z.

  Fact HT_trans x y :
    HT x -> y el x -> HT y.
  Proof.
    intros [A B] C. split.
    - auto.
    - apply A in C. hfs.
  Qed.

  Fact ord_trans_ord x :
    trans x -> (forall z, z el x -> ord z) -> ord x.
  Proof.
    intros A B.
    decide (x=0) as [-> |C]. now constructor.
    assert (D: union x el x).
    { apply chain_union. hfs. now apply ord_chain. }
    enough (union x @ union x = x) as <- by auto using ord.
    extensio as z. split; intros E.
    - hnf in A. hfs.
    - assert (F: z <<= union x) by apply union_el_incl, E.
      decide (z = union x) as [-> |G]. hfs.
      enough (z el union x) by hfs.
      apply ord_incl; auto.
  Qed.

  Theorem ord_HT x :
    ord x <-> HT x.
  Proof.
    split.
    - intros A. split; eauto using ord_trans, ord_ord.
    - epsilon_induction x. intros x IH A. apply ord_trans_ord.
      + now destruct A.
      + eauto using HT_trans.
  Qed.

End Ordinals.