Re: [isabelle] Reasoning with the option type



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!








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