Email Gateway (Aug 17 2022 at 14:43): Email Gateway (Aug 17 2022 at 14:43):From: Norbert Voelker <norbert@essex.ac.uk>
Trying to prove
lemma div_less_square: "[| x < n * n; 0 < n |] ==> x div n < (n::nat)";
arith fails with the following counter example:
x div n = 1, x = 0, n * n = 1, n = 1
This seems odd given that ((x div n) = (0 div 1) = 0) according to
Divides.div_0.
Any thoughts? Is my interpretation of the counter example perhaps incorrect?
Norbert.
Email Gateway (Aug 17 2022 at 14:44):From: nipkow@in.tum.de
lemma div_less_square: "[| x < n * n; 0 < n |] ==> x div n < (n::nat)";
arith fails with the following counter example:
Multiplication and div are outside linear arithmetic and lead into
undecidable territory. Hence arith ignores them (except in special cases
involving numerals) which means that "n * n" and "x div n" are simply
regarded as new variables. In such cases one may get bogus counter examples.
Tobias
Last updated: May 03 2024 at 04:19 UTC