Re: [isabelle] Difficulties with "setsum"



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!






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