[isabelle] Unusual simp behavior

[Sebastien Gouezel]

I just encountered an unusual behavior of simp. It was working fine to
prove a simple inequality. Then I changed a parameter in this inequality
(replacing 7/6 by 5/4, but the inequality remained valid for exactly the
same reason). simp stopped working on the inequality, and I got a trace
message saying "Linear arithmetic should have refuted the assumptions.
Please inform Tobias Nipkow."

It is not a problem for me at all, as try0 told me to use argo instead,
which works fine. But if this is of interest to someone who wants to
investigate further, this is in
afp_devel/thys/Gromov_Hyperbolicity/Morse_Gromov_Theorem.thy, line 1970.

Sebastien

[Tobias Nipkow]

We are aware there is an incompleteness but have not been able to track it down.

Thanks
Tobias

I just encountered an unusual behavior of simp. It was working fine to prove a
simple inequality. Then I changed a parameter in this inequality (replacing 7/6
by 5/4, but the inequality remained valid for exactly the same reason). simp
stopped working on the inequality, and I got a trace message saying "Linear
arithmetic should have refuted the assumptions. Please inform Tobias Nipkow."
It is not a problem for me at all, as try0 told me to use argo instead, which
works fine. But if this is of interest to someone who wants to investigate
further, this is in
afp_devel/thys/Gromov_Hyperbolicity/Morse_Gromov_Theorem.thy, line 1970.
Sebastien