• 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

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
• 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  Coinductive 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  Options and Flags
  • 6.3  Requests to the environment
  • 6.4  Loading files
  • 6.5  Compiled files
  • 6.6  Loadpath
  • 6.7  States and Reset
  • 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
• Chapter 8  Tactics
  • 8.1  Invocation of tactics
  • 8.2  Explicit proof as a term
  • 8.3  Basics
  • 8.4  Negation and contradiction
  • 8.5  Conversion tactics
  • 8.6  Introductions
  • 8.7  Induction and Case Analysis
  • 8.8  Equality
  • 8.9  Equality and inductive sets
  • 8.10  Inversion
  • 8.11  Classical tactics
  • 8.12  Automatizing
  • 8.13  Controlling automation
  • 8.14  Generation of induction principles with Scheme
  • 8.15  Generation of induction principles with Functional Scheme
  • 8.16  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  refine
  • 10.2  eapply
  • 10.3  Scheme
  • 10.4  Functional Scheme and functional induction
  • 10.5  inversion
  • 10.6  dependent induction
  • 10.7  autorewrite
  • 10.8  quote
  • 10.9  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

Part IV Practical tools

• Chapter 13  The Coq commands
  • 13.1  Interactive use (coqtop)
  • 13.2  Batch compilation (coqc)
  • 13.3  Resource file
  • 13.4  Environment variables
  • 13.5  Options
  • 13.6  Compiled libraries checker (coqchk)
• Chapter 14  Utilities
  • 14.1  Building a toplevel extended with user tactics
  • 14.2  Modules dependencies
  • 14.3  Creating a Makefile for Coq modules
  • 14.4  Documenting Coq files with coqdoc
  • 14.5  Exporting Coq theories to XML
  • 14.6  Embedded Coq phrases inside L^AT_EX documents
  • 14.7  Coq and GNU Emacs
  • 14.8  Module specification
  • 14.9  Man pages
• Chapter 15  Coq Integrated Development Environment
  • 15.1  Managing files and buffers, basic edition
  • 15.2  Interactive navigation into Coq scripts
  • 15.3  Try tactics automatically
  • 15.4  Proof folding
  • 15.5  Vernacular commands, templates
  • 15.6  Queries
  • 15.7  Compilation
  • 15.8  Customizations
  • 15.9  Using unicode symbols
  • 15.10  Building a custom CoqIDE with user ML code

Part V Addendum to the Reference Manual

• Presentation of the Addendum
• Chapter 16  Extended pattern-matching
  • 16.1  Patterns
  • 16.2  About patterns of parametric types
  • 16.3  Matching objects of dependent types
  • 16.4  Using pattern matching to write proofs
  • 16.5  Pattern-matching on inductive objects involving local definitions
  • 16.6  Pattern-matching and coercions
  • 16.7  When does the expansion strategy fail ?
• Chapter 17  Implicit Coercions
  • 17.1  General Presentation
  • 17.2  Classes
  • 17.3  Coercions
  • 17.4  Identity Coercions
  • 17.5  Inheritance Graph
  • 17.6  Declaration of Coercions
  • 17.7  Displaying Available Coercions
  • 17.8  Activating the Printing of Coercions
  • 17.9  Classes as Records
  • 17.10  Coercions and Sections
  • 17.11  Coercions and Modules
  • 17.12  Examples
• Chapter 18  Type Classes
  • 18.1  Class and Instance declarations
  • 18.2  Binding classes
  • 18.3  Parameterized Instances
  • 18.4  Sections and contexts
  • 18.5  Building hierarchies
  • 18.6  Summary of the commands
• Chapter 19  Omega: a solver of quantifier-free problems in Presburger Arithmetic
  • 19.1  Description of omega
  • 19.2  Using omega
  • 19.3  Technical data
  • 19.4  Bugs
• Chapter 20  Micromega : tactics for solving arithmetics goals over ordered rings
  • 20.1  The psatz tactic in a hurry
  • 20.2  Positivstellensatz refutations
  • 20.3   lia : the linear integer arithmetic tactic
• Chapter 21  Extraction of programs in Objective Caml and Haskell
  • 21.1  Generating ML code
  • 21.2  Extraction options
  • 21.3  Differences between Coq and ML type systems
  • 21.4  Some examples
• Chapter 22  Program
  • 22.1  Elaborating programs
  • 22.2  Solving obligations
  • 22.3  Frequently Asked Questions
• Chapter 23  The ring and field tactic families
  • 23.1  What does this tactic do?
  • 23.2  The variables map
  • 23.3  Is it automatic?
  • 23.4  Concrete usage in Coq
  • 23.5  Adding a ring structure
  • 23.6  How does it work?
  • 23.7  Dealing with fields
  • 23.8  Adding a new field structure
  • 23.9  Legacy implementation
  • 23.10  History of ring
  • 23.11  Discussion
• Chapter 24  Nsatz: tactics for proving equalities in integral domains
  • 24.1  Using the basic tactic nsatz
  • 24.2  More about nsatz
• Chapter 25  User defined equalities and relations
  • 25.1  Relations and morphisms
  • 25.2  Adding new relations and morphisms
  • 25.3  Rewriting and non reflexive relations
  • 25.4  Rewriting and non symmetric relations
  • 25.5  Rewriting in ambiguous setoid contexts
  • 25.6  First class setoids and morphisms
  • 25.7  Tactics enabled on user provided relations
  • 25.8  Printing relations and morphisms
  • 25.9  Deprecated syntax and backward incompatibilities
  • 25.10  Rewriting under binders
  • 25.11  Sub-relations
  • 25.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.