Table of contents
Table of contents
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 program
7.13 The hints list for Auto and EAuto
7.14 Tacticals
7.15 Generation of induction principles with
Scheme
7.16 A Simple way to define tactic macros
Chapter 8: Detailed examples of tactics
8.1
Refine
8.2
EApply
8.3
Scheme
8.4
Inversion
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 Some Useful Tools for Writing Tactics
10.5 A Complete Example
10.6 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 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
Chapter 15: Execution of extracted programs in Caml and Haskell
15.1 The
Extraction
module
15.2 Some examples
15.3 Bugs
Chapter 16:
Natural
: proofs in natural language
16.1 Introduction
16.2 Activating
Natural
16.3 Customizing
Natural
16.4 Error messages
Chapter 17:
Omega
: a solver of quantifier-free problems in Presburger Arithmetic
17.1 Description of
Omega
17.2 Using
Omega
17.3 Technical data
17.4 Bugs
Chapter 18: The Program Tactic
18.1 Developing certified programs: Motivations
18.2 Using
Program
18.3 Syntax for programs
18.4 Examples
Chapter 19: The
Ring
tactic
19.1 What does this tactic ?
19.2 The variables map
19.3 Is it automatic ?
19.4 Concrete usage in
Coq
19.5 Add a ring structure
19.6 How does it work ?
19.7 History of
Ring
19.8 Discussion about the usage of reflexion
Bibliography
Global Index
Tactics Index
Vernacular Commands Index
Retrieved by Memoweb from
http://pauillac.inria.fr/coq/doc/toc.html
at 8/10/98