Email Gateway (Aug 22 2022 at 09:29): Email Gateway (Aug 22 2022 at 09:29):From: Alfio Martini <alfio.martini@acm.org>
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!
SumIntOption.thy
Email Gateway (Aug 22 2022 at 09:30):From: "Eugene W. Stark" <stark@cs.stonybrook.edu>
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
SumIntOption.thy
Email Gateway (Aug 22 2022 at 09:30):From: Alfio Martini <alfio.martini@acm.org>
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!
Email Gateway (Aug 22 2022 at 09:30):From: Manuel Eberl <eberlm@in.tum.de>
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
Email Gateway (Aug 22 2022 at 09:31):From: Alfio Martini <alfio.martini@acm.org>
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!
Email Gateway (Aug 22 2022 at 09:31):From: Manuel Eberl <eberlm@in.tum.de>
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
Email Gateway (Aug 22 2022 at 09:31):From: Alfio Martini <alfio.martini@acm.org>
Great! I tried to use case, but it did not work, because I was not aware
that
I could declare the arbitrary fixed variables in that way (although it
seems to
be there in section 4.4.2 of the tutorial for the case of structural
induction).
Cheers!
Email Gateway (Aug 22 2022 at 09:32):From: Alfio Martini <alfio.martini@acm.org>
Hi Eugene,
and there are lots of apparently unnecessary
assumptions that float in and out.
You are completely right. My original (long) version would be like this
without
the unnecessary assumptions.
theorem
fixes u::int and l::int
assumes assm: "l≤u"
shows "sumO l u f = Some (∑ k=l..u. (f k))" (is "?P u")
using assms
proof (induct u rule: int_ge_induct)
show "?P l"
proof -
have "sumO l l f = Some (f l)" by simp
also have "... = Some (∑ k=l..l. (f k))" by simp
finally show "sumO l l f = Some (∑ k=l..l. (f k))" by this
qed
next
fix i::int
assume hip01: "i≥l" and HI:"?P i"
show "sumO l (i+1) f = Some (∑ k=l..i+1. (f k))"
proof -
have
"sumO l (i+1) f = (case sumO l i f of
None ⇒ None | Some v ⇒ Some ((f (i+1) + v)))"
using hip01 by simp
also have "... = Some (f (i+1) + (∑ k=l..i. (f k)))"
using HI and hip01 by simp
also have "... = Some (∑ k=l..i+1. (f k))"
proof -
have "{l..i + 1} = insert (i+1) {l..i}" using hip01
by auto
thus ?thesis by simp
qed
finally show "sumO l (i+1) f = Some (∑ k=l..i+1. (f k))" by
this
qed
qed
Best!
Last updated: Apr 19 2024 at 04:17 UTC