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?

Mathias Fleury (May 03 2021 at 13:38):

like https://www.isa-afp.org/browser_info/current/AFP/Recursion-Theory-I/CPair.html?

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: Dec 21 2024 at 16:20 UTC