Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Proof state in Isar proof style are difficult ...

view this post on Zulip Email Gateway (Aug 17 2022 at 14:15):

From: ehmety@univ-nkc.mr
Hi

I was used to ML proof style and now I am trying to learn the isar mode.
But I found it very hard to follow. I am not sure whether this is normal
or I am missing something:

Let me explain this with this example taken from the ‘Structured Proofs in
Isar/HOL’ document:

lemma assumes ex: "EX x. ALL y. P x y" shows "ALL y. EX x. P x y"
proof
fix a
from ex obtain x where "ALL y. P x y" ..
hence "P x a" ..
thus "EX x. P x a" ..
qed

Proof starts with a nice display of the proof state (with every thing I
need):

proof (state): step 1
fixed variables: P
prems:
EX x. ALL y. P x y
goal (lemma, 1 subgoal):

  1. !!y. EX x. P x y

But things go differently

  1. When I do ‘fix a’ for the variable ‘y’ in the goal,
    I get the equality a = a in the ‘fixed variables’ section.

proof (state): step 2

fixed variables: P, a = a
prems:
EX x. ALL y. P x y

goal (lemma, 1 subgoal):

  1. !!y. EX x. P x y

However I was expecting ‘y = a’ instead.

  1. At the second step (from ex obtain
    ) the display becomes difficult to
    follow:
    a) execution of ‘from ex’ gives:

proof (chain): step 3

picking this:
EX x. ALL y. P x y

(no thing shown about the rest of the state)

b) execution of all the 'from' step returns
have (!!x. ALL y. P x y ==> ?thesis) ==> ?thesis
Every thing is hided.

The same thing happens with proof steps starting ‘have’.

How one can see what goals remain to be proved?

This kind of displays confuses me.

Best regards

view this post on Zulip Email Gateway (Aug 17 2022 at 14:15):

From: chen kun <coolchenice81@gmail.com>
Here is an avaiable proof script:
lemma assumes ex: "EX x. ALL y. P x y" shows "ALL y. EX x. P x y"
proof
fix y - - Here must fix "y" ,which is exacatly the variable name
in your goal
from ex obtain x where "ALL y. P x y" by blast
thus "EX x. P x y" by blast
qed

2006/3/22, ehmety@univ-nkc.mr <ehmety@univ-nkc.mr>:

Hi

I was used to ML proof style and now I am trying to learn the isar mode.
But I found it very hard to follow. I am not sure whether this is normal
or I am missing something:

Let me explain this with this example taken from the 'Structured Proofs in
Isar/HOL' document:

lemma assumes ex: "EX x. ALL y. P x y" shows "ALL y. EX x. P x y"
proof
fix a
from ex obtain x where "ALL y. P x y" ..
hence "P x a" ..
thus "EX x. P x a" ..
qed

Proof starts with a nice display of the proof state (with every thing I
need):

proof (state): step 1
fixed variables: P
prems:
EX x. ALL y. P x y
goal (lemma, 1 subgoal):
1. !!y. EX x. P x y

But things go differently
1. When I do 'fix a' for the variable 'y' in the goal,
I get the equality a = a in the 'fixed variables' section.

proof (state): step 2

fixed variables: P, a = a
prems:
EX x. ALL y. P x y

goal (lemma, 1 subgoal):
1. !!y. EX x. P x y

However I was expecting 'y = a' instead.

  1. At the second step (from ex obtain …) the display becomes difficult to
    follow:
    a) execution of 'from ex' gives:

proof (chain): step 3

picking this:
EX x. ALL y. P x y

(nothing shown about the rest of the state)

You can use "print_context ", " print_theorems" , "print_facts" etc.
to inspect proof contexts . See <<Isar-ref.pdf>> 3.3.2 for details .
Or you can simply use command "term ?thesis" to see what the term
?thesis stands for. See <<Isar-ref.pdf>> 3.3.1 for details.

b) execution of all the 'from' step returns
have (!!x. ALL y. P x y ==> ?thesis) ==> ?thesis
Every thing is hided.

The same thing happens with proof steps starting 'have'.

How one can see what goals remain to be proved?

This kind of displays confuses me.

Best regards

view this post on Zulip Email Gateway (Aug 17 2022 at 14:15):

From: Makarius <makarius@sketis.net>
On Wed, 22 Mar 2006, ehmety@univ-nkc.mr wrote:

I was used to ML proof style and now I am trying to learn the isar mode.
But I found it very hard to follow. I am not sure whether this is normal
or I am missing something

It is indeed hard to convert oneself from tactical proving to structured
proof composition in Isar. Certain old habits need to be unlearned --
after being identified as such in the first place.

Most notably direct focus on goal states is superceded by building up a
local context of parameters, assumptions, facts etc. that is eventually
ready to solve a pending problem.

This kind of displays confuses me.

This is a known problem of Isar. There are many ways to perform a proof
(both structured and unstructured) but different information is relevant
in different situations. The system does not impose a particular policy
here, but leaves it to the user to figure out relevant bits required to
proceed with the reasoning.

For beginners it is best to step through existing structured proof texts
without taking the state display too seriously. In fact, Isar proofs can
be easily maintained without looking at internal states at all. It is
still necessary for interactive development, though.

There is an interesting paper by Dixon and Fleuriot
http://homepages.inf.ed.ac.uk/ldixon/papers/jal-05-proofcentric.pdf that
boldly points out that proof state display should be suppressed
altogether, replacing it by a metaphor of editing the structured proof
text as a hierarchical outline that is completed incrementally.

Makarius

Last updated: May 03 2024 at 04:19 UTC