diff options
author | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-11 17:35:41 +0200 |
---|---|---|
committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-14 14:11:58 +0200 |
commit | d5a352faa11576d2eda294ca6872d543b0e695da (patch) | |
tree | 78a26d9118254383c995ce987846a0f53e422b6d /doc | |
parent | 9e3989f949c1e3f20031d9af5a7bc89d97f5a951 (diff) |
Remove duplicate entries for Proof, Qed, Defined, Admitted.
And marginal improvements in the last section of the Gallina chapter.
Diffstat (limited to 'doc')
-rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 92 | ||||
-rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 10 |
2 files changed, 43 insertions, 59 deletions
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 39735a6ed..aa41f8058 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1245,37 +1245,37 @@ inhabitant of the type) is interactively built using tactics. The interactive proof mode is described in Chapter :ref:`proofhandling` and the tactics in Chapter :ref:`Tactics`. The basic assertion command is: -.. cmd:: Theorem @ident : @type +.. cmd:: Theorem @ident {? @binders } : @type -After the statement is asserted, Coq needs a proof. Once a proof of -:token:`type` under the assumptions represented by :token:`binders` is given and -validated, the proof is generalized into a proof of forall , :token:`type` and -the theorem is bound to the name :token:`ident` in the environment. + After the statement is asserted, Coq needs a proof. Once a proof of + :token:`type` under the assumptions represented by :token:`binders` is given and + validated, the proof is generalized into a proof of :n:`forall @binders, @type` and + the theorem is bound to the name :token:`ident` in the environment. -.. exn:: The term @term has type @type which should be Set, Prop or Type. + .. exn:: The term @term has type @type which should be Set, Prop or Type. -.. exn:: @ident already exists. - :name: @ident already exists. (Theorem) + .. exn:: @ident already exists. + :name: @ident already exists. (Theorem) - The name you provided is already defined. You have then to choose - another name. + The name you provided is already defined. You have then to choose + another name. -.. cmdv:: Lemma @ident : @type - :name: Lemma + The following commands are synonyms of :n:`Theorem @ident {? @binders } : type`: -.. cmdv:: Remark @ident : @type - :name: Remark + .. cmdv:: Lemma @ident {? @binders } : @type + :name: Lemma -.. cmdv:: Fact @ident : @type - :name: Fact + .. cmdv:: Remark @ident {? @binders } : @type + :name: Remark -.. cmdv:: Corollary @ident : @type - :name: Corollary + .. cmdv:: Fact @ident {? @binders } : @type + :name: Fact -.. cmdv:: Proposition @ident : @type - :name: Proposition + .. cmdv:: Corollary @ident {? @binders } : @type + :name: Corollary - These commands are synonyms of ``Theorem`` :token:`ident` : :token:`type`. + .. cmdv:: Proposition @ident {? @binders } : @type + :name: Proposition .. cmdv:: Theorem @ident : @type {* with @ident : @type} @@ -1302,13 +1302,13 @@ the theorem is bound to the name :token:`ident` in the environment. .. cmdv:: Definition @ident : @type This allows defining a term of type :token:`type` using the proof editing - mode. It behaves as Theorem but is intended to be used in conjunction with + mode. It behaves as :cmd:`Theorem` but is intended to be used in conjunction with :cmd:`Defined` in order to define a constant of which the computational behavior is relevant. The command can be used also with :cmd:`Example` instead of :cmd:`Definition`. - See also :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`. + .. seealso:: :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`. .. cmdv:: Let @ident : @type @@ -1328,21 +1328,14 @@ the theorem is bound to the name :token:`ident` in the environment. This generalizes the syntax of CoFixpoint so that one or more bodies can be defined interactively using the proof editing mode. -.. cmd:: Proof - - A proof starts by the keyword Proof. Then Coq enters the proof editing mode - until the proof is completed. The proof editing mode essentially contains - tactics that are described in chapter :ref:`Tactics`. Besides tactics, there - are commands to manage the proof editing mode. They are described in Chapter - :ref:`proofhandling`. - -.. cmd:: Qed - - When the proof is completed it should be validated and put in the environment - using the keyword Qed. +A proof starts by the keyword :cmd:`Proof`. Then Coq enters the proof editing mode +until the proof is completed. The proof editing mode essentially contains +tactics that are described in chapter :ref:`Tactics`. Besides tactics, there +are commands to manage the proof editing mode. They are described in Chapter +:ref:`proofhandling`. -.. exn:: @ident already exists. - :name: @ident already exists. (Qed) +When the proof is completed it should be validated and put in the environment +using the keyword :cmd:`Qed`. .. note:: @@ -1351,28 +1344,19 @@ the theorem is bound to the name :token:`ident` in the environment. #. Not only other assertions but any vernacular command can be given while in the process of proving a given assertion. In this case, the command is understood as if it would have been given before the - statements still to be proved. - - #. Proof is recommended but can currently be omitted. On the opposite - side, Qed (or Defined, see below) is mandatory to validate a proof. + statements still to be proved. Nonetheless, this practice is discouraged + and may stop working in future versions. - #. Proofs ended by Qed are declared opaque. Their content cannot be + #. Proofs ended by :cmd:`Qed` are declared opaque. Their content cannot be unfolded (see :ref:`performingcomputations`), thus realizing some form of *proof-irrelevance*. To be able to unfold a - proof, the proof should be ended by Defined (see below). - -.. cmdv:: Defined - :name: Defined - - Same as :cmd:`Qed` but the proof is then declared transparent, which means - that its content can be explicitly used for type-checking and that it can be - unfolded in conversion tactics (see :ref:`performingcomputations`, - :cmd:`Opaque`, :cmd:`Transparent`). + proof, the proof should be ended by :cmd:`Defined`. -.. cmdv:: Admitted - :name: Admitted + #. :cmd:`Proof` is recommended but can currently be omitted. On the opposite + side, :cmd:`Qed` (or :cmd:`Defined`) is mandatory to validate a proof. - Turns the current asserted statement into an axiom and exits the proof mode. + #. One can also use :cmd:`Admitted` in place of :cmd:`Qed` to turn the + current asserted statement into an axiom and exit the proof editing mode. .. [1] This is similar to the expression “*entry* :math:`\{` sep *entry* diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 069cf8a6d..892ddbc16 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -60,7 +60,6 @@ list of assertion commands is given in :ref:`Assertions`. The command used for another statement). .. cmd:: Qed - :name: Qed (interactive proof) This command is available in interactive editing proof mode when the proof is completed. Then :cmd:`Qed` extracts a proof term from the proof @@ -82,9 +81,12 @@ list of assertion commands is given in :ref:`Assertions`. The command even incur a memory overflow. .. cmdv:: Defined - :name: Defined (interactive proof) + :name: Defined - Defines the proved term as a transparent constant. + Same as :cmd:`Qed` but the proof is then declared transparent, which means + that its content can be explicitly used for type-checking and that it can be + unfolded in conversion tactics (see :ref:`performingcomputations`, + :cmd:`Opaque`, :cmd:`Transparent`). .. cmdv:: Save @ident :name: Save @@ -94,7 +96,6 @@ list of assertion commands is given in :ref:`Assertions`. The command has been opened using the :cmd:`Goal` command. .. cmd:: Admitted - :name: Admitted (interactive proof) This command is available in interactive editing mode to give up the current proof and declare the initial goal as an axiom. @@ -125,7 +126,6 @@ list of assertion commands is given in :ref:`Assertions`. The command proof term (see Section :ref:`applyingtheorems`). .. cmd:: Proof - :name: Proof (interactive proof) Is a no-op which is useful to delimit the sequence of tactic commands which start a proof, after a :cmd:`Theorem` command. It is a good practice to |