diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/README.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/README.template.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/addendum/generalized-rewriting.rst | 72 | ||||
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 14 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 14 | ||||
| -rw-r--r-- | doc/sphinx/addendum/parallel-proof-processing.rst | 54 | ||||
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 14 | ||||
| -rw-r--r-- | doc/sphinx/language/cic.rst | 382 | ||||
| -rw-r--r-- | doc/sphinx/language/coq-library.rst | 38 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 25 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 108 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 16 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 170 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 96 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 703 | ||||
| -rw-r--r-- | doc/sphinx/refman-preamble.sty | 10 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 77 |
17 files changed, 1047 insertions, 754 deletions
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index a20b74822c..e4f078c1d6 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -416,12 +416,12 @@ Omitting annotations DO .. code:: - .. tacv:: assert @form as @intro_pattern + .. tacv:: assert @form as @simple_intropattern DON'T .. code:: - .. tacv:: assert form as intro_pattern + .. tacv:: assert form as simple_intropattern Using the ``.. coqtop::`` directive for syntax highlighting ----------------------------------------------------------- diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index 11f0cdc008..81f25bf274 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -172,12 +172,12 @@ Omitting annotations DO .. code:: - .. tacv:: assert @form as @intro_pattern + .. tacv:: assert @form as @simple_intropattern DON'T .. code:: - .. tacv:: assert form as intro_pattern + .. tacv:: assert form as simple_intropattern Using the ``.. coqtop::`` directive for syntax highlighting ----------------------------------------------------------- diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index e468cc63cd..b606fb4dd2 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -714,47 +714,47 @@ following grammar: .. productionlist:: rewriting s, t, u : `strategy` - : | `lemma` - : | `lemma_right_to_left` - : | `failure` - : | `identity` - : | `reflexivity` - : | `progress` - : | `failure_catch` - : | `composition` - : | `left_biased_choice` - : | `iteration_one_or_more` - : | `iteration_zero_or_more` - : | `one_subterm` - : | `all_subterms` - : | `innermost_first` - : | `outermost_first` - : | `bottom_up` - : | `top_down` - : | `apply_hint` - : | `any_of_the_terms` - : | `apply_reduction` - : | `fold_expression` + : `lemma` + : `lemma_right_to_left` + : `failure` + : `identity` + : `reflexivity` + : `progress` + : `failure_catch` + : `composition` + : `left_biased_choice` + : `iteration_one_or_more` + : `iteration_zero_or_more` + : `one_subterm` + : `all_subterms` + : `innermost_first` + : `outermost_first` + : `bottom_up` + : `top_down` + : `apply_hint` + : `any_of_the_terms` + : `apply_reduction` + : `fold_expression` .. productionlist:: rewriting - strategy : "(" `s` ")" + strategy : ( `s` ) lemma : `c` - lemma_right_to_left : "<-" `c` - failure : `fail` - identity : `id` - reflexivity : `refl` - progress : `progress` `s` - failure_catch : `try` `s` - composition : `s` ";" `u` + lemma_right_to_left : <- `c` + failure : fail + identity : id + reflexivity : refl + progress : progress `s` + failure_catch : try `s` + composition : `s` ; `u` left_biased_choice : choice `s` `t` - iteration_one_or_more : `repeat` `s` - iteration_zero_or_more : `any` `s` + iteration_one_or_more : repeat `s` + iteration_zero_or_more : any `s` one_subterm : subterm `s` all_subterms : subterms `s` - innermost_first : `innermost` `s` - outermost_first : `outermost` `s` - bottom_up : `bottomup` `s` - top_down : `topdown` `s` + innermost_first : innermost `s` + outermost_first : outermost `s` + bottom_up : bottomup `s` + top_down : topdown `s` apply_hint : hints `hintdb` any_of_the_terms : terms (`c`)+ apply_reduction : eval `redexpr` @@ -767,7 +767,7 @@ primitive fixpoint operator: .. productionlist:: rewriting try `s` : choice `s` `id` any `s` : fix `u`. try (`s` ; `u`) - repeat `s` : `s` ; `any` `s` + repeat `s` : `s` ; any `s` bottomup s : fix `bu`. (choice (progress (subterms bu)) s) ; try bu topdown s : fix `td`. (choice s (progress (subterms td))) ; try td innermost s : fix `i`. (choice (subterm i) s) diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 64e2d7c4ab..e5b41be691 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -41,8 +41,8 @@ Formally, the syntax of a classes is defined as: .. productionlist:: class: `qualid` - : | Sortclass - : | Funclass + : Sortclass + : Funclass Coercions @@ -184,10 +184,10 @@ Figure :ref:`vernacular` as follows: \comindex{Hypothesis \mbox{\rm (and coercions)}} .. productionlist:: - assumption : assumption_keyword assums . - assums : simple_assums - : | (simple_assums) ... (simple_assums) - simple_assums : ident ... ident :[>] term + assumption : `assumption_keyword` `assums` . + assums : `simple_assums` + : (`simple_assums`) ... (`simple_assums`) + simple_assums : `ident` ... `ident` :[>] `term` If the extra ``>`` is present before the type of some assumptions, these assumptions are declared as coercions. @@ -203,7 +203,7 @@ grammar of inductive types from Figure :ref:`vernacular` as follows: .. productionlist:: inductive : Inductive `ind_body` with ... with `ind_body` - : | CoInductive `ind_body` with ... with `ind_body` + : CoInductive `ind_body` with ... with `ind_body` ind_body : `ident` [ `binders` ] : `term` := [[|] `constructor` | ... | `constructor` ] constructor : `ident` [ `binders` ] [:[>] `term` ] diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index fd66de427c..b076aac1ed 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -38,7 +38,7 @@ The tactics solve propositional formulas parameterized by atomic arithmetic expressions interpreted over a domain :math:`D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}`. The syntax of the formulas is the following: - .. productionlist:: `F` + .. productionlist:: F F : A ∣ P ∣ True ∣ False ∣ F ∧ F ∣ F ∨ F ∣ F ↔ F ∣ F → F ∣ ¬ F A : p = p ∣ p > p ∣ p < p ∣ p ≥ p ∣ p ≤ p p : c ∣ x ∣ −p ∣ p − p ∣ p + p ∣ p × p ∣ p ^ n @@ -145,7 +145,7 @@ weakness, the :tacn:`lia` tactic is using recursively a combination of: + linear *positivstellensatz* refutations; + cutting plane proofs; + case split. - + Cutting plane proofs ~~~~~~~~~~~~~~~~~~~~~~ @@ -250,6 +250,16 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. .. [#] Support for :g:`nat` and :g:`N` is obtained by pre-processing the goal with the ``zify`` tactic. +.. [#] Support for :g:`Z.div` and :g:`Z.modulo` may be obtained by + pre-processing the goal with the ``Z.div_mod_to_equations`` tactic (you may + need to manually run ``zify`` first). +.. [#] Support for :g:`Z.quot` and :g:`Z.rem` may be obtained by pre-processing + the goal with the ``Z.quot_rem_to_equations`` tactic (you may need to manually + run ``zify`` first). +.. [#] Note that support for :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot`, and + :g:`Z.rem` may be simultaneously obtained by pre-processing the goal with the + ``Z.to_euclidean_division_equations`` tactic (you may need to manually run + ``zify`` first). .. [#] Sources and binaries can be found at https://projects.coin-or.org/Csdp .. [#] Variants deal with equalities and strict inequalities. .. [#] In practice, the oracle might fail to produce such a refutation. diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst index 8b7214e2ab..903ee115c9 100644 --- a/doc/sphinx/addendum/parallel-proof-processing.rst +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -52,7 +52,7 @@ in interactive mode. It is not strictly mandatory in batch mode if it is not the first time the file is compiled and if the file itself did not change. When the proof does not begin with Proof using, the system records in an -auxiliary file, produced along with the `.vo` file, the list of section +auxiliary file, produced along with the ``.vo`` file, the list of section variables used. Automatic suggestion of proof annotations @@ -154,22 +154,22 @@ to a worker process. The threshold can be configured with Batch mode --------------- -When |Coq| is used as a batch compiler by running `coqc` or `coqtop` --compile, it produces a `.vo` file for each `.v` file. A `.vo` file contains, -among other things, theorem statements and proofs. Hence to produce a -.vo |Coq| need to process all the proofs of the `.v` file. +When |Coq| is used as a batch compiler by running ``coqc``, it produces +a ``.vo`` file for each ``.v`` file. A ``.vo`` file contains, among other +things, theorem statements and proofs. Hence to produce a .vo |Coq| +need to process all the proofs of the ``.v`` file. The asynchronous processing of proofs can decouple the generation of a -compiled file (like the `.vo` one) that can be loaded by ``Require`` from the +compiled file (like the ``.vo`` one) that can be loaded by ``Require`` from the generation and checking of the proof objects. The ``-quick`` flag can be -passed to `coqc` or `coqtop` to produce, quickly, `.vio` files. -Alternatively, when using a Makefile produced by `coq_makefile`, +passed to ``coqc`` or ``coqtop`` to produce, quickly, ``.vio`` files. +Alternatively, when using a Makefile produced by ``coq_makefile``, the ``quick`` target can be used to compile all files using the ``-quick`` flag. -A `.vio` file can be loaded using ``Require`` exactly as a `.vo` file but +A ``.vio`` file can be loaded using ``Require`` exactly as a ``.vo`` file but proofs will not be available (the Print command produces an error). Moreover, some universe constraints might be missing, so universes -inconsistencies might go unnoticed. A `.vio` file does not contain proof +inconsistencies might go unnoticed. A ``.vio`` file does not contain proof objects, but proof tasks, i.e. what a worker process can transform into a proof object. @@ -177,52 +177,52 @@ Compiling a set of files with the ``-quick`` flag allows one to work, interactively, on any file without waiting for all the proofs to be checked. -When working interactively, one can fully check all the `.v` files by -running `coqc` as usual. +When working interactively, one can fully check all the ``.v`` files by +running ``coqc`` as usual. -Alternatively one can turn each `.vio` into the corresponding `.vo`. All +Alternatively one can turn each ``.vio`` into the corresponding ``.vo``. All .vio files can be processed in parallel, hence this alternative might be faster. The command ``coqtop -schedule-vio2vo 2 a b c`` can be used to -obtain a good scheduling for two workers to produce `a.vo`, `b.vo`, and -`c.vo`. When using a Makefile produced by `coq_makefile`, the ``vio2vo`` target -can be used for that purpose. Variable `J` should be set to the number +obtain a good scheduling for two workers to produce ``a.vo``, ``b.vo``, and +``c.vo``. When using a Makefile produced by ``coq_makefile``, the ``vio2vo`` target +can be used for that purpose. Variable ``J`` should be set to the number of workers, e.g. ``make vio2vo J=2``. The only caveat is that, while the -.vo files obtained from `.vio` files are complete (they contain all proof +.vo files obtained from ``.vio`` files are complete (they contain all proof terms and universe constraints), the satisfiability of all universe constraints has not been checked globally (they are checked to be consistent for every single proof). Constraints will be checked when -these `.vo` files are (recursively) loaded with ``Require``. +these ``.vo`` files are (recursively) loaded with ``Require``. There is an extra, possibly even faster, alternative: just check the -proof tasks stored in `.vio` files without producing the `.vo` files. This +proof tasks stored in ``.vio`` files without producing the ``.vo`` files. This is possibly faster because all the proof tasks are independent, hence one can further partition the job to be done between workers. The ``coqtop -schedule-vio-checking 6 a b c`` command can be used to obtain a -good scheduling for 6 workers to check all the proof tasks of `a.vio`, -`b.vio`, and `c.vio`. Auxiliary files are used to predict how long a proof +good scheduling for 6 workers to check all the proof tasks of ``a.vio``, +``b.vio``, and ``c.vio``. Auxiliary files are used to predict how long a proof task will take, assuming it will take the same amount of time it took last time. When using a Makefile produced by coq_makefile, the -``checkproofs`` target can be used to check all `.vio` files. Variable `J` +``checkproofs`` target can be used to check all ``.vio`` files. Variable ``J`` should be set to the number of workers, e.g. ``make checkproofs J=6``. As -when converting `.vio` files to `.vo` files, universe constraints are not +when converting ``.vio`` files to ``.vo`` files, universe constraints are not checked to be globally consistent. Hence this compilation mode is only useful for quick regression testing and on developments not making -heavy use of the `Type` hierarchy. +heavy use of the ``Type`` hierarchy. Limiting the number of parallel workers -------------------------------------------- Many |Coq| processes may run on the same computer, and each of them may -start many additional worker processes. The `coqworkmgr` utility lets +start many additional worker processes. The ``coqworkmgr`` utility lets one limit the number of workers, globally. The utility accepts the ``-j`` argument to specify the maximum number of -workers (defaults to 2). `coqworkmgr` automatically starts in the +workers (defaults to 2). ``coqworkmgr`` automatically starts in the background and prints an environment variable assignment like ``COQWORKMGR_SOCKET=localhost:45634``. The user must set this variable in all the shells from which |Coq| processes will be started. If one uses just one terminal running the bash shell, then ``export ‘coqworkmgr -j 4‘`` will do the job. -After that, all |Coq| processes, e.g. `coqide` and `coqc`, will respect the +After that, all |Coq| processes, e.g. ``coqide`` and ``coqc``, will respect the limit, globally. diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 99d689132d..8204d93fa7 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -308,13 +308,13 @@ The syntax for adding a new ring is .. 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` + : 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. diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index cc5d9d6205..67683902cd 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -84,7 +84,7 @@ implemented using *algebraic universes*. An algebraic universe :math:`u` is either a variable (a qualified identifier with a number) or a successor of an algebraic universe (an expression :math:`u+1`), or an upper bound of algebraic universes (an -expression :math:`\max(u 1 ,...,u n )`), or the base universe (the expression +expression :math:`\max(u_1 ,...,u_n )`), or the base universe (the expression :math:`0`) which corresponds, in the arity of template polymorphic inductive types (see Section :ref:`well-formed-inductive-definitions`), @@ -117,24 +117,24 @@ the following rules. #. variables, hereafter ranged over by letters :math:`x`, :math:`y`, etc., are terms #. constants, hereafter ranged over by letters :math:`c`, :math:`d`, etc., are terms. #. if :math:`x` is a variable and :math:`T`, :math:`U` are terms then - :math:`∀ x:T,U` (:g:`forall x:T, U` in |Coq| concrete syntax) is a term. - If :math:`x` occurs in :math:`U`, :math:`∀ x:T,U` reads as + :math:`∀ x:T,~U` (:g:`forall x:T, U` in |Coq| concrete syntax) is a term. + If :math:`x` occurs in :math:`U`, :math:`∀ x:T,~U` reads as “for all :math:`x` of type :math:`T`, :math:`U`”. - As :math:`U` depends on :math:`x`, one says that :math:`∀ x:T,U` is + As :math:`U` depends on :math:`x`, one says that :math:`∀ x:T,~U` is a *dependent product*. If :math:`x` does not occur in :math:`U` then - :math:`∀ x:T,U` reads as + :math:`∀ x:T,~U` reads as “if :math:`T` then :math:`U`”. A *non dependent product* can be written: :math:`T \rightarrow U`. #. if :math:`x` is a variable and :math:`T`, :math:`u` are terms then - :math:`λ x:T . u` (:g:`fun x:T => u` + :math:`λ x:T .~u` (:g:`fun x:T => u` in |Coq| concrete syntax) is a term. This is a notation for the - λ-abstraction of λ-calculus :cite:`Bar81`. The term :math:`λ x:T . u` is a function + λ-abstraction of λ-calculus :cite:`Bar81`. The term :math:`λ x:T .~u` is a function which maps elements of :math:`T` to the expression :math:`u`. #. if :math:`t` and :math:`u` are terms then :math:`(t~u)` is a term (:g:`t u` in |Coq| concrete syntax). The term :math:`(t~u)` reads as “t applied to u”. -#. if :g:`x` is a variable, and :math:`t`, :math:`T` and :math:`u` are - terms then :g:`let x:=t:T in u` is +#. if :math:`x` is a variable, and :math:`t`, :math:`T` and :math:`u` are + terms then :math:`\letin{x}{t:T}{u}` is a term which denotes the term :math:`u` where the variable :math:`x` is locally bound to :math:`t` of type :math:`T`. This stands for the common “let-in” construction of functional programs such as ML or Scheme. @@ -145,7 +145,7 @@ the following rules. **Free variables.** The notion of free variables is defined as usual. In the expressions -:g:`λx:T. U` and :g:`∀ x:T, U` the occurrences of :math:`x` in :math:`U` are bound. +:math:`λx:T.~U` and :math:`∀ x:T,~U` the occurrences of :math:`x` in :math:`U` are bound. .. _Substitution: @@ -172,11 +172,11 @@ implicative proposition, to denote :math:`\nat →\Prop` which is the type of unary predicates over the natural numbers, etc. Let us assume that ``mult`` is a function of type :math:`\nat→\nat→\nat` and ``eqnat`` a -predicate of type \nat→\nat→ \Prop. The λ-abstraction can serve to build -“ordinary” functions as in :math:`λ x:\nat.(\kw{mult}~x~x)` (i.e. +predicate of type :math:`\nat→\nat→ \Prop`. The λ-abstraction can serve to build +“ordinary” functions as in :math:`λ x:\nat.~(\kw{mult}~x~x)` (i.e. :g:`fun x:nat => mult x x` in |Coq| notation) but may build also predicates over the natural -numbers. For instance :math:`λ x:\nat.(\kw{eqnat}~x~0)` +numbers. For instance :math:`λ x:\nat.~(\kw{eqnat}~x~0)` (i.e. :g:`fun x:nat => eqnat x 0` in |Coq| notation) will represent the predicate of one variable :math:`x` which asserts the equality of :math:`x` with :math:`0`. This predicate has type @@ -186,7 +186,7 @@ object :math:`P~t` of type :math:`\Prop`, namely a proposition. Furthermore :g:`forall x:nat, P x` will represent the type of functions which associate to each natural number :math:`n` an object of type :math:`(P~n)` and -consequently represent the type of proofs of the formula “:math:`∀ x. P(x`)”. +consequently represent the type of proofs of the formula “:math:`∀ x.~P(x)`”. .. _Typing-rules: @@ -206,7 +206,7 @@ A *local context* is an ordered list of *local declarations* of names which we call *variables*. The declaration of some variable :math:`x` is either a *local assumption*, written :math:`x:T` (:math:`T` is a type) or a *local definition*, written :math:`x:=t:T`. We use brackets to write local contexts. -A typical example is :math:`[x:T;y:=u:U;z:V]`. Notice that the variables +A typical example is :math:`[x:T;~y:=u:U;~z:V]`. Notice that the variables declared in a local context must be distinct. If :math:`Γ` is a local context that declares some :math:`x`, we write :math:`x ∈ Γ`. By writing :math:`(x:T) ∈ Γ` we mean that either :math:`x:T` is an @@ -232,9 +232,9 @@ A *global assumption* will be represented in the global environment as :math:`(c:T)` which assumes the name :math:`c` to be of some type :math:`T`. A *global definition* will be represented in the global environment as :math:`c:=t:T` which defines the name :math:`c` to have value :math:`t` and type :math:`T`. We shall call -such names *constants*. For the rest of the chapter, the :math:`E;c:T` denotes +such names *constants*. For the rest of the chapter, the :math:`E;~c:T` denotes the global environment :math:`E` enriched with the global assumption :math:`c:T`. -Similarly, :math:`E;c:=t:T` denotes the global environment :math:`E` enriched with the +Similarly, :math:`E;~c:=t:T` denotes the global environment :math:`E` enriched with the global definition :math:`(c:=t:T)`. The rules for inductive definitions (see Section @@ -284,14 +284,14 @@ following rules. s \in \Sort c \notin E ------------ - \WF{E;c:T}{} + \WF{E;~c:T}{} .. inference:: W-Global-Def \WTE{}{t}{T} c \notin E --------------- - \WF{E;c:=t:T}{} + \WF{E;~c:=t:T}{} .. inference:: Ax-Prop @@ -328,10 +328,10 @@ following rules. .. inference:: Prod-Prop \WTEG{T}{s} - s \in {\Sort} + s \in \Sort \WTE{\Gamma::(x:T)}{U}{\Prop} ----------------------------- - \WTEG{\forall~x:T,U}{\Prop} + \WTEG{∀ x:T,~U}{\Prop} .. inference:: Prod-Set @@ -339,25 +339,25 @@ following rules. s \in \{\Prop, \Set\} \WTE{\Gamma::(x:T)}{U}{\Set} ---------------------------- - \WTEG{\forall~x:T,U}{\Set} + \WTEG{∀ x:T,~U}{\Set} .. inference:: Prod-Type \WTEG{T}{\Type(i)} \WTE{\Gamma::(x:T)}{U}{\Type(i)} -------------------------------- - \WTEG{\forall~x:T,U}{\Type(i)} + \WTEG{∀ x:T,~U}{\Type(i)} .. inference:: Lam - \WTEG{\forall~x:T,U}{s} + \WTEG{∀ x:T,~U}{s} \WTE{\Gamma::(x:T)}{t}{U} ------------------------------------ - \WTEG{\lb x:T\mto t}{\forall x:T, U} + \WTEG{λ x:T\mto t}{∀ x:T,~U} .. inference:: App - \WTEG{t}{\forall~x:U,T} + \WTEG{t}{∀ x:U,~T} \WTEG{u}{U} ------------------------------ \WTEG{(t\ u)}{\subst{T}{x}{u}} @@ -383,7 +383,7 @@ following rules. .. note:: We may have :math:`\letin{x}{t:T}{u}` well-typed without having - :math:`((λ x:T.u) t)` well-typed (where :math:`T` is a type of + :math:`((λ x:T.~u)~t)` well-typed (where :math:`T` is a type of :math:`t`). This is because the value :math:`t` associated to :math:`x` may be used in a conversion rule (see Section :ref:`Conversion-rules`). @@ -406,18 +406,18 @@ can decide if two programs are *intentionally* equal (one says We want to be able to identify some terms as we can identify the application of a function to a given argument with its result. For -instance the identity function over a given type T can be written -:math:`λx:T. x`. In any global environment :math:`E` and local context +instance the identity function over a given type :math:`T` can be written +:math:`λx:T.~x`. In any global environment :math:`E` and local context :math:`Γ`, we want to identify any object :math:`a` (of type -:math:`T`) with the application :math:`((λ x:T. x) a)`. We define for +:math:`T`) with the application :math:`((λ x:T.~x)~a)`. We define for this a *reduction* (or a *conversion*) rule we call :math:`β`: .. math:: - E[Γ] ⊢ ((λx:T. t) u)~\triangleright_β~\subst{t}{x}{u} + E[Γ] ⊢ ((λx:T.~t)~u)~\triangleright_β~\subst{t}{x}{u} We say that :math:`\subst{t}{x}{u}` is the *β-contraction* of -:math:`((λx:T. t) u)` and, conversely, that :math:`((λ x:T. t) u)` is the +:math:`((λx:T.~t)~u)` and, conversely, that :math:`((λ x:T.~t)~u)` is the *β-expansion* of :math:`\subst{t}{x}{u}`. According to β-reduction, terms of the *Calculus of Inductive @@ -481,7 +481,7 @@ destroyed, this reduction differs from δ-reduction. It is called \WTEG{u}{U} \WTE{\Gamma::(x:=u:U)}{t}{T} -------------- - E[Γ] ⊢ \letin{x}{u}{t}~\triangleright_ζ~\subst{t}{x}{u} + E[Γ] ⊢ \letin{x}{u:U}{t}~\triangleright_ζ~\subst{t}{x}{u} .. _eta-expansion: @@ -490,10 +490,10 @@ destroyed, this reduction differs from δ-reduction. It is called ~~~~~~~~~~~ Another important concept is η-expansion. It is legal to identify any -term :math:`t` of functional type :math:`∀ x:T, U` with its so-called η-expansion +term :math:`t` of functional type :math:`∀ x:T,~U` with its so-called η-expansion .. math:: - λx:T. (t~x) + λx:T.~(t~x) for :math:`x` an arbitrary variable name fresh in :math:`t`. @@ -503,26 +503,26 @@ for :math:`x` an arbitrary variable name fresh in :math:`t`. We deliberately do not define η-reduction: .. math:: - λ x:T. (t~x) \not\triangleright_η t + λ x:T.~(t~x)~\not\triangleright_η~t This is because, in general, the type of :math:`t` need not to be convertible - to the type of :math:`λ x:T. (t~x)`. E.g., if we take :math:`f` such that: + to the type of :math:`λ x:T.~(t~x)`. E.g., if we take :math:`f` such that: .. math:: - f : ∀ x:\Type(2),\Type(1) + f ~:~ ∀ x:\Type(2),~\Type(1) then .. math:: - λ x:\Type(1),(f~x) : ∀ x:\Type(1),\Type(1) + λ x:\Type(1).~(f~x) ~:~ ∀ x:\Type(1),~\Type(1) We could not allow .. math:: - λ x:Type(1),(f x) \triangleright_η f + λ x:\Type(1).~(f~x) ~\triangleright_η~ f - because the type of the reduced term :math:`∀ x:\Type(2),\Type(1)` would not be - convertible to the type of the original term :math:`∀ x:\Type(1),\Type(1).` + because the type of the reduced term :math:`∀ x:\Type(2),~\Type(1)` would not be + convertible to the type of the original term :math:`∀ x:\Type(1),~\Type(1)`. .. _convertibility: @@ -541,10 +541,10 @@ global environment :math:`E` and local context :math:`Γ` iff there exist terms :math:`u_1` and :math:`u_2` such that :math:`E[Γ] ⊢ t_1 \triangleright … \triangleright u_1` and :math:`E[Γ] ⊢ t_2 \triangleright … \triangleright u_2` and either :math:`u_1` and :math:`u_2` are identical, or they are convertible up to η-expansion, -i.e. :math:`u_1` is :math:`λ x:T. u_1'` and :math:`u_2 x` is +i.e. :math:`u_1` is :math:`λ x:T.~u_1'` and :math:`u_2 x` is recursively convertible to :math:`u_1'` , or, symmetrically, -:math:`u_2` is :math:`λx:T. u_2'` -and :math:`u_1 x` is recursively convertible to u_2′ . We then write +:math:`u_2` is :math:`λx:T.~u_2'` +and :math:`u_1 x` is recursively convertible to :math:`u_2'`. We then write :math:`E[Γ] ⊢ t_1 =_{βδιζη} t_2` . Apart from this we consider two instances of polymorphic and @@ -601,8 +601,8 @@ Subtyping rules ------------------- At the moment, we did not take into account one rule between universes -which says that any term in a universe of index i is also a term in -the universe of index i+1 (this is the *cumulativity* rule of |Cic|). +which says that any term in a universe of index :math:`i` is also a term in +the universe of index :math:`i+1` (this is the *cumulativity* rule of |Cic|). This property extends the equivalence relation of convertibility into a *subtyping* relation inductively defined by: @@ -614,25 +614,25 @@ a *subtyping* relation inductively defined by: :math:`E[Γ] ⊢ \Prop ≤_{βδιζη} \Type(i)`, for any :math:`i` #. if :math:`E[Γ] ⊢ T =_{βδιζη} U` and :math:`E[Γ::(x:T)] ⊢ T' ≤_{βδιζη} U'` then - :math:`E[Γ] ⊢ ∀x:T, T′ ≤_{βδιζη} ∀ x:U, U′`. + :math:`E[Γ] ⊢ ∀x:T,~T′ ≤_{βδιζη} ∀ x:U,~U′`. #. if :math:`\ind{p}{Γ_I}{Γ_C}` is a universe polymorphic and cumulative (see Chapter :ref:`polymorphicuniverses`) inductive type (see below) and - :math:`(t : ∀Γ_P ,∀Γ_{\mathit{Arr}(t)}, \Sort)∈Γ_I` + :math:`(t : ∀Γ_P ,∀Γ_{\mathit{Arr}(t)}, S)∈Γ_I` and - :math:`(t' : ∀Γ_P' ,∀Γ_{\mathit{Arr}(t)}', \Sort')∈Γ_I` + :math:`(t' : ∀Γ_P' ,∀Γ_{\mathit{Arr}(t)}', S')∈Γ_I` are two different instances of *the same* inductive type (differing only in universe levels) with constructors .. math:: - [c_1 : ∀Γ_P ,∀ T_{1,1} … T_{1,n_1} , t~v_{1,1} … v_{1,m} ;…; - c_k : ∀Γ_P ,∀ T_{k,1} … T_{k,n_k} ,t~v_{n,1} … v_{n,m} ] + [c_1 : ∀Γ_P ,∀ T_{1,1} … T_{1,n_1} ,~t~v_{1,1} … v_{1,m} ;~…;~ + c_k : ∀Γ_P ,∀ T_{k,1} … T_{k,n_k} ,~t~v_{k,1} … v_{k,m} ] and .. math:: - [c_1 : ∀Γ_P' ,∀ T_{1,1}' … T_{1,n_1}' , t'~v_{1,1}' … v_{1,m}' ;…; - c_k : ∀Γ_P' ,∀ T_{k,1}' … T_{k,n_k}' ,t'~v_{n,1}' … v_{n,m}' ] + [c_1 : ∀Γ_P' ,∀ T_{1,1}' … T_{1,n_1}' ,~t'~v_{1,1}' … v_{1,m}' ;~…;~ + c_k : ∀Γ_P' ,∀ T_{k,1}' … T_{k,n_k}' ,~t'~v_{k,1}' … v_{k,m}' ] respectively then @@ -656,8 +656,8 @@ a *subtyping* relation inductively defined by: .. math:: E[Γ] ⊢ A_i ≤_{βδιζη} A_i' - where :math:`Γ_{\mathit{Arr}(t)} = [a_1 : A_1 ; … ; a_l : A_l ]` and - :math:`Γ_{\mathit{Arr}(t)}' = [a_1 : A_1'; … ; a_l : A_l']`. + where :math:`Γ_{\mathit{Arr}(t)} = [a_1 : A_1 ;~ … ;~a_l : A_l ]` and + :math:`Γ_{\mathit{Arr}(t)}' = [a_1 : A_1';~ … ;~a_l : A_l']`. The conversion rule up to subtyping is now exactly: @@ -677,19 +677,19 @@ The conversion rule up to subtyping is now exactly: form*. There are several ways (or strategies) to apply the reduction rules. Among them, we have to mention the *head reduction* which will play an important role (see Chapter :ref:`tactics`). Any term :math:`t` can be written as -:math:`λ x_1 :T_1 . … λ x_k :T_k . (t_0~t_1 … t_n )` where :math:`t_0` is not an +:math:`λ x_1 :T_1 .~… λ x_k :T_k .~(t_0~t_1 … t_n )` where :math:`t_0` is not an application. We say then that :math:`t_0` is the *head of* :math:`t`. If we assume -that :math:`t_0` is :math:`λ x:T. u_0` then one step of β-head reduction of :math:`t` is: +that :math:`t_0` is :math:`λ x:T.~u_0` then one step of β-head reduction of :math:`t` is: .. math:: - λ x_1 :T_1 . … λ x_k :T_k . (λ x:T. u_0~t_1 … t_n ) \triangleright - λ (x_1 :T_1 )…(x_k :T_k ). (\subst{u_0}{x}{t_1}~t_2 … t_n ) + λ x_1 :T_1 .~… λ x_k :T_k .~(λ x:T.~u_0~t_1 … t_n ) ~\triangleright~ + λ (x_1 :T_1 )…(x_k :T_k ).~(\subst{u_0}{x}{t_1}~t_2 … t_n ) Iterating the process of head reduction until the head of the reduced term is no more an abstraction leads to the *β-head normal form* of :math:`t`: .. math:: - t \triangleright … \triangleright λ x_1 :T_1 . …λ x_k :T_k . (v~u_1 … u_m ) + t \triangleright … \triangleright λ x_1 :T_1 .~…λ x_k :T_k .~(v~u_1 … u_m ) where :math:`v` is not an abstraction (nor an application). Note that the head normal form must not be confused with the normal form since some :math:`u_i` @@ -713,12 +713,12 @@ Formally, we can represent any *inductive definition* as These inductive definitions, together with global assumptions and global definitions, then form the global environment. Additionally, -for any :math:`p` there always exists :math:`Γ_P =[a_1 :A_1 ;…;a_p :A_p ]` such that +for any :math:`p` there always exists :math:`Γ_P =[a_1 :A_1 ;~…;~a_p :A_p ]` such that each :math:`T` in :math:`(t:T)∈Γ_I \cup Γ_C` can be written as: :math:`∀Γ_P , T'` where :math:`Γ_P` is called the *context of parameters*. Furthermore, we must have that each :math:`T` in :math:`(t:T)∈Γ_I` can be written as: :math:`∀Γ_P,∀Γ_{\mathit{Arr}(t)}, S` where -:math:`Γ_{\mathit{Arr}(t)}` is called the *Arity* of the inductive type t and :math:`S` is called -the sort of the inductive type t (not to be confused with :math:`\Sort` which is the set of sorts). +:math:`Γ_{\mathit{Arr}(t)}` is called the *Arity* of the inductive type :math:`t` and :math:`S` is called +the sort of the inductive type :math:`t` (not to be confused with :math:`\Sort` which is the set of sorts). .. example:: @@ -726,8 +726,8 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is .. math:: \ind{1}{[\List:\Set→\Set]}{\left[\begin{array}{rcl} - \Nil & : & \forall A:\Set,\List~A \\ - \cons & : & \forall A:\Set, A→ \List~A→ \List~A + \Nil & : & ∀ A:\Set,~\List~A \\ + \cons & : & ∀ A:\Set,~A→ \List~A→ \List~A \end{array} \right]} @@ -771,8 +771,8 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is \odd&:&\nat → \Prop \end{array}\right]} {\left[\begin{array}{rcl} \evenO &:& \even~0\\ - \evenS &:& \forall n, \odd~n → \even~(\kw{S}~n)\\ - \oddS &:& \forall n, \even~n → \odd~(\kw{S}~n) + \evenS &:& ∀ n,~\odd~n → \even~(\nS~n)\\ + \oddS &:& ∀ n,~\even~n → \odd~(\nS~n) \end{array}\right]} which corresponds to the result of the |Coq| declaration: @@ -792,7 +792,7 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is Types of inductive objects ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We have to give the type of constants in a global environment E which +We have to give the type of constants in a global environment :math:`E` which contains an inductive declaration. .. inference:: Ind @@ -820,9 +820,9 @@ contains an inductive declaration. \begin{array}{l} E[Γ] ⊢ \even : \nat→\Prop\\ E[Γ] ⊢ \odd : \nat→\Prop\\ - E[Γ] ⊢ \even\_O : \even~O\\ - E[Γ] ⊢ \even\_S : \forall~n:\nat, \odd~n → \even~(S~n)\\ - E[Γ] ⊢ \odd\_S : \forall~n:\nat, \even~n → \odd~(S~n) + E[Γ] ⊢ \evenO : \even~\nO\\ + E[Γ] ⊢ \evenS : ∀ n:\nat,~\odd~n → \even~(\nS~n)\\ + E[Γ] ⊢ \oddS : ∀ n:\nat,~\even~n → \odd~(\nS~n) \end{array} @@ -842,11 +842,11 @@ Arity of a given sort +++++++++++++++++++++ A type :math:`T` is an *arity of sort* :math:`s` if it converts to the sort :math:`s` or to a -product :math:`∀ x:T,U` with :math:`U` an arity of sort :math:`s`. +product :math:`∀ x:T,~U` with :math:`U` an arity of sort :math:`s`. .. example:: - :math:`A→\Set` is an arity of sort :math:`\Set`. :math:`∀ A:\Prop,A→ \Prop` is an arity of sort + :math:`A→\Set` is an arity of sort :math:`\Set`. :math:`∀ A:\Prop,~A→ \Prop` is an arity of sort :math:`\Prop`. @@ -858,21 +858,21 @@ sort :math:`s`. .. example:: - :math:`A→ Set` and :math:`∀ A:\Prop,A→ \Prop` are arities. + :math:`A→ \Set` and :math:`∀ A:\Prop,~A→ \Prop` are arities. -Type constructor -++++++++++++++++ -We say that T is a *type of constructor of I* in one of the following +Type of constructor ++++++++++++++++++++ +We say that :math:`T` is a *type of constructor of* :math:`I` in one of the following two cases: + :math:`T` is :math:`(I~t_1 … t_n )` -+ :math:`T` is :math:`∀ x:U,T'` where :math:`T'` is also a type of constructor of :math:`I` ++ :math:`T` is :math:`∀ x:U,~T'` where :math:`T'` is also a type of constructor of :math:`I` .. example:: :math:`\nat` and :math:`\nat→\nat` are types of constructor of :math:`\nat`. - :math:`∀ A:Type,\List~A` and :math:`∀ A:Type,A→\List~A→\List~A` are types of constructor of :math:`\List`. + :math:`∀ A:\Type,~\List~A` and :math:`∀ A:\Type,~A→\List~A→\List~A` are types of constructor of :math:`\List`. .. _positivity: @@ -883,7 +883,7 @@ The type of constructor :math:`T` will be said to *satisfy the positivity condition* for a constant :math:`X` in the following cases: + :math:`T=(X~t_1 … t_n )` and :math:`X` does not occur free in any :math:`t_i` -+ :math:`T=∀ x:U,V` and :math:`X` occurs only strictly positively in :math:`U` and the type :math:`V` ++ :math:`T=∀ x:U,~V` and :math:`X` occurs only strictly positively in :math:`U` and the type :math:`V` satisfies the positivity condition for :math:`X`. Strict positivity @@ -895,13 +895,13 @@ cases: + :math:`X` does not occur in :math:`T` + :math:`T` converts to :math:`(X~t_1 … t_n )` and :math:`X` does not occur in any of :math:`t_i` -+ :math:`T` converts to :math:`∀ x:U,V` and :math:`X` does not occur in type :math:`U` but occurs ++ :math:`T` converts to :math:`∀ x:U,~V` and :math:`X` does not occur in type :math:`U` but occurs strictly positively in type :math:`V` + :math:`T` converts to :math:`(I~a_1 … a_m~t_1 … t_p )` where :math:`I` is the name of an inductive declaration of the form .. math:: - \ind{m}{I:A}{c_1 :∀ p_1 :P_1 ,… ∀p_m :P_m ,C_1 ;…;c_n :∀ p_1 :P_1 ,… ∀p_m :P_m ,C_n} + \ind{m}{I:A}{c_1 :∀ p_1 :P_1 ,… ∀p_m :P_m ,~C_1 ;~…;~c_n :∀ p_1 :P_1 ,… ∀p_m :P_m ,~C_n} (in particular, it is not mutually defined and it has :math:`m` parameters) and :math:`X` does not occur in @@ -916,7 +916,7 @@ condition* for a constant :math:`X` in the following cases: + :math:`T=(I~b_1 … b_m~u_1 … u_p)`, :math:`I` is an inductive definition with :math:`m` parameters and :math:`X` does not occur in any :math:`u_i` -+ :math:`T=∀ x:U,V` and :math:`X` occurs only strictly positively in :math:`U` and the type :math:`V` ++ :math:`T=∀ x:U,~V` and :math:`X` occurs only strictly positively in :math:`U` and the type :math:`V` satisfies the nested positivity condition for :math:`X` @@ -930,7 +930,6 @@ condition* for a constant :math:`X` in the following cases: Inductive nattree (A:Type) : Type := | leaf : nattree A | node : A -> (nat -> nattree A) -> nattree A. - End TreeExample. Then every instantiated constructor of ``nattree A`` satisfies the nested positivity condition for ``nattree``: @@ -943,7 +942,7 @@ condition* for a constant :math:`X` in the following cases: + Type ``A → (nat → nattree A) → nattree A`` of constructor ``node`` satisfies the positivity condition for ``nattree`` because: - - ``nattree`` occurs only strictly positively in ``A`` ... (bullet 3) + - ``nattree`` occurs only strictly positively in ``A`` ... (bullet 1) - ``nattree`` occurs only strictly positively in ``nat → nattree A`` ... (bullet 3 + 2) @@ -958,8 +957,8 @@ We shall now describe the rules allowing the introduction of a new inductive definition. Let :math:`E` be a global environment and :math:`Γ_P`, :math:`Γ_I`, :math:`Γ_C` be contexts -such that :math:`Γ_I` is :math:`[I_1 :∀ Γ_P ,A_1 ;…;I_k :∀ Γ_P ,A_k]`, and -:math:`Γ_C` is :math:`[c_1:∀ Γ_P ,C_1 ;…;c_n :∀ Γ_P ,C_n ]`. Then +such that :math:`Γ_I` is :math:`[I_1 :∀ Γ_P ,A_1 ;~…;~I_k :∀ Γ_P ,A_k]`, and +:math:`Γ_C` is :math:`[c_1:∀ Γ_P ,C_1 ;~…;~c_n :∀ Γ_P ,C_n ]`. Then .. inference:: W-Ind @@ -967,7 +966,7 @@ such that :math:`Γ_I` is :math:`[I_1 :∀ Γ_P ,A_1 ;…;I_k :∀ Γ_P ,A_k]`, (E[Γ_P ] ⊢ A_j : s_j )_{j=1… k} (E[Γ_I ;Γ_P ] ⊢ C_i : s_{q_i} )_{i=1… n} ------------------------------------------ - \WF{E;\ind{p}{Γ_I}{Γ_C}}{Γ} + \WF{E;~\ind{p}{Γ_I}{Γ_C}}{Γ} provided that the following side conditions hold: @@ -990,8 +989,8 @@ the Type hierarchy. .. example:: It is well known that the existential quantifier can be encoded as an - inductive definition. The following declaration introduces the second- - order existential quantifier :math:`∃ X.P(X)`. + inductive definition. The following declaration introduces the + second-order existential quantifier :math:`∃ X.P(X)`. .. coqtop:: in @@ -1028,7 +1027,7 @@ in :math:`\Type`. .. flag:: Auto Template Polymorphism This option, enabled by default, makes every inductive type declared - at level :math:`Type` (without annotations or hiding it behind a + at level :math:`\Type` (without annotations or hiding it behind a definition) template polymorphic. This can be prevented using the ``notemplate`` attribute. @@ -1041,6 +1040,12 @@ in :math:`\Type`. enabled it will prevail over automatic template polymorphism and cause an error when using the ``template`` attribute. +.. warn:: Automatically declaring @ident as template polymorphic. + + Warning ``auto-template`` can be used to find which types are + implicitly declared template polymorphic by :flag:`Auto Template + Polymorphism`. + If :math:`A` is an arity of some sort and :math:`s` is a sort, we write :math:`A_{/s}` for the arity obtained from :math:`A` by replacing its sort with :math:`s`. Especially, if :math:`A` is well-typed in some global environment and local @@ -1049,9 +1054,9 @@ Calculus of Inductive Constructions. The following typing rule is added to the theory. Let :math:`\ind{p}{Γ_I}{Γ_C}` be an inductive definition. Let -:math:`Γ_P = [p_1 :P_1 ;…;p_p :P_p ]` be its context of parameters, -:math:`Γ_I = [I_1:∀ Γ_P ,A_1 ;…;I_k :∀ Γ_P ,A_k ]` its context of definitions and -:math:`Γ_C = [c_1 :∀ Γ_P ,C_1 ;…;c_n :∀ Γ_P ,C_n]` its context of constructors, +:math:`Γ_P = [p_1 :P_1 ;~…;~p_p :P_p ]` be its context of parameters, +:math:`Γ_I = [I_1:∀ Γ_P ,A_1 ;~…;~I_k :∀ Γ_P ,A_k ]` its context of definitions and +:math:`Γ_C = [c_1 :∀ Γ_P ,C_1 ;~…;~c_n :∀ Γ_P ,C_n]` its context of constructors, with :math:`c_i` a constructor of :math:`I_{q_i}`. Let :math:`m ≤ p` be the length of the longest prefix of parameters such that the :math:`m` first arguments of all occurrences of all :math:`I_j` in all :math:`C_k` (even the occurrences in the @@ -1071,15 +1076,15 @@ uniform parameters of :math:`Γ_P` . We have: \end{array} \right. ----------------------------- - E[] ⊢ I_j~q_1 … q_r :∀ [p_{r+1} :P_{r+1} ;…;p_p :P_p], (A_j)_{/s_j} + E[] ⊢ I_j~q_1 … q_r :∀ [p_{r+1} :P_{r+1} ;~…;~p_p :P_p], (A_j)_{/s_j} provided that the following side conditions hold: + :math:`Γ_{P′}` is the context obtained from :math:`Γ_P` by replacing each :math:`P_l` that is an arity with :math:`P_l'` for :math:`1≤ l ≤ r` (notice that :math:`P_l` arity implies :math:`P_l'` - arity since :math:`(E[] ⊢ P_l' ≤_{βδιζη} \subst{P_l}{p_u}{q_u}_{u=1\ldots l-1} )`; + arity since :math:`E[] ⊢ P_l' ≤_{βδιζη} \subst{P_l}{p_u}{q_u}_{u=1\ldots l-1}`); + there are sorts :math:`s_i` , for :math:`1 ≤ i ≤ k` such that, for - :math:`Γ_{I'} = [I_1 :∀ Γ_{P'} ,(A_1)_{/s_1} ;…;I_k :∀ Γ_{P'} ,(A_k)_{/s_k}]` + :math:`Γ_{I'} = [I_1 :∀ Γ_{P'} ,(A_1)_{/s_1} ;~…;~I_k :∀ Γ_{P'} ,(A_k)_{/s_k}]` we have :math:`(E[Γ_{I′} ;Γ_{P′}] ⊢ C_i : s_{q_i})_{i=1… n}` ; + the sorts :math:`s_i` are such that all eliminations, to :math:`\Prop`, :math:`\Set` and :math:`\Type(j)`, are allowed @@ -1097,7 +1102,7 @@ replacements of sorts, needed for this derivation, in the parameters that are arities (this is possible because :math:`\ind{p}{Γ_I}{Γ_C}` well-formed implies that :math:`\ind{p}{Γ_{I'}}{Γ_{C'}}` is well-formed and has the same allowed eliminations, where :math:`Γ_{I′}` is defined as above and -:math:`Γ_{C′} = [c_1 :∀ Γ_{P′} ,C_1 ;…;c_n :∀ Γ_{P′} ,C_n ]`). That is, the changes in the +:math:`Γ_{C′} = [c_1 :∀ Γ_{P′} ,C_1 ;~…;~c_n :∀ Γ_{P′} ,C_n ]`). That is, the changes in the types of each partial instance :math:`q_1 … q_r` can be characterized by the ordered sets of arity sorts among the types of parameters, and to each signature is associated a new inductive definition with fresh names. @@ -1199,10 +1204,11 @@ a strongly normalizing reduction, we cannot accept any sort of recursion (even terminating). So the basic idea is to restrict ourselves to primitive recursive functions and functionals. -For instance, assuming a parameter :g:`A:Set` exists in the local context, -we want to build a function length of type :g:`list A -> nat` which computes -the length of the list, such that :g:`(length (nil A)) = O` and :g:`(length -(cons A a l)) = (S (length l))`. We want these equalities to be +For instance, assuming a parameter :math:`A:\Set` exists in the local context, +we want to build a function :math:`\length` of type :math:`\List~A → \nat` which computes +the length of the list, such that :math:`(\length~(\Nil~A)) = \nO` and +:math:`(\length~(\cons~A~a~l)) = (\nS~(\length~l))`. +We want these equalities to be recognized implicitly and taken into account in the conversion rule. From the logical point of view, we have built a type family by giving @@ -1216,22 +1222,22 @@ In case the inductive definition is effectively a recursive one, we want to capture the extra property that we have built the smallest fixed point of this recursive equation. This says that we are only manipulating finite objects. This analysis provides induction -principles. For instance, in order to prove :g:`∀ l:list A,(has_length A l -(length l))` it is enough to prove: +principles. For instance, in order to prove +:math:`∀ l:\List~A,~(\kw{has}\_\kw{length}~A~l~(\length~l))` it is enough to prove: -+ :g:`(has_length A (nil A) (length (nil A)))` -+ :g:`∀ a:A, ∀ l:list A, (has_length A l (length l)) →` - :g:`(has_length A (cons A a l) (length (cons A a l)))` ++ :math:`(\kw{has}\_\kw{length}~A~(\Nil~A)~(\length~(\Nil~A)))` ++ :math:`∀ a:A,~∀ l:\List~A,~(\kw{has}\_\kw{length}~A~l~(\length~l)) →` + :math:`(\kw{has}\_\kw{length}~A~(\cons~A~a~l)~(\length~(\cons~A~a~l)))` -which given the conversion equalities satisfied by length is the same +which given the conversion equalities satisfied by :math:`\length` is the same as proving: -+ :g:`(has_length A (nil A) O)` -+ :g:`∀ a:A, ∀ l:list A, (has_length A l (length l)) →` - :g:`(has_length A (cons A a l) (S (length l)))` ++ :math:`(\kw{has}\_\kw{length}~A~(\Nil~A)~\nO)` ++ :math:`∀ a:A,~∀ l:\List~A,~(\kw{has}\_\kw{length}~A~l~(\length~l)) →` + :math:`(\kw{has}\_\kw{length}~A~(\cons~A~a~l)~(\nS~(\length~l)))` One conceptually simple way to do that, following the basic scheme @@ -1261,7 +1267,7 @@ The |Coq| term for this proof will be written: .. math:: - \Match~m~\with~(c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | … | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n \kwend + \Match~m~\with~(c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | … | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n~\kwend In this expression, if :math:`m` eventually happens to evaluate to :math:`(c_i~u_1 … u_{p_i})` then the expression will behave as specified in its :math:`i`-th branch @@ -1269,7 +1275,7 @@ and it will reduce to :math:`f_i` where the :math:`x_{i1} …x_{ip_i}` are repla :math:`u_1 … u_{p_i}` according to the ι-reduction. Actually, for type checking a :math:`\Match…\with…\kwend` expression we also need -to know the predicate P to be proved by case analysis. In the general +to know the predicate :math:`P` to be proved by case analysis. In the general case where :math:`I` is an inductively defined :math:`n`-ary relation, :math:`P` is a predicate over :math:`n+1` arguments: the :math:`n` first ones correspond to the arguments of :math:`I` (parameters excluded), and the last one corresponds to object :math:`m`. |Coq| @@ -1303,7 +1309,7 @@ inference rules, we use a more compact notation: .. _Allowed-elimination-sorts: -**Allowed elimination sorts.** An important question for building the typing rule for match is what +**Allowed elimination sorts.** An important question for building the typing rule for :math:`\Match` is what can be the type of :math:`λ a x . P` with respect to the type of :math:`m`. If :math:`m:I` and :math:`I:A` and :math:`λ a x . P : B` then by :math:`[I:A|B]` we mean that one can use :math:`λ a x . P` with :math:`m` in the above match-construct. @@ -1321,7 +1327,7 @@ There is no restriction on the sort of the predicate to be eliminated. [(I~x):A′|B′] ----------------------- - [I:∀ x:A, A′|∀ x:A, B′] + [I:∀ x:A,~A′|∀ x:A,~B′] .. inference:: Set & Type @@ -1341,7 +1347,7 @@ sort :math:`\Prop`. ~ --------------- - [I:Prop|I→Prop] + [I:\Prop|I→\Prop] :math:`\Prop` is the type of logical propositions, the proofs of properties :math:`P` in @@ -1370,7 +1376,7 @@ the proof of :g:`or A B` is not accepted: From the computational point of view, the structure of the proof of :g:`(or A B)` in this term is needed for computing the boolean value. -In general, if :math:`I` has type :math:`\Prop` then :math:`P` cannot have type :math:`I→Set,` because +In general, if :math:`I` has type :math:`\Prop` then :math:`P` cannot have type :math:`I→\Set`, because it will mean to build an informative proof of type :math:`(P~m)` doing a case analysis over a non-computational object that will disappear in the extracted program. But the other way is safe with respect to our @@ -1378,11 +1384,11 @@ interpretation we can have :math:`I` a computational object and :math:`P` a non-computational one, it just corresponds to proving a logical property of a computational object. -In the same spirit, elimination on :math:`P` of type :math:`I→Type` cannot be allowed -because it trivially implies the elimination on :math:`P` of type :math:`I→ Set` by +In the same spirit, elimination on :math:`P` of type :math:`I→\Type` cannot be allowed +because it trivially implies the elimination on :math:`P` of type :math:`I→ \Set` by cumulativity. It also implies that there are two proofs of the same -property which are provably different, contradicting the proof- -irrelevance property which is sometimes a useful axiom: +property which are provably different, contradicting the +proof-irrelevance property which is sometimes a useful axiom: .. example:: @@ -1391,7 +1397,7 @@ irrelevance property which is sometimes a useful axiom: Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y. The elimination of an inductive definition of type :math:`\Prop` on a predicate -:math:`P` of type :math:`I→ Type` leads to a paradox when applied to impredicative +:math:`P` of type :math:`I→ \Type` leads to a paradox when applied to impredicative inductive definition like the second-order existential quantifier :g:`exProp` defined above, because it gives access to the two projections on this type. @@ -1407,7 +1413,7 @@ this type. I~\kw{is an empty or singleton definition} s ∈ \Sort ------------------------------------- - [I:Prop|I→ s] + [I:\Prop|I→ s] A *singleton definition* has only one constructor and all the arguments of this constructor have type :math:`\Prop`. In that case, there is a @@ -1444,7 +1450,7 @@ corresponding to the :math:`c:C` constructor. .. math:: \begin{array}{ll} \{c:(I~p_1\ldots p_r\ t_1 \ldots t_p)\}^P &\equiv (P~t_1\ldots ~t_p~c) \\ - \{c:\forall~x:T,C\}^P &\equiv \forall~x:T,\{(c~x):C\}^P + \{c:∀ x:T,~C\}^P &\equiv ∀ x:T,~\{(c~x):C\}^P \end{array} We write :math:`\{c\}^P` for :math:`\{c:C\}^P` with :math:`C` the type of :math:`c`. @@ -1463,7 +1469,7 @@ We write :math:`\{c\}^P` for :math:`\{c:C\}^P` with :math:`C` the type of :math: can be represented in abstract syntax as .. math:: - \case(t,P,f 1 | f 2 ) + \case(t,P,f_1 | f_2 ) where @@ -1471,27 +1477,27 @@ We write :math:`\{c\}^P` for :math:`\{c:C\}^P` with :math:`C` the type of :math: :nowrap: \begin{eqnarray*} - P & = & \lambda~l~.~P^\prime\\ + P & = & λ l.~P^\prime\\ f_1 & = & t_1\\ - f_2 & = & \lambda~(hd:\nat)~.~\lambda~(tl:\List~\nat)~.~t_2 + f_2 & = & λ (hd:\nat).~λ (tl:\List~\nat).~t_2 \end{eqnarray*} According to the definition: .. math:: - \{(\kw{nil}~\nat)\}^P ≡ \{(\kw{nil}~\nat) : (\List~\nat)\}^P ≡ (P~(\kw{nil}~\nat)) + \{(\Nil~\nat)\}^P ≡ \{(\Nil~\nat) : (\List~\nat)\}^P ≡ (P~(\Nil~\nat)) .. math:: \begin{array}{rl} - \{(\kw{cons}~\nat)\}^P & ≡\{(\kw{cons}~\nat) : (\nat→\List~\nat→\List~\nat)\}^P \\ - & ≡∀ n:\nat, \{(\kw{cons}~\nat~n) : \List~\nat→\List~\nat)\}^P \\ - & ≡∀ n:\nat, ∀ l:\List~\nat, \{(\kw{cons}~\nat~n~l) : \List~\nat)\}^P \\ - & ≡∀ n:\nat, ∀ l:\List~\nat,(P~(\kw{cons}~\nat~n~l)). + \{(\cons~\nat)\}^P & ≡\{(\cons~\nat) : (\nat→\List~\nat→\List~\nat)\}^P \\ + & ≡∀ n:\nat,~\{(\cons~\nat~n) : (\List~\nat→\List~\nat)\}^P \\ + & ≡∀ n:\nat,~∀ l:\List~\nat,~\{(\cons~\nat~n~l) : (\List~\nat)\}^P \\ + & ≡∀ n:\nat,~∀ l:\List~\nat,~(P~(\cons~\nat~n~l)). \end{array} - Given some :math:`P` then :math:`\{(\kw{nil}~\nat)\}^P` represents the expected type of :math:`f_1` , - and :math:`\{(\kw{cons}~\nat)\}^P` represents the expected type of :math:`f_2`. + Given some :math:`P` then :math:`\{(\Nil~\nat)\}^P` represents the expected type of :math:`f_1` , + and :math:`\{(\cons~\nat)\}^P` represents the expected type of :math:`f_2`. .. _Typing-rule: @@ -1512,7 +1518,7 @@ following typing rule E[Γ] ⊢ \case(c,P,f_1 |… |f_l ) : (P~t_1 … t_s~c) provided :math:`I` is an inductive type in a -definition :math:`\ind{r}{Γ_I}{Γ_C}` with :math:`Γ_C = [c_1 :C_1 ;…;c_n :C_n ]` and +definition :math:`\ind{r}{Γ_I}{Γ_C}` with :math:`Γ_C = [c_1 :C_1 ;~…;~c_n :C_n ]` and :math:`c_{p_1} … c_{p_l}` are the only constructors of :math:`I`. @@ -1527,8 +1533,8 @@ definition :math:`\ind{r}{Γ_I}{Γ_C}` with :math:`Γ_C = [c_1 :C_1 ;…;c_n :C_ E[Γ] ⊢ t : (\List ~\nat) \\ E[Γ] ⊢ P : B \\ [(\List ~\nat)|B] \\ - E[Γ] ⊢ f_1 : {(\kw{nil} ~\nat)}^P \\ - E[Γ] ⊢ f_2 : {(\kw{cons} ~\nat)}^P + E[Γ] ⊢ f_1 : \{(\Nil ~\nat)\}^P \\ + E[Γ] ⊢ f_2 : \{(\cons ~\nat)\}^P \end{array} ------------------------------------------------ E[Γ] ⊢ \case(t,P,f_1 |f_2 ) : (P~t) @@ -1551,7 +1557,7 @@ The ι-contraction of this term is :math:`(f_i~a_1 … a_m )` leading to the general reduction rule: .. math:: - \case((c_{p_i}~q_1 … q_r~a_1 … a_m ),P,f_1 |… |f_n ) \triangleright_ι (f_i~a_1 … a_m ) + \case((c_{p_i}~q_1 … q_r~a_1 … a_m ),P,f_1 |… |f_l ) \triangleright_ι (f_i~a_1 … a_m ) .. _Fixpoint-definitions: @@ -1565,14 +1571,14 @@ concrete syntax for a recursive set of mutually recursive declarations is (with :math:`Γ_i` contexts): .. math:: - \fix~f_1 (Γ_1 ) :A_1 :=t_1 \with … \with~f_n (Γ_n ) :A_n :=t_n + \fix~f_1 (Γ_1 ) :A_1 :=t_1~\with … \with~f_n (Γ_n ) :A_n :=t_n The terms are obtained by projections from this set of declarations and are written .. math:: - \fix~f_1 (Γ_1 ) :A_1 :=t_1 \with … \with~f_n (Γ_n ) :A_n :=t_n \for~f_i + \fix~f_1 (Γ_1 ) :A_1 :=t_1~\with … \with~f_n (Γ_n ) :A_n :=t_n~\for~f_i In the inference rules, we represent such a term by @@ -1580,7 +1586,7 @@ In the inference rules, we represent such a term by \Fix~f_i\{f_1 :A_1':=t_1' … f_n :A_n':=t_n'\} with :math:`t_i'` (resp. :math:`A_i'`) representing the term :math:`t_i` abstracted (resp. -generalized) with respect to the bindings in the context Γ_i , namely +generalized) with respect to the bindings in the context :math:`Γ_i`, namely :math:`t_i'=λ Γ_i . t_i` and :math:`A_i'=∀ Γ_i , A_i`. @@ -1592,7 +1598,7 @@ The typing rule is the expected one for a fixpoint. .. inference:: Fix (E[Γ] ⊢ A_i : s_i )_{i=1… n} - (E[Γ,f_1 :A_1 ,…,f_n :A_n ] ⊢ t_i : A_i )_{i=1… n} + (E[Γ;~f_1 :A_1 ;~…;~f_n :A_n ] ⊢ t_i : A_i )_{i=1… n} ------------------------------------------------------- E[Γ] ⊢ \Fix~f_i\{f_1 :A_1 :=t_1 … f_n :A_n :=t_n \} : A_i @@ -1608,14 +1614,14 @@ instance in the case of natural numbers, a proof of the induction principle of type .. math:: - ∀ P:\nat→\Prop, (P~O)→(∀ n:\nat, (P~n)→(P~(\kw{S}~n)))→ ∀ n:\nat, (P~n) + ∀ P:\nat→\Prop,~(P~\nO)→(∀ n:\nat,~(P~n)→(P~(\nS~n)))→ ∀ n:\nat,~(P~n) can be represented by the term: .. math:: \begin{array}{l} - λ P:\nat→\Prop. λ f:(P~O). λ g:(∀ n:\nat, (P~n)→(P~(S~n))).\\ - \Fix~h\{h:∀ n:\nat, (P~n):=λ n:\nat. \case(n,P,f | λp:\nat. (g~p~(h~p)))\} + λ P:\nat→\Prop.~λ f:(P~\nO).~λ g:(∀ n:\nat,~(P~n)→(P~(\nS~n))).\\ + \Fix~h\{h:∀ n:\nat,~(P~n):=λ n:\nat.~\case(n,P,f | λp:\nat.~(g~p~(h~p)))\} \end{array} Before accepting a fixpoint definition as being correctly typed, we @@ -1632,7 +1638,7 @@ fixpoints is extended and becomes where :math:`k_i` are positive integers. Each :math:`k_i` represents the index of parameter of :math:`f_i` , on which :math:`f_i` is decreasing. Each :math:`A_i` should be a type (reducible to a term) starting with at least :math:`k_i` products -:math:`∀ y_1 :B_1 ,… ∀ y_{k_i} :B_{k_i} , A_i'` and :math:`B_{k_i}` an inductive type. +:math:`∀ y_1 :B_1 ,~… ∀ y_{k_i} :B_{k_i} ,~A_i'` and :math:`B_{k_i}` an inductive type. Now in the definition :math:`t_i`, if :math:`f_j` occurs then it should be applied to at least :math:`k_j` arguments and the :math:`k_j`-th argument should be @@ -1642,23 +1648,23 @@ The definition of being structurally smaller is a bit technical. One needs first to define the notion of *recursive arguments of a constructor*. For an inductive definition :math:`\ind{r}{Γ_I}{Γ_C}`, if the type of a constructor :math:`c` has the form -:math:`∀ p_1 :P_1 ,… ∀ p_r :P_r, ∀ x_1:T_1, … ∀ x_r :T_r, (I_j~p_1 … p_r~t_1 … t_s )`, +:math:`∀ p_1 :P_1 ,~… ∀ p_r :P_r,~∀ x_1:T_1,~… ∀ x_r :T_r,~(I_j~p_1 … p_r~t_1 … t_s )`, then the recursive arguments will correspond to :math:`T_i` in which one of the :math:`I_l` occurs. The main rules for being structurally smaller are the following. Given a variable :math:`y` of an inductively defined type in a declaration -:math:`\ind{r}{Γ_I}{Γ_C}` where :math:`Γ_I` is :math:`[I_1 :A_1 ;…;I_k :A_k]`, and :math:`Γ_C` is -:math:`[c_1 :C_1 ;…;c_n :C_n ]`, the terms structurally smaller than :math:`y` are: +:math:`\ind{r}{Γ_I}{Γ_C}` where :math:`Γ_I` is :math:`[I_1 :A_1 ;~…;~I_k :A_k]`, and :math:`Γ_C` is +:math:`[c_1 :C_1 ;~…;~c_n :C_n ]`, the terms structurally smaller than :math:`y` are: -+ :math:`(t~u)` and :math:`λ x:u . t` when :math:`t` is structurally smaller than :math:`y`. ++ :math:`(t~u)` and :math:`λ x:U .~t` when :math:`t` is structurally smaller than :math:`y`. + :math:`\case(c,P,f_1 … f_n)` when each :math:`f_i` is structurally smaller than :math:`y`. If :math:`c` is :math:`y` or is structurally smaller than :math:`y`, its type is an inductive definition :math:`I_p` part of the inductive declaration corresponding to :math:`y`. Each :math:`f_i` corresponds to a type of constructor - :math:`C_q ≡ ∀ p_1 :P_1 ,…,∀ p_r :P_r , ∀ y_1 :B_1 , … ∀ y_k :B_k , (I~a_1 … a_k )` - and can consequently be written :math:`λ y_1 :B_1' . … λ y_k :B_k'. g_i`. (:math:`B_i'` is + :math:`C_q ≡ ∀ p_1 :P_1 ,~…,∀ p_r :P_r ,~∀ y_1 :B_1 ,~… ∀ y_k :B_k ,~(I~a_1 … a_k )` + and can consequently be written :math:`λ y_1 :B_1' .~… λ y_k :B_k'.~g_i`. (:math:`B_i'` is obtained from :math:`B_i` by substituting parameters for variables) the variables :math:`y_j` occurring in :math:`g_i` corresponding to recursive arguments :math:`B_i` (the ones in which one of the :math:`I_l` occurs) are structurally smaller than y. @@ -1702,7 +1708,7 @@ Let :math:`F` be the set of declarations: The reduction for fixpoints is: .. math:: - (\Fix~f_i \{F\} a_1 …a_{k_i}) \triangleright_ι \subst{t_i}{f_k}{\Fix~f_k \{F\}}_{k=1… n} ~a_1 … a_{k_i} + (\Fix~f_i \{F\}~a_1 …a_{k_i}) ~\triangleright_ι~ \subst{t_i}{f_k}{\Fix~f_k \{F\}}_{k=1… n} ~a_1 … a_{k_i} when :math:`a_{k_i}` starts with a constructor. This last restriction is needed in order to keep strong normalization and corresponds to the reduction @@ -1712,13 +1718,11 @@ possible: .. math:: :nowrap: - {\def\plus{\mathsf{plus}} - \def\tri{\triangleright_\iota} - \begin{eqnarray*} - \plus~(\nS~(\nS~\nO))~(\nS~\nO) & \tri & \nS~(\plus~(\nS~\nO)~(\nS~\nO))\\ - & \tri & \nS~(\nS~(\plus~\nO~(\nS~\nO)))\\ - & \tri & \nS~(\nS~(\nS~\nO))\\ - \end{eqnarray*}} + \begin{eqnarray*} + \plus~(\nS~(\nS~\nO))~(\nS~\nO)~& \trii & \nS~(\plus~(\nS~\nO)~(\nS~\nO))\\ + & \trii & \nS~(\nS~(\plus~\nO~(\nS~\nO)))\\ + & \trii & \nS~(\nS~(\nS~\nO))\\ + \end{eqnarray*} .. _Mutual-induction: @@ -1748,9 +1752,9 @@ reference to the global declaration in the subsequent global environment and local context by explicitly applying this constant to the constant :math:`c'`. -Below, if :math:`Γ` is a context of the form :math:`[y_1 :A_1 ;…;y_n :A_n]`, we write -:math:`∀x:U,\subst{Γ}{c}{x}` to mean -:math:`[y_1 :∀ x:U,\subst{A_1}{c}{x};…;y_n :∀ x:U,\subst{A_n}{c}{x}]` +Below, if :math:`Γ` is a context of the form :math:`[y_1 :A_1 ;~…;~y_n :A_n]`, we write +:math:`∀x:U,~\subst{Γ}{c}{x}` to mean +:math:`[y_1 :∀ x:U,~\subst{A_1}{c}{x};~…;~y_n :∀ x:U,~\subst{A_n}{c}{x}]` and :math:`\subst{E}{|Γ|}{|Γ|c}` to mean the parallel substitution :math:`E\{y_1 /(y_1~c)\}…\{y_n/(y_n~c)\}`. @@ -1760,25 +1764,25 @@ and :math:`\subst{E}{|Γ|}{|Γ|c}` to mean the parallel substitution **First abstracting property:** .. math:: - \frac{\WF{E;c:U;E′;c′:=t:T;E″}{Γ}} - {\WF{E;c:U;E′;c′:=λ x:U. \subst{t}{c}{x}:∀x:U,\subst{T}{c}{x};\subst{E″}{c′}{(c′~c)}} - {\subst{Γ}{c}{(c~c′)}}} + \frac{\WF{E;~c:U;~E′;~c′:=t:T;~E″}{Γ}} + {\WF{E;~c:U;~E′;~c′:=λ x:U.~\subst{t}{c}{x}:∀x:U,~\subst{T}{c}{x};~\subst{E″}{c′}{(c′~c)}} + {\subst{Γ}{c′}{(c′~c)}}} .. math:: - \frac{\WF{E;c:U;E′;c′:T;E″}{Γ}} - {\WF{E;c:U;E′;c′:∀ x:U,\subst{T}{c}{x};\subst{E″}{c′}{(c′~c)}}{Γ{c/(c~c′)}}} + \frac{\WF{E;~c:U;~E′;~c′:T;~E″}{Γ}} + {\WF{E;~c:U;~E′;~c′:∀ x:U,~\subst{T}{c}{x};~\subst{E″}{c′}{(c′~c)}}{\subst{Γ}{c′}{(c′~c)}}} .. math:: - \frac{\WF{E;c:U;E′;\ind{p}{Γ_I}{Γ_C};E″}{Γ}} - {\WFTWOLINES{E;c:U;E′;\ind{p+1}{∀ x:U,\subst{Γ_I}{c}{x}}{∀ x:U,\subst{Γ_C}{c}{x}}; - \subst{E″}{|Γ_I ,Γ_C |}{|Γ_I ,Γ_C | c}} - {\subst{Γ}{|Γ_I ,Γ_C|}{|Γ_I ,Γ_C | c}}} + \frac{\WF{E;~c:U;~E′;~\ind{p}{Γ_I}{Γ_C};~E″}{Γ}} + {\WFTWOLINES{E;~c:U;~E′;~\ind{p+1}{∀ x:U,~\subst{Γ_I}{c}{x}}{∀ x:U,~\subst{Γ_C}{c}{x}};~ + \subst{E″}{|Γ_I ;Γ_C |}{|Γ_I ;Γ_C | c}} + {\subst{Γ}{|Γ_I ;Γ_C|}{|Γ_I ;Γ_C | c}}} One can similarly modify a global declaration by generalizing it over a previously defined constant :math:`c′`. Below, if :math:`Γ` is a context of the form -:math:`[y_1 :A_1 ;…;y_n :A_n]`, we write :math:`\subst{Γ}{c}{u}` to mean -:math:`[y_1 :\subst{A_1} {c}{u};…;y_n:\subst{A_n} {c}{u}]`. +:math:`[y_1 :A_1 ;~…;~y_n :A_n]`, we write :math:`\subst{Γ}{c}{u}` to mean +:math:`[y_1 :\subst{A_1} {c}{u};~…;~y_n:\subst{A_n} {c}{u}]`. .. _Second-abstracting-property: @@ -1786,16 +1790,16 @@ a previously defined constant :math:`c′`. Below, if :math:`Γ` is a context of **Second abstracting property:** .. math:: - \frac{\WF{E;c:=u:U;E′;c′:=t:T;E″}{Γ}} - {\WF{E;c:=u:U;E′;c′:=(\letin{x}{u:U}{\subst{t}{c}{x}}):\subst{T}{c}{u};E″}{Γ}} + \frac{\WF{E;~c:=u:U;~E′;~c′:=t:T;~E″}{Γ}} + {\WF{E;~c:=u:U;~E′;~c′:=(\letin{x}{u:U}{\subst{t}{c}{x}}):\subst{T}{c}{u};~E″}{Γ}} .. math:: - \frac{\WF{E;c:=u:U;E′;c′:T;E″}{Γ}} - {\WF{E;c:=u:U;E′;c′:\subst{T}{c}{u};E″}{Γ}} + \frac{\WF{E;~c:=u:U;~E′;~c′:T;~E″}{Γ}} + {\WF{E;~c:=u:U;~E′;~c′:\subst{T}{c}{u};~E″}{Γ}} .. math:: - \frac{\WF{E;c:=u:U;E′;\ind{p}{Γ_I}{Γ_C};E″}{Γ}} - {\WF{E;c:=u:U;E′;\ind{p}{\subst{Γ_I}{c}{u}}{\subst{Γ_C}{c}{u}};E″}{Γ}} + \frac{\WF{E;~c:=u:U;~E′;~\ind{p}{Γ_I}{Γ_C};~E″}{Γ}} + {\WF{E;~c:=u:U;~E′;~\ind{p}{\subst{Γ_I}{c}{u}}{\subst{Γ_C}{c}{u}};~E″}{Γ}} .. _Pruning-the-local-context: @@ -1810,7 +1814,7 @@ One can consequently derive the following property. .. inference:: First pruning property: - \WF{E;c:U;E′}{Γ} + \WF{E;~c:U;~E′}{Γ} c~\kw{does not occur in}~E′~\kw{and}~Γ -------------------------------------- \WF{E;E′}{Γ} @@ -1820,7 +1824,7 @@ One can consequently derive the following property. .. inference:: Second pruning property: - \WF{E;c:=u:U;E′}{Γ} + \WF{E;~c:=u:U;~E′}{Γ} c~\kw{does not occur in}~E′~\kw{and}~Γ -------------------------------------- \WF{E;E′}{Γ} @@ -1861,10 +1865,10 @@ in the sort :math:`\Set`, which is extended to a domain in any sort: .. inference:: ProdImp E[Γ] ⊢ T : s - s ∈ {\Sort} - E[Γ::(x:T)] ⊢ U : Set + s ∈ \Sort + E[Γ::(x:T)] ⊢ U : \Set --------------------- - E[Γ] ⊢ ∀ x:T,U : Set + E[Γ] ⊢ ∀ x:T,~U : \Set This extension has consequences on the inductive definitions which are allowed. In the impredicative system, one can build so-called *large @@ -1879,15 +1883,15 @@ impredicative system for sort :math:`\Set` become: .. inference:: Set1 - s ∈ \{Prop, Set\} + s ∈ \{\Prop, \Set\} ----------------- - [I:Set|I→ s] + [I:\Set|I→ s] .. inference:: Set2 I~\kw{is a small inductive definition} s ∈ \{\Type(i)\} ---------------- - [I:Set|I→ s] + [I:\Set|I→ s] diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 10650af1d1..b82b3b0e80 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -104,18 +104,18 @@ subclass :token:`form` of the syntactic class :token:`term`. The syntax of a nice last column. Or even better, find a proper way to do this! .. productionlist:: - form : True (True) - : | False (False) - : | ~ `form` (not) - : | `form` /\ `form` (and) - : | `form` \/ `form` (or) - : | `form` -> `form` (primitive implication) - : | `form` <-> `form` (iff) - : | forall `ident` : `type`, `form` (primitive for all) - : | exists `ident` [: `specif`], `form` (ex) - : | exists2 `ident` [: `specif`], `form` & `form` (ex2) - : | `term` = `term` (eq) - : | `term` = `term` :> `specif` (eq) + form : True (True) + : False (False) + : ~ `form` (not) + : `form` /\ `form` (and) + : `form` \/ `form` (or) + : `form` -> `form` (primitive implication) + : `form` <-> `form` (iff) + : forall `ident` : `type`, `form` (primitive for all) + : exists `ident` [: `specif`], `form` (ex) + : exists2 `ident` [: `specif`], `form` & `form` (ex2) + : `term` = `term` (eq) + : `term` = `term` :> `specif` (eq) .. note:: @@ -287,13 +287,13 @@ the next section :ref:`specification`): .. productionlist:: specif : `specif` * `specif` (prod) - : | `specif` + `specif` (sum) - : | `specif` + { `specif` } (sumor) - : | { `specif` } + { `specif` } (sumbool) - : | { `ident` : `specif` | `form` } (sig) - : | { `ident` : `specif` | `form` & `form` } (sig2) - : | { `ident` : `specif` & `specif` } (sigT) - : | { `ident` : `specif` & `specif` & `specif` } (sigT2) + : `specif` + `specif` (sum) + : `specif` + { `specif` } (sumor) + : { `specif` } + { `specif` } (sumbool) + : { `ident` : `specif` | `form` } (sig) + : { `ident` : `specif` | `form` & `form` } (sig2) + : { `ident` : `specif` & `specif` } (sigT) + : { `ident` : `specif` & `specif` & `specif` } (sigT2) term : (`term`, `term`) (pair) diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 376a6b8eed..50a56f1d51 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -25,7 +25,7 @@ expressions. In this sense, the :cmd:`Record` construction allows defining record_keyword : Record | Inductive | CoInductive record_body : `ident` [ `binders` ] [: `sort` ] := [ `ident` ] { [ `field` ; … ; `field` ] }. field : `ident` [ `binders` ] : `type` [ where `notation` ] - : | `ident` [ `binders` ] [: `type` ] := `term` + : `ident` [ `binders` ] [: `type` ] := `term` .. cmd:: Record @ident @binders {? : @sort} := {? @ident} { {*; @ident @binders : @type } } @@ -165,8 +165,8 @@ available: .. productionlist:: terms projection : `term` `.` ( `qualid` ) - : | `term` `.` ( `qualid` `arg` … `arg` ) - : | `term` `.` ( @`qualid` `term` … `term` ) + : `term` `.` ( `qualid` `arg` … `arg` ) + : `term` `.` ( @`qualid` `term` … `term` ) Syntax of Record projections @@ -234,7 +234,8 @@ Primitive Projections extended the Calculus of Inductive Constructions with a new binary term constructor `r.(p)` representing a primitive projection `p` applied to a record object `r` (i.e., primitive projections are always applied). - Even if the record type has parameters, these do not appear at + Even if the record type has parameters, these do not appear + in the internal representation of applications of the projection, considerably reducing the sizes of terms when manipulating parameterized records and type checking time. On the user level, primitive projections can be used as a replacement @@ -818,14 +819,14 @@ together, as well as a means of massive abstraction. .. productionlist:: modules module_type : `qualid` - : | `module_type` with Definition `qualid` := `term` - : | `module_type` with Module `qualid` := `qualid` - : | `qualid` `qualid` … `qualid` - : | !`qualid` `qualid` … `qualid` + : `module_type` with Definition `qualid` := `term` + : `module_type` with Module `qualid` := `qualid` + : `qualid` `qualid` … `qualid` + : !`qualid` `qualid` … `qualid` module_binding : ( [Import|Export] `ident` … `ident` : `module_type` ) module_bindings : `module_binding` … `module_binding` module_expression : `qualid` … `qualid` - : | !`qualid` … `qualid` + : !`qualid` … `qualid` Syntax of modules @@ -1814,10 +1815,10 @@ This syntax extension is given in the following grammar: .. productionlist:: explicit_apps term : @ `qualid` `term` … `term` - : | @ `qualid` - : | `qualid` `argument` … `argument` + : @ `qualid` + : `qualid` `argument` … `argument` argument : `term` - : | (`ident` := `term`) + : (`ident` := `term`) Syntax for explicitly giving implicit arguments diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 1a33a9a46e..5ecf007eff 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -127,43 +127,43 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. .. productionlist:: coq term : forall `binders` , `term` - : | fun `binders` => `term` - : | fix `fix_bodies` - : | cofix `cofix_bodies` - : | let `ident` [`binders`] [: `term`] := `term` in `term` - : | let fix `fix_body` in `term` - : | let cofix `cofix_body` in `term` - : | let ( [`name` , … , `name`] ) [`dep_ret_type`] := `term` in `term` - : | let ' `pattern` [in `term`] := `term` [`return_type`] in `term` - : | if `term` [`dep_ret_type`] then `term` else `term` - : | `term` : `term` - : | `term` <: `term` - : | `term` :> - : | `term` -> `term` - : | `term` `arg` … `arg` - : | @ `qualid` [`term` … `term`] - : | `term` % `ident` - : | match `match_item` , … , `match_item` [`return_type`] with + : fun `binders` => `term` + : fix `fix_bodies` + : cofix `cofix_bodies` + : let `ident` [`binders`] [: `term`] := `term` in `term` + : let fix `fix_body` in `term` + : let cofix `cofix_body` in `term` + : let ( [`name` , … , `name`] ) [`dep_ret_type`] := `term` in `term` + : let ' `pattern` [in `term`] := `term` [`return_type`] in `term` + : if `term` [`dep_ret_type`] then `term` else `term` + : `term` : `term` + : `term` <: `term` + : `term` :> + : `term` -> `term` + : `term` `arg` … `arg` + : @ `qualid` [`term` … `term`] + : `term` % `ident` + : match `match_item` , … , `match_item` [`return_type`] with : [[|] `equation` | … | `equation`] end - : | `qualid` - : | `sort` - : | `num` - : | _ - : | ( `term` ) + : `qualid` + : `sort` + : `num` + : _ + : ( `term` ) arg : `term` - : | ( `ident` := `term` ) + : ( `ident` := `term` ) binders : `binder` … `binder` binder : `name` - : | ( `name` … `name` : `term` ) - : | ( `name` [: `term`] := `term` ) - : | ' `pattern` + : ( `name` … `name` : `term` ) + : ( `name` [: `term`] := `term` ) + : ' `pattern` name : `ident` | _ qualid : `ident` | `qualid` `access_ident` sort : Prop | Set | Type fix_bodies : `fix_body` - : | `fix_body` with `fix_body` with … with `fix_body` for `ident` + : `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` + : `cofix_body` with `cofix_body` with … with `cofix_body` for `ident` fix_body : `ident` `binders` [`annotation`] [: `term`] := `term` cofix_body : `ident` [`binders`] [: `term`] := `term` annotation : { struct `ident` } @@ -173,13 +173,13 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. equation : `mult_pattern` | … | `mult_pattern` => `term` mult_pattern : `pattern` , … , `pattern` pattern : `qualid` `pattern` … `pattern` - : | @ `qualid` `pattern` … `pattern` - : | `pattern` as `ident` - : | `pattern` % `ident` - : | `qualid` - : | _ - : | `num` - : | ( `or_pattern` , … , `or_pattern` ) + : @ `qualid` `pattern` … `pattern` + : `pattern` as `ident` + : `pattern` % `ident` + : `qualid` + : _ + : `num` + : ( `or_pattern` , … , `or_pattern` ) or_pattern : `pattern` | … | `pattern` @@ -230,7 +230,7 @@ There are three sorts :g:`Set`, :g:`Prop` and :g:`Type`. 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 +- :g:`Set` is the universe of *program types* or *specifications*. The specifications themselves are typing the programs. We denote specifications by :production:`specif`. This constitutes a semantic subclass of the syntactic class :token:`term`. @@ -524,38 +524,38 @@ The Vernacular .. productionlist:: coq decorated-sentence : [ `decoration` … `decoration` ] `sentence` sentence : `assumption` - : | `definition` - : | `inductive` - : | `fixpoint` - : | `assertion` `proof` + : `definition` + : `inductive` + : `fixpoint` + : `assertion` `proof` assumption : `assumption_keyword` `assums`. assumption_keyword : Axiom | Conjecture - : | Parameter | Parameters - : | Variable | Variables - : | Hypothesis | Hypotheses + : Parameter | Parameters + : Variable | Variables + : Hypothesis | Hypotheses assums : `ident` … `ident` : `term` - : | ( `ident` … `ident` : `term` ) … ( `ident` … `ident` : `term` ) + : ( `ident` … `ident` : `term` ) … ( `ident` … `ident` : `term` ) definition : [Local] Definition `ident` [`binders`] [: `term`] := `term` . - : | Let `ident` [`binders`] [: `term`] := `term` . + : Let `ident` [`binders`] [: `term`] := `term` . inductive : Inductive `ind_body` with … with `ind_body` . - : | CoInductive `ind_body` with … with `ind_body` . + : CoInductive `ind_body` with … with `ind_body` . ind_body : `ident` [`binders`] : `term` := : [[|] `ident` [`binders`] [:`term`] | … | `ident` [`binders`] [:`term`]] fixpoint : Fixpoint `fix_body` with … with `fix_body` . - : | CoFixpoint `cofix_body` with … with `cofix_body` . + : CoFixpoint `cofix_body` with … with `cofix_body` . assertion : `assertion_keyword` `ident` [`binders`] : `term` . assertion_keyword : Theorem | Lemma - : | Remark | Fact - : | Corollary | Proposition - : | Definition | Example + : Remark | Fact + : Corollary | Proposition + : Definition | Example proof : Proof . … Qed . - : | Proof . … Defined . - : | Proof . … Admitted . + : Proof . … Defined . + : Proof . … Admitted . decoration : #[ `attributes` ] attributes : [`attribute`, … , `attribute`] attribute : `ident` - :| `ident` = `string` - :| `ident` ( `attributes` ) + : `ident` = `string` + : `ident` ( `attributes` ) .. todo:: This use of … in this grammar is inconsistent What about removing the proof part of this grammar from this chapter diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 9bc67147f7..1b4d2315aa 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -163,14 +163,14 @@ and ``coqtop``, unless stated otherwise: is equivalent to runningRequire dirpath. :-require dirpath: Load |Coq| compiled library dirpath and import it. This is equivalent to running Require Import dirpath. -:-batch: Exit just after argument parsing. Available for `coqtop` only. -:-compile *file.v*: Compile file *file.v* into *file.vo*. This option +:-batch: Exit just after argument parsing. Available for ``coqtop`` only. +:-compile *file.v*: Deprecated; use ``coqc`` instead. Compile file *file.v* into *file.vo*. This option implies -batch (exit just after argument parsing). It is available only - for `coqtop`, as this behavior is the purpose of `coqc`. -:-compile-verbose *file.v*: Same as -compile but also output the + for `coqtop`, as this behavior is the purpose of ``coqc``. +:-compile-verbose *file.v*: Deprecated. Use ``coqc -verbose``. Same as -compile but also output the content of *file.v* as it is compiled. :-verbose: Output the content of the input file as it is compiled. - This option is available for `coqc` only; it is the counterpart of + This option is available for ``coqc`` only; it is the counterpart of -compile-verbose. :-w (all|none|w₁,…,wₙ): Configure the display of warnings. This option expects all, none or a comma-separated list of warning names or @@ -211,11 +211,11 @@ and ``coqtop``, unless stated otherwise: (to be used by coqdoc, see :ref:`coqdoc`). By default, if *file.v* is being compiled, *file.glob* is used. :-no-glob: Disable the dumping of references for global names. -:-image *file*: Set the binary image to be used by `coqc` to be *file* +:-image *file*: Set the binary image to be used by ``coqc`` to be *file* instead of the standard one. Not of general use. :-bindir *directory*: Set the directory containing |Coq| binaries to be - used by `coqc`. It is equivalent to doing export COQBIN= *directory* - before launching `coqc`. + used by ``coqc``. It is equivalent to doing export COQBIN= *directory* + before launching ``coqc``. :-where: Print the location of |Coq|’s standard library and exit. :-config: Print the locations of |Coq|’s binaries, dependencies, and libraries, then exit. diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 1071682ead..442077616f 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -41,117 +41,121 @@ mode but it can also be used in toplevel definitions as shown below. .. note:: - - The infix tacticals “… \|\| …”, “… + …”, and “… ; …” are associative. + - The infix tacticals ``… || …`` , ``… + …`` , and ``… ; …`` are associative. - - In :token:`tacarg`, there is an overlap between qualid as a direct tactic - argument and :token:`qualid` as a particular case of term. The resolution is - done by first looking for a reference of the tactic language and if - it fails, for a reference to a term. To force the resolution as a - reference of the tactic language, use the form :g:`ltac:(@qualid)`. To - force the resolution as a reference to a term, use the syntax - :g:`(@qualid)`. + .. example:: - - As shown by the figure, tactical ``\|\|`` binds more than the prefix - tacticals try, repeat, do and abstract which themselves bind more - than the postfix tactical “… ;[ … ]” which binds more than “… ; …”. + If you want that :n:`@tactic__2; @tactic__3` be fully run on the first + subgoal generated by :n:`@tactic__1`, before running on the other + subgoals, then you should not write + :n:`@tactic__1; (@tactic__2; @tactic__3)` but rather + :n:`@tactic__1; [> @tactic__2; @tactic__3 .. ]`. - For instance + - In :token:`tacarg`, there is an overlap between :token:`qualid` as a + direct tactic argument and :token:`qualid` as a particular case of + :token:`term`. The resolution is done by first looking for a reference + of the tactic language and if it fails, for a reference to a term. + To force the resolution as a reference of the tactic language, use the + form :n:`ltac:(@qualid)`. To force the resolution as a reference to a + term, use the syntax :n:`(@qualid)`. - .. coqtop:: in + - As shown by the figure, tactical ``… || …`` binds more than the prefix + tacticals :tacn:`try`, :tacn:`repeat`, :tacn:`do` and :tacn:`abstract` + which themselves bind more than the postfix tactical ``… ;[ … ]`` + which binds at the same level as ``… ; …`` . - try repeat tac1 || tac2; tac3; [tac31 | ... | tac3n]; tac4. + .. example:: - is understood as + :n:`try repeat @tactic__1 || @tactic__2; @tactic__3; [ {+| @tactic } ]; @tactic__4` - .. coqtop:: in + is understood as: - try (repeat (tac1 || tac2)); - ((tac3; [tac31 | ... | tac3n]); tac4). + :n:`((try (repeat (@tactic__1 || @tactic__2)); @tactic__3); [ {+| @tactic } ]); @tactic__4` .. productionlist:: coq expr : `expr` ; `expr` - : | [> `expr` | ... | `expr` ] - : | `expr` ; [ `expr` | ... | `expr` ] - : | `tacexpr3` - tacexpr3 : do (`natural` | `ident`) tacexpr3 - : | progress `tacexpr3` - : | repeat `tacexpr3` - : | try `tacexpr3` - : | once `tacexpr3` - : | exactly_once `tacexpr3` - : | timeout (`natural` | `ident`) `tacexpr3` - : | time [`string`] `tacexpr3` - : | only `selector`: `tacexpr3` - : | `tacexpr2` + : [> `expr` | ... | `expr` ] + : `expr` ; [ `expr` | ... | `expr` ] + : `tacexpr3` + tacexpr3 : do (`natural` | `ident`) `tacexpr3` + : progress `tacexpr3` + : repeat `tacexpr3` + : try `tacexpr3` + : once `tacexpr3` + : exactly_once `tacexpr3` + : timeout (`natural` | `ident`) `tacexpr3` + : time [`string`] `tacexpr3` + : only `selector`: `tacexpr3` + : `tacexpr2` tacexpr2 : `tacexpr1` || `tacexpr3` - : | `tacexpr1` + `tacexpr3` - : | tryif `tacexpr1` then `tacexpr1` else `tacexpr1` - : | `tacexpr1` + : `tacexpr1` + `tacexpr3` + : tryif `tacexpr1` then `tacexpr1` else `tacexpr1` + : `tacexpr1` tacexpr1 : fun `name` ... `name` => `atom` - : | let [rec] `let_clause` with ... with `let_clause` in `atom` - : | match goal with `context_rule` | ... | `context_rule` end - : | match reverse goal with `context_rule` | ... | `context_rule` end - : | match `expr` with `match_rule` | ... | `match_rule` end - : | lazymatch goal with `context_rule` | ... | `context_rule` end - : | lazymatch reverse goal with `context_rule` | ... | `context_rule` end - : | lazymatch `expr` with `match_rule` | ... | `match_rule` end - : | multimatch goal with `context_rule` | ... | `context_rule` end - : | multimatch reverse goal with `context_rule` | ... | `context_rule` end - : | multimatch `expr` with `match_rule` | ... | `match_rule` end - : | abstract `atom` - : | abstract `atom` using `ident` - : | first [ `expr` | ... | `expr` ] - : | solve [ `expr` | ... | `expr` ] - : | idtac [ `message_token` ... `message_token`] - : | fail [`natural`] [`message_token` ... `message_token`] - : | fresh [ `component` … `component` ] - : | context `ident` [`term`] - : | eval `redexpr` in `term` - : | type of `term` - : | constr : `term` - : | uconstr : `term` - : | type_term `term` - : | numgoals - : | guard `test` - : | assert_fails `tacexpr3` - : | assert_succeeds `tacexpr3` - : | `atomic_tactic` - : | `qualid` `tacarg` ... `tacarg` - : | `atom` + : let [rec] `let_clause` with ... with `let_clause` in `atom` + : match goal with `context_rule` | ... | `context_rule` end + : match reverse goal with `context_rule` | ... | `context_rule` end + : match `expr` with `match_rule` | ... | `match_rule` end + : lazymatch goal with `context_rule` | ... | `context_rule` end + : lazymatch reverse goal with `context_rule` | ... | `context_rule` end + : lazymatch `expr` with `match_rule` | ... | `match_rule` end + : multimatch goal with `context_rule` | ... | `context_rule` end + : multimatch reverse goal with `context_rule` | ... | `context_rule` end + : multimatch `expr` with `match_rule` | ... | `match_rule` end + : abstract `atom` + : abstract `atom` using `ident` + : first [ `expr` | ... | `expr` ] + : solve [ `expr` | ... | `expr` ] + : idtac [ `message_token` ... `message_token`] + : fail [`natural`] [`message_token` ... `message_token`] + : fresh [ `component` … `component` ] + : context `ident` [`term`] + : eval `redexpr` in `term` + : type of `term` + : constr : `term` + : uconstr : `term` + : type_term `term` + : numgoals + : guard `test` + : assert_fails `tacexpr3` + : assert_succeeds `tacexpr3` + : `atomic_tactic` + : `qualid` `tacarg` ... `tacarg` + : `atom` atom : `qualid` - : | () - : | `integer` - : | ( `expr` ) + : () + : `integer` + : ( `expr` ) component : `string` | `qualid` message_token : `string` | `ident` | `integer` tacarg : `qualid` - : | () - : | ltac : `atom` - : | `term` + : () + : ltac : `atom` + : `term` let_clause : `ident` [`name` ... `name`] := `expr` context_rule : `context_hyp`, ..., `context_hyp` |- `cpattern` => `expr` - : | `cpattern` => `expr` - : | |- `cpattern` => `expr` - : | _ => `expr` + : `cpattern` => `expr` + : |- `cpattern` => `expr` + : _ => `expr` context_hyp : `name` : `cpattern` - : | `name` := `cpattern` [: `cpattern`] + : `name` := `cpattern` [: `cpattern`] match_rule : `cpattern` => `expr` - : | context [ident] [ `cpattern` ] => `expr` - : | _ => `expr` + : context [`ident`] [ `cpattern` ] => `expr` + : _ => `expr` test : `integer` = `integer` - : | `integer` (< | <= | > | >=) `integer` + : `integer` (< | <= | > | >=) `integer` selector : [`ident`] - : | `integer` - : | (`integer` | `integer` - `integer`), ..., (`integer` | `integer` - `integer`) + : `integer` + : (`integer` | `integer` - `integer`), ..., (`integer` | `integer` - `integer`) toplevel_selector : `selector` - : | all - : | par - : | ! + : all + : par + : ! .. productionlist:: coq top : [Local] Ltac `ltac_def` with ... with `ltac_def` ltac_def : `ident` [`ident` ... `ident`] := `expr` - : | `qualid` [`ident` ... `ident`] ::= `expr` + : `qualid` [`ident` ... `ident`] ::= `expr` .. _ltac-semantics: diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index bffbe3e284..483dbd311d 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1445,6 +1445,16 @@ section constant. If tactic is ``move`` or ``case`` and an equation :token:`ident` is given, then clear (step 3) for :token:`d_item` is suppressed (see section :ref:`generation_of_equations_ssr`). +Intro patterns (see section :ref:`introduction_ssr`) +and the ``rewrite`` tactic (see section :ref:`rewriting_ssr`) +let one place a :token:`clear_switch` in the middle of other items +(namely identifiers, views and rewrite rules). This can trigger the +addition of proof context items to the ones being explicitly +cleared, and in turn this can result in clear errors (e.g. if the +context item automatically added occurs in the goal). The +relevant sections describe ways to avoid the unintended clear of +context items. + Matching for apply and exact ```````````````````````````` @@ -1559,7 +1569,7 @@ whose general syntax is i_view ::= {? %{%} } /@term %| /ltac:( @tactic ) .. prodn:: - i_pattern ::= @ident %| > @ident %| _ %| ? %| * %| + %| {? @occ_switch } -> %| {? @occ_switch }<- %| [ {?| @i_item } ] %| - %| [: {+ @ident } ] + i_pattern ::= @ident %| > %| _ %| ? %| * %| + %| {? @occ_switch } -> %| {? @occ_switch }<- %| [ {?| @i_item } ] %| - %| [: {+ @ident } ] .. prodn:: i_block ::= [^ @ident ] %| [^~ @ident ] %| [^~ @num ] @@ -1572,6 +1582,9 @@ The :token:`i_pattern`\s can be seen as a variant of *intro patterns* (see :tacn:`intros`:) each performs an introduction operation, i.e., pops some variables or assumptions from the goal. +Simplification items +````````````````````` + 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 @@ -1583,18 +1596,32 @@ An :token:`s_item` can simplify the set of subgoals or the subgoals themselves: ``/= //``, i.e., ``simpl; try done``. -When an :token:`s_item` bears a :token:`clear_switch`, then the +When an :token:`s_item` immediately precedes a :token:`clear_switch`, then the :token:`clear_switch` is executed *after* the :token:`s_item`, e.g., ``{IHn}//`` will solve some subgoals, possibly using the fact ``IHn``, and will erase ``IHn`` from the context of the remaining subgoals. +Views +````` + The first entry in the :token:`i_view` grammar rule, :n:`/@term`, represents a view (see section :ref:`views_and_reflection_ssr`). It 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. +It is equivalent to :n:`move/@term`. + +A :token:`clear_switch` that immediately precedes an :token:`i_view` +is complemented with the name of the view if an only if the :token:`i_view` +is a simple proof context entry [#10]_. +E.g. ``{}/v`` is equivalent to ``/v{v}``. +This behavior can be avoided by separating the :token:`clear_switch` +from the :token:`i_view` with the ``-`` intro pattern or by putting +parentheses around the view. + +A :token:`clear_switch` that immediately precedes an :token:`i_view` +is executed after the view application. + + If the next :token:`i_item` is a view, then the view is applied to the assumption in top position once all the previous :token:`i_item` have been performed. @@ -1608,6 +1635,9 @@ Notations can be used to name tactics, for example:: lets one write just ``/myop`` in the intro pattern. Note the scope annotation: views are interpreted opening the ``ssripat`` scope. +Intro patterns +`````````````` + |SSR| supports the following :token:`i_pattern`\s: :token:`ident` @@ -1615,16 +1645,24 @@ annotation: views are interpreted opening the ``ssripat`` scope. a new constant, fact, or defined constant :token:`ident`, respectively. Note that defined constants cannot be introduced when δ-expansion is required to expose the top variable or assumption. -``>``:token:`ident` - pops the first assumption. Type class instances are not considered - as assumptions. - The tactic ``move=> >H`` is equivalent to - ``move=> ? ? H`` with enough ``?`` to name ``H`` the first assumption. - On a goal:: + A :token:`clear_switch` (even an empty one) immediately preceding an + :token:`ident` is complemented with that :token:`ident` if and only if + the identifier is a simple proof context entry [#10]_. + As a consequence by prefixing the + :token:`ident` with ``{}`` one can *replace* a context entry. + This behavior can be avoided by separating the :token:`clear_switch` + from the :token:`ident` with the ``-`` intro pattern. +``>`` + pops every variable occurring in the rest of the stack. + Type class instances are popped even if they don't occur + in the rest of the stack. + The tactic ``move=> >`` is equivalent to + ``move=> ? ?`` on a goal such as:: forall x y, x < y -> G - it names ``H`` the assumption ``x < y``. + A typical use if ``move=>> H`` to name ``H`` the first assumption, + in the example above ``x < y``. ``?`` pops the top variable into an anonymous constant or fact, whose name is picked by the tactic interpreter. |SSR| only generates names that cannot @@ -1707,6 +1745,9 @@ annotation: views are interpreted opening the ``ssripat`` scope. Note that |SSR| does not support the syntax ``(ipat, …, ipat)`` for destructing intro-patterns. +Clear switch +```````````` + Clears are deferred until the end of the intro pattern. .. example:: @@ -1729,6 +1770,9 @@ is performed behind the scenes. Facts mentioned in a clear switch must be valid names in the proof context (excluding the section context). +Branching and destructuring +``````````````````````````` + The rules for interpreting branching and destructing :token:`i_pattern` are motivated by the fact that it would be pointless to have a branching pattern if tactic is a ``move``, and in most of the remaining cases @@ -1753,6 +1797,9 @@ interpretation, e.g.: are all equivalent. +Block introduction +`````````````````` + |SSR| supports the following :token:`i_block`\s: :n:`[^ @ident ]` @@ -3029,13 +3076,22 @@ operation should be performed: pattern. In its simplest form, it is a regular term. If no explicit redex switch is present the rewrite pattern to be matched is inferred from the :token:`r_item`. -+ This optional term, or the :token:`r_item`, may be preceded by an occurrence - switch (see section :ref:`selectors_ssr`) or a clear item - (see section :ref:`discharge_ssr`), - these two possibilities being exclusive. An occurrence switch selects ++ This optional term, or the :token:`r_item`, may be preceded by an + :token:`occ_switch` (see section :ref:`selectors_ssr`) or a + :token:`clear_switch` (see section :ref:`discharge_ssr`), + these two possibilities being exclusive. + + An occurrence switch selects the occurrences of the rewrite pattern which should be affected by the rewrite operation. + A clear switch, even an empty one, is performed *after* the + :token:`r_item` is actually processed and is complemented with the name of + the rewrite rule if an only if it is a simple proof context entry [#10]_. + As a consequence one can + write ``rewrite {}H`` to rewrite with ``H`` and dispose ``H`` immediately + afterwards. + This behavior can be avoided by putting parentheses around the rewrite rule. An :token:`r_item` can be: @@ -3290,10 +3346,6 @@ 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 ``````````````````````````````````` @@ -5305,7 +5357,7 @@ discharge item see :ref:`discharge_ssr` generalization item see :ref:`structure_ssr` -.. prodn:: i_pattern ::= @ident %| > @ident %| _ %| ? %| * %| + %| {? @occ_switch } -> %| {? @occ_switch } <- %| [ {?| @i_item } ] %| - %| [: {+ @ident } ] +.. prodn:: i_pattern ::= @ident %| > %| _ %| ? %| * %| + %| {? @occ_switch } -> %| {? @occ_switch } <- %| [ {?| @i_item } ] %| - %| [: {+ @ident } ] intro pattern :ref:`introduction_ssr` @@ -5519,3 +5571,5 @@ Settings in the metatheory .. [#9] The current state of the proof shall be displayed by the Show Proof command of |Coq| proof mode. +.. [#10] A simple proof context entry is a naked identifier (i.e. not between + parentheses) designating a context entry that is not a section variable. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 59602581c7..7eef504ea9 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -33,10 +33,13 @@ extends the folklore notion of tactical) to combine those atomic tactics. This chapter is devoted to atomic tactics. The tactic language will be described in Chapter :ref:`ltac`. +Common elements of tactics +-------------------------- + .. _invocation-of-tactics: Invocation of tactics -------------------------- +~~~~~~~~~~~~~~~~~~~~~ A tactic is applied as an ordinary command. It may be preceded by a goal selector (see Section :ref:`ltac-semantics`). If no selector is @@ -44,9 +47,9 @@ specified, the default selector is used. .. _tactic_invocation_grammar: - .. productionlist:: `sentence` - tactic_invocation : toplevel_selector : tactic. - : |tactic . + .. productionlist:: sentence + tactic_invocation : `toplevel_selector` : `tactic`. + : `tactic`. .. opt:: Default Goal Selector "@toplevel_selector" :name: Default Goal Selector @@ -71,29 +74,31 @@ specified, the default selector is used. Bindings list ~~~~~~~~~~~~~~~~~~~ -Tactics that take a term as argument may also support a bindings list, -so as to instantiate some parameters of the term by name or position. -The general form of a term equipped with a bindings list is ``term with -bindings_list`` where ``bindings_list`` may be of two different forms: +Tactics that take a term as an argument may also support a bindings list +to instantiate some parameters of the term by name or position. +The general form of a term with a bindings list is +:n:`@term with @bindings_list` where :token:`bindings_list` can take two different forms: .. _bindings_list_grammar: - .. productionlist:: `bindings_list` - bindings_list : (ref := `term`) ... (ref := `term`) + .. productionlist:: bindings_list + ref : `ident` + : `num` + bindings_list : (`ref` := `term`) ... (`ref` := `term`) : `term` ... `term` -+ In a bindings list of the form :n:`{* (ref:= term)}`, :n:`ref` is either an ++ In a bindings list of the form :n:`{+ (@ref:= @term)}`, :n:`@ref` is either an :n:`@ident` or a :n:`@num`. The references are determined according to the type of - ``term``. If :n:`ref` is an identifier, this identifier has to be bound in the - type of ``term`` and the binding provides the tactic with an instance for the - parameter of this name. If :n:`ref` is some number ``n``, this number denotes - the ``n``-th non dependent premise of the ``term``, as determined by the type - of ``term``. + :n:`@term`. If :n:`@ref` is an identifier, this identifier has to be bound in the + type of :n:`@term` and the binding provides the tactic with an instance for the + parameter of this name. If :n:`@ref` is a number ``n``, it refers to + the ``n``-th non dependent premise of the :n:`@term`, as determined by the type + of :n:`@term`. .. exn:: No such binder. :undocumented: -+ A bindings list can also be a simple list of terms :n:`{* term}`. ++ A bindings list can also be a simple list of terms :n:`{* @term}`. In that case the references to which these terms correspond are determined by the tactic. In case of :tacn:`induction`, :tacn:`destruct`, :tacn:`elim` and :tacn:`case`, the terms have to @@ -105,6 +110,350 @@ bindings_list`` where ``bindings_list`` may be of two different forms: .. exn:: Not the right number of missing arguments. :undocumented: +.. _intropatterns: + +Intro patterns +~~~~~~~~~~~~~~ + +Intro patterns let you specify the name to assign to variables and hypotheses +introduced by tactics. They also let you split an introduced hypothesis into +multiple hypotheses or subgoals. Common tactics that accept intro patterns +include :tacn:`assert`, :tacn:`intros` and :tacn:`destruct`. + +.. productionlist:: coq + intropattern_list : `intropattern` ... `intropattern` + : `empty` + empty : + intropattern : * + : ** + : `simple_intropattern` + simple_intropattern : `simple_intropattern_closed` [ % `term` ... % `term` ] + simple_intropattern_closed : `naming_intropattern` + : _ + : `or_and_intropattern` + : `equality_intropattern` + naming_intropattern : `ident` + : ? + : ?`ident` + or_and_intropattern : [ `intropattern_list` | ... | `intropattern_list` ] + : ( `simple_intropattern` , ... , `simple_intropattern` ) + : ( `simple_intropattern` & ... & `simple_intropattern` ) + equality_intropattern : -> + : <- + : [= `intropattern_list` ] + or_and_intropattern_loc : `or_and_intropattern` + : `ident` + +Note that the intro pattern syntax varies between tactics. +Most tactics use :n:`@simple_intropattern` in the grammar. +:tacn:`destruct`, :tacn:`edestruct`, :tacn:`induction`, +:tacn:`einduction`, :tacn:`case`, :tacn:`ecase` and the various +:tacn:`inversion` tactics use :n:`@or_and_intropattern_loc`, while +:tacn:`intros` and :tacn:`eintros` use :n:`@intropattern_list`. +The :n:`eqn:` construct in various tactics uses :n:`@naming_intropattern`. + +**Naming patterns** + +Use these elementary patterns to specify a name: + +* :n:`@ident` - use the specified name +* :n:`?` - let Coq choose a name +* :n:`?@ident` - generate a name that begins with :n:`@ident` +* :n:`_` - discard the matched part (unless it is required for another + hypothesis) +* if a disjunction pattern omits a name, such as :g:`[|H2]`, Coq will choose a name + +**Splitting patterns** + +The most common splitting patterns are: + +* split a hypothesis in the form :n:`A /\ B` into two + hypotheses :g:`H1: A` and :g:`H2: B` using the pattern :g:`(H1 & H2)` or + :g:`(H1, H2)` or :g:`[H1 H2]`. + :ref:`Example <intropattern_conj_ex>`. This also works on :n:`A <-> B`, which + is just a notation representing :n:`(A -> B) /\ (B -> A)`. +* split a hypothesis in the form :g:`A \/ B` into two + subgoals using the pattern :g:`[H1|H2]`. The first subgoal will have the hypothesis + :g:`H1: A` and the second subgoal will have the hypothesis :g:`H2: B`. + :ref:`Example <intropattern_disj_ex>` +* split a hypothesis in either of the forms :g:`A /\ B` or :g:`A \/ B` using the pattern :g:`[]`. + +Patterns can be nested: :n:`[[Ha|Hb] H]` can be used to split :n:`(A \/ B) /\ C`. + +Note that there is no equivalent to intro patterns for goals. For a goal :g:`A /\ B`, +use the :tacn:`split` tactic to replace the current goal with subgoals :g:`A` and :g:`B`. +For a goal :g:`A \/ B`, use :tacn:`left` to replace the current goal with :g:`A`, or +:tacn:`right` to replace the current goal with :g:`B`. + +* :n:`( {+, @simple_intropattern}` ) - matches + a product over an inductive type with a + :ref:`single constructor <intropattern_cons_note>`. + If the number of patterns + equals the number of constructor arguments, then it applies the patterns only to + the arguments, and + :n:`( {+, @simple_intropattern} )` is equivalent to :n:`[{+ @simple_intropattern}]`. + If the number of patterns equals the number of constructor arguments plus the number + of :n:`let-ins`, the patterns are applied to the arguments and :n:`let-in` variables. + +* :n:`( {+& @simple_intropattern} )` - matches a right-hand nested term that consists + of one or more nested binary inductive types such as :g:`a1 OP1 a2 OP2 ...` + (where the :g:`OPn` are right-associative). + (If the :g:`OPn` are left-associative, additional parentheses will be needed to make the + term right-hand nested, such as :g:`a1 OP1 (a2 OP2 ...)`.) + The splitting pattern can have more than 2 names, for example :g:`(H1 & H2 & H3)` + matches :g:`A /\ B /\ C`. + The inductive types must have a + :ref:`single constructor with two parameters <intropattern_cons_note>`. + :ref:`Example <intropattern_ampersand_ex>` + +* :n:`[ {+| @intropattern_list} ]` - splits an inductive type that has + :ref:`multiple constructors <intropattern_cons_note>` + such as :n:`A \/ B` + into multiple subgoals. The number of :token:`intropattern_list` must be the same as the number of + constructors for the matched part. +* :n:`[ {+ @intropattern} ]` - splits an inductive type that has a + :ref:`single constructor with multiple parameters <intropattern_cons_note>` + such as :n:`A /\ B` into multiple hypotheses. Use :n:`[H1 [H2 H3]]` to match :g:`A /\ B /\ C`. +* :n:`[]` - splits an inductive type: If the inductive + type has multiple constructors, such as :n:`A \/ B`, + create one subgoal for each constructor. If the inductive type has a single constructor with + multiple parameters, such as :n:`A /\ B`, split it into multiple hypotheses. + +**Equality patterns** + +These patterns can be used when the hypothesis is an equality: + +* :n:`->` - replaces the right-hand side of the hypothesis with the left-hand + side of the hypothesis in the conclusion of the goal; the hypothesis is + cleared; if the left-hand side of the hypothesis is a variable, it is + substituted everywhere in the context and the variable is removed. + :ref:`Example <intropattern_rarrow_ex>` +* :n:`<-` - similar to :n:`->`, but replaces the left-hand side of the hypothesis + with the right-hand side of the hypothesis. +* :n:`[= {*, @intropattern} ]` - If the product is over an equality type, + applies either :tacn:`injection` or :tacn:`discriminate`. + If :tacn:`injection` is applicable, the intropattern + is used on the hypotheses generated by :tacn:`injection`. If the + number of patterns is smaller than the number of hypotheses generated, the + pattern :n:`?` is used to complete the list. + :ref:`Example <intropattern_inj_discr_ex>` + +**Other patterns** + +* :n:`*` - introduces one or more quantified variables from the result + until there are no more quantified variables. + :ref:`Example <intropattern_star_ex>` + +* :n:`**` - introduces one or more quantified variables or hypotheses from the result until there are + no more quantified variables or implications (:g:`->`). :g:`intros **` is equivalent + to :g:`intros`. + :ref:`Example <intropattern_2stars_ex>` + +* :n:`@simple_intropattern_closed {* % @term}` - first applies each of the terms + with the :tacn:`apply ... in` tactic on the hypothesis to be introduced, then it uses + :n:`@simple_intropattern_closed`. + :ref:`Example <intropattern_injection_ex>` + +.. flag:: Bracketing Last Introduction Pattern + + For :n:`intros @intropattern_list`, controls how to handle a + conjunctive pattern that doesn't give enough simple patterns to match + all the arguments in the constructor. If set (the default), |Coq| generates + additional names to match the number of arguments. + Unsetting the option will put the additional hypotheses in the goal instead, behavior that is more + similar to |SSR|'s intro patterns. + + .. deprecated:: 8.10 + +.. _intropattern_cons_note: + +.. note:: + + :n:`A \/ B` and :n:`A /\ B` use infix notation to refer to the inductive + types :n:`or` and :n:`and`. + :n:`or` has multiple constructors (:n:`or_introl` and :n:`or_intror`), + while :n:`and` has a single constructor (:n:`conj`) with multiple parameters + (:n:`A` and :n:`B`). + These are defined in theories/Init/Logic.v. The "where" clauses define the + infix notation for "or" and "and". + + .. coqdoc:: + + Inductive or (A B:Prop) : Prop := + | or_introl : A -> A \/ B + | or_intror : B -> A \/ B + where "A \/ B" := (or A B) : type_scope. + + Inductive and (A B:Prop) : Prop := + conj : A -> B -> A /\ B + where "A /\ B" := (and A B) : type_scope. + +.. note:: + + :n:`intros {+ p}` is not always equivalent to :n:`intros p; ... ; intros p` + if some of the :n:`p` are :g:`_`. In the first form, all erasures are done + at once, while they're done sequentially for each tactic in the second form. + If the second matched term depends on the first matched term and the pattern + for both is :g:`_` (i.e., both will be erased), the first :n:`intros` in the second + form will fail because the second matched term still has the dependency on the first. + +Examples: + +.. _intropattern_conj_ex: + + .. example:: intro pattern for /\\ + + .. coqtop:: reset none + + Goal forall (A: Prop) (B: Prop), (A /\ B) -> True. + + .. coqtop:: out + + intros. + + .. coqtop:: all + + destruct H as (HA & HB). + +.. _intropattern_disj_ex: + + .. example:: intro pattern for \\/ + + .. coqtop:: reset none + + Goal forall (A: Prop) (B: Prop), (A \/ B) -> True. + + .. coqtop:: out + + intros. + + .. coqtop:: all + + destruct H as [HA|HB]. all: swap 1 2. + +.. _intropattern_rarrow_ex: + + .. example:: -> intro pattern + + .. coqtop:: reset none + + Goal forall (x:nat) (y:nat) (z:nat), (x = y) -> (y = z) -> (x = z). + + .. coqtop:: out + + intros * H. + + .. coqtop:: all + + intros ->. + +.. _intropattern_inj_discr_ex: + + .. example:: [=] intro pattern + + The first :n:`intros [=]` uses :tacn:`injection` to strip :n:`(S ...)` from + both sides of the matched equality. The second uses :tacn:`discriminate` on + the contradiction :n:`1 = 2` (internally represented as :n:`(S O) = (S (S O))`) + to complete the goal. + + .. coqtop:: reset none + + Goal forall (n m:nat), (S n) = (S m) -> (S O)=(S (S O)) -> False. + + .. coqtop:: out + + intros *. + + .. coqtop:: all + + intros [= H]. + + .. coqtop:: all + + intros [=]. + +.. _intropattern_ampersand_ex: + + .. example:: (A & B & ...) intro pattern + + .. coqtop:: reset none + + Variables (A : Prop) (B: nat -> Prop) (C: Prop). + + .. coqtop:: out + + Goal A /\ (exists x:nat, B x /\ C) -> True. + + .. coqtop:: all + + intros (a & x & b & c). + +.. _intropattern_star_ex: + + .. example:: * intro pattern + + .. coqtop:: reset out + + Goal forall (A: Prop) (B: Prop), A -> B. + + .. coqtop:: all + + intros *. + +.. _intropattern_2stars_ex: + + .. example:: ** pattern ("intros \**" is equivalent to "intros") + + .. coqtop:: reset out + + Goal forall (A: Prop) (B: Prop), A -> B. + + .. coqtop:: all + + intros **. + + .. example:: compound intro pattern + + .. coqtop:: reset out + + Goal forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C. + + .. coqtop:: all + + intros * [a | (_,c)] f. + all: swap 1 2. + +.. _intropattern_injection_ex: + + .. example:: combined intro pattern using [=] -> and % + + .. coqtop:: reset none + + Require Import Coq.Lists.List. + Section IntroPatterns. + Variables (A : Type) (xs ys : list A). + + .. coqtop:: out + + Example ThreeIntroPatternsCombined : + S (length ys) = 1 -> xs ++ ys = xs. + + .. coqtop:: all + + intros [=->%length_zero_iff_nil]. + + * `intros` would add :g:`H : S (length ys) = 1` + * `intros [=]` would additionally apply :tacn:`injection` to :g:`H` to yield :g:`H0 : length ys = 0` + * `intros [=->%length_zero_iff_nil]` applies the theorem, making H the equality :g:`l=nil`, + which is then applied as for :g:`->`. + + .. coqdoc:: + + Theorem length_zero_iff_nil (l : list A): + length l = 0 <-> l=nil. + + The example is based on `Tej Chajed's coq-tricks <https://github.com/tchajed/coq-tricks/blob/8e6efe4971ed828ac8bdb5512c1f615d7d62691e/src/IntroPatterns.v>`_ + .. _occurrencessets: Occurrence sets and occurrence clauses @@ -113,11 +462,11 @@ Occurrence sets and occurrence clauses An occurrence clause is a modifier to some tactics that obeys the following syntax: - .. productionlist:: `sentence` + .. productionlist:: sentence occurrence_clause : in `goal_occurrences` - goal_occurrences : [`ident` [`at_occurrences`], ... , ident [`at_occurrences`] [|- [* [`at_occurrences`]]]] - :| * |- [* [`at_occurrences`]] - :| * + goal_occurrences : [`ident` [`at_occurrences`], ... , `ident` [`at_occurrences`] [|- [* [`at_occurrences`]]]] + : * |- [* [`at_occurrences`]] + : * at_occurrences : at `occurrences` occurrences : [-] `num` ... `num` @@ -508,10 +857,10 @@ Applying theorems This works as :tacn:`apply ... in` but turns unresolved bindings into existential variables, if any, instead of failing. - .. tacv:: apply {+, @term {? with @bindings_list } } in @ident as @intro_pattern + .. tacv:: apply {+, @term {? with @bindings_list } } in @ident as @simple_intropattern :name: apply ... in ... as - This works as :tacn:`apply ... in` then applies the :token:`intro_pattern` + This works as :tacn:`apply ... in` then applies the :token:`simple_intropattern` to the hypothesis :token:`ident`. .. tacv:: simple apply @term in @ident @@ -525,8 +874,8 @@ Applying theorems Tactic :n:`simple apply @term in @ident` does not either traverse tuples as :n:`apply @term in @ident` does. - .. tacv:: {? simple} apply {+, @term {? with @bindings_list}} in @ident {? as @intro_pattern} - {? simple} eapply {+, @term {? with @bindings_list}} in @ident {? as @intro_pattern} + .. tacv:: {? simple} apply {+, @term {? with @bindings_list}} in @ident {? as @simple_intropattern} + {? simple} eapply {+, @term {? with @bindings_list}} in @ident {? as @simple_intropattern} This summarizes the different syntactic variants of :n:`apply @term in @ident` and :n:`eapply @term in @ident`. @@ -726,149 +1075,17 @@ Managing the local context .. exn:: No such hypothesis: @ident. :undocumented: -.. tacn:: intros @intro_pattern_list +.. tacn:: intros @intropattern_list :name: intros ... - This extension of the tactic :n:`intros` allows to apply tactics on the fly - on the variables or hypotheses which have been introduced. An - *introduction pattern list* :n:`@intro_pattern_list` is a list of - introduction patterns possibly containing the filling introduction - patterns `*` and `**`. An *introduction pattern* is either: - - + a *naming introduction pattern*, i.e. either one of: - - + the pattern :n:`?` - - + the pattern :n:`?ident` - - + an identifier - - + an *action introduction pattern* which itself classifies into: - - + a *disjunctive/conjunctive introduction pattern*, i.e. either one of - - + a disjunction of lists of patterns - :n:`[@intro_pattern_list | ... | @intro_pattern_list]` - - + a conjunction of patterns: :n:`({+, p})` - - + a list of patterns - :n:`({+& p})` - for sequence of right-associative binary constructs - - + an *equality introduction pattern*, i.e. either one of: - - + a pattern for decomposing an equality: :n:`[= {+ p}]` - + the rewriting orientations: :n:`->` or :n:`<-` - - + the on-the-fly application of lemmas: :n:`p{+ %term}` where :n:`p` - itself is not a pattern for on-the-fly application of lemmas (note: - syntax is in experimental stage) - - + the wildcard: :n:`_` - - - Assuming a goal of type :g:`Q → P` (non-dependent product), or of type - :g:`forall x:T, P` (dependent product), the behavior of - :n:`intros p` is defined inductively over the structure of the introduction - pattern :n:`p`: - - Introduction on :n:`?` performs the introduction, and lets Coq choose a fresh - name for the variable; - - Introduction on :n:`?@ident` performs the introduction, and lets Coq choose a - fresh name for the variable based on :n:`@ident`; - - Introduction on :n:`@ident` behaves as described in :tacn:`intro` - - Introduction over a disjunction of list of patterns - :n:`[@intro_pattern_list | ... | @intro_pattern_list ]` expects the product - to be over an inductive type whose number of constructors is `n` (or more - generally over a type of conclusion an inductive type built from `n` - constructors, e.g. :g:`C -> A\/B` with `n=2` since :g:`A\/B` has `2` - constructors): it destructs the introduced hypothesis as :n:`destruct` (see - :tacn:`destruct`) would and applies on each generated subgoal the - corresponding tactic; - - The introduction patterns in :n:`@intro_pattern_list` are expected to consume - no more than the number of arguments of the `i`-th constructor. If it - consumes less, then Coq completes the pattern so that all the arguments of - the constructors of the inductive type are introduced (for instance, the - list of patterns :n:`[ | ] H` applied on goal :g:`forall x:nat, x=0 -> 0=x` - behaves the same as the list of patterns :n:`[ | ? ] H`); - - Introduction over a conjunction of patterns :n:`({+, p})` expects - the goal to be a product over an inductive type :g:`I` with a single - constructor that itself has at least `n` arguments: It performs a case - analysis over the hypothesis, as :n:`destruct` would, and applies the - patterns :n:`{+ p}` to the arguments of the constructor of :g:`I` (observe - that :n:`({+ p})` is an alternative notation for :n:`[{+ p}]`); - - Introduction via :n:`({+& p})` is a shortcut for introduction via - :n:`(p,( ... ,( ..., p ) ... ))`; it expects the hypothesis to be a sequence of - right-associative binary inductive constructors such as :g:`conj` or - :g:`ex_intro`; for instance, a hypothesis with type - :g:`A /\(exists x, B /\ C /\ D)` can be introduced via pattern - :n:`(a & x & b & c & d)`; - - If the product is over an equality type, then a pattern of the form - :n:`[= {+ p}]` applies either :tacn:`injection` or :tacn:`discriminate` - instead of :tacn:`destruct`; if :tacn:`injection` is applicable, the patterns - :n:`{+, p}` are used on the hypotheses generated by :tacn:`injection`; if the - number of patterns is smaller than the number of hypotheses generated, the - pattern :n:`?` is used to complete the list. - - Introduction over ``->`` (respectively over ``<-``) - expects the hypothesis to be an equality and the right-hand-side - (respectively the left-hand-side) is replaced by the left-hand-side - (respectively the right-hand-side) in the conclusion of the goal; - the hypothesis itself is erased; if the term to substitute is a variable, it - is substituted also in the context of goal and the variable is removed too. - - Introduction over a pattern :n:`p{+ %term}` first applies :n:`{+ term}` - on the hypothesis to be introduced (as in :n:`apply {+, term}`) prior to the - application of the introduction pattern :n:`p`; - - Introduction on the wildcard depends on whether the product is dependent or not: - in the non-dependent case, it erases the corresponding hypothesis (i.e. it - behaves as an :tacn:`intro` followed by a :tacn:`clear`) while in the - dependent case, it succeeds and erases the variable only if the wildcard is part - of a more complex list of introduction patterns that also erases the hypotheses - depending on this variable; - - Introduction over :n:`*` introduces all forthcoming quantified variables - appearing in a row; introduction over :n:`**` introduces all forthcoming - quantified variables or hypotheses until the goal is not any more a - quantification or an implication. - - .. example:: - - .. coqtop:: reset all - - Goal forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C. - intros * [a | (_,c)] f. - -.. note:: - - :n:`intros {+ p}` is not equivalent to :n:`intros p; ... ; intros p` - for the following reason: If one of the :n:`p` is a wildcard pattern, it - might succeed in the first case because the further hypotheses it - depends on are eventually erased too while it might fail in the second - case because of dependencies in hypotheses which are not yet - introduced (and a fortiori not yet erased). - -.. note:: - - In :n:`intros @intro_pattern_list`, if the last introduction pattern - is a disjunctive or conjunctive pattern - :n:`[{+| @intro_pattern_list}]`, the completion of :n:`@intro_pattern_list` - so that all the arguments of the i-th constructors of the corresponding - inductive type are introduced can be controlled with the following option: + Introduces one or more variables or hypotheses from the goal by matching the + intro patterns. See the description in :ref:`intropatterns`. - .. flag:: Bracketing Last Introduction Pattern +.. tacn:: eintros @intropattern_list + :name: eintros - Force completion, if needed, when the last introduction pattern is a - disjunctive or conjunctive pattern (on by default). + Works just like :tacn:`intros ...` except that it creates existential variables + for any unresolved variables rather than failing. .. tacn:: clear @ident :name: clear @@ -1057,19 +1274,19 @@ Managing the local context used as a synonym of :tacn:`epose`, i.e. when the :token:`term` does not occur in the goal. -.. tacn:: remember @term as @ident__1 {? eqn:@ident__2 } +.. tacn:: remember @term as @ident__1 {? eqn:@naming_intropattern } :name: remember - This behaves as :n:`set (@ident__1 := @term) in *`, using a logical + This behaves as :n:`set (@ident := @term) in *`, using a logical (Leibniz’s) equality instead of a local definition. - If :n:`@ident__2` is provided, it will be the name of the new equation. + Use :n:`@naming_intropattern` to name or split up the new equation. - .. tacv:: remember @term as @ident__1 {? eqn:@ident__2 } in @goal_occurrences + .. tacv:: remember @term as @ident__1 {? eqn:@naming_intropattern } in @goal_occurrences This is a more general form of :tacn:`remember` that remembers the occurrences of :token:`term` specified by an occurrence set. - .. tacv:: eremember @term as @ident__1 {? eqn:@ident__2 } {? in @goal_occurrences } + .. tacv:: eremember @term as @ident__1 {? eqn:@naming_intropattern } {? in @goal_occurrences } :name: eremember While the different variants of :tacn:`remember` expect that no @@ -1163,16 +1380,16 @@ Controlling the proof flow :name: Proof is not complete. (assert) :undocumented: - .. tacv:: assert @type as @intro_pattern + .. tacv:: assert @type as @simple_intropattern - If :n:`intro_pattern` is a naming introduction pattern (see :tacn:`intro`), + If :n:`simple_intropattern` is an intro pattern (see :ref:`intropatterns`), the hypothesis is named after this introduction pattern (in particular, if - :n:`intro_pattern` is :n:`@ident`, the tactic behaves like - :n:`assert (@ident : @type)`). If :n:`intro_pattern` is an action + :n:`simple_intropattern` is :n:`@ident`, the tactic behaves like + :n:`assert (@ident : @type)`). If :n:`simple_intropattern` is an action introduction pattern, the tactic behaves like :n:`assert @type` followed by the action done by this introduction pattern. - .. tacv:: assert @type as @intro_pattern by @tactic + .. tacv:: assert @type as @simple_intropattern by @tactic This combines the two previous variants of :tacn:`assert`. @@ -1186,7 +1403,7 @@ Controlling the proof flow .. exn:: Variable @ident is already declared. :undocumented: -.. tacv:: eassert @type as @intro_pattern by @tactic +.. tacv:: eassert @type as @simple_intropattern by @tactic :name: eassert While the different variants of :tacn:`assert` expect that no existential @@ -1194,16 +1411,16 @@ Controlling the proof flow This allows not to specify the asserted statement completeley before starting to prove it. -.. tacv:: pose proof @term {? as @intro_pattern} +.. tacv:: pose proof @term {? as @simple_intropattern} :name: pose proof - This tactic behaves like :n:`assert @type {? as @intro_pattern} by exact @term` + This tactic behaves like :n:`assert @type {? as @simple_intropattern} by exact @term` where :token:`type` is the type of :token:`term`. In particular, :n:`pose proof @term as @ident` behaves as :n:`assert (@ident := @term)` - and :n:`pose proof @term as @intro_pattern` is the same as applying the - :token:`intro_pattern` to :token:`term`. + and :n:`pose proof @term as @simple_intropattern` is the same as applying the + :token:`simple_intropattern` to :token:`term`. -.. tacv:: epose proof @term {? as @intro_pattern} +.. tacv:: epose proof @term {? as @simple_intropattern} :name: epose proof While :tacn:`pose proof` expects that no existential variables are generated by @@ -1221,20 +1438,20 @@ Controlling the proof flow This behaves like :n:`enough (@ident : @type)` with the name :token:`ident` of the hypothesis generated by Coq. -.. tacv:: enough @type as @intro_pattern +.. tacv:: enough @type as @simple_intropattern - This behaves like :n:`enough @type` using :token:`intro_pattern` to name or + This behaves like :n:`enough @type` using :token:`simple_intropattern` to name or destruct the new hypothesis. .. tacv:: enough (@ident : @type) by @tactic - enough @type {? as @intro_pattern } by @tactic + enough @type {? as @simple_intropattern } by @tactic This behaves as above but with :token:`tactic` expected to solve the initial goal after the extra assumption :token:`type` is added and possibly destructed. If the - :n:`as @intro_pattern` clause generates more than one subgoal, :token:`tactic` is + :n:`as @simple_intropattern` clause generates more than one subgoal, :token:`tactic` is applied to all of them. -.. tacv:: eenough @type {? as @intro_pattern } {? by @tactic } +.. tacv:: eenough @type {? as @simple_intropattern } {? by @tactic } eenough (@ident : @type) {? by @tactic } :name: eenough; _ @@ -1250,8 +1467,8 @@ Controlling the proof flow subgoals: :g:`U -> T` and :g:`U`. The subgoal :g:`U -> T` comes first in the list of remaining subgoal to prove. -.. tacv:: specialize (@ident {* @term}) {? as @intro_pattern} - specialize @ident with @bindings_list {? as @intro_pattern} +.. tacv:: specialize (@ident {* @term}) {? as @simple_intropattern} + specialize @ident with @bindings_list {? as @simple_intropattern} :name: specialize; _ This tactic works on local hypothesis :n:`@ident`. The @@ -1264,7 +1481,7 @@ Controlling the proof flow uninstantiated arguments are inferred by unification if possible or left quantified in the hypothesis otherwise. With the :n:`as` clause, the local hypothesis :n:`@ident` is left unchanged and instead, the modified hypothesis - is introduced as specified by the :token:`intro_pattern`. The name :n:`@ident` + is introduced as specified by the :token:`simple_intropattern`. The name :n:`@ident` can also refer to a global lemma or hypothesis. In this case, for compatibility reasons, the behavior of :tacn:`specialize` is close to that of :tacn:`generalize`: the instantiated statement becomes an additional premise of @@ -1477,11 +1694,11 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) This is a shortcut for :n:`destruct @term; ...; destruct @term`. - .. tacv:: destruct @term as @disj_conj_intro_pattern + .. tacv:: destruct @term as @or_and_intropattern_loc This behaves as :n:`destruct @term` but uses the names - in :token:`disj_conj_intro_pattern` to name the variables introduced in the - context. The :token:`disj_conj_intro_pattern` must have the + in :token:`or_and_intropattern_loc` to name the variables introduced in the + context. The :token:`or_and_intropattern_loc` must have the form :n:`[p11 ... p1n | ... | pm1 ... pmn ]` with ``m`` being the number of constructors of the type of :token:`term`. Each variable introduced by :tacn:`destruct` in the context of the ``i``-th goal @@ -1491,13 +1708,13 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) pattern (see :tacn:`intros`). This provides a concise notation for chaining destruction of a hypothesis. - .. tacv:: destruct @term eqn:@naming_intro_pattern + .. tacv:: destruct @term eqn:@naming_intropattern :name: destruct ... eqn: This behaves as :n:`destruct @term` but adds an equation between :token:`term` and the value that it takes in each of the possible cases. The name of the equation is specified - by :token:`naming_intro_pattern` (see :tacn:`intros`), + by :token:`naming_intropattern` (see :tacn:`intros`), in particular ``?`` can be used to let Coq generate a fresh name. .. tacv:: destruct @term with @bindings_list @@ -1525,8 +1742,8 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) clause is an occurrence clause whose syntax and behavior is described in :ref:`occurrences sets <occurrencessets>`. - .. tacv:: destruct @term {? with @bindings_list } {? as @disj_conj_intro_pattern } {? eqn:@naming_intro_pattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences } - edestruct @term {? with @bindings_list } {? as @disj_conj_intro_pattern } {? eqn:@naming_intro_pattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences } + .. tacv:: destruct @term {? with @bindings_list } {? as @or_and_intropattern_loc } {? eqn:@naming_intropattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences } + edestruct @term {? with @bindings_list } {? as @or_and_intropattern_loc } {? eqn:@naming_intropattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences } These are the general forms of :tacn:`destruct` and :tacn:`edestruct`. They combine the effects of the ``with``, ``as``, ``eqn:``, ``using``, @@ -1622,11 +1839,11 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) Use in this case the variant :tacn:`elim ... with` below. -.. tacv:: induction @term as @disj_conj_intro_pattern +.. tacv:: induction @term as @or_and_intropattern_loc This behaves as :tacn:`induction` but uses the names in - :n:`@disj_conj_intro_pattern` to name the variables introduced in the - context. The :n:`@disj_conj_intro_pattern` must typically be of the form + :n:`@or_and_intropattern_loc` to name the variables introduced in the + context. The :n:`@or_and_intropattern_loc` must typically be of the form :n:`[ p` :sub:`11` :n:`... p` :sub:`1n` :n:`| ... | p`:sub:`m1` :n:`... p`:sub:`mn` :n:`]` with :n:`m` being the number of constructors of the type of :n:`@term`. Each variable introduced by induction in the context of the i-th goal gets its @@ -1686,8 +1903,8 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) induction y in x |- *. Show 2. -.. tacv:: induction @term with @bindings_list as @disj_conj_intro_pattern using @term with @bindings_list in @goal_occurrences - einduction @term with @bindings_list as @disj_conj_intro_pattern using @term with @bindings_list in @goal_occurrences +.. tacv:: induction @term with @bindings_list as @or_and_intropattern_loc using @term with @bindings_list in @goal_occurrences + einduction @term with @bindings_list as @or_and_intropattern_loc using @term with @bindings_list in @goal_occurrences These are the most general forms of :tacn:`induction` and :tacn:`einduction`. It combines the effects of the with, as, using, and in clauses. @@ -1898,7 +2115,7 @@ and an explanation of the underlying technique. .. exn:: Not the right number of induction arguments. :undocumented: -.. tacv:: functional induction (@qualid {+ @term}) as @disj_conj_intro_pattern using @term with @bindings_list +.. tacv:: functional induction (@qualid {+ @term}) as @simple_intropattern using @term with @bindings_list Similarly to :tacn:`induction` and :tacn:`elim`, this allows giving explicitly the name of the introduced variables, the induction principle, and @@ -2053,18 +2270,18 @@ and an explanation of the underlying technique. .. exn:: goal does not satisfy the expected preconditions. :undocumented: - .. tacv:: injection @term {? with @bindings_list} as {+ @intro_pattern} - injection @num as {+ intro_pattern} - injection as {+ intro_pattern} - einjection @term {? with @bindings_list} as {+ intro_pattern} - einjection @num as {+ intro_pattern} - einjection as {+ intro_pattern} + .. tacv:: injection @term {? with @bindings_list} as {+ @simple_intropattern} + injection @num as {+ simple_intropattern} + injection as {+ simple_intropattern} + einjection @term {? with @bindings_list} as {+ simple_intropattern} + einjection @num as {+ simple_intropattern} + einjection as {+ simple_intropattern} - These variants apply :n:`intros {+ @intro_pattern}` after the call to + These variants apply :n:`intros {+ @simple_intropattern}` after the call to :tacn:`injection` or :tacn:`einjection` so that all equalities generated are moved in - the context of hypotheses. The number of :n:`@intro_pattern` must not exceed + the context of hypotheses. The number of :n:`@simple_intropattern` must not exceed the number of equalities newly generated. If it is smaller, fresh - names are automatically generated to adjust the list of :n:`@intro_pattern` + names are automatically generated to adjust the list of :n:`@simple_intropattern` to the number of new equalities. The original equality is erased if it corresponds to a hypothesis. @@ -2118,10 +2335,10 @@ and an explanation of the underlying technique. This behaves as :n:`inversion` and then erases :n:`@ident` from the context. -.. tacv:: inversion @ident as @intro_pattern +.. tacv:: inversion @ident as @or_and_intropattern_loc - This generally behaves as inversion but using names in :n:`@intro_pattern` - for naming hypotheses. The :n:`@intro_pattern` must have the form + This generally behaves as inversion but using names in :n:`@or_and_intropattern_loc` + for naming hypotheses. The :n:`@or_and_intropattern_loc` must have the form :n:`[p`:sub:`11` :n:`... p`:sub:`1n` :n:`| ... | p`:sub:`m1` :n:`... p`:sub:`mn` :n:`]` with `m` being the number of constructors of the type of :n:`@ident`. Be careful that the list must be of length `m` even if ``inversion`` discards @@ -2153,12 +2370,12 @@ and an explanation of the underlying technique. Goal forall l:list nat, contains0 (1 :: l) -> contains0 l. intros l H; inversion H as [ | l' p Hl' [Heqp Heql'] ]. -.. tacv:: inversion @num as @intro_pattern +.. tacv:: inversion @num as @or_and_intropattern_loc This allows naming the hypotheses introduced by :n:`inversion @num` in the context. -.. tacv:: inversion_clear @ident as @intro_pattern +.. tacv:: inversion_clear @ident as @or_and_intropattern_loc This allows naming the hypotheses introduced by ``inversion_clear`` in the context. Notice that hypothesis names can be provided as if ``inversion`` @@ -2170,7 +2387,7 @@ and an explanation of the underlying technique. Let :n:`{+ @ident}` be identifiers in the local context. This tactic behaves as generalizing :n:`{+ @ident}`, and then performing ``inversion``. -.. tacv:: inversion @ident as @intro_pattern in {+ @ident} +.. tacv:: inversion @ident as @or_and_intropattern_loc in {+ @ident} This allows naming the hypotheses introduced in the context by :n:`inversion @ident in {+ @ident}`. @@ -2180,7 +2397,7 @@ and an explanation of the underlying technique. Let :n:`{+ @ident}` be identifiers in the local context. This tactic behaves as generalizing :n:`{+ @ident}`, and then performing ``inversion_clear``. -.. tacv:: inversion_clear @ident as @intro_pattern in {+ @ident} +.. tacv:: inversion_clear @ident as @or_and_intropattern_loc in {+ @ident} This allows naming the hypotheses introduced in the context by :n:`inversion_clear @ident in {+ @ident}`. @@ -2192,7 +2409,7 @@ and an explanation of the underlying technique. ``inversion`` and then substitutes :n:`@ident` for the corresponding :n:`@@term` in the goal. -.. tacv:: dependent inversion @ident as @intro_pattern +.. tacv:: dependent inversion @ident as @or_and_intropattern_loc This allows naming the hypotheses introduced in the context by :n:`dependent inversion @ident`. @@ -2202,7 +2419,7 @@ and an explanation of the underlying technique. Like ``dependent inversion``, except that :n:`@ident` is cleared from the local context. -.. tacv:: dependent inversion_clear @ident as @intro_pattern +.. tacv:: dependent inversion_clear @ident as @or_and_intropattern_loc This allows naming the hypotheses introduced in the context by :n:`dependent inversion_clear @ident`. @@ -2216,7 +2433,7 @@ and an explanation of the underlying technique. then :n:`@term` must be of type :g:`I:forall (x:T), I x -> s'` where :g:`s'` is the type of the goal. -.. tacv:: dependent inversion @ident as @intro_pattern with @term +.. tacv:: dependent inversion @ident as @or_and_intropattern_loc with @term This allows naming the hypotheses introduced in the context by :n:`dependent inversion @ident with @term`. @@ -2226,7 +2443,7 @@ and an explanation of the underlying technique. Like :tacn:`dependent inversion ... with ...` with but clears :n:`@ident` from the local context. -.. tacv:: dependent inversion_clear @ident as @intro_pattern with @term +.. tacv:: dependent inversion_clear @ident as @or_and_intropattern_loc with @term This allows naming the hypotheses introduced in the context by :n:`dependent inversion_clear @ident with @term`. @@ -2237,7 +2454,7 @@ and an explanation of the underlying technique. It is a very primitive inversion tactic that derives all the necessary equalities but it does not simplify the constraints as ``inversion`` does. -.. tacv:: simple inversion @ident as @intro_pattern +.. tacv:: simple inversion @ident as @or_and_intropattern_loc This allows naming the hypotheses introduced in the context by ``simple inversion``. @@ -3171,7 +3388,7 @@ Automation :name: auto This tactic implements a Prolog-like resolution procedure to solve the - current goal. It first tries to solve the goal using the assumption + current goal. It first tries to solve the goal using the :tacn:`assumption` tactic, then it reduces the goal to an atomic one using intros and introduces the newly generated hypotheses as hints. Then it looks at the list of tactics associated to the head symbol of the goal and @@ -3586,15 +3803,15 @@ The general command to add a hint to some databases :n:`{+ @ident}` is the following. Beware, there is no operator precedence during parsing, one can check with :cmd:`Print HintDb` to verify the current cut expression: - .. productionlist:: `regexp` - e : ident hint or instance identifier - :| _ any hint - :| e\|e′ disjunction - :| e e′ sequence - :| e * Kleene star - :| emp empty - :| eps epsilon - :| ( e ) + .. productionlist:: regexp + e : `ident` hint or instance identifier + : _ any hint + : `e` | `e` disjunction + : `e` `e` sequence + : `e` * Kleene star + : emp empty + : eps epsilon + : ( `e` ) The `emp` regexp does not match any search path while `eps` matches the empty path. During proof search, the path of @@ -4299,15 +4516,15 @@ Automating .. _btauto_grammar: - .. productionlist:: `sentence` - t : x - :∣ true - :∣ false - :∣ orb t1 t2 - :∣ andb t1 t2 - :∣ xorb t1 t2 - :∣ negb t - :∣ if t1 then t2 else t3 + .. productionlist:: sentence + t : `x` + : true + : false + : orb `t` `t` + : andb `t` `t` + : xorb `t` `t` + : negb `t` + : if `t` then `t` else `t` Whenever the formula supplied is not a tautology, it also provides a counter-example. @@ -4343,7 +4560,7 @@ Automating distributivity, constant propagation) and comparing syntactically the results. -.. tacn:: ring_simplify {+ @term} +.. tacn:: ring_simplify {* @term} :name: ring_simplify This tactic applies the normalization procedure described above to @@ -4357,7 +4574,7 @@ the tactic and how to declare new ring structures. All declared field structures can be printed with the ``Print Rings`` command. .. tacn:: field - field_simplify {+ @term} + field_simplify {* @term} field_simplify_eq :name: field; field_simplify; field_simplify_eq diff --git a/doc/sphinx/refman-preamble.sty b/doc/sphinx/refman-preamble.sty index b4fc608e47..8f7b1bb1e8 100644 --- a/doc/sphinx/refman-preamble.sty +++ b/doc/sphinx/refman-preamble.sty @@ -56,27 +56,29 @@ \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} +\newcommand{\plus}{\mathsf{plus}} \newcommand{\Prod}{\textsf{prod}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\si}{\textsf{if}} \newcommand{\sinon}{\textsf{else}} -\newcommand{\Sort}{\cal S} +\newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} +\newcommand{\trii}{\triangleright_\iota} \newcommand{\true}{\textsf{true}} \newcommand{\Type}{\textsf{Type}} \newcommand{\unfold}{\textsf{unfold}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} -\newcommand{\WF}[2]{{\cal W\!F}(#1)[#2]} +\newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} -\newcommand{\WFT}[2]{#1[] \vdash {\cal W\!F}(#2)} -\newcommand{\WFTWOLINES}[2]{{\cal W\!F}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} +\newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} +\newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 47afa5ba0c..ae66791b0c 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -859,41 +859,41 @@ notations are given below. The optional :production:`scope` is described in .. productionlist:: coq notation : [Local] Notation `string` := `term` [`modifiers`] [: `scope`]. - : | [Local] Infix `string` := `qualid` [`modifiers`] [: `scope`]. - : | [Local] Reserved Notation `string` [`modifiers`] . - : | Inductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`]. - : | CoInductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`]. - : | Fixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`]. - : | CoFixpoint `cofix_body` [`decl_notation`] with … with `cofix_body` [`decl_notation`]. - : | [Local] Declare Custom Entry `ident`. + : [Local] Infix `string` := `qualid` [`modifiers`] [: `scope`]. + : [Local] Reserved Notation `string` [`modifiers`] . + : Inductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`]. + : CoInductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`]. + : Fixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`]. + : CoFixpoint `cofix_body` [`decl_notation`] with … with `cofix_body` [`decl_notation`]. + : [Local] Declare Custom Entry `ident`. decl_notation : [where `string` := `term` [: `scope`] and … and `string` := `term` [: `scope`]]. modifiers : at level `num` : in custom `ident` : in custom `ident` at level `num` - : | `ident` , … , `ident` at level `num` [`binderinterp`] - : | `ident` , … , `ident` at next level [`binderinterp`] - : | `ident` `explicit_subentry` - : | left associativity - : | right associativity - : | no associativity - : | only parsing - : | only printing - : | format `string` + : `ident` , … , `ident` at level `num` [`binderinterp`] + : `ident` , … , `ident` at next level [`binderinterp`] + : `ident` `explicit_subentry` + : left associativity + : right associativity + : no associativity + : only parsing + : only printing + : format `string` explicit_subentry : ident - : | global - : | bigint - : | [strict] pattern [at level `num`] - : | binder - : | closed binder - : | constr [`binderinterp`] - : | constr at level `num` [`binderinterp`] - : | constr at next level [`binderinterp`] - : | custom [`binderinterp`] - : | custom at level `num` [`binderinterp`] - : | custom at next level [`binderinterp`] + : global + : bigint + : [strict] pattern [at level `num`] + : binder + : closed binder + : constr [`binderinterp`] + : constr at level `num` [`binderinterp`] + : constr at next level [`binderinterp`] + : custom [`binderinterp`] + : custom at level `num` [`binderinterp`] + : custom at next level [`binderinterp`] binderinterp : as ident - : | as pattern - : | as strict pattern + : as pattern + : as strict pattern .. note:: No typing of the denoted expression is performed at definition time. Type checking is done only at the time of use of the notation. @@ -1496,12 +1496,13 @@ Numeral notations function returns :g:`None`, or if the interpretation is registered for only non-negative integers, and the given numeral is negative. - .. exn:: @ident should go from Decimal.int to @type or (option @type). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. + + .. exn:: @ident should go from Decimal.int to @type or (option @type). Instead of Decimal.int, the types Decimal.uint or Z could be used (you may need to require BinNums or Decimal first). The parsing function given to the :cmd:`Numeral Notation` vernacular is not of the right type. - .. exn:: @ident should go from @type to Decimal.int or (option Decimal.int). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. + .. exn:: @ident should go from @type to Decimal.int or (option Decimal.int). Instead of Decimal.int, the types Decimal.uint or Z could be used (you may need to require BinNums or Decimal first). The printing function given to the :cmd:`Numeral Notation` vernacular is not of the right type. @@ -1692,13 +1693,13 @@ Tactic notations allow to customize the syntax of tactics. They have the followi tacn : Tactic Notation [`tactic_level`] [`prod_item` … `prod_item`] := `tactic`. prod_item : `string` | `tactic_argument_type`(`ident`) tactic_level : (at level `num`) - tactic_argument_type : ident | simple_intropattern | reference - : | hyp | hyp_list | ne_hyp_list - : | constr | uconstr | constr_list | ne_constr_list - : | integer | integer_list | ne_integer_list - : | int_or_var | int_or_var_list | ne_int_or_var_list - : | tactic | tactic0 | tactic1 | tactic2 | tactic3 - : | tactic4 | tactic5 + tactic_argument_type : `ident` | `simple_intropattern` | `reference` + : `hyp` | `hyp_list` | `ne_hyp_list` + : `constr` | `uconstr` | `constr_list` | `ne_constr_list` + : `integer` | `integer_list` | `ne_integer_list` + : `int_or_var` | `int_or_var_list` | `ne_int_or_var_list` + : `tactic` | `tactic0` | `tactic1` | `tactic2` | `tactic3` + : `tactic4` | `tactic5` .. cmd:: Tactic Notation {? (at level @level)} {+ @prod_item} := @tactic. |