Re: [isabelle] Setup termination prover for finitely branching tree recursion



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

On 07/12/15 10:14, Manuel Eberl wrote:
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


On 07/12/15 09:08, Andreas Lochbihler wrote:
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.

1. âts' xa. size (ts' xa) < Suc (âxâUNIV. size (ts' x))


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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.