## Stream: Beginner Questions

### Topic: Cantor's pairing function

#### Lukas Stevens (May 03 2021 at 13:33):

I need an injective function from (int * int) => int, e.g. Cantor's pairing function. Where is this formalised?

#### Manuel Eberl (May 03 2021 at 13:43):

No need to turn to the AFP. You can use prod_encode/prod_decode from HOL-Library.Nat_Bijection. This is also used to prove the countability of products in HOL-Library.Countable.

#### Lukas Stevens (May 03 2021 at 13:44):

Thanks Manuel, I was hoping for something like that :D

#### Manuel Eberl (May 03 2021 at 13:45):

Unrelatedly, my favourite pairing function at least for theoretical purposes is $(a,b) \mapsto 2^a \cdot (2b+1)$. It's much easier to see why this is bijective, and it's very easy to invert as well. The drawback is that it is not as economic as the other one.

#### Lukas Stevens (May 03 2021 at 13:47):

For my application, the function does not have to be economic.

#### Manuel Eberl (May 03 2021 at 13:50):

Yes but still, it's easier to take the one that's already in the library.

#### Manuel Eberl (May 03 2021 at 13:51):

I just like telling people about the one above because it's neat and few people seem to know about it.

#### Manuel Eberl (May 03 2021 at 13:52):

By the way, if you're wondering how I found prod_encode: I knew about HOL-Library.Countable_Set and figured there has to be a pairing function in there somewhere, and I was right. :smile:

#### Lukas Stevens (May 03 2021 at 13:59):

Related question: are there any helpers for proving that combining bijective functions again yield a bijective function? Specifically, I am looking at the function (λ(a, b). int_decode (prod_encode (int_encode a, int_encode b))).

#### Lukas Stevens (May 03 2021 at 14:00):

I tried a bit and only managed to prove it by taking annoyingly small steps

#### Lukas Stevens (May 03 2021 at 14:04):

*prove parts of it (until now)

#### Manuel Eberl (May 03 2021 at 14:05):

Write it with as a composition of bijective functions with ∘ and map_prod:

lemma map_prod_bij:
assumes "bij f" "bij g"
shows   "bij (map_prod f g)"
using assms unfolding bij_def by (intro conjI prod.inj_map map_prod_surj) auto

lemma "(λ(a, b). int_decode (prod_encode (int_encode a, int_encode b))) =
int_decode ∘ prod_encode ∘ map_prod int_encode int_encode"
by auto

lemma "bij (int_decode ∘ prod_encode ∘ map_prod int_encode int_encode)"
by (intro map_prod_bij bij_comp bij_int_encode bij_prod_encode bij_int_decode)


#### Lukas Stevens (May 03 2021 at 14:10):

Thanks!

Last updated: Sep 25 2021 at 09:17 UTC