Email Gateway (Aug 22 2022 at 16:34): Email Gateway (Aug 22 2022 at 16:34):From: Dominique Unruh <unruh@ut.ee>
Hi,
unfortunately, it is nothing so simple as the presence of a ' in the
variable name.
For example, the following fails:
lemma "((0 ≤ pAx11 ∧ 0 ≤ pB11) ∧ 0 ≤ pAx10 ∧ 0 ≤ pB10) ∧ (0 ≤ pAx01 ∧ 0 ≤
pB01) ∧ 0 ≤ pAx00 ∧ 0 ≤ pB00 ⟹
(pAx10 + pAx11 = 1 ∧ pB10 + pB11 ≤ 1) ∧ pAx00 + pAx01 = 1 ∧ pB00 + pB01
≤ 1 ⟹
pAx01 * pB01 * 4 + pAx00 * pB00 * 4 + (pAx01 * pB11 * 4 + pAx00 * pB10
4) +
(pAx11 * pB01 * 4 + pAx10 * pB00 * 4 + (pAx11 * pB10 * 4 + pAx10 * pB11
4))
≤ (12::real) "
apply sos
(It's the same example but with ' replaced by x.)
And the following works:
lemma " (0 ≤ pA'01 ∧ 0 ≤ pB01) ⟹
pA'01 * pB01 * 4
≥ (0::real) "
apply sos
even though it contains a '
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 16:34):From: Lawrence Paulson <lp15@cam.ac.uk>
Well, let’s dig a little further. The exception you get indicates a mismatch between A ==> B and A in the rule implies_elim: the two copies of A are not identical. And indeed we have
(¬ (((0 ≤ pA'11 ∧ 0 ≤ pB11) ∧ 0 ≤ pA'10 ∧ 0 ≤ pB10) ∧ (0 ≤ pA'01 ∧ 0 ≤ pB01) ∧ 0 ≤ pA'00 ∧ 0 ≤ pB00 ⟶
(pA'10 + pA'11 = 1 ∧ pB10 + pB11 ≤ 1) ∧ pA'00 + pA'01 = 1 ∧ pB00 + pB01 ≤ 1 ⟶
pA'01 * pB01 * 4 + pA'00 * pB00 * 4 + (pA'01 * pB11 * 4 + pA'00 * pB10 * 4) +
(pA'11 * pB01 * 4 + pA'10 * pB00 * 4 + (pA'11 * pB10 * 4 + pA'10 * pB11 * 4))
≤ 12) ⟹
False)
on the one hand and
¬ (((0 ≤ pA'11 ∧ 0 ≤ pB11) ∧ 0 ≤ pA'10 ∧ 0 ≤ pB10) ∧ (0 ≤ pA'01 ∧ 0 ≤ pB01) ∧ 0 ≤ pA'00 ∧ 0 ≤ pB00 ⟶
(pA'10 + pA'11 = 1 ∧ pB10 + pB11 ≤ 1) ∧ pA'00 + pA'01 = 1 ∧ pB00 + pB01 ≤ 1 ⟶
pA'01 * pB01 * 4 + pA'00 * pB00 * 4 + (pA'01 * pB11 * 4 + pA'00 * pB10 * 4) +
(pA'11 * pB01 * 4 + pA'10 * pB00 * 4 + (pA'11 * pB10 * 4 + pA'10 * pB11 * 4))
≤ 12) ⟹
0 < 4 * (pA'01 * pB00) +
(- 4 * (pA'01 * pB01) +
(4 * (pA'01 * pB10) +
(- 4 * (pA'01 * pB11) +
(4 * (pA'11 * pB00) +
(- 4 * (pA'11 * pB01) +
(- 4 * (pA'11 * pB10) +
(4 * (pA'11 * pB11) +
(- 4 * (pB00 * pA'01) +
(- 4 * (pB00 * pA'11) +
(4 * (pB01 * pA'01) +
(4 * (pB01 * pA'11) +
(- 4 * (pB10 * pA'01) + (4 * (pB10 * pA'11) + (4 * (pB11 * pA'01) + - 4 * (pB11 * pA'11)))))))))))))))
on the other. It also seems that the expression 4 * (pA'01 * pB00) + (- 4 * (pA'01 * pB01) + …) simplifies to 0 if we invoke the single method (simp add: mult.commute). And therefore
0 < 4 * (pA'01 * pB00) + (- 4 * (pA'01 * pB01) + …)
simplifies to False, as required.
Is there anybody out there who understands this code?
Larry Paulson
Email Gateway (Aug 22 2022 at 16:34):From: Tobias Nipkow <nipkow@in.tum.de>
Yes, thanks for reporting it. The implementor is still around but is doing very
different things for his PhD now. I doubt I can get him to look into it....
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 16:34):From: Dominique Unruh <unruh@ut.ee>
Hi,
[this is tl;dr for most, I guess. But Tobias Nipkow, please have a look at
the last two lines before the signature]
I tried some more to figure out what goes wrong, but I am giving up now.
However, I figured out some things that might be useful for whoever tries
next:
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.
The bug can be traced down to the following internal call:
ML {*
val ctxt = @{context}
val t = @{cterm "0 ≤ c ∧ 0 ≤ a ⟶ a + bb = 1 ∧ c ≤ 1 ⟶ bb * c * 4 ≤
(12::real)"};;
val t' = @{cterm "0 ≤ c ∧ 0 ≤ a ⟶ a + b = 1 ∧ c ≤ 1 ⟶ b * c * 4 ≤
(12::real)"};; (* A good term where the error does not occur *)
val prover = (Sum_of_Squares.Prover (SOS_Wrapper.run_solver ctxt));;
*}
ML {*
Sum_of_Squares.real_sos prover ctxt t
*}
(real_sos is not exported by Sum_of_Squares, nor is run_solver by
SOS_Wrapper, you need to add them to the exported vals for this example to
work.)
This, in turn, calls the following where the error occurs:
ML {*
RealArith.gen_prover_real_arith ctxt
(Sum_of_Squares.real_nonlinear_subst_prover prover ctxt) t
*}
And in this one, we can track down the bug some more:
The value th2, defined by "val (th2, certs) = overall [] [] [specl avs
(Thm.assume (Thm.rhs_of th1))]" is "False" when using the "good" t'.
But it is "0 < - 1 * (bb * c) + c * bb" otherwise.
In turn, overall performs a call to "prover (rev cert_choice)
hol_of_positivstellensatz (eq,le,lt)" which is the call that returns the
thm used in th2.
(Note: prover is the value prover defined in the ML snippet above)
And the (single) call to hol_of_positivstellensatz performed by prover
returns the value that is later used for th2.
So the bug could be either in hol_of_positivstellensatz (part of
positivestellensatz.ML by Amine Chaieb), or of sos (by Philipp Meyer and
Amine Chaieb).
To decide that, one would need better understand of the code (or just more
time for debugging).
Tobias: which of the two is the one whom you doubt you could raise?
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 16:36):From: Makarius <makarius@sketis.net>
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
ch-sos_term_ord
Email Gateway (Aug 22 2022 at 16:36):From: Dominique Unruh <unruh@ut.ee>
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:
Email Gateway (Aug 22 2022 at 16:37):From: Dominique Unruh <unruh@ut.ee>
Hello,
please let me know if there is a better place to report bugs.
I noticed the following problem with the method "sos": There a goal one
which sos works fine gives an error when using other variable names (but
everything else being the same).
An example theory is attached.
The second proof raises a THM exception on my computer (Linux,
Isabelle-2017).
Another (minor) issue is: In sos_wrapper.ML, the function get_result does
not define a message for return code 10 which is "Program stopped by signal
(SIXCPU, SIGTERM, etc.)" according to
https://projects.coin-or.org/Csdp/raw-attachment/wiki/WikiStart/csdpuser.pdf.
(Although this error message is slightly confusing, too, when it happens
with a long-running sos-call.)
Best wishes,
Dominique.
Bug.thy
Email Gateway (Aug 22 2022 at 16:37):From: Lawrence Paulson <lp15@cam.ac.uk>
Dear Dominique, thanks for your message. So the problem is that variables with names like pA’11 break the sos method?
The implementers of this proof method are long gone, but it’s a good bet that the faulty code is here:
(* map polynomials to strings *)
fun string_of_varpow x k =
let
val term = Thm.term_of x
val name =
(case term of
Free (n, _) => n
| _ => error "Term in monomial not free variable")
in
if k = 1 then name else name ^ "^" ^ string_of_int k
end
(In HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML.)
No doubt we have a function to deal with identifiers that contain strange characters. Does anybody have a suggestion?
Larry Paulson
Email Gateway (Aug 22 2022 at 16:42):From: Tobias Nipkow <nipkow@in.tum.de>
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
smime.p7s
Email Gateway (Aug 22 2022 at 16:44):From: Makarius <makarius@sketis.net>
The Isabelle/ML library provides various ways to order terms, and some
other more basic data types like string and indexname.
Working with the Simplifier (or related conversions) usually requires an
ordering that conforms to its policies, notably Term_Ord.term_ord /
termless (sometimes Term_Ord.term_lpo).
Working with auxiliary set/map data structures that need to be fast is
usually done with fast_string_ord, fast_indexname_ord, fast_term_ord
etc. There is no semantic intention behind these orderings, and they can
actually look strange when used for printing a table: the output needs
to be sorted by a more natural order.
With this in mind an educated guess says: FuncUtil tables are right in
using fast_term_ord derivatives and sum_of_squares.ML was wrong using
fast_term_ord with Semiring_Normalizer. This is further supported by the
empiric exploration of Isabelle + AFP: the change c46910a6bfce was
sufficient to make the counter examples work and did not break existing
applications.
There is additional confusion in this code base due to preference of
cterm over term: it might be a consequence of porting tools from
HOL-Light, which only has cterm (and calls it term). There are also a
bit too many clones of operations, with non-canonical name and signature
(like simple_cterm_ord, which corresponds to Term_Ord.termless).
Makarius
Last updated: Apr 26 2024 at 16:20 UTC