• Home
• About Coq
• Get Coq
• Documentation
• Community

The Coq Proof Assistant

• Introduction
  • How to read this book
  • List of additional documentation
• 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

Part I The language

• Chapter 1  The Gallina specification language
  • 1.1  Lexical conventions
  • 1.2  Terms
  • 1.3  The Vernacular
• Chapter 2  Extensions of Gallina
  • 2.1  Record types
  • 2.2  Variants and extensions of match
  • 2.3  Advanced recursive functions
  • 2.4  Section mechanism
  • 2.5  Module system
  • 2.6  Libraries and qualified names
  • 2.7  Implicit arguments
  • 2.8  Coercions
  • 2.9  Printing constructions in full
  • 2.10  Printing universes
  • 2.11  Existential variables
• Chapter 3  The Coq library
  • 3.1  The basic library
  • 3.2  The standard library
  • 3.3  Users’ contributions
• Chapter 4  Calculus of Inductive Constructions
  • 4.1  The terms
  • 4.2  Typing rules
  • 4.3  Conversion rules
  • 4.4  Subtyping rules
  • 4.5  Inductive definitions
  • 4.6  Admissible rules for global environments
  • 4.7  Co-inductive types
  • 4.8  The Calculus of Inductive Construction with impredicative Set
• Chapter 5  The Module System
  • 5.1  Modules and module types
  • 5.2  Typing Modules

Part II The proof engine

• Chapter 6  Vernacular commands
  • 6.1  Displaying
  • 6.2  Flags, Options and Tables
  • 6.3  Requests to the environment
  • 6.4  Loading files
  • 6.5  Compiled files
  • 6.6  Loadpath
  • 6.7  Backtracking
  • 6.8  Quitting and debugging
  • 6.9  Controlling display
  • 6.10  Controlling the reduction strategies and the conversion algorithm
  • 6.11  Controlling the locality of commands
• Chapter 7  Proof handling
  • 7.1  Switching on/off the proof editing mode
  • 7.2  Navigation in the proof tree
  • 7.3  Requesting information
  • 7.4  Controlling the effect of proof editing commands
  • 7.5  Controlling memory usage
• Chapter 8  Tactics
  • 8.1  Invocation of tactics
  • 8.2  Applying theorems
  • 8.3  Managing the local context
  • 8.4  Controlling the proof flow
  • 8.5  Case analysis and induction
  • 8.6  Rewriting expressions
  • 8.7  Performing computations
  • 8.8  Automation
  • 8.9  Controlling automation
  • 8.10  Decision procedures
  • 8.11  Everything after this point has yet to be sorted
  • 8.12  Equality
  • 8.13  Equality and inductive sets
  • 8.14  Inversion
  • 8.15  Classical tactics
  • 8.16  Automatizing
  • 8.17  Non-logical tactics
  • 8.18  Simple tactic macros
• Chapter 9  The tactic language
  • 9.1  Syntax
  • 9.2  Semantics
  • 9.3  Tactic toplevel definitions
  • 9.4  Debugging L_tac tactics
• Chapter 10  Detailed examples of tactics
  • 10.1  dependent induction
  • 10.2  autorewrite
  • 10.3  quote
  • 10.4  Using the tactical language
• Chapter 11  The Mathematical Proof Language
  • 11.1  Introduction
  • 11.2  Syntax
  • 11.3  Language description
  • 11.4  More details and Formal Semantics

Part III User extensions

• Chapter 12  Syntax extensions and interpretation scopes
  • 12.1  Notations
  • 12.2  Interpretation scopes
  • 12.3  Abbreviations
  • 12.4  Tactic Notations
• Chapter 13  Proof schemes
  • 13.1  Generation of induction principles with Scheme
  • 13.2  Generation of induction principles with Functional Scheme
  • 13.3  Generation of inversion principles with Derive Inversion

Part IV Practical tools

• Chapter 14  The Coq commands
  • 14.1  Interactive use (coqtop)
  • 14.2  Batch compilation (coqc)
  • 14.3  Customization
  • 14.4  Compiled libraries checker (coqchk)
• Chapter 15  Utilities
  • 15.1  Building a toplevel extended with user tactics
  • 15.2  Modules dependencies
  • 15.3  Creating a Makefile for Coq modules
  • 15.4  Documenting Coq files with coqdoc
  • 15.5  Embedded Coq phrases inside L^AT_EX documents
  • 15.6  Coq and GNU Emacs
  • 15.7  Module specification
  • 15.8  Man pages
• Chapter 16  Coq Integrated Development Environment
  • 16.1  Managing files and buffers, basic edition
  • 16.2  Interactive navigation into Coq scripts
  • 16.3  Try tactics automatically
  • 16.4  Proof folding
  • 16.5  Vernacular commands, templates
  • 16.6  Queries
  • 16.7  Compilation
  • 16.8  Customizations
  • 16.9  Using Unicode symbols

Part V Addendum to the Reference Manual

• Presentation of the Addendum
• Chapter 17  Extended pattern-matching
  • 17.1  Patterns
  • 17.2  About patterns of parametric types
  • 17.3  Matching objects of dependent types
  • 17.4  Using pattern matching to write proofs
  • 17.5  Pattern-matching on inductive objects involving local definitions
  • 17.6  Pattern-matching and coercions
  • 17.7  When does the expansion strategy fail ?
• Chapter 18  Implicit Coercions
  • 18.1  General Presentation
  • 18.2  Classes
  • 18.3  Coercions
  • 18.4  Identity Coercions
  • 18.5  Inheritance Graph
  • 18.6  Declaration of Coercions
  • 18.7  Displaying Available Coercions
  • 18.8  Activating the Printing of Coercions
  • 18.9  Classes as Records
  • 18.10  Coercions and Sections
  • 18.11  Coercions and Modules
  • 18.12  Examples
• Chapter 19  Canonical Structures
  • 19.1  Notation overloading
  • 19.2  Hierarchy of structures
• Chapter 20  Type Classes
  • 20.1  Class and Instance declarations
  • 20.2  Binding classes
  • 20.3  Parameterized Instances
  • 20.4  Sections and contexts
  • 20.5  Building hierarchies
  • 20.6  Summary of the commands
• Chapter 21  Omega: a solver of quantifier-free problems in Presburger Arithmetic
  • 21.1  Description of omega
  • 21.2  Using omega
  • 21.3  Technical data
  • 21.4  Bugs
• Chapter 22  Micromega: tactics for solving arithmetic goals over ordered rings
  • 22.1  Short description of the tactics
  • 22.2  Positivstellensatz refutations
  • 22.3  lra: a decision procedure for linear real and rational arithmetic
  • 22.4  lia: a tactic for linear integer arithmetic
  • 22.5  nra: a proof procedure for non-linear arithmetic
  • 22.6  nia: a proof procedure for non-linear integer arithmetic
  • 22.7  psatz: a proof procedure for non-linear arithmetic
• Chapter 23  Extraction of programs in Objective Caml and Haskell
  • 23.1  Generating ML code
  • 23.2  Extraction options
  • 23.3  Differences between Coq and ML type systems
  • 23.4  Some examples
• Chapter 24  Program
  • 24.1  Elaborating programs
  • 24.2  Solving obligations
  • 24.3  Frequently Asked Questions
• Chapter 25  The ring and field tactic families
  • 25.1  What does this tactic do?
  • 25.2  The variables map
  • 25.3  Is it automatic?
  • 25.4  Concrete usage in Coq
  • 25.5  Adding a ring structure
  • 25.6  How does it work?
  • 25.7  Dealing with fields
  • 25.8  Adding a new field structure
  • 25.9  History of ring
  • 25.10  Discussion
• Chapter 26  Nsatz: tactics for proving equalities in integral domains
  • 26.1  Using the basic tactic nsatz
  • 26.2  More about nsatz
• Chapter 27  Generalized rewriting
  • 27.1  Introduction to generalized rewriting
  • 27.2  Commands and tactics
  • 27.3  Extensions
  • 27.4  Strategies for rewriting
• Chapter 28  Asynchronous and Parallel Proof Processing
  • 28.1  Proof annotations
  • 28.2  Proof blocks and error resilience
  • 28.3  Interactive mode
  • 28.4  Batch mode
  • 28.5  Limiting the number of parallel workers
• Chapter 29  Polymorphic Universes
  • 29.1  General Presentation
  • 29.2  Polymorphic, Monomorphic
  • 29.3  Global and local universes
  • 29.4  Conversion and unification
  • 29.5  Minimization
  • 29.6  Explicit Universes
• Chapter 30  Miscellaneous extensions
  • 30.1  Program derivation
• References
• Global Index
• Tactics Index
• Vernacular Commands Index
• Vernacular Options Index
• Index of Error Messages

Navigation

• Cover
• Table of contents
• Index
  • General
  • Commands
  • Options
  • Tactics
  • Errors

• webmaster
• xhtml valid
• CSS valid

This document was translated from L^AT_EX by H^EV^EA.