diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/addendum/canonical-structures.rst | 18 | ||||
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 30 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 13 | ||||
| -rw-r--r-- | doc/sphinx/language/cic.rst | 12 | ||||
| -rw-r--r-- | doc/sphinx/language/coq-library.rst | 26 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 12 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/detailed-tactic-examples.rst | 643 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 126 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 126 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 10 |
12 files changed, 528 insertions, 499 deletions
diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst index 6843e9eaa1..3af3115a59 100644 --- a/doc/sphinx/addendum/canonical-structures.rst +++ b/doc/sphinx/addendum/canonical-structures.rst @@ -6,14 +6,14 @@ Canonical Structures :Authors: Assia Mahboubi and Enrico Tassi -This chapter explains the basics of Canonical Structure and how they can be used +This chapter explains the basics of canonical structures and how they can be used to overload notations and build a hierarchy of algebraic structures. The examples are taken from :cite:`CSwcu`. We invite the interested reader to refer to this paper for all the details that are omitted here for brevity. The interested reader shall also find in :cite:`CSlessadhoc` a detailed description -of another, complementary, use of Canonical Structures: advanced proof search. +of another, complementary, use of canonical structures: advanced proof search. This latter papers also presents many techniques one can employ to tune the -inference of Canonical Structures. +inference of canonical structures. Notation overloading @@ -38,21 +38,21 @@ of the terms that are compared. End theory. End EQ. -We use Coq modules as name spaces. This allows us to follow the same +We use Coq modules as namespaces. This allows us to follow the same pattern and naming convention for the rest of the chapter. The base -name space contains the definitions of the algebraic structure. To +namespace contains the definitions of the algebraic structure. To keep the example small, the algebraic structure ``EQ.type`` we are defining is very simplistic, and characterizes terms on which a binary relation is defined, without requiring such relation to validate any property. The inner theory module contains the overloaded notation ``==`` -and will eventually contain lemmas holding on all the instances of the +and will eventually contain lemmas holding all the instances of the algebraic structure (in this case there are no lemmas). Note that in practice the user may want to declare ``EQ.obj`` as a coercion, but we will not do that here. The following line tests that, when we assume a type ``e`` that is in -theEQ class, then we can relates two of its objects with ``==``. +theEQ class, we can relate two of its objects with ``==``. .. coqtop:: all @@ -312,7 +312,7 @@ The following script registers an ``LEQ`` class for ``nat`` and for the type constructor ``*``. It also tests that they work as expected. Unfortunately, these declarations are very verbose. In the following -subsection we show how to make these declaration more compact. +subsection we show how to make them more compact. .. coqtop:: all @@ -385,7 +385,7 @@ with message "T is not an EQ.type"”. The other utilities are used to ask |Coq| to solve a specific unification problem, that will in turn require the inference of some canonical structures. -They are explained in mode details in :cite:`CSwcu`. +They are explained in more details in :cite:`CSwcu`. We now have all we need to create a compact “packager” to declare instances of the ``LEQ`` class. diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 09faa06765..f134022eb6 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -31,7 +31,7 @@ A class with `n` parameters is any defined name with a type :g:`forall (x₁:A₁)..(xₙ:Aₙ),s` where ``s`` is a sort. Thus a class with parameters is considered as a single class and not as a family of classes. An object of a class ``C`` is any term of type :g:`C t₁ .. tₙ`. -In addition to these user-classes, we have two abstract classes: +In addition to these user-defined classes, we have two built-in classes: * ``Sortclass``, the class of sorts; its objects are the terms whose type is a @@ -50,11 +50,11 @@ Formally, the syntax of a classes is defined as: Coercions --------- -A name ``f`` can be declared as a coercion between a source user-class +A name ``f`` can be declared as a coercion between a source user-defined class ``C`` with `n` parameters and a target class ``D`` if one of these conditions holds: - * ``D`` is a user-class, then the type of ``f`` must have the form + * ``D`` is a user-defined class, then the type of ``f`` must have the form :g:`forall (x₁:A₁)..(xₙ:Aₙ)(y:C x₁..xₙ), D u₁..uₘ` where `m` is the number of parameters of ``D``. * ``D`` is ``Funclass``, then the type of ``f`` must have the form @@ -65,8 +65,8 @@ conditions holds: We then write :g:`f : C >-> D`. The restriction on the type of coercions is called *the uniform inheritance condition*. -.. note:: The abstract class ``Sortclass`` can be used as a source class, but - the abstract class ``Funclass`` cannot. +.. note:: The built-in class ``Sortclass`` can be used as a source class, but + the built-in class ``Funclass`` cannot. To coerce an object :g:`t:C t₁..tₙ` of ``C`` towards ``D``, we have to apply the coercion ``f`` to it; the obtained term :g:`f t₁..tₙ t` is @@ -95,7 +95,7 @@ We can now declare ``f`` as coercion from ``C'`` to ``D``, since we can The identity coercions have a special status: to coerce an object :g:`t:C' t₁..tₖ` -of ``C'`` towards ``C``, we does not have to insert explicitly ``Id_C'_C`` +of ``C'`` towards ``C``, we do not have to insert explicitly ``Id_C'_C`` since :g:`Id_C'_C t₁..tₖ t` is convertible with ``t``. However we "rewrite" the type of ``t`` to become an object of ``C``; in this case, it becomes :g:`C uₙ'..uₖ'` where each ``uᵢ'`` is the result of the @@ -121,7 +121,7 @@ by the coercions ``f₁..fₖ``. The application of a coercion path to a term consists of the successive application of its coercions. -Declaration of Coercions +Declaring Coercions ------------------------- .. cmd:: Coercion @qualid : @class >-> @class @@ -140,8 +140,8 @@ Declaration of Coercions .. warn:: Ambiguous path. - When the coercion :token:`qualid` is added to the inheritance graph, non - valid coercion paths are ignored; they are signaled by a warning + When the coercion :token:`qualid` is added to the inheritance graph, + invalid coercion paths are ignored; they are signaled by a warning displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`. .. cmdv:: Local Coercion @qualid : @class >-> @class @@ -215,7 +215,7 @@ declaration, this constructor is declared as a coercion. .. cmdv:: Local Identity Coercion @ident : @ident >-> @ident - Idem but locally to the current section. + Same as ``Identity Coercion`` but locally to the current section. .. cmdv:: SubClass @ident := @type :name: SubClass @@ -319,7 +319,7 @@ Coercions and Modules Since |Coq| version 8.3, the coercions present in a module are activated only when the module is explicitly imported. Formerly, the coercions - were activated as soon as the module was required, whatever it was + were activated as soon as the module was required, whether it was imported or not. This option makes it possible to recover the behavior of the versions of @@ -387,8 +387,8 @@ We give now an example using identity coercions. In the case of functional arguments, we use the monotonic rule of -sub-typing. Approximatively, to coerce :g:`t:forall x:A,B` towards -:g:`forall x:A',B'`, one have to coerce ``A'`` towards ``A`` and ``B`` +sub-typing. To coerce :g:`t : forall x : A, B` towards +:g:`forall x : A', B'`, we have to coerce ``A'`` towards ``A`` and ``B`` towards ``B'``. An example is given below: .. coqtop:: all @@ -424,8 +424,8 @@ replaced by ``x:A'`` where ``A'`` is the result of the application to ``Sortclass`` if it exists. This case occurs in the abstraction :g:`fun x:A => t`, universal quantification :g:`forall x:A,B`, global variables and parameters of (co-)inductive definitions and -functions. In :g:`forall x:A,B`, such a coercion path may be applied -to ``B`` also if necessary. +functions. In :g:`forall x:A,B`, such a coercion path may also be applied +to ``B`` if necessary. .. coqtop:: all diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 0e9c23b9bb..2407a9051a 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -96,15 +96,14 @@ and checked to be :math:`-1`. .. tacn:: lra :name: lra -This tactic is searching for *linear* refutations using Fourier -elimination [#]_. As a result, this tactic explores a subset of the *Cone* -defined as + This tactic is searching for *linear* refutations using Fourier + elimination [#]_. As a result, this tactic explores a subset of the *Cone* + defined as - :math:`\mathit{LinCone}(S) =\left\{ \left. \sum_{p \in S} \alpha_p \times p~\right|~\alpha_p \mbox{ are positive constants} \right\}` + :math:`\mathit{LinCone}(S) =\left\{ \left. \sum_{p \in S} \alpha_p \times p~\right|~\alpha_p \mbox{ are positive constants} \right\}` -The deductive power of `lra` is the combined deductive power of -`ring_simplify` and `fourier`. There is also an overlap with the field -tactic *e.g.*, :math:`x = 10 * x / 10` is solved by `lra`. + The deductive power of :tacn:`lra` overlaps with the one of :tacn:`field` + tactic *e.g.*, :math:`x = 10 * x / 10` is solved by :tacn:`lra`. `lia`: a tactic for linear integer arithmetic diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index b01a4ef0f9..98e81ebc65 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1175,7 +1175,7 @@ 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, so such that :g:`(length (nil A)) = O` and :g:`(length +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 recognized implicitly and taken into account in the conversion rule. @@ -1364,7 +1364,7 @@ irrelevance property which is sometimes a useful axiom: 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 inductive definition like the second-order existential quantifier -:g:`exProp` defined above, because it give access to the two projections on +:g:`exProp` defined above, because it gives access to the two projections on this type. @@ -1613,7 +1613,7 @@ 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 type an inductive definition in a declaration +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: @@ -1625,7 +1625,7 @@ Given a variable :math:`y` of type an inductive definition in a declaration 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 - obtained from :math:`B_i` by substituting parameters variables) the variables + 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. @@ -1801,7 +1801,7 @@ definitions can be found in :cite:`Gimenez95b,Gim98,GimCas05`. .. _The-Calculus-of-Inductive-Construction-with-impredicative-Set: -The Calculus of Inductive Construction with impredicative Set +The Calculus of Inductive Constructions with impredicative Set ----------------------------------------------------------------- |Coq| can be used as a type-checker for the Calculus of Inductive @@ -1834,7 +1834,7 @@ inductive definitions* like the example of second-order existential quantifier (:g:`exSet`). There should be restrictions on the eliminations which can be -performed on such definitions. The eliminations rules in the +performed on such definitions. The elimination rules in the impredicative system for sort :math:`\Set` become: diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index afb49413dd..52c56d2bd2 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -705,21 +705,29 @@ fixpoint equation can be proved. Accessing the Type level ~~~~~~~~~~~~~~~~~~~~~~~~ -The basic library includes the definitions of the counterparts of some data-types and logical -quantifiers at the ``Type``: level: negation, pair, and properties -of ``identity``. This is the module ``Logic_Type.v``. +The standard library includes ``Type`` level definitions of counterparts of some +logic concepts and basic lemmas about them. + +The module ``Datatypes`` defines ``identity``, which is the ``Type`` level counterpart +of equality: + +.. index:: + single: identity (term) + +.. coqtop:: in + + Inductive identity (A:Type) (a:A) : A -> Type := + identity_refl : identity a a. + +Some properties of ``identity`` are proved in the module ``Logic_Type``, which also +provides the definition of ``Type`` level negation: .. index:: single: notT (term) - single: prodT (term) - single: pairT (term) .. coqtop:: in Definition notT (A:Type) := A -> False. - Inductive prodT (A B:Type) : Type := pairT (_:A) (_:B). - -At the end, it defines data-types at the ``Type`` level. Tactics ~~~~~~~ @@ -889,7 +897,7 @@ Notation Interpretation Some tactics for real numbers +++++++++++++++++++++++++++++ -In addition to the powerful ``ring``, ``field`` and ``fourier`` +In addition to the powerful ``ring``, ``field`` and ``lra`` tactics (see Chapter :ref:`tactics`), there are also: .. tacn:: discrR diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 509ac92f81..394b928ada 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -781,7 +781,8 @@ Section :ref:`gallina-definitions`). .. cmd:: Section @ident - This command is used to open a section named `ident`. + This command is used to open a section named :token:`ident`. + Section names do not need to be unique. .. cmd:: End @ident @@ -1079,7 +1080,7 @@ The definition of ``N`` using the module type expression ``SIG`` with Module N : SIG' := M. -If we just want to be sure that the our implementation satisfies a +If we just want to be sure that our implementation satisfies a given module type without restricting the interface, we can use a transparent constraint diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index bdaa2aa1a2..e15bcb8e2c 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -546,12 +546,12 @@ The printing for one token can be removed with Initially, the pretty-printing table contains the following mapping: -==== === ==== ===== === ==== ==== === -`->` → `<-` ← `*` × -`<=` ≤ `>=` ≥ `=>` ⇒ -`<>` ≠ `<->` ↔ `|-` ⊢ -`\/` ∨ `/\\` ∧ `~` ¬ -==== === ==== ===== === ==== ==== === +===== === ==== ===== === ==== ==== === +`->` → `<-` ← `*` × +`<=` ≤ `>=` ≥ `=>` ⇒ +`<>` ≠ `<->` ↔ `|-` ⊢ +`\\/` ∨ `/\\` ∧ `~` ¬ +===== === ==== ===== === ==== ==== === Any of these can be overwritten or suppressed using the printing commands. diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst index 84810ddba5..78719c1ef1 100644 --- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst +++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst @@ -25,7 +25,7 @@ argument an hypothesis to generalize. It uses the JMeq datatype defined in Coq.Logic.JMeq, hence we need to require it before. For example, revisiting the first example of the inversion documentation: -.. coqtop:: in +.. coqtop:: in reset Require Import Coq.Logic.JMeq. @@ -63,6 +63,10 @@ to use an heterogeneous equality to relate the new hypothesis to the old one (which just disappeared here). However, the tactic works just as well in this case, e.g.: +.. coqtop:: none + + Abort. + .. coqtop:: in Variable Q : forall (n m : nat), Le n m -> Prop. @@ -80,7 +84,7 @@ to recover the needed equalities. Also, some subgoals should be directly solved because of inconsistent contexts arising from the constraints on indexes. The nice thing is that we can make a tactic based on discriminate, injection and variants of substitution to -automatically do such simplifications (which may involve the K axiom). +automatically do such simplifications (which may involve the axiom K). This is what the ``simplify_dep_elim`` tactic from ``Coq.Program.Equality`` does. For example, we might simplify the previous goals considerably: @@ -101,9 +105,9 @@ are ``dependent induction`` and ``dependent destruction`` that do induction or simply case analysis on the generalized hypothesis. For example we can redo what we’ve done manually with dependent destruction: -.. coqtop:: in +.. coqtop:: none - Require Import Coq.Program.Equality. + Abort. .. coqtop:: in @@ -122,9 +126,9 @@ destructed hypothesis actually appeared in the goal, the tactic would still be able to invert it, contrary to dependent inversion. Consider the following example on vectors: -.. coqtop:: in +.. coqtop:: none - Require Import Coq.Program.Equality. + Abort. .. coqtop:: in @@ -167,7 +171,7 @@ predicates on a real example. We will develop an example application to the theory of simply-typed lambda-calculus formalized in a dependently-typed style: -.. coqtop:: in +.. coqtop:: in reset Inductive type : Type := | base : type @@ -226,11 +230,15 @@ name. A term is either an application of: Once we have this datatype we want to do proofs on it, like weakening: -.. coqtop:: in undo +.. coqtop:: in Lemma weakening : forall G D tau, term (G ; D) tau -> forall tau', term (G , tau' ; D) tau. +.. coqtop:: none + + Abort. + The problem here is that we can’t just use induction on the typing derivation because it will forget about the ``G ; D`` constraint appearing in the instance. A solution would be to rewrite the goal as: @@ -241,6 +249,10 @@ in the instance. A solution would be to rewrite the goal as: forall G D, (G ; D) = G' -> forall tau', term (G, tau' ; D) tau. +.. coqtop:: none + + Abort. + With this proper separation of the index from the instance and the right induction loading (putting ``G`` and ``D`` after the inducted-on hypothesis), the proof will go through, but it is a very tedious @@ -252,6 +264,7 @@ back automatically. Indeed we can simply write: .. coqtop:: in Require Import Coq.Program.Tactics. + Require Import Coq.Program.Equality. .. coqtop:: in @@ -308,17 +321,14 @@ it can be used directly. apply weak, IHterm. -If there is an easy first-order solution to these equations as in this -subgoal, the ``specialize_eqs`` tactic can be used instead of giving -explicit proof terms: - -.. coqtop:: all +Now concluding this subgoal is easy. - specialize_eqs IHterm. +.. coqtop:: in -This concludes our example. + constructor; apply IHterm; reflexivity. -See also: The :tacn:`induction`, :tacn:`case`, and :tacn:`inversion` tactics. +.. seealso:: + The :tacn:`induction`, :tacn:`case`, and :tacn:`inversion` tactics. autorewrite @@ -331,79 +341,83 @@ involves conditional rewritings and shows how to deal with them using the optional tactic of the ``Hint Rewrite`` command. -Example 1: Ackermann function +.. example:: + Ackermann function -.. coqtop:: in + .. coqtop:: in reset - Reset Initial. + Require Import Arith. -.. coqtop:: in + .. coqtop:: in - Require Import Arith. + Variable Ack : nat -> nat -> nat. -.. coqtop:: in + .. coqtop:: in - Variable Ack : nat -> nat -> nat. + Axiom Ack0 : forall m:nat, Ack 0 m = S m. + Axiom Ack1 : forall n:nat, Ack (S n) 0 = Ack n 1. + Axiom Ack2 : forall n m:nat, Ack (S n) (S m) = Ack n (Ack (S n) m). -.. coqtop:: in + .. coqtop:: in - Axiom Ack0 : forall m:nat, Ack 0 m = S m. - Axiom Ack1 : forall n:nat, Ack (S n) 0 = Ack n 1. - Axiom Ack2 : forall n m:nat, Ack (S n) (S m) = Ack n (Ack (S n) m). + Hint Rewrite Ack0 Ack1 Ack2 : base0. -.. coqtop:: in + .. coqtop:: all - Hint Rewrite Ack0 Ack1 Ack2 : base0. + Lemma ResAck0 : Ack 3 2 = 29. -.. coqtop:: all + .. coqtop:: all - Lemma ResAck0 : Ack 3 2 = 29. + autorewrite with base0 using try reflexivity. -.. coqtop:: all +.. example:: + MacCarthy function - autorewrite with base0 using try reflexivity. + .. coqtop:: in reset -Example 2: Mac Carthy function + Require Import Omega. -.. coqtop:: in + .. coqtop:: in - Require Import Omega. + Variable g : nat -> nat -> nat. -.. coqtop:: in + .. coqtop:: in - Variable g : nat -> nat -> nat. + Axiom g0 : forall m:nat, g 0 m = m. + Axiom g1 : forall n m:nat, (n > 0) -> (m > 100) -> g n m = g (pred n) (m - 10). + Axiom g2 : forall n m:nat, (n > 0) -> (m <= 100) -> g n m = g (S n) (m + 11). -.. coqtop:: in + .. coqtop:: in - Axiom g0 : forall m:nat, g 0 m = m. - Axiom g1 : forall n m:nat, (n > 0) -> (m > 100) -> g n m = g (pred n) (m - 10). - Axiom g2 : forall n m:nat, (n > 0) -> (m <= 100) -> g n m = g (S n) (m + 11). + Hint Rewrite g0 g1 g2 using omega : base1. + .. coqtop:: in -.. coqtop:: in + Lemma Resg0 : g 1 110 = 100. - Hint Rewrite g0 g1 g2 using omega : base1. + .. coqtop:: out -.. coqtop:: in + Show. - Lemma Resg0 : g 1 110 = 100. + .. coqtop:: all -.. coqtop:: out + autorewrite with base1 using reflexivity || simpl. - Show. + .. coqtop:: none -.. coqtop:: all + Qed. - autorewrite with base1 using reflexivity || simpl. + .. coqtop:: all -.. coqtop:: all + Lemma Resg1 : g 1 95 = 91. - Lemma Resg1 : g 1 95 = 91. + .. coqtop:: all -.. coqtop:: all + autorewrite with base1 using reflexivity || simpl. - autorewrite with base1 using reflexivity || simpl. + .. coqtop:: none + Qed. .. _quote: @@ -419,7 +433,7 @@ the form ``(f t)``. ``L`` must have a constructor of type: ``A -> L``. Here is an example: -.. coqtop:: in +.. coqtop:: in reset Require Import Quote. @@ -461,16 +475,11 @@ corresponding left-hand side and call yourself recursively on sub- terms. If there is no match, we are at a leaf: return the corresponding constructor (here ``f_const``) applied to the term. - -Error messages: - - -#. quote: not a simple fixpoint +.. exn:: quote: not a simple fixpoint Happens when ``quote`` is not able to perform inversion properly. - Introducing variables map ~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -553,7 +562,13 @@ example, this is the case for the :tacn:`ring` tactic. Then one must provide to is ``[O S]`` then closed natural numbers will be considered as constants and other terms as variables. -Example: +.. coqtop:: in reset + + Require Import Quote. + +.. coqtop:: in + + Parameters A B C : Prop. .. coqtop:: in @@ -594,8 +609,9 @@ Example: quote interp_f [ B C iff ]. -Warning: Since function inversion is undecidable in general case, -don’t expect miracles from it! +.. warning:: + Since functional inversion is undecidable in the general case, + don’t expect miracles from it! .. tacv:: quote @ident in @term using @tactic @@ -607,25 +623,28 @@ don’t expect miracles from it! Same as above, but will use the additional ``ident`` list to chose which subterms are constants (see above). -See also: comments of source file ``plugins/quote/quote.ml`` +.. seealso:: + Comments from the source file ``plugins/quote/quote.ml`` -See also: the :tacn:`ring` tactic. +.. seealso:: + The :tacn:`ring` tactic. -Using the tactical language +Using the tactic language --------------------------- About the cardinality of the set of natural numbers ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -A first example which shows how to use pattern matching over the -proof contexts is the proof that natural numbers have more than two -elements. The proof of such a lemma can be done as follows: +The first example which shows how to use pattern matching over the +proof context is a proof of the fact that natural numbers have more +than two elements. This can be done as follows: -.. coqtop:: in +.. coqtop:: in reset - Lemma card_nat : ~ (exists x : nat, exists y : nat, forall z:nat, x = z \/ y = z). + Lemma card_nat : + ~ exists x : nat, exists y : nat, forall z:nat, x = z \/ y = z. Proof. .. coqtop:: in @@ -637,8 +656,8 @@ elements. The proof of such a lemma can be done as follows: elim (Hy 0); elim (Hy 1); elim (Hy 2); intros; match goal with - | [_:(?a = ?b),_:(?a = ?c) |- _ ] => - cut (b = c); [ discriminate | transitivity a; auto ] + | _ : ?a = ?b, _ : ?a = ?c |- _ => + cut (b = c); [ discriminate | transitivity a; auto ] end. .. coqtop:: in @@ -651,16 +670,14 @@ solved by a match goal structure and, in particular, with only one pattern (use of non-linear matching). -Permutation on closed lists +Permutations of lists ~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Another more complex example is the problem of permutation on closed -lists. The aim is to show that a closed list is a permutation of -another one. - -First, we define the permutation predicate as shown here: +A more complex example is the problem of permutations of +lists. The aim is to show that a list is a permutation of +another list. -.. coqtop:: in +.. coqtop:: in reset Section Sort. @@ -670,205 +687,179 @@ First, we define the permutation predicate as shown here: .. coqtop:: in - Inductive permut : list A -> list A -> Prop := - | permut_refl : forall l, permut l l - | permut_cons : forall a l0 l1, permut l0 l1 -> permut (a :: l0) (a :: l1) - | permut_append : forall a l, permut (a :: l) (l ++ a :: nil) - | permut_trans : forall l0 l1 l2, permut l0 l1 -> permut l1 l2 -> permut l0 l2. + Inductive perm : list A -> list A -> Prop := + | perm_refl : forall l, perm l l + | perm_cons : forall a l0 l1, perm l0 l1 -> perm (a :: l0) (a :: l1) + | perm_append : forall a l, perm (a :: l) (l ++ a :: nil) + | perm_trans : forall l0 l1 l2, perm l0 l1 -> perm l1 l2 -> perm l0 l2. .. coqtop:: in End Sort. -A more complex example is the problem of permutation on closed lists. -The aim is to show that a closed list is a permutation of another one. First, we define the permutation predicate as shown above. - .. coqtop:: none Require Import List. -.. coqtop:: all - - Ltac Permut n := - match goal with - | |- (permut _ ?l ?l) => apply permut_refl - | |- (permut _ (?a :: ?l1) (?a :: ?l2)) => - let newn := eval compute in (length l1) in - (apply permut_cons; Permut newn) - | |- (permut ?A (?a :: ?l1) ?l2) => - match eval compute in n with - | 1 => fail - | _ => - let l1' := constr:(l1 ++ a :: nil) in - (apply (permut_trans A (a :: l1) l1' l2); - [ apply permut_append | compute; Permut (pred n) ]) - end - end. - - -.. coqtop:: all - - Ltac PermutProve := - match goal with - | |- (permut _ ?l1 ?l2) => - match eval compute in (length l1 = length l2) with - | (?n = ?n) => Permut n - end - end. - -Next, we can write naturally the tactic and the result can be seen -above. We can notice that we use two top level definitions -``PermutProve`` and ``Permut``. The function to be called is -``PermutProve`` which computes the lengths of the two lists and calls -``Permut`` with the length if the two lists have the same -length. ``Permut`` works as expected. If the two lists are equal, it -concludes. Otherwise, if the lists have identical first elements, it -applies ``Permut`` on the tail of the lists. Finally, if the lists -have different first elements, it puts the first element of one of the -lists (here the second one which appears in the permut predicate) at -the end if that is possible, i.e., if the new first element has been -at this place previously. To verify that all rotations have been done -for a list, we use the length of the list as an argument for Permut -and this length is decremented for each rotation down to, but not -including, 1 because for a list of length ``n``, we can make exactly -``n−1`` rotations to generate at most ``n`` distinct lists. Here, it -must be noticed that we use the natural numbers of Coq for the -rotation counter. In :ref:`ltac-syntax`, we can -see that it is possible to use usual natural numbers but they are only -used as arguments for primitive tactics and they cannot be handled, in -particular, we cannot make computations with them. So, a natural -choice is to use Coq data structures so that Coq makes the -computations (reductions) by eval compute in and we can get the terms -back by match. - -With ``PermutProve``, we can now prove lemmas as follows: - .. coqtop:: in - Lemma permut_ex1 : permut nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil). + Ltac perm_aux n := + match goal with + | |- (perm _ ?l ?l) => apply perm_refl + | |- (perm _ (?a :: ?l1) (?a :: ?l2)) => + let newn := eval compute in (length l1) in + (apply perm_cons; perm_aux newn) + | |- (perm ?A (?a :: ?l1) ?l2) => + match eval compute in n with + | 1 => fail + | _ => + let l1' := constr:(l1 ++ a :: nil) in + (apply (perm_trans A (a :: l1) l1' l2); + [ apply perm_append | compute; perm_aux (pred n) ]) + end + end. -.. coqtop:: in +Next we define an auxiliary tactic ``perm_aux`` which takes an argument +used to control the recursion depth. This tactic behaves as follows. If +the lists are identical (i.e. convertible), it concludes. Otherwise, if +the lists have identical heads, it proceeds to look at their tails. +Finally, if the lists have different heads, it rotates the first list by +putting its head at the end if the new head hasn't been the head previously. To check this, we keep track of the +number of performed rotations using the argument ``n``. We do this by +decrementing ``n`` each time we perform a rotation. It works because +for a list of length ``n`` we can make exactly ``n - 1`` rotations +to generate at most ``n`` distinct lists. Notice that we use the natural +numbers of Coq for the rotation counter. From :ref:`ltac-syntax` we know +that it is possible to use the usual natural numbers, but they are only +used as arguments for primitive tactics and they cannot be handled, so, +in particular, we cannot make computations with them. Thus the natural +choice is to use Coq data structures so that Coq makes the computations +(reductions) by ``eval compute in`` and we can get the terms back by match. + +.. coqtop:: in + + Ltac solve_perm := + match goal with + | |- (perm _ ?l1 ?l2) => + match eval compute in (length l1 = length l2) with + | (?n = ?n) => perm_aux n + end + end. - Proof. PermutProve. Qed. +The main tactic is ``solve_perm``. It computes the lengths of the two lists +and uses them as arguments to call ``perm_aux`` if the lengths are equal (if they +aren't, the lists cannot be permutations of each other). Using this tactic we +can now prove lemmas as follows: .. coqtop:: in - Lemma permut_ex2 : permut nat - (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil) - (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil). - - Proof. PermutProve. Qed. + Lemma solve_perm_ex1 : + perm nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil). + Proof. solve_perm. Qed. +.. coqtop:: in + Lemma solve_perm_ex2 : + perm nat + (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil) + (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil). + Proof. solve_perm. Qed. Deciding intuitionistic propositional logic ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. _decidingintuitionistic1: - -.. coqtop:: all - - Ltac Axioms := - match goal with - | |- True => trivial - | _:False |- _ => elimtype False; assumption - | _:?A |- ?A => auto - end. - -.. _decidingintuitionistic2: - -.. coqtop:: all - - Ltac DSimplif := - repeat - (intros; - match goal with - | id:(~ _) |- _ => red in id - | id:(_ /\ _) |- _ => - elim id; do 2 intro; clear id - | id:(_ \/ _) |- _ => - elim id; intro; clear id - | id:(?A /\ ?B -> ?C) |- _ => - cut (A -> B -> C); - [ intro | intros; apply id; split; assumption ] - | id:(?A \/ ?B -> ?C) |- _ => - cut (B -> C); - [ cut (A -> C); - [ intros; clear id - | intro; apply id; left; assumption ] - | intro; apply id; right; assumption ] - | id0:(?A -> ?B),id1:?A |- _ => - cut B; [ intro; clear id0 | apply id0; assumption ] - | |- (_ /\ _) => split - | |- (~ _) => red - end). - -.. coqtop:: all - - Ltac TautoProp := - DSimplif; - Axioms || - match goal with - | id:((?A -> ?B) -> ?C) |- _ => - cut (B -> C); - [ intro; cut (A -> B); - [ intro; cut C; - [ intro; clear id | apply id; assumption ] - | clear id ] - | intro; apply id; intro; assumption ]; TautoProp - | id:(~ ?A -> ?B) |- _ => - cut (False -> B); - [ intro; cut (A -> False); - [ intro; cut B; - [ intro; clear id | apply id; assumption ] - | clear id ] - | intro; apply id; red; intro; assumption ]; TautoProp - | |- (_ \/ _) => (left; TautoProp) || (right; TautoProp) - end. - -The pattern matching on goals allows a complete and so a powerful -backtracking when returning tactic values. An interesting application -is the problem of deciding intuitionistic propositional logic. -Considering the contraction-free sequent calculi LJT* of Roy Dyckhoff -:cite:`Dyc92`, it is quite natural to code such a tactic -using the tactic language as shown on figures: :ref:`Deciding -intuitionistic propositions (1) <decidingintuitionistic1>` and -:ref:`Deciding intuitionistic propositions (2) -<decidingintuitionistic2>`. The tactic ``Axioms`` tries to conclude -using usual axioms. The tactic ``DSimplif`` applies all the reversible -rules of Dyckhoff’s system. Finally, the tactic ``TautoProp`` (the -main tactic to be called) simplifies with ``DSimplif``, tries to -conclude with ``Axioms`` and tries several paths using the -backtracking rules (one of the four Dyckhoff’s rules for the left -implication to get rid of the contraction and the right or). - -For example, with ``TautoProp``, we can prove tautologies like those: - -.. coqtop:: in - - Lemma tauto_ex1 : forall A B:Prop, A /\ B -> A \/ B. +Pattern matching on goals allows a powerful backtracking when returning tactic +values. An interesting application is the problem of deciding intuitionistic +propositional logic. Considering the contraction-free sequent calculi LJT* of +Roy Dyckhoff :cite:`Dyc92`, it is quite natural to code such a tactic using the +tactic language as shown below. -.. coqtop:: in - - Proof. TautoProp. Qed. - -.. coqtop:: in +.. coqtop:: in reset - Lemma tauto_ex2 : - forall A B:Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B. + Ltac basic := + match goal with + | |- True => trivial + | _ : False |- _ => contradiction + | _ : ?A |- ?A => assumption + end. .. coqtop:: in - Proof. TautoProp. Qed. + Ltac simplify := + repeat (intros; + match goal with + | H : ~ _ |- _ => red in H + | H : _ /\ _ |- _ => + elim H; do 2 intro; clear H + | H : _ \/ _ |- _ => + elim H; intro; clear H + | H : ?A /\ ?B -> ?C |- _ => + cut (A -> B -> C); + [ intro | intros; apply H; split; assumption ] + | H: ?A \/ ?B -> ?C |- _ => + cut (B -> C); + [ cut (A -> C); + [ intros; clear H + | intro; apply H; left; assumption ] + | intro; apply H; right; assumption ] + | H0 : ?A -> ?B, H1 : ?A |- _ => + cut B; [ intro; clear H0 | apply H0; assumption ] + | |- _ /\ _ => split + | |- ~ _ => red + end). + +.. coqtop:: in + + Ltac my_tauto := + simplify; basic || + match goal with + | H : (?A -> ?B) -> ?C |- _ => + cut (B -> C); + [ intro; cut (A -> B); + [ intro; cut C; + [ intro; clear H | apply H; assumption ] + | clear H ] + | intro; apply H; intro; assumption ]; my_tauto + | H : ~ ?A -> ?B |- _ => + cut (False -> B); + [ intro; cut (A -> False); + [ intro; cut B; + [ intro; clear H | apply H; assumption ] + | clear H ] + | intro; apply H; red; intro; assumption ]; my_tauto + | |- _ \/ _ => (left; my_tauto) || (right; my_tauto) + end. + +The tactic ``basic`` tries to reason using simple rules involving truth, falsity +and available assumptions. The tactic ``simplify`` applies all the reversible +rules of Dyckhoff’s system. Finally, the tactic ``my_tauto`` (the main +tactic to be called) simplifies with ``simplify``, tries to conclude with +``basic`` and tries several paths using the backtracking rules (one of the +four Dyckhoff’s rules for the left implication to get rid of the contraction +and the right ``or``). + +Having defined ``my_tauto``, we can prove tautologies like these: + +.. coqtop:: in + + Lemma my_tauto_ex1 : + forall A B : Prop, A /\ B -> A \/ B. + Proof. my_tauto. Qed. + +.. coqtop:: in + + Lemma my_tauto_ex2 : + forall A B : Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B. + Proof. my_tauto. Qed. Deciding type isomorphisms ~~~~~~~~~~~~~~~~~~~~~~~~~~ -A more tricky problem is to decide equalities between types and modulo +A more tricky problem is to decide equalities between types modulo isomorphisms. Here, we choose to use the isomorphisms of the simply typed λ-calculus with Cartesian product and unit type (see, for example, :cite:`RC95`). The axioms of this λ-calculus are given below. @@ -915,112 +906,104 @@ example, :cite:`RC95`). The axioms of this λ-calculus are given below. End Iso_axioms. +.. coqtop:: in + Ltac simplify_type ty := + match ty with + | ?A * ?B * ?C => + rewrite <- (Ass A B C); try simplify_type_eq + | ?A * ?B -> ?C => + rewrite (Cur A B C); try simplify_type_eq + | ?A -> ?B * ?C => + rewrite (Dis A B C); try simplify_type_eq + | ?A * unit => + rewrite (P_unit A); try simplify_type_eq + | unit * ?B => + rewrite (Com unit B); try simplify_type_eq + | ?A -> unit => + rewrite (AR_unit A); try simplify_type_eq + | unit -> ?B => + rewrite (AL_unit B); try simplify_type_eq + | ?A * ?B => + (simplify_type A; try simplify_type_eq) || + (simplify_type B; try simplify_type_eq) + | ?A -> ?B => + (simplify_type A; try simplify_type_eq) || + (simplify_type B; try simplify_type_eq) + end + with simplify_type_eq := + match goal with + | |- ?A = ?B => try simplify_type A; try simplify_type B + end. -.. _typeisomorphism1: - -.. coqtop:: all - - Ltac DSimplif trm := - match trm with - | (?A * ?B * ?C) => - rewrite <- (Ass A B C); try MainSimplif - | (?A * ?B -> ?C) => - rewrite (Cur A B C); try MainSimplif - | (?A -> ?B * ?C) => - rewrite (Dis A B C); try MainSimplif - | (?A * unit) => - rewrite (P_unit A); try MainSimplif - | (unit * ?B) => - rewrite (Com unit B); try MainSimplif - | (?A -> unit) => - rewrite (AR_unit A); try MainSimplif - | (unit -> ?B) => - rewrite (AL_unit B); try MainSimplif - | (?A * ?B) => - (DSimplif A; try MainSimplif) || (DSimplif B; try MainSimplif) - | (?A -> ?B) => - (DSimplif A; try MainSimplif) || (DSimplif B; try MainSimplif) - end - with MainSimplif := - match goal with - | |- (?A = ?B) => try DSimplif A; try DSimplif B - end. - -.. coqtop:: all +.. coqtop:: in - Ltac Length trm := - match trm with - | (_ * ?B) => let succ := Length B in constr:(S succ) - | _ => constr:(1) - end. + Ltac len trm := + match trm with + | _ * ?B => let succ := len B in constr:(S succ) + | _ => constr:(1) + end. -.. coqtop:: all +.. coqtop:: in Ltac assoc := repeat rewrite <- Ass. +.. coqtop:: in -.. _typeisomorphism2: - -.. coqtop:: all - - Ltac DoCompare n := - match goal with - | [ |- (?A = ?A) ] => reflexivity - | [ |- (?A * ?B = ?A * ?C) ] => - apply Cons; let newn := Length B in - DoCompare newn - | [ |- (?A * ?B = ?C) ] => - match eval compute in n with - | 1 => fail - | _ => - pattern (A * B) at 1; rewrite Com; assoc; DoCompare (pred n) - end - end. - -.. coqtop:: all + Ltac solve_type_eq n := + match goal with + | |- ?A = ?A => reflexivity + | |- ?A * ?B = ?A * ?C => + apply Cons; let newn := len B in solve_type_eq newn + | |- ?A * ?B = ?C => + match eval compute in n with + | 1 => fail + | _ => + pattern (A * B) at 1; rewrite Com; assoc; solve_type_eq (pred n) + end + end. - Ltac CompareStruct := - match goal with - | [ |- (?A = ?B) ] => - let l1 := Length A - with l2 := Length B in - match eval compute in (l1 = l2) with - | (?n = ?n) => DoCompare n - end - end. +.. coqtop:: in -.. coqtop:: all + Ltac compare_structure := + match goal with + | |- ?A = ?B => + let l1 := len A + with l2 := len B in + match eval compute in (l1 = l2) with + | ?n = ?n => solve_type_eq n + end + end. - Ltac IsoProve := MainSimplif; CompareStruct. +.. coqtop:: in + Ltac solve_iso := simplify_type_eq; compare_structure. -The tactic to judge equalities modulo this axiomatization can be -written as shown on these figures: :ref:`type isomorphism tactic (1) -<typeisomorphism1>` and :ref:`type isomorphism tactic (2) -<typeisomorphism2>`. The algorithm is quite simple. Types are reduced -using axioms that can be oriented (this done by ``MainSimplif``). The -normal forms are sequences of Cartesian products without Cartesian -product in the left component. These normal forms are then compared -modulo permutation of the components (this is done by -``CompareStruct``). The main tactic to be called and realizing this -algorithm isIsoProve. +The tactic to judge equalities modulo this axiomatization is shown above. +The algorithm is quite simple. First types are simplified using axioms that +can be oriented (this is done by ``simplify_type`` and ``simplify_type_eq``). +The normal forms are sequences of Cartesian products without Cartesian product +in the left component. These normal forms are then compared modulo permutation +of the components by the tactic ``compare_structure``. If they have the same +lengths, the tactic ``solve_type_eq`` attempts to prove that the types are equal. +The main tactic that puts all these components together is called ``solve_iso``. -Here are examples of what can be solved by ``IsoProve``. +Here are examples of what can be solved by ``solve_iso``. .. coqtop:: in - Lemma isos_ex1 : - forall A B:Set, A * unit * B = B * (unit * A). + Lemma solve_iso_ex1 : + forall A B : Set, A * unit * B = B * (unit * A). Proof. - intros; IsoProve. + intros; solve_iso. Qed. .. coqtop:: in - Lemma isos_ex2 : - forall A B C:Set, - (A * unit -> B * (C * unit)) = (A * unit -> (C -> unit) * C) * (unit -> A -> B). + Lemma solve_iso_ex2 : + forall A B C : Set, + (A * unit -> B * (C * unit)) = + (A * unit -> (C -> unit) * C) * (unit -> A -> B). Proof. - intros; IsoProve. + intros; solve_iso. Qed. diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 278a4ff012..dc355fa013 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -10,8 +10,8 @@ This chapter gives a compact documentation of |Ltac|, the tactic language available in |Coq|. We start by giving the syntax, and next, we present the informal semantics. If you want to know more regarding this language and especially about its foundations, you can refer to :cite:`Del00`. Chapter -:ref:`detailedexamplesoftactics` is devoted to giving examples of use of this -language on small but also with non-trivial problems. +:ref:`detailedexamplesoftactics` is devoted to giving small but nontrivial +use examples of this language. .. _ltac-syntax: @@ -33,7 +33,7 @@ notation :g:`_` can also be used to denote metavariable whose instance is irrelevant. In the notation :g:`?id`, the identifier allows us to keep instantiations and to make constraints whereas :g:`_` shows that we are not interested in what will be matched. On the right hand side of pattern-matching -clauses, the named metavariable are used without the question mark prefix. There +clauses, the named metavariables are used without the question mark prefix. There is also a special notation for second-order pattern-matching problems: in an applicative pattern of the form :g:`@?id id1 … idn`, the variable id matches any complex expression with (possible) dependencies in the variables :g:`id1 … idn` @@ -160,13 +160,13 @@ Semantics --------- Tactic expressions can only be applied in the context of a proof. The -evaluation yields either a term, an integer or a tactic. Intermediary +evaluation yields either a term, an integer or a tactic. Intermediate results can be terms or integers but the final result must be a tactic which is then applied to the focused goals. There is a special case for ``match goal`` expressions of which the clauses evaluate to tactics. Such expressions can only be used as end result of -a tactic expression (never as argument of a non recursive local +a tactic expression (never as argument of a non-recursive local definition or of an application). The rest of this section explains the semantics of every construction of @@ -197,8 +197,8 @@ following form: :name: [> ... | ... | ... ] (dispatch) The expressions :n:`@expr__i` are evaluated to :n:`v__i`, for - i=0,...,n and all have to be tactics. The :n:`v__i` is applied to the - i-th goal, for =1,...,n. It fails if the number of focused goals is not + i = 0, ..., n and all have to be tactics. The :n:`v__i` is applied to the + i-th goal, for i = 1, ..., n. It fails if the number of focused goals is not exactly n. .. note:: @@ -221,7 +221,7 @@ following form: .. tacv:: [> @expr .. ] In this variant, the tactic :n:`@expr` is applied independently to each of - the goals, rather than globally. In particular, if there are no goal, the + the goals, rather than globally. In particular, if there are no goals, the tactic is not run at all. A tactic which expects multiple goals, such as ``swap``, would act as if a single goal is focused. @@ -385,11 +385,12 @@ tactic to work (i.e. which does not fail) among a panel of tactics: :name: first The :n:`@expr__i` are evaluated to :n:`v__i` and :n:`v__i` must be - tactic values, for i=1,...,n. Supposing n>1, it applies, in each focused - goal independently, :n:`v__1`, if it works, it stops otherwise it + tactic values for i = 1, ..., n. Supposing n > 1, + :n:`first [@expr__1 | ... | @expr__n]` applies :n:`v__1` in each + focused goal independently and stops if it succeeds; otherwise it tries to apply :n:`v__2` and so on. It fails when there is no applicable tactic. In other words, - :n:`first [:@expr__1 | ... | @expr__n]` behaves, in each goal, as the the first + :n:`first [@expr__1 | ... | @expr__n]` behaves, in each goal, as the the first :n:`v__i` to have *at least* one success. .. exn:: No applicable tactic. @@ -397,7 +398,7 @@ tactic to work (i.e. which does not fail) among a panel of tactics: .. tacv:: first @expr This is an |Ltac| alias that gives a primitive access to the first - tactical as a |Ltac| definition without going through a parsing rule. It + tactical as an |Ltac| definition without going through a parsing rule. It expects to be given a list of tactics through a ``Tactic Notation``, allowing to write notations of the following form: @@ -454,7 +455,7 @@ single success *a posteriori*: :n:`@expr` is evaluated to ``v`` which must be a tactic value. The tactic value ``v`` is applied but only its first success is used. If ``v`` fails, - :n:`once @expr` fails like ``v``. If ``v`` has a least one success, + :n:`once @expr` fails like ``v``. If ``v`` has at least one success, :n:`once @expr` succeeds once, but cannot produce more successes. Checking the successes @@ -475,7 +476,7 @@ one* success: .. warning:: The experimental status of this tactic pertains to the fact if ``v`` - performs side effects, they may occur in a unpredictable way. Indeed, + performs side effects, they may occur in an unpredictable way. Indeed, normally ``v`` would only be executed up to the first success until backtracking is needed, however exactly_once needs to look ahead to see whether a second success exists, and may run further effects @@ -515,8 +516,9 @@ among a panel of tactics: :name: solve The :n:`@expr__i` are evaluated to :n:`v__i` and :n:`v__i` must be - tactic values, for i=1,...,n. Supposing n>1, it applies :n:`v__1` to - each goal independently, if it doesn’t solve the goal then it tries to + tactic values, for i = 1, ..., n. Supposing n > 1, + :n:`solve [@expr__1 | ... | @expr__n]` applies :n:`v__1` to + each goal independently and stops if it succeeds; otherwise it tries to apply :n:`v__2` and so on. It fails if there is no solving tactic. .. exn:: Cannot solve the goal. @@ -546,15 +548,13 @@ Failing This is the always-failing tactic: it does not solve any goal. It is useful for defining other tacticals since it can be caught by - :tacn:`try`, :tacn:`repeat`, :tacn:`match goal`, or the branching tacticals. The - :tacn:`fail` tactic will, however, succeed if all the goals have already been - solved. + :tacn:`try`, :tacn:`repeat`, :tacn:`match goal`, or the branching tacticals. .. tacv:: fail @num The number is the failure level. If no level is specified, it defaults to 0. The level is used by :tacn:`try`, :tacn:`repeat`, :tacn:`match goal` and the branching - tacticals. If 0, it makes :tacn:`match goal` considering the next clause + tacticals. If 0, it makes :tacn:`match goal` consider the next clause (backtracking). If non zero, the current :tacn:`match goal` block, :tacn:`try`, :tacn:`repeat`, or branching command is aborted and the level is decremented. In the case of :n:`+`, a non-zero level skips the first backtrack point, even if @@ -572,7 +572,9 @@ Failing .. tacv:: gfail :name: gfail - This variant fails even if there are no goals left. + This variant fails even when used after :n:`;` and there are no goals left. + Similarly, ``gfail`` fails even when used after ``all:`` and there are no + goals left. See the example for clarification. .. tacv:: gfail {* message_token} @@ -582,10 +584,41 @@ Failing there are no goals left. Be careful however if Coq terms have to be printed as part of the failure: term construction always forces the tactic into the goals, meaning that if there are no goals when it is - evaluated, a tactic call like :n:`let x:=H in fail 0 x` will succeed. + evaluated, a tactic call like :n:`let x := H in fail 0 x` will succeed. .. exn:: Tactic Failure message (level @num). + .. exn:: No such goal. + :name: No such goal. (fail) + + .. example:: + + .. coqtop:: all + + Goal True. + Proof. fail. Abort. + + Goal True. + Proof. trivial; fail. Qed. + + Goal True. + Proof. trivial. fail. Abort. + + Goal True. + Proof. trivial. all: fail. Qed. + + Goal True. + Proof. gfail. Abort. + + Goal True. + Proof. trivial; gfail. Abort. + + Goal True. + Proof. trivial. gfail. Abort. + + Goal True. + Proof. trivial. all: gfail. Abort. + Timeout ~~~~~~~ @@ -605,7 +638,7 @@ amount of time: which is very machine-dependent: a script that works on a quick machine may fail on a slow one. The converse is even possible if you combine a timeout with some other tacticals. This tactical is hence proposed only - for convenience during debug or other development phases, we strongly + for convenience during debugging or other development phases, we strongly advise you to not leave any timeout in final scripts. Note also that this tactical isn’t available on the native Windows port of Coq. @@ -617,9 +650,9 @@ A tactic execution can be timed: .. tacn:: time @string @expr :name: time - evaluates :n:`@expr` and displays the time the tactic expression ran, whether it - fails or successes. In case of several successes, the time for each successive - runs is displayed. Time is in seconds and is machine-dependent. The :n:`@string` + evaluates :n:`@expr` and displays the running time of the tactic expression, whether it + fails or succeeds. In case of several successes, the time for each successive + run is displayed. Time is in seconds and is machine-dependent. The :n:`@string` argument is optional. When provided, it is used to identify this particular occurrence of time. @@ -685,12 +718,12 @@ Local definitions can be done as follows: each :n:`@expr__i` is evaluated to :n:`v__i`, then, :n:`@expr` is evaluated by substituting :n:`v__i` to each occurrence of :n:`@ident__i`, for - i=1,...,n. There is no dependencies between the :n:`@expr__i` and the + i = 1, ..., n. There are no dependencies between the :n:`@expr__i` and the :n:`@ident__i`. - Local definitions can be recursive by using :n:`let rec` instead of :n:`let`. + Local definitions can be made recursive by using :n:`let rec` instead of :n:`let`. In this latter case, the definitions are evaluated lazily so that the rec - keyword can be used also in non recursive cases so as to avoid the eager + keyword can be used also in non-recursive cases so as to avoid the eager evaluation of local definitions. .. but rec changes the binding!! @@ -704,7 +737,7 @@ An application is an expression of the following form: The reference :n:`@qualid` must be bound to some defined tactic definition expecting at least as many arguments as the provided :n:`tacarg`. The - expressions :n:`@expr__i` are evaluated to :n:`v__i`, for i=1,...,n. + expressions :n:`@expr__i` are evaluated to :n:`v__i`, for i = 1, ..., n. .. what expressions ?? @@ -755,7 +788,7 @@ We can carry out pattern matching on terms with: evaluation of :n:`@expr__1` fails, or if the evaluation of :n:`@expr__1` succeeds but returns a tactic in execution position whose execution fails, then :n:`cpattern__2` is used and so on. The pattern - :n:`_` matches any term and shunts all remaining patterns if any. If all + :n:`_` matches any term and shadows all remaining patterns if any. If all clauses fail (in particular, there is no pattern :n:`_`) then a no-matching-clause error is raised. @@ -821,14 +854,14 @@ We can carry out pattern matching on terms with: Pattern matching on goals ~~~~~~~~~~~~~~~~~~~~~~~~~ -We can make pattern matching on goals using the following expression: +We can perform pattern matching on goals using the following expression: .. we should provide the full grammar here .. tacn:: match goal with {+| {+ hyp} |- @cpattern => @expr } | _ => @expr end :name: match goal - If each hypothesis pattern :n:`hyp`\ :sub:`1,i`, with i=1,...,m\ :sub:`1` is + If each hypothesis pattern :n:`hyp`\ :sub:`1,i`, with i = 1, ..., m\ :sub:`1` is matched (non-linear first-order unification) by an hypothesis of the goal and if :n:`cpattern_1` is matched by the conclusion of the goal, then :n:`@expr__1` is evaluated to :n:`v__1` by substituting the @@ -857,10 +890,10 @@ We can make pattern matching on goals using the following expression: It is important to know that each hypothesis of the goal can be matched by at most one hypothesis pattern. The order of matching is the - following: hypothesis patterns are examined from the right to the left + following: hypothesis patterns are examined from right to left (i.e. hyp\ :sub:`i,m`\ :sub:`i`` before hyp\ :sub:`i,1`). For each - hypothesis pattern, the goal hypothesis are matched in order (fresher - hypothesis first), but it possible to reverse this order (older first) + hypothesis pattern, the goal hypotheses are matched in order (newest + first), but it possible to reverse this order (oldest first) with the :n:`match reverse goal with` variant. .. tacv:: multimatch goal with {+| {+ hyp} |- @cpattern => @expr } | _ => @expr end @@ -896,6 +929,10 @@ produce subgoals but generates a term to be used in tactic expressions: value of :n:`@ident` by the value of :n:`@expr`. .. exn:: Not a context variable. + :undocumented: + + .. exn:: Unbound context identifier @ident. + :undocumented: Generating fresh hypothesis names ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1167,7 +1204,7 @@ Interactive debugger This option governs the step-by-step debugger that comes with the |Ltac| interpreter When the debugger is activated, it stops at every step of the evaluation of -the current |Ltac| expression and it prints information on what it is doing. +the current |Ltac| expression and prints information on what it is doing. The debugger stops, prompting for a command which can be one of the following: @@ -1185,6 +1222,9 @@ following: | r string: | advance up to the next call to “idtac string” | +-----------------+-----------------------------------------------+ +.. exn:: Debug mode not available in the IDE + :undocumented: + A non-interactive mode for the debugger is available via the option: .. opt:: Ltac Batch Debug @@ -1204,9 +1244,9 @@ which can sometimes be so slow as to impede interactive usage. The reasons for the performence degradation can be intricate, like a slowly performing |Ltac| match or a sub-tactic whose performance only degrades in certain situations. The profiler generates a call tree and -indicates the time spent in a tactic depending its calling context. Thus +indicates the time spent in a tactic depending on its calling context. Thus it allows to locate the part of a tactic definition that contains the -performance bug. +performance issue. .. opt:: Ltac Profiling @@ -1240,8 +1280,12 @@ performance bug. Goal forall x y z A B C D E F G H I J K L M N O P Q R S T U V W X Y Z, max x (max y z) = max (max x y) z /\ max x (max y z) = max (max x y) z - /\ (A /\ B /\ C /\ D /\ E /\ F /\ G /\ H /\ I /\ J /\ K /\ L /\ M /\ N /\ O /\ P /\ Q /\ R /\ S /\ T /\ U /\ V /\ W /\ X /\ Y /\ Z - -> Z /\ Y /\ X /\ W /\ V /\ U /\ T /\ S /\ R /\ Q /\ P /\ O /\ N /\ M /\ L /\ K /\ J /\ I /\ H /\ G /\ F /\ E /\ D /\ C /\ B /\ A). + /\ + (A /\ B /\ C /\ D /\ E /\ F /\ G /\ H /\ I /\ J /\ K /\ L /\ M /\ + N /\ O /\ P /\ Q /\ R /\ S /\ T /\ U /\ V /\ W /\ X /\ Y /\ Z + -> + Z /\ Y /\ X /\ W /\ V /\ U /\ T /\ S /\ R /\ Q /\ P /\ O /\ N /\ + M /\ L /\ K /\ J /\ I /\ H /\ G /\ F /\ E /\ D /\ C /\ B /\ A). Proof. .. coqtop:: all diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index eba0db3ff5..44376080c3 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -321,7 +321,7 @@ Navigation in the proof tree goal, much like :cmd:`Focus` does, however, the subproof can only be unfocused when it has been fully solved ( *i.e.* when there is no focused goal left). Unfocusing is then handled by ``}`` (again, without a - terminating period). See also example in next section. + terminating period). See also an example in the next section. Note that when a focused goal is proved a message is displayed together with a suggestion about the right bullet or ``}`` to unfocus it @@ -403,7 +403,7 @@ The following example script illustrates all these features: .. exn:: No such goal. Focus next goal with bullet @bullet. - You tried to apply a tactic but no goal where under focus. Using :n:`@bullet` is mandatory here. + You tried to apply a tactic but no goals were under focus. Using :n:`@bullet` is mandatory here. .. exn:: No such goal. Try unfocusing with %{. @@ -470,7 +470,7 @@ Requesting information constructed. These holes appear as a question mark indexed by an integer, and applied to the list of variables in the context, since it may depend on them. The types obtained by abstracting away the context - from the type of each hole-placer are also printed. + from the type of each placeholder are also printed. .. cmdv:: Show Conjectures :name: Show Conjectures diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 89668a2d7e..e6bc84365c 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -26,8 +26,8 @@ address a particular goal in the list by writing n:tactic which means “apply tactic tactic to goal number n”. We can show the list of subgoals by typing Show (see Section :ref:`requestinginformation`). -Since not every rule applies to a given statement, every tactic cannot -be used to reduce any goal. In other words, before applying a tactic +Since not every rule applies to a given statement, not every tactic can +be used to reduce a given goal. In other words, before applying a tactic to a given goal, the system checks that some *preconditions* are satisfied. If it is not the case, the tactic raises an error message. @@ -107,10 +107,10 @@ bindings_list`` where ``bindings_list`` may be of two different forms: .. _occurencessets: -Occurrences sets and occurrences clauses +Occurrence sets and occurrence clauses ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -An occurrences clause is a modifier to some tactics that obeys the +An occurrence clause is a modifier to some tactics that obeys the following syntax: .. _tactic_occurence_grammar: @@ -137,7 +137,7 @@ negates the condition so that the clause denotes all the occurrences except the ones explicitly mentioned after the minus sign. As an exception to the left-to-right order, the occurrences in -thereturn subexpression of a match are considered *before* the +the return subexpression of a match are considered *before* the occurrences in the matched term. In the second case, the ``*`` on the left of ``|-`` means that all occurrences @@ -151,7 +151,7 @@ no numbers are given, all occurrences of :n:`@term` in the goal are selected. Finally, the last notation is an abbreviation for ``* |- *``. Note also that ``|-`` is optional in the first case when no ``*`` is given. -Here are some tactics that understand occurrences clauses: :tacn:`set`, :tacn:`remember` +Here are some tactics that understand occurrence clauses: :tacn:`set`, :tacn:`remember` , :tacn:`induction`, :tacn:`destruct`. @@ -281,7 +281,7 @@ Applying theorems :g:`t`:sub:`n` in the goal. See :tacn:`pattern` to transform the goal so that it gets the form :g:`(fun x => Q) u`:sub:`1` :g:`...` :g:`u`:sub:`n`. - .. exn:: Unable to unify ... with ... . + .. exn:: Unable to unify @term with @term. The apply tactic failed to match the conclusion of :token:`term` and the current goal. You can help the apply tactic by transforming your goal with @@ -466,7 +466,7 @@ Applying theorems the tuple is (recursively) decomposed and the first component of the tuple of which a non-dependent premise matches the conclusion of the type of :n:`@ident`. Tuples are decomposed in a width-first left-to-right order (for - instance if the type of :g:`H1` is a :g:`A <-> B` statement, and the type of + instance if the type of :g:`H1` is :g:`A <-> B` and the type of :g:`H2` is :g:`A` then ``apply H1 in H2`` transforms the type of :g:`H2` into :g:`B`). The tactic ``apply`` relies on first-order pattern-matching with dependent types. @@ -846,7 +846,7 @@ quantification or an implication. :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 in are eventually erased too while it might fail in the second + 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). @@ -1040,7 +1040,7 @@ The name of the hypothesis in the proof-term, however, is left unchanged. .. tacv:: remember @term as @ident in @goal_occurrences This is a more general form of :n:`remember` that remembers the occurrences - of term specified by an occurrences set. + of term specified by an occurrence set. .. tacv:: eremember @term as @ident .. tacv:: eremember @term as @ident in @goal_occurrences @@ -1523,7 +1523,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) .. tacv:: case_eq @term - The tactic :n:`case_eq` is a variant of the :n:`case` tactic that allow to + The tactic :n:`case_eq` is a variant of the :n:`case` tactic that allows to perform case analysis on a term without completely forgetting its original form. This is done by generating equalities between the original form of the term and the outcomes of the case analysis. @@ -1806,7 +1806,7 @@ and an explanation of the underlying technique. following the definition of a function. It makes use of a principle generated by ``Function`` (see :ref:`advanced-recursive-functions`) or ``Functional Scheme`` (see :ref:`functional-scheme`). - Note that this tactic is only available after a + Note that this tactic is only available after a ``Require Import FunInd``. .. example:: .. coqtop:: reset all @@ -1825,7 +1825,7 @@ and an explanation of the underlying technique. arguments explicitly. .. note:: - Parentheses over :n:`@qualid {+ @term}` are mandatory. + Parentheses around :n:`@qualid {+ @term}` are not mandatory and can be skipped. .. note:: :n:`functional induction (f x1 x2 x3)` is actually a wrapper for @@ -2237,7 +2237,7 @@ See also: :ref:`advanced-recursive-functions` To prove the goal, we may need to reason by cases on H and to derive that m is necessarily of the form (S m 0 ) for certain m 0 and that - (Le n m 0 ). Deriving these conditions corresponds to prove that the + (Le n m 0 ). Deriving these conditions corresponds to proving that the only possible constructor of (Le (S n) m) isLeS and that we can invert the-> in the type of LeS. This inversion is possible because Le is the smallest set closed by the constructors LeO and LeS. @@ -2598,7 +2598,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. Adds :n:`@term` to the database used by :tacn:`stepl`. - The tactic is especially useful for parametric setoids which are not accepted + This tactic is especially useful for parametric setoids which are not accepted as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see :ref:`Generalizedrewriting`). @@ -2708,7 +2708,7 @@ the conversion in hypotheses :n:`{+ @ident}`. Normalization according to the flags is done by first evaluating the head of the expression into a *weak-head* normal form, i.e. until the - evaluation is bloked by a variable (or an opaque constant, or an + evaluation is blocked by a variable (or an opaque constant, or an axiom), as e.g. in :g:`x u1 ... un` , or :g:`match x with ... end`, or :g:`(fix f x {struct x} := ...) x`, or is a constructed form (a :math:`\lambda`-expression, a constructor, a cofixpoint, an inductive type, a @@ -2804,14 +2804,18 @@ the conversion in hypotheses :n:`{+ @ident}`. This tactic applies to a goal that has the form:: - forall (x:T1) ... (xk:Tk), t + forall (x:T1) ... (xk:Tk), T - with :g:`t` :math:`\beta`:math:`\iota`:math:`\zeta`-reducing to :g:`c t`:sub:`1` :g:`... t`:sub:`n` and :g:`c` a + with :g:`T` :math:`\beta`:math:`\iota`:math:`\zeta`-reducing to :g:`c t`:sub:`1` :g:`... t`:sub:`n` and :g:`c` a constant. If :g:`c` is transparent then it replaces :g:`c` with its definition (say :g:`t`) and then reduces :g:`(t t`:sub:`1` :g:`... t`:sub:`n` :g:`)` according to :math:`\beta`:math:`\iota`:math:`\zeta`-reduction rules. .. exn:: Not reducible. + :undocumented: + +.. exn:: No head constant to reduce. + :undocumented: .. tacn:: hnf :name: hnf @@ -2821,8 +2825,7 @@ the conversion in hypotheses :n:`{+ @ident}`. reduces the head of the goal until it becomes a product or an irreducible term. All inner :math:`\beta`:math:`\iota`-redexes are also reduced. - Example: The term :g:`forall n:nat, (plus (S n) (S n))` is not reduced by - :n:`hnf`. + Example: The term :g:`fun n : nat => S n + S n` is not reduced by :n:`hnf`. .. note:: The :math:`\delta` rule only applies to transparent constants (see :ref:`vernac-controlling-the-reduction-strategies` @@ -2862,7 +2865,7 @@ the conversion in hypotheses :n:`{+ @ident}`. + A constant can be marked to be unfolded only if applied to enough arguments. The number of arguments required can be specified using the - ``/`` symbol in the arguments list of the ``Arguments`` vernacular command. + ``/`` symbol in the argument list of the :cmd:`Arguments` vernacular command. .. example:: .. coqtop:: all @@ -3030,7 +3033,7 @@ the conversion in hypotheses :n:`{+ @ident}`. For instance, if the current goal :g:`T` is expressible as :math:`\varphi`:g:`(t)` where the notation captures all the instances of :g:`t` in :math:`\varphi`:g:`(t)`, then :n:`pattern t` transforms it into - :g:`(fun x:A =>` :math:`\varphi`:g:`(x)) t`. This command can be used, for + :g:`(fun x:A =>` :math:`\varphi`:g:`(x)) t`. This tactic can be used, for instance, when the tactic ``apply`` fails on matching. .. tacv:: pattern @term at {+ @num} @@ -3072,10 +3075,10 @@ Conversion tactics applied to hypotheses listed in this section. If :n:`@ident` is a local definition, then :n:`@ident` can be replaced by - (Type of :n:`@ident`) to address not the body but the type of the local + (type of :n:`@ident`) to address not the body but the type of the local definition. - Example: :n:`unfold not in (Type of H1) (Type of H3)`. + Example: :n:`unfold not in (type of H1) (type of H3)`. .. exn:: No such hypothesis: @ident. @@ -3216,10 +3219,10 @@ in the given databases. .. tacn:: autorewrite with {+ @ident} :name: autorewrite -This tactic [4]_ carries out rewritings according the rewriting rule +This tactic [4]_ carries out rewritings according to the rewriting rule bases :n:`{+ @ident}`. -Each rewriting rule of a base :n:`@ident` is applied to the main subgoal until +Each rewriting rule from the base :n:`@ident` is applied to the main subgoal until it fails. Once all the rules have been processed, if the main subgoal has progressed (e.g., if it is distinct from the initial main goal) then the rules of this base are processed again. If the main subgoal has not progressed then @@ -3312,7 +3315,7 @@ automatically created. (c.f. :ref:`The hints databases for auto and eauto <thehintsdatabasesforautoandeauto>`), making the retrieval more efficient. The legacy implementation (the default one for new databases) uses the DT only on goals without existentials (i.e., :tacn:`auto` - goals), for non-Immediate hints and do not make use of transparency + goals), for non-Immediate hints and does not make use of transparency hints, putting more work on the unification that is run after retrieval (it keeps a list of the lemmas in case the DT is not used). The new implementation enabled by the discriminated option makes use @@ -3496,7 +3499,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is The `emp` regexp does not match any search path while `eps` matches the empty path. During proof search, the path of successive successful hints on a search branch is recorded, as a - list of identifiers for the hints (note Hint Extern’s do not have + list of identifiers for the hints (note that Hint Extern’s do not have an associated identifier). Before applying any hint :n:`@ident` the current path `p` extended with :n:`@ident` is matched against the current cut expression `c` associated to @@ -3535,15 +3538,14 @@ Hint databases defined in the Coq standard library ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Several hint databases are defined in the Coq standard library. The -actual content of a database is the collection of the hints declared +actual content of a database is the collection of hints declared to belong to this database in each of the various modules currently -loaded. Especially, requiring new modules potentially extend a -database. At Coq startup, only the core database is non empty and can -be used. +loaded. Especially, requiring new modules may extend the database. +At Coq startup, only the core database is nonempty and can be used. :core: This special database is automatically used by ``auto``, except when pseudo-database ``nocore`` is given to ``auto``. The core database - contains only basic lemmas about negation, conjunction, and so on from. + contains only basic lemmas about negation, conjunction, and so on. Most of the hints in this database come from the Init and Logic directories. :arith: This database contains all lemmas about Peano’s arithmetic proved in the @@ -3655,7 +3657,7 @@ but this is a mere workaround and has some limitations (for instance, external hints cannot be removed). A proper way to fix this issue is to bind the hints to their module scope, as -for most of the other objects Coq uses. Hints should only made available when +for most of the other objects Coq uses. Hints should only be made available when the module they are defined in is imported, not just required. It is very difficult to change the historical behavior, as it would break a lot of scripts. We propose a smooth transitional path by providing the :opt:`Loose Hint Behavior` @@ -3774,9 +3776,9 @@ Therefore, the use of :tacn:`intros` in the previous proof is unnecessary. :name: dtauto While :tacn:`tauto` recognizes inductively defined connectives isomorphic to - the standard connective ``and, prod, or, sum, False, Empty_set, unit, True``, - :tacn:`dtauto` recognizes also all inductive types with one constructors and - no indices, i.e. record-style connectives. + the standard connectives ``and``, ``prod``, ``or``, ``sum``, ``False``, + ``Empty_set``, ``unit``, ``True``, :tacn:`dtauto` also recognizes all inductive + types with one constructor and no indices, i.e. record-style connectives. .. tacn:: intuition @tactic :name: intuition @@ -3792,7 +3794,7 @@ For instance, the tactic :g:`intuition auto` applied to the goal :: - (forall (x:nat), P x)/\B -> (forall (y:nat),P y)/\ P O \/B/\ P O + (forall (x:nat), P x) /\ B -> (forall (y:nat), P y) /\ P O \/ B /\ P O internally replaces it by the equivalent one: @@ -3819,9 +3821,9 @@ some incompatibilities. :name: dintuition While :tacn:`intuition` recognizes inductively defined connectives - isomorphic to the standard connective ``and``, ``prod``, ``or``, ``sum``, ``False``, - ``Empty_set``, ``unit``, ``True``, :tacn:`dintuition` recognizes also all inductive - types with one constructors and no indices, i.e. record-style connectives. + isomorphic to the standard connectives ``and``, ``prod``, ``or``, ``sum``, ``False``, + ``Empty_set``, ``unit``, ``True``, :tacn:`dintuition` also recognizes all inductive + types with one constructor and no indices, i.e. record-style connectives. .. opt:: Intuition Negation Unfolding @@ -3836,11 +3838,12 @@ The :tacn:`rtauto` tactic solves propositional tautologies similarly to what reflection scheme applied to a sequent calculus proof of the goal. The search procedure is also implemented using a different technique. -Users should be aware that this difference may result in faster proof- search +Users should be aware that this difference may result in faster proof-search but slower proof-checking, and :tacn:`rtauto` might not solve goals that :tacn:`tauto` would be able to solve (e.g. goals involving universal quantifiers). +Note that this tactic is only available after a ``Require Import Rtauto``. .. tacn:: firstorder :name: firstorder @@ -3887,7 +3890,7 @@ inductive definition. The tactic :tacn:`congruence`, by Pierre Corbineau, implements the standard Nelson and Oppen congruence closure algorithm, which is a decision procedure -for ground equalities with uninterpreted symbols. It also include the +for ground equalities with uninterpreted symbols. It also includes constructor theory (see :tacn:`injection` and :tacn:`discriminate`). If the goal is a non-quantified equality, congruence tries to prove it with non-quantified equalities in the context. Otherwise it tries to infer a discriminable equality @@ -3895,8 +3898,8 @@ from those in the context. Alternatively, congruence tries to prove that a hypothesis is equal to the goal or to the negation of another hypothesis. :tacn:`congruence` is also able to take advantage of hypotheses stating -quantified equalities, you have to provide a bound for the number of extra -equalities generated that way. Please note that one of the members of the +quantified equalities, but you have to provide a bound for the number of extra +equalities generated that way. Please note that one of the sides of the equality must contain all the quantified variables in order for congruence to match against it. @@ -3932,7 +3935,7 @@ match against it. discriminable equality but this proof could not be built in Coq because of dependently-typed functions. -.. exn:: Goal is solvable by congruence but some arguments are missing. Try congruence with ..., replacing metavariables by arbitrary terms. +.. exn:: Goal is solvable by congruence but some arguments are missing. Try congruence with {+ @term}, replacing metavariables by arbitrary terms. The decision procedure could solve the goal with the provision that additional arguments are supplied for some partially applied constructors. Any term of an @@ -4071,10 +4074,10 @@ symbol :g:`=`. .. tacn:: decide equality :name: decide equality - This tactic solves a goal of the form :g:`forall x y:R, {x=y}+{ ~x=y}`, + This tactic solves a goal of the form :g:`forall x y : R, {x = y} + {~ x = y}`, where :g:`R` is an inductive type such that its constructors do not take proofs or functions as arguments, nor objects in dependent types. It - solves goals of the form :g:`{x=y}+{ ~x=y}` as well. + solves goals of the form :g:`{x = y} + {~ x = y}` as well. .. tacn:: compare @term @term :name: compare @@ -4214,9 +4217,9 @@ using the ``Require Import`` command. Use ``classical_right`` to prove the right part of the disjunction with the assumption that the negation of left part holds. -.. _tactics-automatizing: +.. _tactics-automating: -Automatizing +Automating ------------ @@ -4245,6 +4248,12 @@ constructed over the following grammar: Internally, it uses a system very similar to the one of the ring tactic. + Note that this tactic is only available after a ``Require Import Btauto``. + +.. exn:: Cannot recognize a boolean equality. + + The goal is not of the form :g:`t = u`. Especially note that :tacn:`btauto` + doesn't introduce variables into the context on its own. .. tacn:: omega :name: omega @@ -4270,7 +4279,7 @@ distributivity, constant propagation) and comparing syntactically the results. :n:`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 sides are normalized. @@ -4319,21 +4328,6 @@ printed with the Print Fields command. See also: file plugins/setoid_ring/RealField.v for an example of instantiation, theory theories/Reals for many examples of use of field. -.. tacn:: fourier - :name: fourier - -This tactic written by Loïc Pottier solves linear inequalities on real -numbers using Fourier’s method :cite:`Fourier`. This tactic must be loaded by -``Require Import Fourier``. - -.. example:: - .. coqtop:: reset all - - Require Import Reals. - Require Import Fourier. - Goal forall x y:R, (x < y)%R -> (y + 1 >= x - 1)%R. - intros; fourier. - Non-logical tactics ------------------------ diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index c37233734b..0a517973c2 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1097,7 +1097,7 @@ described first. The scope of :cmd:`Opaque` is limited to the current section, or current file, unless the variant :cmd:`Global Opaque` is used. - See also: sections :ref:`performingcomputations`, :ref:`tactics-automatizing`, + See also: sections :ref:`performingcomputations`, :ref:`tactics-automating`, :ref:`proof-editing-mode` .. exn:: The reference @qualid was not found in the current environment. @@ -1131,7 +1131,7 @@ described first. There is no constant referred by :n:`@qualid` in the environment. See also: sections :ref:`performingcomputations`, - :ref:`tactics-automatizing`, :ref:`proof-editing-mode` + :ref:`tactics-automating`, :ref:`proof-editing-mode` .. _vernac-strategy: @@ -1217,19 +1217,19 @@ scope of their effect. There are four kinds of commands: current section or module it occurs in. As an example, the :cmd:`Coercion` and :cmd:`Strategy` commands belong to this category. + Commands whose default behavior is to stop their effect at the end - of the section they occur in but to extent their effect outside the module or + of the section they occur in but to extend their effect outside the module or library file they occur in. For these commands, the Local modifier limits the effect of the command to the current module if the command does not occur in a section and the Global modifier extends the effect outside the current sections and current module if the command occurs in a section. As an example, the :cmd:`Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong to this category. Notice that a subclass of these commands do not support - extension of their scope outside sections at all and the Global is not + extension of their scope outside sections at all and the Global modifier is not applicable to them. + Commands whose default behavior is to stop their effect at the end of the section or module they occur in. For these commands, the ``Global`` modifier extends their effect outside the sections and modules they - occurs in. The :cmd:`Transparent` and :cmd:`Opaque` + occur in. The :cmd:`Transparent` and :cmd:`Opaque` (see Section :ref:`vernac-controlling-the-reduction-strategies`) commands belong to this category. + Commands whose default behavior is to extend their effect outside |