# Re: [isabelle] Difficulties with "setsum" (Alfio Martini)

• To: cl-isabelle-users at lists.cam.ac.uk
• Subject: Re: [isabelle] Difficulties with "setsum" (Alfio Martini)
• From: "W. Douglas Maurer" <maurer at gwu.edu>
• Date: Wed, 22 Apr 2015 20:29:00 -0400
• Cc: maurer at gwu.edu
• References: <mailman.39335.1429716197.13101.cl-isabelle-users@lists.cam.ac.uk>

```On 22 Apr 2015, Alfio Martini <alfio.martini at acm.org> wrote:

```
```While trying to prove the correctness of a simple function that returns
the sum of the values between integers  l and u, I stumbled upon
an unexpected problem: I was not able to prove that

(Sum k=l..(u+1). k) = (u+1) + (Sum k=l...u) if l<u+1, which should
hold by the definition of an indexed sum.
```
```
I asked this question on March 6th, 2015, in the following more general form:

```
I am having problems with forward proofs by induction. I would like for Isar to be able to prove that 1+4+9+...+n*n = (n*(n+1)*(2*n+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.
```
```
This appeared in Cl-isabelle-users Digest, Vol 117, Issue 10, #6, and Andreas Lochbihler replied to it as follows:
```
```
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)"
atLeastLessThanPlusOne_atLeastAtMost_int atLeastLessThan_iff
```
```
Hope this helps,
Andreas
```
```
This appeared in Cl-isabelle-users Digest, Vol 117, Issue 10, #7.
--
Prof. W. Douglas Maurer                Washington, DC 20052, USA
Department of Computer Science         Tel. (1-202)994-5921
The George Washington University       Fax  (1-202)994-4875

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.