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

```Hi Douglas,

I followed that discussion very closely. In fact, from those messages
I took the idea of structuring the proof that I emailed in a previous
thy file in this thread. Somehow I have missed this particular remark
from Andreas who is,  amongst many other experts in this list,

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 "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

I use the Windows installation of  Isabelle 2014 and my sledgehammer
installation does not find any proof for this lemma. Actually, it never
finds any proof whatsoever. I have just realized that it does not solve
even that lemma in section 3 (First Steps) of the Sledgehammer tutorial. I
have always used Sledgehammer as it is packaged. I just set z3
non-commercial
use to "yes". The prover "remote-vampire" is never available (literally),
while e, spass and z3 always time out.

I will have to take a look into this. This is really making may Isabelle
experience miserable  at the moment.

All the Best!

On Wed, Apr 22, 2015 at 9:29 PM, W. Douglas Maurer <maurer at gwu.edu> wrote:

> 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)"
>> by(metis add.commute atLeastAtMostPlus1_int_conv
>>           atLeastLessThanPlusOne_atLeastAtMost_int atLeastLessThan_iff
>>           finite_atLeastAtMost_int linear not_less setsum.insert
>>
>> 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
>
>

--
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
www.inf.pucrs.br/alfio
Av. Ipiranga, 6681 - PrÃdio 32 - Faculdade de InformÃtica
90619-900 -Porto Alegre - RS - Brasil

```

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