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

1 A Brief Overview......Page 1
1.1 Expressions, Types, & Functions......Page 2
1.5 A Sorting Example......Page 5
1.7 Contents of This Book......Page 9
2.2.1 Simple Types......Page 17
1.2 Propositions & Proofs......Page 3
1.3 Propositions & Types......Page 4
1.5.2 The Relation "to have the same elements"......Page 6
1.5.4 An Auxiliary Function......Page 7
1.5.5 The Main Sorting Function......Page 8
1.8 Lexical Conventions......Page 11
2.1 First Steps......Page 13
2.1.2 Interpretation Scopes......Page 14
2.1.3 Type Checking......Page 15
2.2.2 Identifiers, Environments, Contexts......Page 18
2.2.3 Expressions & Their Types......Page 20
2.2.4 Free & Bound Variables; alpha-conversion......Page 27
2.3.1 Global Declarations & Definitions......Page 29
2.3.2 Sections & Local Variables......Page 30
2.4 Computing......Page 33
2.4.2 Reduction Rules......Page 34
2.4.3 Reduction Sequences......Page 36
2.5.1 The Set Sort......Page 37
2.5.2 Universes......Page 38
2.5.3 Definitions & Declarations of Specifications......Page 39
2.6 Realizing Specifications......Page 67
3 Propositions & Proofs......Page 69
3.1.1 The World of Propositions & Proofs......Page 71
3.1.2 Goals & Tactics......Page 72
3.1.3 A First Goal-directed Proof......Page 73
3.2.1 Proposition Building Rules......Page 77
3.2.2 Inference Rules & Tactics......Page 78
3.3 Structure of an Interactive Proof......Page 82
3.3.3 Undoing......Page 83
3.4 Proof Irrelevance......Page 84
3.4.2 Are Tactics Helpful for Building Programs?......Page 85
3.5 Sections & Proofs......Page 86
3.6.1 Tacticals......Page 87
3.6.2 Maintenance Issues......Page 91
3.7.1 A Complete Set of Tactics......Page 93
3.8.1 The cut & assert Tactics......Page 94
3.8.2 An Introduction to Automatic Tactics......Page 96
3.9 A New Kind of Abstraction......Page 97
4 Dependent Products, or Pandora's Box......Page 99
4.1.1 Extending the Scope of Arrows......Page 100
4.1.2 On Binding......Page 104
4.1.3 A New Construct......Page 105
4.2.1 The Application Typing Rule......Page 107
4.2.2 The Abstraction Typing Rule......Page 110
4.2.3 Type Inference......Page 112
4.2.5 Dependent Products & the Convertibility Order......Page 116
4.3.1 Formation Rule for Products......Page 117
4.3.2 Dependent Types......Page 118
4.3.3 Polymorphism......Page 120
4.3.4 Equality in the Coq System......Page 124
4.3.5 Higher-Order Types......Page 125
5.1.1 exact & assumption......Page 131
5.1.2 The intro Tactic......Page 132
5.1.3 The apply Tactic......Page 134
5.1.4 The unfold Tactic......Page 141
5.2.1 Introduction & Elimination Rules......Page 142
5.2.2 Using Contradictions......Page 144
5.2.3 Negation......Page 145
5.2.4 Conjunction & Disjunction......Page 147
5.2.6 Existential Quantification......Page 149
5.3.1 Proving Equalities......Page 150
5.3.2 Using Equality: Rewriting Tactics......Page 151
5.3.3 * The pattern Tactic......Page 153
5.3.4 * Conditional Rewriting......Page 154
5.3.6 Other Tactics on Equality......Page 155
5.5.2 True & False......Page 156
5.5.3 Leibniz Equality......Page 157
5.5.4 Some Other Connectives & Quantifiers......Page 159
5.5.5 A Guideline for Impredicative Definitions......Page 161
6.1.1 Enumerated Types......Page 163
6.1.2 Simple Reasoning & Computing......Page 165
6.1.3 The elim Tactic......Page 167
6.1.4 Pattern Matching......Page 168
6.1.5 Record Types......Page 171
6.1.6 Records with Variants......Page 172
6.2.1 The case Tactic......Page 174
6.2.2 Contradictory Equalities......Page 177
6.2.3 Injective Constructors......Page 179
6.2.5 * Guidelines for the case Tactic......Page 182
6.3 Recursive Types......Page 186
6.3.1 Natural Numbers as an Inductive Type......Page 187
6.3.2 Proof by Induction on Natural Numbers......Page 188
6.3.3 Recursive Programming......Page 190
6.3.4 Variations in the Form of Constructors......Page 193
6.3.5 ** Types with Functional Fields......Page 196
6.3.6 Proofs on Recursive Functions......Page 198
6.3.7 Anonymous Recursive Functions (fix)......Page 200
6.4.1 Polymorphic Lists......Page 201
6.4.2 The option Type......Page 203
6.4.3 The Type of Pairs......Page 205
6.5.1 First-Order Data as Parameters......Page 206
6.5.2 Variably Dependent Inductive Types......Page 207
6.6.1 Non-dependent Empty Types......Page 210
6.6.2 Dependence & Empty Types......Page 211
7.1.1 Case-by-Case Analysis & Recursion......Page 213
7.1.2 Conversions......Page 214
7.2 Tactics auto & eauto......Page 216
7.2.1 Tactic Database Handling: Hint......Page 217
7.3.1 The auto rewrite Tactic......Page 220
7.3.2 The subst Tactic......Page 221
7.4.1 The ring Tactic......Page 222
7.4.2 The omega Tactic......Page 224
7.4.3 The field Tactic......Page 225
7.5 Other Decision Procedures......Page 226
7.6 ** The Tactic Definition Language......Page 227
7.6.1 Arguments in Tactics......Page 228
7.6.2 Pattern Matching......Page 229
7.6.3 Using Reduction in Defined Tactics......Page 236
8.1.1 A Few Examples......Page 237
8.1.2 Inductive Predicates & Logic Programming......Page 239
8.1.3 Advice for Inductive Definitions......Page 240
8.1.4 The Example of Sorted Lists......Page 241
8.2 Inductive Properties & Logical Connectives......Page 243
8.2.2 Representing Contradiction......Page 244
8.2.5 Representing Existential Quantification......Page 245
8.2.7 *** Heterogeneous Equality......Page 246
8.2.8 An Exotic Induction Principle?......Page 251
8.3.1 Structured intros......Page 252
8.3.3 * Induction on Inductive Predicates......Page 253
8.3.4 * Induction on le......Page 255
8.4 * Inductive Relations & Functions......Page 259
8.4.1 Representing the Factorial Function......Page 260
8.4.2 ** Representing the Semantics of a Language......Page 265
8.4.3 ** Proving Semantic Properties......Page 266
8.5.1 Instantiating the Argument......Page 270
8.5.2 Inversion......Page 272
9 * Functions & Their Specifications......Page 277
9.1.1 The "Subset" Type......Page 278
9.1.3 Certified Disjoint Sum......Page 280
9.2 Strong Specifications......Page 282
9.2.2 Building Functions as Proofs......Page 283
9.2.3 Preconditions for Partial Functions......Page 284
9.2.4 ** Proving Preconditions......Page 285
9.2.5 ** Reinforcing Specifications......Page 286
9.2.6 *** Minimal Specification Strengthening......Page 287
9.2.7 The refine Tactic......Page 291
9.3.1 Structural Recursion with Multiple Steps......Page 293
9.3.3 Recursive Functions with Several Arguments......Page 297
9.4.1 Weakly Specified Division......Page 302
9.4.2 Well-specified Binary Division......Page 307
10.1 Extracting Toward Functional Languages......Page 311
10.1.1 The Extraction Command......Page 312
10.1.2 The Extraction Mechanism......Page 313
10.1.3 Prop, Set, & Extraction......Page 321
10.2.1 The Why Tool......Page 323
10.2.2 *** The Inner Workings of Why......Page 326
11.1.1 The Data Structure......Page 335
11.1.3 Describing Search Trees......Page 337
11.2.2 Inserting a Number......Page 339
11.2.3 ** Removing a Number......Page 340
11.4.1 Realizing the Occurrence Test......Page 341
11.4.2 Insertion......Page 344
11.4.3 Removing Elements......Page 348
11.5 Possible Improvements......Page 349
11.6 Another Example......Page 350
12 * The Module System......Page 351
12.1 Signatures......Page 352
12.2.1 Building a Module......Page 354
12.2.2 An Example: Keys......Page 355
12.2.3 Parametric Modules (Functors)......Page 358
12.3.1 Enriching a Theory with a Functor......Page 361
12.3.2 Lexicographic Order as a Functor......Page 363
12.4 A Dictionary Module......Page 365
12.4.3 A Trivial Implementation......Page 366
12.4.4 An Efficient Implementation......Page 368
12.5 Conclusion......Page 371
13.1.1 The Colnductive Command......Page 373
13.1.3 Infinite Lists (Streams)......Page 374
13.1.5 Lazy Binary Trees......Page 375
13.2.2 Pattern Matching......Page 376
13.3 Building Infinite Objects......Page 377
13.3.2 The CoFixpoint Command......Page 378
13.3.3 A Few Co-recursive Functions......Page 380
13.3.4 Badly Formed Definitions......Page 382
13.4 Unfolding Techniques......Page 383
13.4.2 Applying the Decomposition Lemma......Page 384
13.4.3 Simplifying a Call to a Co-recursive Function......Page 385
13.5 Inductive Predicates over Co-inductive Types......Page 387
13.6 Co-inductive Predicates......Page 388
13.6.2 Building Infinite Proofs......Page 389
13.6.3 Guard Condition Violation......Page 391
13.6.4 Elimination Techniques......Page 392
13.7.1 The bisimilar Predicate......Page 394
13.7.2 Using Bisimilarity......Page 396
13.8 The Park Principle......Page 397
13.9 LTL......Page 398
13.10.1 Automata & Traces......Page 401
13.11 Conclusion......Page 402
14.1.1 The Inductive Type......Page 403
14.1.2 The Constructors......Page 405
14.1.3 Building the Induction Principle......Page 408
14.1.4 Typing Recursors......Page 411
14.1.5 Induction Principles for Predicates......Page 418
14.2 *** Pattern Matching & Recursion on Proofs......Page 420
14.2.1 Restrictions on Pattern Matching......Page 421
14.2.2 Relaxing the Restrictions......Page 422
14.2.3 Recursion......Page 424
14.3.1 Trees & Forests......Page 426
14.3.2 Proofs by Mutual Induction......Page 428
14.3.3 *** Trees & Tree Lists......Page 430
15 * General Recursion......Page 433
15.1 Bounded Recursion......Page 434
15.2.2 Accessibility Proofs......Page 437
15.2.3 Assembling Well-founded Relations......Page 439
15.2.5 The Recursor well_founded_induction......Page 440
15.2.6 Well-founded Euclidean Division......Page 441
15.2.7 Nested Recursion......Page 445
15.3 ** General Recursion by Iteration......Page 446
15.3.2 Termination Proof......Page 447
15.3.4 Proving the Fixpoint Equation......Page 450
15.3.5 Using the Fixpoint Equation......Page 452
15.4 *** Recursion on an Ad Hoc Predicate......Page 453
15.4.2 Inversion Theorems......Page 454
15.4.3 Defining the Function......Page 455
15.4.4 Proving Properties of the Function......Page 456
16.1 General Presentation......Page 459
16.2 Direct Computation Proofs......Page 461
16.3.1 Proofs Modulo Associativity......Page 464
16.3.2 Making the Type & the Operator More Generic......Page 468
16.3.3 *** Commutativity: Sorting Variables......Page 471
16.4 Conclusion......Page 473
Insertion Sort......Page 475
References......Page 479
Index......Page 485
Coq & Its Libraries......Page 486
Examples from the Book......Page 490
Monographs in Theoretical Computer Science · An EA TCS Series......Page 496
Texts in Theoretical Computer Science · An EA TCS Series......Page 497