*To*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] Fwd: Difficulties with "setsum"*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Wed, 22 Apr 2015 14:17:44 -0300*In-reply-to*: <CAAPnxw0ui63gpx9st5TKhANiAHtFsmarvFenMA6-4xdPTVHn4A@mail.gmail.com>*References*: <CAAPnxw0x5zBbRJHKZmOahydu+p=AugWjtz_NoGdsPVsxhFAeuQ@mail.gmail.com> <5537B772.9080209@in.tum.de> <CAAPnxw0yO6hUhoWMBb+LLuEqifQ_tHAPuOxW5_zJ6rPaffMnig@mail.gmail.com> <3b8220ed7e2f8734fefb83c5b4ee239d@cam.ac.uk> <CAAPnxw0ui63gpx9st5TKhANiAHtFsmarvFenMA6-4xdPTVHn4A@mail.gmail.com>*Sender*: alfio.martini at gmail.com

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

**References**:**[isabelle] Difficulties with "setsum"***From:*Alfio Martini

**Re: [isabelle] Difficulties with "setsum"***From:*Manuel Eberl

**Re: [isabelle] Difficulties with "setsum"***From:*Alfio Martini

**Re: [isabelle] Difficulties with "setsum"***From:*Wenda Li

- Previous by Date: Re: [isabelle] Difficulties with "setsum"
- Next by Date: Re: [isabelle] Difficulties with "setsum"
- Previous by Thread: Re: [isabelle] Difficulties with "setsum"
- Next by Thread: Re: [isabelle] Difficulties with "setsum"
- Cl-isabelle-users April 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list