Email Gateway (Aug 22 2022 at 18:28): Email Gateway (Aug 22 2022 at 18:28):From: Sebastien Gouezel <sebastien.gouezel@univ-nantes.fr>
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
Email Gateway (Aug 22 2022 at 18:28):From: Tobias Nipkow <nipkow@in.tum.de>
We are aware there is an incompleteness but have not been able to track it down.
Thanks
Tobias
smime.p7s
Last updated: Apr 18 2024 at 12:27 UTC