Table of contents
Cover page
Introduction
How to read this book
List of additionnal documentation
Credits
Credits: addendum for version 6.1
Credits: addendum for version 6.2
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
Cases
2.3 Forced type
2.4 Local definitions
2.5 Section mechanism
2.6 Implicit arguments
2.7 Implicit Coercions
Chapter 3: The
Coq
library
3.1 The basic library
3.2 The standard library
3.3 Users' contributions
Chapter 4: The Calculus of Inductive Constructions
4.1 The terms
4.2 Typed terms
4.3 Conversion rules
4.4 Definitions in environments
4.5 Inductive Definitions
4.6 Coinductive types
Part: II
The proof engine
Chapter 5: Vernacular commands
5.1 Displaying
5.2 Requests to the environment
5.3 Loading files
5.4 Compiled files
5.5 Loadpath
5.6 States and Reset
5.7 Syntax facilities
5.8 Miscellaneous
Chapter 6: Proof handling
6.1 Switching on/off the proof editing mode
6.2 Navigation in the proof tree
6.3 Displaying information
Chapter 7: Tactics
7.1 Syntax of tactics and tacticals
7.2 Explicit proof as a term
7.3 Basics
7.4 Negation and contradiction
7.5 Conversion tactics
7.6 Introductions
7.7 Eliminations (Induction and Case Analysis)
7.8 Equality
7.9 Equality and inductive sets
7.10 Inversion
7.11 Automatizing
7.12 Developing certified programs
7.13 The hints databases for Auto and EAuto
7.14 Tacticals
7.15 Generation of induction principles with
Scheme
7.16 Simple tactic macros
Chapter 8: Detailed examples of tactics
8.1
Refine
8.2
EApply
8.3
Scheme
8.4
Inversion
8.5
AutoRewrite
8.6
Quote
Part: III
User extensions
Chapter 9: Syntax extensions
9.1 Abstract syntax trees (AST)
9.2 Extendable grammars
9.3 Writing your own pretty printing rules
Chapter 10: Writing ad-hoc Tactics in Coq
10.1 Introduction
10.2 Tactic Macros
10.3 An Overview of
Coq
's Architecture
10.4 The tactic writer mini-HOWTO
10.5 Some Useful Tools for Writing Tactics
10.6 A Complete Example
10.7 Testing and Debugging your Tactic
Part: IV
Practical tools
Chapter 11: The
Coq
commands
11.1 Interactive use (
coqtop
)
11.2 Batch compilation (
coqc
)
11.3 Resource file
11.4 Environment variables
11.5 Options
Chapter 12: Utilities
12.1 Building a toplevel extended with user tactics
12.2 Modules dependencies
12.3 Creating a
Makefile
for
Coq
modules
12.4
Coq_SearchIsos
: information retrieval in a
Coq
proofs library
12.5
Coq
and L
A
T
E
X
12.6
Coq
and HTML
12.7
Coq
and
GNU Emacs
12.8 Module specification
12.9 Man pages
Presentation of the Addendum
Chapter 13: ML-style pattern-matching
13.1 Patterns
13.2 About patterns of parametric types
13.3 Matching objects of dependent types
13.4 Using pattern matching to write proofs
13.5 When does the expansion strategy fail ?
Chapter 14: Implicit Coercions
14.1 General Presentation
14.2 Classes
14.3 Coercions
14.4 Inheritance Graph
14.5 Commands
14.6 Coercions and Pretty-Printing
14.7 Inheritance Mechanism -- Examples
14.8 Classes as Records
14.9 Coercions and Sections
14.10 Examples
Chapter 15:
Natural
: proofs in natural language
15.1 Introduction
15.2 Activating
Natural
15.3 Customizing
Natural
15.4 Error messages
Chapter 16:
Omega
: a solver of quantifier-free problems in Presburger Arithmetic
16.1 Description of
Omega
16.2 Using
Omega
16.3 Technical data
16.4 Bugs
Chapter 17: The Program Tactic
17.1 Developing certified programs: Motivations
17.2 Using
Program
17.3 Syntax for programs
17.4 Examples
Chapter 18: Proof of imperative programs
18.1 How it works
18.2 Syntax of annotated programs
18.3 Local and global variables
18.4 Function call
18.5 Libraries
18.6 Extraction
18.7 Examples
18.8 Bugs
Chapter 19: Execution of extracted programs in Caml and Haskell
19.1 The
Extraction
module
19.2 Some examples
19.3 Bugs
Chapter 20: The
Ring
tactic
20.1 What does this tactic?
20.2 The variables map
20.3 Is it automatic?
20.4 Concrete usage in
Coq
20.5 Add a ring structure
20.6 How does it work?
20.7 History of
Ring
20.8 Discussion
Bibliography
Global Index
Tactics Index
Vernacular Commands Index
Index of Error Messages