Simplifier - term ordering · General

Hey,
I'm currently trying to write a small tactic that normalizes "cost-expressions" and is capable of solving inequality side-conditions of the following form, or at least reducing it to goals on natural numbers:

cost ''ll_call'' 3 + cost ''ll_sub'' (3*n+1) + cost ''ll_call'' (n*n)
        <= cost ''ll_call'' (n*n+10) + cost ''ll_add'' 4 + cost ''ll_sub'' (10*n+3)
<--
3+n*n<=n*n+10 /\ 3*n+1 <= 10*n+3

One way I came up with is to use the simplifier with @{thms add_ac} and get the right term ordering, such that terms are sorted by the first argument of cost, then condensed, and finally reduce to inequalities on natural numbers.
I found Pure/term_ord.ML and Simplifier.set_term_ord. It seems that Term_Ord.term_ord is the default, and it uses the size of the term first for comparison.

At some point I got annoyed and solved the whole thing ad-hoc with another approach: a prolog-style method that iterates through the sums left and right of the inequality and extracts the inequalities on natural numbers.

Whats the right way to do this. I guess it occurs in several places, and the above is only an ad-hoc solution. I found @Manuel Eberl's Group_Sort is it somehow related? Did you encounter similar issues and how did you solve it?

Manuel Eberl (Jun 17 2020 at 09:58):

Oh god, how did you even find this abomination? You could probably use `Group_Sort', but it's fairly ad-hoc itself.

It's a fairly annoying problem. You can either solve it by introducing a lot of tags and simplifier setup (a bit like the Group Sort thing) to rearrange the left-hand sides and right-hand sides, or you could do it with a conversion in ML. I'm not really sure which solution is nicer.

I've encountered the problem ‘you have a sum/product/whatever of terms, now rearrange it in some way’ (e.g. pull out a particular term) occasionally, and I've used both of the above approaches to solve it. Neither of them were pretty. I think nowadays I tend to go for the ML conversion approach more because I'm more comfortable writing these than I was in the past and it is more flexible, more direct, more robust, and faster.

Stream: General

Topic: Simplifier - term ordering

maximilian p.l. haslbeck (Jun 16 2020 at 16:08):

Manuel Eberl (Jun 17 2020 at 09:58):

maximilian p.l. haslbeck (Jun 17 2020 at 10:00):

maximilian p.l. haslbeck (Jun 17 2020 at 10:01):