Email Gateway (Aug 22 2022 at 11:59): Email Gateway (Aug 22 2022 at 11:59):From: Manuel Eberl <eberlm@in.tum.de>
No idea about why what you are doing does not work, but the following
does work:
lemma le_setsum_nat [termination_simp]:
assumes "finite A" "x ∈ A"
shows "f (g x) ≤ (∑x∈A. f (g x) :: nat)"
proof -
have "f (g x) = (∑x∈{x}. f (g x))" by simp
also from assms have "… ≤ (∑x∈A. f (g x))" by (intro setsum_mono2) auto
finally show ?thesis by simp
qed
Note that it doesn't work if you replace "f (g x)" with just "f x".
Unification problem, perhaps?
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 11:59):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Manuel,
Thanks for the suggestion, your rule does suffice to prove the termination of my given
example. It differs from the existing estimation rules in that the left hand side of the
conclusion must be exactly of the summation form. The existing rules encode a transitivity
step
"[| y <= f (g x); f (g x) <= (∑x∈A. f (g x)) |] ==> y <= (∑x∈A. f (g x))"
and this is what introduces the schematic variable ?x in the assumptions which cause all
the trouble. And in general, this transitivity step is indeed needed (and your rule fails
there). For example, if the recursion in the datatype goes through another type.
datatype (plugins del: size) 'a tree2 = Leaf2 | Node2 'a "char ⇒ 'a tree2 × 'a"
instantiation tree2 :: (type) size begin
primrec size_tree2 :: "'a tree2 ⇒ nat"
where
"size_tree2 Leaf2 = 0"
| "size_tree2 (Node2 x ts) =
Suc (setsum (Suc ∘ fst ∘ (map_prod size_tree2 id ∘ ts)) UNIV)"
instance ..
end
fun zip_prod where "zip_prod f g (x, y) (u, v) = (f x u, g y v)"
fun zip_tree2 :: "'a tree2 ⇒ 'b tree2 ⇒ ('a × 'b) tree2"
where
"zip_tree2 (Node2 x ts) (Node2 y ts') =
Node2 (x, y) (λz. zip_prod zip_tree2 Pair (ts z) (ts' z))"
| "zip_tree2 _ _ = Leaf2"
Do you think one can generalise your rule in a way such that it still works with
lexicographic_order?
Best,
Andreas
Email Gateway (Aug 22 2022 at 12:07):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear experts of the simplifier and/or the function package,
For a datatype of finitely branching trees, I would like to setup the terminiation prover
of the function package such that it can automatically prove termination of my recursive
functions. My problem is that I cannot mimick the setup for other datatypes like lists and
I am running out of ideas how this can be fit into lexicographic order.
Here is my usecase and the analysis of the problem. The datatype tree recurses through the
function type, but the domain of the functions is finite. Thus, it is possible to define a
size function, although this must be done manually in Isabelle2015 (using setsum for
summing the sizes of the subtrees).
datatype (plugins del: size) 'a tree = Leaf | Node 'a "char ⇒ 'a tree"
instantiation tree :: (type) size begin
primrec size_tree :: "'a tree ⇒ nat" where
"size_tree Leaf = 0"
| "size_tree (Node x ts) = Suc (setsum (size_tree ∘ ts) UNIV)"
instance ..
end
Now, I would like lexicographic_order to prove termination of a function definition such
as the following:
fun zip_tree :: "'a tree ⇒ 'b tree ⇒ ('a × 'b) tree"
where
"zip_tree (Node x ts) (Node y ts') = Node (x, y) (λz. zip_tree (ts z) (ts' z))"
| "zip_tree _ _ = Leaf"
Without further setup, the termination proof fails because the proof tactic cannot solve
goals such as the following.
For recursion through lists, there is a custom setup, namely the theorems
size_list_estimation and size_list_estimation' which are declared as [termination_simp].
thm size_list_estimation' ⟦?x ∈ set ?xs; ?y ≤ ?f ?x⟧ ⟹ ?y ≤ size_list ?f ?xs
Now I tried to mimick this setup for the setsum operator:
lemma setsum_estimation'[termination_simp]:
"(y :: nat) ≤ f x ⟹ finite (UNIV :: 'a set) ⟹ y ≤ setsum f (UNIV :: 'a set)"
From what I could see from the code, these *_estimation rules work as follows:
lexicographic_order internally uses the proof method (auto simp add: termination_simp)
to solve the goals, that is, the termination proof are solved mostly by conditional rewriting.
In particular, termination_simp contains the rule ?m ≤ ?n ⟹ ?m < Suc ?n, so the above
subgoal 1. can be solved if the simplifier can prove "size (ts' xa) <= (∑x∈UNIV. size (ts'
x))". And this is where *_estimation' triggers.
Unfortunately, the simplifier does not like setsum_estimation' as much as it likes
size_list_estimation'. Both rules contain the free variable ?x in the assumptions that is
not bound by the conclusion, so trouble is to be expected.
In the case of size_list_estimation', the first premise ?x : set ?xs instantiates the ?x
because the termination goal typically contains an assumption x : set xs due to a
congrence rule (and the simplifier calls the HOL unsafe solver, which instantiates the
variable as a matching assumption is available). Thus, the second assumption ?y <= ?f ?x
no longer contains schematic variables and the simplifier can usually discharge the goal.
In case of setsum_estimation', there is no such first premise that could instantiate ?x
(because the corresponding assumption would be "?x : UNIV" which holds trivially). Thus,
the recursive invocation of the simplifier is left with a goal such as
"!!x. f x <= f (?x x)"
Simplification fails (because there is no suitable solver) and thus it cannot prove
termination.
If I add a solver to the simpset which applies the rule "order_refl", then the termination
proof succeeds. Yet, my feeling says that such a solver is not a good idea in general,
because it will instantiate variables too aggressively. So this looks like a hack that is
better avoided.
Are there ideas for a better size function or a better setup for termination_simp? Has
anyone else run into this problem before?
Best,
Andreas
Last updated: Apr 25 2024 at 16:19 UTC