I need an injective function from
(int * int) => int, e.g. Cantor's pairing function. Where is this formalised?
No need to turn to the AFP. You can use
HOL-Library.Nat_Bijection. This is also used to prove the countability of products in
Thanks Manuel, I was hoping for something like that :D
Unrelatedly, my favourite pairing function at least for theoretical purposes is . 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.
For my application, the function does not have to be economic.
Yes but still, it's easier to take the one that's already in the library.
I just like telling people about the one above because it's neat and few people seem to know about it.
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:
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))).
I tried a bit and only managed to prove it by taking annoyingly small steps
*prove parts of it (until now)
Write it with as a composition of bijective functions with
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)
Last updated: Sep 25 2021 at 09:17 UTC