I need an injective function from (int * int) => int
, e.g. Cantor's pairing function. Where is this formalised?
like https://www.isa-afp.org/browser_info/current/AFP/Recursion-Theory-I/CPair.html?
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
.
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 ∘
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)
Thanks!
Last updated: Nov 11 2024 at 01:24 UTC