Require Import Classical.

Inductive Ordinal : Type :=
  | ordS : Ordinal → Ordinal
  | ord_sup: ∀ {I:Type}, (I→Ordinal) → Ordinal.


Inductive ord_le : Ordinal → Ordinal → Prop :=
  | ord_le_respects_succ: ∀ alpha beta:Ordinal,
    ord_le alpha beta → ord_le (ordS alpha) (ordS beta)
  | ord_le_S_sup: ∀ (alpha:Ordinal) (J:Type)
    (beta:J→Ordinal) (j:J), ord_le (ordS alpha) (beta j) →
    ord_le (ordS alpha) (ord_sup beta)
  | ord_sup_minimal: ∀ (I:Type) (alpha:I→Ordinal)
    (beta:Ordinal), (∀ i:I, ord_le (alpha i) beta) →
                    ord_le (ord_sup alpha) beta.

Definition ord_lt (alpha beta:Ordinal) :=
  ord_le (ordS alpha) beta.
Definition ord_eq (alpha beta:Ordinal) :=
  ord_le alpha beta ∧ ord_le beta alpha.
Definition ord_ge (alpha beta:Ordinal) :=
  ord_le beta alpha.
Definition ord_gt (alpha beta:Ordinal) :=
  ord_lt beta alpha.

Delimit Scope ordinal_scope with Ordinal.
Open Scope ordinal_scope.
Notation "alpha < beta" := (ord_lt alpha beta) : ordinal_scope.
Notation "alpha <= beta" := (ord_le alpha beta) : ordinal_scope.
Notation "alpha == beta" := (ord_eq alpha beta)
  (at level 70) : ordinal_scope.
Notation "alpha > beta" := (ord_gt alpha beta) : ordinal_scope.
Notation "alpha >= beta" := (ord_ge alpha beta) : ordinal_scope.

Lemma ord_le_respects_succ_converse: ∀ alpha beta:Ordinal,
  ordS alpha ≤ ordS beta → alpha ≤ beta.
Proof.
intros.
inversion_clear H.
assumption.
Qed.

Lemma ord_le_S_sup_converse: ∀ (alpha:Ordinal)
  (J:Type) (beta:J→Ordinal), ordS alpha ≤ ord_sup beta →
  ∃ j:J, ordS alpha ≤ beta j.
Proof.
intros.
inversion H.
∃ j.
assumption.
Qed.

Lemma ord_sup_minimal_converse: ∀ (I:Type)
  (alpha:I→Ordinal) (beta:Ordinal),
  ord_sup alpha ≤ beta → ∀ i:I, alpha i ≤ beta.
Proof.
intros.
inversion H.
Require Import Eqdep.
apply inj_pair2 in H2.
destruct H2.
apply H3.
Qed.

Lemma ord_le_trans: ∀ alpha beta gamma:Ordinal,
  alpha ≤ beta → beta ≤ gamma → alpha ≤ gamma.
Proof.
induction alpha.
induction beta.
induction gamma.
intros.
apply ord_le_respects_succ.
apply IHalpha with beta.
apply ord_le_respects_succ_converse; trivial.
apply ord_le_respects_succ_converse; trivial.
intros.
apply ord_le_S_sup_converse in H1.
destruct H1 as [i].
apply ord_le_S_sup with i.
apply H; trivial.
intros.
pose proof (ord_sup_minimal_converse _ _ _ H1).
apply ord_le_S_sup_converse in H0.
destruct H0 as [i].
apply H with i; trivial.
intros.
pose proof (ord_sup_minimal_converse _ _ _ H0).
constructor.
intro.
apply H with beta; trivial.
Qed.

Lemma ord_le_sup: ∀ (I:Type) (alpha:I→Ordinal) (i:I),
  alpha i ≤ ord_sup alpha.
Proof.
assert (∀ beta:Ordinal, beta ≤ beta ∧
  ∀ (I:Type) (alpha:I→Ordinal) (i:I),
  beta ≤ alpha i → beta ≤ ord_sup alpha).
induction beta.
destruct IHbeta.
split.
apply ord_le_respects_succ; trivial.
intros.
apply ord_le_S_sup with i.
trivial.
split.
apply ord_sup_minimal.
intro.
destruct (H i).
apply H1 with i; trivial.
intros J alpha j ?.
apply ord_sup_minimal.
intro.
destruct (H i).
apply H2 with j.
apply ord_le_trans with (ord_sup o).
apply H2 with i; trivial.
trivial.

intros.
destruct (H (alpha i)).
apply H1 with i; trivial.
Qed.

Lemma ord_le_refl: ∀ alpha:Ordinal, alpha ≤ alpha.
Proof.
induction alpha.
apply ord_le_respects_succ; trivial.
apply ord_sup_minimal.
apply ord_le_sup.
Qed.

Lemma ord_le_S: ∀ alpha:Ordinal, alpha ≤ ordS alpha.
Proof.
induction alpha.
apply ord_le_respects_succ; trivial.
apply ord_sup_minimal.
intro.
apply ord_le_trans with (ordS (o i)).
apply H.
apply ord_le_respects_succ.
apply ord_le_sup.
Qed.

Lemma ord_lt_le: ∀ alpha beta:Ordinal,
  alpha < beta → alpha ≤ beta.
Proof.
intros.
apply ord_le_trans with (ordS alpha); trivial.
apply ord_le_S.
Qed.

Lemma ord_lt_le_trans: ∀ alpha beta gamma:Ordinal,
  alpha < beta → beta ≤ gamma → alpha < gamma.
Proof.
intros.
apply ord_le_trans with beta; trivial.
Qed.

Lemma ord_le_lt_trans: ∀ alpha beta gamma:Ordinal,
  alpha ≤ beta → beta < gamma → alpha < gamma.
Proof.
intros.
apply ord_le_trans with (ordS beta); trivial.
apply ord_le_respects_succ; trivial.
Qed.

Lemma ord_lt_trans: ∀ alpha beta gamma:Ordinal,
  alpha < beta → beta < gamma → alpha < gamma.
Proof.
intros.
apply ord_lt_le_trans with beta; trivial;
 apply ord_lt_le; trivial.
Qed.

Lemma ord_lt_respects_succ: ∀ alpha beta:Ordinal,
  alpha < beta → ordS alpha < ordS beta.
Proof.
intros.
apply ord_le_respects_succ; trivial.
Qed.

Lemma ord_total_order: ∀ alpha beta:Ordinal,
  alpha < beta ∨ alpha == beta ∨ alpha > beta.
Proof.
induction alpha.
induction beta.
destruct (IHalpha beta) as [|[|]].
left; apply ord_lt_respects_succ; trivial.
right; left.
split.
apply ord_le_respects_succ; apply H.
apply ord_le_respects_succ; apply H.
right; right.
apply ord_lt_respects_succ; trivial.

destruct (classic (∃ i:I, ordS alpha < o i)).
destruct H0 as [i].
left.
apply ord_lt_le_trans with (o i); trivial.
apply ord_le_sup.
destruct (classic (∃ i:I, ordS alpha == o i)).
destruct H1 as [i].
right; left.
split.
apply ord_le_trans with (o i).
apply H1.
apply ord_le_sup.
apply ord_sup_minimal.
intro.
destruct (H i0) as [|[|]].
contradiction H0; ∃ i0; trivial.
apply H2.
apply ord_lt_le; trivial.
assert (∀ i:I, ordS alpha > o i).
intros.
destruct (H i) as [|[|]].
contradiction H0; ∃ i; trivial.
contradiction H1; ∃ i; trivial.
trivial.
right; right.
apply ord_le_lt_trans with alpha.
apply ord_sup_minimal.
intro.
apply ord_le_respects_succ_converse.
apply H2.
apply ord_le_refl.

induction beta.
case (classic (∃ i:I, o i > ordS beta)); intro.
destruct H0 as [i].
right; right.
apply ord_lt_le_trans with (o i); trivial.
apply ord_le_sup.
case (classic (∃ i:I, o i == ordS beta)); intro.
right; left.
destruct H1 as [i].
split.
apply ord_sup_minimal.
intro j.
destruct (H j (ordS beta)) as [|[|]].
apply ord_lt_le; trivial.
apply H2.
contradiction H0; ∃ j; trivial.
apply ord_le_trans with (o i).
apply H1.
apply ord_le_sup.
left.
apply ord_le_respects_succ.
apply ord_sup_minimal.
intro.
destruct (H i (ordS beta)) as [|[|]].
apply ord_le_respects_succ_converse; trivial.
contradiction H1; ∃ i; trivial.
contradiction H0; ∃ i; trivial.

case (classic (∃ j:I0, ord_sup o < o0 j)); intro.
left.
destruct H1 as [j].
apply ord_lt_le_trans with (o0 j); trivial.
apply ord_le_sup.
case (classic (∃ i:I, o i > ord_sup o0)); intro.
destruct H2 as [i].
right; right.
apply ord_lt_le_trans with (o i); trivial.
apply ord_le_sup.

right; left.
split.
apply ord_sup_minimal; intro.
destruct (H i (ord_sup o0)) as [|[|]].
apply ord_lt_le; trivial.
apply H3.
contradiction H2; ∃ i; trivial.
apply ord_sup_minimal; intro j.
destruct (H0 j) as [|[|]].
contradiction H1; ∃ j; trivial.
apply H3.
apply ord_lt_le; trivial.
Qed.

Lemma ordinals_well_founded: well_founded ord_lt.
Proof.
red; intro alpha.
induction alpha.
constructor.
intros beta ?.
apply ord_le_respects_succ_converse in H.
constructor; intros gamma ?.
destruct IHalpha.
apply H1.
apply ord_lt_le_trans with beta; trivial.

constructor; intros alpha ?.
apply ord_le_S_sup_converse in H0.
destruct H0 as [j].

destruct (H j).
apply H1; trivial.
Qed.

Lemma ord_lt_irrefl: ∀ alpha:Ordinal, ~(alpha < alpha).
Proof.
intro; red; intro.
assert (∀ beta:Ordinal, beta ≠ alpha).
intro.
pose proof (ordinals_well_founded beta).
induction H0.
red; intro.
symmetry in H2; destruct H2.
contradiction (H1 alpha H); trivial.
contradiction (H0 alpha); trivial.
Qed.

Inductive successor_ordinal : Ordinal→Prop :=
  | intro_succ_ord: ∀ alpha:Ordinal,
    successor_ordinal (ordS alpha)
  | succ_ord_wd: ∀ alpha beta:Ordinal,
    successor_ordinal alpha → alpha == beta →
    successor_ordinal beta.
Inductive limit_ordinal : Ordinal→Prop :=
  | intro_limit_ord: ∀ {I:Type} (alpha:I→Ordinal),
    (∀ i:I, ∃ j:I, alpha i < alpha j) →
    limit_ordinal (ord_sup alpha)
  | limit_ord_wd: ∀ alpha beta:Ordinal,
    limit_ordinal alpha → alpha == beta →
    limit_ordinal beta.

Lemma ord_successor_or_limit: ∀ alpha:Ordinal,
  successor_ordinal alpha ∨ limit_ordinal alpha.
Proof.
induction alpha.
left; constructor.
destruct (classic (∀ i:I, ∃ j:I, o i < o j)).
right; constructor; trivial.
destruct (not_all_ex_not _ _ H0) as [i].
assert (∀ j:I, o j ≤ o i).
intro.
destruct (ord_total_order (o i) (o j)) as [|[|]].
contradiction H1; ∃ j; trivial.
apply H2.
apply ord_lt_le; trivial.

assert (ord_sup o == o i).
split.
apply ord_sup_minimal; trivial.
apply ord_le_sup.
case (H i); intro.
left; apply succ_ord_wd with (o i); trivial.
split; apply H3.
right.
apply limit_ord_wd with (o i); trivial.
split; apply H3.
Qed.

Lemma successor_ordinal_not_limit: ∀ alpha:Ordinal,
  successor_ordinal alpha → ¬ limit_ordinal alpha.
Proof.
intros; red; intro.
induction H.
inversion_clear H0.
induction H as [I beta|].
assert (ord_sup beta ≤ alpha).
apply ord_sup_minimal.
intro.
apply ord_le_respects_succ_converse.
destruct (H i) as [j].
apply ord_le_trans with (beta j); trivial.
apply ord_le_trans with (ord_sup beta).
apply ord_le_sup.
apply H1.

contradiction (ord_lt_irrefl alpha).
apply ord_le_trans with (ord_sup beta); trivial.
apply H1.

apply IHlimit_ordinal.
split; apply ord_le_trans with beta;
  (apply H0 || apply H1).

contradiction IHsuccessor_ordinal.
apply limit_ord_wd with beta; trivial.
split; apply H1.
Qed.