Email Gateway (Jan 09 2021 at 15:21): Email Gateway (Jan 09 2021 at 15:21):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
This is not necessarily new behavior to Isabelle2021-RC1, but I just observed a reason that
explains why it occurs, and might lead someone to be able to fix it.
Not infrequently, sledgehammer will report "Try this: using X Y Z ... by presburger", but when you
actually insert this, the proof fails. In the past, I have observed that the result can often be
salvaged by using "metis" in place of "presburger" (though for the cases where this arises, which
do not actually involve Presburger arithmetic, presburger can often be much, much faster than other
methods).
Today I just noticed that whether or not presburger succeeds can sometimes be sensitive to the
ordering of the assumptions in the "using" clause that precedes "by presburger". I confirmed that,
in at least one instance where the "using X Y Z ... by presburger" did not succeed, that it
did succeed when the assumptions were permuted. More specifically, I applied sledgehammer to
something of the form:
using A B C ...
I received the suggestion "using X Y Z ... by presburger", but "using A B C ... X Y Z ... by presburger"
did not succeed. However after permuting "A B C ... X Y Z ..." appropriately, presburger did succeed.
I don't know if proof methods are permitted to be sensitive to the order of assumptions in the context.
I would think that this would not be desirable. In any case, it seems that one class of failures of
"by presburger" suggestions returned by sledgehammer are due to presburger having such a sensitivity.
Last updated: Jul 15 2022 at 23:21 UTC