Email Gateway (Aug 18 2022 at 12:44): Email Gateway (Aug 18 2022 at 12:44):From: Hauser Bruno <bhauser@student.ethz.ch>
Hi
I want to prove the following lemma: ((i - (1::int)) * i div 2) + i = i * (i + 1) div 2. Proving the property for naturals succeeds. I now want to proof it for positive, nonzero integers. Trying to solve the lemma (i_equation_int) automatically with sledgehammer did not succeed. So, no "trivial" solution seems to exist yet.
lemma i_equation_int: "[|(n - (1::nat)) * n div 2 + n = n * (n + 1) div 2; int n = i; i > 0|] ==> ((i - (1::int)) * i div 2) + i = i * (i + 1) div 2"
Can someone give me a hint how to proof it by (maybe) using the facts, that i > 0 and the equation holds for naturals?
Is there a general way for proofing lemmas like: (i>0) & (int n = i) & P(n) ==> P(i) ?
Thank you,
Bruno Hauser
Email Gateway (Aug 18 2022 at 12:44):From: Tobias Nipkow <nipkow@in.tum.de>
Here is a direct proof, without preconditions:
lemma "(i - (1::int)) * i div 2 + i = i * (i + 1) div 2"
Tactic arith cannot deal with it because it contains multiplication in
an essential way. However, if you first multiply out, then arith can
solve it:
apply(simp add: ring_simps)
apply arith
done
Regards
Tobias
Hauser Bruno wrote:
Email Gateway (Aug 18 2022 at 12:44):From: Jeremy Avigad <avigad@cmu.edu>
Hauser Bruno wrote:
Is there a general way for proofing lemmas like: (i>0) & (int n = i)
& P(n) ==> P(i) ?
Dear Bruno,
The answer is "yes" and "no." There are methods for transferring results
from the natural numbers to the integers and vice-versa, though they are
imperfect.
Suppose you have a theorem of the form "ALL (n::nat). P n" and you want
a theorem of the form "ALL i >= (0::int). P' i", where P' is the
translation of P to the integers (e.g. nat functions and relations like
+, div, < are replaced by the integer versions).
First, use a general rule to convert "ALL i >= (0::int). P' i" to "ALL
n. P' (int n)." Then using simplification rules like
int n + int m = int (n + m)
(int n) div (int m) = int (n div m)
int n < int m = n < m
and magically "ALL n. P'(int n)" is transformed to "ALL n. P n," which
is what you have already proved. Amine Chaieb once described a similar
method on this mailing list.
(Your question involved proving, more simply, P'(int n) from P n, which
only needs the simplification rules.)
I have been revising the number theory libraries and using this method
to make sure that all basic theorems are in place for both nats and
ints. If you want, I can send you a file that works in the developer
version of Isabelle, which uses the method above to transfer results
involving gcd, lcm, factorial, prime, congruence, choose, and fib. But
it is still tedious. Chaieb and I have been working on better ways of
automating the procedure, and hope to have better methods soon.
Jeremy
Last updated: May 03 2024 at 04:19 UTC