Email Gateway (Aug 19 2022 at 13:50): Email Gateway (Aug 19 2022 at 13:50):From: Markus Schmetkamp <m.schmetkamp@gmx.de>
Hi people,
I want to prove this lemma:
lemma bijection: "?f::(nat × nat => nat). bij f"
My idea was to define a function like this:
fun f :: "nat × nat => nat" where
"f (0,0) = 0" |
"f (n, Suc m) = Suc (f (Suc n, m))" |
"f (Suc n, 0) = Suc (f (0, n))"
This function should go along each diagonal in nat x nat counting the
tuples.
Unfortunately isabelle can't find a termination order.
Has anyone an idea, to prove this lemma?
Best wishes
Markus
Email Gateway (Aug 19 2022 at 13:50):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I will not prove the entire lemma for you, but I can tell you how to
prove the termination of your function.
Your function requires a non-trivial termination relation, one that
Isabelle's function package cannot find automatically. I suggest a
lexicographic ordering w.r.t. the sum of the two arguments and the
second argument, i.e. in every recursive call, either the sum of the
argument decreases or it stays the same and the second element decreases.
In Isabelle, that can be done like this:
function f :: "nat × nat => nat" where
"f (0,0) = 0" |
"f (n, Suc m) = Suc (f (Suc n, m))" |
"f (Suc n, 0) = Suc (f (0, n))"
by pat_completeness simp_all
termination by (relation "(λ(a,b). a+b) <mlex> measure snd")
(auto intro: wf_mlex mlex_less mlex_leq)
“measure”is a function that takes a measuring function (i.e. 'a => nat)
and turns it into the associated strict ordering relation. <mlex> is
an operator that takes a relation and combines it with another measure
to a new lexicographic ordering relation.
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 13:50):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
You might save some effort by using looking at ~~/src/HOL/Library/Nat_Bijection. It
defines a suitable function prod_encode and proves that it is bijection in lemma
bij_prod_encode.
Andreas
Last updated: Apr 19 2024 at 08:19 UTC