Re: [isabelle] Method sos fails depending on variable names



This is my fault. I had promised to make the change that Dominique proposed but had planned to do it after the end of term. Sorry about that.

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 seems
crucial
that 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
Description: S/MIME Cryptographic Signature



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