diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/README.rst | 26 | ||||
| -rw-r--r-- | doc/sphinx/README.template.rst | 11 | ||||
| -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 | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/coq-library.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 123 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 1076 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 14 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 270 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 59 |
15 files changed, 846 insertions, 809 deletions
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 3036fac815..32de15ee31 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -32,7 +32,16 @@ Names (link targets) are auto-generated for most simple objects, though they can - Vernacs (commands) have their name set to the first word of their signature. For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```. - Vernac variants, tactic notations, and tactic variants do not have a default name. -Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms). Undocumented objects should have the `:undocumented:` flag instead, as shown above. +Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms). Undocumented objects should have the `:undocumented:` flag instead, as shown above. When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects):: + + .. cmdv:: Lemma @ident {? @binders} : @type + Remark @ident {? @binders} : @type + Fact @ident {? @binders} : @type + Corollary @ident {? @binders} : @type + Proposition @ident {? @binders} : @type + :name: Lemma; Remark; Fact; Corollary; Proposition + + These commands are all synonyms of :n:`Theorem @ident {? @binders } : type`. Notations --------- @@ -114,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/README.template.rst b/doc/sphinx/README.template.rst index f90efa9958..f1d2541eb6 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -32,7 +32,16 @@ Names (link targets) are auto-generated for most simple objects, though they can - Vernacs (commands) have their name set to the first word of their signature. For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```. - Vernac variants, tactic notations, and tactic variants do not have a default name. -Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms). Undocumented objects should have the `:undocumented:` flag instead, as shown above. +Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms). Undocumented objects should have the `:undocumented:` flag instead, as shown above. When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects):: + + .. cmdv:: Lemma @ident {? @binders} : @type + Remark @ident {? @binders} : @type + Fact @ident {? @binders} : @type + Corollary @ident {? @binders} : @type + Proposition @ident {? @binders} : @type + :name: Lemma; Remark; Fact; Corollary; Proposition + + These commands are all synonyms of :n:`Theorem @ident {? @binders } : type`. Notations --------- diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index e10e16c107..e4d24a1f7e 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 47d3a7d7cd..6a9b343ba8 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 f65400e88c..8127d3df3f 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 a756597986..2562dec468 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 136f9088b1..f3ae493817 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 75ff72c4da..20e4069f45 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -1,3 +1,5 @@ +.. _introduction: + ------------------------ Introduction ------------------------ diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 6af6e78972..afb49413dd 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -200,6 +200,8 @@ The following abbreviations are allowed: The type annotation ``:A`` can be omitted when ``A`` can be synthesized by the system. +.. _coq-equality: + Equality ++++++++ diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 53b993eddc..c21d8d4ec8 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -13,42 +13,37 @@ Extensions of |Gallina| Record types ---------------- -The ``Record`` construction is a macro allowing the definition of +The :cmd:`Record` construction is a macro allowing the definition of records as is done in many programming languages. Its syntax is -described in the grammar below. In fact, the ``Record`` macro is more general +described in the grammar below. In fact, the :cmd:`Record` macro is more general than the usual record types, since it allows also for “manifest” -expressions. In this sense, the ``Record`` construction allows defining +expressions. In this sense, the :cmd:`Record` construction allows defining “signatures”. .. _record_grammar: .. productionlist:: `sentence` - record : `record_keyword` ident [binders] [: sort] := [ident] { [`field` ; … ; `field`] }. + record : `record_keyword` `ident` [ `binders` ] [: `sort` ] := [ `ident` ] { [ `field` ; … ; `field` ] }. record_keyword : Record | Inductive | CoInductive - field : name [binders] : type [ where notation ] - : | name [binders] [: term] := term + field : `ident` [ `binders` ] : `type` [ where `notation` ] + : | `ident` [ `binders` ] [: `type` ] := `term` In the expression: -.. cmd:: Record @ident {* @param } {? : @sort} := {? @ident} { {*; @ident {* @binder } : @term } } +.. cmd:: Record @ident @binders {? : @sort} := {? @ident} { {*; @ident @binders : @type } } -the first identifier `ident` is the name of the defined record and `sort` is its +the first identifier :token:`ident` is the name of the defined record and :token:`sort` is its type. The optional identifier following ``:=`` is the name of its constructor. If it is omitted, -the default name ``Build_``\ `ident`, where `ident` is the record name, is used. If `sort` is +the default name ``Build_``\ :token:`ident`, where :token:`ident` is the record name, is used. If :token:`sort` is omitted, the default sort is `\Type`. The identifiers inside the brackets are the names of -fields. For a given field `ident`, its type is :g:`forall binder …, term`. +fields. For a given field :token:`ident`, its type is :g:`forall binders, type`. Remark that the type of a particular identifier may depend on a previously-given identifier. Thus the -order of the fields is important. Finally, each `param` is a parameter of the record. +order of the fields is important. Finally, :token:`binders` are parameters of the record. More generally, a record may have explicitly defined (a.k.a. manifest) fields. For instance, we might have: - -.. coqtop:: in - - Record ident param : sort := { ident₁ : type₁ ; ident₂ := term₂ ; ident₃ : type₃ }. - -in which case the correctness of |type_3| may rely on the instance |term_2| of |ident_2| and |term_2| in turn -may depend on |ident_1|. +:n:`Record @ident @binders : @sort := { @ident₁ : @type₁ ; @ident₂ := @term₂ ; @ident₃ : @type₃ }`. +in which case the correctness of :n:`@type₃` may rely on the instance :n:`@term₂` of :n:`@ident₂` and :n:`@term₂` may in turn depend on :n:`@ident₁`. .. example:: @@ -69,11 +64,10 @@ depends on both ``top`` and ``bottom``. Let us now see the work done by the ``Record`` macro. First the macro generates a variant type definition with just one constructor: +:n:`Variant @ident {? @binders } : @sort := @ident₀ {? @binders }`. -.. cmd:: Variant @ident {* @params} : @sort := @ident {* (@ident : @term_1)} - -To build an object of type `ident`, one should provide the constructor -|ident_0| with the appropriate number of terms filling the fields of the record. +To build an object of type :n:`@ident`, one should provide the constructor +:n:`@ident₀` with the appropriate number of terms filling the fields of the record. .. example:: Let us define the rational :math:`1/2`: @@ -379,6 +373,7 @@ we have the following equivalence Notice that the printing uses the :g:`if` syntax because `sumbool` is declared as such (see :ref:`controlling-match-pp`). +.. _irrefutable-patterns: Irrefutable patterns: the destructuring let variants ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1930,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 @@ -2245,6 +2241,7 @@ This option (off by default) activates the full display of how the context of an existential variable is instantiated at each of the occurrences of the existential variable. +.. _tactics-in-terms: Solving existential variables using tactics ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 76a016ff64..c26ae2a93b 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -48,26 +48,26 @@ Blanks Comments Comments in Coq are enclosed between ``(*`` and ``*)``, and can be nested. - They can contain any character. However, string literals must be + They can contain any character. However, :token:`string` literals must be correctly closed. Comments are treated as blanks. Identifiers and access identifiers - Identifiers, written ident, are sequences of letters, digits, ``_`` and + Identifiers, written :token:`ident`, are sequences of letters, digits, ``_`` and ``'``, that do not start with a digit or ``'``. That is, they are recognized by the following lexical class: .. productionlist:: coq first_letter : a..z ∣ A..Z ∣ _ ∣ unicode-letter subsequent_letter : a..z ∣ A..Z ∣ 0..9 ∣ _ ∣ ' ∣ unicode-letter ∣ unicode-id-part - ident : `first_letter` [`subsequent_letter` … `subsequent_letter`] - access_ident : . `ident` + ident : `first_letter`[`subsequent_letter`…`subsequent_letter`] + access_ident : .`ident` - All characters are meaningful. In particular, identifiers are case- - sensitive. The entry ``unicode-letter`` non-exhaustively includes Latin, + All characters are meaningful. In particular, identifiers are case-sensitive. + The entry ``unicode-letter`` non-exhaustively includes Latin, Greek, Gothic, Cyrillic, Arabic, Hebrew, Georgian, Hangul, Hiragana and Katakana characters, CJK ideographs, mathematical letter-like - symbols, hyphens, non-breaking space, … The entry ``unicode-id-part`` non- - exhaustively includes symbols for prime letters and subscripts. + symbols, hyphens, non-breaking space, … The entry ``unicode-id-part`` + non-exhaustively includes symbols for prime letters and subscripts. Access identifiers, written :token:`access_ident`, are identifiers prefixed by `.` (dot) without blank. They are used in the syntax of qualified @@ -79,8 +79,8 @@ Natural numbers and integers .. productionlist:: coq digit : 0..9 - num : `digit` … `digit` - integer : [-] `num` + num : `digit`…`digit` + integer : [-]`num` Strings Strings are delimited by ``"`` (double quote), and enclose a sequence of @@ -139,14 +139,14 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. : | `term` <: `term` : | `term` :> : | `term` -> `term` - : | `term` arg … arg + : | `term` `arg` … `arg` : | @ `qualid` [`term` … `term`] : | `term` % `ident` : | match `match_item` , … , `match_item` [`return_type`] with : [[|] `equation` | … | `equation`] end : | `qualid` : | `sort` - : | num + : | `num` : | _ : | ( `term` ) arg : `term` @@ -155,6 +155,7 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. binder : `name` : | ( `name` … `name` : `term` ) : | ( `name` [: `term`] := `term` ) + : | ' `pattern` name : `ident` | _ qualid : `ident` | `qualid` `access_ident` sort : Prop | Set | Type @@ -162,7 +163,7 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. : | `fix_body` with `fix_body` with … with `fix_body` for `ident` cofix_bodies : `cofix_body` : | `cofix_body` with `cofix_body` with … with `cofix_body` for `ident` - fix_body : `ident` `binders` [annotation] [: `term`] := `term` + fix_body : `ident` `binders` [`annotation`] [: `term`] := `term` cofix_body : `ident` [`binders`] [: `term`] := `term` annotation : { struct `ident` } match_item : `term` [as `name`] [in `qualid` [`pattern` … `pattern`]] @@ -176,7 +177,7 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. : | `pattern` % `ident` : | `qualid` : | _ - : | num + : | `num` : | ( `or_pattern` , … , `or_pattern` ) or_pattern : `pattern` | … | `pattern` @@ -185,7 +186,7 @@ Types ----- Coq terms are typed. Coq types are recognized by the same syntactic -class as :token`term`. We denote by :token:`type` the semantic subclass +class as :token:`term`. We denote by :production:`type` the semantic subclass of types inside the syntactic class :token:`term`. .. _gallina-identifiers: @@ -197,8 +198,8 @@ Qualified identifiers and simple identifiers (definitions, lemmas, theorems, remarks or facts), *global variables* (parameters or axioms), *inductive types* or *constructors of inductive types*. *Simple identifiers* (or shortly :token:`ident`) are a syntactic subset -of qualified identifiers. Identifiers may also denote local *variables*, -what qualified identifiers do not. +of qualified identifiers. Identifiers may also denote *local variables*, +while qualified identifiers do not. Numerals -------- @@ -211,7 +212,7 @@ numbers (see :ref:`datatypes`). .. note:: - negative integers are not at the same level as :token:`num`, for this + Negative integers are not at the same level as :token:`num`, for this would make precedence unnatural. Sorts @@ -220,12 +221,12 @@ Sorts There are three sorts :g:`Set`, :g:`Prop` and :g:`Type`. - :g:`Prop` is the universe of *logical propositions*. The logical propositions - themselves are typing the proofs. We denote propositions by *form*. + themselves are typing the proofs. We denote propositions by :production:`form`. This constitutes a semantic subclass of the syntactic class :token:`term`. - :g:`Set` is is the universe of *program types* or *specifications*. The specifications themselves are typing the programs. We denote - specifications by *specif*. This constitutes a semantic subclass of + specifications by :production:`specif`. This constitutes a semantic subclass of the syntactic class :token:`term`. - :g:`Type` is the type of :g:`Prop` and :g:`Set` @@ -241,18 +242,18 @@ Various constructions such as :g:`fun`, :g:`forall`, :g:`fix` and :g:`cofix` *bind* variables. A binding is represented by an identifier. If the binding variable is not used in the expression, the identifier can be replaced by the symbol :g:`_`. When the type of a bound variable cannot be synthesized by the -system, it can be specified with the notation ``(ident : type)``. There is also +system, it can be specified with the notation :n:`(@ident : @type)`. There is also a notation for a sequence of binding variables sharing the same type: -``(``:token:`ident`:math:`_1`…:token:`ident`:math:`_n` : :token:`type```)``. A +:n:`({+ @ident} : @type)`. A binder can also be any pattern prefixed by a quote, e.g. :g:`'(x,y)`. Some constructions allow the binding of a variable to value. This is called a “let-binder”. The entry :token:`binder` of the grammar accepts either an assumption binder as defined above or a let-binder. The notation in -the latter case is ``(ident := term)``. In a let-binder, only one +the latter case is :n:`(@ident := @term)`. In a let-binder, only one variable can be introduced at the same time. It is also possible to give the type of the variable as follows: -``(ident : term := term)``. +:n:`(@ident : @type := @term)`. Lists of :token:`binder` are allowed. In the case of :g:`fun` and :g:`forall`, it is intended that at least one binder of the list is an assumption otherwise @@ -263,7 +264,7 @@ the case of a single sequence of bindings sharing the same type (e.g.: Abstractions ------------ -The expression ``fun ident : type => term`` defines the +The expression :n:`fun @ident : @type => @term` defines the *abstraction* of the variable :token:`ident`, of type :token:`type`, over the term :token:`term`. It denotes a function of the variable :token:`ident` that evaluates to the expression :token:`term` (e.g. :g:`fun x : A => x` denotes the identity @@ -283,7 +284,7 @@ Section :ref:`let-in`). Products -------- -The expression :g:`forall ident : type, term` denotes the +The expression :n:`forall @ident : @type, @term` denotes the *product* of the variable :token:`ident` of type :token:`type`, over the term :token:`term`. As for abstractions, :g:`forall` is followed by a binder list, and products over several variables are equivalent to an iteration of one-variable @@ -314,17 +315,17 @@ The expression :token:`term`\ :math:`_0` :token:`term`\ :math:`_1` ... :token:`term`\ :math:`_1` ) … ) :token:`term`\ :math:`_n` : associativity is to the left. -The notation ``(ident := term)`` for arguments is used for making +The notation :n:`(@ident := @term)` for arguments is used for making explicit the value of implicit arguments (see Section :ref:`explicit-applications`). Type cast --------- -The expression ``term : type`` is a type cast expression. It enforces +The expression :n:`@term : @type` is a type cast expression. It enforces the type of :token:`term` to be :token:`type`. -``term <: type`` locally sets up the virtual machine for checking that +:n:`@term <: @type` locally sets up the virtual machine for checking that :token:`term` has type :token:`type`. Inferable subterms @@ -339,20 +340,18 @@ guess the missing piece of information. Let-in definitions ------------------ -``let`` :token:`ident` := :token:`term`:math:`_1` in :token:`term`:math:`_2` -denotes the local binding of :token:`term`:math:`_1` to the variable -:token:`ident` in :token:`term`:math:`_2`. There is a syntactic sugar for let-in -definition of functions: ``let`` :token:`ident` :token:`binder`:math:`_1` … -:token:`binder`:math:`_n` := :token:`term`:math:`_1` in :token:`term`:math:`_2` -stands for ``let`` :token:`ident` := ``fun`` :token:`binder`:math:`_1` … -:token:`binder`:math:`_n` => :token:`term`:math:`_1` in :token:`term`:math:`_2`. +:n:`let @ident := @term in @term’` +denotes the local binding of :token:`term` to the variable +:token:`ident` in :token:`term`’. There is a syntactic sugar for let-in +definition of functions: :n:`let @ident {+ @binder} := @term in @term’` +stands for :n:`let @ident := fun {+ @binder} => @term in @term’`. Definition by case analysis --------------------------- Objects of inductive types can be destructurated by a case-analysis construction called *pattern-matching* expression. A pattern-matching -expression is used to analyze the structure of an inductive objects and +expression is used to analyze the structure of an inductive object and to apply specific treatments accordingly. This paragraph describes the basic form of pattern-matching. See @@ -360,14 +359,14 @@ Section :ref:`Mult-match` and Chapter :ref:`extendedpatternmatching` for the des of the general form. The basic form of pattern-matching is characterized by a single :token:`match_item` expression, a :token:`mult_pattern` restricted to a single :token:`pattern` and :token:`pattern` restricted to the form -:token:`qualid` :token:`ident`. +:n:`@qualid {* @ident}`. -The expression match :token:`term`:math:`_0` :token:`return_type` with +The expression match ":token:`term`:math:`_0` :token:`return_type` with :token:`pattern`:math:`_1` => :token:`term`:math:`_1` :math:`|` … :math:`|` -:token:`pattern`:math:`_n` => :token:`term`:math:`_n` end, denotes a -:token:`pattern-matching` over the term :token:`term`:math:`_0` (expected to be +:token:`pattern`:math:`_n` => :token:`term`:math:`_n` end" denotes a +*pattern-matching* over the term :token:`term`:math:`_0` (expected to be of an inductive type :math:`I`). The terms :token:`term`:math:`_1`\ …\ -:token:`term`:math:`_n` are the :token:`branches` of the pattern-matching +:token:`term`:math:`_n` are the *branches* of the pattern-matching expression. Each of :token:`pattern`:math:`_i` has a form :token:`qualid` :token:`ident` where :token:`qualid` must denote a constructor. There should be exactly one branch for every constructor of :math:`I`. @@ -395,40 +394,39 @@ is dependent in the return type. For instance, in the following example: Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) := match b as x return or (eq bool x true) (eq bool x false) with - | true => or_introl (eq bool true true) (eq bool true false) - (eq_refl bool true) - | false => or_intror (eq bool false true) (eq bool false false) - (eq_refl bool false) + | true => or_introl (eq bool true true) (eq bool true false) (eq_refl bool true) + | false => or_intror (eq bool false true) (eq bool false false) (eq_refl bool false) end. -the branches have respective types or :g:`eq bool true true :g:`eq bool true -false` and or :g:`eq bool false true` :g:`eq bool false false` while the whole -pattern-matching expression has type or :g:`eq bool b true` :g:`eq bool b -false`, the identifier :g:`x` being used to represent the dependency. Remark -that when the term being matched is a variable, the as clause can be -omitted and the term being matched can serve itself as binding name in -the return type. For instance, the following alternative definition is -accepted and has the same meaning as the previous one. +the branches have respective types ":g:`or (eq bool true true) (eq bool true false)`" +and ":g:`or (eq bool false true) (eq bool false false)`" while the whole +pattern-matching expression has type ":g:`or (eq bool b true) (eq bool b false)`", +the identifier :g:`b` being used to represent the dependency. -.. coqtop:: in +.. note:: - Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) := - match b return or (eq bool b true) (eq bool b false) with - | true => or_introl (eq bool true true) (eq bool true false) - (eq_refl bool true) - | false => or_intror (eq bool false true) (eq bool false false) - (eq_refl bool false) - end. + When the term being matched is a variable, the ``as`` clause can be + omitted and the term being matched can serve itself as binding name in + the return type. For instance, the following alternative definition is + accepted and has the same meaning as the previous one. + + .. coqtop:: in + + Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) := + match b return or (eq bool b true) (eq bool b false) with + | true => or_introl (eq bool true true) (eq bool true false) (eq_refl bool true) + | false => or_intror (eq bool false true) (eq bool false false) (eq_refl bool false) + end. The second subcase is only relevant for annotated inductive types such -as the equality predicate (see Section :ref:`Equality`), +as the equality predicate (see Section :ref:`coq-equality`), the order predicate on natural numbers or the type of lists of a given length (see Section :ref:`matching-dependent`). In this configuration, the type of each branch can depend on the type dependencies specific to the branch and the whole pattern-matching expression has a type determined by the specific dependencies in the type of the term being matched. This dependency of the return type in the annotations of the inductive type -is expressed using a “in I _ ... _ :token:`pattern`:math:`_1` ... +is expressed using a “:g:`in` :math:`I` :g:`_ … _` :token:`pattern`:math:`_1` … :token:`pattern`:math:`_n`” clause, where - :math:`I` is the inductive type of the term being matched; @@ -452,44 +450,43 @@ For instance, in the following example: | eq_refl _ => eq_refl A x end. -the type of the branch has type :g:`eq A x x` because the third argument of -g:`eq` is g:`x` in the type of the pattern :g:`refl_equal`. On the contrary, the +the type of the branch is :g:`eq A x x` because the third argument of +:g:`eq` is :g:`x` in the type of the pattern :g:`eq_refl`. On the contrary, the type of the whole pattern-matching expression has type :g:`eq A y x` because the third argument of eq is y in the type of H. This dependency of the case analysis -in the third argument of :g:`eq` is expressed by the identifier g:`z` in the +in the third argument of :g:`eq` is expressed by the identifier :g:`z` in the return type. Finally, the third subcase is a combination of the first and second subcase. In particular, it only applies to pattern-matching on terms in -a type with annotations. For this third subcase, both the clauses as and -in are available. +a type with annotations. For this third subcase, both the clauses ``as`` and +``in`` are available. There are specific notations for case analysis on types with one or two -constructors: “if … then … else …” and “let (…, ” (see -Sections :ref:`if-then-else` and :ref:`let-in`). +constructors: ``if … then … else …`` and ``let (…,…) := … in …`` (see +Sections :ref:`if-then-else` and :ref:`irrefutable-patterns`). Recursive functions ------------------- -The expression “fix :token:`ident`:math:`_1` :token:`binder`:math:`_1` : -:token:`type`:math:`_1` ``:=`` :token:`term`:math:`_1` with … with +The expression “``fix`` :token:`ident`:math:`_1` :token:`binder`:math:`_1` ``:`` +:token:`type`:math:`_1` ``:=`` :token:`term`:math:`_1` ``with … with`` :token:`ident`:math:`_n` :token:`binder`:math:`_n` : :token:`type`:math:`_n` -``:=`` :token:`term`:math:`_n` for :token:`ident`:math:`_i`” denotes the -:math:`i`\ component of a block of functions defined by mutual well-founded +``:=`` :token:`term`:math:`_n` ``for`` :token:`ident`:math:`_i`” denotes the +:math:`i`-th component of a block of functions defined by mutual structural recursion. It is the local counterpart of the :cmd:`Fixpoint` command. When -:math:`n=1`, the “for :token:`ident`:math:`_i`” clause is omitted. +:math:`n=1`, the “``for`` :token:`ident`:math:`_i`” clause is omitted. -The expression “cofix :token:`ident`:math:`_1` :token:`binder`:math:`_1` : -:token:`type`:math:`_1` with … with :token:`ident`:math:`_n` :token:`binder`:math:`_n` -: :token:`type`:math:`_n` for :token:`ident`:math:`_i`” denotes the -:math:`i`\ component of a block of terms defined by a mutual guarded -co-recursion. It is the local counterpart of the ``CoFixpoint`` command. See -Section :ref:`CoFixpoint` for more details. When -:math:`n=1`, the “ for :token:`ident`:math:`_i`” clause is omitted. +The expression “``cofix`` :token:`ident`:math:`_1` :token:`binder`:math:`_1` ``:`` +:token:`type`:math:`_1` ``with … with`` :token:`ident`:math:`_n` :token:`binder`:math:`_n` +: :token:`type`:math:`_n` ``for`` :token:`ident`:math:`_i`” denotes the +:math:`i`-th component of a block of terms defined by a mutual guarded +co-recursion. It is the local counterpart of the :cmd:`CoFixpoint` command. When +:math:`n=1`, the “``for`` :token:`ident`:math:`_i`” clause is omitted. The association of a single fixpoint and a local definition have a special -syntax: “let fix f … := … in …” stands for “let f := fix f … := … in …”. The -same applies for co-fixpoints. +syntax: :n:`let fix @ident @binders := @term in` stands for +:n:`let @ident := fix @ident @binders := @term in`. The same applies for co-fixpoints. .. _vernacular: @@ -527,6 +524,9 @@ The Vernacular : | Proof . … Admitted . .. todo:: This use of … in this grammar is inconsistent + What about removing the proof part of this grammar from this chapter + and putting it somewhere where top-level tactics can be described as well? + See also #7583. This grammar describes *The Vernacular* which is the language of commands of Gallina. A sentence of the vernacular language, like in @@ -551,77 +551,74 @@ has type :token:`type`. .. _Axiom: -.. cmd:: Axiom @ident : @term +.. cmd:: Parameter @ident : @type - This command links :token:`term` to the name :token:`ident` as its specification in - the global context. The fact asserted by :token:`term` is thus assumed as a + This command links :token:`type` to the name :token:`ident` as its specification in + the global context. The fact asserted by :token:`type` is thus assumed as a postulate. -.. exn:: @ident already exists. - :name: @ident already exists. (Axiom) - -.. cmdv:: Parameter @ident : @term - :name: Parameter - - Is equivalent to ``Axiom`` :token:`ident` : :token:`term` - -.. cmdv:: Parameter {+ @ident } : @term - - Adds parameters with specification :token:`term` - -.. cmdv:: Parameter {+ ( {+ @ident } : @term ) } - - Adds blocks of parameters with different specifications. + .. exn:: @ident already exists. + :name: @ident already exists. (Axiom) + :undocumented: -.. cmdv:: Parameters {+ ( {+ @ident } : @term ) } + .. cmdv:: Parameter {+ @ident } : @type - Synonym of ``Parameter``. + Adds several parameters with specification :token:`type`. -.. cmdv:: Local Axiom @ident : @term + .. cmdv:: Parameter {+ ( {+ @ident } : @type ) } - Such axioms are never made accessible through their unqualified name by - :cmd:`Import` and its variants. You have to explicitly give their fully - qualified name to refer to them. + Adds blocks of parameters with different specifications. -.. cmdv:: Conjecture @ident : @term - :name: Conjecture + .. cmdv:: Local Parameter {+ ( {+ @ident } : @type ) } + :name: Local Parameter - Is equivalent to ``Axiom`` :token:`ident` : :token:`term`. + Such parameters are never made accessible through their unqualified name by + :cmd:`Import` and its variants. You have to explicitly give their fully + qualified name to refer to them. -.. cmd:: Variable @ident : @term + .. cmdv:: {? Local } Parameters {+ ( {+ @ident } : @type ) } + {? Local } Axiom {+ ( {+ @ident } : @type ) } + {? Local } Axioms {+ ( {+ @ident } : @type ) } + {? Local } Conjecture {+ ( {+ @ident } : @type ) } + {? Local } Conjectures {+ ( {+ @ident } : @type ) } + :name: Parameters; Axiom; Axioms; Conjecture; Conjectures -This command links :token:`term` to the name :token:`ident` in the context of -the current section (see Section :ref:`section-mechanism` for a description of -the section mechanism). When the current section is closed, name :token:`ident` -will be unknown and every object using this variable will be explicitly -parametrized (the variable is *discharged*). Using the ``Variable`` command out -of any section is equivalent to using ``Local Parameter``. + These variants are synonyms of :n:`{? Local } Parameter {+ ( {+ @ident } : @type ) }`. -.. exn:: @ident already exists. - :name: @ident already exists. (Variable) +.. cmd:: Variable @ident : @type -.. cmdv:: Variable {+ @ident } : @term + This command links :token:`type` to the name :token:`ident` in the context of + the current section (see Section :ref:`section-mechanism` for a description of + the section mechanism). When the current section is closed, name :token:`ident` + will be unknown and every object using this variable will be explicitly + parametrized (the variable is *discharged*). Using the :cmd:`Variable` command out + of any section is equivalent to using :cmd:`Local Parameter`. - Links :token:`term` to each :token:`ident`. + .. exn:: @ident already exists. + :name: @ident already exists. (Variable) + :undocumented: -.. cmdv:: Variable {+ ( {+ @ident } : @term) } + .. cmdv:: Variable {+ @ident } : @term - Adds blocks of variables with different specifications. + Links :token:`type` to each :token:`ident`. -.. cmdv:: Variables {+ ( {+ @ident } : @term) } - :name: Variables + .. cmdv:: Variable {+ ( {+ @ident } : @term ) } -.. cmdv:: Hypothesis {+ ( {+ @ident } : @term) } - :name: Hypothesis + Adds blocks of variables with different specifications. -.. cmdv:: Hypotheses {+ ( {+ @ident } : @term) } + .. cmdv:: Variables {+ ( {+ @ident } : @term) } + Hypothesis {+ ( {+ @ident } : @term) } + Hypotheses {+ ( {+ @ident } : @term) } + :name: Variables; Hypothesis; Hypotheses -Synonyms of ``Variable``. + These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @term) }`. -It is advised to use the keywords ``Axiom`` and ``Hypothesis`` for -logical postulates (i.e. when the assertion *term* is of sort ``Prop``), -and to use the keywords ``Parameter`` and ``Variable`` in other cases -(corresponding to the declaration of an abstract mathematical entity). +.. note:: + It is advised to use the commands :cmd:`Axiom`, :cmd:`Conjecture` and + :cmd:`Hypothesis` (and their plural forms) for logical postulates (i.e. when + the assertion :token:`type` is of sort :g:`Prop`), and to use the commands + :cmd:`Parameter` and :cmd:`Variable` (and their plural forms) in other cases + (corresponding to the declaration of an abstract mathematical entity). .. _gallina-definitions: @@ -649,63 +646,65 @@ Section :ref:`typing-rules`. This command binds :token:`term` to the name :token:`ident` in the environment, provided that :token:`term` is well-typed. -.. exn:: @ident already exists. - :name: @ident already exists. (Definition) - -.. cmdv:: Definition @ident : @term := @term - - It checks that the type of :token:`term`:math:`_2` is definitionally equal to - :token:`term`:math:`_1`, and registers :token:`ident` as being of type - :token:`term`:math:`_1`, and bound to value :token:`term`:math:`_2`. - + .. exn:: @ident already exists. + :name: @ident already exists. (Definition) + :undocumented: -.. cmdv:: Definition @ident {* @binder } : @term := @term + .. cmdv:: Definition @ident : @type := @term - This is equivalent to ``Definition`` :token:`ident` : :g:`forall` - :token:`binder`:math:`_1` … :token:`binder`:math:`_n`, :token:`term`:math:`_1` := - fun :token:`binder`:math:`_1` … - :token:`binder`:math:`_n` => :token:`term`:math:`_2`. + This variant checks that the type of :token:`term` is definitionally equal to + :token:`type`, and registers :token:`ident` as being of type + :token:`type`, and bound to value :token:`term`. -.. cmdv:: Local Definition @ident := @term + .. exn:: The term @term has type @type while it is expected to have type @type'. + :undocumented: - Such definitions are never made accessible through their - unqualified name by :cmd:`Import` and its variants. - You have to explicitly give their fully qualified name to refer to them. + .. cmdv:: Definition @ident @binders {? : @term } := @term -.. cmdv:: Example @ident := @term - :name: Example + This is equivalent to + :n:`Definition @ident : forall @binders, @term := fun @binders => @term`. -.. cmdv:: Example @ident : @term := @term + .. cmdv:: Local Definition @ident {? @binders } {? : @type } := @term + :name: Local Definition -.. cmdv:: Example @ident {* @binder } : @term := @term + Such definitions are never made accessible through their + unqualified name by :cmd:`Import` and its variants. + You have to explicitly give their fully qualified name to refer to them. -These are synonyms of the Definition forms. + .. cmdv:: {? Local } Example @ident {? @binders } {? : @type } := @term + :name: Example -.. exn:: The term @term has type @type while it is expected to have type @type. + This is equivalent to :cmd:`Definition`. -See also :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`. +.. seealso:: :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`. .. cmd:: Let @ident := @term -This command binds the value :token:`term` to the name :token:`ident` in the -environment of the current section. The name :token:`ident` disappears when the -current section is eventually closed, and, all persistent objects (such -as theorems) defined within the section and depending on :token:`ident` are -prefixed by the let-in definition ``let`` :token:`ident` ``:=`` :token:`term` -``in``. Using the ``Let`` command out of any section is equivalent to using -``Local Definition``. + This command binds the value :token:`term` to the name :token:`ident` in the + environment of the current section. The name :token:`ident` disappears when the + current section is eventually closed, and all persistent objects (such + as theorems) defined within the section and depending on :token:`ident` are + prefixed by the let-in definition :n:`let @ident := @term in`. + Using the :cmd:`Let` command out of any section is equivalent to using + :cmd:`Local Definition`. -.. exn:: @ident already exists. - :name: @ident already exists. (Let) + .. exn:: @ident already exists. + :name: @ident already exists. (Let) + :undocumented: -.. cmdv:: Let @ident : @term := @term + .. cmdv:: Let @ident {? @binders } {? : @type } := @term + :undocumented: -.. cmdv:: Let Fixpoint @ident @fix_body {* with @fix_body} + .. cmdv:: Let Fixpoint @ident @fix_body {* with @fix_body} + :name: Let Fixpoint + :undocumented: -.. cmdv:: Let CoFixpoint @ident @cofix_body {* with @cofix_body} + .. cmdv:: Let CoFixpoint @ident @cofix_body {* with @cofix_body} + :name: Let CoFixpoint + :undocumented: -See also Sections :ref:`section-mechanism`, commands :cmd:`Opaque`, -:cmd:`Transparent`, and tactic :tacn:`unfold`. +.. seealso:: Section :ref:`section-mechanism`, commands :cmd:`Opaque`, + :cmd:`Transparent`, and tactic :tacn:`unfold`. .. _gallina-inductive-definitions: @@ -719,63 +718,80 @@ explain also co-inductive types. Simple inductive types ~~~~~~~~~~~~~~~~~~~~~~ -The definition of a simple inductive type has the following form: +.. cmd:: Inductive @ident : {? @sort } := {? | } @ident : @type {* | @ident : @type } -.. cmd:: Inductive @ident : @sort := {? | } @ident : @type {* | @ident : @type } + This command defines a simple inductive type and its constructors. + The first :token:`ident` is the name of the inductively defined type + and :token:`sort` is the universe where it lives. The next :token:`ident`\s + are the names of its constructors and :token:`type` their respective types. + Depending on the universe where the inductive type :token:`ident` lives + (e.g. its type :token:`sort`), Coq provides a number of destructors. + Destructors are named :token:`ident`\ ``_ind``, :token:`ident`\ ``_rec`` + or :token:`ident`\ ``_rect`` which respectively correspond to elimination + principles on :g:`Prop`, :g:`Set` and :g:`Type`. + The type of the destructors expresses structural induction/recursion + principles over objects of type :token:`ident`. + The constant :token:`ident`\ ``_ind`` is always provided, + whereas :token:`ident`\ ``_rec`` and :token:`ident`\ ``_rect`` can be + impossible to derive (for example, when :token:`ident` is a proposition). -The name :token:`ident` is the name of the inductively defined type and -:token:`sort` is the universes where it lives. The :token:`ident` are the names -of its constructors and :token:`type` their respective types. The types of the -constructors have to satisfy a *positivity condition* (see Section -:ref:`positivity`) for :token:`ident`. This condition ensures the soundness of -the inductive definition. If this is the case, the :token:`ident` are added to -the environment with their respective types. Accordingly to the universe where -the inductive type lives (e.g. its type :token:`sort`), Coq provides a number of -destructors for :token:`ident`. Destructors are named ``ident_ind``, -``ident_rec`` or ``ident_rect`` which respectively correspond to -elimination principles on :g:`Prop`, :g:`Set` and :g:`Type`. The type of the -destructors expresses structural induction/recursion principles over objects of -:token:`ident`. We give below two examples of the use of the Inductive -definitions. + .. exn:: Non strictly positive occurrence of @ident in @type. -The set of natural numbers is defined as: + The types of the constructors have to satisfy a *positivity condition* + (see Section :ref:`positivity`). This condition ensures the soundness of + the inductive definition. -.. coqtop:: all + .. exn:: The conclusion of @type is not valid; it must be built from @ident. - Inductive nat : Set := - | O : nat - | S : nat -> nat. + The conclusion of the type of the constructors must be the inductive type + :token:`ident` being defined (or :token:`ident` applied to arguments in + the case of annotated inductive types — cf. next section). -The type nat is defined as the least :g:`Set` containing :g:`O` and closed by -the :g:`S` constructor. The names :g:`nat`, :g:`O` and :g:`S` are added to the -environment. + .. example:: + The set of natural numbers is defined as: -Now let us have a look at the elimination principles. They are three of them: -:g:`nat_ind`, :g:`nat_rec` and :g:`nat_rect`. The type of :g:`nat_ind` is: + .. coqtop:: all -.. coqtop:: all + Inductive nat : Set := + | O : nat + | S : nat -> nat. - Check nat_ind. + The type nat is defined as the least :g:`Set` containing :g:`O` and closed by + the :g:`S` constructor. The names :g:`nat`, :g:`O` and :g:`S` are added to the + environment. -This is the well known structural induction principle over natural -numbers, i.e. the second-order form of Peano’s induction principle. It -allows proving some universal property of natural numbers (:g:`forall -n:nat, P n`) by induction on :g:`n`. + Now let us have a look at the elimination principles. They are three of them: + :g:`nat_ind`, :g:`nat_rec` and :g:`nat_rect`. The type of :g:`nat_ind` is: -The types of :g:`nat_rec` and :g:`nat_rect` are similar, except that they pertain -to :g:`(P:nat->Set)` and :g:`(P:nat->Type)` respectively. They correspond to -primitive induction principles (allowing dependent types) respectively -over sorts ``Set`` and ``Type``. The constant ``ident_ind`` is always -provided, whereas ``ident_rec`` and ``ident_rect`` can be impossible -to derive (for example, when :token:`ident` is a proposition). + .. coqtop:: all -.. coqtop:: in + Check nat_ind. + + This is the well known structural induction principle over natural + numbers, i.e. the second-order form of Peano’s induction principle. It + allows proving some universal property of natural numbers (:g:`forall + n:nat, P n`) by induction on :g:`n`. + + The types of :g:`nat_rec` and :g:`nat_rect` are similar, except that they pertain + to :g:`(P:nat->Set)` and :g:`(P:nat->Type)` respectively. They correspond to + primitive induction principles (allowing dependent types) respectively + over sorts ``Set`` and ``Type``. + + .. cmdv:: Inductive @ident {? : @sort } := {? | } {*| @ident {? @binders } {? : @type } } + + Constructors :token:`ident`\s can come with :token:`binders` in which case, + the actual type of the constructor is :n:`forall @binders, @type`. + + In the case where inductive types have no annotations (next section + gives an example of such annotations), a constructor can be defined + by only giving the type of its arguments. + + .. example:: - Inductive nat : Set := O | S (_:nat). + .. coqtop:: in + + Inductive nat : Set := O | S (_:nat). -In the case where inductive types have no annotations (next section -gives an example of such annotations), a constructor can be defined -by only giving the type of its arguments. Simple annotated inductive types ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -784,203 +800,195 @@ In an annotated inductive types, the universe where the inductive type is defined is no longer a simple sort, but what is called an arity, which is a type whose conclusion is a sort. -As an example of annotated inductive types, let us define the -:g:`even` predicate: - -.. coqtop:: all +.. example:: - Inductive even : nat -> Prop := - | even_0 : even O - | even_SS : forall n:nat, even n -> even (S (S n)). + As an example of annotated inductive types, let us define the + :g:`even` predicate: -The type :g:`nat->Prop` means that even is a unary predicate (inductively -defined) over natural numbers. The type of its two constructors are the -defining clauses of the predicate even. The type of :g:`even_ind` is: + .. coqtop:: all -.. coqtop:: all + Inductive even : nat -> Prop := + | even_0 : even O + | even_SS : forall n:nat, even n -> even (S (S n)). - Check even_ind. + The type :g:`nat->Prop` means that even is a unary predicate (inductively + defined) over natural numbers. The type of its two constructors are the + defining clauses of the predicate even. The type of :g:`even_ind` is: -From a mathematical point of view it asserts that the natural numbers satisfying -the predicate even are exactly in the smallest set of naturals satisfying the -clauses :g:`even_0` or :g:`even_SS`. This is why, when we want to prove any -predicate :g:`P` over elements of :g:`even`, it is enough to prove it for :g:`O` -and to prove that if any natural number :g:`n` satisfies :g:`P` its double -successor :g:`(S (S n))` satisfies also :g:`P`. This is indeed analogous to the -structural induction principle we got for :g:`nat`. + .. coqtop:: all -.. exn:: Non strictly positive occurrence of @ident in @type. + Check even_ind. -.. exn:: The conclusion of @type is not valid; it must be built from @ident. + From a mathematical point of view it asserts that the natural numbers satisfying + the predicate even are exactly in the smallest set of naturals satisfying the + clauses :g:`even_0` or :g:`even_SS`. This is why, when we want to prove any + predicate :g:`P` over elements of :g:`even`, it is enough to prove it for :g:`O` + and to prove that if any natural number :g:`n` satisfies :g:`P` its double + successor :g:`(S (S n))` satisfies also :g:`P`. This is indeed analogous to the + structural induction principle we got for :g:`nat`. Parametrized inductive types ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -In the previous example, each constructor introduces a different -instance of the predicate even. In some cases, all the constructors -introduces the same generic instance of the inductive definition, in -which case, instead of an annotation, we use a context of parameters -which are binders shared by all the constructors of the definition. +.. cmdv:: Inductive @ident @binders {? : @type } := {? | } @ident : @type {* | @ident : @type} -The general scheme is: + In the previous example, each constructor introduces a different + instance of the predicate :g:`even`. In some cases, all the constructors + introduce the same generic instance of the inductive definition, in + which case, instead of an annotation, we use a context of parameters + which are :token:`binders` shared by all the constructors of the definition. -.. cmdv:: Inductive @ident {+ @binder} : @term := {? | } @ident : @type {* | @ident : @type} - -Parameters differ from inductive type annotations in the fact that the -conclusion of each type of constructor :g:`term` invoke the inductive type with -the same values of parameters as its specification. - -A typical example is the definition of polymorphic lists: - -.. coqtop:: in + Parameters differ from inductive type annotations in the fact that the + conclusion of each type of constructor invoke the inductive type with + the same values of parameters as its specification. - Inductive list (A:Set) : Set := - | nil : list A - | cons : A -> list A -> list A. + .. example:: -.. note:: + A typical example is the definition of polymorphic lists: - In the type of :g:`nil` and :g:`cons`, we write :g:`(list A)` and not - just :g:`list`. The constructors :g:`nil` and :g:`cons` will have respectively - types: + .. coqtop:: in - .. coqtop:: all + Inductive list (A:Set) : Set := + | nil : list A + | cons : A -> list A -> list A. - Check nil. - Check cons. + In the type of :g:`nil` and :g:`cons`, we write :g:`(list A)` and not + just :g:`list`. The constructors :g:`nil` and :g:`cons` will have respectively + types: - Types of destructors are also quantified with :g:`(A:Set)`. + .. coqtop:: all -Variants -++++++++ + Check nil. + Check cons. -.. coqtop:: in + Types of destructors are also quantified with :g:`(A:Set)`. - Inductive list (A:Set) : Set := nil | cons (_:A) (_:list A). + Once again, it is possible to specify only the type of the arguments + of the constructors, and to omit the type of the conclusion: -This is an alternative definition of lists where we specify the -arguments of the constructors rather than their full type. + .. coqtop:: in -.. coqtop:: in + Inductive list (A:Set) : Set := nil | cons (_:A) (_:list A). - Variant sum (A B:Set) : Set := left : A -> sum A B | right : B -> sum A B. +.. note:: + + It is possible in the type of a constructor, to + invoke recursively the inductive definition on an argument which is not + the parameter itself. -The ``Variant`` keyword is identical to the ``Inductive`` keyword, except -that it disallows recursive definition of types (in particular lists cannot -be defined with the Variant keyword). No induction scheme is generated for -this variant, unless :opt:`Nonrecursive Elimination Schemes` is set. + One can define : -.. exn:: The @num th argument of @ident must be @ident in @type. + .. coqtop:: all -New from Coq V8.1 -+++++++++++++++++ + Inductive list2 (A:Set) : Set := + | nil2 : list2 A + | cons2 : A -> list2 (A*A) -> list2 A. -The condition on parameters for inductive definitions has been relaxed -since Coq V8.1. It is now possible in the type of a constructor, to -invoke recursively the inductive definition on an argument which is not -the parameter itself. + that can also be written by specifying only the type of the arguments: -One can define : + .. coqtop:: all reset -.. coqtop:: all + Inductive list2 (A:Set) : Set := nil2 | cons2 (_:A) (_:list2 (A*A)). - Inductive list2 (A:Set) : Set := - | nil2 : list2 A - | cons2 : A -> list2 (A*A) -> list2 A. + But the following definition will give an error: -that can also be written by specifying only the type of the arguments: + .. coqtop:: all -.. coqtop:: all reset + Fail Inductive listw (A:Set) : Set := + | nilw : listw (A*A) + | consw : A -> listw (A*A) -> listw (A*A). - Inductive list2 (A:Set) : Set := nil2 | cons2 (_:A) (_:list2 (A*A)). + because the conclusion of the type of constructors should be :g:`listw A` + in both cases. -But the following definition will give an error: + + A parametrized inductive definition can be defined using annotations + instead of parameters but it will sometimes give a different (bigger) + sort for the inductive definition and will produce a less convenient + rule for case elimination. -.. coqtop:: all +.. seealso:: + Section :ref:`inductive-definitions` and the :tacn:`induction` tactic. - Fail Inductive listw (A:Set) : Set := - | nilw : listw (A*A) - | consw : A -> listw (A*A) -> listw (A*A). +Variants +~~~~~~~~ -Because the conclusion of the type of constructors should be :g:`listw A` in -both cases. +.. cmd:: Variant @ident @binders {? : @type } := {? | } @ident : @type {* | @ident : @type} -A parametrized inductive definition can be defined using annotations -instead of parameters but it will sometimes give a different (bigger) -sort for the inductive definition and will produce a less convenient -rule for case elimination. + The :cmd:`Variant` command is identical to the :cmd:`Inductive` command, except + that it disallows recursive definition of types (for instance, lists cannot + be defined using :cmd:`Variant`). No induction scheme is generated for + this variant, unless option :opt:`Nonrecursive Elimination Schemes` is on. -See also Section :ref:`inductive-definitions` and the :tacn:`induction` -tactic. + .. exn:: The @num th argument of @ident must be @ident in @type. + :undocumented: Mutually defined inductive types ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The definition of a block of mutually inductive types has the form: +.. cmdv:: Inductive @ident {? : @type } := {? | } {*| @ident : @type } {* with {? | } {*| @ident {? : @type } } } -.. cmdv:: Inductive @ident : @term := {? | } @ident : @type {* | @ident : @type } {* with @ident : @term := {? | } @ident : @type {* | @ident : @type }} + This variant allows defining a block of mutually inductive types. + It has the same semantics as the above :cmd:`Inductive` definition for each + :token:`ident`. All :token:`ident` are simultaneously added to the environment. + Then well-typing of constructors can be checked. Each one of the :token:`ident` + can be used on its own. -It has the same semantics as the above ``Inductive`` definition for each -:token:`ident` All :token:`ident` are simultaneously added to the environment. -Then well-typing of constructors can be checked. Each one of the :token:`ident` -can be used on its own. + .. cmdv:: Inductive @ident @binders {? : @type } := {? | } {*| @ident : @type } {* with {? | } {*| @ident @binders {? : @type } } } -It is also possible to parametrize these inductive definitions. However, -parameters correspond to a local context in which the whole set of -inductive declarations is done. For this reason, the parameters must be -strictly the same for each inductive types The extended syntax is: + In this variant, the inductive definitions are parametrized + with :token:`binders`. However, parameters correspond to a local context + in which the whole set of inductive declarations is done. For this + reason, the parameters must be strictly the same for each inductive types. -.. cmdv:: Inductive @ident {+ @binder} : @term := {? | } @ident : @type {* | @ident : @type } {* with @ident {+ @binder} : @term := {? | } @ident : @type {* | @ident : @type }} - -The typical example of a mutual inductive data type is the one for trees and -forests. We assume given two types :g:`A` and :g:`B` as variables. It can -be declared the following way. +.. example:: + The typical example of a mutual inductive data type is the one for trees and + forests. We assume given two types :g:`A` and :g:`B` as variables. It can + be declared the following way. -.. coqtop:: in + .. coqtop:: in - Variables A B : Set. + Variables A B : Set. - Inductive tree : Set := - node : A -> forest -> tree + Inductive tree : Set := node : A -> forest -> tree - with forest : Set := - | leaf : B -> forest - | cons : tree -> forest -> forest. + with forest : Set := + | leaf : B -> forest + | cons : tree -> forest -> forest. -This declaration generates automatically six induction principles. They are -respectively called :g:`tree_rec`, :g:`tree_ind`, :g:`tree_rect`, -:g:`forest_rec`, :g:`forest_ind`, :g:`forest_rect`. These ones are not the most -general ones but are just the induction principles corresponding to each -inductive part seen as a single inductive definition. + This declaration generates automatically six induction principles. They are + respectively called :g:`tree_rec`, :g:`tree_ind`, :g:`tree_rect`, + :g:`forest_rec`, :g:`forest_ind`, :g:`forest_rect`. These ones are not the most + general ones but are just the induction principles corresponding to each + inductive part seen as a single inductive definition. -To illustrate this point on our example, we give the types of :g:`tree_rec` -and :g:`forest_rec`. + To illustrate this point on our example, we give the types of :g:`tree_rec` + and :g:`forest_rec`. -.. coqtop:: all + .. coqtop:: all - Check tree_rec. + Check tree_rec. - Check forest_rec. + Check forest_rec. -Assume we want to parametrize our mutual inductive definitions with the -two type variables :g:`A` and :g:`B`, the declaration should be -done the following way: + Assume we want to parametrize our mutual inductive definitions with the + two type variables :g:`A` and :g:`B`, the declaration should be + done the following way: -.. coqtop:: in + .. coqtop:: in - Inductive tree (A B:Set) : Set := - node : A -> forest A B -> tree A B + Inductive tree (A B:Set) : Set := node : A -> forest A B -> tree A B - with forest (A B:Set) : Set := - | leaf : B -> forest A B - | cons : tree A B -> forest A B -> forest A B. + with forest (A B:Set) : Set := + | leaf : B -> forest A B + | cons : tree A B -> forest A B -> forest A B. -Assume we define an inductive definition inside a section. When the -section is closed, the variables declared in the section and occurring -free in the declaration are added as parameters to the inductive -definition. + Assume we define an inductive definition inside a section + (cf. :ref:`section-mechanism`). When the section is closed, the variables + declared in the section and occurring free in the declaration are added as + parameters to the inductive definition. -See also Section :ref:`section-mechanism`. +.. seealso:: + A generic command :cmd:`Scheme` is useful to build automatically various + mutual induction principles. .. _coinductive-types: @@ -995,41 +1003,47 @@ constructors. Infinite objects are introduced by a non-ending (but effective) process of construction, defined in terms of the constructors of the type. -An example of a co-inductive type is the type of infinite sequences of -natural numbers, usually called streams. It can be introduced in -Coq using the ``CoInductive`` command: +.. cmd:: CoInductive @ident @binders {? : @type } := {? | } @ident : @type {* | @ident : @type} -.. coqtop:: all + This command introduces a co-inductive type. + The syntax of the command is the same as the command :cmd:`Inductive`. + No principle of induction is derived from the definition of a co-inductive + type, since such principles only make sense for inductive types. + For co-inductive types, the only elimination principle is case analysis. + +.. example:: + An example of a co-inductive type is the type of infinite sequences of + natural numbers, usually called streams. - CoInductive Stream : Set := - Seq : nat -> Stream -> Stream. + .. coqtop:: in -The syntax of this command is the same as the command :cmd:`Inductive`. Notice -that no principle of induction is derived from the definition of a co-inductive -type, since such principles only make sense for inductive ones. For co-inductive -ones, the only elimination principle is case analysis. For example, the usual -destructors on streams :g:`hd:Stream->nat` and :g:`tl:Str->Str` can be defined -as follows: + CoInductive Stream : Set := Seq : nat -> Stream -> Stream. -.. coqtop:: all + The usual destructors on streams :g:`hd:Stream->nat` and :g:`tl:Str->Str` + can be defined as follows: - Definition hd (x:Stream) := let (a,s) := x in a. - Definition tl (x:Stream) := let (a,s) := x in s. + .. coqtop:: in + + Definition hd (x:Stream) := let (a,s) := x in a. + Definition tl (x:Stream) := let (a,s) := x in s. Definition of co-inductive predicates and blocks of mutually -co-inductive definitions are also allowed. An example of a co-inductive -predicate is the extensional equality on streams: +co-inductive definitions are also allowed. + +.. example:: + An example of a co-inductive predicate is the extensional equality on + streams: -.. coqtop:: all + .. coqtop:: in - CoInductive EqSt : Stream -> Stream -> Prop := - eqst : forall s1 s2:Stream, - hd s1 = hd s2 -> EqSt (tl s1) (tl s2) -> EqSt s1 s2. + CoInductive EqSt : Stream -> Stream -> Prop := + eqst : forall s1 s2:Stream, + hd s1 = hd s2 -> EqSt (tl s1) (tl s2) -> EqSt s1 s2. -In order to prove the extensionally equality of two streams :g:`s1` and :g:`s2` -we have to construct an infinite proof of equality, that is, an infinite object -of type :g:`(EqSt s1 s2)`. We will see how to introduce infinite objects in -Section :ref:`cofixpoint`. + In order to prove the extensional equality of two streams :g:`s1` and :g:`s2` + we have to construct an infinite proof of equality, that is, an infinite + object of type :g:`(EqSt s1 s2)`. We will see how to introduce infinite + objects in Section :ref:`cofixpoint`. Definition of recursive functions --------------------------------- @@ -1043,197 +1057,178 @@ constructions. .. _Fixpoint: -.. cmd:: Fixpoint @ident @params {struct @ident} : @type := @term - -This command allows defining functions by pattern-matching over inductive objects -using a fixed point construction. The meaning of this declaration is to -define :token:`ident` a recursive function with arguments specified by the -binders in :token:`params` such that :token:`ident` applied to arguments corresponding -to these binders has type :token:`type`:math:`_0`, and is equivalent to the -expression :token:`term`:math:`_0`. The type of the :token:`ident` is consequently -:g:`forall` :token:`params`, :token:`type`:math:`_0` and the value is equivalent to -:g:`fun` :token:`params` :g:`=>` :token:`term`:math:`_0`. - -To be accepted, a ``Fixpoint`` definition has to satisfy some syntactical -constraints on a special argument called the decreasing argument. They -are needed to ensure that the Fixpoint definition always terminates. The -point of the {struct :token:`ident`} annotation is to let the user tell the -system which argument decreases along the recursive calls. For instance, -one can define the addition function as : - -.. coqtop:: all - - Fixpoint add (n m:nat) {struct n} : nat := - match n with - | O => m - | S p => S (add p m) - end. +.. cmd:: Fixpoint @ident @binders {? {struct @ident} } {? : @type } := @term -The ``{struct`` :token:`ident```}`` annotation may be left implicit, in this case the -system try successively arguments from left to right until it finds one that -satisfies the decreasing condition. + This command allows defining functions by pattern-matching over inductive + objects using a fixed point construction. The meaning of this declaration is + to define :token:`ident` a recursive function with arguments specified by + the :token:`binders` such that :token:`ident` applied to arguments + corresponding to these :token:`binders` has type :token:`type`, and is + equivalent to the expression :token:`term`. The type of :token:`ident` is + consequently :n:`forall @binders, @type` and its value is equivalent + to :n:`fun @binders => @term`. -.. note:: + To be accepted, a :cmd:`Fixpoint` definition has to satisfy some syntactical + constraints on a special argument called the decreasing argument. They + are needed to ensure that the :cmd:`Fixpoint` definition always terminates. + The point of the :n:`{struct @ident}` annotation is to let the user tell the + system which argument decreases along the recursive calls. - Some fixpoints may have several arguments that fit as decreasing - arguments, and this choice influences the reduction of the fixpoint. Hence an - explicit annotation must be used if the leftmost decreasing argument is not the - desired one. Writing explicit annotations can also speed up type-checking of - large mutual fixpoints. + The :n:`{struct @ident}` annotation may be left implicit, in this case the + system tries successively arguments from left to right until it finds one + that satisfies the decreasing condition. -The match operator matches a value (here :g:`n`) with the various -constructors of its (inductive) type. The remaining arguments give the -respective values to be returned, as functions of the parameters of the -corresponding constructor. Thus here when :g:`n` equals :g:`O` we return -:g:`m`, and when :g:`n` equals :g:`(S p)` we return :g:`(S (add p m))`. + .. note:: -The match operator is formally described in detail in Section -:ref:`match-construction`. -The system recognizes that in the inductive call :g:`(add p m)` the first -argument actually decreases because it is a *pattern variable* coming from -:g:`match n with`. + + Some fixpoints may have several arguments that fit as decreasing + arguments, and this choice influences the reduction of the fixpoint. + Hence an explicit annotation must be used if the leftmost decreasing + argument is not the desired one. Writing explicit annotations can also + speed up type-checking of large mutual fixpoints. -.. example:: + + In order to keep the strong normalization property, the fixed point + reduction will only be performed when the argument in position of the + decreasing argument (which type should be in an inductive definition) + starts with a constructor. - The following definition is not correct and generates an error message: - .. coqtop:: all + .. example:: + One can define the addition function as : - Fail Fixpoint wrongplus (n m:nat) {struct n} : nat := - match m with - | O => n - | S p => S (wrongplus n p) - end. + .. coqtop:: all - because the declared decreasing argument n actually does not decrease in - the recursive call. The function computing the addition over the second - argument should rather be written: + Fixpoint add (n m:nat) {struct n} : nat := + match n with + | O => m + | S p => S (add p m) + end. - .. coqtop:: all + The match operator matches a value (here :g:`n`) with the various + constructors of its (inductive) type. The remaining arguments give the + respective values to be returned, as functions of the parameters of the + corresponding constructor. Thus here when :g:`n` equals :g:`O` we return + :g:`m`, and when :g:`n` equals :g:`(S p)` we return :g:`(S (add p m))`. - Fixpoint plus (n m:nat) {struct m} : nat := - match m with - | O => n - | S p => S (plus n p) - end. + The match operator is formally described in + Section :ref:`match-construction`. + The system recognizes that in the inductive call :g:`(add p m)` the first + argument actually decreases because it is a *pattern variable* coming + from :g:`match n with`. -.. example:: + .. example:: - The ordinary match operation on natural numbers can be mimicked in the - following way. + The following definition is not correct and generates an error message: - .. coqtop:: all + .. coqtop:: all - Fixpoint nat_match - (C:Set) (f0:C) (fS:nat -> C -> C) (n:nat) {struct n} : C := - match n with - | O => f0 - | S p => fS p (nat_match C f0 fS p) - end. + Fail Fixpoint wrongplus (n m:nat) {struct n} : nat := + match m with + | O => n + | S p => S (wrongplus n p) + end. -.. example:: + because the declared decreasing argument :g:`n` does not actually + decrease in the recursive call. The function computing the addition over + the second argument should rather be written: - The recursive call may not only be on direct subterms of the recursive - variable n but also on a deeper subterm and we can directly write the - function mod2 which gives the remainder modulo 2 of a natural number. + .. coqtop:: all - .. coqtop:: all + Fixpoint plus (n m:nat) {struct m} : nat := + match m with + | O => n + | S p => S (plus n p) + end. - Fixpoint mod2 (n:nat) : nat := - match n with - | O => O - | S p => match p with - | O => S O - | S q => mod2 q - end - end. + .. example:: -In order to keep the strong normalization property, the fixed point -reduction will only be performed when the argument in position of the -decreasing argument (which type should be in an inductive definition) -starts with a constructor. + The recursive call may not only be on direct subterms of the recursive + variable :g:`n` but also on a deeper subterm and we can directly write + the function :g:`mod2` which gives the remainder modulo 2 of a natural + number. -The ``Fixpoint`` construction enjoys also the with extension to define functions -over mutually defined inductive types or more generally any mutually recursive -definitions. + .. coqtop:: all -.. cmdv:: Fixpoint @ident @params {struct @ident} : @type := @term {* with @ident {+ @params} : @type := @term} + Fixpoint mod2 (n:nat) : nat := + match n with + | O => O + | S p => match p with + | O => S O + | S q => mod2 q + end + end. -allows to define simultaneously fixpoints. -The size of trees and forests can be defined the following way: + .. cmdv:: Fixpoint @ident @binders {? {struct @ident} } {? : @type } := @term {* with @ident @binders {? : @type } := @term } + + This variant allows defining simultaneously several mutual fixpoints. + It is especially useful when defining functions over mutually defined + inductive types. -.. coqtop:: all + .. example:: + The size of trees and forests can be defined the following way: - Fixpoint tree_size (t:tree) : nat := - match t with - | node a f => S (forest_size f) - end - with forest_size (f:forest) : nat := - match f with - | leaf b => 1 - | cons t f' => (tree_size t + forest_size f') - end. + .. coqtop:: all -A generic command Scheme is useful to build automatically various mutual -induction principles. It is described in Section -:ref:`proofschemes-induction-principles`. + Fixpoint tree_size (t:tree) : nat := + match t with + | node a f => S (forest_size f) + end + with forest_size (f:forest) : nat := + match f with + | leaf b => 1 + | cons t f' => (tree_size t + forest_size f') + end. .. _cofixpoint: Definitions of recursive objects in co-inductive types ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: CoFixpoint @ident : @type := @term +.. cmd:: CoFixpoint @ident {? @binders } {? : @type } := @term -introduces a method for constructing an infinite object of a coinductive -type. For example, the stream containing all natural numbers can be -introduced applying the following method to the number :g:`O` (see -Section :ref:`coinductive-types` for the definition of :g:`Stream`, :g:`hd` and -:g:`tl`): + This command introduces a method for constructing an infinite object of a + coinductive type. For example, the stream containing all natural numbers can + be introduced applying the following method to the number :g:`O` (see + Section :ref:`coinductive-types` for the definition of :g:`Stream`, :g:`hd` + and :g:`tl`): -.. coqtop:: all - - CoFixpoint from (n:nat) : Stream := Seq n (from (S n)). - -Oppositely to recursive ones, there is no decreasing argument in a -co-recursive definition. To be admissible, a method of construction must -provide at least one extra constructor of the infinite object for each -iteration. A syntactical guard condition is imposed on co-recursive -definitions in order to ensure this: each recursive call in the -definition must be protected by at least one constructor, and only by -constructors. That is the case in the former definition, where the -single recursive call of :g:`from` is guarded by an application of -:g:`Seq`. On the contrary, the following recursive function does not -satisfy the guard condition: + .. coqtop:: all -.. coqtop:: all + CoFixpoint from (n:nat) : Stream := Seq n (from (S n)). - Fail CoFixpoint filter (p:nat -> bool) (s:Stream) : Stream := - if p (hd s) then Seq (hd s) (filter p (tl s)) else filter p (tl s). + Oppositely to recursive ones, there is no decreasing argument in a + co-recursive definition. To be admissible, a method of construction must + provide at least one extra constructor of the infinite object for each + iteration. A syntactical guard condition is imposed on co-recursive + definitions in order to ensure this: each recursive call in the + definition must be protected by at least one constructor, and only by + constructors. That is the case in the former definition, where the single + recursive call of :g:`from` is guarded by an application of :g:`Seq`. + On the contrary, the following recursive function does not satisfy the + guard condition: -The elimination of co-recursive definition is done lazily, i.e. the -definition is expanded only when it occurs at the head of an application -which is the argument of a case analysis expression. In any other -context, it is considered as a canonical expression which is completely -evaluated. We can test this using the command ``Eval``, which computes -the normal forms of a term: + .. coqtop:: all -.. coqtop:: all + Fail CoFixpoint filter (p:nat -> bool) (s:Stream) : Stream := + if p (hd s) then Seq (hd s) (filter p (tl s)) else filter p (tl s). - Eval compute in (from 0). - Eval compute in (hd (from 0)). - Eval compute in (tl (from 0)). + The elimination of co-recursive definition is done lazily, i.e. the + definition is expanded only when it occurs at the head of an application + which is the argument of a case analysis expression. In any other + context, it is considered as a canonical expression which is completely + evaluated. We can test this using the command :cmd:`Eval`, which computes + the normal forms of a term: -.. cmdv:: CoFixpoint @ident @params : @type := @term + .. coqtop:: all - As for most constructions, arguments of co-fixpoints expressions - can be introduced before the :g:`:=` sign. + Eval compute in (from 0). + Eval compute in (hd (from 0)). + Eval compute in (tl (from 0)). -.. cmdv:: CoFixpoint @ident : @type := @term {+ with @ident : @type := @term } + .. cmdv:: CoFixpoint @ident {? @binders } {? : @type } := @term {* with @ident {? @binders } : {? @type } := @term } - As in the :cmd:`Fixpoint` command, it is possible to introduce a block of - mutually dependent methods. + As in the :cmd:`Fixpoint` command, it is possible to introduce a block of + mutually dependent methods. .. _Assertions: @@ -1253,6 +1248,7 @@ Chapter :ref:`Tactics`. The basic assertion command is: 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. + :undocumented: .. exn:: @ident already exists. :name: @ident already exists. (Theorem) @@ -1266,24 +1262,16 @@ Chapter :ref:`Tactics`. The basic assertion command is: This feature, called nested proofs, is disabled by default. To activate it, turn option :opt:`Nested Proofs Allowed` on. - The following commands are synonyms of :n:`Theorem @ident {? @binders } : type`: - .. cmdv:: Lemma @ident {? @binders } : @type - :name: Lemma - - .. cmdv:: Remark @ident {? @binders } : @type - :name: Remark - - .. cmdv:: Fact @ident {? @binders } : @type - :name: Fact - - .. cmdv:: Corollary @ident {? @binders } : @type - :name: Corollary + Remark @ident {? @binders } : @type + Fact @ident {? @binders } : @type + Corollary @ident {? @binders } : @type + Proposition @ident {? @binders } : @type + :name: Lemma; Remark; Fact; Corollary; Proposition - .. cmdv:: Proposition @ident {? @binders } : @type - :name: Proposition + These commands are all synonyms of :n:`Theorem @ident {? @binders } : type`. -.. cmdv:: Theorem @ident : @type {* with @ident : @type} +.. cmdv:: Theorem @ident {? @binders } : @type {* with @ident {? @binders } : @type} This command is useful for theorems that are proved by simultaneous induction over a mutually inductive assumption, or that assert mutually dependent @@ -1305,7 +1293,7 @@ Chapter :ref:`Tactics`. The basic assertion command is: The command can be used also with :cmd:`Lemma`, :cmd:`Remark`, etc. instead of :cmd:`Theorem`. -.. cmdv:: Definition @ident : @type +.. cmdv:: Definition @ident {? @binders } : @type This allows defining a term of type :token:`type` using the proof editing mode. It behaves as :cmd:`Theorem` but is intended to be used in conjunction with @@ -1316,22 +1304,22 @@ Chapter :ref:`Tactics`. The basic assertion command is: .. seealso:: :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`. -.. cmdv:: Let @ident : @type +.. cmdv:: Let @ident {? @binders } : @type - Like Definition :token:`ident` : :token:`type`. except that the definition is + Like :n:`Definition @ident {? @binders } : @type` except that the definition is turned into a let-in definition generalized over the declarations depending on it after closing the current section. -.. cmdv:: Fixpoint @ident @binders with +.. cmdv:: Fixpoint @ident @binders : @type {* with @ident @binders : @type} - This generalizes the syntax of Fixpoint so that one or more bodies + This generalizes the syntax of :cmd:`Fixpoint` so that one or more bodies can be defined interactively using the proof editing mode (when a body is omitted, its type is mandatory in the syntax). When the block - of proofs is completed, it is intended to be ended by Defined. + of proofs is completed, it is intended to be ended by :cmd:`Defined`. -.. cmdv:: CoFixpoint @ident with +.. cmdv:: CoFixpoint @ident {? @binders } : @type {* with @ident {? @binders } : @type} - This generalizes the syntax of CoFixpoint so that one or more bodies + This generalizes the syntax of :cmd:`CoFixpoint` so that one or more bodies can be defined interactively using the proof editing mode. A proof starts by the keyword :cmd:`Proof`. Then Coq enters the proof editing mode diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 59a88771a0..5dba92429e 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -139,7 +139,19 @@ Here we describe only few of them. can be extended by including other paths in which ``*.cm*`` files are searched. For example ``COQ_SRC_SUBDIRS+=user-contrib/Unicoq`` lets you build a plugin containing OCaml code that depends on the - OCaml code of ``Unicoq``. + OCaml code of ``Unicoq`` +:COQFLAGS: + override the flags passed to ``coqc``. By default ``-q``. +:COQEXTRAFLAGS: + extend the flags passed to ``coqc`` +:COQCHKFLAGS: + override the flags passed to ``coqchk``. By default ``-silent -o``. +:COQCHKEXTRAFLAGS: + extend the flags passed to ``coqchk`` +:COQDOCFLAGS: + override the flags passed to ``coqdoc``. By default ``-interpolate -utf8``. +:COQDOCEXTRAFLAGS: + extend the flags passed to ``coqdoc`` **Rule extension** diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 2b128b98fe..88c1e225fd 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -178,7 +178,7 @@ Sequence A sequence is an expression of the following form: .. tacn:: @expr ; @expr - :name: ; + :name: ltac-seq The expression :n:`@expr__1` is evaluated to :n:`v__1`, which must be a tactic value. The tactic :n:`v__1` is applied to the current goal, diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 63cd0f3ead..6fb73a030f 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 da4c3f9d74..d0a0d568ea 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -879,14 +879,6 @@ quantification or an implication. This is equivalent to :n:`clear @ident. ... clear @ident.` -.. tacv:: clearbody @ident - :name: clearbody - - This tactic expects :n:`@ident` to be a local definition then clears its - body. Otherwise said, this tactic turns a definition into an assumption. - -.. exn:: @ident is not a local definition. - .. tacv:: clear - {+ @ident} This tactic clears all the hypotheses except the ones depending in the @@ -901,6 +893,15 @@ quantification or an implication. This clears the hypothesis :n:`@ident` and all the hypotheses that depend on it. +.. tacv:: clearbody {+ @ident} + :name: clearbody + + This tactic expects :n:`{+ @ident}` to be local definitions and clears their + respective bodies. + In other words, it turns the given definitions into assumptions. + +.. exn:: @ident is not a local definition. + .. tacn:: revert {+ @ident} :name: revert @@ -970,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. @@ -2867,8 +2868,8 @@ the conversion in hypotheses :n:`{+ @ident}`. .. coqtop:: all Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x). - Notation "f \o g" := (fcomp f g) (at level 50). Arguments fcomp {A B C} f g x /. + Notation "f \o g" := (fcomp f g) (at level 50). After that command the expression :g:`(f \o g)` is left untouched by ``simpl`` while :g:`((f \o g) t)` is reduced to :g:`(f (g t))`. @@ -3702,19 +3703,24 @@ Setting implicit automation tactics time the term argument of a tactic has one of its holes not fully resolved. - .. example:: + .. deprecated:: 8.9 - .. coqtop:: all + This command is deprecated. Use :ref:`typeclasses <typeclasses>` or + :ref:`tactics-in-terms <tactics-in-terms>` instead. - Parameter quo : nat -> forall n:nat, n<>0 -> nat. - Notation "x // y" := (quo x y _) (at level 40). - Declare Implicit Tactic assumption. - Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }. - intros. - exists (n // m). + .. example:: + + .. coqtop:: all - The tactic ``exists (n // m)`` did not fail. The hole was solved - by ``assumption`` so that it behaved as ``exists (quo n m H)``. + Parameter quo : nat -> forall n:nat, n<>0 -> nat. + Notation "x // y" := (quo x y _) (at level 40). + Declare Implicit Tactic assumption. + Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }. + intros. + exists (n // m). + + The tactic ``exists (n // m)`` did not fail. The hole was solved + by ``assumption`` so that it behaved as ``exists (quo n m H)``. .. _decisionprocedures: @@ -3943,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 |