Re: [isabelle] Reasoning with the option type



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



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