diff options
Diffstat (limited to 'doc/sphinx/proof-engine/proof-handling.rst')
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 38 |
1 files changed, 16 insertions, 22 deletions
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index c28e85171..a77b127eb 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -20,20 +20,18 @@ 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 called the *local -context* of the goal. Initially, the local context contains the local -variables and hypotheses of the current section (see Section :ref:`TODO_gallina_assumptions`) -and the local variables and hypotheses of the theorem statement. It is -enriched by the use of certain tactics (see e.g. ``intro`` in Section -:ref:`managingthelocalcontext`). +To each subgoal is associated a number of hypotheses called the *local context* +of the goal. Initially, the local context contains the local variables and +hypotheses of the current section (see Section :ref:`gallina-assumptions`) and +the local variables and hypotheses of the theorem statement. It is enriched by +the use of certain tactics (see e.g. :tacn:`intro`). When a proof is completed, the message ``Proof completed`` is displayed. One can then register this proof as a defined constant in the environment. Because there exists a correspondence between proofs and -terms of λ-calculus, known as the *Curry-Howard isomorphism* [[How80]_, -[Bar81]_, [Gir89]_, [Hue88]_ ], |Coq| -stores proofs as terms of |Cic|. Those terms -are called *proof terms*. +terms of λ-calculus, known as the *Curry-Howard isomorphism* +:cite:`How80,Bar81,Gir89,Hue88`, |Coq| stores proofs as terms of |Cic|. Those +terms are called *proof terms*. .. exn:: No focused proof @@ -46,13 +44,10 @@ out of the proof editing mode. Switching on/off the proof editing mode ------------------------------------------- -The proof editing mode is entered by asserting a statement, which -typically is the assertion of a theorem: - -.. cmd:: Theorem @ident [@binders] : @form. - -The list of assertion commands is given in Section :ref:TODO-assertions_and_proof`. The -command ``Goal`` can also be used. +The proof editing mode is entered by asserting a statement, which typically is +the assertion of a theorem using an assertion command like :cmd:`Theorem`. The +list of assertion commands is given in Section :ref:`Assertions`. The command +:cmd:`Goal` can also be used. .. cmd:: Goal @form. @@ -95,14 +90,13 @@ Forces the name of the original goal to be :n:`@ident`. This command (and the following ones) can only be used if the original goal has been opened using the ``Goal`` command. - .. cmd:: Admitted. This command is available in interactive editing proof mode to give up the current proof and declare the initial goal as an axiom. - .. cmd:: Proof @term. + :name: Proof `term` This command applies in proof editing mode. It is equivalent to @@ -127,7 +121,7 @@ See also: ``Proof with tactic.`` in Section .. cmd:: Proof using @ident1 ... @identn. This command applies in proof editing mode. It declares the set of -section variables (see :ref:`TODO-gallina-assumptions`) used by the proof. At ``Qed`` time, the +section variables (see :ref:`gallina-assumptions`) used by the proof. At ``Qed`` time, the system will assert that the set of section variables actually used in the proof is a subset of the declared one. @@ -354,10 +348,10 @@ Error messages: You are trying to use ``}`` but the current subproof has not been fully solved. .. exn:: No such goal + :name: No such goal (focusing) .. exn:: Brackets only support the single numbered goal selector - See also error messages about bullets below. .. _bullets: @@ -597,4 +591,4 @@ the ongoing proof. This command forces the |OCaml| runtime to perform a heap compaction. This is in general an expensive operation. See: `OCaml Gc <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_ -There is also an analogous tactic ``optimize_heap`` (see~:ref:`tactic-optimizeheap`) +There is also an analogous tactic :tac:`optimize_heap`. |