• 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

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  Typed terms
  • 4.3  Conversion rules
  • 4.4  Derived rules for environments
  • 4.5  Inductive Definitions
  • 4.6  Co-inductive types
  • 4.7  Cic: 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  State files
  • 6.9  Quitting and debugging
  • 6.10  Controlling display
  • 6.11  Controlling the reduction strategies and the conversion algorithm
  • 6.12  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
• 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  Things that do not fit other sections
  • 8.12  Everything after this point has yet to be sorted
  • 8.13  Equality
  • 8.14  Equality and inductive sets
  • 8.15  Inversion
  • 8.16  Classical tactics
  • 8.17  Automatizing
  • 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  By environment variables
  • 14.5  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  Exporting Coq theories to XML
  • 15.6  Embedded Coq phrases inside L^AT_EX documents
  • 15.7  Coq and GNU Emacs
  • 15.8  Module specification
  • 15.9  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  Type Classes
  • 19.1  Class and Instance declarations
  • 19.2  Binding classes
  • 19.3  Parameterized Instances
  • 19.4  Sections and contexts
  • 19.5  Building hierarchies
  • 19.6  Summary of the commands
• Chapter 20  Omega: a solver of quantifier-free problems in Presburger Arithmetic
  • 20.1  Description of omega
  • 20.2  Using omega
  • 20.3  Technical data
  • 20.4  Bugs
• Chapter 21  Micromega : tactics for solving arithmetic goals over ordered rings
  • 21.1  Short description of the tactics
  • 21.2  Positivstellensatz refutations
  • 21.3  lra : a decision procedure for linear real and rational arithmetic
  • 21.4   psatz : a proof procedure for non-linear arithmetic
  • 21.5   lia : a tactic for linear integer arithmetic
  • 21.6   nia : a proof procedure for non-linear integer arithmetic
• Chapter 22  Extraction of programs in Objective Caml and Haskell
  • 22.1  Generating ML code
  • 22.2  Extraction options
  • 22.3  Differences between Coq and ML type systems
  • 22.4  Some examples
• Chapter 23  Program
  • 23.1  Elaborating programs
  • 23.2  Solving obligations
  • 23.3  Frequently Asked Questions
• Chapter 24  The ring and field tactic families
  • 24.1  What does this tactic do?
  • 24.2  The variables map
  • 24.3  Is it automatic?
  • 24.4  Concrete usage in Coq
  • 24.5  Adding a ring structure
  • 24.6  How does it work?
  • 24.7  Dealing with fields
  • 24.8  Adding a new field structure
  • 24.9  Legacy implementation
  • 24.10  History of ring
  • 24.11  Discussion
• Chapter 25  Nsatz: tactics for proving equalities in integral domains
  • 25.1  Using the basic tactic nsatz
  • 25.2  More about nsatz
• Chapter 26  User defined equalities and relations
  • 26.1  Relations and morphisms
  • 26.2  Adding new relations and morphisms
  • 26.3  Rewriting and non reflexive relations
  • 26.4  Rewriting and non symmetric relations
  • 26.5  Rewriting in ambiguous setoid contexts
  • 26.6  First class setoids and morphisms
  • 26.7  Tactics enabled on user provided relations
  • 26.8  Printing relations and morphisms
  • 26.9  Deprecated syntax and backward incompatibilities
  • 26.10  Rewriting under binders
  • 26.11  Sub-relations
  • 26.12  Constant unfolding
• References
• Global Index
• Tactics Index
• Vernacular Commands Index
• Index of Error Messages

Navigation

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

• webmaster
• xhtml valid
• CSS valid

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