# Introduction¶

This document is the Reference Manual of the Coq proof assistant. To start using Coq, it is advised to first read a tutorial. Links to several tutorials can be found at https://coq.inria.fr/documentation (see also 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
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,
properties and proofs are formalized in the same language called
*Calculus of Inductive Constructions*, that is a
\(\lambda\)-calculus with a rich type system. All logical judgments
in Coq are typing judgments. The very heart of the Coq system is the
type-checking algorithm that checks the correctness of proofs, in other
words that checks that a program complies to its specification. Coq also
provides an interactive proof assistant to build proofs using specific
programs called *tactics*.

All services of the Coq proof assistant are accessible by interpretation
of a command language called *the vernacular*.

Coq has an interactive mode in which commands are interpreted as the user types them in from the keyboard and a compiled mode where commands are processed from a file.

- In interactive mode, users can develop their theories and proofs step by step, and query the system for available theorems and definitions. The interactive mode is generally run with the help of an IDE, such as CoqIDE, documented in Coq Integrated Development Environment, Emacs with Proof-General [Asp00] [1], or jsCoq to run Coq in your browser (see https://github.com/ejgallego/jscoq). The coqtop read-eval-print-loop can also be used directly, for debugging purposes.
- The compiled mode acts as a proof checker taking a file containing a whole development in order to ensure its correctness. Moreover, Coq’s compiler provides an output file containing a compact representation of its input. The compiled mode is run with the coqc command.

See also

## How to read this book¶

This is a Reference Manual, so it is not made for a 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. Nonetheless, the manual has some structure that is explained below.

- The first part describes the specification language, Gallina. Chapters The Gallina specification language and Extensions of Gallina describe the concrete syntax as well as the meaning of programs, theorems and proofs in the Calculus of Inductive Constructions. Chapter The Coq library describes the standard library of Coq. Chapter Calculus of Inductive Constructions is a mathematical description of the formalism. Chapter The Module System describes the module system.
- The second part describes the proof engine. It is divided in six
chapters. Chapter Vernacular commands presents all commands (we
call them
*vernacular commands*) that are not directly related to interactive proving: requests to the environment, complete or partial evaluation, loading and compiling files. How to start and stop proofs, do multiple proofs in parallel is explained in Chapter Proof handling. In Chapter Tactics, all commands that realize one or more steps of the proof are presented: we call them*tactics*. The language to combine these tactics into complex proof strategies is given in Chapter The tactic language. Examples of tactics are described in Chapter Detailed examples of tactics. Finally, the SSReflect proof language is presented in Chapter The SSReflect proof language. - The third part describes how to extend the syntax of Coq in Chapter Syntax extensions and interpretation scopes and how to define new induction principles in Chapter Proof schemes.
- In the fourth part more practical tools are documented. First in Chapter The Coq commands, the usage of coqc (batch mode) and coqtop (interactive mode) with their options is described. Then, in Chapter Utilities, various utilities that come with the Coq distribution are presented. Finally, Chapter Coq Integrated Development Environment describes CoqIDE.
- The fifth part documents a number of advanced features, including coercions, canonical structures, typeclasses, program extraction, and specialized solvers and tactics. See the table of contents for a complete list.

## List of additional documentation¶

This manual does not contain all the documentation the user may need about Coq. Various informations can be found in the following documents:

- Tutorial
- A companion volume to this reference manual, the Coq Tutorial, is aimed at gently introducing new users to developing proofs in Coq without assuming prior knowledge of type theory. In a second step, the user can read also the tutorial on recursive types (document RecTutorial.ps).
- Installation
- A text file INSTALL that comes with the sources explains how to install Coq.
- The Coq standard library
- A commented version of sources of the Coq standard library (including only the specifications, the proofs are removed) is available at https://coq.inria.fr/stdlib/.

# Table of contents¶

- Introduction
- Credits
- Credits: addendum for version 6.1
- Credits: addendum for version 6.2
- Credits: addendum for version 6.3
- Credits: versions 7
- Credits: version 8.0
- Credits: version 8.1
- Credits: version 8.2
- Credits: version 8.3
- Credits: version 8.4
- Credits: version 8.5
- Credits: version 8.6
- Credits: version 8.7
- Credits: version 8.8

- The Gallina specification language
- Extensions of Gallina
- Record types
- Variants and extensions of
`match`

- Advanced recursive functions
- Section mechanism
- Module system
- Libraries and qualified names
- Implicit arguments
- The different kinds of implicit arguments
- Maximal or non maximal insertion of implicit arguments
- Casual use of implicit arguments
- Declaration of implicit arguments
- Automatic declaration of implicit arguments
- 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
- Explicit applications
- Renaming implicit arguments
- Displaying what the implicit arguments are
- Explicit displaying of implicit arguments for pretty-printing
- Interaction with subtyping
- Deactivation of implicit arguments for parsing
- Canonical structures
- Implicit types of variables
- Implicit generalization

- Coercions
- Printing constructions in full
- Printing universes
- Existential variables

- The Coq library
- Calculus of Inductive Constructions
- The Module System

- Vernacular commands
- Proof handling
- Tactics
- Invocation of tactics
- Applying theorems
- Managing the local context
- Controlling the proof flow
- Case analysis and induction
- Rewriting expressions
- Performing computations
- Automation
- Controlling automation
- Decision procedures
- Checking properties of terms
- Equality
- Equality and inductive sets
- Inversion
- Classical tactics
- Automatizing
- Non-logical tactics
- Simple tactic macros

- The tactic language
- Syntax
- Semantics
- Sequence
- Local application of tactics
- Goal selectors
- For loop
- Repeat loop
- Error catching
- Detecting progress
- Backtracking branching
- First tactic to work
- Left-biased branching
- Generalized biased branching
- Soft cut
- Checking the successes
- Checking the failure
- Checking the success
- Solving
- Identity
- Failing
- Timeout
- Timing a tactic
- Timing a tactic that evaluates to a term
- Local definitions
- Application
- Function construction
- Pattern matching on terms
- Pattern matching on goals
- Filling a term context
- Generating fresh hypothesis names
- Computing in a constr
- Recovering the type of a term
- Manipulating untyped terms
- Counting the goals
- Testing boolean expressions
- Proving a subgoal as a separate lemma

- Tactic toplevel definitions
- Debugging L
_{tac}tactics

- Detailed examples of tactics
- 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

- Locking, unlocking
- Congruence

- Contextual patterns
- Views and reflection
- SSReflect searching tool
- Synopsis and Index

- Syntax extensions and interpretation scopes
- Notations
- Basic notations
- Precedences and associativity
- Complex notations
- Simple factorization rules
- Displaying symbolic notations
- The Infix command
- Reserving notations
- Simultaneous definition of terms and notations
- Displaying informations about notations
- Locating notations
- Notations and binders
- Notations with recursive patterns
- Notations with recursive patterns involving binders
- Predefined entries
- Summary

- Interpretation scopes
- Abbreviations
- Tactic Notations

- Notations
- Proof schemes

- The Coq commands
- Utilities
- Coq Integrated Development Environment

- Extended pattern-matching
- 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?

- Implicit Coercions
- Canonical Structures
- Type Classes
- Omega: a solver for quantifier-free problems in Presburger Arithmetic
- Micromega: tactics for solving arithmetic goals over ordered rings
- Short description of the tactics
*Positivstellensatz*refutations- lra: a decision procedure for linear real and rational arithmetic
- lia: a tactic for linear integer arithmetic
- nra: a proof procedure for non-linear arithmetic
- nia: a proof procedure for non-linear integer arithmetic
- psatz: a proof procedure for non-linear arithmetic

- Extraction of programs in OCaml and Haskell
- Program
- The ring and field tactic families
- Nsatz: tactics for proving equalities in integral domains
- Generalized rewriting
- Asynchronous and Parallel Proof Processing
- Miscellaneous extensions
- Polymorphic Universes

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.

[1] | Proof-General is available at https://proofgeneral.github.io/. Optionally, you can enhance it with the minor mode Company-Coq [PCC16] (see https://github.com/cpitclaudel/company-coq). |