Chapter 6: Proof handling
In Coq's proof editing mode all top-level commands documented in chapter 5 remain available and the user has access to specialized commands dealing with proof development pragmas documented in this section. He can also use some other specialized commands called tactics. They are the very tools allowing the user to deal with logical reasoning. They are documented in chapter 7.When switching in editing proof mode, the prompt Coq < is changed into ident < where ident is the declared name of the theorem currently edited.
At each stage of a proof development, one has a list of goals to prove. Initially, the list consists only in the theorem itself. After having applied some tactics, the list of goals contains the subgoals generated by the tactics.
To each subgoal is associated a number of hypotheses we call the local context of the goal. Initially, the local context is empty. It is enriched by the use of certain tactics (see mainly section 7.3.3).
When a proof is achieved the message Subtree proved! is displayed. One can then store this proof as a defined constant in the environment. Because there exists a correspondence between proofs and terms of l-calculus, known as the Curry-Howard isomorphism [54, 5, 51, 56], Coq stores proofs as terms of Cic. Those terms are called proof terms.
It is possible to edit several proofs at the same time: see section 6.1.7
Error message: When one attempts to use a proof editing command out of the proof editing mode, Coq raises the error message : No focused proof.
- 6.1 Switching on/off the proof editing mode
- 6.2 Navigation in the proof tree
- 6.3 Displaying information