diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/README.rst | 15 | ||||
| -rw-r--r-- | doc/sphinx/addendum/generalized-rewriting.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 23 | ||||
| -rwxr-xr-x | doc/sphinx/conf.py | 7 | ||||
| -rw-r--r-- | doc/sphinx/credits.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/index.rst | 33 | ||||
| -rw-r--r-- | doc/sphinx/introduction.rst | 9 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 83 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 270 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 15 |
10 files changed, 235 insertions, 227 deletions
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 35a605ddd..32de15ee3 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -123,11 +123,24 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the induction principles. -``.. prodn::`` :black_nib: Grammar productions. +``.. prodn::`` A grammar production. This is useful if you intend to document individual grammar productions. Otherwise, use Sphinx's `production lists <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_. + Unlike ``.. productionlist``\ s, this directive accepts notation syntax. + + + Usage:: + + .. prodn:: token += production + .. prodn:: token ::= production + + Example:: + + .. prodn:: term += let: @pattern := @term in @term + .. prodn:: occ_switch ::= { {? + %| - } {* @num } } + ``.. tacn::`` :black_nib: A tactic, or a tactic notation. Example:: diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index e10e16c10..e4d24a1f7 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -106,7 +106,7 @@ argument. Morphisms can also be contravariant in one or more of their arguments. A morphism is contravariant on an argument associated to the relation -instance :math`R` if it is covariant on the same argument when the inverse +instance :math:`R` if it is covariant on the same argument when the inverse relation :math:`R^{−1}` (``inverse R`` in Coq) is considered. The special arrow ``-->`` is used in signatures for contravariant morphisms. diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 47d3a7d7c..6a9b343ba 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -310,16 +310,15 @@ The :n:`@ident` is not relevant. It is just used for error messages. The axioms. The optional list of modifiers is used to tailor the behavior of the tactic. The following list describes their syntax and effects: -.. prodn:: - ring_mod ::= abstract %| decidable @term %| morphism @term - %| setoid @term @term - %| constants [@ltac] - %| preprocess [@ltac] - %| postprocess [@ltac] - %| power_tac @term [@ltac] - %| sign @term - %| div @term - +.. productionlist:: coq + ring_mod : abstract | decidable `term` | morphism `term` + : | setoid `term` `term` + : | constants [`ltac`] + : | preprocess [`ltac`] + : | postprocess [`ltac`] + : | power_tac `term` [`ltac`] + : | sign `term` + : | div `term` abstract declares the ring as abstract. This is the default. @@ -663,8 +662,8 @@ messages. :n:`@term` is a proof that the field signature satisfies the (semi-)field axioms. The optional list of modifiers is used to tailor the behavior of the tactic. -.. prodn:: - field_mod := @ring_mod %| completeness @term +.. productionlist:: coq + field_mod : `ring_mod` | completeness `term` Since field tactics are built upon ``ring`` tactics, all modifiers of the ``Add Ring`` apply. There is only one diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index f65400e88..8127d3df3 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -104,7 +104,6 @@ exclude_patterns = [ 'Thumbs.db', '.DS_Store', 'introduction.rst', - 'credits.rst', 'README.rst', 'README.template.rst' ] @@ -201,9 +200,9 @@ html_static_path = ['_static'] # The empty string is equivalent to '%b %d, %Y'. #html_last_updated_fmt = None -# If true, SmartyPants will be used to convert quotes and dashes to -# typographically correct entities. -html_use_smartypants = False # FIXME wrap code in <code> tags, otherwise quotesget converted in there +# FIXME: this could be re-enabled after ensuring that smart quotes are locally +# disabled for all relevant directives +smartquotes = False # Custom sidebar templates, maps document names to template names. #html_sidebars = {} diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst index a75659798..2562dec46 100644 --- a/doc/sphinx/credits.rst +++ b/doc/sphinx/credits.rst @@ -1,3 +1,8 @@ +.. include:: preamble.rst +.. include:: replaces.rst + +.. _credits: + ------------------------------------------- Credits ------------------------------------------- diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst index 136f9088b..f3ae49381 100644 --- a/doc/sphinx/index.rst +++ b/doc/sphinx/index.rst @@ -1,16 +1,31 @@ -.. _introduction: - .. include:: preamble.rst .. include:: replaces.rst .. include:: introduction.rst -.. include:: credits.rst ------------------ Table of contents ------------------ .. toctree:: + :caption: Indexes + + genindex + coq-cmdindex + coq-tacindex + coq-optindex + coq-exnindex + +.. No entries yet + * :index:`thmindex` + +.. toctree:: + :caption: Preamble + + self + credits + +.. toctree:: :caption: The language language/gallina-specification-language @@ -65,18 +80,6 @@ Table of contents zebibliography -.. toctree:: - :caption: Indexes - - genindex - coq-cmdindex - coq-tacindex - coq-optindex - coq-exnindex - -.. No entries yet - * :index:`thmindex` - This material (the Coq Reference Manual) may be distributed only subject to the terms and conditions set forth in the Open Publication License, v1.0 or later (the latest version is presently available at diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index 75ff72c4d..bc72877b6 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -1,3 +1,5 @@ +.. _introduction: + ------------------------ Introduction ------------------------ @@ -101,13 +103,6 @@ List of additional documentation This manual does not contain all the documentation the user may need about |Coq|. Various informations can be found in the following documents: -Tutorial - A companion volume to this reference manual, the |Coq| Tutorial, is - aimed at gently introducing new users to developing proofs in |Coq| - without assuming prior knowledge of type theory. In a second step, - the user can read also the tutorial on recursive types (document - `RecTutorial.ps`). - Installation A text file `INSTALL` that comes with the sources explains how to install |Coq|. diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index ff5d352c9..c21d8d4ec 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1925,74 +1925,75 @@ applied to an unknown structure instance (an implicit argument) and a value. The complete documentation of canonical structures can be found in :ref:`canonicalstructures`; here only a simple example is given. -Assume that `qualid` denotes an object ``(Build_struc`` |c_1| … |c_n| ``)`` in the -structure *struct* of which the fields are |x_1|, …, |x_n|. Assume that -`qualid` is declared as a canonical structure using the command - .. cmd:: Canonical Structure @qualid -Then, each time an equation of the form ``(``\ |x_i| ``_)`` |eq_beta_delta_iota_zeta| |c_i| has to be -solved during the type-checking process, `qualid` is used as a solution. -Otherwise said, `qualid` is canonically used to extend the field |c_i| -into a complete structure built on |c_i|. + This command declares :token:`qualid` as a canonical structure. -Canonical structures are particularly useful when mixed with coercions -and strict implicit arguments. Here is an example. + Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the + structure :g:`struct` of which the fields are |x_1|, …, |x_n|. + Then, each time an equation of the form ``(``\ |x_i| ``_)`` |eq_beta_delta_iota_zeta| |c_i| has to be + solved during the type-checking process, :token:`qualid` is used as a solution. + Otherwise said, :token:`qualid` is canonically used to extend the field |c_i| + into a complete structure built on |c_i|. -.. coqtop:: all + Canonical structures are particularly useful when mixed with coercions + and strict implicit arguments. - Require Import Relations. + .. example:: - Require Import EqNat. + Here is an example. - Set Implicit Arguments. + .. coqtop:: all - Unset Strict Implicit. + Require Import Relations. - Structure Setoid : Type := {Carrier :> Set; Equal : relation Carrier; - Prf_equiv : equivalence Carrier Equal}. + Require Import EqNat. - Definition is_law (A B:Setoid) (f:A -> B) := forall x y:A, Equal x y -> Equal (f x) (f y). + Set Implicit Arguments. - Axiom eq_nat_equiv : equivalence nat eq_nat. + Unset Strict Implicit. - Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv. + Structure Setoid : Type := {Carrier :> Set; Equal : relation Carrier; + Prf_equiv : equivalence Carrier Equal}. - Canonical Structure nat_setoid. + Definition is_law (A B:Setoid) (f:A -> B) := forall x y:A, Equal x y -> Equal (f x) (f y). -Thanks to ``nat_setoid`` declared as canonical, the implicit arguments ``A`` -and ``B`` can be synthesized in the next statement. + Axiom eq_nat_equiv : equivalence nat eq_nat. -.. coqtop:: all + Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv. - Lemma is_law_S : is_law S. + Canonical Structure nat_setoid. -Remark: If a same field occurs in several canonical structure, then -only the structure declared first as canonical is considered. + Thanks to :g:`nat_setoid` declared as canonical, the implicit arguments :g:`A` + and :g:`B` can be synthesized in the next statement. -.. cmdv:: Canonical Structure @ident := @term : @type + .. coqtop:: all -.. cmdv:: Canonical Structure @ident := @term + Lemma is_law_S : is_law S. -.. cmdv:: Canonical Structure @ident : @type := @term + .. note:: + If a same field occurs in several canonical structures, then + only the structure declared first as canonical is considered. -These are equivalent to a regular definition of `ident` followed by the declaration -``Canonical Structure`` `ident`. + .. cmdv:: Canonical Structure @ident {? : @type } := @term -See also: more examples in user contribution category (Rocq/ALGEBRA). + This is equivalent to a regular definition of :token:`ident` followed by the + declaration :n:`Canonical Structure @ident`. -Print Canonical Projections. -++++++++++++++++++++++++++++ +.. cmd:: Print Canonical Projections -This displays the list of global names that are components of some -canonical structure. For each of them, the canonical structure of -which it is a projection is indicated. For instance, the above example -gives the following output: + This displays the list of global names that are components of some + canonical structure. For each of them, the canonical structure of + which it is a projection is indicated. -.. coqtop:: all + .. example:: + + For instance, the above example gives the following output: + + .. coqtop:: all - Print Canonical Projections. + Print Canonical Projections. Implicit types of variables diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 63cd0f3ea..6fb73a030 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -37,7 +37,7 @@ bookkeeping is performed on the conclusion of the goal, using for that purpose a couple of syntactic constructions behaving similar to tacticals (and often named as such in this chapter). The ``:`` tactical moves hypotheses from the context to the conclusion, while ``=>`` moves hypotheses from the -conclusion to the context, and in moves back and forth an hypothesis from the +conclusion to the context, and ``in`` moves back and forth an hypothesis from the context to the conclusion for the time of applying an action to it. While naming hypotheses is commonly done by means of an ``as`` clause in the @@ -47,20 +47,22 @@ often followed by ``=>`` to explicitly name them. While generalizing the goal is normally not explicitly needed in Chapter :ref:`tactics`, it is an explicit operation performed by ``:``. +.. seealso:: :ref:`bookkeeping_ssr` + Beside the difference of bookkeeping model, this chapter includes specific tactics which have no explicit counterpart in Chapter :ref:`tactics` -such as tactics to mix forward steps and generalizations as generally -have or without loss. +such as tactics to mix forward steps and generalizations as +:tacn:`generally have` or :tacn:`without loss`. |SSR| adopts the point of view that rewriting, definition expansion and partial evaluation participate all to a same concept of rewriting a goal in a larger sense. As such, all these functionalities -are provided by the rewrite tactic. +are provided by the :tacn:`rewrite <rewrite (ssreflect)>` tactic. |SSR| includes a little language of patterns to select subterms in tactics or tacticals where it matters. Its most notable application is -in the rewrite tactic, where patterns are used to specify where the -rewriting step has to take place. +in the :tacn:`rewrite <rewrite (ssreflect)>` tactic, where patterns are +used to specify where the rewriting step has to take place. Finally, |SSR| supports so-called reflection steps, typically allowing to switch back and forth between the computational view and @@ -87,20 +89,24 @@ Getting started ~~~~~~~~~~~~~~~ To be available, the tactics presented in this manual need the -following minimal set of libraries to loaded: ``ssreflect.v``, +following minimal set of libraries to be loaded: ``ssreflect.v``, ``ssrfun.v`` and ``ssrbool.v``. Moreover, these tactics come with a methodology specific to the authors of |SSR| and which requires a few options to be set in a different way than in their default way. All in all, this corresponds to working in the following context: -.. coqtop:: all +.. coqtop:: in From Coq Require Import ssreflect ssrfun ssrbool. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +.. seealso:: + :opt:`Implicit Arguments`, :opt:`Strict Implicit`, + :opt:`Printing Implicit Defensive` + .. _compatibility_issues_ssr: @@ -114,14 +120,14 @@ compatible with the rest of |Coq|, up to a few discrepancies: + New keywords (``is``) might clash with variable, constant, tactic or tactical names, or with quasi-keywords in tactic or vernacular notations. -+ New tactic(al)s names (``last``, ``done``, ``have``, ``suffices``, - ``suff``, ``without loss``, ``wlog``, ``congr``, ``unlock``) ++ New tactic(al)s names (:tacn:`last`, :tacn:`done`, :tacn:`have`, :tacn:`suffices`, + :tacn:`suff`, :tacn:`without loss`, :tacn:`wlog`, :tacn:`congr`, :tacn:`unlock`) might clash with user tactic names. + Identifiers with both leading and trailing ``_``, such as ``_x_``, are reserved by |SSR| and cannot appear in scripts. -+ The extensions to the rewrite tactic are partly incompatible with those ++ The extensions to the :tacn:`rewrite` tactic are partly incompatible with those available in current versions of |Coq|; in particular: ``rewrite .. in - (type of k)`` or ``rewrite .. in *`` or any other variant of ``rewrite`` + (type of k)`` or ``rewrite .. in *`` or any other variant of :tacn:`rewrite` will not work, and the |SSR| syntax and semantics for occurrence selection and rule chaining is different. Use an explicit rewrite direction (``rewrite <- …`` or ``rewrite -> …``) to access the |Coq| rewrite tactic. @@ -139,7 +145,7 @@ compatible with the rest of |Coq|, up to a few discrepancies: Note that the full syntax of |SSR|’s rewrite and reserved identifiers are enabled only if the ssreflect module has been required and if ``SsrSyntax`` has - been imported. Thus a file that requires (without importing) ssreflect + been imported. Thus a file that requires (without importing) ``ssreflect`` and imports ``SsrSyntax``, can be required and imported without automatically enabling |SSR|’s extended rewrite syntax and reserved identifiers. @@ -148,9 +154,10 @@ compatible with the rest of |Coq|, up to a few discrepancies: such as have, set and pose. + The generalization of if statements to non-Boolean conditions is turned off by |SSR|, because it is mostly subsumed by Coercion to ``bool`` of the - ``sumXXX`` types (declared in ``ssrfun.v``) and the ``if`` *term* ``is`` *pattern* ``then`` - *term* ``else`` *term* construct (see :ref:`pattern_conditional_ssr`). To use the - generalized form, turn off the |SSR| Boolean if notation using the command: + ``sumXXX`` types (declared in ``ssrfun.v``) and the + :n:`if @term is @pattern then @term else @term` construct + (see :ref:`pattern_conditional_ssr`). To use the + generalized form, turn off the |SSR| Boolean ``if`` notation using the command: ``Close Scope boolean_if_scope``. + The following two options can be unset to disable the incompatible rewrite syntax and allow reserved identifiers to appear in scripts. @@ -191,9 +198,9 @@ construct differs from the latter in that + The pattern can be nested (deep pattern matching), in particular, this allows expression of the form: -.. coqtop:: in +.. coqdoc:: - let: exist (x, y) p_xy := Hp in … . + let: exist (x, y) p_xy := Hp in … . + The destructured constructor is explicitly given in the pattern, and is used for type inference. @@ -222,11 +229,7 @@ construct differs from the latter in that The ``let:`` construct is just (more legible) notation for the primitive -|Gallina| expression - -.. coqtop:: in - - match term with pattern => term end. +|Gallina| expression :n:`match @term with @pattern => @term end`. The |SSR| destructuring assignment supports all the dependent match annotations; the full syntax is @@ -286,28 +289,17 @@ assignment with a refutable pattern, adapted to the pure functional setting of |Gallina|, which lacks a ``Match_Failure`` exception. Like ``let:`` above, the ``if…is`` construct is just (more legible) notation -for the primitive |Gallina| expression: - -.. coqtop:: in - - match term with pattern => term | _ => term end. +for the primitive |Gallina| expression +:n:`match @term with @pattern => @term | _ => @term end`. Similarly, it will always be displayed as the expansion of this form in terms of primitive match expressions (where the default expression may be replicated). Explicit pattern testing also largely subsumes the generalization of -the if construct to all binary data types; compare: - -.. coqtop:: in - - if term is inl _ then term else term. - -and: - -.. coqtop:: in - - if term then term else term. +the ``if`` construct to all binary data types; compare +:n:`if @term is inl _ then @term else @term` and +:n:`if @term then @term else @term`. The latter appears to be marginally shorter, but it is quite ambiguous, and indeed often requires an explicit annotation @@ -434,7 +426,7 @@ a functional constant, whose implicit arguments are prenex, i.e., the first As these prenex implicit arguments are ubiquitous and have often large display strings, it is strongly recommended to change the default display settings of |Coq| so that they are not printed (except after -a ``Set Printing All command``). All |SSR| library files thus start +a ``Set Printing All`` command). All |SSR| library files thus start with the incantation .. coqtop:: all undo @@ -496,19 +488,10 @@ Definitions .. tacn:: pose :name: pose (ssreflect) -This tactic allows to add a defined constant to a proof context. -|SSR| generalizes this tactic in several ways. In particular, the -|SSR| pose tactic supports *open syntax*: the body of the -definition does not need surrounding parentheses. For instance: - -.. coqtop:: reset - - From Coq Require Import ssreflect. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. - Lemma test : True. - Proof. + This tactic allows to add a defined constant to a proof context. + |SSR| generalizes this tactic in several ways. In particular, the + |SSR| pose tactic supports *open syntax*: the body of the + definition does not need surrounding parentheses. For instance: .. coqtop:: in @@ -518,10 +501,18 @@ is a valid tactic expression. The pose tactic is also improved for the local definition of higher order terms. Local definitions of functions can use the same syntax as -global ones. For example, the tactic ``pose`` supoprts parameters: +global ones. +For example, the tactic :tacn:`pose <pose (ssreflect)>` supoprts parameters: .. example:: + .. coqtop:: reset + + From Coq Require Import ssreflect. + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. + .. coqtop:: all Lemma test : True. @@ -631,8 +622,10 @@ where: surrounding the second :token:`term` are mandatory. + In the occurrence switch :token:`occ_switch`, if the first element of the list is a natural, this element should be a number, and not an Ltac - variable. The empty list {} is not interpreted as a valid occurrence - switch. + variable. The empty list ``{}`` is not interpreted as a valid occurrence + switch, it is rather used as a flag to signal the intent of the user to + clear the name following it (see :ref:`ssr_rewrite_occ_switch` and + :ref:`introduction_ssr`) The tactic: @@ -667,7 +660,7 @@ The tactic first tries to find a subterm of the goal matching the second :token:`term` (and its type), and stops at the first subterm it finds. Then the occurrences of this subterm selected by the optional :token:`occ_switch` -are replaced by :token:`ident` and a definition ``ident := term`` +are replaced by :token:`ident` and a definition :n:`@ident := @term` is added to the context. If no :token:`occ_switch` is present, then all the occurrences are abstracted. @@ -676,20 +669,20 @@ abstracted. Matching ```````` -The matching algorithm compares a pattern ``term`` with a subterm of the +The matching algorithm compares a pattern :token:`term` with a subterm of the goal by comparing their heads and then pairwise unifying their arguments (modulo conversion). Head symbols match under the following conditions: -+ If the head of ``term`` is a constant, then it should be syntactically ++ If the head of :token:`term` is a constant, then it should be syntactically equal to the head symbol of the subterm. + If this head is a projection of a canonical structure, then canonical structure equations are used for the matching. + If the head of term is *not* a constant, the subterm should have the same structure (λ abstraction,let…in structure …). -+ If the head of ``term`` is a hole, the subterm should have at least as - many arguments as ``term``. ++ If the head of :token:`term` is a hole, the subterm should have at least as + many arguments as :token:`term`. .. example:: @@ -1082,7 +1075,7 @@ constants to the goal. Because they are tacticals, ``:`` and ``=>`` can be combined, as in -.. coqtop: in +.. coqtop:: in move: m le_n_m => p le_n_p. @@ -1147,9 +1140,7 @@ induction on the top variable ``m`` with elim=> [|m IHm] n le_n. The general form of the localization tactical in is also best -explained in terms of the goal stack: - -.. coqtop:: in +explained in terms of the goal stack:: tactic in a H1 H2 *. @@ -1212,8 +1203,8 @@ product or a ``let…in``, and performs ``hnf`` otherwise. Of course this tactic is most often used in combination with the bookkeeping tacticals (see section :ref:`introduction_ssr` and :ref:`discharge_ssr`). These -combinations mostly subsume the ``intros``, ``generalize``, ``revert``, ``rename``, -``clear`` and ``pattern`` tactics. +combinations mostly subsume the :tacn:`intros`, :tacn:`generalize`, :tacn:`revert`, :tacn:`rename`, +:tacn:`clear` and :tacn:`pattern` tactics. The case tactic @@ -1229,15 +1220,11 @@ The |SSR| case tactic has a special behavior on equalities. If the top assumption of the goal is an equality, the case tactic “destructs” it as a set of equalities between the constructor arguments of its left and right hand sides, as per the tactic injection. For example, -``case`` changes the goal - -.. coqtop:: in +``case`` changes the goal:: (x, y) = (1, 2) -> G. -into - -.. coqtop:: in +into:: x = 1 -> y = 2 -> G. @@ -1289,9 +1276,7 @@ In fact the |SSR| tactic: .. tacn:: apply :name: apply (ssreflect) -is a synonym for: - -.. coqtop:: in +is a synonym for:: intro top; first [refine top | refine (top _) | refine (top _ _) | …]; clear top. @@ -1322,18 +1307,14 @@ existential metavariables of sort Prop. Note that the last ``_`` of the tactic ``apply: (ex_intro _ (exist _ y _))`` - represents a proof that ``y < 3``. Instead of generating the goal - - .. coqtop:: in + represents a proof that ``y < 3``. Instead of generating the goal:: 0 < proj1_sig (exist (fun n : nat => n < 3) y ?Goal). the system tries to prove ``y < 3`` calling the trivial tactic. If it succeeds, let’s say because the context contains ``H : y < 3``, then the - system generates the following goal: - - .. coqtop:: in + system generates the following goal:: 0 < proj1_sig (exist (fun n => n < 3) y H). @@ -1505,7 +1486,7 @@ The abstract tactic ``````````````````` .. tacn:: abstract: {+ d_item} - :name abstract (ssreflect) + :name: abstract (ssreflect) This tactic assigns an abstract constant previously introduced with the ``[: name ]`` intro pattern (see section :ref:`introduction_ssr`). @@ -1560,7 +1541,7 @@ whose general syntax is :name: => .. prodn:: - i_item ::= @i_pattern %| @s_item %| @clear_switch %| /@term + i_item ::= @i_pattern %| @s_item %| @clear_switch %| {? %{%} } /@term .. prodn:: s_item ::= /= %| // %| //= @@ -1579,7 +1560,7 @@ variables or assumptions from the goal. An :token:`s_item` can simplify the set of subgoals or the subgoals themselves: + ``//`` removes all the “trivial” subgoals that can be resolved by the - |SSR| tactic ``done`` described in :ref:`terminators_ssr`, i.e., + |SSR| tactic :tacn:`done` described in :ref:`terminators_ssr`, i.e., it executes ``try done``. + ``/=`` simplifies the goal by performing partial evaluation, as per the tactic ``simpl`` [#5]_. @@ -1662,6 +1643,11 @@ The view is applied to the top assumption. While it is good style to use the :token:`i_item` i * to pop the variables and assumptions corresponding to each constructor, this is not enforced by |SSR|. +``/`` :token:`term` + Interprets the top of the stack with the view :token:`term`. + It is equivalent to ``move/term``. The optional flag ``{}`` can + be used to signal that the :token:`term`, when it is a context entry, + has to be cleared. ``-`` does nothing, but counts as an intro pattern. It can also be used to force the interpretation of ``[`` :token:`i_item` * ``| … |`` @@ -1737,7 +1723,7 @@ new constant as an equation. The tactic: .. coqtop:: in - move En: (size l) => n. + move En: (size l) => n. where ``l`` is a list, replaces ``size l`` by ``n`` in the goal and adds the fact ``En : size l = n`` to the context. @@ -1745,7 +1731,7 @@ This is quite different from: .. coqtop:: in - pose n := (size l). + pose n := (size l). which generates a definition ``n := (size l)``. It is not possible to generalize or rewrite such a definition; on the other hand, it is @@ -1834,7 +1820,7 @@ compact syntax: .. coqtop:: in - case: {2}_ / eqP. + case: {2}_ / eqP. where ``_`` is interpreted as ``(_ == _)`` since ``eqP T a b : reflect (a = b) (a == b)`` and reflect is a type family with @@ -1999,19 +1985,9 @@ into a closing one (similar to now). Its general syntax is: .. tacn:: by @tactic :name: by -The Ltac expression: - -.. coqtop:: in - - by [@tactic | [@tactic | …]. - -is equivalent to: - -.. coqtop:: in - - [by @tactic | by @tactic | ...]. - -and this form should be preferred to the former. +The Ltac expression :n:`by [@tactic | [@tactic | …]` is equivalent to +:n:`[by @tactic | by @tactic | ...]` and this form should be preferred +to the former. In the script provided as example in section :ref:`indentation_ssr`, the paragraph corresponding to each sub-case ends with a tactic line prefixed @@ -2021,20 +1997,13 @@ with a ``by``, like in: by apply/eqP; rewrite -dvdn1. -The by tactical is implemented using the user-defined, and extensible -done tactic. This done tactic tries to solve the current goal by some -trivial means and fails if it doesn’t succeed. Indeed, the tactic -expression: - -.. coqtop:: in - - by tactic. - -is equivalent to: +.. tacn:: done + :name: done -.. coqtop:: in - - tactic; done. +The :tacn:`by` tactical is implemented using the user-defined, and extensible +:tacn:`done` tactic. This :tacn:`done` tactic tries to solve the current goal by some +trivial means and fails if it doesn’t succeed. Indeed, the tactic +expression :n:`by @tactic` is equivalent to :n:`@tactic; done`. Conversely, the tactic @@ -2440,7 +2409,7 @@ tactic: The behavior of the defective have tactic makes it possible to generalize it in the following general construction: -.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item | {+ @binder } } {? : @term } {? := @term | by @tactic } +.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item | {+ @ssr_binder } } {? : @term } {? := @term | by @tactic } Open syntax is supported for both :token:`term`. For the description of :token:`i_item` and :token:`s_item` see section @@ -2735,7 +2704,7 @@ type classes inference. Full inference for ``ty``. The first subgoal demands a proof of such instantiated statement. -+ coqtop:: ++ .. coqdoc:: have foo : ty := . @@ -2817,21 +2786,23 @@ Another useful construct is reduction, showing that a particular case is in fact general enough to prove a general property. This kind of reasoning step usually starts with: “Without loss of generality, we can suppose that …”. Formally, this corresponds to the proof of a goal -G by introducing a cut wlog_statement -> G. Hence the user shall -provide a proof for both (wlog_statement -> G) -> G and -wlog_statement -> G. However, such cuts are usually rather +``G`` by introducing a cut ``wlog_statement -> G``. Hence the user shall +provide a proof for both ``(wlog_statement -> G) -> G`` and +``wlog_statement -> G``. However, such cuts are usually rather painful to perform by -hand, because the statement wlog_statement is tedious to write by hand, +hand, because the statement ``wlog_statement`` is tedious to write by hand, and sometimes even to read. -|SSR| implements this kind of reasoning step through the without -loss tactic, whose short name is ``wlog``. It offers support to describe +|SSR| implements this kind of reasoning step through the :tacn:`without loss` +tactic, whose short name is :tacn:`wlog`. It offers support to describe the shape of the cut statements, by providing the simplifying hypothesis and by pointing at the elements of the initial goals which should be generalized. The general syntax of without loss is: .. tacn:: wlog {? suff } {? @clear_switch } {? @i_item } : {* @ident } / @term :name: wlog +.. tacv:: without loss {? suff } {? @clear_switch } {? @i_item } : {* @ident } / @term + :name: without loss where each :token:`ident` is a constant in the context of the goal. Open syntax is supported for :token:`term`. @@ -2839,13 +2810,14 @@ of the goal. Open syntax is supported for :token:`term`. In its defective form: .. tacv:: wlog: / @term +.. tacv:: without loss: / @term on a goal G, it creates two subgoals: a first one to prove the formula (term -> G) -> G and a second one to prove the formula term -> G. -If the optional list of :token:`itent` is present +If the optional list of :token:`ident` is present on the left side of ``/``, these constants are generalized in the premise (term -> G) of the first subgoal. By default bodies of local definitions are erased. This behavior can be inhibited by prefixing the @@ -2858,9 +2830,9 @@ In the second subgoal, the tactic: move=> clear_switch i_item. is performed if at least one of these optional switches is present in -the ``wlog`` tactic. +the :tacn:`wlog` tactic. -The ``wlog`` tactic is specially useful when a symmetry argument +The :tacn:`wlog` tactic is specially useful when a symmetry argument simplifies a proof. Here is an example showing the beginning of the proof that quotient and reminder of natural number euclidean division are unique. @@ -2881,9 +2853,10 @@ are unique. wlog: q1 q2 r1 r2 / q1 <= q2. by case (le_gt_dec q1 q2)=> H; last symmetry; eauto with arith. -The ``wlog suff`` variant is simpler, since it cuts wlog_statement instead -of wlog_statement -> G. It thus opens the goals wlog_statement -> G -and wlog_statement. +The ``wlog suff`` variant is simpler, since it cuts ``wlog_statement`` instead +of ``wlog_statement -> G``. It thus opens the goals +``wlog_statement -> G`` +and ``wlog_statement``. In its simplest form the ``generally have : …`` tactic is equivalent to ``wlog suff : …`` followed by last first. When the ``have`` tactic is used @@ -2922,7 +2895,7 @@ Advanced generalization The complete syntax for the items on the left hand side of the ``/`` separator is the following one: -.. tacv wlog … : {? @clear_switch | {? @ } @ident | ( {? @ } @ident := @c_pattern) } / @term +.. tacv:: wlog … : {? @clear_switch | {? @ } @ident | ( {? @ } @ident := @c_pattern) } / @term Clear operations are intertwined with generalization operations. This helps in particular avoiding dependency issues while generalizing some @@ -3270,6 +3243,7 @@ the equality. Indeed the left hand side of ``H`` does not match the redex identified by the pattern ``x + y * 4``. +.. _ssr_rewrite_occ_switch: Occurrence switches and redex switches `````````````````````````````````````` @@ -3294,6 +3268,9 @@ the rewrite tactic. The effect of the tactic on the initial goal is to rewrite this lemma at the second occurrence of the first matching ``x + y + 0`` of the explicit rewrite redex ``_ + y + 0``. +An empty occurrence switch ``{}`` is not interpreted as a valid occurrence +switch. It has the effect of clearing the :token:`r_item` (when it is the name +of a context entry). Occurrence selection and repetition ``````````````````````````````````` @@ -3691,7 +3668,8 @@ selective rewriting, blocking on the fly the reduction in the term ``t``. .. coqtop:: reset - From Coq Require Import ssreflect ssrfun ssrbool List. + From Coq Require Import ssreflect ssrfun ssrbool. + From Coq Require Import List. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -4684,9 +4662,11 @@ Note that the goal interpretation view mechanism supports both ``apply`` and ``exact`` tactics. As expected, a goal interpretation view command exact/term should solve the current goal or it will fail. -*Warning* Goal interpretation view tactics are *not* compatible with -the bookkeeping tactical ``=>`` since this would be redundant with the -``apply: term => _`` construction. +.. warning:: + + Goal interpretation view tactics are *not* compatible with + the bookkeeping tactical ``=>`` since this would be redundant with the + ``apply: term => _`` construction. Boolean reflection @@ -5273,7 +5253,7 @@ Notation scope Module name -.. prodn:: name ::= @qualid +.. prodn:: modname ::= @qualid Natural number @@ -5283,14 +5263,10 @@ where :token:`ident` is an Ltac variable denoting a standard |Coq| numeral (should not be the name of a tactic which can be followed by a bracket ``[``, like ``do``, ``have``,…) -Pattern - -.. prodn:: pattern ::= @term - Items and switches ~~~~~~~~~~~~~~~~~~ -.. prodn:: binder ::= @ident %| ( @ident {? : @term } ) +.. prodn:: ssr_binder ::= @ident %| ( @ident {? : @term } ) binder see :ref:`abbreviations_ssr`. @@ -5314,7 +5290,7 @@ generalization item see :ref:`structure_ssr` intro pattern :ref:`introduction_ssr` -.. prodn:: i_item ::= @clear_switch %| @s_item %| @i_pattern %| / @term +.. prodn:: i_item ::= @clear_switch %| @s_item %| @i_pattern %| {? %{%} } / @term intro item see :ref:`introduction_ssr` @@ -5385,11 +5361,13 @@ case analysis see :ref:`the_defective_tactics_ssr` rewrite see :ref:`rewriting_ssr` -.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @binder } } {? : @term } := @term -.. tacv:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @binder } } : @term {? by @tactic } +.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } {? : @term } := @term +.. tacv:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } : @term {? by @tactic } .. tacn:: have suff {? @clear_switch } {? @i_pattern } {? : @term } := @term .. tacv:: have suff {? @clear_switch } {? @i_pattern } : @term {? by @tactic } .. tacv:: gen have {? @ident , } {? @i_pattern } : {+ @gen_item } / @term {? by @tactic } +.. tacv:: generally have {? @ident , } {? @i_pattern } : {+ @gen_item } / @term {? by @tactic } + :name: generally have forward chaining see :ref:`structure_ssr` @@ -5398,8 +5376,12 @@ forward chaining see :ref:`structure_ssr` specializing see :ref:`structure_ssr` -.. tacn:: suff {* @i_item } {? @i_pattern } {+ @binder } : @term {? by @tactic } +.. tacn:: suff {* @i_item } {? @i_pattern } {+ @ssr_binder } : @term {? by @tactic } + :name: suff +.. tacv:: suffices {* @i_item } {? @i_pattern } {+ @ssr_binder } : @term {? by @tactic } + :name: suffices .. tacv:: suff {? have } {? @clear_switch } {? @i_pattern } : @term {? by @tactic } +.. tacv:: suffices {? have } {? @clear_switch } {? @i_pattern } : @term {? by @tactic } backchaining see :ref:`structure_ssr` @@ -5407,7 +5389,7 @@ backchaining see :ref:`structure_ssr` local definition :ref:`definitions_ssr` -.. tacv:: pose @ident {+ @binder } := @term +.. tacv:: pose @ident {+ @ssr_binder } := @term local function definition diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 90ca0da43..d0a0d568e 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -971,7 +971,7 @@ quantification or an implication. move H0 before H. .. tacn:: rename @ident into @ident - :name: rename ... into ... + :name: rename This renames hypothesis :n:`@ident` into :n:`@ident` in the current context. The name of the hypothesis in the proof-term, however, is left unchanged. @@ -3949,9 +3949,20 @@ succeeds, and results in an error otherwise. :name: constr_eq This tactic checks whether its arguments are equal modulo alpha - conversion and casts. + conversion, casts and universe constraints. It may unify universes. .. exn:: Not equal. +.. exn:: Not equal (due to universes). + +.. tacn:: constr_eq_strict @term @term + :name: constr_eq_strict + + This tactic checks whether its arguments are equal modulo alpha + conversion, casts and universe constraints. It does not add new + constraints. + +.. exn:: Not equal. +.. exn:: Not equal (due to universes). .. tacn:: unify @term @term :name: unify |