Bijections between nat and nat * nat

Using Coq
1

The pairing function [1] is a way to implement bijections between nat and nat * nat. However, for the bijectivity proofs one requires facts about division, square roots, and floor function (which are tricky in Coq).

What is the most elegant Coq approach to write

  • a function encode: nat * nat -> nat
  • a function decode: nat -> nat * nat
  • a lemma forall z, decode (encode z) = z
  • a lemma forall n, encode (decode n) = n

possibly using lia or nia for automation?

[1] https://en.wikipedia.org/wiki/Pairing_function

1 Like
2

Here’s (lines 113 to 244) an example of a proof of bijectivity of Cantor’s pairing function that I proved a while ago.

1 Like
3

I find the coding 2^n * (2 * m + 1) - 1 often easier to manipulate.
It is used in ollibs but not exactly with the specification you ask. It is there proved to be both injective and surjective but the decoding function is hidden in cpair_surj.

4

I have updated ollibs in which the first 100 lines should now be what you want.
The only difference is that it uses a triple of functions (because I mostly focus on encoding in my developments):

  • a function pcpair: nat -> nat -> nat
  • a function pdpair1: nat -> nat
  • a function pdpair2: nat -> nat
  • a lemma forall n m, pdpair1 (pcpair n m) = n
  • a lemma forall n m, pdpair2 (pcpair n m) = m
  • a lemma forall p, pcpair (pdpair1 p) (pdpair2 p) = p

In order to avoid the dependecy over funtheory, simply inline:

Definition injective2 {A B C} (f : A -> B -> C) :=
  forall x y x' y', f x y = f x' y' -> x = x' /\ y = y'.
Definition surjective2 {A B C} (f : A -> B -> C) :=
  forall z, {'(x,y) | z = f x y }.