Email Gateway (Aug 22 2022 at 13:58): Email Gateway (Aug 22 2022 at 13:58):From: Lukas Bulwahn <lukas.bulwahn@gmail.com>
Dear Isabelle developers,
in my latest Isabelle formalization, I stumbled upon an
issue with the linear arithmetic method that the smt method
internally uses.
I am especially reporting this as this tool asks me to do
so with this warning:
Linear arithmetic should have refuted the assumptions.
Please inform Tobias Nipkow.
As it is unclear to me as an user, which tool is to blame,
I must leave it to you, Jasmin, Sascha and Tobias, to find the
details of tool interaction below.
The following theory fragment shows the issue I encountered
in Isabelle2016 (on Windows 10), but I could not test it
on a recent Isabelle developer version yet:
›
theory Issue imports Transcendental
begin
text ‹
First, here is the original formulation of the lemma as I encountered the issue.
Sledgehammer found the smt proof, but smt then fails.
›
lemma sin_diff_minus:
assumes "0 ≤ x" "x ≤ y" "y ≤ 2 * pi"
shows "sin ((x - y) / 2) = - sin ((y - x) / 2)"
apply (smt minus_divide_left sin_minus)
oops
text ‹
In fact, the assumptions are not required for the proof
and the issue can be reproduced in a slightly smaller
lemma without the use of assumptions.
›
lemma sin_diff_minus:
fixes x y :: real
shows "sin ((x - y) / 2) = - sin ((y - x) / 2)"
apply (smt minus_divide_left sin_minus)
oops
text ‹
Fortunately, an alternative proof is quickly found.
The lemma is proved with a few simplification steps.
›
lemma sin_diff_minus:
fixes x y :: real
shows "sin ((x - y) / 2) = - sin ((y - x) / 2)"
by (simp only: sin_minus[symmetric] minus_divide_left minus_diff_eq)
end
Email Gateway (Aug 22 2022 at 13:59):From: Tobias Nipkow <nipkow@in.tum.de>
This is a known problem in linear arithmetic but I haven't gotten around to
tracking it down.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 13:59):From: Sascha Böhme <boehmes@in.tum.de>
Hi Lukas,
linarith works as follows: Based on a decomposition of the original problem into a set of linear inequalities, it tries to find a refutation for them. The trace for the refutation is used to replay the steps, which should yield the Theorem False in the end. Proof replay essentially applies the simplifier with a carefully selected simpset. Whenever the final theorem differs from False, the warning you noticed is shown.
In your particular case, the obvious simplification for „(2x +2y) / 2“ is not performed, because some rule or simproc is missing in linarith’s simpset. Extending the simpset appropriately would be a solution. I’ll see what I can do, such that your issue is resolved in the next release of Isabelle.
Cheers,
Sascha
Von: Lukas Bulwahn
Email Gateway (Aug 22 2022 at 13:59):From: Lawrence Paulson <lp15@cam.ac.uk>
This precise sort of thing has always annoyed me. I was under the impression that we could perform such simplifications (when there is a gcd; simply distributing the /2 is trivial), but upon looking, it seems that no such simprocs ever existed.
Larry
Email Gateway (Aug 22 2022 at 13:59):From: Tobias Nipkow <nipkow@in.tum.de>
Thank you for the analysis, Sascha. Your suggestion for solving the problem
would indeed be welcome. The core of the problem is that we don't have a
completeness result about what our arithmetic simplification procedures do. They
do what they do.
In this particular case the problem comes from the fact that although linear
arithmetic dutifully multiplies the inequations by 2 to get rid of the /2, the
effect is not what is intended: 2*(x+y)/2 is not simplified to x+y, instead the
2 is pulled inside. This is in contrast to 2*x/2, which is simplified to x.
The problem here is that although there is a simproc that simplifies 2*(x+y)/2
to x+y, it cannot do its job because distributivity kicks in first. [In case you
wonder if linear arithmetic needs distributivity, it does: you cannot even build
HOL if you remove distributivity from the linear arithmetic setup.]
Tobias
smime.p7s
Last updated: Apr 26 2024 at 20:16 UTC