*To*: "W. Douglas Maurer" <maurer at gwu.edu>*Subject*: Re: [isabelle] Difficulties with "setsum" (Alfio Martini)*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Wed, 22 Apr 2015 23:50:39 -0300*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <a0620070fd15deab6d15d@192.168.1.6>*References*: <mailman.39335.1429716197.13101.cl-isabelle-users@lists.cam.ac.uk> <a0620070fd15deab6d15d@192.168.1.6>*Sender*: alfio.martini at gmail.com

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

**Follow-Ups**:**Re: [isabelle] Difficulties with "setsum" (Alfio Martini)***From:*Makarius

- Previous by Date: [isabelle] CfP HOFM Workshop @ SEFM 2015 (York, UK)
- Next by Date: [isabelle] Is there example to use Backward Hoare and Forward Floyd to find subgoal from goal
- Previous by Thread: Re: [isabelle] Difficulties with "setsum" (Alfio Martini)
- Next by Thread: Re: [isabelle] Difficulties with "setsum" (Alfio Martini)
- Cl-isabelle-users April 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list