Mercurial > cpdt > repo
comparison src/InductiveTypes.v @ 30:4887ddb1ad23
Parameterized inductives
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Mon, 08 Sep 2008 15:38:34 -0400 |
| parents | add8215ec72a |
| children | 1a82839f83b7 |
comparison
equal
deleted
inserted
replaced
| 29:add8215ec72a | 30:4887ddb1ad23 |
|---|---|
| 355 P NLeaf -> | 355 P NLeaf -> |
| 356 (forall n : nat_btree, | 356 (forall n : nat_btree, |
| 357 P n -> forall (n0 : nat) (n1 : nat_btree), P n1 -> P (NNode n n0 n1)) -> | 357 P n -> forall (n0 : nat) (n1 : nat_btree), P n1 -> P (NNode n n0 n1)) -> |
| 358 forall n : nat_btree, P n | 358 forall n : nat_btree, P n |
| 359 ]] *) | 359 ]] *) |
| 360 | |
| 361 | |
| 362 (** * Parameterized Types *) | |
| 363 | |
| 364 (** We can also define polymorphic inductive types, as with algebraic datatypes in Haskell and ML. *) | |
| 365 | |
| 366 Inductive list (T : Set) : Set := | |
| 367 | Nil : list T | |
| 368 | Cons : T -> list T -> list T. | |
| 369 | |
| 370 Fixpoint length T (ls : list T) : nat := | |
| 371 match ls with | |
| 372 | Nil => O | |
| 373 | Cons _ ls' => S (length ls') | |
| 374 end. | |
| 375 | |
| 376 Fixpoint app T (ls1 ls2 : list T) {struct ls1} : list T := | |
| 377 match ls1 with | |
| 378 | Nil => ls2 | |
| 379 | Cons x ls1' => Cons x (app ls1' ls2) | |
| 380 end. | |
| 381 | |
| 382 Theorem length_app : forall T (ls1 ls2 : list T), length (app ls1 ls2) | |
| 383 = plus (length ls1) (length ls2). | |
| 384 induction ls1; crush. | |
| 385 Qed. | |
| 386 | |
| 387 (** There is a useful shorthand for writing many definitions that share the same parameter, based on Coq's %\textit{%#<i>#section#</i>#%}% mechanism. The following block of code is equivalent to the above: *) | |
| 388 | |
| 389 (* begin hide *) | |
| 390 Reset list. | |
| 391 (* end hide *) | |
| 392 | |
| 393 Section list. | |
| 394 Variable T : Set. | |
| 395 | |
| 396 Inductive list : Set := | |
| 397 | Nil : list | |
| 398 | Cons : T -> list -> list. | |
| 399 | |
| 400 Fixpoint length (ls : list) : nat := | |
| 401 match ls with | |
| 402 | Nil => O | |
| 403 | Cons _ ls' => S (length ls') | |
| 404 end. | |
| 405 | |
| 406 Fixpoint app (ls1 ls2 : list) {struct ls1} : list := | |
| 407 match ls1 with | |
| 408 | Nil => ls2 | |
| 409 | Cons x ls1' => Cons x (app ls1' ls2) | |
| 410 end. | |
| 411 | |
| 412 Theorem length_app : forall ls1 ls2 : list, length (app ls1 ls2) | |
| 413 = plus (length ls1) (length ls2). | |
| 414 induction ls1; crush. | |
| 415 Qed. | |
| 416 End list. | |
| 417 | |
| 418 (** After we end the section, the [Variable]s we used are added as extra function parameters for each defined identifier, as needed. *) | |
| 419 | |
| 420 Check list. | |
| 421 (** [[ | |
| 422 | |
| 423 list | |
| 424 : Set -> Set | |
| 425 ]] *) | |
| 426 | |
| 427 Check Cons. | |
| 428 (** [[ | |
| 429 | |
| 430 Cons | |
| 431 : forall T : Set, T -> list T -> list T | |
| 432 ]] *) | |
| 433 | |
| 434 Check length. | |
| 435 (** [[ | |
| 436 | |
| 437 length | |
| 438 : forall T : Set, list T -> nat | |
| 439 ]] | |
| 440 | |
| 441 The extra parameter [T] is treated as a new argument to the induction principle, too. *) | |
| 442 | |
| 443 Check list_ind. | |
| 444 (** [[ | |
| 445 | |
| 446 list_ind | |
| 447 : forall (T : Set) (P : list T -> Prop), | |
| 448 P (Nil T) -> | |
| 449 (forall (t : T) (l : list T), P l -> P (Cons t l)) -> | |
| 450 forall l : list T, P l | |
| 451 ]] | |
| 452 | |
| 453 Thus, even though we just saw that [T] is added as an extra argument to the constructor [Cons], there is no quantifier for [T] in the type of the inductive case like there is for each of the other arguments. *) |