[isabelle] Discharging one (trivial) case without nesting the proof

[Joachim Breitner]

Dear Isabelle users (and devs),

Chrisoph’s question (http://stackoverflow.com/questions/16629417) proofs
by cases reminded me of a feature wish that I wanted to talk about for a
while.

In pen-and-paper proofs, if there are corner cases for which the result
is immediate, I just mention them at the beginning and continue with the
interesting cases:

Lemma: Every set that has property Q also has property P.

Proof: Let S be a set with property Q. Clearly, empty sets have
property P, so assume x ∈ S.
[long proof]
So S has property P.

In Isar, I would have to write:

lemma "Q S → P S"
proof
assume "Q S"
show "P S"
proof(cases "S = {}")
assume True thus "P S" by simp
next
assume False
then obtain "x ∈ S" by auto
..
show "P S"
qed
qed

What I don’t like about this is that the main proof (..) is indented
deeper than it is in my mental model of the proof.

Note that if I could conclude False from "S = {}" and my current facts,
I could write the proof without additional indenting, e.g. using obtain.
But showing False or showing that the result holds is not a huge
difference in my understanding of a particular proof, so what I would
like to see is, for example,

lemma "Q S → P S"
proof
assume "Q S"

trivially "S ~= {}"
proof
assume "~ ~ S = {}"
show "P S" by simp
qed
then obtain "x ∈ S" by auto
..
show "P S"
qed

where (attention, obviously inaccurate understanding of Isar’s workings
under the hood following:) "trivially P" opens a proof goal "~P ==> ?P",
and the user is expected to finish this proof with "show Q" where Q is
the same result that he will show in the outer block. After the
"trivially P" command, P is added to the facts and to this. Note the
similarity with the obtain command, where I have to shown an abstract
"that".

I know that this is but a small reshuffling of the statements that I’d
have to write with "show Q proof(cases P)...", but it does make a
difference for the readability of the proof.

Bonus points if somehow inside the proof block opened by tivially the
statement to be shown is somehow inferred, so that I can just write

lemma "Q S → P S"
proof
assume "Q S"

trivially "S ~= {}" by simp
then obtain "x ∈ S" by auto
..
show "P S"
qed

Greetings and happy Whitsun,
Joachim

--
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

[Christian Sternagel]

On 05/19/2013 07:02 PM, Joachim Breitner wrote:
> lemma "Q S → P S"
> proof
> assume "Q S"
> show "P S"
> proof(cases "S = {}")
> assume True thus "P S" by simp
> next
> assume False
> then obtain "x ∈ S" by auto
> ..
> show "P S"
> qed
> qed

Instead, you could write:

lemma "Q S --> P S"

proof
assume "Q S"
show "P S"
proof (cases "S = {}")

assume "S ~= {}"

then obtain "x : S" by auto

...
show "P S"
qed simp
qed

which looks (I guess) very similar to what you suggested:

> lemma "Q S → P S"
> proof
> assume "Q S"
> trivially "S ~= {}"
> proof
> assume "~ ~ S = {}"
> show "P S" by simp
> qed
> then obtain "x ∈ S" by auto
> ..
> show "P S"
> qed
>

Maybe I do not get your main point?

cheers

chris

[Joachim Breitner]

Hi,

It does look similar, but I still have to start the proof by stating
what I want to show (which I would not do in the pen-and-paper proof),
and I still have to have two nested blocks.

I also have cases in mind where the „trivial“ proof is a bit more
involved than something that you would put after qed, but still much
shorter than the „main proof“.

Also, putting it after the qed almost completely hides that the case is
handled. Compare this with the pen-and-paper-proof: The trivial case is
mentioned beforehand (and then discharged as uninteresting).

I know that my arguing is very much on the „personal preference and
perception“ level, and getting proofs to look good and to be a pleasant
read is a very subjective thing...

Maybe I could also state my idea this way, which does not talk about
style any more and might allow other uses as well:

Would it be possible to get a variant of obtains where the proof
obligation is not an abstract "this", but rather the actually
goal shown afterwards?

This introduces a non-linearity into the proof that might feel very
wrong in ProofGeneral, but with the parallel style of jedit, this might
actually make sense. One would probably start with a proof of "sorry"
for the proof, continue the rest, and then finish the obtains proof when
the conclusion correctly known.


Greetings,