diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 13 | ||||
| -rw-r--r-- | doc/sphinx/credits.rst | 101 | ||||
| -rw-r--r-- | doc/sphinx/introduction.rst | 4 | ||||
| -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 | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 8 | ||||
| -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 | 122 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 10 |
12 files changed, 553 insertions, 520 deletions
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/credits.rst b/doc/sphinx/credits.rst index 5d9324a656..2988b194e2 100644 --- a/doc/sphinx/credits.rst +++ b/doc/sphinx/credits.rst @@ -40,7 +40,7 @@ foundation of mathematics on constructive principles. The second one, Girard’s polymorphic :math:`\lambda`-calculus :math:`F_\omega`, is a very strong functional system in which we may represent higher-order logic proof structures. Combining both systems in a higher-order -extension of the Automath languages, T. Coquand presented in 1985 the +extension of the Automath language, T. Coquand presented in 1985 the first version of the *Calculus of Constructions*, CoC. This strong logical system allowed powerful axiomatizations, but direct inductive definitions were not possible, and inductive notions had to be defined @@ -246,14 +246,14 @@ pretty-printing rules has also changed. Eduardo Giménez redesigned the internal tactic libraries, giving uniform names to Caml functions corresponding to |Coq| tactic names. -Bruno Barras wrote new more efficient reductions functions. +Bruno Barras wrote new, more efficient reduction functions. Hugo Herbelin introduced more uniform notations in the |Coq| specification language: the definitions by fixpoints and pattern-matching have a more readable syntax. Patrick Loiseleur introduced user-friendly notations for arithmetic expressions. -New tactics were introduced: Eduardo Giménez improved a mechanism to +New tactics were introduced: Eduardo Giménez improved the mechanism to introduce macros for tactics, and designed special tactics for (co)inductive definitions; Patrick Loiseleur designed a tactic to simplify polynomial expressions in an arbitrary commutative ring which @@ -279,12 +279,12 @@ Loiseleur. Credits: addendum for version 6.3 ================================= -The main changes in version V6.3 was the introduction of a few new +The main changes in version V6.3 were the introduction of a few new tactics and the extension of the guard condition for fixpoint definitions. B. Barras extended the unification algorithm to complete partial terms -and solved various tricky bugs related to universes. +and fixed various tricky bugs related to universes. D. Delahaye developed the ``AutoRewrite`` tactic. He also designed the new behavior of ``Intro`` and provided the tacticals ``First`` and @@ -318,8 +318,8 @@ internal architecture of the system. The |Coq| version 7.0 was distributed in March 2001, version 7.1 in September 2001, version 7.2 in January 2002, version 7.3 in May 2002 and version 7.4 in February 2003. -Jean-Christophe Filliâtre designed the architecture of the new system, -he introduced a new representation for environments and wrote a new +Jean-Christophe Filliâtre designed the architecture of the new system. +He introduced a new representation for environments and wrote a new kernel for type-checking terms. His approach was to use functional data-structures in order to get more sharing, to prepare the addition of modules and also to get closer to a certified kernel. @@ -351,7 +351,7 @@ Letouzey adapted user contributions to extract ML programs when it was sensible. Jean-Christophe Filliâtre wrote ``coqdoc``, a documentation tool for |Coq| libraries usable from version 7.2. -Bruno Barras improved the reduction algorithms efficiency and the +Bruno Barras improved the efficiency of the reduction algorithm and the confidence level in the correctness of |Coq| critical type-checking algorithm. @@ -368,8 +368,8 @@ propositional inductive types. Loïc Pottier developed Fourier, a tactic solving linear inequalities on real numbers. -Pierre Crégut developed a new version based on reflexion of the Omega -decision tactic. +Pierre Crégut developed a new, reflection-based version of the Omega +decision procedure. Claudio Sacerdoti Coen designed an XML output for the |Coq| modules to be used in the Hypertextual Electronic Library of Mathematics (HELM cf @@ -419,7 +419,7 @@ main motivations were with a functional programming perfume (e.g. abstraction is now written fun), and more directly accessible to the novice (e.g. dependent product is now written forall and allows omission of - types). Also, parentheses and are no longer mandatory for function + types). Also, parentheses are no longer mandatory for function application. - extensibility: some standard notations (e.g. “<” and “>”) were @@ -438,8 +438,8 @@ language and of the language of commands has been carried out. The purpose here is a better uniformity making the tactics and commands easier to use and to remember. -Thirdly, a restructuration and uniformisation of the standard library of -Coq has been performed. There is now just one Leibniz’ equality usable +Thirdly, a restructuring and uniformization of the standard library of +Coq has been performed. There is now just one Leibniz equality usable for all the different kinds of |Coq| objects. Also, the set of real numbers now lies at the same level as the sets of natural and integer numbers. Finally, the names of the standard properties of numbers now @@ -447,7 +447,7 @@ follow a standard pattern and the symbolic notations for the standard definitions as well. The fourth point is the release of |CoqIDE|, a new graphical gtk2-based -interface fully integrated to |Coq|. Close in style from the Proof General +interface fully integrated with |Coq|. Close in style to the Proof General Emacs interface, it is faster and its integration with |Coq| makes interactive developments more friendly. All mathematical Unicode symbols are usable within |CoqIDE|. @@ -461,18 +461,17 @@ improved tactics (including a new tactic for solving first-order statements), new management commands, extended libraries. Bruno Barras and Hugo Herbelin have been the main contributors of the -reflexion and the implementation of the new syntax. The smart automatic +reflection and the implementation of the new syntax. The smart automatic translator from old to new syntax released with |Coq| is also their work with contributions by Olivier Desmettre. -Hugo Herbelin is the main designer and implementor of the notion of +Hugo Herbelin is the main designer and implementer of the notion of interpretation scopes and of the commands for easily adding new notations. -Hugo Herbelin is the main implementor of the restructuration of the -standard library. +Hugo Herbelin is the main implementer of the restructured standard library. -Pierre Corbineau is the main designer and implementor of the new tactic +Pierre Corbineau is the main designer and implementer of the new tactic for solving first-order statements in presence of inductive types. He is also the maintainer of the non-domain specific automation tactics. @@ -487,14 +486,14 @@ Pierre Letouzey and Jacek Chrząszcz respectively maintained the extraction tool and module system of |Coq|. Jean-Christophe Filliâtre, Pierre Letouzey, Hugo Herbelin and other -contributors from Sophia-Antipolis and Nijmegen participated to the -extension of the library. +contributors from Sophia-Antipolis and Nijmegen participated in +extending the library. Julien Narboux built a NSIS-based automatic |Coq| installation tool for the Windows platform. Hugo Herbelin and Christine Paulin coordinated the development which was -under the responsability of Christine Paulin. +under the responsibility of Christine Paulin. | Palaiseau & Orsay, Apr. 2004 | Hugo Herbelin & Christine Paulin @@ -525,12 +524,12 @@ arbitrary transition systems. Claudio Sacerdoti Coen added new features to the module system. -Benjamin Grégoire, Assia Mahboubi and Bruno Barras developed a new more -efficient and more general simplification algorithm on rings and +Benjamin Grégoire, Assia Mahboubi and Bruno Barras developed a new, more +efficient and more general simplification algorithm for rings and semi-rings. -Laurent Théry and Bruno Barras developed a new significantly more -efficient simplification algorithm on fields. +Laurent Théry and Bruno Barras developed a new, significantly more +efficient simplification algorithm for fields. Hugo Herbelin, Pierre Letouzey, Julien Forest, Julien Narboux and Claudio Sacerdoti Coen added new tactic features. @@ -554,7 +553,7 @@ Jean-Christophe Filliâtre’s contribution on finite maps have been integrated to the |Coq| standard library. Pierre Letouzey developed a library about finite sets “à la Objective Caml”. With Jean-Marc Notin, he extended the library on lists. Pierre Letouzey’s contribution on -rational numbers has been integrated and extended.. +rational numbers has been integrated and extended. Pierre Corbineau extended his tactic for solving first-order statements. He wrote a reflection-based intuitionistic tautology solver. @@ -589,8 +588,8 @@ various aspects. Regarding the language of |Coq|, the main novelty is the introduction by Matthieu Sozeau of a package of commands providing Haskell-style type classes. Type classes, that come with a few convenient features such as -type-based resolution of implicit arguments, plays a new role of -landmark in the architecture of |Coq| with respect to automatization. For +type-based resolution of implicit arguments, play a new landmark role +in the architecture of |Coq| with respect to automation. For instance, thanks to type classes support, Matthieu Sozeau could implement a new resolution-based version of the tactics dedicated to rewriting on arbitrary transitive relations. @@ -599,13 +598,13 @@ Another major improvement of |Coq| 8.2 is the evolution of the arithmetic libraries and of the tools associated to them. Benjamin Grégoire and Laurent Théry contributed a modular library for building arbitrarily large integers from bounded integers while Evgeny Makarov contributed a -modular library of abstract natural and integer arithmetics together +modular library of abstract natural and integer arithmetic together with a few convenient tactics. On his side, Pierre Letouzey made numerous extensions to the arithmetic libraries on :math:`\mathbb{Z}` -and :math:`\mathbb{Q}`, including extra support for automatization in +and :math:`\mathbb{Q}`, including extra support for automation in presence of various number-theory concepts. -Frédéric Besson contributed a reflexive tactic based on Krivine-Stengle +Frédéric Besson contributed a reflective tactic based on Krivine-Stengle Positivstellensatz (the easy way) for validating provability of systems of inequalities. The platform is flexible enough to support the validation of any algorithm able to produce a “certificate” for the @@ -620,10 +619,10 @@ relying on Benjamin Grégoire and Laurent Théry’s library, delivered a library of unbounded integers in base :math:`2^{31}`. As importantly, he developed a notion of “retro-knowledge” so as to safely extend the kernel-located bytecode-based efficient evaluation algorithm of |Coq| -version 8.1 to use 31-bits machine arithmetics for efficiently computing +version 8.1 to use 31-bits machine arithmetic for efficiently computing with the library of integers he developed. -Beside the libraries, various improvements contributed to provide a more +Beside the libraries, various improvements were contributed to provide a more comfortable end-user language and more expressive tactic language. Hugo Herbelin and Matthieu Sozeau improved the pattern-matching compilation algorithm (detection of impossible clauses in pattern-matching, @@ -632,7 +631,7 @@ and Matthieu Sozeau contributed various new convenient syntactic constructs and new tactics or tactic features: more inference of redundant information, better unification, better support for proof or definition by fixpoint, more expressive rewriting tactics, better -support for meta-variables, more convenient notations, ... +support for meta-variables, more convenient notations... Élie Soubiran improved the module system, adding new features (such as an “include” command) and making it more flexible and more general. He @@ -641,7 +640,7 @@ mechanism. Matthieu Sozeau extended the Russell language, ending in an convenient way to write programs of given specifications, Pierre Corbineau extended -the Mathematical Proof Language and the automatization tools that +the Mathematical Proof Language and the automation tools that accompany it, Pierre Letouzey supervised and extended various parts of the standard library, Stéphane Glondu contributed a few tactics and improvements, Jean-Marc Notin provided help in debugging, general @@ -662,7 +661,7 @@ adaptation of the interface of the old “setoid rewrite” tactic to the new version. Lionel Mamane worked on the interaction between |Coq| and its external interfaces. With Samuel Mimram, he also helped making |Coq| compatible with recent software tools. Russell O’Connor, Cezary -Kaliscyk, Milad Niqui contributed to improve the libraries of integers, +Kaliszyk, Milad Niqui contributed to improve the libraries of integers, rational, and real numbers. We also thank many users and partners for suggestions and feedback, in particular Pierre Castéran and Arthur Charguéraud, the INRIA Marelle team, Georges Gonthier and the @@ -704,8 +703,8 @@ The module system evolved significantly. Besides the resolution of some efficiency issues and a more flexible construction of module types, Élie Soubiran brought a new model of name equivalence, the :math:`\Delta`-equivalence, which respects as much as possible the names -given by the users. He also designed with Pierre Letouzey a new -convenient operator ``<+`` for nesting functor application, that +given by the users. He also designed with Pierre Letouzey a new, +convenient operator ``<+`` for nesting functor application that provides a light notation for inheriting the properties of cascading modules. @@ -719,7 +718,7 @@ the extraction mechanism. Bruno Barras and Élie Soubiran maintained the Coq checker, Julien Forest maintained the Function mechanism for reasoning over recursively defined functions. Matthieu Sozeau, Hugo Herbelin and Jean-Marc Notin maintained coqdoc. Frédéric Besson -maintained the Micromega plateform for deciding systems of inequalities. +maintained the Micromega platform for deciding systems of inequalities. Pierre Courtieu maintained the support for the Proof General Emacs interface. Claude Marché maintained the plugin for calling external provers (dp). Yves Bertot made some improvements to the libraries of @@ -736,7 +735,7 @@ support for benchmarking and archiving. Many users helped by reporting problems, providing patches, suggesting improvements or making useful comments, either on the bug tracker or on -the Coq-club mailing list. This includes but not exhaustively Cédric +the Coq-Club mailing list. This includes but not exhaustively Cédric Auger, Arthur Charguéraud, François Garillot, Georges Gonthier, Robin Green, Stéphane Lescuyer, Eelis van der Weegen, ... @@ -772,8 +771,8 @@ structured scripts (bullets and proof brackets) but, even if yet not user-available, the new engine also provides the basis for refining existential variables using tactics, for applying tactics to several goals simultaneously, for reordering goals, all features which are -planned for the next release. The new proof engine forced to reimplement -info and Show Script differently, what was done by Pierre Letouzey. +planned for the next release. The new proof engine forced Pierre Letouzey +to reimplement info and Show Script differently. Before version 8.4, |CoqIDE| was linked to |Coq| with the graphical interface living in a separate thread. From version 8.4, |CoqIDE| is a @@ -784,7 +783,7 @@ sessions in parallel. Relying on the infrastructure work made by Vincent Gross, Pierre Letouzey, Pierre Boutillier and Pierre-Marie Pédrot contributed many various refinements of |CoqIDE|. -Coq 8.4 also comes with a bunch of many various smaller-scale changes +Coq 8.4 also comes with a bunch of various smaller-scale changes and improvements regarding the different components of the system. The underlying logic has been extended with :math:`\eta`-conversion @@ -831,7 +830,7 @@ Pierre Letouzey added a tactic timeout and the interruptibility of vm\_compute. Bug fixes and miscellaneous improvements of the tactic language came from Hugo Herbelin, Pierre Letouzey and Matthieu Sozeau. -Regarding decision tactics, Loïc Pottier maintained Nsatz, moving in +Regarding decision tactics, Loïc Pottier maintained nsatz, moving in particular to a type-class based reification of goals while Frédéric Besson maintained Micromega, adding in particular support for division. @@ -894,7 +893,7 @@ Boutillier (MacOS), Stéphane Glondu (Debian). Releasing, testing and benchmarking support was provided by Jean-Marc Notin. Many suggestions for improvements were motivated by feedback from users, -on either the bug tracker or the coq-club mailing list. Special thanks +on either the bug tracker or the Coq-Club mailing list. Special thanks are going to the users who contributed patches, starting with Tom Prince. Other patch contributors include Cédric Auger, David Baelde, Dan Grayson, Paolo Herms, Robbert Krebbers, Marc Lasson, Hendrik Tews and @@ -1036,7 +1035,7 @@ X). Maxime Dénès improved significantly the testing and benchmarking support. Many power users helped to improve the design of the new features via -the bug tracker, the coq development mailing list or the coq-club +the bug tracker, the coq development mailing list or the Coq-Club mailing list. Special thanks are going to the users who contributed patches and intensive brain-storming, starting with Jason Gross, Jonathan Leivent, Greg Malecha, Clément Pit-Claudel, Marc Lasson, Lionel @@ -1154,13 +1153,13 @@ Gregory Malecha, and Matthieu Sozeau. Matej Košík maintained and greatly improved the continuous integration setup and the testing of |Coq| contributions. He also contributed many API -improvement and code cleanups throughout the system. +improvements and code cleanups throughout the system. The contributors for this version are Bruno Barras, C.J. Bell, Yves Bertot, Frédéric Besson, Pierre Boutillier, Tej Chajed, Guillaume Claret, Xavier Clerc, Pierre Corbineau, Pierre Courtieu, Maxime Dénès, Ricky Elrod, Emilio Jesús Gallego Arias, Jason Gross, Hugo Herbelin, -Sébastien Hinderer, Jacques-Henri Jourdan, Matej Kosik, Xavier Leroy, +Sébastien Hinderer, Jacques-Henri Jourdan, Matej Košík, Xavier Leroy, Pierre Letouzey, Gregory Malecha, Cyprien Mangin, Erik Martin-Dorel, Guillaume Melquiond, Clément Pit–Claudel, Pierre-Marie Pédrot, Daniel de Rauglaudre, Lionel Rieg, Gabriel Scherer, Thomas Sibut-Pinote, Matthieu @@ -1171,7 +1170,7 @@ Dénès, who was also in charge of the release process. Many power users helped to improve the design of the new features via the bug tracker, the pull request system, the |Coq| development mailing -list or the coq-club mailing list. Special thanks to the users who +list or the Coq-Club mailing list. Special thanks to the users who contributed patches and intensive brain-storming and code reviews, starting with Cyril Cohen, Jason Gross, Robbert Krebbers, Jonathan Leivent, Xavier Leroy, Gregory Malecha, Clément Pit–Claudel, Gabriel @@ -1279,7 +1278,7 @@ the maintainer of this release. Many power users helped to improve the design of the new features via the bug tracker, the pull request system, the |Coq| development mailing list or the -coq-club mailing list. Special thanks to the users who contributed patches and +Coq-Club mailing list. Special thanks to the users who contributed patches and intensive brain-storming and code reviews, starting with Jason Gross, Ralf Jung, Robbert Krebbers, Xavier Leroy, Clément Pit–Claudel and Gabriel Scherer. It would however be impossible to mention exhaustively the names of everybody who diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index c7bc69db4e..1a610396e5 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -12,7 +12,7 @@ https://github.com/coq/coq/wiki#coq-tutorials). The |Coq| system is designed to develop mathematical proofs, and especially to write formal specifications, programs and to verify that -programs are correct with respect to their specification. It provides a +programs are correct with respect to their specifications. It provides a specification language named |Gallina|. Terms of |Gallina| can represent programs as well as properties of these programs and proofs of these properties. Using the so-called *Curry-Howard isomorphism*, programs, @@ -52,7 +52,7 @@ are processed from a file. How to read this book ===================== -This is a Reference Manual, so it is not made for a continuous reading. +This is a Reference Manual, so it is not intended for continuous reading. We recommend using the various indexes to quickly locate the documentation you are looking for. There is a global index, and a number of specific indexes for tactics, vernacular commands, and error messages and warnings. 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..d9b2490452 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1079,7 +1079,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/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index ac6a20198d..8250b4b3d6 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1430,6 +1430,12 @@ the following attributes names are recognized: Takes as value the optional attributes ``since`` and ``note``; both have a string value. + This attribute can trigger the following warnings: + + .. warn:: Tactic @qualid is deprecated since @string. @string. + + .. warn:: Tactic Notation @qualid is deprecated since @string. @string. + Here are a few examples: .. coqtop:: all reset @@ -1440,7 +1446,7 @@ Here are a few examples: exact O. Defined. - #[deprecated(since="8.9.0", note="use idtac instead")] + #[deprecated(since="8.9.0", note="Use idtac instead.")] Ltac foo := idtac. Goal True. 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 ec085a71e5..9b4d724e02 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`. @@ -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. @@ -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 |