Email Gateway (Aug 18 2022 at 15:50): Email Gateway (Aug 18 2022 at 15:50):From: Ian Lynagh <igloo@earth.li>
Hi all,
Here are some of the things I have been struggling with as an Isabelle
complete beginner (but with a some knowledge of coq). I hope you will
find this useful in improving the Isabelle language and/or docs.
I have "(Isabelle2009-1: December 2009)".
How does Isabelle know how much to process when I click the "Process the
next proof command" in Proof-General? In coq this is nice and simple: It
processes up to the next "." (that's actually a slight simplification,
but that's not relevant here). With Isabelle, I'm not really sure what
happens. If I have this source:
theory Test
imports Main
begin
lemma "A & B ==> B & A"
proof
and I have processed up to, but not including, "proof", then pressing
the arrow processes "proof" and succeeds. But if I also write "foo"
after "proof", even with some whitespace:
theory Test
imports Main
begin
lemma "A & B ==> B & A"
proof
foo
Isabelle says
*** Unknown proof method: "foo"
*** At command "proof".
and if I had put a "." after "proof"
theory Test
imports Main
begin
lemma "A & B ==> B & A"
proof.
then now the "lemma" line fails with
*** Outer syntax error: end of input expected,
*** but command proof was found
I can't emphasise enough just how thoroughly confused I am by this.
===================================================================
It also makes Isabelle hard to use for me. My coq scripts generally look
like:
<valid proof that I've finished>.
<the line I'm working on>.
<invalid stuff, alternate possibilities for the next line, etc>
and the invalid stuff, coming after a ".", doesn't interfere with my
work on the current line. I have to keep fiddling with comments to do
this in Isabelle.
How does one write a comment in Isabelle? If I search for "comment" in
tutorial.pdf then the first real mention is on p67(p57), in the
"Document Preparation" section. Three pages later, in the same section,
says
Isabelle source comments, which are of the form (* ... *)
and as far as I can see this is the only mention in the document - a
section I didn't look at, as I wasn't concerned with making PDFs at this
stage. "comments" is also not in the index; I would never have thought
to look up "source comments". I would expect to be told what comments
look like around p14-15(p4-5).
Am I right in thinking that "--" does not start a comment in a source
file? Because while trying to copy/paste/run this example:
lemma assumes P: "! x. P x" shows "! x. P(f x)"
proof -- allI: (!! x. ?P x) = ! x. ?P x
fix a
from P show "P(f a)" .. -- allE : [[ x. ?P x; ?P ?x = ?R ]] = ?R
qed
from p9 of isar-overview.pdf I certainly assumed that it did. Having to
look up the ASCII names of the symbols is annoying enough; why not use
Isabelle comment syntax when putting comments in the middle of example
Isabelle code?
I was very surprised to not find Isabelle packaged in Debian. This was a
significant factor in me not also trying Isabelle about 2 years ago, when
I started with coq, and if coq's Czar showed more signs of life I would
not have considered trying Isabelle. I am sad to see in
http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=494491
that this seems to be deliberate.
Thanks for reading, and I hope you found this useful.
Thanks
Ian
Email Gateway (Aug 18 2022 at 15:50):From: Makarius <makarius@sketis.net>
On Sat, 14 Aug 2010, Ian Lynagh wrote:
I have "(Isabelle2009-1: December 2009)".
There is no problem with it, but you might want to try the current version
Isabelle2009-2 (June 2010).
How does Isabelle know how much to process when I click the "Process the
next proof command" in Proof-General?
It processes the next command, up to the last non-whitespace text before
the following command. Of course, the question here is what a "command"
actually means in Isabelle/Isar. The quick reference in Appendix A of the
isar-ref manual might be helpful.
In particular, "." is a command of its own, not a command terminator like
in Coq. (We have the more conventional ";" for that, but it has almost
come out of use in recent years, since Proof General is good enough to
determine command boundaries from the keywords alone.)
But if I also write "foo" after "proof", even with some whitespace:
theory Test
imports Main
beginlemma "A & B ==> B & A"
prooffoo
Isabelle says
*** Unknown proof method: "foo"
*** At command "proof".
In Isar 'proof' and 'qed' are not just parentheses, but actually do
something. See the quick reference again, especially for important
abbreviations like "by m1 m2 == proof m1 qed m2". Extra whitespace never
makes a difference in syntax recognition.
and if I had put a "." after "proof"
theory Test
imports Main
beginlemma "A & B ==> B & A"
proof.then now the "lemma" line fails with
*** Outer syntax error: end of input expected,
*** but command proof was found
Here the confusion is again that "." is completely different from Coq.
Put a space between these two commands, and you should see proper
font-lock highlighting in Emacs and less confusing Isabelle
It also makes Isabelle hard to use for me. My coq scripts generally look
like:
<valid proof that I've finished>.
<the line I'm working on>.
<invalid stuff, alternate possibilities for the next line, etc>
and the invalid stuff, coming after a ".", doesn't interfere with my
work on the current line. I have to keep fiddling with comments to do
this in Isabelle.
As mentioned above, Proof General will stop before the next proper command
keyword. E.g. you can put a dummy stopper like 'done' or '.' before the
invalid stuff to prevent it from running into it.
How does one write a comment in Isabelle?
Normally you don't, but you intersperse the formal text with informal one,
using commands like 'text' or 'section' or 'subsection'. Small marginal
attachments can be written everywhere like this:
assume A -- "blah blah"
In any case you need to quote such text using "..." or the more convenient
{* ... *} The latter allows to have quoted text inside without further
escapes.
Isabelle source comments, which are of the form (* ... *) and as far as
I can see this is the only mention in the document
Think of these "source comments" like % in LaTeX, i.e. they are not really
part of what you write.
Am I right in thinking that "--" does not start a comment in a source
file? Because while trying to copy/paste/run this example:
After all these years, the generated PDF/LaTeX files are still unsuitable
for copy/paste. There have been some recent movements in the pdflatex
camp towards more serious "tagged PDF", and there is some hope that we
will be able to use it soon.
For now you should start with real example source files, to get an idea
how to type things, especially where to put quotes and where not.
Makarius
Email Gateway (Aug 18 2022 at 15:50):From: Ian Lynagh <igloo@earth.li>
Thanks for your reply Makarius. Some helpful tips there, although the
main purpose of my mail was to try to highlight the sorts of
difficulties that beginners (well, at least one beginner!) run into.
Actually, I've just run into something that really does have me stumped:
It seems that "fix a" does nothing at all, yet it can be necessary;
looks like magic to me! e.g. in this proof:
theory Test
imports Main
begin
lemma assumes P: "! x. P x" shows "! x. P(f x)"
proof
fix a
from P show "P(f a)" ..
qed
the "proof state" is the same before and after the "fix a" line (well,
apart from the step counter being incremented, but I assume that's not
relevant), as are the "cases", "facts", and "term bindings". So how am I
meant to know whether I need to fix something, if doing so has no
visible effect? Am I missing something?
This is a real problem for me in the proof I'm trying to write. I have
goals like
!!bool. principalType (EBool bool) = Some t ==> STyping (EBool bool) t
and I have no idea if the commands I'm giving are taking me in the right
direction or not, as they seemingly do nothing.
I am also surprised that "facts", and perhaps also "term bindings", are
not shown by default. Not only that, but proof general has given me a
toolbar button that tells me "theory Test", but not a toolbar button to
tell me the current facts; is wanting the former really more common than
wanting the latter?
That reminds me of another minor irritation: If I write this partial
proof:
theory Test
imports Main
begin
lemma "A & B ==> B & A"
proof
assume "A & B" thus B
and then "Process whole buffer", and then complete the proof as:
theory Test
imports Main
begin
lemma "A & B ==> B & A"
proof
assume "A & B" thus B..
next
assume "A & B" thus "A" ..
qed
then I can "Process whole buffer" again and the proof is accepted. But
if I then "Retract whole buffer" and "Process whole buffer" again then
the proof is now rejected (due to the missing space between "B" and
"..").
Thanks
Ian
Email Gateway (Aug 18 2022 at 15:50):From: Ian Lynagh <igloo@earth.li>
Perhaps the question I should really have asked is:
Given a proof state of
goal (1 subgoal):
1. !!x. P (f x)
why does "fix a" not give a proof state of:
goal (1 subgoal):
1. P (f a)
?
Thanks
Ian
Email Gateway (Aug 18 2022 at 15:51):From: Makarius <makarius@sketis.net>
On Sun, 15 Aug 2010, Ian Lynagh wrote:
Some helpful tips there, although the main purpose of my mail was to try
to highlight the sorts of difficulties that beginners (well, at least
one beginner!) run into.
This is a bidirectional process: While your initial encounter with the
system helps to iron out certain issues eventually (which often takes
years), the immediate tips help you to get forward right now.
It seems that "fix a" does nothing at all, yet it can be necessary;
looks like magic to me! e.g. in this proof:theory Test
imports Main
beginlemma assumes P: "! x. P x" shows "! x. P(f x)"
proof
fix a
from P show "P(f a)" ..
qedthe "proof state" is the same before and after the "fix a" line
The Isar "context elements" 'fix' and 'assume' mainly act on the proof
context, not the goal state. In the traditional approach to tactical
theorem proving, all your information was kept in the goal state,
occasionally encoded a bit indirectly. E.g. the "premises" of a subgoal
of the form A ==> B ==> C would simulate local facts that can be used to
conclude C. In Isar, local facts are first class in the context outside
of the context.
Incidently, reducing goal states to the bare minumum also improves
performance of proof tools. Unlike other attempts at human-readable proof
scripts, Isar processing is actually faster than traditional scripting!
The main idea of the interplay of proof contexts vs. goal states is this:
* The system asks you to establish something, e.g. a sub-problem of the
form !!x. A x ==> B x
* You build up a local context and show something in it, e.g. by saying
fix x assume "A x" show "B x" <proof>
* The system composes this contextual result, typically solving one of
the pending sub-problems.
The "canonical answer" fix/assume/show above is really just an example.
There is some flexibility here. See also section "2.2.3 Structured proof
refinement" in the isar-ref manual.
You also need to keep in mind that the goal output follows more the
tactical tradition. I.e. you should not answer by show "!!x. A x ==> B x"
above, which can also lead to some surprises.
apart from the step counter being incremented, but I assume that's not
relevant), as are the "cases", "facts", and "term bindings". So how am I
meant to know whether I need to fix something, if doing so has no
visible effect?
You always need to 'fix' an entity, if it is meant to be "arbitrary, but
fixed", i.e. starting as a local constant and becoming a schematic
variable eventually (after leving the local context).
Sometimes it is convenient to experiment with undeclared free variables.
The system allows this, but uses some extra highlighting (usually yellow)
in the display. This indicates that you can never generalize such
entities (without violating the Isar structure).
I am also surprised that "facts", and perhaps also "term bindings", are
not shown by default.
The Isar proof context contains many things, and can be even arbitrarily
extended in ML user space. The default output is a bit of a mixture of
historical accidents and traditions from tactical proving (which is the
primary model of Proof General). At some point, all of this needs some
reconsideration -- I am working on it right now, after Isabelle/Isar has
been locked into Proof General / TTY interaction for more than a decade.
In this new interaction model (i.e. see my paper on UITP 2010) goal state
output actually happens to be a performance bottle-neck for the system,
not just confusing to the user. All of this needs some careful rethinking
on the system side ...
Makarius
Last updated: Nov 21 2024 at 12:39 UTC