# ordinal: finite ordinals, sets of finite ordinals

Require Import List.
Require Import PeanoNat.
Require Import common comparisons.

Set Implicit Arguments.

# Boolean strict order on natural numbers

Fixpoint ltb i j :=
match i,j with
| O,S _true
| _,Ofalse
| S i, S jltb i j
end.
Declare Scope ltb_scope.
Notation "i < j" := (ltb i j = true) : ltb_scope.
Notation "i <= j" := (ltb j i = false) : ltb_scope.
Delimit Scope ltb_scope with ltb.
Local Open Scope ltb_scope.

Lemma ltb_plus_l i m n: i<m i<m+n.
Proof. revert i; induction m; destruct i; simpl; auto; discriminate. Qed.

Lemma ltb_plus_r i m n: i<n m+i<m+n.
Proof. revert i; induction m; destruct i; simpl; auto; discriminate. Qed.

Lemma leb_plus_r i n: n n+i.
Proof. induction n; simpl. now destruct i. assumption. Qed.

Lemma ltb_minus n m i: i<n+m n i i-n < m.
Proof. revert n. induction i; destruct n; simpl; auto. discriminate. Qed.

Lemma lt_n_1 a: a<1 a=0.
Proof. destruct a as [|[|?]]; trivial; discriminate. Qed.

Definition lt_ge_dec i n: {i<n}+{ni}.
Proof. case_eq (ltb i n). now left. now right. Defined.

# Additional induction schemes for natural numbers

Lemma ltb_ind (P: nat nat Prop)
(H0: n, P (S n) 0)
(HS: n i, P n i P (S n) (S i)):
n i, i<n P n i.
Proof.
induction n; intros i Hi. destruct i; discriminate.
destruct i. apply H0. now apply HS, IHn.
Qed.

Lemma nat_ind_2: P: nat Prop,
P 0 P 1 ( n, P n P ((S (S n)))) n, P n.
Proof.
intros P H0 H1 HSS.
assert (G: m, P m P (S m)).
induction m. split; assumption.
destruct IHm as [IHm IHSm].
split. assumption. apply (HSS m), IHm.
intro n. destruct (G n). assumption.
Qed.

# Ordinals

we use a record rather than a dependent inductive in order to
• get slightly more efficient computations
• get simpler proofs
using a Boolean strict order also simplifies proofs w.r.t. using the lt predicate from the standard library
Record ord n := Ord {nat_of_ord:> nat; ord_lt: nat_of_ord<n}.
Arguments Ord [_] i _: rename.

zero and successor
Definition ord0 {n}: ord (S n) := @Ord (S n) 0 eq_refl.
Definition ordS {n} (i: ord n): ord (S n) := @Ord (S n) (S i) (ord_lt i).

## ordinals as a cmpType

we just compare the underlying natural numbers
Definition eqb_ord {n} (i j: ord n) := eqb_nat i j.

Lemma eq_ord n (i j: ord n): @eq nat i j i=j.
Proof. destruct i; destruct j; simpl; intro. subst. f_equal. apply UIP_cmp. Qed.

Lemma eqb_ord_spec n (i j: ord n): reflect (i=j) (eqb_ord i j).
Proof.
unfold eqb_ord. case eqb_spec; intro E; constructor.
apply eq_ord, E. congruence.
Qed.

Definition ord_compare {n} (i j: ord n) := nat_compare i j.
Lemma ord_compare_spec n (i j: ord n): compare_spec (i=j) (ord_compare i j).
Proof.
unfold ord_compare.
case cmp_spec; constructor; try apply eq_ord; congruence.
Qed.

Canonical Structure cmp_ord n := mk_cmp _ (@eqb_ord_spec n) _ (@ord_compare_spec n).

## basic properties

ord 0 is empty
Lemma ord_0_empty: ord 0 False.
Proof. intros [[|?]]; discriminate. Qed.

ord 1 has only one element: 0
Lemma ord0_unique: i: ord 1, i=ord0.
Proof.
intros [[|i] Hi]; apply eq_ord. reflexivity.
destruct i; discriminate.
Qed.

induction scheme for ordinals
Lemma ord_ind' (P: n, ord n Prop)
(H0: n, P (S n) ord0)
(HS: n i, P n i P (S n) (ordS i)):
n i, P n i.
Proof.
induction n. intro i. elim (ord_0_empty i).
destruct i as [[|i] Hi].
replace (Ord 0 Hi) with (@ord0 n) by now apply eq_ord. apply H0.
replace (Ord (S i) Hi) with (ordS (@Ord n i Hi)) by now apply eq_ord. apply HS, IHn.
Qed.

## sequence of all ordinals below n

Fixpoint seq n: list (ord n) :=
match n with
| 0 ⇒ nil
| S ncons ord0 (map ordS (seq n))
end.

completeness of the above sequence
Lemma in_seq: {n} (i: ord n), In i (seq n).
Proof.
induction i using ord_ind'. now left.
right. rewrite in_map_iff. eauto.
Qed.

## shifting ans splitting ordinals

shifting
Definition lshift {m n} (i: ord m): ord (m+n) := Ord i (ltb_plus_l _ _ _ (ord_lt i)).
Definition rshift {m n} (i: ord n): ord (m+n) := Ord (m+i) (ltb_plus_r _ _ _ (ord_lt i)).

spliting the sequence of all ordinals
Lemma seq_cut n m: seq (n+m) = map lshift (seq n) ++ map rshift (seq m).
Proof.
induction n; simpl.
rewrite <-(map_id (seq m)) at 1. apply map_ext.
intros [i Hi]. apply eq_ord. reflexivity.
rewrite IHn, map_app. f_equal. apply eq_ord. reflexivity.
rewrite 3map_map. f_equal; apply map_ext; intros [i Hi]; apply eq_ord; reflexivity.
Qed.

splitting an ordinal
Definition split {n m} (i: ord (n+m)): ord n + ord m :=
match lt_ge_dec i n with
| left Hiinl _ (Ord _ Hi)
| right Hjinr _ (Ord _ (ltb_minus _ _ _ (ord_lt i) Hj))
end.

Inductive split_case n m (i: ord (n+m)): ord n + ord m Set :=
| split_l: j: ord n, i=lshift j split_case i (inl j)
| split_r: j: ord m, i=rshift j split_case i (inr j).

Lemma split_spec n m (i: ord (n+m)): split_case i (split i).
Proof.
unfold split. case lt_ge_dec; constructor; apply eq_ord; simpl. reflexivity.
destruct i as [j Hj]. simpl in ×. revert n m e Hj.
induction j; destruct n; simpl; auto. discriminate.
intros. f_equal. eapply IHj; eassumption.
Qed.

basic properties of split and shifting
Lemma split_lshift n m i: @split n m (lshift i) = inl i.
Proof.
case split_spec; intros j E.
f_equal. apply eq_ord. injection E. congruence.
exfalso. injection E. clear E. destruct i as [i Hi].
simpl. intros →. rewrite leb_plus_r in Hi. discriminate.
Qed.

Lemma split_rshift n m i: @split n m (rshift i) = inr i.
Proof.
case split_spec; intros j E.
exfalso. injection E. clear E. destruct j as [j Hj]. simpl. intros <-.
rewrite leb_plus_r in Hj. discriminate.
f_equal. apply eq_ord. symmetry. injection E. apply Nat.add_cancel_l.
Qed.

Lemma eqb_ord_lrshift n m i j: eqb_ord (@lshift n m i) (@rshift n m j) = false.
Proof.
destruct i as [i Hi]; destruct j as [j Hj]. unfold eqb_ord. simpl.
case eqb_spec; trivial. intro E. rewrite E in Hi. rewrite leb_plus_r in Hi. discriminate.
Qed.

Lemma eqb_ord_rlshift n m i j: eqb_ord (@rshift n m i) (@lshift n m j) = false.
Proof. rewrite eqb_sym. apply eqb_ord_lrshift. Qed.

Lemma eqb_ord_rrshift n m i j: eqb_ord (@rshift n m i) (@rshift n m j) = eqb_ord i j.
Proof.
destruct i as [i Hi]; destruct j as [j Hj]. unfold eqb_ord. simpl.
do 2 case eqb_spec; trivial. intros E E'. elim E. eapply Nat.add_cancel_l, E'.
congruence.
Qed.

Lemma split_ord0 m: @split 1 m ord0 = inl ord0.
Proof. reflexivity. Qed.

Lemma split_ordS m i: @split 1 m (ordS i) = inr i.
Proof.
case split_spec; intros j Hj.
rewrite (ord0_unique j) in Hj. discriminate.
destruct i; destruct j. injection Hj. intros <-. f_equal. now apply eq_ord.
Qed.

# Finite sets of ordinals as ordinals

we encode a finite subset of ord n as an element of ord (2^n), using the coding of the characteristic function of the set as a bitvector of length n
since we need to compute a little bit with these encoded sets, we first define the bijection on natural numbers, before encapsulating into ordinals.
Module set.

## on natural numbers

xO' i = 2*i, xI' i = 2*i+1
Fixpoint xO' i := match i with 0 ⇒ 0 | S iS (S (xO' i)) end.
Fixpoint xI' i := match i with 0 ⇒ 1 | S iS (S (xI' i)) end.

from characteristic functions to natural numbers: accumulate bits until a given length (n) is reached
Fixpoint of_fun' n (f: nat bool): nat :=
match n with
| 0 ⇒ 0
| S nif f 0
then xI' (of_fun' n (fun if (S i)))
else xO' (of_fun' n (fun if (S i)))
end.

od x returns the pair (o,y) s.t. x = 2*y+o
Fixpoint od x :=
match x with
| O(false,O)
| S O(true,O)
| S (S x) ⇒ let (o,x) := od x in (o,S x)
end.

testing membership: read the ith bit, using od this function is presented in such a strange way to get efficiency: the partial application mem' n x reduces to the pattern matching function that precisely corresponds to the membership function of x. For instance, mem' 4 {1,2} reduces to fun i match i with 0 | 3 false | 1 | 2 true | _ assert_false end
Fixpoint mem' n x :=
match n with
| 0 ⇒ fun iassert_false false
| S n
let (o,x) := od x in
let f := mem' n x in
fun imatch i with Oo | S if i end
end.

correctness of mem' and of_fun'
Lemma od_xO i: od (xO' i) = (false,i).
Proof. induction i; simpl. reflexivity. now rewrite IHi. Qed.

Lemma od_xI i: od (xI' i) = (true,i).
Proof. induction i; simpl. reflexivity. now rewrite IHi. Qed.

Lemma mem_of_fun' n: f i, i<n mem' n (of_fun' n f) i = f i.
Proof.
induction n; intros f i Hi; simpl. destruct i; discriminate.
case_eq (f 0); intro H.
rewrite od_xI. destruct i. congruence. now rewrite IHn.
rewrite od_xO. destruct i. congruence. now rewrite IHn.
Qed.

## encapsulation into ordinals

Lemma xO_bound: n i, i<n xO' i < double n.
Proof. now apply ltb_ind. Qed.

Lemma xI_bound: n i, i<n xI' i < double n.
Proof. now apply ltb_ind. Qed.

Lemma of_fun_bound: n f, of_fun' n f < pow2 n.
Proof.
induction n; intro f. reflexivity.
simpl. case f.
now apply xI_bound.
now apply xO_bound.
Qed.

Lemma od_bound a: n, a < double n snd (od a) < n.
Proof.
induction a using nat_ind_2; intros n Hn; simpl.
destruct n; simpl. discriminate. reflexivity.
destruct n; simpl. discriminate. reflexivity.
revert IHa. case od; simpl. intros o a' IH.
destruct n. discriminate. apply IH, Hn.
Qed.

extending a Boolean function on ordinals into a function on natural numbers
Definition app' n (f: ord n bool) (i: nat) :=
match lt_ge_dec i n with
| left Hf (Ord i H)
| _false
end.

encapsulation of the various operations into ordinals
Definition xO n (i: ord n): ord (double n) := Ord (xO' i) (xO_bound _ _ (ord_lt i)).
Definition xI n (i: ord n): ord (double n) := Ord (xI' i) (xI_bound _ _ (ord_lt i)).
Definition mem n (x: ord (pow2 n)) (i: ord n) := mem' n x i.
Definition of_fun n (f: ord n bool): ord (pow2 n) := Ord (of_fun' n (app' f)) (of_fun_bound _ _).
retraction from ord n bool into ord (pow2 n)
Lemma mem_of_fun n (f: ord n bool) i: mem (of_fun f) i = f i.
Proof.
unfold mem, of_fun. simpl. rewrite mem_of_fun' by apply ord_lt.
unfold app'. case lt_ge_dec. intros. f_equal. now apply eq_ord.
rewrite (ord_lt i). discriminate.
Qed.

injectivity of the od function
Lemma od_inj a b: od a = od b a = b.
Proof.
revert b. induction a using nat_ind_2; intros [|[|b]]; simpl;
trivial; (try (case od; discriminate)); (try discriminate).
intro. f_equal. f_equal. apply IHa. revert H.
case od. case od. congruence.
Qed.

extensionality on natural numbers
Lemma ext' n: a b,
a<pow2 n b<pow2 n ( i, i<n mem' n a i = mem' n b i)
a = b.
Proof.
induction n; simpl; intros a b Ha Hb H.
rewrite lt_n_1 by assumption. now apply lt_n_1.
apply od_inj. revert H. generalize (od_bound _ _ Ha), (od_bound _ _ Hb).
case od. intros oa a' Ha'.
case od. intros ob b' Hb'.
intro H. f_equal.
apply (H 0 eq_refl).
apply IHn; trivial. intros i Hi. apply (H (S i) Hi).
Qed.

extensionality on ordinals (i.e., with mem_of_fun, mem/of_fun form a bijection)
Lemma ext n (a b: ord (pow2 n)): ( i, mem a i = mem b i) a = b.
Proof.
intro H. apply eq_ord. eapply ext'. apply ord_lt. apply ord_lt.
intros i Hi. apply (H (Ord i Hi)).
Qed.

Lemma xO_0 n: xO (@ord0 n) = @ord0 (S (double n)).
Proof. now apply eq_ord. Qed.
Lemma xO_S n (i: ord n): xO (ordS i) = ordS (ordS (xO i)).
Proof. now apply eq_ord. Qed.
Lemma xI_0 n: xI (@ord0 n) = ordS (@ord0 (double n)).
Proof. now apply eq_ord. Qed.
Lemma xI_S n (i: ord n): xI (ordS i) = ordS (ordS (xI i)).
Proof. now apply eq_ord. Qed.

Lemma mem_xO_0 n (f: ord (pow2 n)): @mem (S n) (xO f) ord0 = false.
Proof. unfold mem. simpl. now rewrite od_xO. Qed.
Lemma mem_xO_S n (f: ord (pow2 n)) i: @mem (S n) (xO f) (ordS i) = mem f i.
Proof. unfold mem. simpl. now rewrite od_xO. Qed.
Lemma mem_xI_0 n (f: ord (pow2 n)): @mem (S n) (xI f) ord0 = true.
Proof. unfold mem. simpl. now rewrite od_xI. Qed.
Lemma mem_xI_S n (f: ord (pow2 n)) i: @mem (S n) (xI f) (ordS i) = mem f i.
Proof. unfold mem. simpl. now rewrite od_xI. Qed.

End set.