9 Dependent Data Structures 165
9.1 More Length-Indexed Lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . 165
9.2 Heterogeneous Lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 169
9.2.1 A Lambda Calculus Interpreter . . . . . . . . . . . . . . . . . . . . . 171
9.3 Recursive Type Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 173
9.4 Data Structures as Index Functions . . . . . . . . . . . . . . . . . . . . . . . 175
9.4.1 Another Interpreter Example . . . . . . . . . . . . . . . . . . . . . . 179
9.5 Choosing Between Representations . . . . . . . . . . . . . . . . . . . . . . . 183
10 Reasoning About Equality Proofs 185
10.1 The Definitional Equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . 185
10.2 Heterogeneous Lists Revisited . . . . . . . . . . . . . . . . . . . . . . . . . . 189
10.3 Type-Casts in Theorem Statements . . . . . . . . . . . . . . . . . . . . . . . 194
10.4 Heterogeneous Equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 199
10.5 Equivalence of Equality Axioms . . . . . . . . . . . . . . . . . . . . . . . . . 204
10.6 Equality of Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 205
11 Generic Programming 208
11.1 Reifying Datatype Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . 208
11.2 Recursive Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 210
11.2.1 Pretty-Printing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 213
11.2.2 Mapping . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 216
11.3 Proving Theorems about Recursive Definitions . . . . . . . . . . . . . . . . . 217
12 Universes and Axioms 224
12.1 The Type Hierarchy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 224
12.1.1 Inductive Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . 227
12.1.2 Deciphering Baffling Messages About Inability to Unify . . . . . . . . 231
12.2 The Prop Universe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 233
12.3 Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 236
12.3.1 The Basics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 237
12.3.2 Axioms of Choice . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 241
12.3.3 Axioms and Computation . . . . . . . . . . . . . . . . . . . . . . . . 243
12.3.4 Methods for Avoiding Axioms . . . . . . . . . . . . . . . . . . . . . . 244
III Proof Engineering 253
13 Proof Search by Logic Programming 254
13.1 Introducing Logic Programming . . . . . . . . . . . . . . . . . . . . . . . . . 254
13.2 Searching for Underconstrained Values . . . . . . . . . . . . . . . . . . . . . 261
13.3 Synthesizing Programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 264
13.4 More on auto Hints . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 268
4
