Re: [isabelle] Isar-Level cases command



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



On 25/11/14 10:15, Joachim Breitner wrote:
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





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