Introduction and Contents¶
This is the reference manual of Coq. Coq is an interactive theorem prover. It lets you formalize mathematical concepts and then helps you interactively generate machine-checked proofs of theorems. Machine checking gives users much more confidence that the proofs are correct compared to human-generated and -checked proofs. Coq has been used in a number of flagship verification projects, including the CompCert verified C compiler, and has served to verify the proof of the four color theorem (among many other mathematical formalizations).
Users generate proofs by entering a series of tactics that constitute
steps in the proof. There are many built-in tactics, some of which
are elementary, while others implement complex decision procedures
(such as lia
, a decision procedure for linear integer
arithmetic). Ltac and its planned replacement,
Ltac2, provide languages to define new tactics by
combining existing tactics with looping and conditional constructs.
These permit automation of large parts of proofs and sometimes entire
proofs. Furthermore, users can add novel tactics or functionality by
creating Coq plugins using OCaml.
The Coq kernel, a small part of Coq, does the final verification that the tactic-generated proof is valid. Usually the tactic-generated proof is indeed correct, but delegating proof verification to the kernel means that even if a tactic is buggy, it won't be able to introduce an incorrect proof into the system.
Finally, Coq also supports extraction of verified programs to programming languages such as OCaml and Haskell. This provides a way of executing Coq code efficiently and can be used to create verified software libraries.
To learn Coq, beginners are advised to first start with a tutorial / book. Several such tutorials / books are listed at https://coq.inria.fr/documentation.
This manual is organized in three main parts, plus an appendix:
The first part presents the specification language of Coq, that allows to define programs and state mathematical theorems. Core language presents the language that the kernel of Coq understands. Language extensions presents the richer language, with notations, implicits, etc. that a user can use and which is translated down to the language of the kernel by means of an "elaboration process".
The second part presents proof mode, the central feature of Coq. Basic proof writing introduces this interactive mode and the available proof languages. Automatic solvers and programmable tactics presents some more advanced tactics, while Creating new tactics is about the languages that allow a user to combine tactics together and develop new ones.
The third part shows how to use Coq in practice. Libraries and plugins presents some of the essential reusable blocks from the ecosystem and some particularly important extensions such as the program extraction mechanism. Command-line and graphical tools documents important tools that a user needs to build a Coq project.
In the appendix, History and recent changes presents the history of Coq and changes in recent releases. This is an important reference if you upgrade the version of Coq that you use. The various indexes are very useful to quickly browse the manual and find what you are looking for. They are often the main entry point to the manual.
The full table of contents is presented below:
Contents¶
- Core language
- Basic notions and conventions
- Sorts
- Functions and assumptions
- Definitions
- Conversion rules
- Typing rules
- Variants and the
match
construct - Record types
- Inductive types and recursive functions
- Coinductive types and corecursive functions
- Sections
- The Module System
- Primitive objects
- Polymorphic Universes
- SProp (proof irrelevant propositions)
- Language extensions
- Existential variables
- Implicit arguments
- The different kinds of implicit arguments
- Maximal and non-maximal insertion of implicit arguments
- Casual use of implicit arguments
- Declaration of implicit arguments
- Implicit Argument Binders
- Mode for automatic declaration of implicit arguments
- Controlling strict implicit arguments
- Controlling contextual implicit arguments
- Controlling reversible-pattern implicit arguments
- Controlling the insertion of implicit arguments not followed by explicit arguments
- Combining manual declaration and automatic declaration
- Explicit applications
- Displaying implicit arguments
- Displaying implicit arguments when pretty-printing
- Interaction with subtyping
- Deactivation of implicit arguments for parsing
- Implicit types of variables
- Implicit generalization
- Extended pattern matching
- Variants and extensions of
match
- Patterns
- Multiple patterns
- Aliasing subpatterns
- Nested patterns
- Disjunctive patterns
- About patterns of parametric types
- Implicit arguments in patterns
- Matching objects of dependent types
- Understanding dependencies in patterns
- When the elimination predicate must be provided
- Using pattern matching to write proofs
- Pattern-matching on inductive objects involving local definitions
- Pattern-matching and coercions
- When does the expansion strategy fail?
- Variants and extensions of
- Syntax extensions and notation scopes
- Notations
- Basic notations
- Precedences and associativity
- Complex notations
- Simple factorization rules
- Use of notations for printing
- The Infix command
- Reserving notations
- Simultaneous definition of terms and notations
- Enabling and disabling notations
- Displaying information about notations
- Locating notations
- Inheritance of the properties of arguments of constants bound to a notation
- Notations and binders
- Binders bound in the notation and parsed as identifiers
- Binders bound in the notation and parsed as patterns
- Binders bound in the notation and parsed as terms
- Binders bound in the notation and parsed as general binders
- Binders not bound in the notation
- Notations with expressions used both as binder and term
- Notations with recursive patterns
- Notations with recursive patterns involving binders
- Predefined entries
- Custom entries
- Syntax
- Notation scopes
- Abbreviations
- Numbers and strings
- Tactic Notations
- Notations
- Setting properties of a function's arguments
- Implicit Coercions
- Typeclasses
- Canonical Structures
- Program
- Commands
- Basic proof writing
- Proof mode
- Tactics
- Reasoning with equalities
- Reasoning with inductive types
- The SSReflect proof language
- Introduction
- Usage
- Gallina extensions
- Basic tactics
- Control flow
- Rewriting
- An extended rewrite tactic
- Remarks and examples
- Rewrite redex selection
- Chained rewrite steps
- Explicit redex switches are matched first
- Occurrence switches and redex switches
- Occurrence selection and repetition
- Multi-rule rewriting
- Wildcards vs abstractions
- When SSReflect rewrite fails on standard Coq licit rewrite
- Existential metavariables and rewriting
- Rewriting under binders
- Locking, unlocking
- Congruence
- Contextual patterns
- Views and reflection
- Synopsis and Index
- Automatic solvers and programmable tactics
- Solvers for logic and equality
- Micromega: solvers for arithmetic goals over ordered rings
- Short description of the tactics
- Positivstellensatz refutations
lra
: a decision procedure for linear real and rational arithmeticlia
: a tactic for linear integer arithmeticnra
: a proof procedure for non-linear arithmeticnia
: a proof procedure for non-linear integer arithmeticpsatz
: a proof procedure for non-linear arithmeticzify
: pre-processing of arithmetic goals
- ring and field: solvers for polynomial and rational equations
- Nsatz: a solver for equalities in integral domains
- Programmable proof search
- Generalized rewriting
- Creating new tactics
- Ltac
- Syntax
- Values
- Goal selectors
- Processing multiple goals
- Branching and backtracking
- Control flow
- Alternatives
- Success and failure
- Manipulating values
- Pattern matching on terms: match
- Pattern matching on goals and hypotheses: match goal
- Filling a term context
- Generating fresh hypothesis names
- Computing in a term: eval
- Getting the type of a term
- Manipulating untyped terms: type_term
- Counting goals: numgoals
- Testing boolean expressions: guard
- Checking properties of terms
- Timing
- Print/identity tactic: idtac
- Tactic toplevel definitions
- Examples of using
L
tac - Debugging
L
tac tactics
- Ltac2
- Ltac
- Libraries and plugins
- Command-line and graphical tools
- Building Coq Projects
- Coq commands
- Documenting Coq files with coqdoc
- CoqIDE
- Asynchronous and Parallel Proof Processing
- History and recent changes
- Early history of Coq
- Historical roots
- Versions 1 to 5
- Versions 6
- Versions 7
- Summary of changes
- Details of changes in 7.0 and 7.1
- Main novelties
- Details of changes
- Language: new "let-in" construction
- Language: long names
- Language: miscellaneous
- Language: Cases
- Reduction
- New tactics
- Changes in existing tactics
- Efficiency
- Concrete syntax of constructions
- Parsing and grammar extension
- New commands
- Changes in existing commands
- Tools
- Extraction
- Standard library
- New user contributions
- Details of changes in 7.2
- Details of changes in 7.3
- Details of changes in 7.4
- Recent changes
- Version 8.19
- Version 8.18
- Version 8.17
- Version 8.16
- Version 8.15
- Version 8.14
- Version 8.13
- Version 8.12
- Version 8.11
- Version 8.10
- Version 8.9
- Version 8.8
- Version 8.7
- Version 8.6
- Version 8.5
- Version 8.4
- Version 8.3
- Version 8.2
- Version 8.1
- Version 8.0
- Early history of Coq
- Indexes
- Bibliography
Note
License
This material (the Coq Reference Manual) may be distributed only subject to the terms and conditions set forth in the Open Publication License, v1.0 or later (the latest version is presently available at http://www.opencontent.org/openpub). Options A and B are not elected.