[isabelle] Fwd: Difficulties with "setsum"



---------- Forwarded message ----------
From: Alfio Martini <alfio.martini at acm.org>
Date: Wed, Apr 22, 2015 at 2:17 PM
Subject: Re: [isabelle] Difficulties with "setsum"
To: Wenda Li <wl302 at cam.ac.uk>


Hi Wenda,

>if both sides can be evaluated to the same value, you can discharge the
goal by "eval"

Great. Did not know this.

 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


Very clever. Thanks a lot!!

Best!

On Wed, Apr 22, 2015 at 2:07 PM, Wenda Li <wl302 at cam.ac.uk> wrote:

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



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



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