Consider an interactive proof tactic

[atomb]

I'm starting to think that an interactive proof tactic, interactive :: ProofScript, that would allow the user to view the current goal, apply rewrites, and so on, could be relatively easy to implement and very convenient for quicker iteration on large proofs that involve substantial rewriting.

Writing a function of that type that prompted for user input and then ran existing proof tactics based on it would probably be pretty easy. The key question is what sort of input it would accept. The options that occur to me are:

• Some very limited input in simplified syntax that was sufficient to describe invocation of existing proof tactics on already-bound variables or constants. This would probably be very easy to implement at the cost of less flexibility and the need for users to learn another (simple) syntax.
• Full support for arbitrary SAWScript expressions in the ProofScript monad. This could be more complex to implement, as we'd have to invoke the SAWScript type checker and interpreter recursively, but would be flexible and familiar. And it may turn out that it would actually be pretty easy.

[msaaltink]

This would be a very nice thing to have.

[msaaltink]

A very useful feature would be to have the memoization table (that establishes the list of let-bound variables in the printed goal formula) persist (and be augmented, I suppose) between operations on the goal. It can be irritating to have figured out what the important x@ names are in order to read and understand the goal, only to have all the names change if you apply some new rewrite rule or unfold a function. Persistent names would make it a lot easier to track how various proof steps are affecting the goal.

[robdockins]

The proof_subshell command added in #1689 is a major step in this direction.

I think the memo table idea @msaaltink mentions is also a very useful idea, especially if the user can rename parts to given them more useful names. Even more important, I think, is to allow the user some way to refer to those names; right now it is very annoying that you cannot refer to intermediate values in a proof step, even though the pretty-printer is showing you the intermediate structure you want to manipulate.