Re: [isabelle] Beginner's struggles
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:
lemma assumes P: "! x. P x" shows "! x. P(f x)"
from P show "P(f a)" ..
the "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
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 ...
This archive was generated by a fusion of
Pipermail (Mailman edition) and