*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Method sos fails depending on variable names*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 1 Feb 2018 07:30:59 +0100*In-reply-to*: <CAPFfTE4uoEL=xd2u8YEsHo47PivkMBwHX9c1k85oXOWctVwpgg@mail.gmail.com>*References*: <CAPFfTE4a3wPzaM71YMVU5E7wK=HQzsmSrQ=4TjENAc_TWM_0Vg@mail.gmail.com> <0B0D3D89-8C30-46AE-86D4-26814825549A@cam.ac.uk> <CAPFfTE7HxW9KzXHdW00OLH5DVEU+mTUo0+Xz6wCavFJkA6mekg@mail.gmail.com> <E27D0E09-3ECF-4F4B-9455-9944FB100DD2@cam.ac.uk> <CAPFfTE6+iLpE-B9AXp6EEhoKvp5DJJMtThgBnXyn2RL0715OJw@mail.gmail.com> <78fd5147-46f6-85e9-9dcf-861b56f1eff9@sketis.net> <CAPFfTE4uoEL=xd2u8YEsHo47PivkMBwHX9c1k85oXOWctVwpgg@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:52.0) Gecko/20100101 Thunderbird/52.5.2

Tobias On 01/02/2018 00:32, Dominique Unruh wrote:

Hi, oups, it seems that the discussion with Tobias and Larry went off the mailing list. I did exactly the same as you (including learning how to use the debugger :) ), a pity about the duplicated effort... Sorry for that. For what it's worth, here is the analysis I wrote to Tobias and Larry some weeks ago:As supposed, there is a mismatch in term orderings, one sorting first by string length, the other lexicographically. Looking at term_ord.ML, the first would be fast_term_ord, and the second term_ord. With that information, we simply look for occurrences of those. In positivstellensatz.ML, we have the line: fun simple_cterm_ord t u = Term_Ord.term_ord (Thm.term_of t, Thm.term_of u) = LESS and in sum_of_squares.ML, we have fun simple_cterm_ord t u = Term_Ord.fast_term_ord (Thm.term_of t, Thm.term_of u) = LESS (twice). If we change fast_term_ord into term_ord here, the bug disappears. Of course, without understanding the code, we cannot be sure that this is exactly what's needed. In particular, there are also calls to FuncUtil.cterm_ord (which internally uses fast_term_ord). Should they be replaced, too? It does not seem to make a difference for my test case, but who knows. In any case, I think replacing fast_term_ord in the two places is better than the status quo.Best wishes, Dominique. On 31 January 2018 at 22:41, Makarius <makarius at sketis.net> wrote:On 11/01/18 15:51, Dominique Unruh wrote:A much smaller example of the bug is: lemma shows "0 â c â 0 â a â a + bb = 1 â c â 1 â bb * c * 4 â (12::real) " apply sos If we replace bb -> b, or c -> cc, the error vanishes. So it seemscrucialthat bb is longer than c. Perhaps it has to do something with some term ordering applied somewhere.Thanks for this concise example. I've spent 2h with it in our fancy Isabelle/ML debugger IDE, but actually found the problem by looking carefully at the sources in the old-fashioned manner: HOL/Library/positivstellensatz.ML and HOL/Library/positivstellensatz.ML use different term orderings for normalization. This is amended in the included changeset for Isabelle2017. In the Isabelle repository it is now c46910a6bfce. Makarius

**Attachment:
smime.p7s**

- Previous by Date: Re: [isabelle] Timing information from isabelle build
- Next by Date: Re: [isabelle] Method sos fails depending on variable names
- Previous by Thread: [isabelle] 25th Automated Reasoning Workshop (ARW 2018), University of Cambridge, 12-13 April 2018
- Next by Thread: Re: [isabelle] Method sos fails depending on variable names
- Cl-isabelle-users February 2018 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list