Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions

Front Cover
Springer Science & Business Media, May 14, 2004 - Mathematics - 472 pages

Coq is an interactive proof assistant for the development of mathematical theories and formally certified software. It is based on a theory called the calculus of inductive constructions, a variant of type theory.

This book provides a pragmatic introduction to the development of proofs and certified programs using Coq. With its large collection of examples and exercises it is an invaluable tool for researchers, students, and engineers interested in formal methods and the development of zero-fault software.

 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

A Brief Overview
1
11 Expressions Types and Functions
2
12 Propositions and Proofs
3
13 Propositions and Types
4
14 Specifications and Certified Programs
5
151 Inductive Definitions
6
153 A Specification for a Sorting Program
7
155 The Main Sorting Function
8
814 The Example of Sorted Lists
215
82 Inductive Properties and Logical Connectives
217
821 Representing Truth
218
823 Representing Conjunction
219
826 Representing Equality
220
828 An Exotic Induction Principle?
225
83 Reasoning about Inductive Properties
226
832 The constructor Tactics
227

16 Learning Coq
9
18 Lexical Conventions
11
Types and Expressions
13
211 Terms Expressions Types
14
213 Type Checking
15
22 The Rules of the Game
17
222 Identifiers Environments Contexts
18
223 Expressions and Their Types
20
224 Free and Bound Variables aconversion
27
23 Declarations and Definitions
29
232 Sections and Local Variables
30
24 Computing
33
241 Substitution
34
243 Reduction Sequences
36
244 Convertibility
37
252 Universes
38
253 Definitions and Declarations of Specifications
39
26 Realizing Specifications
41
Propositions and Proofs
43
31 Minimal Propositional Logic
45
312 Goals and Tactics
46
313 A First Goaldirected Proof
47
32 Relating Typing Rules and Tactics
51
322 Inference Rules and Tactics
52
33 Structure of an Interactive Proof
56
331 Activating the Goal Handling System
57
334 Regular End of a Proof
58
341 Theorem Versus Definition
59
35 Sections and Proofs
60
36 Composing Tactics
61
362 Maintenance Issues
65
37 On Completeness for Propositional Logic
67
372 Unprovable Propositions
68
382 An Introduction to Automatic Tactics
70
39 A New Kind of Abstraction
71
Dependent Products or Pandoras Box
73
41 In Praise of Dependence
74
412 On Binding
78
413 A New Construct
79
42 Typing Rules and Dependent Products
81
422 The Abstraction Typing Rule
84
423 Type Inference
86
424 The Conversion Rule
90
43 Expressive power of the Dependent Product
91
432 Dependent Types
92
433 Polymorphism
94
434 Equality in the Coq System
98
435 HigherOrder Types
99
Everyday Logic
105
512 The intro Tactic
106
513 The apply Tactic
108
514 The unfold Tactic
115
52 Logical Connectives
116
522 Using Contradictions
118
523 Negation
119
524 Conjunction and Disjunction
121
525 About the repeat Tactical
123
53 Equality and Rewriting
124
Rewriting Tactics
125
533 The pattern Tactic
127
534 Conditional Rewriting
128
535 Searching Theorems for Rewriting
129
54 Tactic Summary Table
130
553 Leibniz Equality
131
554 Some Other Connectives and Quantifiers
133
555 A Guideline for Impredicative Definitions
135
Inductive Data Types
137
612 Simple Reasoning and Computing
139
613 The elim Tactic
141
614 Pattern Matching
142
615 Record Types
145
616 Records with Variants
146
62 CaseBased Reasoning
148
622 Contradictory Equalities
151
623 Injective Constructors
153
624 Inductive Types and Equality
156
63 Recursive Types
160
631 Natural Numbers as an Inductive Type
161
632 Proof by Induction on Natural Numbers
162
633 Recursive Programming
164
634 Variations in the Form of Constructors
167
635 Types with Functional Fields
170
636 Proofs on Recursive Functions
172
637 Anonymous Recursive Functions fix
174
64 Polymorphic Types
175
642 The option Type
177
643 The Type of Pairs
179
644 The Type of Disjoint Sums
180
652 Variably Dependent Inductive Types
181
66 Empty Types
184
662 Dependence and Empty Types
185
Tactics and Automation
187
712 Conversions
188
72 Tactics auto and eauto
190
Hint
191
722 The eauto Tactic
194
732 The subst Tactic
195
74 Numerical Tactics
196
742 The omega Tactic
198
743 The field Tactic
199
744 The f ourier Tactic
200
76 The Tactic Definition Language
201
761 Arguments in Tactics
202
762 Pattern Matching
203
763 Using Reduction in Defined Tactics
210
Inductive Predicates
211
812 Inductive Predicates and Logic Programming
213
813 Advice for Inductive Definitions
214
834 Induction on le
229
84 Inductive Relations and Functions
233
841 Representing the Factorial Function
234
842 Representing the Semantics of a Language
239
843 Proving Semantic Properties
240
85 Elaborate Behavior of elim
244
852 Inversion
246
Functions and Their Specifications
251
91 Inductive Types for Specifications
252
912 Nested Subset Types
254
914 Hybrid Disjoint Sum
256
921 Wellspecified Functions
257
923 Preconditions for Partial Functions
258
924 Proving Preconditions
259
925 Reinforcing Specifications
260
926 Minimal Specification Strengthening
261
927 The refine Tactic
265
93 Variations on Structural Recursion
267
932 Simplifying the Step
271
94 Binary Division
276
942 Wellspecified Binary Division
281
Extraction and Imperative Programming
285
1011 The Extraction Command
286
1012 The Extraction Mechanism
287
1013 Prop Set and Extraction
295
102 Describing Imperative Programs
297
1022 The Inner Workings of Why
300
A Case Study
309
1112 A Naive Approach to Deciding Occurrence
311
112 Specifying Programs
313
1123 Removing a Number
314
113 Auxiliary Lemmas
315
1142 Insertion
318
1143 Removing Elements
322
115 Possible Improvements
323
116 Another Example
324
The Module System
325
121 Signatures
326
122 Modules
328
Keys
329
1223 Parametric Modules Functors
332
123 A Theory of Decidable Order Relations
335
1232 Lexicographic Order as a Functor
337
124 A Dictionary Module
339
1241 Enriched Implementations
340
1244 An Efficient Implementation
342
125 Conclusion
347
Infinite Objects and Proofs
349
1312 Specific Features of Coinductive Types
350
1314 Lazy Lists
351
132 Techniques for Coinductive Types
352
133 Building Infinite Objects
353
1331 A Failed Attempt
354
1333 A Few Corecursive Functions
356
1334 Badly Formed Definitions
358
134 Unfolding Techniques
359
1341 Systematic Decomposition
360
1343 Simplifying a Call to a Corecursive Function
361
135 Inductive Predicates over Coinductive Types
363
136 Coinductive Predicates
364
1361 A Predicate for Infinite Sequences
365
1363 Guard Condition Violation
367
1364 Elimination Techniques
368
137 Bisimilarity
370
1372 Using Bisimilarity
372
138 The Park Principle
373
139 LTL
374
Transition Systems
377
1311 Conclusion
378
Foundations of Inductive Types
379
1412 The Constructors
381
1413 Building the Induction Principle
384
1414 Typing Recursors
387
1415 Induction Principles for Predicates
394
1416 The Scheme Command
396
1421 Restrictions on Pattern Matching
397
1422 Relaxing the Restrictions
398
1423 Recursion
400
143 Mutually Inductive Types
402
1432 Proofs by Mutual Induction
404
1433 Trees and Tree Lists
406
General Recursion
409
151 Bounded Recursion
410
152 Wellfounded Recursive Functions
413
1523 Assembling Wellfounded Relations
415
1524 Wellfounded Recursion
416
1526 Wellfounded Euclidean Division
417
1527 Nested Recursion
421
153 General Recursion by Iteration
422
1531 The Functional Related to a Recursive Function
423
1533 Building the Actual Function
426
1535 Using the Fixpoint Equation
428
1536 Discussion
429
1541 Defining an Ad Hoc Predicate
430
1543 Defining the Function
431
1544 Proving Properties of the Function
432
Proof by Reflection
435
162 Direct Computation Proofs
437
163 Proof by Algebraic Computation
440
1632 Making the Type and the Operator More Generic
444
Sorting Variables
447
164 Conclusion
449
Insertion Sort
451
References
455
Index
461
Coq and Its Libraries
462
Examples from the Book
466
Copyright

Other editions - View all

Common terms and phrases

Popular passages

Page 456 - ... pages 27-71, Kluwer Academic Publishers, 1988. [7] RL ConStable, SF Allen, HM Bromley, WR Cleaveland, JF Cremer, RW Harper, DJ Howe, TB Knoblock, NP Mendler, P. Panagaden, JT Sasaki, and SF Smith. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall International, 1986. [8] Thierry Coquand. An analysis of Girard's paradox. In Symposium on Logic in Computer Science, pages 227-236, IEEE Computer Society Press, 1986. [9] Thierry Coquand and Gerard Huet. The calculus of...
Page 456 - An axiomatization of linear temporal logic in the calculus of inductive constructions.

Bibliographic information