# Re: [isabelle] Difficulties with "setsum"

```Hi,

I think that the main problem is that the automatic methods cannot cope
with following trivial
lemmas, although both sides evaluate correctly with the command 'value',

value "(setsum id {1::int..2}) + (3::int)"
value "(setsum id {1::int..3})"
lemma "(setsum id {1::int..3}) = (setsum id {1..2}) + 3" oops
value "(setsum id {-3::int..3})"
value "(setsum id {-3::int..2}) + 3"
lemma "(setsum id {-3::int..3}) = (setsum id {-3..2}) + 3" oops

I tried sledgehammer  but it does not find anything. Anyway, the last time
sledgehammer worked
fine for me was with Isabelle 2012.

Best!

On Wed, Apr 22, 2015 at 12:00 PM, Manuel Eberl <eberlm at in.tum.de> wrote:

> The problem is that in order to "unroll" the setsum, you first have to
> bring the numerals (e.g. 2, 3, 4) into successor notation. One way to do
>
> apply (auto simp: eval_nat_numeral)
>
> Most of your example work automatically with these, but you will have to
> massage expressions like "(â k::nat â {j. 1âj â jâ3}. k)" by hand a bit
> first, e.g. by proving that "{j. 1âj â jâ3} = {1..3}".
>
>
> One could easily write simplification rules that unroll setsums over
> constant intervals like these automatically or even write a simproc that
> does that, but I don't think that would be very helpful in practice.
>
> Cheers,
>
> Manuel
>
>
>
> On 22/04/15 16:46, Alfio Martini wrote:
>
>> Dear Isabelle Users,
>>
>> 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 ano 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.
>>
>> My thy file is attached and, in the proof, is the only line with "sorry".
>> I would very grateful if anyone could take a quick look at that.
>>
>> To get a better feeling of what are the underlying simplification rules,
>> I performed some tests with setsum, but the results were disappointing.
>> (see below).
>>
>> Besides, acoording to "What is is Main", setsum is defined in
>> "Finite_Set",
>> but in Isabelle 2014 it is defined  in "Groups_Big".
>>
>> (* Testing the setsum function                            *)
>> fun i2n::"int â nat" where
>> "i2n x = (if x â 0 then 0 else Suc (i2n (x - 1)))"
>>
>> value  "int (setsum id {1::nat..5})" (* this works *)
>> lemma  "setsum id {1::nat..2} = (Suc (Suc (Suc 0)))"
>>     apply (auto) oops
>> lemma "setsum id {1::nat..5}= i2n 15"
>>      apply (auto) oops
>> lemma  "(setsum id {1::nat..2})= Suc (Suc (Suc 0))"
>>      apply (auto) oops
>> lemma  "(â k::nat â {j. 1âj â jâ3}. k) = 6"
>>       apply  oops
>> lemma  "(â k::nat | kâ1 â kâ2 . k) = Suc (Suc (Suc 0))"
>>     apply (auto) oops
>> lemma "(â k::nat=1..3. k)= (â k=1..2. k) + 3" oops
>> term "â k=1..n. k"
>> value "â k::nat = 2 ..1. k" (* this works *)
>> (*  end of test                                            *)
>>
>>
>> All the Best!
>>
>>
>
>

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