Lukas Bulwahn
2016-08-13 07:56:18 UTC
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
--
Best regards,
Lukas
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
--
Best regards,
Lukas