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



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




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