Re: [isabelle] Isar-Level cases command



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


On 11/25/2014 10:15 AM, 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.