aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx')
-rw-r--r--doc/sphinx/README.rst3
-rw-r--r--doc/sphinx/addendum/extraction.rst42
-rw-r--r--doc/sphinx/addendum/miscellaneous-extensions.rst1
-rw-r--r--doc/sphinx/addendum/program.rst34
-rw-r--r--doc/sphinx/addendum/ring.rst88
-rw-r--r--doc/sphinx/language/cic.rst18
-rw-r--r--doc/sphinx/language/coq-library.rst5
-rw-r--r--doc/sphinx/language/gallina-extensions.rst14
-rw-r--r--doc/sphinx/language/gallina-specification-language.rst6
-rw-r--r--doc/sphinx/practical-tools/utilities.rst4
-rw-r--r--doc/sphinx/proof-engine/detailed-tactic-examples.rst6
-rw-r--r--doc/sphinx/proof-engine/proof-handling.rst2
-rw-r--r--doc/sphinx/proof-engine/ssreflect-proof-language.rst1
-rw-r--r--doc/sphinx/proof-engine/tactics.rst19
-rw-r--r--doc/sphinx/user-extensions/syntax-extensions.rst18
15 files changed, 160 insertions, 101 deletions
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 32de15ee31..1643baf0e8 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -239,6 +239,9 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo
http://docutils.sourceforge.net/docs/ref/rst/directives.html#generic-admonition
for more details.
+ Optionally, any text immediately following the ``.. example::`` header is
+ used as the example's title.
+
Example::
.. example:: Adding a hint to a database
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index cb93d48a41..8c1eacf085 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -116,13 +116,13 @@ be optimized in order to be efficient (for instance, when using
induction principles we do not want to compute all the recursive calls
but only the needed ones). So the extraction mechanism provides an
automatic optimization routine that will be called each time the user
-want to generate |OCaml| programs. The optimizations can be split in two
+wants to generate an |OCaml| program. The optimizations can be split in two
groups: the type-preserving ones (essentially constant inlining and
reductions) and the non type-preserving ones (some function
abstractions of dummy types are removed when it is deemed safe in order
to have more elegant types). Therefore some constants may not appear in the
resulting monolithic |OCaml| program. In the case of modular extraction,
-even if some inlining is done, the inlined constant are nevertheless
+even if some inlining is done, the inlined constants are nevertheless
printed, to ensure session-independent programs.
Concerning Haskell, type-preserving optimizations are less useful
@@ -185,7 +185,7 @@ The type-preserving optimizations are controlled by the following |Coq| options:
**Inlining and printing of a constant declaration:**
-A user can explicitly ask for a constant to be extracted by two means:
+The user can explicitly ask for a constant to be extracted by two means:
* by mentioning it on the extraction command line
@@ -224,19 +224,18 @@ principles of extraction (logical parts and types).
When an actual extraction takes place, an error is normally raised if the
:cmd:`Extraction Implicit` declarations cannot be honored, that is
-if any of the implicited variables still occurs in the final code.
+if any of the implicit arguments still occurs in the final code.
This behavior can be relaxed via the following option:
.. opt:: Extraction SafeImplicits
Default is on. When this option is off, a warning is emitted
- instead of an error if some implicited variables still occur in the
+ instead of an error if some implicit arguments still occur in the
final code of an extraction. This way, the extracted code may be
obtained nonetheless and reviewed manually to locate the source of the issue
- (in the code, some comments mark the location of these remaining
- implicited variables).
+ (in the code, some comments mark the location of these remaining implicit arguments).
Note that this extracted code might not compile or run properly,
- depending of the use of these remaining implicited variables.
+ depending of the use of these remaining implicit arguments.
Realizing axioms
~~~~~~~~~~~~~~~~
@@ -296,7 +295,7 @@ The number of type variables is checked by the system. For example:
Realizing an axiom via :cmd:`Extract Constant` is only useful in the
case of an informative axiom (of sort ``Type`` or ``Set``). A logical axiom
-have no computational content and hence will not appears in extracted
+has no computational content and hence will not appear in extracted
terms. But a warning is nonetheless issued if extraction encounters a
logical axiom. This warning reminds user that inconsistent logical
axioms may lead to incorrect or non-terminating extracted terms.
@@ -312,7 +311,7 @@ Realizing inductive types
The system also provides a mechanism to specify ML terms for inductive
types and constructors. For instance, the user may want to use the ML
-native boolean type instead of |Coq| one. The syntax is the following:
+native boolean type instead of the |Coq| one. The syntax is the following:
.. cmd:: Extract Inductive @qualid => @string [ {+ @string } ]
@@ -332,10 +331,10 @@ native boolean type instead of |Coq| one. The syntax is the following:
branches in functional form, and then the inductive element to
destruct. For instance, the match branch ``| S n => foo`` gives the
functional form ``(fun n -> foo)``. Note that a constructor with no
- argument is considered to have one unit argument, in order to block
+ arguments is considered to have one unit argument, in order to block
early evaluation of the branch: ``| O => bar`` leads to the functional
form ``(fun () -> bar)``. For instance, when extracting ``nat``
- into |OCaml| ``int``, the code to provide has type:
+ into |OCaml| ``int``, the code to be provided has type:
``(unit->'a)->(int->'a)->int->'a``.
.. caution:: As for :cmd:`Extract Constant`, this command should be used with care:
@@ -371,7 +370,7 @@ Typical examples are the following:
When extracting to |OCaml|, if an inductive constructor or type has arity 2 and
the corresponding string is enclosed by parentheses, and the string meets
|OCaml|'s lexical criteria for an infix symbol, then the rest of the string is
- used as infix constructor or type.
+ used as an infix constructor or type.
.. coqtop:: in
@@ -389,7 +388,7 @@ Avoiding conflicts with existing filenames
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When using :cmd:`Extraction Library`, the names of the extracted files
-directly depends from the names of the |Coq| files. It may happen that
+directly depend on the names of the |Coq| files. It may happen that
these filenames are in conflict with already existing files,
either in the standard library of the target language or in other
code that is meant to be linked with the extracted code.
@@ -475,17 +474,18 @@ type-checker without any ``Obj.magic`` (see examples below).
Some examples
-------------
-We present here two examples of extractions, taken from the
-|Coq| Standard Library. We choose |OCaml| as target language,
-but all can be done in the other dialects with slight modifications.
+We present here two examples of extraction, taken from the
+|Coq| Standard Library. We choose |OCaml| as the target language,
+but everything, with slight modifications, can also be done in the
+other languages supported by extraction.
We then indicate where to find other examples and tests of extraction.
A detailed example: Euclidean division
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The file ``Euclid`` contains the proof of Euclidean division.
-The natural numbers used there are unary integers of type ``nat``,
-defined by two constructors ``O`` and ``S``.
+The natural numbers used here are unary, represented by the type``nat``,
+which is defined by two constructors ``O`` and ``S``.
This module contains a theorem ``eucl_dev``, whose type is::
forall b:nat, b > 0 -> forall a:nat, diveucl a b
@@ -579,7 +579,7 @@ extraction test:
* ``stalmarck`` : https://github.com/coq-contribs/stalmarck
Note that ``continuations`` and ``multiplier`` are a bit particular. They are
-examples of developments where ``Obj.magic`` are needed. This is
-probably due to an heavy use of impredicativity. After compilation, those
+examples of developments where ``Obj.magic`` is needed. This is
+probably due to a heavy use of impredicativity. After compilation, those
two examples run nonetheless, thanks to the correction of the
extraction :cite:`Let02`.
diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst
index b6c35d8fa7..0f2d35d044 100644
--- a/doc/sphinx/addendum/miscellaneous-extensions.rst
+++ b/doc/sphinx/addendum/miscellaneous-extensions.rst
@@ -32,6 +32,7 @@ When the proof ends two constants are defined:
ends with ``Qed``, and transparent if the proof ends with ``Defined``.
.. example::
+
.. coqtop:: all
Require Coq.derive.Derive.
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index b685e68e43..28fe68d78d 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -38,12 +38,12 @@ obligations which need to be resolved to create the final term.
Elaborating programs
---------------------
-The main difference from |Coq| is that an object in a type T : Set can
-be considered as an object of type { x : T | P} for any wellformed P :
-Prop. If we go from T to the subset of T verifying property P, we must
-prove that the object under consideration verifies it. Russell will
-generate an obligation for every such coercion. In the other
-direction, Russell will automatically insert a projection.
+The main difference from |Coq| is that an object in a type :g:`T : Set` can
+be considered as an object of type :g:`{x : T | P}` for any well-formed
+:g:`P : Prop`. If we go from :g:`T` to the subset of :g:`T` verifying property
+:g:`P`, we must prove that the object under consideration verifies it. Russell
+will generate an obligation for every such coercion. In the other direction,
+Russell will automatically insert a projection.
Another distinction is the treatment of pattern-matching. Apart from
the following differences, it is equivalent to the standard match
@@ -67,7 +67,7 @@ operation (see :ref:`extendedpatternmatching`).
(match x as y return (x = y -> _) with
| 0 => fun H : x = 0 -> t
| S n => fun H : x = S n -> u
- end) (eq_refl n).
+ end) (eq_refl x).
This permits to get the proper equalities in the context of proof
obligations inside clauses, without which reasoning is very limited.
@@ -75,7 +75,7 @@ operation (see :ref:`extendedpatternmatching`).
+ Generation of inequalities. If a pattern intersects with a previous
one, an inequality is added in the context of the second branch. See
for example the definition of div2 below, where the second branch is
- typed in a context where ∀ p, _ <> S (S p).
+ typed in a context where :g:`∀ p, _ <> S (S p)`.
+ Coercion. If the object being matched is coercible to an inductive
type, the corresponding coercion will be automatically inserted. This
also works with the previous mechanism.
@@ -88,7 +88,7 @@ coercions.
This controls the special treatment of pattern-matching generating equalities
and inequalities when using |Program| (it is on by default). All
- pattern-matchings and let-patterns are handled using the standard algorithm
+ pattern-matches and let-patterns are handled using the standard algorithm
of |Coq| (see :ref:`extendedpatternmatching`) when this option is
deactivated.
@@ -108,9 +108,9 @@ typechecker will fall back directly to |Coq|’s usual typing of dependent
pattern-matching if a return or in clause is specified. Likewise, the
if construct is not treated specially by |Program| so boolean tests in
the code are not automatically reflected in the obligations. One can
-use the dec combinator to get the correct hypotheses as in:
+use the :g:`dec` combinator to get the correct hypotheses as in:
-.. coqtop:: none
+.. coqtop:: in
Require Import Program Arith.
@@ -120,7 +120,7 @@ use the dec combinator to get the correct hypotheses as in:
if dec (leb n 0) then 0
else S (pred n).
-The let tupling construct :g:`let (x1, ..., xn) := t in b` does not
+The :g:`let` tupling construct :g:`let (x1, ..., xn) := t in b` does not
produce an equality, contrary to the let pattern construct :g:`let ’(x1,
..., xn) := t in b`. Also, :g:`term :>` explicitly asks the system to
coerce term to its support type. It can be useful in notations, for
@@ -200,7 +200,7 @@ The structural fixpoint operator behaves just like the one of |Coq| (see
:cmd:`Fixpoint`), except it may also generate obligations. It works
with mutually recursive definitions too.
-.. coqtop:: reset none
+.. coqtop:: reset in
Require Import Program Arith.
@@ -264,7 +264,7 @@ Program Lemma
Definition` and use it as the goal afterwards. Otherwise the proof
will be started with the elaborated version as a goal. The
:g:`Program` prefix can similarly be used as a prefix for
- :g:`Variable`, :g:`Hypothesis`, :g:`Axiom` etc...
+ :g:`Variable`, :g:`Hypothesis`, :g:`Axiom` etc.
.. _solving_obligations:
@@ -300,7 +300,7 @@ optional tactic is replaced by the default one if not specified.
Start the proof of the next unsolved obligation.
-.. cmd:: Solve Obligations {? of @ident} {? with @tactic}
+.. cmd:: Solve Obligations {? {? of @ident} with @tactic}
Tries to solve each obligation of ``ident`` using the given ``tactic`` or the default one.
@@ -322,13 +322,13 @@ optional tactic is replaced by the default one if not specified.
.. opt:: Transparent Obligations
- Control whether all obligations should be declared as transparent
+ Controls whether all obligations should be declared as transparent
(the default), or if the system should infer which obligations can be
declared opaque.
.. opt:: Hide Obligations
- Control whether obligations appearing in the
+ Controls whether obligations appearing in the
term should be hidden as implicit arguments of the special
constantProgram.Tactics.obligation.
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index 6a9b343ba8..d5c33dc1d4 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -13,7 +13,7 @@ The ring and field tactic families
:Author: Bruno Barras, Benjamin Grégoire, Assia Mahboubi, Laurent Théry [#f1]_
-This chapter presents the tactics dedicated to deal with ring and
+This chapter presents the tactics dedicated to dealing with ring and
field equations.
What does this tactic do?
@@ -36,7 +36,7 @@ is strictly less than the following monomial according to the lexicographic
order. It is an easy theorem to show that every polynomial is equivalent (modulo
the ring properties) to exactly one canonical sum. This canonical sum is called
the normal form of the polynomial. In fact, the actual representation shares
-monomials with same prefixes. So what does ring? It normalizes polynomials over
+monomials with same prefixes. So what does the ``ring`` tactic do? It normalizes polynomials over
any ring or semi-ring structure. The basic use of ``ring`` is to simplify ring
expressions, so that the user does not have to deal manually with the theorems
of associativity and commutativity.
@@ -59,9 +59,8 @@ The variables map
It is frequent to have an expression built with :math:`+` and :math:`\times`,
but rarely on variables only. Let us associate a number to each subterm of a
-ring expression in the Gallina language. For example in the ring |nat|, consider
-the expression:
-
+ring expression in the Gallina language. For example, consider this expression
+in the semiring ``nat``:
::
@@ -104,7 +103,7 @@ Concrete usage in Coq
.. tacn:: ring
The ``ring`` tactic solves equations upon polynomial expressions of a ring
-(or semi-ring) structure. It proceeds by normalizing both hand sides
+(or semi-ring) structure. It proceeds by normalizing both sides
of the equation (w.r.t. associativity, commutativity and
distributivity, constant propagation, rewriting of monomials) and
comparing syntactically the results.
@@ -112,9 +111,9 @@ comparing syntactically the results.
.. tacn:: ring_simplify
``ring_simplify`` applies the normalization procedure described above to
-the terms given. The tactic then replaces all occurrences of the terms
+the given terms. The tactic then replaces all occurrences of the terms
given in the conclusion of the goal by their normal forms. If no term
-is given, then the conclusion should be an equation and both hand
+is given, then the conclusion should be an equation and both
sides are normalized. The tactic can also be applied in a hypothesis.
The tactic must be loaded by ``Require Import Ring``. The ring structures
@@ -187,7 +186,7 @@ Error messages:
.. exn:: Cannot find a declared ring structure for equality @term.
- Same as above is the case of the ``ring`` tactic.
+ Same as above in the case of the ``ring`` tactic.
Adding a ring structure
@@ -198,8 +197,8 @@ carrier set, an equality, and ring operations: ``Ring_theory.ring_theory``
and ``Ring_theory.semi_ring_theory``) satisfies the ring axioms. Semi-
rings (rings without + inverse) are also supported. The equality can
be either Leibniz equality, or any relation declared as a setoid (see
-:ref:`tactics-enabled-on-user-provided-relations`). The definition of ring and semi-rings (see module
-``Ring_theory``) is:
+:ref:`tactics-enabled-on-user-provided-relations`).
+The definitions of ring and semiring (see module ``Ring_theory``) are:
.. coqtop:: in
@@ -305,7 +304,7 @@ The syntax for adding a new ring is
.. cmd:: Add Ring @ident : @term {? ( @ring_mod {* , @ring_mod } )}
-The :n:`@ident` is not relevant. It is just used for error messages. The
+The :n:`@ident` is not relevant. It is used just for error messages. The
:n:`@term` is a proof that the ring signature satisfies the (semi-)ring
axioms. The optional list of modifiers is used to tailor the behavior
of the tactic. The following list describes their syntax and effects:
@@ -386,7 +385,7 @@ sign :n:`@term`
div :n:`@term`
allows ``ring`` and ``ring_simplify`` to use monomials with
- coefficient other than 1 in the rewriting. The term :n:`@term` is a proof
+ coefficients other than 1 in the rewriting. The term :n:`@term` is a proof
that a given division function satisfies the specification of an
euclidean division function (:n:`@term` has to be a proof of
``Ring_theory.div_theory``). For example, this function is called when
@@ -414,13 +413,13 @@ Error messages:
How does it work?
----------------------
-The code of ring is a good example of tactic written using *reflection*.
-What is reflection? Basically, it is writing |Coq| tactics in |Coq|, rather
-than in |OCaml|. From the philosophical point of view, it is
-using the ability of the Calculus of Constructions to speak and reason
-about itself. For the ring tactic we used Coq as a programming
-language and also as a proof environment to build a tactic and to
-prove it correctness.
+The code of ``ring`` is a good example of a tactic written using *reflection*.
+What is reflection? Basically, using it means that a part of a tactic is written
+in Gallina, Coq's language of terms, rather than |Ltac| or |OCaml|. From the
+philosophical point of view, reflection is using the ability of the Calculus of
+Constructions to speak and reason about itself. For the ``ring`` tactic we used
+Coq as a programming language and also as a proof environment to build a tactic
+and to prove its correctness.
The interested reader is strongly advised to have a look at the
file ``Ring_polynom.v``. Here a type for polynomials is defined:
@@ -452,7 +451,7 @@ Polynomials in normal form are defined as:
where ``Pinj n P`` denotes ``P`` in which :math:`V_i` is replaced by :math:`V_{i+n}` ,
and ``PX P n Q`` denotes :math:`P \otimes V_1^n \oplus Q'`, `Q'` being `Q` where :math:`V_i` is replaced by :math:`V_{i+1}`.
-Variables maps are represented by list of ring elements, and two
+Variable maps are represented by lists of ring elements, and two
interpretation functions, one that maps a variables map and a
polynomial to an element of the concrete ring, and the second one that
does the same for normal forms:
@@ -490,18 +489,18 @@ concrete expression `p’`, which is the concrete normal form of `p`. This is su
`p’` |la| |le|
========= ====== ====
-The user do not see the right part of the diagram. From outside, the
-tactic behaves like a |bdi| simplification extended with AC rewriting
-rules. Basically, the proof is only the application of the main
-correctness theorem to well-chosen arguments.
+The user does not see the right part of the diagram. From outside, the
+tactic behaves like a |bdi| simplification extended with rewriting rules
+for associativity and commutativity. Basically, the proof is only the
+application of the main correctness theorem to well-chosen arguments.
Dealing with fields
------------------------
.. tacn:: field
-The ``field`` tactic is an extension of the ``ring`` to deal with rational
-expression. Given a rational expression :math:`F = 0`. It first reduces the
+The ``field`` tactic is an extension of the ``ring`` tactic that deals with rational
+expressions. Given a rational expression :math:`F = 0`. It first reduces the
expression `F` to a common denominator :math:`N/D = 0` where `N` and `D`
are two ring expressions. For example, if we take :math:`F = (1 − 1/x) x − x + 1`, this
gives :math:`N = (x − 1) x − x^2 + x` and :math:`D = x`. It then calls ring to solve
@@ -523,7 +522,7 @@ structures can be declared to the system with the ``Add Field`` command
(in ``plugins/setoid_ring``). It is exported by module ``Rbase``, so
that requiring ``Rbase`` or ``Reals`` is enough to use the field tactics on
real numbers. Rational numbers in canonical form are also declared as
-a field in module ``Qcanon``.
+a field in the module ``Qcanon``.
.. example::
@@ -559,8 +558,8 @@ a field in module ``Qcanon``.
performs the simplification in the conclusion of the
goal, :math:`F_1 = F_2` becomes :math:`N_1 / D_1 = N_2 / D_2`. A normalization step
(the same as the one for rings) is then applied to :math:`N_1`, :math:`D_1`,
- :math:`N_2` and :math:`D_2`. This way, polynomials remain in factorized form during the
- fraction simplifications. This yields smaller expressions when
+ :math:`N_2` and :math:`D_2`. This way, polynomials remain in factorized form during
+ fraction simplification. This yields smaller expressions when
reducing to the same denominator since common factors can be canceled.
.. tacv:: field_simplify [{* @term }]
@@ -657,7 +656,7 @@ The syntax for adding a new field is
.. cmd:: Add Field @ident : @term {? ( @field_mod {* , @field_mod } )}
-The :n:`@ident` is not relevant. It is just used for error
+The :n:`@ident` is not relevant. It is used just for error
messages. :n:`@term` is a proof that the field signature satisfies the
(semi-)field axioms. The optional list of modifiers is used to tailor
the behavior of the tactic.
@@ -704,9 +703,8 @@ it using reflection (see :cite:`Bou97`). Later, it
was rewritten by Patrick Loiseleur: the new tactic does not any
more require ``ACDSimpl`` to compile and it makes use of |bdi|-reduction not
only to replace the rewriting steps, but also to achieve the
-interleaving of computation and reasoning (see :ref:`discussion_reflection`). He also wrote a
-few |ML| code for the ``Add Ring`` command, that allow to register new rings
-dynamically.
+interleaving of computation and reasoning (see :ref:`discussion_reflection`). He also wrote
+some |ML| code for the ``Add Ring`` command that allows registering new rings dynamically.
Proofs terms generated by ring are quite small, they are linear in the
number of :math:`\oplus` and :math:`\otimes` operations in the normalized terms. Type-checking
@@ -733,15 +731,15 @@ Then it is rewritten to ``34 − x + 2 * x + 12``, very far from the expected re
Here rewriting is not sufficient: you have to do some kind of reduction
(some kind of computation) to achieve the normalization.
-The tactic ``ring`` is not only faster than a classical one: using
-reflection, we get for free integration of computation and reasoning
-that would be very complex to implement in the classic fashion.
+The tactic ``ring`` is not only faster than the old one: by using
+reflection, we get for free the integration of computation and reasoning
+that would be very difficult to implement without it.
Is it the ultimate way to write tactics? The answer is: yes and no.
-The ``ring`` tactic uses intensively the conversion rule of |Cic|, that is
-replaces proof by computation the most as it is possible. It can be
-useful in all situations where a classical tactic generates huge proof
-terms. Symbolic Processing and Tautologies are in that case. But there
+The ``ring`` tactic intensively uses the conversion rules of the Calculus of
+Inductive Constructions, i.e. it replaces proofs by computations as much as possible.
+It can be useful in all situations where a classical tactic generates huge proof
+terms, like symbolic processing and tautologies. But there
are also tactics like ``auto`` or ``linear`` that do many complex computations,
using side-effects and backtracking, and generate a small proof term.
Clearly, it would be significantly less efficient to replace them by
@@ -750,12 +748,12 @@ tactics using reflection.
Another idea suggested by Benjamin Werner: reflection could be used to
couple an external tool (a rewriting program or a model checker)
with |Coq|. We define (in |Coq|) a type of terms, a type of *traces*, and
-prove a correction theorem that states that *replaying traces* is safe
-w.r.t some interpretation. Then we let the external tool do every
+prove a correctness theorem that states that *replaying traces* is safe
+with respect to some interpretation. Then we let the external tool do every
computation (using side-effects, backtracking, exception, or others
features that are not available in pure lambda calculus) to produce
-the trace: now we can check in |Coq| that the trace has the expected
-semantic by applying the correction lemma.
+the trace. Now we can check in |Coq| that the trace has the expected
+semantics by applying the correctness theorem.
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 98e81ebc65..6e0c1e1b61 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -723,6 +723,7 @@ each :math:`T` in :math:`(t:T)∈Γ_I` can be written as: :math:`∀Γ_P,∀Γ_{
the sort of the inductive type t (not to be confused with :math:`\Sort` which is the set of sorts).
.. example::
+
The declaration for parameterized lists is:
.. math::
@@ -741,6 +742,7 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is
| cons : A -> list A -> list A.
.. example::
+
The declaration for a mutual inductive definition of tree and forest
is:
@@ -763,6 +765,7 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is
| consf : tree -> forest -> forest.
.. example::
+
The declaration for a mutual inductive definition of even and odd is:
.. math::
@@ -811,6 +814,7 @@ contains an inductive declaration.
E[Γ] ⊢ c : C
.. example::
+
Provided that our environment :math:`E` contains inductive definitions we showed before,
these two inference rules above enable us to conclude that:
@@ -919,6 +923,7 @@ condition* for a constant :math:`X` in the following cases:
.. example::
+
For instance, if one considers the following variant of a tree type
branching over the natural numbers:
@@ -985,6 +990,7 @@ 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)`.
@@ -1102,6 +1108,7 @@ sorts at each instance of a pattern-matching (see Section :ref:`Destructors`). A
an example, let us consider the following definition:
.. example::
+
.. coqtop:: in
Inductive option (A:Type) : Type :=
@@ -1118,6 +1125,7 @@ if :g:`option` is applied to a type in :math:`\Prop`, then, the result is not se
if set in :math:`\Prop`.
.. example::
+
.. coqtop:: all
Check (fun A:Set => option A).
@@ -1126,6 +1134,7 @@ if set in :math:`\Prop`.
Here is another example.
.. example::
+
.. coqtop:: in
Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B.
@@ -1136,6 +1145,7 @@ none in :math:`\Type`, and in :math:`\Type` otherwise. In all cases, the three k
eliminations schemes are allowed.
.. example::
+
.. coqtop:: all
Check (fun A:Set => prod A).
@@ -1324,6 +1334,7 @@ the extraction mechanism. Assume :math:`A` and :math:`B` are two propositions, a
logical disjunction :math:`A ∨ B` is defined inductively by:
.. example::
+
.. coqtop:: in
Inductive or (A B:Prop) : Prop :=
@@ -1334,6 +1345,7 @@ The following definition which computes a boolean value by case over
the proof of :g:`or A B` is not accepted:
.. example::
+
.. coqtop:: all
Fail Definition choice (A B: Prop) (x:or A B) :=
@@ -1357,6 +1369,7 @@ property which are provably different, contradicting the proof-
irrelevance property which is sometimes a useful axiom:
.. example::
+
.. coqtop:: all
Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y.
@@ -1390,6 +1403,7 @@ be used for rewriting not only in logical propositions but also in any
type.
.. example::
+
.. coqtop:: all
Print eq_rec.
@@ -1421,6 +1435,7 @@ We write :math:`\{c\}^P` for :math:`\{c:C\}^P` with :math:`C` the type of :math:
.. example::
+
The following term in concrete syntax::
match t as l return P' with
@@ -1485,6 +1500,7 @@ definition :math:`\ind{r}{Γ_I}{Γ_C}` with :math:`Γ_C = [c_1 :C_1 ;…;c_n :C_
.. example::
+
Below is a typing rule for the term shown in the previous example:
.. inference:: list example
@@ -1634,6 +1650,7 @@ The following definitions are correct, we enter them using the :cmd:`Fixpoint`
command and show the internal representation.
.. example::
+
.. coqtop:: all
Fixpoint plus (n m:nat) {struct n} : nat :=
@@ -1810,6 +1827,7 @@ option ``-impredicative-set``. For example, using the ordinary `coqtop`
command, the following is rejected,
.. example::
+
.. coqtop:: all
Fail Definition id: Set := forall X:Set,X->X.
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index 52c56d2bd2..9de30e2190 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -848,6 +848,7 @@ Notation Interpretation Precedence Associativity
.. example::
+
.. coqtop:: all reset
Require Import ZArith.
@@ -887,6 +888,7 @@ Notation Interpretation
=============== ===================
.. example::
+
.. coqtop:: all reset
Require Import Reals.
@@ -906,6 +908,7 @@ tactics (see Chapter :ref:`tactics`), there are also:
Proves that two real integer constants are different.
.. example::
+
.. coqtop:: all reset
Require Import DiscrR.
@@ -919,6 +922,7 @@ tactics (see Chapter :ref:`tactics`), there are also:
Allows unfolding the ``Rabs`` constant and splits corresponding conjunctions.
.. example::
+
.. coqtop:: all reset
Require Import Reals.
@@ -933,6 +937,7 @@ tactics (see Chapter :ref:`tactics`), there are also:
corresponding to the condition on each operand of the product.
.. example::
+
.. coqtop:: all reset
Require Import Reals.
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 394b928ada..7dd0a6e383 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -70,7 +70,9 @@ generates a variant type definition with just one constructor:
To build an object of type :n:`@ident`, one should provide the constructor
:n:`@ident₀` with the appropriate number of terms filling the fields of the record.
-.. example:: Let us define the rational :math:`1/2`:
+.. example::
+
+ Let us define the rational :math:`1/2`:
.. coqtop:: in
@@ -1849,15 +1851,15 @@ are named as expected.
.. example:: (continued)
-.. coqtop:: all
+ .. coqtop:: all
- Arguments p [s t] _ [u] _: rename.
+ Arguments p [s t] _ [u] _: rename.
- Check (p r1 (u:=c)).
+ Check (p r1 (u:=c)).
- Check (p (s:=a) (t:=b) r1 (u:=c) r2).
+ Check (p (s:=a) (t:=b) r1 (u:=c) r2).
- Fail Arguments p [s t] _ [w] _ : assert.
+ Fail Arguments p [s t] _ [w] _ : assert.
.. _displaying-implicit-args:
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 8250b4b3d6..da5cd00d72 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -758,6 +758,7 @@ Simple inductive types
the case of annotated inductive types — cf. next section).
.. example::
+
The set of natural numbers is defined as:
.. coqtop:: all
@@ -976,6 +977,7 @@ Mutually defined inductive types
reason, the parameters must be strictly the same for each inductive types.
.. example::
+
The typical example of a mutual inductive data type is the one for trees and
forests. We assume given two types :g:`A` and :g:`B` as variables. It can
be declared the following way.
@@ -1048,6 +1050,7 @@ of the type.
For co-inductive types, the only elimination principle is case analysis.
.. example::
+
An example of a co-inductive type is the type of infinite sequences of
natural numbers, usually called streams.
@@ -1067,6 +1070,7 @@ Definition of co-inductive predicates and blocks of mutually
co-inductive definitions are also allowed.
.. example::
+
An example of a co-inductive predicate is the extensional equality on
streams:
@@ -1129,6 +1133,7 @@ constructions.
.. example::
+
One can define the addition function as :
.. coqtop:: all
@@ -1201,6 +1206,7 @@ constructions.
inductive types.
.. example::
+
The size of trees and forests can be defined the following way:
.. coqtop:: all
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index e15bcb8e2c..59bc2d22aa 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -218,6 +218,7 @@ file timing data:
On ``Mac OS``, this works best if you’ve installed ``gnu-time``.
.. example::
+
For example, the output of ``make TIMED=1`` may look like
this:
@@ -295,6 +296,7 @@ file timing data:
files which take effectively no time to compile.
.. example::
+
For example, the output table from
``make print-pretty-timed-diff`` may look like this:
@@ -318,6 +320,7 @@ line timing data:
line-by-line timing information.
.. example::
+
For example, running ``make all TIMING=1`` may result in a file like this:
::
@@ -345,6 +348,7 @@ line timing data:
This target requires python to build the table.
.. example::
+
For example, running ``print-pretty-single-time-diff`` might give a table like this:
::
diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
index 78719c1ef1..225df8d54c 100644
--- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst
+++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
@@ -341,8 +341,7 @@ involves conditional rewritings and shows how to deal with them using
the optional tactic of the ``Hint Rewrite`` command.
-.. example::
- Ackermann function
+.. example:: Ackermann function
.. coqtop:: in reset
@@ -370,8 +369,7 @@ the optional tactic of the ``Hint Rewrite`` command.
autorewrite with base0 using try reflexivity.
-.. example::
- MacCarthy function
+.. example:: MacCarthy function
.. coqtop:: in reset
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 44376080c3..a9d0c16376 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -375,6 +375,7 @@ or focus the next one.
The following example script illustrates all these features:
.. example::
+
.. coqtop:: all
Goal (((True /\ True) /\ True) /\ True) /\ True.
@@ -511,6 +512,7 @@ Requesting information
:token:`ident`
.. example::
+
.. coqtop:: all
Show Match nat.
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 6fb73a030f..8a2fc3996a 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -4632,6 +4632,7 @@ bookkeeping steps.
.. example::
+
The following example use the ``~~`` prenex notation for boolean negation:
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index e6bc84365c..fdb04bf9a0 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -207,6 +207,7 @@ Applying theorems
useful to advanced users.
.. example::
+
.. coqtop:: reset all
Inductive Option : Set :=
@@ -366,6 +367,7 @@ Applying theorems
.. warn:: When @term contains more than one non dependent product the tactic lapply only takes into account the first product.
.. example::
+
Assume we have a transitive relation ``R`` on ``nat``:
.. coqtop:: reset in
@@ -837,6 +839,7 @@ quantified variables or hypotheses until the goal is not any more a
quantification or an implication.
.. example::
+
.. coqtop:: all
Goal forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C.
@@ -958,6 +961,7 @@ quantification or an implication.
.. exn:: Cannot move @ident after @ident : it depends on @ident.
.. example::
+
.. coqtop:: all
Goal forall x :nat, x = 0 -> forall z y:nat, y=y-> 0=x.
@@ -1082,6 +1086,7 @@ The name of the hypothesis in the proof-term, however, is left unchanged.
obtain atomic ones.
.. example::
+
.. coqtop:: all
Goal forall A B C:Prop, A /\ B /\ C \/ B /\ C \/ C /\ A -> C.
@@ -1252,6 +1257,7 @@ Controlling the proof flow
respect to some term.
.. example::
+
.. coqtop:: reset none
Goal forall x y:nat, 0 <= x + y + y.
@@ -1567,6 +1573,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
performs induction using this subterm.
.. example::
+
.. coqtop:: reset all
Lemma induction_test : forall n:nat, n = n -> n <= n.
@@ -1636,6 +1643,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
those are generalized as well in the statement to prove.
.. example::
+
.. coqtop:: reset all
Lemma comm x y : x + y = y + x.
@@ -1744,6 +1752,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
still get enough information in the proofs.
.. example::
+
.. coqtop:: reset all
Lemma le_minus : forall n:nat, n < 1 -> n = 0.
@@ -1809,6 +1818,7 @@ and an explanation of the underlying technique.
Note that this tactic is only available after a ``Require Import FunInd``.
.. example::
+
.. coqtop:: reset all
Require Import FunInd.
@@ -2856,6 +2866,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
+ A constant can be marked to be never unfolded by ``cbn`` or ``simpl``:
.. example::
+
.. coqtop:: all
Arguments minus n m : simpl never.
@@ -2868,6 +2879,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
``/`` symbol in the argument list of the :cmd:`Arguments` vernacular command.
.. example::
+
.. coqtop:: all
Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x).
@@ -2880,6 +2892,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
always unfolded.
.. example::
+
.. coqtop:: all
Definition volatile := fun x : nat => x.
@@ -2890,6 +2903,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
such arguments.
.. example::
+
.. coqtop:: all
Arguments minus !n !m.
@@ -3180,6 +3194,7 @@ where :tacn:`auto` uses simple :tacn:`apply`). As a consequence, :tacn:`eauto`
can solve such a goal:
.. example::
+
.. coqtop:: all
Hint Resolve ex_intro.
@@ -3748,6 +3763,7 @@ The following goal can be proved by :tacn:`tauto` whereas :tacn:`auto` would
fail:
.. example::
+
.. coqtop:: reset all
Goal forall (x:nat) (P:nat -> Prop), x = 0 \/ P x -> x <> 0 -> P x.
@@ -3904,6 +3920,7 @@ equality must contain all the quantified variables in order for congruence to
match against it.
.. example::
+
.. coqtop:: reset all
Theorem T (A:Type) (f:A -> A) (g: A -> A -> A) a b: a=(f a) -> (g b (f a))=(f (f a)) -> (g a b)=(f (g b a)) -> (g a b)=a.
@@ -4315,6 +4332,7 @@ declare new field structures. All declared field structures can be
printed with the Print Fields command.
.. example::
+
.. coqtop:: reset all
Require Import Reals.
@@ -4426,6 +4444,7 @@ Simple tactic macros
A simple example has more value than a long explanation:
.. example::
+
.. coqtop:: reset all
Ltac Solve := simpl; intros; auto.
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 6e98da1c04..37394386e6 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -650,7 +650,7 @@ example of recursive notation with closed binders:
A recursive pattern for binders can be used in position of a recursive
pattern for terms. Here is an example:
-.. coqtop:: in
+.. coqtop:: in
Notation "'FUNAPP' x .. y , f" :=
(fun x => .. (fun y => (.. (f x) ..) y ) ..)
@@ -1137,7 +1137,7 @@ The ``function_scope`` interpretation scope
.. index:: function_scope
-The scope ``function_scope`` also has a special status.
+The scope ``function_scope`` also has a special status.
It is temporarily activated each time the argument of a global reference is
recognized to be a ``Funclass`` istance, i.e., of type :g:`forall x:A, B` or
:g:`A -> B`.
@@ -1152,11 +1152,11 @@ Scopes` or :cmd:`Print Scope`.
``type_scope``
This scope includes infix * for product types and infix + for sum types. It
- is delimited by key ``type``, and bound to the coercion class
+ is delimited by key ``type``, and bound to the coercion class
``Sortclass``, as described above.
``function_scope``
- This scope is delimited by key ``function``, and bound to the coercion class
+ This scope is delimited by key ``function``, and bound to the coercion class
``Funclass``, as described above.
``nat_scope``
@@ -1455,7 +1455,9 @@ tactic language. Tactic notations obey the following syntax:
.. [#and_or_levels] which are the levels effectively chosen in the current
implementation of Coq
-.. [#no_associativity] Coq accepts notations declared as ``no associative`` but the parser on
- which Coq is built, namely Camlp4, currently does not implement the
- ``no associativity`` and replaces it by a ``left associativity``; hence it is
- the same for Coq: ``no associativity`` is in fact ``left associativity``.
+.. [#no_associativity] Coq accepts notations declared as ``no
+ associativity`` but the parser on which Coq is built, namely
+ Camlp5, currently does not implement ``no associativity`` and
+ replaces it with ``left associativity``; hence it is the same for
+ Coq: ``no associativity`` is in fact ``left associativity``, for
+ the purposes of parsing
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 05:06:03 +0000