# Re: [isabelle] Reasoning with the option type

Since the induction hypothesis contains meta implication, there is no other way to write it. You can, however, give names to your three different cases so you don't have to fix/assume everything yourself:
```

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[case_names 1 2 3])
case (1 l f)
show ?case by simp
next
case (2 n m f)
thus ?case using setsum_last_int by simp
next
case (3 n m f)
hence False by simp
thus "?P n m f" by (rule FalseE)
qed

Cheers,

Manuel

On 28/04/15 17:11, Alfio Martini wrote:
```
```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 <mailto: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 <mailto: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
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.

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
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 <http://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.