Library Ordinal
This library defines the type ord of tree ordinals.
This formalisation of tree ordinals is based on notes by Peter Hancock:
(Ordinal-theoretic) Proof Theory. Course notes from Midlands Graduate School, 2008.
http://personal.cis.strath.ac.uk/~ph/
http://events.cs.bham.ac.uk/mgs2008/notes/proofTheory.pdf
See also the formalisation in Isabelle by Michael Compton: http://www4.informatik.tu-muenchen.de/~isabelle/html-data/library/HOL/Induct/Tree.html
This formalisation of tree ordinals is based on notes by Peter Hancock:
(Ordinal-theoretic) Proof Theory. Course notes from Midlands Graduate School, 2008.
http://personal.cis.strath.ac.uk/~ph/
http://events.cs.bham.ac.uk/mgs2008/notes/proofTheory.pdf
See also the formalisation in Isabelle by Michael Compton: http://www4.informatik.tu-muenchen.de/~isabelle/html-data/library/HOL/Induct/Tree.html
Set Implicit Arguments.
Delimit Scope ord_scope with ord.
Open Scope ord_scope.
Inductive type for tree ordinals.
The intuition is that the Limit constructor represents the least
upper bound of its argument sequence.
We might like to exclude sequences such as (4,4,4,...), since they would not necessarily represent a limit ordinal. A way to do this is by imposing a monotonicity property on the Limit arguments. We first define an ordering on ord and, using that, define a subset of ord where the Limit arguments are monotone (in library WfOrdinal).
We might like to exclude sequences such as (4,4,4,...), since they would not necessarily represent a limit ordinal. A way to do this is by imposing a monotonicity property on the Limit arguments. We first define an ordering on ord and, using that, define a subset of ord where the Limit arguments are monotone (in library WfOrdinal).
Type of predecessor indices of an ordinal.
Fixpoint pd_type (alpha : ord) : Set :=
match alpha with
| Zero => False
| Succ alpha => (unit + pd_type alpha) % type
| Limit f => { n : nat & pd_type (f n) }
end.
Reserved Notation "alpha [ i ]" (at level 60).
match alpha with
| Zero => False
| Succ alpha => (unit + pd_type alpha) % type
| Limit f => { n : nat & pd_type (f n) }
end.
Reserved Notation "alpha [ i ]" (at level 60).
Predecessor indices of an ordinal are essentially the paths on its tree
structure starting from the root that cross at least one Succ
constructor.
Predecessor of an ordinal for a given predecessor index.
Fixpoint pd (alpha : ord) : pd_type alpha -> ord :=
match alpha with
| Zero => False_rect _
| Succ alpha => fun i => match i with
| inl tt => alpha
| inr t => alpha[t]
end
| Limit f => fun i => match i with
| existT n t => (f n)[t]
end
end
where "alpha [ i ]" := (pd alpha i) : ord_scope.
match alpha with
| Zero => False_rect _
| Succ alpha => fun i => match i with
| inl tt => alpha
| inr t => alpha[t]
end
| Limit f => fun i => match i with
| existT n t => (f n)[t]
end
end
where "alpha [ i ]" := (pd alpha i) : ord_scope.
pd_type and pd can be seen as defining a 'subtree' partial order on
ord. We use it to define an extensional non-strict order on ord.
Non-strict order on ord.
Inductive ord_le : ord -> ord -> Prop :=
| Ord_le_Zero : forall beta,
Zero <= beta
| Ord_le_Succ : forall alpha beta i,
alpha <= beta[i] ->
Succ alpha <= beta
| Ord_le_Limit : forall f beta,
(forall n, f n <= beta) ->
Limit f <= beta
where "alpha <= beta" := (ord_le alpha beta) : ord_scope.
| Ord_le_Zero : forall beta,
Zero <= beta
| Ord_le_Succ : forall alpha beta i,
alpha <= beta[i] ->
Succ alpha <= beta
| Ord_le_Limit : forall f beta,
(forall n, f n <= beta) ->
Limit f <= beta
where "alpha <= beta" := (ord_le alpha beta) : ord_scope.
Strict order on ord.
Definition ord_lt (alpha beta : ord) := exists i, alpha <= beta[i].
Infix " < " := ord_lt : ord_scope.
Infix " < " := ord_lt : ord_scope.
Equality on ord.
Definition ord_eq alpha beta := alpha <= beta /\ beta <= alpha.
Infix " == " := ord_eq (no associativity, at level 75) : ord_scope.
Infix " == " := ord_eq (no associativity, at level 75) : ord_scope.
We proceed with some useful lemmas about these relations.
First predecessor of a successor is the original ordinal.
Lemma first_pd_after_succ_id :
forall alpha, alpha = Succ alpha [inl (pd_type alpha) tt].
Proof.
trivial.
Qed.
forall alpha, alpha = Succ alpha [inl (pd_type alpha) tt].
Proof.
trivial.
Qed.
No successor ordinal <= zero.
Lemma ord_le_not_succ_zero :
forall alpha, ~ Succ alpha <= Zero.
Proof.
intros alpha H.
inversion_clear H.
destruct i.
Qed.
forall alpha, ~ Succ alpha <= Zero.
Proof.
intros alpha H.
inversion_clear H.
destruct i.
Qed.
No double successor <= 1.
Lemma ord_le_not_succ_succ_one :
forall alpha, ~ Succ (Succ alpha) <= Succ Zero.
Proof.
intros alpha H.
inversion_clear H.
destruct i.
destruct u.
apply (@ord_le_not_succ_zero alpha).
assumption.
assumption.
Qed.
forall alpha, ~ Succ (Succ alpha) <= Succ Zero.
Proof.
intros alpha H.
inversion_clear H.
destruct i.
destruct u.
apply (@ord_le_not_succ_zero alpha).
assumption.
assumption.
Qed.
If alpha <= zero, alpha <= any ordinal.
Lemma ord_le_zero_right :
forall alpha beta,
alpha <= Zero ->
alpha <= beta.
Proof.
induction alpha as [| alpha _ | f IH]; intros beta H.
constructor.
inversion_clear H.
destruct i.
inversion_clear H.
constructor.
intro n.
apply IH.
trivial.
Qed.
forall alpha beta,
alpha <= Zero ->
alpha <= beta.
Proof.
induction alpha as [| alpha _ | f IH]; intros beta H.
constructor.
inversion_clear H.
destruct i.
inversion_clear H.
constructor.
intro n.
apply IH.
trivial.
Qed.
If alpha <= a predecessor of beta, alpha <= beta.
Lemma ord_le_pd_right :
forall alpha beta (i : pd_type beta),
alpha <= beta[i] ->
alpha <= beta.
Proof.
induction alpha as [| alpha IH | f IH]; intros beta i H.
constructor.
apply Ord_le_Succ with i.
inversion H as [| a b j |].
apply IH with j.
assumption.
constructor.
intro n.
inversion_clear H.
apply IH with i.
trivial.
Qed.
forall alpha beta (i : pd_type beta),
alpha <= beta[i] ->
alpha <= beta.
Proof.
induction alpha as [| alpha IH | f IH]; intros beta i H.
constructor.
apply Ord_le_Succ with i.
inversion H as [| a b j |].
apply IH with j.
assumption.
constructor.
intro n.
inversion_clear H.
apply IH with i.
trivial.
Qed.
If alpha <= beta, all predecessors of alpha <= beta.
Lemma ord_le_pd_left :
forall alpha beta (i : pd_type alpha),
alpha <= beta ->
alpha[i] <= beta.
Proof.
intros alpha beta i H.
induction H as [| alpha beta j H IH | f beta H IH].
destruct i.
destruct i as [[] | i']; apply ord_le_pd_right with j.
apply H.
apply IH.
destruct i.
apply IH.
Qed.
forall alpha beta (i : pd_type alpha),
alpha <= beta ->
alpha[i] <= beta.
Proof.
intros alpha beta i H.
induction H as [| alpha beta j H IH | f beta H IH].
destruct i.
destruct i as [[] | i']; apply ord_le_pd_right with j.
apply H.
apply IH.
destruct i.
apply IH.
Qed.
If alpha <= beta, alpha <= the successor of beta.
Lemma ord_le_succ_right :
forall alpha beta,
alpha <= beta ->
alpha <= Succ beta.
Proof.
induction alpha as [| alpha _ | f IH]; intros beta H.
constructor.
inversion_clear H.
apply Ord_le_Succ with (inr unit i).
assumption.
constructor.
intro n.
apply IH.
inversion_clear H.
trivial.
Qed.
forall alpha beta,
alpha <= beta ->
alpha <= Succ beta.
Proof.
induction alpha as [| alpha _ | f IH]; intros beta H.
constructor.
inversion_clear H.
apply Ord_le_Succ with (inr unit i).
assumption.
constructor.
intro n.
apply IH.
inversion_clear H.
trivial.
Qed.
If the successor of alpha <= beta, alpha <= beta.
Lemma ord_le_succ_left :
forall alpha beta,
Succ alpha <= beta ->
alpha <= beta.
Proof.
intros alpha beta H.
rewrite (first_pd_after_succ_id alpha).
apply ord_le_pd_left.
assumption.
Qed.
forall alpha beta,
Succ alpha <= beta ->
alpha <= beta.
Proof.
intros alpha beta H.
rewrite (first_pd_after_succ_id alpha).
apply ord_le_pd_left.
assumption.
Qed.
If the successor of alpha <= the successor of beta, alpha <= beta.
Lemma ord_le_succ_elim :
forall alpha beta,
Succ alpha <= Succ beta ->
alpha <= beta.
Proof.
inversion_clear 1.
destruct i as [[] |]; [| apply ord_le_pd_right with p]; assumption.
Qed.
forall alpha beta,
Succ alpha <= Succ beta ->
alpha <= beta.
Proof.
inversion_clear 1.
destruct i as [[] |]; [| apply ord_le_pd_right with p]; assumption.
Qed.
If the alpha <= beta, the successor of alpha <= the successor of beta.
Lemma ord_le_succ_intro :
forall alpha beta,
alpha <= beta ->
Succ alpha <= Succ beta.
Proof.
intros.
apply Ord_le_Succ with (inl (pd_type beta) tt).
assumption.
Qed.
forall alpha beta,
alpha <= beta ->
Succ alpha <= Succ beta.
Proof.
intros.
apply Ord_le_Succ with (inl (pd_type beta) tt).
assumption.
Qed.
No successor of alpha is <= alpha.
Lemma ord_le_not_succ :
forall alpha, ~ Succ alpha <= alpha.
Proof.
induction alpha as [| alpha IH | f IH]; intro H.
apply ord_le_not_succ_zero with Zero.
assumption.
apply IH.
exact (ord_le_succ_elim H).
inversion_clear H as [| a b i H' |].
inversion_clear H' as [| | a b H].
destruct i as [n i].
apply IH with n.
apply Ord_le_Succ with i.
apply H.
Qed.
forall alpha, ~ Succ alpha <= alpha.
Proof.
induction alpha as [| alpha IH | f IH]; intro H.
apply ord_le_not_succ_zero with Zero.
assumption.
apply IH.
exact (ord_le_succ_elim H).
inversion_clear H as [| a b i H' |].
inversion_clear H' as [| | a b H].
destruct i as [n i].
apply IH with n.
apply Ord_le_Succ with i.
apply H.
Qed.
If alpha <= a function value, alpha <= the limit of that function.
Suggested by Bruno Barras.
Lemma ord_le_limit_right :
forall alpha f n,
alpha <= f n ->
alpha <= Limit f.
Proof.
induction alpha as [| alpha _ | f IH]; intros g n H.
constructor.
inversion_clear H.
apply Ord_le_Succ with (existT (fun n => pd_type (g n)) n i).
assumption.
constructor.
intro m.
apply (IH m g n).
inversion_clear H.
trivial.
Qed.
forall alpha f n,
alpha <= f n ->
alpha <= Limit f.
Proof.
induction alpha as [| alpha _ | f IH]; intros g n H.
constructor.
inversion_clear H.
apply Ord_le_Succ with (existT (fun n => pd_type (g n)) n i).
assumption.
constructor.
intro m.
apply (IH m g n).
inversion_clear H.
trivial.
Qed.
If a limit <= alpha, any value value of the function <= alpha.
Lemma ord_le_limit_left :
forall alpha f n,
Limit f <= alpha ->
f n <= alpha.
Proof.
intros alpha f n H.
inversion_clear H.
trivial.
Qed.
forall alpha f n,
Limit f <= alpha ->
f n <= alpha.
Proof.
intros alpha f n H.
inversion_clear H.
trivial.
Qed.
<= is reflexive.
Lemma ord_le_refl :
forall alpha, alpha <= alpha.
Proof.
induction alpha as [| alpha IH | f IH].
constructor.
apply Ord_le_Succ with (inl (pd_type alpha) tt).
assumption.
constructor.
intro n.
apply ord_le_limit_right with n.
apply IH.
Qed.
forall alpha, alpha <= alpha.
Proof.
induction alpha as [| alpha IH | f IH].
constructor.
apply Ord_le_Succ with (inl (pd_type alpha) tt).
assumption.
constructor.
intro n.
apply ord_le_limit_right with n.
apply IH.
Qed.
<= is transitive.
Lemma ord_le_trans :
forall alpha beta gamma,
alpha <= beta ->
beta <= gamma ->
alpha <= gamma.
Proof.
intros alpha beta gamma H1.
revert gamma.
induction H1 as [| alpha beta i H IH | f beta H IH]; intros gamma H2.
constructor.
induction H2 as [| beta gamma j H' _ | f gamma H' IH'].
destruct i.
apply Ord_le_Succ with j.
apply IH.
destruct i as [[] | i']; simpl in * |- *.
assumption.
apply ord_le_pd_left.
assumption.
destruct i as [n i]; simpl in * |- *.
apply (IH' n i H IH).
constructor.
intro n.
exact (IH n gamma H2).
Qed.
forall alpha beta gamma,
alpha <= beta ->
beta <= gamma ->
alpha <= gamma.
Proof.
intros alpha beta gamma H1.
revert gamma.
induction H1 as [| alpha beta i H IH | f beta H IH]; intros gamma H2.
constructor.
induction H2 as [| beta gamma j H' _ | f gamma H' IH'].
destruct i.
apply Ord_le_Succ with j.
apply IH.
destruct i as [[] | i']; simpl in * |- *.
assumption.
apply ord_le_pd_left.
assumption.
destruct i as [n i]; simpl in * |- *.
apply (IH' n i H IH).
constructor.
intro n.
exact (IH n gamma H2).
Qed.
<= is antisymmetric (for ==).
Lemma ord_le_antisymm :
forall alpha beta,
alpha <= beta ->
beta <= alpha ->
alpha == beta.
Proof.
intros.
unfold ord_eq.
split; assumption.
Qed.
forall alpha beta,
alpha <= beta ->
beta <= alpha ->
alpha == beta.
Proof.
intros.
unfold ord_eq.
split; assumption.
Qed.
== is reflexive.
== is symmetric.
== is transitive.
Lemma ord_eq_trans :
forall alpha beta gamma,
alpha == beta ->
beta == gamma ->
alpha == gamma.
Proof.
destruct 1.
destruct 1.
split; apply ord_le_trans with beta; assumption.
Qed.
forall alpha beta gamma,
alpha == beta ->
beta == gamma ->
alpha == gamma.
Proof.
destruct 1.
destruct 1.
split; apply ord_le_trans with beta; assumption.
Qed.
Not zero < zero.
If alpha <= beta, not beta <= a predecessor of alpha.
Lemma ord_le_not_pd_right :
forall alpha beta i,
alpha <= beta ->
~ beta <= alpha[i].
Proof.
induction alpha as [| alpha IH | f IH]; intros beta i H1 H2.
destruct i.
destruct i.
destruct u.
apply ord_le_not_succ with alpha.
apply ord_le_trans with beta; assumption.
exact (IH beta p (ord_le_succ_left H1) H2).
destruct i.
inversion_clear H1.
exact (IH x beta p (H x) H2).
Qed.
forall alpha beta i,
alpha <= beta ->
~ beta <= alpha[i].
Proof.
induction alpha as [| alpha IH | f IH]; intros beta i H1 H2.
destruct i.
destruct i.
destruct u.
apply ord_le_not_succ with alpha.
apply ord_le_trans with beta; assumption.
exact (IH beta p (ord_le_succ_left H1) H2).
destruct i.
inversion_clear H1.
exact (IH x beta p (H x) H2).
Qed.
Not alpha <= a predecessor of alpha.
Lemma ord_le_not_pd_right_weak :
forall alpha i, ~ alpha <= alpha[i].
Proof.
intros.
apply ord_le_not_pd_right.
apply ord_le_refl.
Qed.
forall alpha i, ~ alpha <= alpha[i].
Proof.
intros.
apply ord_le_not_pd_right.
apply ord_le_refl.
Qed.
< is transitive.
Lemma ord_lt_trans :
forall alpha beta gamma,
alpha < beta ->
beta < gamma ->
alpha < gamma.
Proof.
intros alpha beta gamma.
destruct 1 as [i].
destruct 1 as [j].
exists j.
apply ord_le_trans with beta; [apply ord_le_pd_right with i |]; assumption.
Qed.
forall alpha beta gamma,
alpha < beta ->
beta < gamma ->
alpha < gamma.
Proof.
intros alpha beta gamma.
destruct 1 as [i].
destruct 1 as [j].
exists j.
apply ord_le_trans with beta; [apply ord_le_pd_right with i |]; assumption.
Qed.
< is irreflexive.
Lemma ord_lt_irrefl :
forall alpha, ~ alpha < alpha.
Proof.
intros alpha H.
destruct H as [i H].
exact (ord_le_not_pd_right_weak i H).
Qed.
forall alpha, ~ alpha < alpha.
Proof.
intros alpha H.
destruct H as [i H].
exact (ord_le_not_pd_right_weak i H).
Qed.
< is asymmetric.
Lemma ord_lt_asymm :
forall alpha beta,
alpha < beta ->
~ beta < alpha.
Proof.
intros alpha beta H1 H2.
destruct H1 as [i H1].
destruct H2 as [j H2].
apply (@ord_le_not_pd_right alpha beta j);
[apply ord_le_pd_right with i |]; assumption.
Qed.
forall alpha beta,
alpha < beta ->
~ beta < alpha.
Proof.
intros alpha beta H1 H2.
destruct H1 as [i H1].
destruct H2 as [j H2].
apply (@ord_le_not_pd_right alpha beta j);
[apply ord_le_pd_right with i |]; assumption.
Qed.
pd_type is closed under transitivity.
Lemma pd_trans :
forall alpha i j,
exists k, pd alpha k = pd (pd alpha i) j.
Proof.
induction alpha as [| alpha IH | f IH]; intros.
elim i.
destruct i as [[] | i]; simpl in j |- *.
exists (inr _ j).
reflexivity.
destruct (IH i j) as [k H].
exists (inr _ k).
assumption.
destruct i as [n i]; simpl in j |- *.
destruct (IH n i j) as [k H].
exists (existT (fun n => pd_type (f n)) n k).
assumption.
Qed.
forall alpha i j,
exists k, pd alpha k = pd (pd alpha i) j.
Proof.
induction alpha as [| alpha IH | f IH]; intros.
elim i.
destruct i as [[] | i]; simpl in j |- *.
exists (inr _ j).
reflexivity.
destruct (IH i j) as [k H].
exists (inr _ k).
assumption.
destruct i as [n i]; simpl in j |- *.
destruct (IH n i j) as [k H].
exists (existT (fun n => pd_type (f n)) n k).
assumption.
Qed.
If the successor of alpha < beta, alpha < beta.
Lemma ord_lt_succ_left :
forall alpha beta,
Succ alpha < beta ->
alpha < beta.
Proof.
intros alpha beta.
destruct 1 as [i H].
exists i.
apply ord_le_succ_left.
assumption.
Qed.
forall alpha beta,
Succ alpha < beta ->
alpha < beta.
Proof.
intros alpha beta.
destruct 1 as [i H].
exists i.
apply ord_le_succ_left.
assumption.
Qed.
If alpha < beta, alpha < the successor of beta.
Lemma ord_lt_succ_right :
forall alpha beta,
alpha < beta ->
alpha < Succ beta.
Proof.
intros alpha beta.
destruct 1 as [i H].
exists (inl (pd_type beta) tt).
apply ord_le_pd_right with i.
assumption.
Qed.
forall alpha beta,
alpha < beta ->
alpha < Succ beta.
Proof.
intros alpha beta.
destruct 1 as [i H].
exists (inl (pd_type beta) tt).
apply ord_le_pd_right with i.
assumption.
Qed.
If alpha < beta, alpha <= beta.
Lemma ord_lt_ord_le :
forall alpha beta, alpha < beta -> alpha <= beta.
Proof.
intros alpha beta.
destruct 1 as [i H].
apply ord_le_pd_right with i.
assumption.
Qed.
forall alpha beta, alpha < beta -> alpha <= beta.
Proof.
intros alpha beta.
destruct 1 as [i H].
apply ord_le_pd_right with i.
assumption.
Qed.
If alpha < beta, the successor of alpha <= beta.
Lemma ord_lt_ord_le_succ :
forall alpha beta,
alpha < beta ->
Succ alpha <= beta.
Proof.
intros alpha beta.
destruct 1 as [i H].
apply Ord_le_Succ with i.
assumption.
Qed.
forall alpha beta,
alpha < beta ->
Succ alpha <= beta.
Proof.
intros alpha beta.
destruct 1 as [i H].
apply Ord_le_Succ with i.
assumption.
Qed.
If alpha < beta, not beta <= alpha.
Lemma ord_lt_not_ord_le :
forall alpha beta,
alpha < beta ->
~ beta <= alpha.
Proof.
intros alpha beta H1 H2.
destruct H1 as [i H1].
apply (@ord_le_not_pd_right beta alpha i); assumption.
Qed.
forall alpha beta,
alpha < beta ->
~ beta <= alpha.
Proof.
intros alpha beta H1 H2.
destruct H1 as [i H1].
apply (@ord_le_not_pd_right beta alpha i); assumption.
Qed.
If alpha <= a predecessor of the successor of beta, alpha <= beta.
Lemma ord_le_succ_pd_right :
forall alpha beta i,
alpha <= Succ beta [i] ->
alpha <= beta.
Proof.
induction alpha; intros.
simpl in H.
destruct i.
destruct u.
assumption.
apply Ord_le_Zero.
destruct beta.
destruct i.
destruct u.
destruct (ord_le_not_succ_zero H).
destruct p.
apply Ord_le_Succ with (inl (pd_type beta) tt).
simpl.
simpl in H.
destruct i.
destruct u.
apply ord_le_succ_elim.
assumption.
destruct p.
apply ord_le_succ_left.
destruct u.
assumption.
apply ord_le_succ_left.
apply ord_le_pd_right with p.
assumption.
simpl in H.
destruct i.
destruct u.
assumption.
destruct p.
apply ord_le_limit_right with x.
apply ord_le_pd_right with p.
assumption.
apply Ord_le_Limit.
intro.
inversion_clear H0.
apply H with i.
apply H1.
Qed.
forall alpha beta i,
alpha <= Succ beta [i] ->
alpha <= beta.
Proof.
induction alpha; intros.
simpl in H.
destruct i.
destruct u.
assumption.
apply Ord_le_Zero.
destruct beta.
destruct i.
destruct u.
destruct (ord_le_not_succ_zero H).
destruct p.
apply Ord_le_Succ with (inl (pd_type beta) tt).
simpl.
simpl in H.
destruct i.
destruct u.
apply ord_le_succ_elim.
assumption.
destruct p.
apply ord_le_succ_left.
destruct u.
assumption.
apply ord_le_succ_left.
apply ord_le_pd_right with p.
assumption.
simpl in H.
destruct i.
destruct u.
assumption.
destruct p.
apply ord_le_limit_right with x.
apply ord_le_pd_right with p.
assumption.
apply Ord_le_Limit.
intro.
inversion_clear H0.
apply H with i.
apply H1.
Qed.
Ordinal arithmetic.
Fixpoint add (alpha beta : ord) : ord :=
match beta with
| Zero => alpha
| Succ beta => Succ (add alpha beta)
| Limit f => Limit (fun o => add alpha (f o))
end.
Fixpoint mul (alpha beta : ord) : ord :=
match beta with
| Zero => Zero
| Succ beta => add (mul alpha beta) alpha
| Limit f => Limit (fun o => mul alpha (f o))
end.
Fixpoint exp (alpha beta : ord) : ord :=
match beta with
| Zero => Succ Zero
| Succ beta => mul (exp alpha beta) alpha
| Limit f => Limit (fun o => exp alpha (f o))
end.
Lemma ord_le_add_right :
forall alpha beta,
alpha <= add alpha beta.
Proof.
intros alpha beta.
induction beta as [| beta IH | f IH].
apply ord_le_refl.
apply ord_le_succ_right.
exact IH.
apply ord_le_limit_right with 0.
apply IH.
Qed.
Lemma ord_le_add :
forall alpha beta gamma,
beta <= gamma ->
add alpha beta <= add alpha gamma.
Proof.
intros alpha beta gamma H.
induction H as [gamma | beta gamma i H IH | f gamma H IH].
apply ord_le_add_right.
induction gamma as [| gamma IHg | f IHg]; simpl.
elim i.
destruct i as [[] | i].
apply Ord_le_Succ with (inl (pd_type (add alpha gamma)) tt).
apply IH.
apply ord_le_succ_right.
apply IHg with i; assumption.
destruct i as [n i].
apply ord_le_limit_right with n.
apply IHg with i; assumption.
constructor.
intro n.
apply IH.
Qed.
Lemma ord_lt_add :
forall alpha beta gamma,
beta < gamma ->
add alpha beta < add alpha gamma.
Proof.
intros alpha beta gamma H.
unfold ord_lt; destruct H as [i H].
induction gamma as [| gamma _ | f IH]; simpl.
destruct i.
exists (inl _ tt); simpl.
apply ord_le_add.
destruct i as [[] | i].
assumption.
apply ord_le_pd_right with i.
assumption.
destruct i as [n i].
specialize IH with n i.
destruct IH as [j IH].
assumption.
exists (existT (fun n => pd_type (add alpha (f n))) n j).
assumption.
Qed.
The natural numbers can be coerced into finite ordinals.
Fixpoint nat_as_ord (n : nat) : ord :=
match n with
| O => Zero
| S n => Succ (nat_as_ord n)
end.
Coercion nat_as_ord : nat >-> ord.
The smallest infinite ordinal is the limit of the natural numbers.
We show that <= and < on ordinals are the same as <= and < on
natural numbers.
Require Import Le.
Lemma le_implies_ord_le : forall n m, (n <= m)%nat -> n <= m.
Proof.
induction n as [| n IH]; intros m H.
constructor.
destruct m as [| m].
contradiction le_Sn_0 with n.
apply ord_le_succ_intro.
apply IH.
apply le_S_n.
assumption.
Qed.
Lemma ord_le_implies_le : forall (n m : nat), n <= m -> (n <= m)%nat.
Proof.
induction n as [| n IH]; intros m H.
apply le_0_n.
destruct m as [| m].
contradiction ord_le_not_succ_zero with n.
apply le_n_S.
apply IH.
apply ord_le_succ_elim.
assumption.
Qed.
Lemma ord_le_le : forall n m, (n <= m)%nat <-> n <= m.
Proof.
split.
apply le_implies_ord_le.
apply ord_le_implies_le.
Qed.
Require Import Lt.
Lemma lt_implies_ord_lt : forall n m, (n < m)%nat -> n < m.
Proof.
induction n as [| n IH]; intros m H.
destruct H; exists (inl _ tt); constructor.
destruct m as [| m].
contradiction lt_n_O with (S n).
exists (inl _ tt).
apply ord_lt_ord_le_succ; simpl.
apply IH.
apply lt_S_n.
assumption.
Qed.
Lemma ord_lt_implies_lt : forall (n m : nat), n < m -> (n < m)%nat.
Proof.
induction n as [| n IH]; intros m H.
destruct H as [i H].
destruct m as [| m].
elim i.
apply lt_0_Sn.
destruct H as [i H].
destruct m as [| m].
elim i.
apply lt_n_S.
apply IH.
destruct m as [| m].
destruct i as [[] | []].
contradiction ord_le_not_succ_zero with n.
exists (inl _ tt).
destruct i as [[] | [[] | i]].
apply ord_le_succ_elim.
assumption.
apply ord_le_succ_left.
assumption.
apply ord_le_succ_left.
apply ord_le_pd_right with i.
assumption.
Qed.
Lemma ord_lt_lt : forall n m, (n < m)%nat <-> n < m.
Proof.
split.
apply lt_implies_ord_lt.
apply ord_lt_implies_lt.
Qed.
We now prove two simple facts about our equality == containing
different representations of omega.
Lemma fact_a :
Limit (fun n => S n) == omega.
Proof.
split; constructor; intro n.
apply Ord_le_Succ with (existT (fun n:nat => pd_type n) (S n) (inl _ tt)).
apply ord_le_refl.
destruct n as [| n].
constructor.
apply Ord_le_Succ with (existT (fun n:nat => pd_type (S n)) n (inl _ tt)).
apply ord_le_refl.
Qed.
Lemma fact_b :
Limit (fun n => n * 2) == omega.
Proof.
split; constructor; intro n.
destruct n as [| n]; simpl.
constructor.
apply Ord_le_Succ with (existT (fun n:nat => pd_type n) (S (S (n * 2))) (inl _ tt)).
apply ord_le_refl.
destruct n as [| n].
constructor.
apply Ord_le_Succ with (existT (fun n:nat => pd_type (n * 2)) (S n) (inl _ tt)).
simpl.
induction n as [| n IH]; simpl.
constructor.
apply ord_le_succ_right.
apply ord_le_succ_intro.
exact IH.
Qed.
A weak inversion property of ordinals equal to omega.
Lemma ord_eq_omega_discriminate :
forall alpha,
alpha == omega ->
exists f, alpha = Limit f.
Proof.
intros [| alpha | f] [H1 H2].
inversion_clear H2.
contradict (ord_le_not_succ_zero (H 1)).
inversion_clear H1.
inversion_clear H2.
destruct i as [n i].
contradict (ord_le_not_pd_right i (ord_le_succ_elim (H0 (S n))) H).
exists f; reflexivity.
Qed.
Close Scope ord_scope.
forall alpha,
alpha == omega ->
exists f, alpha = Limit f.
Proof.
intros [| alpha | f] [H1 H2].
inversion_clear H2.
contradict (ord_le_not_succ_zero (H 1)).
inversion_clear H1.
inversion_clear H2.
destruct i as [n i].
contradict (ord_le_not_pd_right i (ord_le_succ_elim (H0 (S n))) H).
exists f; reflexivity.
Qed.
Close Scope ord_scope.