Download Proof General

Chapter 10: Coq Proof General
51
10 Coq Proof General
Coq Proof General is an instantiation of Proof General for the Coq proof assistant. It supports
most of the generic features of Proof General.
10.1 Coq-specific commands
Coq Proof General supplies the following key-bindings:
C-c C-a C-i
Inserts “Intros ”
C-c C-a C-a
Inserts “Apply ”
C-c C-a C-s
Inserts “Section ”
C-c C-a C-e
Inserts “End <section-name>.” (this should work well with nested sections).
C-c C-a C-o
Prompts for a SearchIsos argument.
10.2 Editing multiple proofs
Coq allows the user to enter top-level commands while editing a proof script. For example, if
the user realizes that the current proof will fail without an additional axiom, he or she can add
that axiom to the system while in the middle of the proof. Similarly, the user can nest lemmas,
beginning a new lemma while in the middle of an earlier one, and as the lemmas are proved or
their proofs aborted they are popped off a stack.
Coq Proof General supports this feature of Coq. Top-level commands entered while in a proof
are well backtracked. If new lemmas are started, Coq Proof General lets the user work on the
proof of the new lemma, and when the lemma is finished it falls back to the previous one. This
is supported to any nesting depth that Coq allows.
Warning! Using Coq commands for navigating inside the different proofs (Resume and especially
Suspend) are not supported, backtracking will break syncronization.
Special note: The old feature that moved nested proofs outside the current proof is disabled.
10.3 User-loaded tactics
Another feature that Coq allows is the extension of the grammar of the proof assistant by new
tactic commands. This feature interacts with the proof script management of Proof General,
because Proof General needs to know when a tactic is called that alters the proof state. When
the user tries to retract across an extended tactic in a script, the algorithm for calculating how
far to undo has a default behavior that is not always accurate in proof mode: do "Undo".
Coq Proof General does not currently support dynamic tactic extension in Coq: this is desirable
but requires assistance from the Coq core. Instead we provide a way to add tactic and command
names in the ‘.emacs’ file. Four Configurable variables allows to register personal new tactics
and commands into four categories:
• state changing commands, which need "Back" to be backtracked;
• state changing tactics, which need "Undo" to be backtracked;
• state preserving commands, which do not need to be backtracked;
• state preserving tactics, which do not need to be backtracked;