*To*: Manuel Eberl <eberlm at in.tum.de>*Subject*: Re: [isabelle] Reasoning with the option type*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Tue, 28 Apr 2015 12:11:45 -0300*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <553F594F.4000207@in.tum.de>*References*: <CAAPnxw2YxsozyTqNnsmZghfdRa6_6f9mVTcPT7fqC7SCtp42qg@mail.gmail.com> <553F5055.2080009@cs.stonybrook.edu> <CAAPnxw0m+0cE8mTy0ABpFuBR45_iuF2-ipjkAXREaUTJb55=YA@mail.gmail.com> <553F594F.4000207@in.tum.de>*Sender*: alfio.martini at gmail.com

Hi Manuel, Thank you for the explanations about this more general technique. I have seen now that it is explained in detail in the "Programming and Proving" tutorial under the name of "computation induction". I have tried to see the logical structure underlying your version of the proof using Isar. I came up with the following and I assume there is a more elegant way to write it. lemma setsum_last_int: "(n::int) < m â f m + setsum f {n..m - 1} = setsum f {n..m}" by (subst setsum.insert[symmetric]) (auto simp del: setsum.insert intro: setsum.cong) theorem assumes "l â u" shows "sumO l u f = Some (âk=l..u. f k)" (is "?P l u f") using assms proof (induction l u f rule: sumO.induct) fix l::int and f show "?P l l f" by simp next fix n::int and m and f assume "n<m" and "(n â m - 1 ==> ?P n (m - 1) f)" then show "?P n m f" using setsum_last_int by simp next fix n::int and m and f assume "m<n" and "nâm" then have False by simp then show "?P n m f" by (rule FalseE) qed It was very helpful, because I havenÂt seen before that the last goal follows by a simple contradiction. Yet, I am not comfortable with the way I wrote the induction hypothesis in the second goal. I had to use the metalogical symbol "==>". Assuming that I insist and writing all the details above, how could I avoid using "==>"? I have no clue. Best! On Tue, Apr 28, 2015 at 6:56 AM, Manuel Eberl <eberlm at in.tum.de> wrote: > It is, of course, not unreasonable to do things by hand like you did in > order to get to know the system better. > > I would, however, like to show you how to shorten the proof a bit more. > Isabelle's automation is very powerful, but you have to help it along a > bit. As a rule, when you try to prove a fact about a recursively-defined > function, it is advisable to use the induction rule for that function that > the function package gives you. It makes things easier, both for you and > for the automation. > > So let's apply it and see what we end up with: > > theorem > "l â u â sumO l u f = Some (âk=l..u. f k)" > apply (induction l u f rule: sumO.induct) > apply simp_all > > The remaining goal is then something like > ân m f. n < m â f m + setsum f {n..m - 1} = setsum f {n..m} > > This should be intuitively obvious, we're just splitting off the last term > in the sum from n to m. We can show this as an auxiliary lemma, e.g. > > lemma setsum_last_int: > "(n::int) < m â f m + setsum f {n..m - 1} = setsum f {n..m}" > by (subst setsum.insert[symmetric]) (auto simp del: setsum.insert intro: > setsum.cong) > > Now the proof is fully automatic: > theorem > "l â u â sumO l u f = Some (âk=l..u. f k)" > by (induction l u f rule: sumO.induct) (simp_all add: setsum_last_int) > > > Cheers, > > Manuel > > > > On 28/04/15 11:34, Alfio Martini wrote: > >> Hi Eugene, >> >> Thank you for your feedback. Indeed it looks much shorter, since the >> simplifier takes care of the >> many intermediate steps I wrote it down. Anyway, at least for these >> exercises, I try to use Isabelle to check >> my handwritten proofs (or any handwritten proof that is made without >> assuming automated tools). >> That is why they look unnecessary long. But I will use some of your >> suggestions in order to improve its presentation. >> >> Best! >> >> On Tue, Apr 28, 2015 at 6:18 AM, Eugene W. Stark <stark at cs.stonybrook.edu >> > >> wrote: >> >> I am not very experienced, but I looked at your proof. >>> It seems very long, and there are lots of apparently unnecessary >>> assumptions that float in and out. I came up with the attached, >>> which is rather shorter. I did not see how the use of the >>> option type introduces any complication here. Hopefully I did >>> not misunderstand something important. >>> >>> - Gene Stark >>> >>> >>> On 04/27/2015 11:55 PM, Alfio Martini wrote: >>> >>>> Dear Isabelle Users, >>>> >>>> In a previous thread (Isabelle: A logic of partial functions?) I asked >>>> some questions about the use of the constant "undefined" when >>>> dealing with partial functions, which have to be made total according >>>> to the foundations of Isabelle. >>>> >>>> The long thread about my difficulties with Sledgehammer made >>>> me realize that my definition was not general enough. And after >>>> looking into the very well written tutorial on Code Generation, I >>>> was convinced that I had to deal with the option type. >>>> >>>> I'm also very grateful to all that reply my original messages with >>>> many insightful and helpful observations. >>>> So, if some novice is interested I include here (my) proof of the >>>> total correctness of that sum algorithm. >>>> >>>> I only ask the evaluation of some more experienced user, if >>>> this is the correct way to reason with the option type. It looks >>>> a bit clumsy. >>>> >>>> The thy file is attached. Many thanks for any remarks! >>>> >>>> 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

**Follow-Ups**:**Re: [isabelle] Reasoning with the option type***From:*Manuel Eberl

**References**:**[isabelle] Reasoning with the option type***From:*Alfio Martini

**Re: [isabelle] Reasoning with the option type***From:*Eugene W. Stark

**Re: [isabelle] Reasoning with the option type***From:*Alfio Martini

**Re: [isabelle] Reasoning with the option type***From:*Manuel Eberl

- Previous by Date: [isabelle] accessing ML definitions in isabelle_process
- Next by Date: Re: [isabelle] Reasoning with the option type
- Previous by Thread: Re: [isabelle] Reasoning with the option type
- Next by Thread: Re: [isabelle] Reasoning with the option type
- 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