Library RelationAlgebra.ordinal


ordinal: finite ordinals, sets of finite ordinals


Require Import List.
Require Import common comparisons.

Set Standard Proposition Elimination Names.
Local Unset Injection On Proofs.
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.
Notation "i < j" := (ltb i j = true).
Notation "i <= j" := (ltb j i = false).

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 H 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 Plus.plus_reg_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 Plus.plus_reg_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

bounds about the various operations
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.

additional lemmas


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.