# pair: encoding pairs of ordinals as ordinals

more precisely, ord n × ord m into ord (n×m)

Require Import Psatz PeanoNat Compare_dec Euclid.
Require Import ordinal.

Set Asymmetric Patterns.
Set Implicit Arguments.
Local Open Scope ltb_scope.

equivalence between our Boolean strict order on nat, and the standard one from the standard library
Lemma ltb_lt x y: ltb x y = true lt x y.
Proof.
revert y. induction x; destruct y; simpl.
split. discriminate. inversion 1.
split. lia. trivial.
split. discriminate. inversion 1.
rewrite IHx. lia.
Qed.

auxiliary lemma
Lemma mk_lt n m x y: x<n y<m y×n+x < n×m.
Proof. setoid_rewrite ltb_lt. nia. Qed.

since x is bounded by n, we encode the pair (x,y) as y×n+x
Definition mk n m (x: ord n) (y: ord m): ord (n×m).
destruct x as [x Hx]; destruct y as [y Hy].
apply Ord with (y×n+x).
now apply mk_lt.
Defined.

Lemma ord_nm_lt_O_n {n m} (x: ord (n×m)): lt 0 n.
Proof. destruct n. elim (ord_0_empty x). lia. Qed.

first projection, by modulo
Definition pi1 {n m} (p: ord (n×m)): ord n :=
let '(divex _ x Hx _) := eucl_dev n (ord_nm_lt_O_n p) p in (Ord x (proj2 (ltb_lt _ _) Hx)).

second projection, by division
Definition pi2 {n m} (p: ord (n×m)): ord m.
destruct (eucl_dev n (ord_nm_lt_O_n p) p) as [y x Hx Hy].
apply Ord with y.
unfold gt in ×.
destruct p as [p Hp]. simpl in Hy. rewrite Hy in Hp. clear p Hy.
destruct (le_lt_dec m y) as [Hy|Hy]. 2: now apply ltb_lt. exfalso.
apply ltb_lt in Hp. abstract nia.
Defined.

Lemma euclid_unique n: lt 0 n
x y x' y', lt x n lt x' n y×n+x = y'×n+x' y=y' x=x'.
Proof.
intros Hn x y x' y' Hx Hx' H. rewrite Nat.mul_comm, (Nat.mul_comm y') in H. split.
erewrite Nat.div_unique. 3: eassumption. 2: assumption.
rewrite H. eapply Nat.div_unique. 2: symmetry; eassumption. assumption.
erewrite Nat.mod_unique. 3: eassumption. 2: assumption.
rewrite H. eapply Nat.mod_unique. 2: symmetry; eassumption. assumption.
Qed.

projections behave as expected
Lemma pi1mk n m: x y, pi1 (@mk n m x y) = x.
Proof.
intros [x Hx] [y Hy]. unfold pi1, mk. case eucl_dev.
intros y' x' Hx' H. apply eq_ord. apply euclid_unique in H as [_ ?]; auto.
nia. now apply ltb_lt.
Qed.

Lemma pi2mk n m: x y, pi2 (@mk n m x y) = y.
Proof.
intros [x Hx] [y Hy]. unfold pi2, mk. case eucl_dev.
intros y' x' Hx' H. apply eq_ord. simpl. apply euclid_unique in H as [? _]; auto.
nia. now apply ltb_lt.
Qed.

surjective pairing
Lemma mkpi12 n m: p, @mk n m (pi1 p) (pi2 p) = p.
Proof.
intros [p Hp]. unfold pi1, pi2, mk. case eucl_dev. simpl. intros y x Hx Hy.
apply eq_ord. simpl. now rewrite Hy.
Qed.