Email Gateway (Aug 18 2022 at 14:04): Email Gateway (Aug 18 2022 at 14:04):From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
Hi all,
the induction rules that the function package generates for a function
definitions are usually great. However, is always quantifies over all
parameters of the function, even if they are just passed through all
recursive calls. For some proofs, I would like not to have them
quantified. Is there an option to the function package to declare such
parameters to treat differently (like the for clause for inductive)?
A concrete example:
fun map where
"map f [] = []"
| "map f (x # xs) = f x # map f xs"
produces the induction rule map.induct:
[| !!f. P f []; !!f x xs. P f xs ==> P f (x # xs) |] ==> P a0 a1
but I would much more like the following rule (which I currently derive
by hand from the generated one):
[| P []; !!x xs. P xs ==> P (x # xs) |] ==> P a
Thanks,
Andreas
Email Gateway (Aug 18 2022 at 14:04):From: Alexander Krauss <krauss@in.tum.de>
Hi Andreas,
Currently, there is no such option. In fact, a for-clause would not
solve the problem completely, since even if an argument arguments does
change in recursive calls, one would sometime like to see it
eliminated from the induction rule.
In suce a case, I usually project away the extra arguments manually
(using something like [where P="%x y. Q y", standard]), which is not
nice but works.
Cheers,
Alex
Email Gateway (Aug 18 2022 at 14:05):From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
Hi Alex,
the induction rules that the function package generates for a function
definitions are usually great. However, is always quantifies over all
parameters of the function, even if they are just passed through all
recursive calls. For some proofs, I would like not to have them
quantified. Is there an option to the function package to declare such
parameters to treat differently (like the for clause for inductive)?Currently, there is no such option. In fact, a for-clause would not
solve the problem completely, since even if an argument arguments does
change in recursive calls, one would sometime like to see it eliminated
from the induction rule.
That is right, but a for clause would also help in proving compatibility
for overlapping patterns, because already the function graph definition
could use the for clause. Then, reasoning on the graph becomes easier
and the termination proof as well, because one would not need to code
the functional dependency on the fixed parameters into the relation.
In suce a case, I usually project away the extra arguments manually
(using something like [where P="%x y. Q y", standard]), which is not
nice but works.
I also use that trick to derive my own induction rules. However, this
does not work, if one of the fixed parameters is used in some guard to
the recursive call. Here is a concrete example:
datatype 'a array = Array "'a list"
primrec array_length :: "'a array => nat"
where "array_length (Array a) = length a"
function assoc_list_of_array_code :: "'a array => nat => (nat * 'a) list"
where
"assoc_list_of_array_code a n =
(if array_length a < n then []
else ... # assoc_list_of_array_code a (n + 1))"
by pat_completeness auto
termination assoc_list_of_array_code
by(relation "measure (%p. array_length (fst p) - snd p)") auto
My desired induction rule is:
(!!n. (n < array_length a ==> P (n + 1)) ==> P n) ==> P n
I obtain it by instantiating P in assoc_list_of_array_code.induct to
"%a' n. a = a' --> P n" and doing some more manipulations.
If you have some time somewhen you might consider such a for clause as a
feature request. Here is what I think would be a nice definition:
function assoc_list_of_array_code :: "'a array => nat => (nat * 'a) list"
for a :: "'a array
where
"assoc_list_of_array_code a n =
(if array_length a < n then []
else ... # assoc_list_of_array_code a (n + 1))"
by pat_completeness auto
termination assoc_list_of_array_code
by(relation "%a. measure (%n. array_length a - n)") auto
Anyway, I will have a look at your induct_scheme method.
Cheers,
Andreas
Email Gateway (Aug 18 2022 at 14:05):From: Alexander Krauss <krauss@in.tum.de>
Andreas Lochbihler wrote:
Looks reasonable. I'll think about it.
Cheers,
Alex
Last updated: Nov 21 2024 at 12:39 UTC