Coq
8.11.2

Indexes

  • Index
  • Command index
  • Tactic index
  • Flags, options and tables index
  • Errors and warnings index

Preamble

  • Introduction and Contents
  • Early history of Coq
    • Historical roots
    • Versions 1 to 5
      • Version 1
      • Version 2
      • Version 3
      • Version 4
      • Version 5
    • Versions 6
      • Version 6.1
      • Version 6.2
      • Version 6.3
    • Versions 7
      • Summary of changes
      • Details of changes in 7.0 and 7.1
        • Main novelties
        • Details of changes
      • Details of changes in 7.2
      • Details of changes in 7.3
        • Changes in 7.3.1
      • Details of changes in 7.4
  • Recent changes
    • Version 8.11
      • Summary of changes
      • Changes in 8.11+beta1
      • Changes in 8.11.0
      • Changes in 8.11.1
      • Changes in 8.11.2
    • Version 8.10
      • Summary of changes
      • Other changes in 8.10+beta1
      • Changes in 8.10+beta2
      • Changes in 8.10+beta3
      • Changes in 8.10.0
      • Changes in 8.10.1
      • Changes in 8.10.2
    • Version 8.9
      • Summary of changes
      • Details of changes in 8.9+beta1
      • Changes in 8.8.0
      • Changes in 8.8.1
    • Version 8.8
      • Summary of changes
      • Details of changes in 8.8+beta1
      • Details of changes in 8.8.0
      • Details of changes in 8.8.1
      • Details of changes in 8.8.2
    • Version 8.7
      • Summary of changes
      • Potential compatibility issues
      • Details of changes in 8.7+beta1
      • Details of changes in 8.7+beta2
      • Details of changes in 8.7.0
      • Details of changes in 8.7.1
      • Details of changes in 8.7.2
    • Version 8.6
      • Summary of changes
      • Potential sources of incompatibilities
      • Details of changes in 8.6beta1
      • Details of changes in 8.6
      • Details of changes in 8.6.1
    • Version 8.5
      • Summary of changes
      • Potential sources of incompatibilities
      • Details of changes in 8.5beta1
      • Details of changes in 8.5beta2
      • Details of changes in 8.5beta3
      • Details of changes in 8.5
      • Details of changes in 8.5pl1
      • Details of changes in 8.5pl2
      • Details of changes in 8.5pl3
    • Version 8.4
      • Summary of changes
      • Potential sources of incompatibilities
      • Details of changes in 8.4beta
      • Details of changes in 8.4beta2
      • Details of changes in 8.4
    • Version 8.3
      • Summary of changes
      • Details of changes
    • Version 8.2
      • Summary of changes
      • Details of changes
    • Version 8.1
      • Summary of changes
      • Details of changes in 8.1beta
      • Details of changes in 8.1gamma
      • Details of changes in 8.1
    • Version 8.0
      • Summary of changes
      • Details of changes in 8.0beta old syntax
      • Details of changes in 8.0beta new syntax
      • Details of changes in 8.0

The language

  • The Gallina specification language
    • About the grammars in the manual
    • Lexical conventions
    • Terms
      • Syntax of terms
      • Types
      • Qualified identifiers and simple identifiers
      • Numerals
      • Sorts
      • Binders
      • Abstractions
      • Products
      • Applications
      • Type cast
      • Inferable subterms
      • Let-in definitions
      • Definition by case analysis
      • Recursive functions
    • The Vernacular
      • Assumptions
      • Definitions
      • Inductive definitions
        • Simple inductive types
        • Simple annotated inductive types
        • Parameterized inductive types
        • Variants
        • Mutually defined inductive types
        • Co-inductive types
      • Definition of recursive functions
        • Definition of functions by recursion over inductive objects
        • Definitions of recursive objects in co-inductive types
      • Assertions and proofs
      • Attributes
  • Extensions of Gallina
    • Record types
      • Primitive Projections
        • Primitive Record Types
        • Reduction
        • Compatibility Projections and match
    • Variants and extensions of match
      • Multiple and nested pattern matching
      • Pattern-matching on boolean values: the if expression
      • Irrefutable patterns: the destructuring let variants
        • First destructuring let syntax
        • Second destructuring let syntax
      • Controlling pretty-printing of match expressions
        • Printing nested patterns
        • Factorization of clauses with same right-hand side
        • Use of a default clause
        • Printing of wildcard patterns
        • Printing of the elimination predicate
        • Printing matching on irrefutable patterns
        • Printing matching on booleans
    • Advanced recursive functions
    • Section mechanism
    • Module system
      • Reserved commands inside an interactive module
      • Reserved commands inside an interactive module type:
    • Libraries and qualified names
      • Names of libraries
      • Qualified names
      • Libraries and filesystem
    • Implicit arguments
      • The different kinds of implicit arguments
        • Implicit arguments inferable from the knowledge of other arguments of a function
        • Implicit arguments inferable by resolution
      • Maximal or non maximal insertion of implicit arguments
      • Casual use of implicit arguments
      • Declaration of implicit arguments
        • Implicit Argument Binders
        • Declaring 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
      • Explicit displaying of existential instances for pretty-printing
      • Solving existential variables using tactics
    • Primitive Integers
    • Primitive Floats
    • Bidirectionality hints
  • The Coq library
    • The basic library
      • Notations
      • Logic
        • Propositional Connectives
        • Quantifiers
        • Equality
        • Lemmas
      • Datatypes
        • Programming
      • Specification
      • Basic Arithmetic
      • Well-founded recursion
      • Accessing the Type level
      • Tactics
    • The standard library
      • Survey
      • Peano’s arithmetic (nat)
      • Notations for integer arithmetic
      • Real numbers library
        • Notations for real numbers
        • Some tactics for real numbers
      • List library
      • Floats library
    • Users’ contributions
  • Calculus of Inductive Constructions
    • The terms
      • Sorts
      • Terms
    • Typing rules
    • Conversion rules
      • β-reduction
      • ι-reduction
      • δ-reduction
      • ζ-reduction
      • η-expansion
      • Proof Irrelevance
      • Convertibility
    • Subtyping rules
    • Inductive Definitions
      • Types of inductive objects
      • Well-formed inductive definitions
        • Arity of a given sort
        • Arity
        • Type of constructor
        • Positivity Condition
        • Strict positivity
        • Nested Positivity
        • Correctness rules
        • Template polymorphism
      • Destructors
        • The match ... with ... end construction
      • Fixpoint definitions
        • Typing rule
        • Reduction rule
    • Admissible rules for global environments
    • Co-inductive types
    • The Calculus of Inductive Constructions with impredicative Set
  • The Module System
    • Modules and module types
    • Typing Modules

The proof engine

  • Vernacular commands
    • Displaying
    • Flags, Options and Tables
      • Scope qualifiers for Set and Unset
    • Requests to the environment
    • Printing flags
    • Loading files
    • Compiled files
    • Loadpath
    • Backtracking
    • Quitting and debugging
    • Controlling display
    • Controlling the reduction strategies and the conversion algorithm
    • Controlling the locality of commands
    • Controlling Typing Flags
    • Internal registration commands
      • Exposing constants to OCaml libraries
      • Inlining hints for the fast reduction machines
      • Registering primitive operations
  • Proof handling
    • Switching on/off the proof editing mode
      • Proof using options
      • Name a set of section hypotheses for Proof using
      • Proof modes
    • Navigation in the proof tree
      • Bullets
      • Mandatory Bullets
      • Set Bullet Behavior
    • Requesting information
    • Showing differences between proof steps
      • How to enable diffs
      • How diffs are calculated
    • Controlling the effect of proof editing commands
    • Controlling memory usage
  • Tactics
    • Common elements of tactics
      • Invocation of tactics
      • Bindings list
      • Intro patterns
      • Occurrence sets and occurrence clauses
    • Applying theorems
    • Managing the local context
    • Controlling the proof flow
    • Case analysis and induction
    • Rewriting expressions
    • Performing computations
      • Conversion tactics applied to hypotheses
    • Automation
    • Controlling automation
      • The hints databases for auto and eauto
        • Creating Hint databases
      • Hint databases defined in the Coq standard library
      • Hint locality
      • Setting implicit automation tactics
    • Decision procedures
    • Checking properties of terms
    • Equality
    • Equality and inductive sets
    • Inversion
    • Classical tactics
    • Automating
    • Non-logical tactics
    • Delaying solving unification constraints
    • Proof maintenance
    • Performance-oriented tactic variants
  • Ltac
    • 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
      • Defining Ltac functions
      • Printing Ltac tactics
    • Examples of using Ltac
      • Proof that the natural numbers have at least two elements
      • Proving that a list is a permutation of a second list
      • Deciding intuitionistic propositional logic
      • Deciding type isomorphisms
    • Debugging Ltac tactics
      • Backtraces
      • Info trace
      • Interactive debugger
      • Profiling Ltac tactics
      • Run-time optimization tactic
  • Ltac2
    • General design
    • ML component
      • Overview
      • Type Syntax
      • Type declarations
      • Term Syntax
      • Ltac Definitions
      • Reduction
      • Typing
      • Effects
        • Standard IO
        • Fatal errors
        • Backtracking
        • Goals
    • Meta-programming
      • Overview
      • Generic Syntax for Quotations
        • Built-in quotations
        • Strict vs. non-strict mode
      • Term Antiquotations
        • Syntax
        • Semantics
      • Match over terms
      • Match over goals
    • Notations
      • Scopes
      • Notations
      • Abbreviations
    • Evaluation
    • Debug
    • Compatibility layer with Ltac1
      • Ltac1 from Ltac2
        • Simple API
        • Low-level API
      • Ltac2 from Ltac1
      • Switching between Ltac languages
    • Transition from Ltac1
      • Syntax changes
      • Tactic delay
      • Variable binding
        • In Ltac expressions
        • In quotations
      • Exception catching
  • Detailed examples of tactics
    • dependent induction
      • A larger example
    • autorewrite
  • The SSReflect proof language
    • Introduction
      • Acknowledgments
    • Usage
      • Getting started
      • Compatibility issues
    • Gallina extensions
      • Pattern assignment
      • Pattern conditional
      • Parametric polymorphism
      • Anonymous arguments
      • Wildcards
      • Definitions
      • Abbreviations
        • Matching
        • Occurrence selection
      • Basic localization
    • Basic tactics
      • Bookkeeping
      • The defective tactics
        • The move tactic.
        • The case tactic
        • The elim tactic
        • The apply tactic
      • Discharge
        • Clear rules
        • Matching for apply and exact
        • The abstract tactic
      • Introduction in the context
        • Simplification items
        • Views
        • Intro patterns
        • Clear switch
        • Branching and destructuring
        • Block introduction
      • Generation of equations
      • Type families
    • Control flow
      • Indentation and bullets
      • Terminators
      • Selectors
      • Iteration
      • Localization
      • Structure
        • The have tactic.
        • Generating let in context entries with have
        • The have tactic and typeclass resolution
        • Variants: the suff and wlog tactics
    • 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
        • The under tactic
        • Interactive mode
        • One-liner mode
      • Locking, unlocking
      • Congruence
    • Contextual patterns
      • Syntax
      • Matching contextual patterns
      • Examples
        • Contextual pattern in set and the : tactical
        • Contextual patterns in rewrite
      • Patterns for recurrent contexts
    • Views and reflection
      • Interpreting eliminations
      • Interpreting assumptions
        • Specializing assumptions
      • Interpreting goals
      • Boolean reflection
      • The reflect predicate
      • General mechanism for interpreting goals and assumptions
        • Specializing assumptions
        • Interpreting assumptions
      • Interpreting equivalences
      • Declaring new Hint Views
      • Multiple views
    • SSReflect searching tool
    • Synopsis and Index
      • Parameters
      • Items and switches
      • Tactics
      • Tacticals
      • Commands
      • Settings

User extensions

  • 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 information about notations
      • Locating notations
      • 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 not bound in the notation
      • Notations with recursive patterns
      • Notations with recursive patterns involving binders
      • Predefined entries
      • Custom entries
      • Summary
        • Syntax of notations
        • Persistence of notations
    • Interpretation scopes
      • Global interpretation rules for notations
      • Local interpretation rules for notations
        • Local opening of an interpretation scope
        • Binding arguments of a constant to an interpretation scope
        • Binding types of arguments to an interpretation scope
      • The type_scope interpretation scope
      • The function_scope interpretation scope
      • Interpretation scopes used in the standard library of Coq
      • Displaying information about scopes
    • Abbreviations
    • Numeral notations
    • String notations
    • Tactic Notations
  • Proof schemes
    • Generation of induction principles with Scheme
      • Automatic declaration of schemes
      • Combined Scheme
    • Generation of induction principles with Functional Scheme
    • Generation of inversion principles with Derive Inversion

Practical tools

  • The Coq commands
    • Interactive use (coqtop)
    • Batch compilation (coqc)
    • Customization at launch time
      • By resource file
      • By environment variables
      • By command line options
    • Compiled interfaces (produced using -vos)
    • Compiled libraries checker (coqchk)
  • Utilities
    • Using Coq as a library
    • Building a Coq project
      • Building a Coq project with coq_makefile
        • CoqMakefile.local
        • Timing targets and performance testing
        • Reusing/extending the generated Makefile
        • Building a subset of the targets with -j
      • Building a Coq project with Dune
    • Computing Module dependencies
    • Documenting Coq files with coqdoc
      • Principles
        • Coq material inside documentation.
        • Pretty-printing.
        • Sections
        • Lists.
        • Rules.
        • Emphasis.
        • Escaping to LaTeX and HTML.
        • Verbatim
        • Hyperlinks
        • Hiding / Showing parts of the source.
      • Usage
        • Command line options
      • The coqdoc LaTeX style file
    • Embedded Coq phrases inside LaTeX documents
    • Man pages
  • Coq Integrated Development Environment
    • Managing files and buffers, basic editing
    • Interactive navigation into Coq scripts
    • Vernacular commands, templates
    • Queries
    • Compilation
    • Customizations
    • Using Unicode symbols
      • Displaying Unicode symbols
      • Bindings for input of Unicode symbols
      • Adding custom bindings
      • Character encoding for saved files

Addendum

  • Extended pattern matching
    • Patterns
    • Multiple patterns
    • Aliasing subpatterns
    • Nested patterns
    • Disjunctive patterns
    • About patterns of parametric types
      • Parameters in patterns
    • Implicit arguments in patterns
    • Matching objects of dependent types
    • Understanding dependencies in patterns
    • When the elimination predicate must be provided
      • Dependent pattern matching
      • Multiple dependent pattern matching
      • Patterns in in
    • 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
    • General Presentation
    • Classes
    • Coercions
    • Identity Coercions
    • Inheritance Graph
    • Declaring Coercions
    • Displaying Available Coercions
    • Activating the Printing of Coercions
    • Classes as Records
    • Coercions and Sections
    • Coercions and Modules
    • Examples
      • Coercion at function application
      • Coercion to a type
      • Coercion to a function
  • Canonical Structures
    • Notation overloading
      • Derived Canonical Structures
    • Hierarchy of structures
      • Compact declaration of Canonical Structures
  • Typeclasses
    • Class and Instance declarations
    • Binding classes
    • Parameterized Instances
    • Sections and contexts
    • Building hierarchies
      • Superclasses
      • Substructures
    • Summary of the commands
      • Typeclasses Transparent, Typeclasses Opaque
      • Settings
      • Typeclasses eauto :=
  • Omega: a solver for quantifier-free problems in Presburger Arithmetic
    • Description of omega
    • Arithmetical goals recognized by omega
    • Messages from omega
    • Using omega
    • Options
    • Technical data
      • Overview of the tactic
      • Overview of the OMEGA decision procedure
    • Bugs
  • 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
      • High level view of lia
      • Cutting plane proofs
      • Case split
    • 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
    • zify: pre-processing of arithmetic goals
  • Extraction of programs in OCaml and Haskell
    • Generating ML Code
    • Extraction Options
      • Setting the target language
      • Inlining and optimizations
      • Extra elimination of useless arguments
      • Realizing axioms
      • Realizing inductive types
      • Avoiding conflicts with existing filenames
      • Additional settings
    • Differences between Coq and ML type systems
    • Some examples
      • A detailed example: Euclidean division
      • Extraction's horror museum
      • Users' Contributions
  • Program
    • Elaborating programs
      • Syntactic control over equalities
      • Program Definition
      • Program Fixpoint
      • Program Lemma
    • Solving obligations
    • Frequently Asked Questions
  • The ring and field tactic families
    • What does this tactic do?
    • The variables map
    • Is it automatic?
    • Concrete usage in Coq
    • Adding a ring structure
    • How does it work?
    • Dealing with fields
    • Adding a new field structure
    • History of ring
    • Discussion
  • Nsatz: tactics for proving equalities in integral domains
    • More about nsatz
  • Generalized rewriting
    • Introduction to generalized rewriting
      • Relations and morphisms
      • Adding new relations and morphisms
      • Rewriting and non reflexive relations
      • Rewriting and non symmetric relations
      • Rewriting in ambiguous setoid contexts
    • Commands and tactics
      • First class setoids and morphisms
      • Tactics enabled on user provided relations
      • Printing relations and morphisms
      • Deprecated syntax and backward incompatibilities
    • Extensions
      • Rewriting under binders
      • Subrelations
      • Constant unfolding
    • Strategies for rewriting
      • Definitions
      • Usage
  • Asynchronous and Parallel Proof Processing
    • Proof annotations
      • Automatic suggestion of proof annotations
    • Proof blocks and error resilience
      • Caveats
    • Interactive mode
      • Caveats
    • Batch mode
    • Limiting the number of parallel workers
  • Miscellaneous extensions
    • Program derivation
  • Polymorphic Universes
    • General Presentation
    • Polymorphic, Monomorphic
    • Cumulative, NonCumulative
      • An example of a proof using cumulativity
    • Cumulativity Weak Constraints
    • Global and local universes
    • Conversion and unification
    • Minimization
    • Explicit Universes
      • Polymorphic definitions
    • Universe polymorphism and sections
  • SProp (proof irrelevant propositions)
    • Basic constructs
    • Encodings for strict propositions
    • Issues with non-cumulativity

Reference

  • Bibliography
Coq
  • Docs »
  • Search
  • Edit on GitHub

© Copyright 1999-2020, Inria, CNRS and contributors.

Built with Sphinx using a theme provided by Read the Docs.