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



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.