# denum: retracting various countable types into positives

Require Import common positives ordinal.
Set Implicit Arguments.

# Sums

Definition mk_sum (x: positive+positive) :=
match x with
| inl pxO p
| inr pxI p
end.
Definition get_sum x :=
match x with
| xO pinl p
| xI pinr p
| _assert_false (inl xH)
end.
Lemma get_mk_sum x: get_sum (mk_sum x) = x.
Proof. now destruct x. Qed.

# Pairs

Fixpoint xpair y x :=
match x with
| xHxI (xO y)
| xO xxO (xO (xpair y x))
| xI xxI (xI (xpair y x))
end.
Definition mk_pair (x: positive×positive) := xpair (snd x) (fst x).
Fixpoint get_pair x :=
match x with
| xI (xO p) ⇒ (xH,p)
| xO (xO x) ⇒ let '(x,y) := get_pair x in (xO x,y)
| xI (xI x) ⇒ let '(x,y) := get_pair x in (xI x,y)
| _assert_false (xH,xH)
end.
Lemma get_mk_pair x: get_pair (mk_pair x) = x.
Proof.
destruct x as [x y]. unfold mk_pair. simpl.
induction x; simpl; now rewrite ?IHx.
Qed.

# Natural numbers

we use a much simpler function than the standard bijection, since we only need a retract
Definition mk_nat := nat_rec (fun _positive) xH (fun _xO).
Fixpoint get_nat x :=
match x with
| xHO
| xO xS (get_nat x)
| _assert_false O
end.
Lemma get_mk_nat x: get_nat (mk_nat x) = x.
Proof. induction x; simpl; now rewrite ?IHx. Qed.

# Ordinals

Definition mk_ord n (x: ord n) := mk_nat x.
get_ord returns an option since n could be 0, this is not problematic in practice
Definition get_ord n (x: positive): option (ord n).
set (y:=get_nat x). case (lt_ge_dec y n).
intro Hy. exact (Some (Ord y Hy)).
intros _. exact None.
Defined.
Lemma get_mk_ord n x: get_ord n (mk_ord x) = Some x.
Proof.
unfold mk_ord, get_ord. destruct x as [i Hi]; simpl.
rewrite get_mk_nat. case lt_ge_dec.
intro. f_equal. now apply eq_ord.
rewrite Hi at 1. discriminate.
Qed.