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,
always very helpful.


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
> zle_add1_eq_le)



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
>> zle_add1_eq_le)
>>
>> 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.