Re: [isabelle] Difficulties with "setsum"



Hi Manuel,

Thanks for the feedback. But in my proof, I am working with integers and
that line
with "sorry" does not get proved with this lemma. The line with "sorry"
addresses the very definition
of indexed sums, I think.

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


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