Mercurial > cpdt > repo

comparison src/InductiveTypes.v @ 208:b9e9ff52913c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Port InductiveTypes
author Adam Chlipala <adamc@hcoop.net>
date Mon, 09 Nov 2009 11:09:50 -0500
parents f05514cc6c0d
children b149a07b9b5b
comparison
equal deleted inserted replaced
207:a7be5d9a2fd4 208:b9e9ff52913c
33 | tt. 33 | tt.
34 34
35 (** This vernacular command defines a new inductive type [unit] whose only value is [tt], as we can see by checking the types of the two identifiers: *) 35 (** This vernacular command defines a new inductive type [unit] whose only value is [tt], as we can see by checking the types of the two identifiers: *)
36 36
37 Check unit. 37 Check unit.
38 (** [[ 38 (** [unit : Set] *)
39 39
40 unit : Set
41 ]] *)
42 Check tt. 40 Check tt.
43 (** [[ 41 (** [tt : unit] *)
44
45 tt : unit
46 ]] *)
47 42
48 (** We can prove that [unit] is a genuine singleton type. *) 43 (** We can prove that [unit] is a genuine singleton type. *)
49 44
50 Theorem unit_singleton : forall x : unit, x = tt. 45 Theorem unit_singleton : forall x : unit, x = tt.
46
51 (** The important thing about an inductive type is, unsurprisingly, that you can do induction over its values, and induction is the key to proving this theorem. We ask to proceed by induction on the variable [x]. *) 47 (** The important thing about an inductive type is, unsurprisingly, that you can do induction over its values, and induction is the key to proving this theorem. We ask to proceed by induction on the variable [x]. *)
48
52 (* begin thide *) 49 (* begin thide *)
53 induction x. 50 induction x.
54 (** The goal changes to: [[ 51
55 52 (** The goal changes to:
53 [[
56 tt = tt 54 tt = tt
57 ]] *) 55 ]] *)
56
58 (** ...which we can discharge trivially. *) 57 (** ...which we can discharge trivially. *)
58
59 reflexivity. 59 reflexivity.
60 Qed. 60 Qed.
61 (* end thide *) 61 (* end thide *)
62 62
63 (** It seems kind of odd to write a proof by induction with no inductive hypotheses. We could have arrived at the same result by beginning the proof with: [[ 63 (** It seems kind of odd to write a proof by induction with no inductive hypotheses. We could have arrived at the same result by beginning the proof with: [[
64 64
65 destruct x. 65 destruct x.
66 66
67 ]] 67 ]]
68 68
69 ...which corresponds to "proof by case analysis" in classical math. For non-recursive inductive types, the two tactics will always have identical behavior. Often case analysis is sufficient, even in proofs about recursive types, and it is nice to avoid introducing unneeded induction hypotheses. 69 %\noindent%...which corresponds to "proof by case analysis" in classical math. For non-recursive inductive types, the two tactics will always have identical behavior. Often case analysis is sufficient, even in proofs about recursive types, and it is nice to avoid introducing unneeded induction hypotheses.
70 70
71 What exactly %\textit{%#<i>#is#</i>#%}% the induction principle for [unit]? We can ask Coq: *) 71 What exactly %\textit{%#<i>#is#</i>#%}% the induction principle for [unit]? We can ask Coq: *)
72 72
73 Check unit_ind. 73 Check unit_ind.
74 (** [[ 74 (** [unit_ind : forall P : unit -> Prop, P tt -> forall u : unit, P u] *)
75 75
76 unit_ind : forall P : unit -> Prop, P tt -> forall u : unit, P u 76 (** Every [Inductive] command defining a type [T] also defines an induction principle named [T_ind]. Coq follows the Curry-Howard correspondence and includes the ingredients of programming and proving in the same single syntactic class. Thus, our type, operations over it, and principles for reasoning about it all live in the same language and are described by the same type system. The key to telling what is a program and what is a proof lies in the distinction between the type [Prop], which appears in our induction principle; and the type [Set], which we have seen a few times already.
77 ]]
78
79 Every [Inductive] command defining a type [T] also defines an induction principle named [T_ind]. Coq follows the Curry-Howard correspondence and includes the ingredients of programming and proving in the same single syntactic class. Thus, our type, operations over it, and principles for reasoning about it all live in the same language and are described by the same type system. The key to telling what is a program and what is a proof lies in the distinction between the type [Prop], which appears in our induction principle; and the type [Set], which we have seen a few times already.
80 77
81 The convention goes like this: [Set] is the type of normal types, and the values of such types are programs. [Prop] is the type of logical propositions, and the values of such types are proofs. Thus, an induction principle has a type that shows us that it is a function for building proofs. 78 The convention goes like this: [Set] is the type of normal types, and the values of such types are programs. [Prop] is the type of logical propositions, and the values of such types are proofs. Thus, an induction principle has a type that shows us that it is a function for building proofs.
82 79
83 Specifically, [unit_ind] quantifies over a predicate [P] over [unit] values. If we can present a proof that [P] holds of [tt], then we are rewarded with a proof that [P] holds for any value [u] of type [unit]. In our last proof, the predicate was [(fun u : unit => u = tt)]. 80 Specifically, [unit_ind] quantifies over a predicate [P] over [unit] values. If we can present a proof that [P] holds of [tt], then we are rewarded with a proof that [P] holds for any value [u] of type [unit]. In our last proof, the predicate was [(fun u : unit => u = tt)].
84 81
99 (** Because [Empty_set] has no elements, the fact of having an element of this type implies anything. We use [destruct 1] instead of [destruct x] in the proof because unused quantified variables are relegated to being referred to by number. (There is a good reason for this, related to the unity of quantifiers and implication. An implication is just a quantification over a proof, where the quantified variable is never used. It generally makes more sense to refer to implication hypotheses by number than by name, and Coq treats our quantifier over an unused variable as an implication in determining the proper behavior.) 96 (** Because [Empty_set] has no elements, the fact of having an element of this type implies anything. We use [destruct 1] instead of [destruct x] in the proof because unused quantified variables are relegated to being referred to by number. (There is a good reason for this, related to the unity of quantifiers and implication. An implication is just a quantification over a proof, where the quantified variable is never used. It generally makes more sense to refer to implication hypotheses by number than by name, and Coq treats our quantifier over an unused variable as an implication in determining the proper behavior.)
100 97
101 We can see the induction principle that made this proof so easy: *) 98 We can see the induction principle that made this proof so easy: *)
102 99
103 Check Empty_set_ind. 100 Check Empty_set_ind.
104 (** [[ 101 (** [Empty_set_ind : forall (P : Empty_set -> Prop) (e : Empty_set), P e] *)
105 102
106 Empty_set_ind : forall (P : Empty_set -> Prop) (e : Empty_set), P e 103 (** In other words, any predicate over values from the empty set holds vacuously of every such element. In the last proof, we chose the predicate [(fun _ : Empty_set => 2 + 2 = 5)].
107 ]]
108
109 In other words, any predicate over values from the empty set holds vacuously of every such element. In the last proof, we chose the predicate [(fun _ : Empty_set => 2 + 2 = 5)].
110 104
111 We can also apply this get-out-of-jail-free card programmatically. Here is a lazy way of converting values of [Empty_set] to values of [unit]: *) 105 We can also apply this get-out-of-jail-free card programmatically. Here is a lazy way of converting values of [Empty_set] to values of [unit]: *)
112 106
113 Definition e2u (e : Empty_set) : unit := match e with end. 107 Definition e2u (e : Empty_set) : unit := match e with end.
114 108
139 133
140 Theorem not_inverse : forall b : bool, not (not b) = b. 134 Theorem not_inverse : forall b : bool, not (not b) = b.
141 (* begin thide *) 135 (* begin thide *)
142 destruct b. 136 destruct b.
143 137
144 (** After we case analyze on [b], we are left with one subgoal for each constructor of [bool]. 138 (** After we case-analyze on [b], we are left with one subgoal for each constructor of [bool].
145 139
146 [[ 140 [[
147
148 2 subgoals 141 2 subgoals
149 142
150 ============================ 143 ============================
151 not (not true) = true 144 not (not true) = true
152 ]] 145 ]]
153 146
154 [[ 147 [[
155 subgoal 2 is: 148 subgoal 2 is:
156 not (not false) = false 149 not (not false) = false
150
157 ]] 151 ]]
158 152
159 The first subgoal follows by Coq's rules of computation, so we can dispatch it easily: *) 153 The first subgoal follows by Coq's rules of computation, so we can dispatch it easily: *)
160 154
161 reflexivity. 155 reflexivity.
178 (** [discriminate] is used to prove that two values of an inductive type are not equal, whenever the values are formed with different constructors. In this case, the different constructors are [true] and [false]. 172 (** [discriminate] is used to prove that two values of an inductive type are not equal, whenever the values are formed with different constructors. In this case, the different constructors are [true] and [false].
179 173
180 At this point, it is probably not hard to guess what the underlying induction principle for [bool] is. *) 174 At this point, it is probably not hard to guess what the underlying induction principle for [bool] is. *)
181 175
182 Check bool_ind. 176 Check bool_ind.
183 (** [[ 177 (** [bool_ind : forall P : bool -> Prop, P true -> P false -> forall b : bool, P b] *)
184
185 bool_ind : forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
186 ]] *)
187 178
188 179
189 (** * Simple Recursive Types *) 180 (** * Simple Recursive Types *)
190 181
191 (** The natural numbers are the simplest common example of an inductive type that actually deserves the name. *) 182 (** The natural numbers are the simplest common example of an inductive type that actually deserves the name. *)
218 Qed. 209 Qed.
219 (* end thide *) 210 (* end thide *)
220 211
221 (** We can also now get into genuine inductive theorems. First, we will need a recursive function, to make things interesting. *) 212 (** We can also now get into genuine inductive theorems. First, we will need a recursive function, to make things interesting. *)
222 213
223 Fixpoint plus (n m : nat) {struct n} : nat := 214 Fixpoint plus (n m : nat) : nat :=
224 match n with 215 match n with
225 | O => m 216 | O => m
226 | S n' => S (plus n' m) 217 | S n' => S (plus n' m)
227 end. 218 end.
228 219
229 (** Recall that [Fixpoint] is Coq's mechanism for recursive function definitions, and that the [{struct n}] annotation is noting which function argument decreases structurally at recursive calls. 220 (** Recall that [Fixpoint] is Coq's mechanism for recursive function definitions. Some theorems about [plus] can be proved without induction. *)
230
231 Some theorems about [plus] can be proved without induction. *)
232 221
233 Theorem O_plus_n : forall n : nat, plus O n = n. 222 Theorem O_plus_n : forall n : nat, plus O n = n.
234 (* begin thide *) 223 (* begin thide *)
235 intro; reflexivity. 224 intro; reflexivity.
236 Qed. 225 Qed.
237 (* end thide *) 226 (* end thide *)
238 227
239 (** Coq's computation rules automatically simplify the application of [plus]. If we just reverse the order of the arguments, though, this no longer works, and we need induction. *) 228 (** Coq's computation rules automatically simplify the application of [plus], because unfolding the definition of [plus] gives us a [match] expression where the branch to be taken is obvious from syntax alone. If we just reverse the order of the arguments, though, this no longer works, and we need induction. *)
240 229
241 Theorem n_plus_O : forall n : nat, plus n O = n. 230 Theorem n_plus_O : forall n : nat, plus n O = n.
242 (* begin thide *) 231 (* begin thide *)
243 induction n. 232 induction n.
244 233
247 reflexivity. 236 reflexivity.
248 237
249 (** Our second subgoal is more work and also demonstrates our first inductive hypothesis. 238 (** Our second subgoal is more work and also demonstrates our first inductive hypothesis.
250 239
251 [[ 240 [[
252
253 n : nat 241 n : nat
254 IHn : plus n O = n 242 IHn : plus n O = n
255 ============================ 243 ============================
256 plus (S n) O = S n 244 plus (S n) O = S n
245
257 ]] 246 ]]
258 247
259 We can start out by using computation to simplify the goal as far as we can. *) 248 We can start out by using computation to simplify the goal as far as we can. *)
260 249
261 simpl. 250 simpl.
276 (* end thide *) 265 (* end thide *)
277 266
278 (** We can check out the induction principle at work here: *) 267 (** We can check out the induction principle at work here: *)
279 268
280 Check nat_ind. 269 Check nat_ind.
281 (** [[ 270 (** %\vspace{-.15in}% [[
282 271 nat_ind : forall P : nat -> Prop,
283 nat_ind : forall P : nat -> Prop, 272 P O -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
284 P O -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n 273
285 ]] 274 ]]
286 275
287 Each of the two cases of our last proof came from the type of one of the arguments to [nat_ind]. We chose [P] to be [(fun n : nat => plus n O = n)]. The first proof case corresponded to [P O], and the second case to [(forall n : nat, P n -> P (S n))]. The free variable [n] and inductive hypothesis [IHn] came from the argument types given here. 276 Each of the two cases of our last proof came from the type of one of the arguments to [nat_ind]. We chose [P] to be [(fun n : nat => plus n O = n)]. The first proof case corresponded to [P O] and the second case to [(forall n : nat, P n -> P (S n))]. The free variable [n] and inductive hypothesis [IHn] came from the argument types given here.
288 277
289 Since [nat] has a constructor that takes an argument, we may sometimes need to know that that constructor is injective. *) 278 Since [nat] has a constructor that takes an argument, we may sometimes need to know that that constructor is injective. *)
290 279
291 Theorem S_inj : forall n m : nat, S n = S m -> n = m. 280 Theorem S_inj : forall n m : nat, S n = S m -> n = m.
292 (* begin thide *) 281 (* begin thide *)
312 match ls with 301 match ls with
313 | NNil => O 302 | NNil => O
314 | NCons _ ls' => S (nlength ls') 303 | NCons _ ls' => S (nlength ls')
315 end. 304 end.
316 305
317 Fixpoint napp (ls1 ls2 : nat_list) {struct ls1} : nat_list := 306 Fixpoint napp (ls1 ls2 : nat_list) : nat_list :=
318 match ls1 with 307 match ls1 with
319 | NNil => ls2 308 | NNil => ls2
320 | NCons n ls1' => NCons n (napp ls1' ls2) 309 | NCons n ls1' => NCons n (napp ls1' ls2)
321 end. 310 end.
322 311
328 induction ls1; crush. 317 induction ls1; crush.
329 Qed. 318 Qed.
330 (* end thide *) 319 (* end thide *)
331 320
332 Check nat_list_ind. 321 Check nat_list_ind.
333 (** [[ 322 (** %\vspace{-.15in}% [[
334 323 nat_list_ind
335 nat_list_ind
336 : forall P : nat_list -> Prop, 324 : forall P : nat_list -> Prop,
337 P NNil -> 325 P NNil ->
338 (forall (n : nat) (n0 : nat_list), P n0 -> P (NCons n n0)) -> 326 (forall (n : nat) (n0 : nat_list), P n0 -> P (NCons n n0)) ->
339 forall n : nat_list, P n 327 forall n : nat_list, P n
340 ]] 328 ]]
351 match tr with 339 match tr with
352 | NLeaf => S O 340 | NLeaf => S O
353 | NNode tr1 _ tr2 => plus (nsize tr1) (nsize tr2) 341 | NNode tr1 _ tr2 => plus (nsize tr1) (nsize tr2)
354 end. 342 end.
355 343
356 Fixpoint nsplice (tr1 tr2 : nat_btree) {struct tr1} : nat_btree := 344 Fixpoint nsplice (tr1 tr2 : nat_btree) : nat_btree :=
357 match tr1 with 345 match tr1 with
358 | NLeaf => NNode tr2 O NLeaf 346 | NLeaf => NNode tr2 O NLeaf
359 | NNode tr1' n tr2' => NNode (nsplice tr1' tr2) n tr2' 347 | NNode tr1' n tr2' => NNode (nsplice tr1' tr2) n tr2'
360 end. 348 end.
361 349
373 induction tr1; crush. 361 induction tr1; crush.
374 Qed. 362 Qed.
375 (* end thide *) 363 (* end thide *)
376 364
377 Check nat_btree_ind. 365 Check nat_btree_ind.
378 (** [[ 366 (** %\vspace{-.15in}% [[
379 367 nat_btree_ind
380 nat_btree_ind
381 : forall P : nat_btree -> Prop, 368 : forall P : nat_btree -> Prop,
382 P NLeaf -> 369 P NLeaf ->
383 (forall n : nat_btree, 370 (forall n : nat_btree,
384 P n -> forall (n0 : nat) (n1 : nat_btree), P n1 -> P (NNode n n0 n1)) -> 371 P n -> forall (n0 : nat) (n1 : nat_btree), P n1 -> P (NNode n n0 n1)) ->
385 forall n : nat_btree, P n 372 forall n : nat_btree, P n
398 match ls with 385 match ls with
399 | Nil => O 386 | Nil => O
400 | Cons _ ls' => S (length ls') 387 | Cons _ ls' => S (length ls')
401 end. 388 end.
402 389
403 Fixpoint app T (ls1 ls2 : list T) {struct ls1} : list T := 390 Fixpoint app T (ls1 ls2 : list T) : list T :=
404 match ls1 with 391 match ls1 with
405 | Nil => ls2 392 | Nil => ls2
406 | Cons x ls1' => Cons x (app ls1' ls2) 393 | Cons x ls1' => Cons x (app ls1' ls2)
407 end. 394 end.
408 395
430 match ls with 417 match ls with
431 | Nil => O 418 | Nil => O
432 | Cons _ ls' => S (length ls') 419 | Cons _ ls' => S (length ls')
433 end. 420 end.
434 421
435 Fixpoint app (ls1 ls2 : list) {struct ls1} : list := 422 Fixpoint app (ls1 ls2 : list) : list :=
436 match ls1 with 423 match ls1 with
437 | Nil => ls2 424 | Nil => ls2
438 | Cons x ls1' => Cons x (app ls1' ls2) 425 | Cons x ls1' => Cons x (app ls1' ls2)
439 end. 426 end.
440 427
451 (* end hide *) 438 (* end hide *)
452 439
453 (** After we end the section, the [Variable]s we used are added as extra function parameters for each defined identifier, as needed. *) 440 (** After we end the section, the [Variable]s we used are added as extra function parameters for each defined identifier, as needed. *)
454 441
455 Print list. 442 Print list.
456 (** [[ 443 (** %\vspace{-.15in}% [[
457 444 Inductive list (T : Set) : Set :=
458
459 Inductive list (T : Set) : Set :=
460 Nil : list T | Cons : T -> list T -> list Tlist 445 Nil : list T | Cons : T -> list T -> list Tlist
446
461 ]] 447 ]]
462 448
463 The final definition is the same as what we wrote manually before. The other elements of the section are altered similarly, turning out exactly as they were before, though we managed to write their definitions more succinctly. *) 449 The final definition is the same as what we wrote manually before. The other elements of the section are altered similarly, turning out exactly as they were before, though we managed to write their definitions more succinctly. *)
464 450
465 Check length. 451 Check length.
466 (** [[ 452 (** %\vspace{-.15in}% [[
467 453 length
468 length
469 : forall T : Set, list T -> nat 454 : forall T : Set, list T -> nat
470 ]] 455 ]]
471 456
472 The parameter [T] is treated as a new argument to the induction principle, too. *) 457 The parameter [T] is treated as a new argument to the induction principle, too. *)
473 458
474 Check list_ind. 459 Check list_ind.
475 (** [[ 460 (** %\vspace{-.15in}% [[
476 461 list_ind
477 list_ind
478 : forall (T : Set) (P : list T -> Prop), 462 : forall (T : Set) (P : list T -> Prop),
479 P (Nil T) -> 463 P (Nil T) ->
480 (forall (t : T) (l : list T), P l -> P (Cons t l)) -> 464 (forall (t : T) (l : list T), P l -> P (Cons t l)) ->
481 forall l : list T, P l 465 forall l : list T, P l
482 ]] 466 ]]
504 with olength (ol : odd_list) : nat := 488 with olength (ol : odd_list) : nat :=
505 match ol with 489 match ol with
506 | OCons _ el => S (elength el) 490 | OCons _ el => S (elength el)
507 end. 491 end.
508 492
509 Fixpoint eapp (el1 el2 : even_list) {struct el1} : even_list := 493 Fixpoint eapp (el1 el2 : even_list) : even_list :=
510 match el1 with 494 match el1 with
511 | ENil => el2 495 | ENil => el2
512 | ECons n ol => ECons n (oapp ol el2) 496 | ECons n ol => ECons n (oapp ol el2)
513 end 497 end
514 498
515 with oapp (ol : odd_list) (el : even_list) {struct ol} : odd_list := 499 with oapp (ol : odd_list) (el : even_list) : odd_list :=
516 match ol with 500 match ol with
517 | OCons n el' => OCons n (eapp el' el) 501 | OCons n el' => OCons n (eapp el' el)
518 end. 502 end.
519 503
520 (** Everything is going roughly the same as in past examples, until we try to prove a theorem similar to those that came before. *) 504 (** Everything is going roughly the same as in past examples, until we try to prove a theorem similar to those that came before. *)
535 519
536 We have no induction hypothesis, so we cannot prove this goal without starting another induction, which would reach a similar point, sending us into a futile infinite chain of inductions. The problem is that Coq's generation of [T_ind] principles is incomplete. We only get non-mutual induction principles generated by default. *) 520 We have no induction hypothesis, so we cannot prove this goal without starting another induction, which would reach a similar point, sending us into a futile infinite chain of inductions. The problem is that Coq's generation of [T_ind] principles is incomplete. We only get non-mutual induction principles generated by default. *)
537 521
538 Abort. 522 Abort.
539 Check even_list_ind. 523 Check even_list_ind.
540 (** [[ 524 (** %\vspace{-.15in}% [[
541 525 even_list_ind
542 even_list_ind
543 : forall P : even_list -> Prop, 526 : forall P : even_list -> Prop,
544 P ENil -> 527 P ENil ->
545 (forall (n : nat) (o : odd_list), P (ECons n o)) -> 528 (forall (n : nat) (o : odd_list), P (ECons n o)) ->
546 forall e : even_list, P e 529 forall e : even_list, P e
530
547 ]] 531 ]]
548 532
549 We see that no inductive hypotheses are included anywhere in the type. To get them, we must ask for mutual principles as we need them, using the [Scheme] command. *) 533 We see that no inductive hypotheses are included anywhere in the type. To get them, we must ask for mutual principles as we need them, using the [Scheme] command. *)
550 534
551 Scheme even_list_mut := Induction for even_list Sort Prop 535 Scheme even_list_mut := Induction for even_list Sort Prop
552 with odd_list_mut := Induction for odd_list Sort Prop. 536 with odd_list_mut := Induction for odd_list Sort Prop.
553 537
554 Check even_list_mut. 538 Check even_list_mut.
555 (** [[ 539 (** %\vspace{-.15in}% [[
556 540 even_list_mut
557 even_list_mut
558 : forall (P : even_list -> Prop) (P0 : odd_list -> Prop), 541 : forall (P : even_list -> Prop) (P0 : odd_list -> Prop),
559 P ENil -> 542 P ENil ->
560 (forall (n : nat) (o : odd_list), P0 o -> P (ECons n o)) -> 543 (forall (n : nat) (o : odd_list), P0 o -> P (ECons n o)) ->
561 (forall (n : nat) (e : even_list), P e -> P0 (OCons n e)) -> 544 (forall (n : nat) (e : even_list), P e -> P0 (OCons n e)) ->
562 forall e : even_list, P e 545 forall e : even_list, P e
546
563 ]] 547 ]]
564 548
565 This is the principle we wanted in the first place. There is one more wrinkle left in using it: the [induction] tactic will not apply it for us automatically. It will be helpful to look at how to prove one of our past examples without using [induction], so that we can then generalize the technique to mutual inductive types. *) 549 This is the principle we wanted in the first place. There is one more wrinkle left in using it: the [induction] tactic will not apply it for us automatically. It will be helpful to look at how to prove one of our past examples without using [induction], so that we can then generalize the technique to mutual inductive types. *)
566 550
567 Theorem n_plus_O' : forall n : nat, plus n O = n. 551 Theorem n_plus_O' : forall n : nat, plus n O = n.
626 (* end thide *) 610 (* end thide *)
627 611
628 (** We can take a look at the induction principle behind this proof. *) 612 (** We can take a look at the induction principle behind this proof. *)
629 613
630 Check formula_ind. 614 Check formula_ind.
631 (** [[ 615 (** %\vspace{-.15in}% [[
632 616 formula_ind
633 formula_ind
634 : forall P : formula -> Prop, 617 : forall P : formula -> Prop,
635 (forall n n0 : nat, P (Eq n n0)) -> 618 (forall n n0 : nat, P (Eq n n0)) ->
636 (forall f0 : formula, 619 (forall f0 : formula,
637 P f0 -> forall f1 : formula, P f1 -> P (And f0 f1)) -> 620 P f0 -> forall f1 : formula, P f1 -> P (And f0 f1)) ->
638 (forall f1 : nat -> formula, 621 (forall f1 : nat -> formula,
639 (forall n : nat, P (f1 n)) -> P (Forall f1)) -> 622 (forall n : nat, P (f1 n)) -> P (Forall f1)) ->
640 forall f2 : formula, P f2 623 forall f2 : formula, P f2
641 ]] *) 624
642 625 ]]
643 (** Focusing on the [Forall] case, which comes third, we see that we are allowed to assume that the theorem holds %\textit{%#<i>#for any application of the argument function [f1]#</i>#%}%. That is, Coq induction principles do not follow a simple rule that the textual representations of induction variables must get shorter in appeals to induction hypotheses. Luckily for us, the people behind the metatheory of Coq have verified that this flexibility does not introduce unsoundness. 626
627 Focusing on the [Forall] case, which comes third, we see that we are allowed to assume that the theorem holds %\textit{%#<i>#for any application of the argument function [f1]#</i>#%}%. That is, Coq induction principles do not follow a simple rule that the textual representations of induction variables must get shorter in appeals to induction hypotheses. Luckily for us, the people behind the metatheory of Coq have verified that this flexibility does not introduce unsoundness.
644 628
645 %\medskip% 629 %\medskip%
646 630
647 Up to this point, we have seen how to encode in Coq more and more of what is possible with algebraic datatypes in Haskell and ML. This may have given the inaccurate impression that inductive types are a strict extension of algebraic datatypes. In fact, Coq must rule out some types allowed by Haskell and ML, for reasons of soundness. Reflexive types provide our first good example of such a case. 631 Up to this point, we have seen how to encode in Coq more and more of what is possible with algebraic datatypes in Haskell and ML. This may have given the inaccurate impression that inductive types are a strict extension of algebraic datatypes. In fact, Coq must rule out some types allowed by Haskell and ML, for reasons of soundness. Reflexive types provide our first good example of such a case.
648 632
649 Given our last example of an inductive type, many readers are probably eager to try encoding the syntax of lambda calculus. Indeed, the function-based representation technique that we just used, called %\textit{%#<i>#higher-order abstract syntax (HOAS)#</i>#%}%, is the representation of choice for lambda calculi in Twelf and in many applications implemented in Haskell and ML. Let us try to import that choice to Coq: *) 633 Given our last example of an inductive type, many readers are probably eager to try encoding the syntax of lambda calculus. Indeed, the function-based representation technique that we just used, called %\textit{%#<i>#higher-order abstract syntax (HOAS)#</i>#%}%, is the representation of choice for lambda calculi in Twelf and in many applications implemented in Haskell and ML. Let us try to import that choice to Coq: *)
650 634
651 (** [[ 635 (** [[
652
653 Inductive term : Set := 636 Inductive term : Set :=
654 | App : term -> term -> term 637 | App : term -> term -> term
655 | Abs : (term -> term) -> term. 638 | Abs : (term -> term) -> term.
656 639
657 [[
658 Error: Non strictly positive occurrence of "term" in "(term -> term) -> term" 640 Error: Non strictly positive occurrence of "term" in "(term -> term) -> term"
641
659 ]] 642 ]]
660 643
661 We have run afoul of the %\textit{%#<i>#strict positivity requirement#</i>#%}% for inductive definitions, which says that the type being defined may not occur to the left of an arrow in the type of a constructor argument. It is important that the type of a constructor is viewed in terms of a series of arguments and a result, since obviously we need recursive occurrences to the lefts of the outermost arrows if we are to have recursive occurrences at all. 644 We have run afoul of the %\textit{%#<i>#strict positivity requirement#</i>#%}% for inductive definitions, which says that the type being defined may not occur to the left of an arrow in the type of a constructor argument. It is important that the type of a constructor is viewed in terms of a series of arguments and a result, since obviously we need recursive occurrences to the lefts of the outermost arrows if we are to have recursive occurrences at all.
662 645
663 Why must Coq enforce this restriction? Imagine that our last definition had been accepted, allowing us to write this function: 646 Why must Coq enforce this restriction? Imagine that our last definition had been accepted, allowing us to write this function:
681 (** * An Interlude on Proof Terms *) 664 (** * An Interlude on Proof Terms *)
682 665
683 (** As we have emphasized a few times already, Coq proofs are actually programs, written in the same language we have been using in our examples all along. We can get a first sense of what this means by taking a look at the definitions of some of the induction principles we have used. *) 666 (** As we have emphasized a few times already, Coq proofs are actually programs, written in the same language we have been using in our examples all along. We can get a first sense of what this means by taking a look at the definitions of some of the induction principles we have used. *)
684 667
685 Print unit_ind. 668 Print unit_ind.
686 (** [[ 669 (** %\vspace{-.15in}% [[
687 670 unit_ind =
688 unit_ind = 671 fun P : unit -> Prop => unit_rect P
689 fun P : unit -> Prop => unit_rect P
690 : forall P : unit -> Prop, P tt -> forall u : unit, P u 672 : forall P : unit -> Prop, P tt -> forall u : unit, P u
673
691 ]] 674 ]]
692 675
693 We see that this induction principle is defined in terms of a more general principle, [unit_rect]. *) 676 We see that this induction principle is defined in terms of a more general principle, [unit_rect]. *)
694 677
695 Check unit_rect. 678 Check unit_rect.
696 (** [[ 679 (** %\vspace{-.15in}% [[
697 680 unit_rect
698 unit_rect
699 : forall P : unit -> Type, P tt -> forall u : unit, P u 681 : forall P : unit -> Type, P tt -> forall u : unit, P u
682
700 ]] 683 ]]
701 684
702 [unit_rect] gives [P] type [unit -> Type] instead of [unit -> Prop]. [Type] is another universe, like [Set] and [Prop]. In fact, it is a common supertype of both. Later on, we will discuss exactly what the significances of the different universes are. For now, it is just important that we can use [Type] as a sort of meta-universe that may turn out to be either [Set] or [Prop]. We can see the symmetry inherent in the subtyping relationship by printing the definition of another principle that was generated for [unit] automatically: *) 685 [unit_rect] gives [P] type [unit -> Type] instead of [unit -> Prop]. [Type] is another universe, like [Set] and [Prop]. In fact, it is a common supertype of both. Later on, we will discuss exactly what the significances of the different universes are. For now, it is just important that we can use [Type] as a sort of meta-universe that may turn out to be either [Set] or [Prop]. We can see the symmetry inherent in the subtyping relationship by printing the definition of another principle that was generated for [unit] automatically: *)
703 686
704 Print unit_rec. 687 Print unit_rec.
705 (** [[ 688 (** %\vspace{-.15in}% [[
706 689 unit_rec =
707 unit_rec = 690 fun P : unit -> Set => unit_rect P
708 fun P : unit -> Set => unit_rect P
709 : forall P : unit -> Set, P tt -> forall u : unit, P u 691 : forall P : unit -> Set, P tt -> forall u : unit, P u
692
710 ]] 693 ]]
711 694
712 This is identical to the definition for [unit_ind], except that we have substituted [Set] for [Prop]. For most inductive types [T], then, we get not just induction principles [T_ind], but also recursion principles [T_rec]. We can use [T_rec] to write recursive definitions without explicit [Fixpoint] recursion. For instance, the following two definitions are equivalent: *) 695 This is identical to the definition for [unit_ind], except that we have substituted [Set] for [Prop]. For most inductive types [T], then, we get not just induction principles [T_ind], but also recursion principles [T_rec]. We can use [T_rec] to write recursive definitions without explicit [Fixpoint] recursion. For instance, the following two definitions are equivalent: *)
713 696
714 Definition always_O (u : unit) : nat := 697 Definition always_O (u : unit) : nat :=
720 unit_rec (fun _ : unit => nat) O u. 703 unit_rec (fun _ : unit => nat) O u.
721 704
722 (** Going even further down the rabbit hole, [unit_rect] itself is not even a primitive. It is a functional program that we can write manually. *) 705 (** Going even further down the rabbit hole, [unit_rect] itself is not even a primitive. It is a functional program that we can write manually. *)
723 706
724 Print unit_rect. 707 Print unit_rect.
725 708 (** %\vspace{-.15in}% [[
726 (** [[ 709 unit_rect =
727 710 fun (P : unit -> Type) (f : P tt) (u : unit) =>
728 unit_rect = 711 match u as u0 return (P u0) with
729 fun (P : unit -> Type) (f : P tt) (u : unit) => 712 | tt => f
730 match u as u0 return (P u0) with 713 end
731 | tt => f
732 end
733 : forall P : unit -> Type, P tt -> forall u : unit, P u 714 : forall P : unit -> Type, P tt -> forall u : unit, P u
715
734 ]] 716 ]]
735 717
736 The only new feature we see is an [as] clause for a [match], which is used in concert with the [return] clause that we saw in the introduction. Since the type of the [match] is dependent on the value of the object being analyzed, we must give that object a name so that we can refer to it in the [return] clause. 718 The only new feature we see is an [as] clause for a [match], which is used in concert with the [return] clause that we saw in the introduction. Since the type of the [match] is dependent on the value of the object being analyzed, we must give that object a name so that we can refer to it in the [return] clause.
737 719
738 To prove that [unit_rect] is nothing special, we can reimplement it manually. *) 720 To prove that [unit_rect] is nothing special, we can reimplement it manually. *)
739 721
740 Definition unit_rect' (P : unit -> Type) (f : P tt) (u : unit) := 722 Definition unit_rect' (P : unit -> Type) (f : P tt) (u : unit) :=
741 match u return (P u) with 723 match u with
742 | tt => f 724 | tt => f
743 end. 725 end.
744 726
745 (** We use the handy shorthand that lets us omit an [as] annotation when matching on a variable, simply using that variable directly in the [return] clause. 727 (** We rely on Coq's heuristics for inferring [match] annotations.
746 728
747 We can check the implement of [nat_rect] as well: *) 729 We can check the implementation of [nat_rect] as well: *)
748 730
749 Print nat_rect. 731 Print nat_rect.
750 (** [[ 732 (** %\vspace{-.15in}% [[
751 733 nat_rect =
752 nat_rect = 734 fun (P : nat -> Type) (f : P O) (f0 : forall n : nat, P n -> P (S n)) =>
753 fun (P : nat -> Type) (f : P O) (f0 : forall n : nat, P n -> P (S n)) => 735 fix F (n : nat) : P n :=
754 fix F (n : nat) : P n := 736 match n as n0 return (P n0) with
755 match n as n0 return (P n0) with 737 | O => f
756 | O => f 738 | S n0 => f0 n0 (F n0)
757 | S n0 => f0 n0 (F n0) 739 end
758 end 740 : forall P : nat -> Type,
759 : forall P : nat -> Type, 741 P O -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
760 P O -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n 742 ]]
761 ]] 743
762 744 Now we have an actual recursive definition. [fix] expressions are an anonymous form of [Fixpoint], just as [fun] expressions stand for anonymous non-recursive functions. Beyond that, the syntax of [fix] mirrors that of [Fixpoint]. We can understand the definition of [nat_rect] better by reimplementing [nat_ind] using sections. *)
763 Now we have an actual recursive definition. [fix] expressions are an anonymous form of [Fixpoint], just as [fun] expressions stand for anonymous non-recursive functions. Beyond that, the syntax of [fix] mirrors that of [Fixpoint]. We can understand the definition of [nat_rect] better by reimplementing [nat_ind] using sections. *) 745
764 746 Section nat_ind'.
765 Section nat_ind'. 747 (** First, we have the property of natural numbers that we aim to prove. *)
766 (** First, we have the property of natural numbers that we aim to prove. *) 748
767 Variable P : nat -> Prop. 749 Variable P : nat -> Prop.
768 750
769 (** Then we require a proof of the [O] case. *) 751 (** Then we require a proof of the [O] case. *)
770 Hypothesis O_case : P O. 752
771 753 Hypothesis O_case : P O.
772 (** Next is a proof of the [S] case, which may assume an inductive hypothesis. *) 754
773 Hypothesis S_case : forall n : nat, P n -> P (S n). 755 (** Next is a proof of the [S] case, which may assume an inductive hypothesis. *)
774 756
775 (** Finally, we define a recursive function to tie the pieces together. *) 757 Hypothesis S_case : forall n : nat, P n -> P (S n).
776 Fixpoint nat_ind' (n : nat) : P n := 758
777 match n return (P n) with 759 (** Finally, we define a recursive function to tie the pieces together. *)
778 | O => O_case 760
779 | S n' => S_case (nat_ind' n') 761 Fixpoint nat_ind' (n : nat) : P n :=
780 end. 762 match n with
781 End nat_ind'. 763 | O => O_case
782 764 | S n' => S_case (nat_ind' n')
783 (** Closing the section adds the [Variable]s and [Hypothesis]es as new [fun]-bound arguments to [nat_ind'], and, modulo the use of [Prop] instead of [Type], we end up with the exact same definition that was generated automatically for [nat_rect]. 765 end.
784 766 End nat_ind'.
785 %\medskip% 767
786 768 (** Closing the section adds the [Variable]s and [Hypothesis]es as new [fun]-bound arguments to [nat_ind'], and, modulo the use of [Prop] instead of [Type], we end up with the exact same definition that was generated automatically for [nat_rect].
787 We can also examine the definition of [even_list_mut], which we generated with [Scheme] for a mutually-recursive type. *) 769
788 770 %\medskip%
789 Print even_list_mut. 771
790 (** [[ 772 We can also examine the definition of [even_list_mut], which we generated with [Scheme] for a mutually-recursive type. *)
791 773
792 even_list_mut = 774 Print even_list_mut.
793 fun (P : even_list -> Prop) (P0 : odd_list -> Prop) 775 (** %\vspace{-.15in}% [[
794 (f : P ENil) (f0 : forall (n : nat) (o : odd_list), P0 o -> P (ECons n o)) 776 even_list_mut =
795 (f1 : forall (n : nat) (e : even_list), P e -> P0 (OCons n e)) => 777 fun (P : even_list -> Prop) (P0 : odd_list -> Prop)
796 fix F (e : even_list) : P e := 778 (f : P ENil) (f0 : forall (n : nat) (o : odd_list), P0 o -> P (ECons n o))
797 match e as e0 return (P e0) with 779 (f1 : forall (n : nat) (e : even_list), P e -> P0 (OCons n e)) =>
798 | ENil => f 780 fix F (e : even_list) : P e :=
799 | ECons n o => f0 n o (F0 o) 781 match e as e0 return (P e0) with
800 end 782 | ENil => f
801 with F0 (o : odd_list) : P0 o := 783 | ECons n o => f0 n o (F0 o)
802 match o as o0 return (P0 o0) with 784 end
803 | OCons n e => f1 n e (F e) 785 with F0 (o : odd_list) : P0 o :=
804 end 786 match o as o0 return (P0 o0) with
805 for F 787 | OCons n e => f1 n e (F e)
806 : forall (P : even_list -> Prop) (P0 : odd_list -> Prop), 788 end
807 P ENil -> 789 for F
808 (forall (n : nat) (o : odd_list), P0 o -> P (ECons n o)) -> 790 : forall (P : even_list -> Prop) (P0 : odd_list -> Prop),
809 (forall (n : nat) (e : even_list), P e -> P0 (OCons n e)) -> 791 P ENil ->
810 forall e : even_list, P e 792 (forall (n : nat) (o : odd_list), P0 o -> P (ECons n o)) ->
811 ]] 793 (forall (n : nat) (e : even_list), P e -> P0 (OCons n e)) ->
812 794 forall e : even_list, P e
813 We see a mutually-recursive [fix], with the different functions separated by [with] in the same way that they would be separated by [and] in ML. A final [for] clause identifies which of the mutually-recursive functions should be the final value of the [fix] expression. Using this definition as a template, we can reimplement [even_list_mut] directly. *) 795
814 796 ]]
815 Section even_list_mut'. 797
816 (** First, we need the properties that we are proving. *) 798 We see a mutually-recursive [fix], with the different functions separated by [with] in the same way that they would be separated by [and] in ML. A final [for] clause identifies which of the mutually-recursive functions should be the final value of the [fix] expression. Using this definition as a template, we can reimplement [even_list_mut] directly. *)
817 Variable Peven : even_list -> Prop. 799
818 Variable Podd : odd_list -> Prop. 800 Section even_list_mut'.
819 801 (** First, we need the properties that we are proving. *)
820 (** Next, we need proofs of the three cases. *) 802
821 Hypothesis ENil_case : Peven ENil. 803 Variable Peven : even_list -> Prop.
822 Hypothesis ECons_case : forall (n : nat) (o : odd_list), Podd o -> Peven (ECons n o). 804 Variable Podd : odd_list -> Prop.
823 Hypothesis OCons_case : forall (n : nat) (e : even_list), Peven e -> Podd (OCons n e). 805
824 806 (** Next, we need proofs of the three cases. *)
825 (** Finally, we define the recursive functions. *) 807
826 Fixpoint even_list_mut' (e : even_list) : Peven e := 808 Hypothesis ENil_case : Peven ENil.
827 match e return (Peven e) with 809 Hypothesis ECons_case : forall (n : nat) (o : odd_list), Podd o -> Peven (ECons n o).
828 | ENil => ENil_case 810 Hypothesis OCons_case : forall (n : nat) (e : even_list), Peven e -> Podd (OCons n e).
829 | ECons n o => ECons_case n (odd_list_mut' o) 811
830 end 812 (** Finally, we define the recursive functions. *)
831 with odd_list_mut' (o : odd_list) : Podd o := 813
832 match o return (Podd o) with 814 Fixpoint even_list_mut' (e : even_list) : Peven e :=
833 | OCons n e => OCons_case n (even_list_mut' e) 815 match e with
834 end. 816 | ENil => ENil_case
817 | ECons n o => ECons_case n (odd_list_mut' o)
818 end
819 with odd_list_mut' (o : odd_list) : Podd o :=
820 match o with
821 | OCons n e => OCons_case n (even_list_mut' e)
822 end.
835 End even_list_mut'. 823 End even_list_mut'.
836 824
837 (** Even induction principles for reflexive types are easy to implement directly. For our [formula] type, we can use a recursive definition much like those we wrote above. *) 825 (** Even induction principles for reflexive types are easy to implement directly. For our [formula] type, we can use a recursive definition much like those we wrote above. *)
838 826
839 Section formula_ind'. 827 Section formula_ind'.
843 P f1 -> P f2 -> P (And f1 f2). 831 P f1 -> P f2 -> P (And f1 f2).
844 Hypothesis Forall_case : forall f : nat -> formula, 832 Hypothesis Forall_case : forall f : nat -> formula,
845 (forall n : nat, P (f n)) -> P (Forall f). 833 (forall n : nat, P (f n)) -> P (Forall f).
846 834
847 Fixpoint formula_ind' (f : formula) : P f := 835 Fixpoint formula_ind' (f : formula) : P f :=
848 match f return (P f) with 836 match f with
849 | Eq n1 n2 => Eq_case n1 n2 837 | Eq n1 n2 => Eq_case n1 n2
850 | And f1 f2 => And_case (formula_ind' f1) (formula_ind' f2) 838 | And f1 f2 => And_case (formula_ind' f1) (formula_ind' f2)
851 | Forall f' => Forall_case f' (fun n => formula_ind' (f' n)) 839 | Forall f' => Forall_case f' (fun n => formula_ind' (f' n))
852 end. 840 end.
853 End formula_ind'. 841 End formula_ind'.
864 (** This is an example of a %\textit{%#<i>#nested#</i>#%}% inductive type definition, because we use the type we are defining as an argument to a parametrized type family. Coq will not allow all such definitions; it effectively pretends that we are defining [nat_tree] mutually with a version of [list] specialized to [nat_tree], checking that the resulting expanded definition satisfies the usual rules. For instance, if we replaced [list] with a type family that used its parameter as a function argument, then the definition would be rejected as violating the positivity restriction. 852 (** This is an example of a %\textit{%#<i>#nested#</i>#%}% inductive type definition, because we use the type we are defining as an argument to a parametrized type family. Coq will not allow all such definitions; it effectively pretends that we are defining [nat_tree] mutually with a version of [list] specialized to [nat_tree], checking that the resulting expanded definition satisfies the usual rules. For instance, if we replaced [list] with a type family that used its parameter as a function argument, then the definition would be rejected as violating the positivity restriction.
865 853
866 Like we encountered for mutual inductive types, we find that the automatically-generated induction principle for [nat_tree] is too weak. *) 854 Like we encountered for mutual inductive types, we find that the automatically-generated induction principle for [nat_tree] is too weak. *)
867 855
868 Check nat_tree_ind. 856 Check nat_tree_ind.
869 (** [[ 857 (** %\vspace{-.15in}% [[
870 858 nat_tree_ind
871 nat_tree_ind
872 : forall P : nat_tree -> Prop, 859 : forall P : nat_tree -> Prop,
873 P NLeaf' -> 860 P NLeaf' ->
874 (forall (n : nat) (l : list nat_tree), P (NNode' n l)) -> 861 (forall (n : nat) (l : list nat_tree), P (NNode' n l)) ->
875 forall n : nat_tree, P n 862 forall n : nat_tree, P n
863
876 ]] 864 ]]
877 865
878 There is no command like [Scheme] that will implement an improved principle for us. In general, it takes creativity to figure out how to incorporate nested uses to different type families. Now that we know how to implement induction principles manually, we are in a position to apply just such creativity to this problem. 866 There is no command like [Scheme] that will implement an improved principle for us. In general, it takes creativity to figure out how to incorporate nested uses to different type families. Now that we know how to implement induction principles manually, we are in a position to apply just such creativity to this problem.
879 867
880 First, we will need an auxiliary definition, characterizing what it means for a property to hold of every element of a list. *) 868 First, we will need an auxiliary definition, characterizing what it means for a property to hold of every element of a list. *)
891 End All. 879 End All.
892 880
893 (** It will be useful to look at the definitions of [True] and [/\], since we will want to write manual proofs of them below. *) 881 (** It will be useful to look at the definitions of [True] and [/\], since we will want to write manual proofs of them below. *)
894 882
895 Print True. 883 Print True.
896 (** [[ 884 (** %\vspace{-.15in}% [[
897 885 Inductive True : Prop := I : True
898 Inductive True : Prop := I : True 886
899 ]] 887 ]]
900 888
901 That is, [True] is a proposition with exactly one proof, [I], which we may always supply trivially. 889 That is, [True] is a proposition with exactly one proof, [I], which we may always supply trivially.
902 890
903 Finding the definition of [/\] takes a little more work. Coq supports user registration of arbitrary parsing rules, and it is such a rule that is letting us write [/\] instead of an application of some inductive type family. We can find the underlying inductive type with the [Locate] command. *) 891 Finding the definition of [/\] takes a little more work. Coq supports user registration of arbitrary parsing rules, and it is such a rule that is letting us write [/\] instead of an application of some inductive type family. We can find the underlying inductive type with the [Locate] command. *)
904 892
905 Locate "/\". 893 Locate "/\".
906 (** [[ 894 (** %\vspace{-.15in}% [[
907 895 Notation Scope
908 Notation Scope 896 "A /\ B" := and A B : type_scope
909 "A /\ B" := and A B : type_scope 897 (default interpretation)
910 (default interpretation)
911 ]] *) 898 ]] *)
912 899
913 Print and. 900 Print and.
914 (** [[ 901 (** %\vspace{-.15in}% [[
915 902 Inductive and (A : Prop) (B : Prop) : Prop := conj : A -> B -> A /\ B
916 Inductive and (A : Prop) (B : Prop) : Prop := conj : A -> B -> A /\ B 903 For conj: Arguments A, B are implicit
917 For conj: Arguments A, B are implicit 904 For and: Argument scopes are [type_scope type_scope]
918 For and: Argument scopes are [type_scope type_scope] 905 For conj: Argument scopes are [type_scope type_scope _ _]
919 For conj: Argument scopes are [type_scope type_scope _ _] 906
920 ]] 907 ]]
921 908
922 In addition to the definition of [and] itself, we get information on implicit arguments and parsing rules for [and] and its constructor [conj]. We will ignore the parsing information for now. The implicit argument information tells us that we build a proof of a conjunction by calling the constructor [conj] on proofs of the conjuncts, with no need to include the types of those proofs as explicit arguments. 909 In addition to the definition of [and] itself, we get information on implicit arguments and parsing rules for [and] and its constructor [conj]. We will ignore the parsing information for now. The implicit argument information tells us that we build a proof of a conjunction by calling the constructor [conj] on proofs of the conjuncts, with no need to include the types of those proofs as explicit arguments.
923 910
924 %\medskip% 911 %\medskip%
933 All P ls -> P (NNode' n ls). 920 All P ls -> P (NNode' n ls).
934 921
935 (** A first attempt at writing the induction principle itself follows the intuition that nested inductive type definitions are expanded into mutual inductive definitions. 922 (** A first attempt at writing the induction principle itself follows the intuition that nested inductive type definitions are expanded into mutual inductive definitions.
936 923
937 [[ 924 [[
938
939 Fixpoint nat_tree_ind' (tr : nat_tree) : P tr := 925 Fixpoint nat_tree_ind' (tr : nat_tree) : P tr :=
940 match tr return (P tr) with 926 match tr with
941 | NLeaf' => NLeaf'_case 927 | NLeaf' => NLeaf'_case
942 | NNode' n ls => NNode'_case n ls (list_nat_tree_ind ls) 928 | NNode' n ls => NNode'_case n ls (list_nat_tree_ind ls)
943 end 929 end
944 930
945 with list_nat_tree_ind (ls : list nat_tree) : All P ls := 931 with list_nat_tree_ind (ls : list nat_tree) : All P ls :=
946 match ls return (All P ls) with 932 match ls with
947 | Nil => I 933 | Nil => I
948 | Cons tr rest => conj (nat_tree_ind' tr) (list_nat_tree_ind rest) 934 | Cons tr rest => conj (nat_tree_ind' tr) (list_nat_tree_ind rest)
949 end. 935 end.
950 936
951 ]] 937 ]]
952 938
953 Coq rejects this definition, saying "Recursive call to nat_tree_ind' has principal argument equal to "tr" instead of rest." The term "nested inductive type" hints at the solution to the problem. Just like true mutually-inductive types require mutually-recursive induction principles, nested types require nested recursion. *) 939 Coq rejects this definition, saying "Recursive call to nat_tree_ind' has principal argument equal to "tr" instead of rest." The term "nested inductive type" hints at the solution to the problem. Just like true mutually-inductive types require mutually-recursive induction principles, nested types require nested recursion. *)
954 940
955 Fixpoint nat_tree_ind' (tr : nat_tree) : P tr := 941 Fixpoint nat_tree_ind' (tr : nat_tree) : P tr :=
956 match tr return (P tr) with 942 match tr with
957 | NLeaf' => NLeaf'_case 943 | NLeaf' => NLeaf'_case
958 | NNode' n ls => NNode'_case n ls 944 | NNode' n ls => NNode'_case n ls
959 ((fix list_nat_tree_ind (ls : list nat_tree) : All P ls := 945 ((fix list_nat_tree_ind (ls : list nat_tree) : All P ls :=
960 match ls return (All P ls) with 946 match ls with
961 | Nil => I 947 | Nil => I
962 | Cons tr rest => conj (nat_tree_ind' tr) (list_nat_tree_ind rest) 948 | Cons tr rest => conj (nat_tree_ind' tr) (list_nat_tree_ind rest)
963 end) ls) 949 end) ls)
964 end. 950 end.
965 951
994 | NNode' _ trs => S (sum (map ntsize trs)) 980 | NNode' _ trs => S (sum (map ntsize trs))
995 end. 981 end.
996 982
997 (** Notice that Coq was smart enough to expand the definition of [map] to verify that we are using proper nested recursion, even through a use of a higher-order function. *) 983 (** Notice that Coq was smart enough to expand the definition of [map] to verify that we are using proper nested recursion, even through a use of a higher-order function. *)
998 984
999 Fixpoint ntsplice (tr1 tr2 : nat_tree) {struct tr1} : nat_tree := 985 Fixpoint ntsplice (tr1 tr2 : nat_tree) : nat_tree :=
1000 match tr1 with 986 match tr1 with
1001 | NLeaf' => NNode' O (Cons tr2 Nil) 987 | NLeaf' => NNode' O (Cons tr2 Nil)
1002 | NNode' n Nil => NNode' n (Cons tr2 Nil) 988 | NNode' n Nil => NNode' n (Cons tr2 Nil)
1003 | NNode' n (Cons tr trs) => NNode' n (Cons (ntsplice tr tr2) trs) 989 | NNode' n (Cons tr trs) => NNode' n (Cons (ntsplice tr tr2) trs)
1004 end. 990 end.
1018 = plus (ntsize tr2) (ntsize tr1). 1004 = plus (ntsize tr2) (ntsize tr1).
1019 (* begin thide *) 1005 (* begin thide *)
1020 Hint Rewrite plus_S : cpdt. 1006 Hint Rewrite plus_S : cpdt.
1021 1007
1022 (** We know that the standard induction principle is insufficient for the task, so we need to provide a [using] clause for the [induction] tactic to specify our alternate principle. *) 1008 (** We know that the standard induction principle is insufficient for the task, so we need to provide a [using] clause for the [induction] tactic to specify our alternate principle. *)
1009
1023 induction tr1 using nat_tree_ind'; crush. 1010 induction tr1 using nat_tree_ind'; crush.
1024 1011
1025 (** One subgoal remains: [[ 1012 (** One subgoal remains: [[
1026
1027 n : nat 1013 n : nat
1028 ls : list nat_tree 1014 ls : list nat_tree
1029 H : All 1015 H : All
1030 (fun tr1 : nat_tree => 1016 (fun tr1 : nat_tree =>
1031 forall tr2 : nat_tree, 1017 forall tr2 : nat_tree,
1035 ntsize 1021 ntsize
1036 match ls with 1022 match ls with
1037 | Nil => NNode' n (Cons tr2 Nil) 1023 | Nil => NNode' n (Cons tr2 Nil)
1038 | Cons tr trs => NNode' n (Cons (ntsplice tr tr2) trs) 1024 | Cons tr trs => NNode' n (Cons (ntsplice tr tr2) trs)
1039 end = S (plus (ntsize tr2) (sum (map ntsize ls))) 1025 end = S (plus (ntsize tr2) (sum (map ntsize ls)))
1026
1040 ]] 1027 ]]
1041 1028
1042 After a few moments of squinting at this goal, it becomes apparent that we need to do a case analysis on the structure of [ls]. The rest is routine. *) 1029 After a few moments of squinting at this goal, it becomes apparent that we need to do a case analysis on the structure of [ls]. The rest is routine. *)
1043 1030
1044 destruct ls; crush. 1031 destruct ls; crush.
1060 (** * Manual Proofs About Constructors *) 1047 (** * Manual Proofs About Constructors *)
1061 1048
1062 (** It can be useful to understand how tactics like [discriminate] and [injection] work, so it is worth stepping through a manual proof of each kind. We will start with a proof fit for [discriminate]. *) 1049 (** It can be useful to understand how tactics like [discriminate] and [injection] work, so it is worth stepping through a manual proof of each kind. We will start with a proof fit for [discriminate]. *)
1063 1050
1064 Theorem true_neq_false : true <> false. 1051 Theorem true_neq_false : true <> false.
1052
1065 (* begin thide *) 1053 (* begin thide *)
1066 (** We begin with the tactic [red], which is short for "one step of reduction," to unfold the definition of logical negation. *) 1054 (** We begin with the tactic [red], which is short for "one step of reduction," to unfold the definition of logical negation. *)
1067 1055
1068 red. 1056 red.
1069 (** [[ 1057 (** [[
1070
1071 ============================ 1058 ============================
1072 true = false -> False 1059 true = false -> False
1060
1073 ]] 1061 ]]
1074 1062
1075 The negation is replaced with an implication of falsehood. We use the tactic [intro H] to change the assumption of the implication into a hypothesis named [H]. *) 1063 The negation is replaced with an implication of falsehood. We use the tactic [intro H] to change the assumption of the implication into a hypothesis named [H]. *)
1076 1064
1077 intro H. 1065 intro H.
1078 (** [[ 1066 (** [[
1079
1080 H : true = false 1067 H : true = false
1081 ============================ 1068 ============================
1082 False 1069 False
1070
1083 ]] 1071 ]]
1084 1072
1085 This is the point in the proof where we apply some creativity. We define a function whose utility will become clear soon. *) 1073 This is the point in the proof where we apply some creativity. We define a function whose utility will become clear soon. *)
1086 1074
1087 Definition f (b : bool) := if b then True else False. 1075 Definition f (b : bool) := if b then True else False.
1088 1076
1089 (** It is worth recalling the difference between the lowercase and uppercase versions of truth and falsehood: [True] and [False] are logical propositions, while [true] and [false] are boolean values that we can case-analyze. We have defined [f] such that our conclusion of [False] is computationally equivalent to [f false]. Thus, the [change] tactic will let us change the conclusion to [f false]. *) 1077 (** It is worth recalling the difference between the lowercase and uppercase versions of truth and falsehood: [True] and [False] are logical propositions, while [true] and [false] are boolean values that we can case-analyze. We have defined [f] such that our conclusion of [False] is computationally equivalent to [f false]. Thus, the [change] tactic will let us change the conclusion to [f false]. *)
1090 1078
1091 change (f false). 1079 change (f false).
1092 (** [[ 1080 (** [[
1093
1094 H : true = false 1081 H : true = false
1095 ============================ 1082 ============================
1096 f false 1083 f false
1084
1097 ]] 1085 ]]
1098 1086
1099 Now the righthand side of [H]'s equality appears in the conclusion, so we can rewrite, using the notation [<-] to request to replace the righthand side the equality with the lefthand side. *) 1087 Now the righthand side of [H]'s equality appears in the conclusion, so we can rewrite, using the notation [<-] to request to replace the righthand side the equality with the lefthand side. *)
1100 1088
1101 rewrite <- H. 1089 rewrite <- H.
1102 (** [[ 1090 (** [[
1103
1104 H : true = false 1091 H : true = false
1105 ============================ 1092 ============================
1106 f true 1093 f true
1094
1107 ]] 1095 ]]
1108 1096
1109 We are almost done. Just how close we are to done is revealed by computational simplification. *) 1097 We are almost done. Just how close we are to done is revealed by computational simplification. *)
1110 1098
1111 simpl. 1099 simpl.
1112 (** [[ 1100 (** [[
1113
1114 H : true = false 1101 H : true = false
1115 ============================ 1102 ============================
1116 True 1103 True
1104
1117 ]] *) 1105 ]] *)
1118 1106
1119 trivial. 1107 trivial.
1120 Qed. 1108 Qed.
1121 (* end thide *) 1109 (* end thide *)