diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 18 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 39 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 10 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 16 |
4 files changed, 50 insertions, 33 deletions
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 46851050ac..741f9fe5b0 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -144,8 +144,9 @@ list of assertion commands is given in :ref:`Assertions`. The command the proof is a subset of the declared one. The set of declared variables is closed under type dependency. For - example if ``T`` is variable and a is a variable of type ``T``, the commands - ``Proof using a`` and ``Proof using T a`` are actually equivalent. + example, if ``T`` is a variable and ``a`` is a variable of type + ``T``, then the commands ``Proof using a`` and ``Proof using T a`` + are equivalent. .. cmdv:: Proof using {+ @ident } with @tactic @@ -632,16 +633,15 @@ How to enable diffs ``````````````````` .. opt:: Diffs %( "on" %| "off" %| "removed" %) + :name: Diffs - .. This ref doesn't work: :opt:`Set Diffs %( "on" %| "off" %| "removed" %)` - - The “on” option highlights added tokens in green, while the “removed” option - additionally reprints items with removed tokens in red. Unchanged tokens in - modified items are shown with pale green or red. (Colors are user-configurable.) + The “on” option highlights added tokens in green, while the “removed” option + additionally reprints items with removed tokens in red. Unchanged tokens in + modified items are shown with pale green or red. (Colors are user-configurable.) For coqtop, showing diffs can be enabled when starting coqtop with the -``-diffs on|off|removed`` command-line option or with the ``Set Diffs`` -command within Coq. You will need to provide the ``-color on|auto`` command-line option when +``-diffs on|off|removed`` command-line option or by setting the :opt:`Diffs` option +within Coq. You will need to provide the ``-color on|auto`` command-line option when you start coqtop in either case. Colors for coqtop can be configured by setting the ``COQ_COLORS`` environment diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 52609546d5..3ca0ffe678 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -916,11 +916,8 @@ but also folds ``x`` in the goal. .. coqtop:: reset From Coq Require Import ssreflect. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. - .. coqtop:: all undo + .. coqtop:: all Lemma test x t (Hx : x = 3) : x + t = 4. set z := 3 in Hx. @@ -929,6 +926,10 @@ If the localization also mentions the goal, then the result is the following one .. example:: + .. coqtop:: reset + + From Coq Require Import ssreflect. + .. coqtop:: all Lemma test x t (Hx : x = 3) : x + t = 4. @@ -2485,8 +2486,7 @@ destruction of existential assumptions like in the tactic: .. coqtop:: all Lemma test : True. - have [x Px]: exists x : nat, x > 0. - Focus 2. + have [x Px]: exists x : nat, x > 0; last first. An alternative use of the ``have`` tactic is to provide the explicit proof term for the intermediate lemma, using tactics of the form: @@ -2564,8 +2564,7 @@ copying the goal itself. .. coqtop:: all Lemma test : True. - have suff H : 2 + 2 = 3. - Focus 2. + have suff H : 2 + 2 = 3; last first. Note that H is introduced in the second goal. @@ -2852,8 +2851,7 @@ pattern will be used to process its instance. .. coqtop:: all Lemma simple n (ngt0 : 0 < n ) : P n. - gen have ltnV, /andP[nge0 neq0] : n ngt0 / (0 <= n) && (n != 0). - Focus 2. + gen have ltnV, /andP[nge0 neq0] : n ngt0 / (0 <= n) && (n != 0); last first. .. _advanced_generalization_ssr: @@ -3556,6 +3554,7 @@ corresponding new goals will be generated. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. + Set Warnings "-notation-overridden". .. coqtop:: all @@ -3756,9 +3755,10 @@ which the function is supplied: :name: congr This tactic: -+ checks that the goal is a Leibniz equality -+ matches both sides of this equality with “term applied to some arguments”, inferring the right number of arguments from the goal and the type of term. This may expand some definitions or fixpoints. -+ generates the subgoals corresponding to pairwise equalities of the arguments present in the goal. + + + checks that the goal is a Leibniz equality; + + matches both sides of this equality with “term applied to some arguments”, inferring the right number of arguments from the goal and the type of term. This may expand some definitions or fixpoints; + + generates the subgoals corresponding to pairwise equalities of the arguments present in the goal. The goal can be a non dependent product ``P -> Q``. In that case, the system asserts the equation ``P = Q``, uses it to solve the goal, and @@ -4918,7 +4918,7 @@ which produces the converse implication. In both cases, the two first Prop arguments are implicit. If ``term`` is an instance of the ``reflect`` predicate, then ``A`` will be one -of the defined view hints for the ``reflec``t predicate, which are by +of the defined view hints for the ``reflect`` predicate, which are by default the ones present in the file ``ssrbool.v``. These hints are not only used for choosing the appropriate direction of the translation, but they also allow complex transformation, involving negations. @@ -4933,9 +4933,9 @@ but they also allow complex transformation, involving negations. Unset Printing Implicit Defensive. Section Test. - .. coqtop:: in + .. coqtop:: all - Lemma introN : forall (P : Prop) (b : bool), reflect P b -> ~ P -> ~~b. + Check introN. .. coqtop:: all @@ -4945,12 +4945,11 @@ but they also allow complex transformation, involving negations. In fact this last script does not exactly use the hint ``introN``, but the more general hint: - .. coqtop:: in + .. coqtop:: all - Lemma introNTF : forall (P : Prop) (b c : bool), - reflect P b -> (if c then ~ P else P) -> ~~ b = c. + Check introNTF. - The lemma ` `introN`` is an instantiation of introNF using c := true. + The lemma ``introN`` is an instantiation of ``introNF`` using ``c := true``. Note that views, being part of :token:`i_pattern`, can be used to interpret assertions too. For example the following script asserts ``a && b`` but diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index db9f04ba11..26f4ec6242 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -103,7 +103,7 @@ bindings_list`` where ``bindings_list`` may be of two different forms: .. exn:: Not the right number of missing arguments. -.. _occurencessets: +.. _occurrencessets: Occurrence sets and occurrence clauses ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1024,7 +1024,7 @@ Managing the local context This notation allows specifying which occurrences of :token:`term` have to be substituted in the context. The :n:`in @goal_occurrences` clause is an occurrence clause whose syntax and behavior are described in - :ref:`goal occurences <occurencessets>`. + :ref:`goal occurrences <occurrencessets>`. .. tacv:: set (@ident @binders := @term) {? in @goal_occurrences } @@ -1509,7 +1509,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) This syntax is used for selecting which occurrences of :token:`term` the case analysis has to be done on. The :n:`in @goal_occurrences` clause is an occurrence clause whose syntax and behavior is described - in :ref:`occurences sets <occurencessets>`. + in :ref:`occurrences sets <occurrencessets>`. .. tacv:: destruct @term {? with @bindings_list } {? as @disj_conj_intro_pattern } {? eqn:@naming_intro_pattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences } edestruct @term {? with @bindings_list } {? as @disj_conj_intro_pattern } {? eqn:@naming_intro_pattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences } @@ -1659,7 +1659,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) This syntax is used for selecting which occurrences of :n:`@term` the induction has to be carried on. The :n:`in @goal_occurrences` clause is an occurrence clause whose syntax and behavior is described in - :ref:`occurences sets <occurencessets>`. If variables or hypotheses not + :ref:`occurrences sets <occurrencessets>`. If variables or hypotheses not mentioning :n:`@term` in their type are listed in :n:`@goal_occurrences`, those are generalized as well in the statement to prove. @@ -3513,6 +3513,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is Info 1 auto with eqdec. .. cmdv:: Hint Cut @regexp + :name: Hint Cut .. warning:: @@ -3546,6 +3547,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is initial cut expression being `emp`. .. cmdv:: Hint Mode @qualid {* (+ | ! | -)} + :name: Hint Mode This sets an optional mode of use of the identifier :n:`@qualid`. When proof-search faces a goal that ends in an application of :n:`@qualid` to diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index be65ff7570..a69cf209c7 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -461,6 +461,7 @@ Requests to the environment .. note:: .. table:: Search Blacklist @string + :name: Search Blacklist Specifies a set of strings used to exclude lemmas from the results of :cmd:`Search`, :cmd:`SearchHead`, :cmd:`SearchPattern` and :cmd:`SearchRewrite` queries. A lemma whose @@ -1200,3 +1201,18 @@ scope of their effect. There are four kinds of commands: modifier extends the effect outside the module even when the command occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this category. + +.. _exposing-constants-to-ocaml-libraries: + +Exposing constants to OCaml libraries +---------------------------------------------------------------- + +.. cmd:: Register @qualid__1 as @qualid__2 + + This command exposes the constant :n:`@qualid__1` to OCaml libraries under + the name :n:`@qualid__2`. This constant can then be dynamically located + calling :n:`Coqlib.lib_ref "@qualid__2"`; i.e., there is no need to known + where is the constant defined (file, module, library, etc.). + + Due to its internal nature, this command is not for general use. It is meant + to appear only in standard libraries and in support libraries of plug-ins. |