Email Gateway (Aug 19 2022 at 10:29): Email Gateway (Aug 19 2022 at 10:29):From: Tjark Weber <webertj@in.tum.de>
Hi,
Consider this (simplified) example of a recursive function whose
definition involves set comprehension:
function (sequential) f :: "nat ⇒ nat" where
"f 0 = 1"
| "f n = ∑{f k | k. k < n}"
by pat_completeness auto
How to prove termination? In particular,
termination f
apply (relation "measure id")
results in an unprovable goal.
Best regards,
Tjark
Email Gateway (Aug 19 2022 at 10:29):From: Johannes Hölzl <hoelzl@in.tum.de>
Hi Tjark and Lars,
You need a congruence rule not for setsum but for {f k | k. k< n} which
is conjunction. A simple solution is to rewrite the rule with the image
operator, it already has the correct fundef-cong rule installed:
function (sequential) f :: "nat ⇒ nat" where
"f 0 = 1"
| "f n = ∑(f ` {..< n})"
by pat_completeness auto
termination by lexicographic_order
With
declare rev_conj_cong[fundef_cong]
your version also works.
Email Gateway (Aug 19 2022 at 10:29):From: Tjark Weber <webertj@in.tum.de>
Indeed it does. Many thanks!
Best regards,
Tjark
Last updated: Apr 25 2024 at 20:15 UTC