# Re: [isabelle] Difficulties with "setsum"

```Hi Alfio,

Your sorry can be proved by:

also have "... = (â k=l..i+1. k)"
proof -
have "{l..i + 1} = insert (i+1) {l..i}" using hip02 by auto
thus ?thesis by simp
qed

Also note, goals like this:

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

```
if both sides can be evaluated to the same value, you can discharge the goal by "eval".
```
Cheers,
Wenda

On 2015-04-22 17:24, Alfio Martini wrote:
```
```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
```this is to add eval_nat_numeral to your simpset, e.g.

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!

```
```

```
```
--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge

```

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