Plans for extending Proof General support in Isabelle

These notes are based on discussions of DavidAspinall and MakariusWenzel at MKM2006.

Extending Isabelle with "Proof Obligations"

Idea:

• sorry <id> to save current state
• resume <id> to restore an earlier (or later?) saved state

This allows the interface to fill in subproofs by generating identifiers and issuing "sorry" behind the scenes. In the editor it might be displayed as a red ellipsis.

Hope: this should work cleanly on Isar because sub-proofs are really independent.

Now the record of saved states seems to become part of proof state?

Backpatching proofs

Isabelle can perhaps support a backpatch operation on proofs with embedded sorry to efficiently fill in obligations without complete replay.

On the other hand, we might want to allow replay in the interface as an alternative, so perhaps this should be configurable.

At the prover level we might only need to say whether independent nested proofs can be undone. But it seems like we should make the resume command more general, also Coq's new labelled prompt and undoto need to be encompassed in PGIP, see PGIPBasicUndoModel .

Proof construction wizards with templates/outline

Idea

• Isabelle can output templates which are filled in in the Interface.
• This would enable a more document-centred development, without auxiliary goals display that is less meaningful in Isar.

E.g. print induct displays template with sorry <id> (proof obligations) in subproofs.

So in fact we already always have complete proofs.

Idea is to have hierarchical scripts with compositional

Cf. Agda-style interface, where Emacs displays highlighted meta variables generated by the system, and queries the system for commands available for refining those variables, to synthesis terms. Emacs protocol is very simple. (Paper describing this in UITP05).

Note that there are some existing features:

• In ProofGeneralEmacs, Coq has holes mechanism added by PierreCourtieu
• In ProofGeneralEmacs, PhoX has proof-by-menu mechanism
• In ProofGeneralKit architecture, we have operations (opcmd) and types.
  • Perhaps we want a special kind of opcmd which allows for PBP-style feedback, like the "print induct" example. In this case the template text isn't hardwired and static, but can be generated dynamically by the system. See PGIPDisplayOperations for discussion.

Ideally we would like to have more kinds of holes: holes for terms, facts, etc. Maybe special identifiers here: syntactically legal but nonsense (DUMMY term, type, _/nothing fact, etc).

Of course: holes need to be marked up for interface.

Suggestion: just find these by regexps, BUT then the interface cannot know the types of the holes (unless separate regexps for each type, etc). BETTER seems if system can add PGIP markup for holes, so we can know them (and not care about their text content):

      <hole objtype="term">   </hole>

What can Proof General know about proof scripts so far?

1. block structure for Isar proofs (already in PGIPBasicUndoModel with nesting)
2. facts for chaining - where they're emitted. How might this second thing be useful? Certain inspection operations make sense when they didn't before?
3. print_theorems - prints just the additions of the last command. But also want to know about
   • types
   • constants
   • datatypes
   • facts (this)
4. we could have a command which examines arbitrary previous history of top level states

So one way to inspect the script would be for PG to issue a print_theorems (and other print_XX or inspection commands) after each command has been executed.

This seems inefficient/tedious if we do it after every command. Doing it at the end of a theory would not be so bad, but then we would not have local information during the theory.

DA: IMO it seems better if Isabelle would emit this information pro-actively (cf. theorem dependencies at the moment). There seems to be a place for adding hooks for Isabelle packages so that they can emit useful indexing information.

Parsing proof scripts, returning meta-information

We'd like to get some intentional information from commands within proof scripts, especially:

• names of identifiers that are bound
• names of identifiers that are referenced
• positions of declarations/definitions of names

Is it possible to have a lightweight execution which does not execute proofs but does calculate name bindings, etc?

Alternatively (or as an interim), we should provide this information during normal processing, when Proof General can cache it (conceptually or actually, adding it to the PGIP markup of the source text).

Perhaps the best we can do is provide approximate position information (to the start of a command) because the syntax is not known. Also binding forms can introduce zero or more identifiers at once. However, this is a restriction for simple refactorings that we want to allow, such as renaming. The editor really should have an exact location if it is going to replace identifiers.

Printing proof scripts

If we had real parse trees for Isar scripts, then we could generate, manipulate and print them to make Isar source texts.

Applications:

• Larry wants this for constructing scripts containing proofs generated automatically by resolution provers.
• Lucas wants this for proof planning. Note that the planning refinement involves a potentially expensive undo-redo cycle where we change the outline "proof sketch". Seems possible to support this wholly in the interface, though.
• David probably needs this for forms of refactoring and proof patterns (similar to Bundy/Dixon's plans to investigate planning in-the-large)

Question: how can we support this kind of thing without having canonical ways of generating texts? (Possibly: the opcmd mechanism of the interface)

Annotations in inner syntax

Would be highly desirable to have a way of passing annotations to the print engine. Annotations are typically used to refer back to abstract syntax.

Alternative/additionally: if we can manipulate that abstract syntax directly via a special "raw term" print mode parser, we may recover a robust input syntax. This could be used by the interface to construct terms to send to Isabelle, e.g. to make instantiations or to search for matching theorems. However the "raw term" mode probably wouldn't be desirable for inclusion in source scripts.

Cf Matita design for bidirectional transformations between view and source. They describe "three formats": content level [semantics], presentation level [MathML], interchange level [XML].