Email Gateway (Aug 19 2022 at 16:29): Email Gateway (Aug 19 2022 at 16:29):From: Joachim Breitner <breitner@kit.edu>
Dear Isabelle-users,
we (rightfully) pride ourselves with how natural nicely written Isar
proofs are. But things are (always) not perfect, and there is always
room for careful improvements.
Consider this rather idiomatic proof:
lemma "length (filter P xs) ≤ length xs"
proof(induction xs)
case Nil thus ?case by simp
next
case (Cons x xs)
show ?case
proof(cases "P x")
case True with Cons
have "length (filter P (x#xs)) = Suc (length (filter P xs))" by simp
also note Cons.IH
also have "Suc (length xs) = length (x#xs)" by simp
finally show ?thesis by this simp
next
case False with Cons
have "length (filter P (x#xs)) = length (filter P xs)" by simp
also note Cons.IH
also have "length xs ≤ length (x#xs)" by simp
finally show ?thesis .
qed
qed
It is a nicely written structural proof and easy to follow. But there is
a wart: The case distinction!
* I have to write "show ?case" to initiate a case distinction. But
this is not natural: At this point, the final result is not what
is on my mind. And in a manually written proof, I would not
re-state the current goal at this point.
* If I had not used the "case" command I would actually have to
copy’n’paste the current goal here; obviously not very nice.
Especially if there are multiple case distinction, each
requiring me to copy that.
* The goal was conveniently named ?case, but suddenly I have to
write ?thesis. I (believe I) understand the techical reasons,
but again, this is a violation of the principle of least
surprise.
What I would like to be able to write is something like
lemma "length (filter P xs) ≤ length xs"
proof(induction xs)
case Nil thus ?case by simp
next
case (Cons x xs)
cases("P x")
case True with Cons
have "length (filter P (x#xs)) = Suc (length (filter P xs))" by simp
also note Cons.IH
also have "Suc (length xs) = length (x#xs)" by simp
finally show ?case by this simp
next
case False with Cons
have "length (filter P (x#xs)) = length (filter P xs)" by simp
also note Cons.IH
also have "length xs ≤ length (x#xs)" by simp
finally show ?case .
qed
qed
No seemingly redundant statement of the subgoals, the ability to simply
use ?case and the conventional flow of thoughts and facts in such a
proof.
This would also open the way to conveniently discharge multiple subgoals
in one case distinction:
lemma "A" and "B"
proof-
have "C" sorry
cases ("D")
case True
from C show A using True sorry
thus B using True sorry
next
case False
from C show B using False sorry
thus A using False sorry
qed
qed
(Note that in this case, no ?thesis is available, and
show A and B proof (cases "D")
does not do the right thing, as it apply the cases rule only to the
first subgoal, so it becomes messy to do this proof right now.)
This is the users mailing list, so I’ll refrain from making wild
assumptions about if and how this could be implemented, and whether
there is a similarity to the obtains command, but instead ask you for
feedback on the user-facing design of this feature:
Is it something you’d want as well?
Is the syntax nice?
What could be the closing keyword, if not qed?
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 16:29):From: Christian Sternagel <c.sternagel@gmail.com>
I think this "use-case" is covered by raw proof blocks. In general I
often find that proofs get much more readable when using those (of cause
the caveat is that we often have to restate assumptions/their negations,
but this can all be handled by tasteful use of "let ?x = ..." before).
So here is what I would write:
lemma "length (filter P xs) ≤ length xs"
proof (induction xs)
case (Cons x xs)
{ assume "P x"
with Cons have "length (filter P (x#xs)) = Suc (length (filter P
xs))" by simp
also note Cons.IH
also have "Suc (length xs) = length (x#xs)" by simp
finally have ?case by simp }
moreover
{ assume "¬ P x"
with Cons have "length (filter P (x#xs)) = length (filter P xs)" by
simp
also note Cons.IH
also have "length xs ≤ length (x#xs)" by simp
finally have ?case . }
ultimately show ?case by cases
qed simp
cheers
chris
Email Gateway (Aug 19 2022 at 16:29):From: Joachim Breitner <breitner@kit.edu>
Hi,
right. This works ok for boolean cases, but what if my invocation of the
"cases" method is actually a complicate 5-way case distinction on some
expression, or an inductive predicate with multiple variables and lots
of assumptions in each case.
There I really would like to rely on named cases, and that rules out
manual proof blocks.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 16:29):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Joachim,
Personally, I do not mind having to state the "show ?case" part, because it makes clear
that you really need to do the case distinction to prove the whole case. In fact, I think
that your case distinction in the example is not as it should be, because you only need it
to for the unfolding of filter. The remaining reasoning is essentially the same, and I
would prefer if that could be expressed more easily.
Here's what I would like to see as the proof structure:
lemma "length (filter P xs) ≤ length xs"
proof(induction xs)
case Nil thus ?case by simp
next
case (Cons x xs)
let ?n = "if P x then 1 else 0"
have "length (filter P (x#xs)) = ?n + length (filter P xs)"
by(cases "P x") simp_all
also note Cons.IH
also have "?n + length xs <= length (x # xs)"
by(cases "P x") simp_all
finally show ?case .
qed
Unfortunately, Isabelle does not provide good syntax to express such expression. I think
this is the reason for having so many proofs in the style of show ?case proof(cases ...).
As Christian Sternagel mentioned, raw proof blocks are sometimes an option, but I do not
like them much either. If you have multiple goals, you can use "case_tac [!] ..." instead
of "cases ..." to do a case distinction on all of them. Unfortunately, this does not give
you the case names.
Andreas
Email Gateway (Aug 19 2022 at 16:30):From: Joachim Breitner <breitner@kit.edu>
Hi,
True, in this sense the example is a bit lacking. And you are rightly
pointing out that fact that for showing an intermediate statement using
case distinction the current scheme is useful. So I would not go as far
to expect that
cases ("xs")
case Nil
have P
next
case (Cons x xs')
have P
qed
to be equivalent to
have P
proof (cases "xs"))
case Nil
have P
next
case (Cons x xs')
have P
qed
and hence (heh) suggest this feature only for the case (heh) where one
or more actual subgoals are shown (heh) in each case (heh).
(Although I would not dismiss the above if it turns out to be feasible).
Greetings,
Joachim
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC