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

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

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`

.

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 }.
```