Email Gateway (Aug 22 2022 at 09:02): Email Gateway (Aug 22 2022 at 09:02):From: "W. Douglas Maurer" <maurer@gwu.edu>
I am having problems with forward proofs by induction. I would like
for Isar to be able to prove that 1+4+9+...+nn = (n(n+1)(2n+1))/6
and the like. In order to do the inductive proof, I have to know that
m<=n implies (f(m)+f(m+1)+...+f(n+1)) =
(f(m)+f(m+1)+...+f(n))+f(n+1), for integers m and n. In Isar, this
becomes that m<=n implies (setsum f {m..n+1} = (setsum f {m..n}) +
f(n+1)). This would seem to be a fundamental rule, and yet I cannot
seem to find it anywhere in either the library or the supplemental
library. The closest I have come to it is a lemma called
setsum_atMost_Suc in section 59.8 (Summation Indexed over Intervals)
of the library. This says that (SUM i<=Suc n. f i) = (SUM i<=n. f
i)+f(Suc n), where SUM represents the upper-case sigma. It works for
m = 0, but not in the general case; and not every induction with an
integer index starts with 0. How do I get this to work?
(A friend suggested that I use the Query panel to search for
theorems; and, specifically, searching for setsum and Suc returns
theorems such as setsum_op_ivl_Suc, setsum_head_upt_Suc,
setsum_head_Suc, and setsum_cl_ivl_Suc. These, however, do not appear
to meet my needs, because they all involve Suc, and therefore involve
nat rather than int, and therefore do not cover the case when m < 0.)
Email Gateway (Aug 22 2022 at 09:02):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
There are far fewer theorems about setsum over intervals of integers than over natural
numbers. Still, there are enough theorems in the library to prove what you want.
Sledgehammer finds the following proof for me:
lemma "m ≤ n ⟹ setsum f {m..n + 1} = setsum f {m..n} + f (n + 1 :: int)"
by(metis add.commute atLeastAtMostPlus1_int_conv
atLeastLessThanPlusOne_atLeastAtMost_int atLeastLessThan_iff
finite_atLeastAtMost_int linear not_less setsum.insert zle_add1_eq_le)
Hope this helps,
Andreas
Last updated: Apr 23 2024 at 04:18 UTC