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:

   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

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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.