Email Gateway (Aug 18 2022 at 12:01): Email Gateway (Aug 18 2022 at 12:01):From: John Matthews <matthews@galois.com>
I'm having problems proving termination of the well-founded recursive
function xs_strm defined below, and other functions like it.
The termination measure is just less_than, and I've installed
appropriate congruence rules. However, the function package generates
an unprovable termination condition.
On the other hand, I have been able to manually prove the identical
function xs_strm2 below is well-founded by defining it in terms of
the wfrec combinator and manually applying the congruence rules. Below
are the definitions and lemmas needed to show the problem.
Thanks in advance,
-john
section "Auxiliary function and lemma"
text {*Coerces a finite prefix of an infinite stream (represented as a
@{typ "nat \<Rightarrow> 'a"} function) into a finite list. *}
definition
strm_to_list :: "nat \<Rightarrow> (nat \<Rightarrow> 'a)
\<Rightarrow> 'a list" where
"strm_to_list n f = map f [0..<n]"
lemma length_strm_to_list[simp]:
"length (strm_to_list n f) = n"
by (simp add: strm_to_list_def)
section {* Congruence rules for proving termination of @{term
"xs_strm"} below. *}
lemma nth_cons_cong[fundef_cong]:
"\<lbrakk>i = i';
i' = 0 \<Longrightarrow> x = x';
\<And>j. i = Suc j \<Longrightarrow> xs ! j = xs' ! j\<rbrakk>
\<Longrightarrow>
(x # xs) ! i = (x' # xs') ! i'"
by (cases i, auto)
lemma nth_out_of_bounds:
"length xs \<le> n \<Longrightarrow> xs ! n = [] ! (n - length xs)"
apply (induct xs arbitrary: n, auto simp add: nth_list_def)
by (case_tac n, auto)
lemma nth_take_cong[fundef_cong]:
assumes "i = i'"
and "n = n'"
and "i' < n' \<Longrightarrow> xs ! i' = xs' ! i'"
and "length xs = length xs'"
shows "(take n xs) ! i = (take n' xs') ! i'"
(is "?lhs = ?rhs")
using prems apply (cases "i' < n'", auto)
apply (subst nth_out_of_bounds, auto)
by (subst (2) nth_out_of_bounds, auto)
lemma nth_strm_to_list_cong[fundef_cong]:
"\<lbrakk>n = n';
i = i';
i < n \<Longrightarrow> f i' = f' i'\<rbrakk> \<Longrightarrow>
strm_to_list n f ! i = strm_to_list n' f' ! i'"
apply (simp add: strm_to_list_def)
apply (cases "i' < n'", auto)
apply (subst nth_out_of_bounds, auto)
by (subst (2) nth_out_of_bounds, auto)
section "An unsuccessful attempt to prove termination of the
well-founded function @{term xs_strm} below"
function
xs_strm :: "nat \<Rightarrow> nat" where
"xs_strm i
= (0 # take 2 (strm_to_list 3 xs_strm)) ! i"
by pat_completeness auto
termination
apply (relation less_than)
apply auto
-- "I am left with an unprovable termination condition"
oops
section "Manually applying congruence rules to prove termination of the
identical function @{term xs_strm2}"
definition
xs_strm2 :: "nat \<Rightarrow> nat" where
"xs_strm2 = wfrec less_than (\<lambda>R i. (0 # take 2
(strm_to_list 3 R)) ! i)"
lemma def_xs_strm2:
"xs_strm2 i = (0 # take 2 (strm_to_list 3 xs_strm2)) ! i"
(is "?lhs = ?rhs")
proof -
let "?H R i" = "((0::nat) # take 2 (strm_to_list 3 R)) ! i"
from wfrec[OF wf_less_than, where H="?H" and a=i] xs_strm2_def
have "?lhs = ?H (cut xs_strm2 less_than i) i" by simp
also have "\<dots> = ?rhs"
-- "Manually applying congruence rules here"
apply (subst nth_cons_cong, simp_all)
apply (subst nth_take_cong, simp_all)
apply (subst nth_strm_to_list_cong, simp_all)
by (simp add: cut_apply)
finally show ?thesis .
qed
Email Gateway (Aug 18 2022 at 12:01):From: Alexander Krauss <krauss@in.tum.de>
Hi John,
I'm having problems proving termination of the well-founded recursive
function xs_strm defined below, and other functions like it.
Good to see that you are driving all available tools to their limits and
beyond, as usual :-) But it might actually work...
The problem is that nth_take_cong has the premise about the lengths
being equal. In the function definition, a "recursive call" will be
generated by this premise because the instance occuring contains the
function being defined. But this simplifies away in your manual proof
because "length (strm_to_list n f)" does not depend on f.
So you need just one more cong rule to tell function about this:
lemma length_strm_to_list_cong[fundef_cong]:
"n = n' ==> length (strm_to_list n f) = length (strm_to_list n' f')"
by simp
Then it works.
Alex
Email Gateway (Aug 18 2022 at 12:02):From: John Matthews <matthews@galois.com>
Thanks Alex, that did the trick nicely. It seems to be holding up for
defining mutually-recursive lists as well.
-john
Last updated: May 03 2024 at 04:19 UTC