Library Coq.Arith.Cantor


Implementation of the Cantor pairing and its inverse function

Require Import PeanoNat Lia.

Bijections between nat * nat and nat
Cantor pairing to_nat

Definition to_nat '(x, y) : nat :=
  y + (nat_rec _ 0 (fun i m => (S i) + m) (y + x)).

Cantor pairing inverse of_nat

Definition of_nat (n : nat) : nat * nat :=
  nat_rec _ (0, 0) (fun _ '(x, y) =>
    match x with | S x => (x, S y) | _ => (S y, 0) end) n.

of_nat is the left inverse for to_nat

Lemma cancel_of_to p : of_nat (to_nat p) = p.

to_nat is injective

Corollary to_nat_inj p q : to_nat p = to_nat q -> p = q.

to_nat is the left inverse for of_nat

Lemma cancel_to_of n : to_nat (of_nat n) = n.

of_nat is injective

Corollary of_nat_inj n m : of_nat n = of_nat m -> n = m.

Polynomial specifications of to_nat

Lemma to_nat_spec x y :
  to_nat (x, y) * 2 = y * 2 + (y + x) * S (y + x).

Lemma to_nat_spec2 x y :
  to_nat (x, y) = y + (y + x) * S (y + x) / 2.

to_nat is non-decreasing in (the sum of) pair components

Lemma to_nat_non_decreasing x y : y + x <= to_nat (x, y).