• 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

Part I The language

• The Gallina specification language
  • Lexical conventions
  • Terms
  • The Vernacular
• Extensions of Gallina
  • Record types
  • Variants and extensions of match
  • Advanced recursive functions
  • Section mechanism
  • Module system
  • Libraries and qualified names
  • Implicit arguments
  • Coercions
  • Printing constructions in full
  • Printing universes
• The Coq library
  • The basic library
  • The standard library
  • Users’ contributions
• Calculus of Inductive Constructions
  • The terms
  • Typed terms
  • Conversion rules
  • Derived rules for environments
  • Inductive Definitions
  • Coinductive types
  • Cic: the Calculus of Inductive Construction with impredicative Set
• The Module System
  • Modules and module types
  • Typing Modules

Part II The proof engine

• Vernacular commands
  • Displaying
  • Requests to the environment
  • Loading files
  • Compiled files
  • Loadpath
  • States and Reset
  • Quitting and debugging
  • Controlling display
  • Controlling the reduction strategies and the conversion algorithm
• Proof handling
  • Switching on/off the proof editing mode
  • Navigation in the proof tree
  • Requesting information
• Tactics
  • Invocation of tactics
  • Explicit proof as a term
  • Basics
  • Negation and contradiction
  • Conversion tactics
  • Introductions
  • Induction and Case Analysis
  • Equality
  • Equality and inductive sets
  • Inversion
  • Classical tactics
  • Automatizing
  • Controlling automation
  • Generation of induction principles with Scheme
  • Generation of induction principles with Functional Scheme
  • Simple tactic macros
• The tactic language
  • Syntax
  • Semantics
  • Tactic toplevel definitions
  • Debugging L_tac tactics
• Detailed examples of tactics
  • refine
  • eapply
  • Scheme
  • Functional Scheme and functional induction
  • inversion
  • dependent induction
  • autorewrite
  • quote
  • Using the tactical language
• The C-zar mathematical proof language
  • Introduction
  • Syntax
  • Language description
  • More details and Formal Semantics

Part III User extensions

• Syntax extensions and interpretation scopes
  • Notations
  • Interpretation scopes
  • Abbreviations
  • Tactic Notations

Part IV Practical tools

• The Coq commands
  • Interactive use (coqtop)
  • Batch compilation (coqc)
  • Resource file
  • Environment variables
  • Options
  • Compiled libraries checker (coqchk)
• Utilities
  • Building a toplevel extended with user tactics
  • Modules dependencies
  • Creating a Makefile for Coq modules
  • Documenting Coq files with coqdoc
  • Exporting Coq theories to XML
  • Embedded Coq phrases inside L^AT_EX documents
  • Coq and GNU Emacs
  • Module specification
  • Man pages
• Coq Integrated Development Environment
  • Managing files and buffers, basic edition
  • Interactive navigation into Coq scripts
  • Try tactics automatically
  • Vernacular commands, templates
  • Queries
  • Compilation
  • Customizations
  • Using unicode symbols
  • Building a custom CoqIDE with user ML code

Part V Addendum to the Reference Manual

• Presentation of the Addendum
• Extended pattern-matching
  • Patterns
  • About patterns of parametric types
  • Matching objects of dependent types
  • 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
  • Declaration of Coercions
  • Displaying Available Coercions
  • Activating the Printing of Coercions
  • Classes as Records
  • Coercions and Sections
  • Examples
• Type Classes
  • Class and Instance declarations
  • Binding classes
  • Parameterized Instances
  • Building hierarchies
  • Summary of the commands
• Omega: a solver of quantifier-free problems in Presburger Arithmetic
  • Description of omega
  • Using omega
  • Technical data
  • Bugs
• Micromega : tactics for solving arithmetics goals over ordered rings
  • The psatz tactic in a hurry
  • Positivstellensatz refutations
  • lia : the linear integer arithmetic tactic
• Extraction of programs in Objective Caml and Haskell
  • Generating ML code
  • Extraction options
  • Differences between Coq and ML type systems
  • Some examples
• Program
  • Elaborating programs
  • 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
  • Legacy implementation
  • History of ring
  • Discussion
• User defined equalities and relations
  • Relations and morphisms
  • Adding new relations and morphisms
  • Rewriting and non reflexive relations
  • Rewriting and non symmetric relations
  • Rewriting in ambiguous setoid contexts
  • First class setoids and morphisms
  • Tactics enabled on user provided relations
  • Printing relations and morphisms
  • Deprecated syntax and backward incompatibilities
  • Rewriting under binders
  • Sub-relations
  • Constant unfolding
• Calling external provers
  • The gappa tactic
• References
• Global Index
• Tactics Index
• Vernacular Commands Index
• Index of Error Messages

Navigation

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

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