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