Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] proving a class instantiation.

Email Gateway (Aug 18 2022 at 16:24):

From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello,

I have a problem proving a class instantiation.

after the instance keyword I get the following proof obligation:

OFCLASS('a N, some_algebra_class)

First question is how do I unfold this expression to be able to
use apply scripts and not isar structured proofs.

Second if I start an isar proof using the keyword proof,
then I get 8 proof subgoals:

1. /\ a b c . a * b = a * c ==> b = c

2. /\ b a c . b * a = c * a ==> b = c
   ...

3. ...

I have 8 lemmas proved already for all these subgoals.

Now if I use:

fix a b c::"'a N" show "a * b = a * c ==> b = c" by (rule
cancel_times_left, simp) next;

I cannot get rid of the first suboal. The first subgoal changes to:

1. /\ a b c . a * b = a * c ==> ?a12 a b c * b =?a12 a b c * c

2. /\ b a c . b * a = c * a ==> b = c
   ...

3. ...

I find this proof style very difficult. As I mentioned I have
already lemmas for all these subgoals, but I am not
able to use the lemmas to prove the subgoals. Is there an easier
way of discharging the subgoals without retyping them?

Best regards,

Viorel

Email Gateway (Aug 18 2022 at 16:24):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Viorel,

I think what you basically have to write is

instance
apply intro_classes
apply (fact <all your already proved facts)+
done

which can be collapsed to

instance proof
qed (fact <all your already proved facts)+

See the Isar Reference manual for the intro_classes and fact methods.

However I do not recommend to have the obligations proved as separate
lemmas: after instantiation, you can use the corresponding theorems of
the class specification, so this introduces perhaps confusing duplication.

Hope this helps,
Florian
signature.asc

Email Gateway (Aug 18 2022 at 16:24):

From: Brian Huffman <brianh@cs.pdx.edu>
On Tue, Nov 9, 2010 at 4:17 AM, Viorel Preoteasa
<viorel.preoteasa@abo.fi> wrote:

fix a b c::"'a N" show "a * b = a * c ==> b = c"  by (rule
cancel_times_left, simp) next;

I cannot get rid of the first suboal. The first subgoal changes to:

1. /\ a b c . a * b = a * c ==> ?a12 a b c * b =?a12 a b c * c
2. /\ b a c . b * a = c * a ==> b = c

Isar proofs behave strangely when you 'show' something with a
meta-implication (==>) in it, as you've done here. This has been
discussed on the mailing list before:

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2009-April/msg00052.html
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2009-September/msg00044.html

The quick fix is to avoid using this:

fix a b c::"'a N" show "a * b = a * c ==> b = c"

and instead use explicit 'assume' commands:

fix a b c::"'a N" assume "a * b = a * c" thus "b = c"

Hopefully this strange behavior can be changed in a future release of
Isabelle, because using 'show' with meta-implications is useful
sometimes, and users seem to get stuck on the same problem on a
regular basis.

• Brian

Email Gateway (Aug 18 2022 at 16:24):

From: Makarius <makarius@sketis.net>
On Tue, 9 Nov 2010, Brian Huffman wrote:

<viorel.preoteasa@abo.fi> wrote:

fix a b c::"'a N" show "a * b = a * c ==> b = c"  by (rule
cancel_times_left, simp) next;

I cannot get rid of the first suboal. The first subgoal changes to:

1. /\ a b c . a * b = a * c ==> ?a12 a b c * b =?a12 a b c * c
2. /\ b a c . b * a = c * a ==> b = c

The quick fix is to avoid using this:

fix a b c::"'a N" show "a * b = a * c ==> b = c"

and instead use explicit 'assume' commands:

fix a b c::"'a N" assume "a * b = a * c" thus "b = c"

Hopefully this strange behavior can be changed in a future release of
Isabelle,

users seem to get stuck on the same problem on a regular basis.

This is mainly due to the historic goal state output: when the system
prints a subgoal "!!x. A x ==> B x" it means "for arbitrary but fixed x
you may now assume A x and then have to show B x", but this is not
immediately clear. Since the post-Proof-General model is less centered
around goal states anyway, the confusion might disappear by itself at some
point. There are also other reforms in the pipeline (for many years
already) that did not make it into the light of reality yet.

because using 'show' with meta-implications is useful sometimes

Can you give an example for that? I.e. where show "!!x. A x ==> B x"
is needed as such, instead of something that is equivalent to
{ fix x assume "A x" then show "B x" ... } ?

Makarius

Email Gateway (Aug 18 2022 at 16:25):

From: Brian Huffman <brianh@cs.pdx.edu>
On Tue, Nov 9, 2010 at 6:02 AM, Makarius <makarius@sketis.net> wrote:

On Tue, 9 Nov 2010, Brian Huffman wrote:

because using 'show' with meta-implications is useful sometimes

Can you give an example for that?  I.e. where show "!!x. A x ==> B x"
is needed as such

I've used the show "!!x. A x ==> B x" pattern most often in class
instance or locale interpretation proofs, where I have several goals,
and maybe one or two of them have fixes or assumptions. Often I need
to prove a few facts (using have "...") that will be used in multiple
places.

instance
proof
have lemma1: "..."
show "... first class assumption ..."
by (... lemma1 ...)
show "!!x. A x ==> ... second class assumption ..."
by (... lemma1 ...)
show "!!x. B x ==> ... third class assumption ..."
by (... lemma1 ...)
qed

I can't use "next", since that erases all of my local facts along with
the local assumptions:

instance
proof
have lemma1: "..."
show "... first class assumption ..."
by (... lemma1 ...)
next
fix x assume "A x" thus "... second class assumption ..."
by (... lemma1 ...)
(* error: lemma1 is no longer in scope! *)

The only alternative that I knew about before now was to add another
level of nesting, and restate the goal again. For large locale
interpretations this is quite verbose, compared to the original
solution. (Recall that show ?thesis doesn't work for locale
interpretations!)

instance
proof -
have lemma1: "..."
show "OFCLASS('a, foo_class)"
proof
show "... first class assumption ..."
by (... lemma1 ...)
next
fix x assume "A x" thus "... second class assumption ..."
by (... lemma1 ...)
next
fix x assume "B x" thus "... third class assumption ..."
by (... lemma1 ...)
qed
qed

instead of something that is equivalent to
{ fix x assume "A x" then show "B x" ... } ?

Until now I didn't know that using 'show' inside a proof block { .. }
would even work to discharge a goal. Where is this documented? In the
Isar tutorial, proof blocks are only ever used with 'have'.

Indeed, it seems like this would work well in the situation I
described, and it is only a bit more verbose than the show "!!x. A x
==> B x" approach.

Even though it seems that show "!!x. A x ==> B x" is never strictly
necessary, I think that the handling of it should be changed: It
should have exactly the same effect on the goal state as {fix x assume
"A x" thus "B x" }, which is what most users expect. The only other
design choice that makes sense to me is to have show "!!x. A x ==> B
x" cause an error message. The current behavior is just weird.

• Brian

Email Gateway (Aug 18 2022 at 16:25):

From: Tobias Nipkow <nipkow@in.tum.de>
There is one frequent situation where stating a goal in the wysiwyg
style (i.e. with ==>) works very well, namely inductions.

Tobias

Brian Huffman schrieb:

Email Gateway (Aug 18 2022 at 16:25):

From: Makarius <makarius@sketis.net>
On Tue, 9 Nov 2010, Brian Huffman wrote:

On Tue, Nov 9, 2010 at 6:02 AM, Makarius <makarius@sketis.net> wrote:

On Tue, 9 Nov 2010, Brian Huffman wrote:

because using 'show' with meta-implications is useful sometimes

Can you give an example for that?  I.e. where show "!!x. A x ==> B x"
is needed as such

I've used the show "!!x. A x ==> B x" pattern most often in class
instance or locale interpretation proofs, where I have several goals,
and maybe one or two of them have fixes or assumptions. Often I need
to prove a few facts (using have "...") that will be used in multiple
places.

instance
proof
have lemma1: "..."
show "... first class assumption ..."
by (... lemma1 ...)
show "!!x. A x ==> ... second class assumption ..."
by (... lemma1 ...)
show "!!x. B x ==> ... third class assumption ..."
by (... lemma1 ...)
qed

I can't use "next", since that erases all of my local facts along with
the local assumptions:

instance
proof
have lemma1: "..."
show "... first class assumption ..."
by (... lemma1 ...)
next
fix x assume "A x" thus "... second class assumption ..."
by (... lemma1 ...)
(* error: lemma1 is no longer in scope! *)

The only alternative that I knew about before now was to add another
level of nesting, and restate the goal again. For large locale
interpretations this is quite verbose, compared to the original
solution. (Recall that show ?thesis doesn't work for locale
interpretations!)

You can use 'next' -- with plain blocks { ... } without restating a nested
goal. See also section "6.1.2 Blocks" in the isar-ref manual of
Isabelle2009-2.

instead of something that is equivalent to
{ fix x assume "A x" then show "B x" ... } ?

Until now I didn't know that using 'show' inside a proof block { .. }
would even work to discharge a goal. Where is this documented? In the
Isar tutorial, proof blocks are only ever used with 'have'.

The situation of Isabelle manuals is very complex. In general you cannot
expect a tutorial to tell the full story, although the explanation of
'next' in the Isar tutorial is especially misleading, since it suggests a
connection to subgoals that does not exist.

While the reference manuals that are maintained by myself are more
precise, they are often harder to understand. In recent years I have
started to add some examples, so this should become better. (The isar-ref
manual is still lagging behind, but the implementation manual already
gives many concrete standard schemes that work.)

Indeed, it seems like this would work well in the situation I described,
and it is only a bit more verbose than the show "!!x. A x ==> B x"
approach.

Even though it seems that show "!!x. A x ==> B x" is never strictly
necessary, I think that the handling of it should be changed: It should
have exactly the same effect on the goal state as {fix x assume "A x"
thus "B x" }, which is what most users expect. The only other design
choice that makes sense to me is to have show "!!x. A x ==> B x" cause
an error message. The current behavior is just weird.

I'd say it is just a small detail that has not found its proper
application yet. The behaviour is not accidental, and I was fully aware
of it around 1999 when that part of Isar emerged. If I would have forced
other aspects of the language like that in the past, many useful patterns
would have been eliminated.

The recurrent user confusion is always of the same pattern: people think
in terms of tactical goal states and suddenly find themselves in the world
of structured Isar proofs, typically via class instantiation proofs.
This problem can be solved by having the system react on user input in a
way that immediately guides in the right direction.

Makarius

Email Gateway (Aug 18 2022 at 16:25):

From: Makarius <makarius@sketis.net>
It is in fact a short form of this:

{ fix x presume "A x" show "B x" ... }

The question about "short-cuts" in general is of a slightly different
nature. One way is to have the "IDE" make it quick and easy to produce the
right text. Another way is to come up with some extra notational devices
that address this point, and maybe 2 or 3 other ones.

I did start to experiment with various short versions of
{fix x assume "A x" show "B x" ... } in 2006, analogous
to fixes/assumes/shows/obtains at the theory level, but it got swamped in
the release chaos of 2006/2007. But it is not forgotten, and will
re-emerge and some point ...

Makarius

Email Gateway (Aug 18 2022 at 16:25):

From: Brian Huffman <brianh@cs.pdx.edu>
So of the two possible interpretations of show "!!x. A x ==> B x", you
specifically chose the version with 'presume' rather than 'assume'.
Why did you think this was the right choice? Comments on the mailing
list have clearly shown that users uniformly expect the 'assume'
interpretation, and are thoroughly confused by the current behavior.

http://en.wikipedia.org/wiki/Principle_of_least_astonishment

• Brian

Email Gateway (Aug 18 2022 at 16:26):

From: Makarius <makarius@sketis.net>
The behaviour of show "!!x. A x ==> B x" is a natural consequence of how
rule application works in Isar, and I did not force it into another
direction when it emerged many years ago. This is the same principle that
made most of the language work out very well in the end. So you are
asking to close a door where you have entered yourself before.

Moreover, the "expected" treatment of such inlined rules would dilute
important concepts of the Isar language design, and make it harder to
learn it properly later on. One such principle is that native structural
language elements are preferred over logical formulae. If you take the
existing fixes/assumes/shows/obtains for example, it gives the user an
opportinity to add names, attributes, is patterns etc. that can be later
used in the proof. It also avoids an argument, if !!/==> are just copies
of !/--> in HOL, or a separete notation for rules, or whatever.

Abbreviating { fix assume "A x" show "B x" ... } as
show "!!x. A x ==> B x" looses the advantages of Isar structure.
Instead, one could support something simular to fixes/assumes/shows inside
a proof, but as always it requires substantial time to study the
consequences of adding new trees to the garden, and maybe removing some
old ones.

This delicate process of tending the arboretum is further complicated by
different traditions being present at the same time. The whole Isar
framework grew out of certain ideas of tactical reasoning, natural
deduction rule composition, semi-automated reasoning, and fit together so
smoothly that many people still think that "apply" scripts are native to
Isar (although they are only guests).

A marginal question concerning consistency and least surprise: Why do many
people still indent toplevel Isar proofs differently from local ones? E.g.
like this:

lemma foo
by simp

instead of the proper form according to the true logical structure of
Isar:

lemma foo
by simp

Here the "surprise" has again historical roots, because the first version
is how unstructured proof scripts would look like, before they where
manually converted to the new language many years ago.

Makarius

Email Gateway (Aug 18 2022 at 16:26):

From: Tobias Nipkow <nipkow@in.tum.de>

A marginal question concerning consistency and least surprise: Why do
many people still indent toplevel Isar proofs differently from local
ones? E.g. like this:

lemma foo
by simp

instead of the proper form according to the true logical structure of Isar:

lemma foo
by simp

Lambda calculus terms do not need outermost parentheses. Paragraphs in
Ennglish texts are indented, except for the first one in a section. Etc.
For good reasons in each case. And in this case there is not just a
sctructural reason but also the similarity with standard mathematical
practice.

Tobias

Here the "surprise" has again historical roots, because the first
version is how unstructured proof scripts would look like, before they
where manually converted to the new language many years ago.

Makarius

Email Gateway (Aug 18 2022 at 16:27):

From: Makarius <makarius@sketis.net>
I did some thorough research on such details before setting a certain
default in formal proof documents.

The point of paragraph markup is to emphasize the division of the text.
There are two traditions. The one with the indentation and without line
spacing is a bit more "anglo saxon" than the other, and more common in
software packages from the US. But it is not universal, and fails to
achieve its intention with the typical mix of formal and informal parts in
Isar documents.

Here is a recent example:
http://isabelle.in.tum.de/repos/isabelle/rev/b8d89db3e238 that made a big
difference in the clarity of the structure of a text where many paragraphs
are shorter than one line.

Makarius

Email Gateway (Aug 18 2022 at 16:27):

From: Tobias Nipkow <nipkow@in.tum.de>
You misunderstood me. I have not argued that paragraphs should be
indented but that there is an exception to this rule for the first
paragraph - this being another instance of the rule-with-an-exception
pattern. Indeed, your default latex spacing and indenting avoids
excessive and unnecessary indentation. Interestingly avoiding more or
less the indentation pattern you get by the "proper" Isar indentation
rules at the proof level:

lemma
by

lemma
by

Tobias

Makarius schrieb:

Last updated: Nov 21 2024 at 12:39 UTC