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
Credits: addendum for version 6.3
Credits: versions 7
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 Section mechanism
2.5 Logical paths of libraries and compilation units
2.6 Qualified names
2.7 Implicit arguments
2.8 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 Derived rules for 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 The hints databases for Auto and EAuto
7.13 Tacticals
7.14 Generation of induction principles with
Scheme
7.15 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: The tactic language
10.1 Syntax
10.2 Semantic
10.3 Examples
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
and L
A
T
E
X
12.5
Coq
and HTML
12.6
Coq
and
GNU Emacs
12.7 Module specification
12.8 Man pages
Presentation of the Addendum
Chapter 13: Extended 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 Pattern-matching on inductive objects involving local definitions
13.6 Pattern-matching and coercions
13.7 When does the expansion strategy fail ?
Chapter 14: Implicit Coercions
14.1 General Presentation
14.2 Classes
14.3 Coercions
14.4 Identity Coercions
14.5 Inheritance Graph
14.6 Declaration of Coercions
14.7 Displaying Available Coercions
14.8 Activating the Printing of Coercions
14.9 Classes as Records
14.10 Coercions and Sections
14.11 Examples
Chapter 15:
Omega
: a solver of quantifier-free problems in Presburger Arithmetic
15.1 Description of
Omega
15.2 Using
Omega
15.3 Technical data
15.4 Bugs
Chapter 16: Proof of imperative programs
16.1 How it works
16.2 Syntax of annotated programs
16.3 Local and global variables
16.4 Function call
16.5 Libraries
16.6 Examples
16.7 Bugs
Chapter 17: Extraction of programs in Objective Caml and Haskell
17.1 Generating ML code
17.2 Extraction options
17.3 Differences between
Coq
and ML type systems
17.4 Some examples
Chapter 18: The
Ring
tactic
18.1 What does this tactic?
18.2 The variables map
18.3 Is it automatic?
18.4 Concrete usage in
Coq
18.5 Add a ring structure
18.6 How does it work?
18.7 History of
Ring
18.8 Discussion
Chapter 19: The
Setoid_replace
tactic
19.1 Description of
Setoid_replace
19.2 Adding new setoid or morphisms
19.3 Adding new morphisms
19.4 The tactic itself
Bibliography
Global Index
Tactics Index
Vernacular Commands Index
Index of Error Messages