Mercurial > cpdt > repo
comparison src/InductiveTypes.v @ 31:1a82839f83b7
Mutual induction
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Mon, 08 Sep 2008 16:00:02 -0400 |
| parents | 4887ddb1ad23 |
| children | 77e1a7eda0b8 |
comparison
equal
deleted
inserted
replaced
| 30:4887ddb1ad23 | 31:1a82839f83b7 |
|---|---|
| 449 (forall (t : T) (l : list T), P l -> P (Cons t l)) -> | 449 (forall (t : T) (l : list T), P l -> P (Cons t l)) -> |
| 450 forall l : list T, P l | 450 forall l : list T, P l |
| 451 ]] | 451 ]] |
| 452 | 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. *) | 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. *) |
| 454 | |
| 455 | |
| 456 (** * Mutually Inductive Types *) | |
| 457 | |
| 458 (** We can define inductive types that refer to each other: *) | |
| 459 | |
| 460 Inductive even_list : Set := | |
| 461 | ENil : even_list | |
| 462 | ECons : nat -> odd_list -> even_list | |
| 463 | |
| 464 with odd_list : Set := | |
| 465 | OCons : nat -> even_list -> odd_list. | |
| 466 | |
| 467 Fixpoint elength (el : even_list) : nat := | |
| 468 match el with | |
| 469 | ENil => O | |
| 470 | ECons _ ol => S (olength ol) | |
| 471 end | |
| 472 | |
| 473 with olength (ol : odd_list) : nat := | |
| 474 match ol with | |
| 475 | OCons _ el => S (elength el) | |
| 476 end. | |
| 477 | |
| 478 Fixpoint eapp (el1 el2 : even_list) {struct el1} : even_list := | |
| 479 match el1 with | |
| 480 | ENil => el2 | |
| 481 | ECons n ol => ECons n (oapp ol el2) | |
| 482 end | |
| 483 | |
| 484 with oapp (ol : odd_list) (el : even_list) {struct ol} : odd_list := | |
| 485 match ol with | |
| 486 | OCons n el' => OCons n (eapp el' el) | |
| 487 end. | |
| 488 | |
| 489 (** Everything is going roughly the same as in past examples, until we try to prove a theorem similar to those that came before. *) | |
| 490 | |
| 491 Theorem elength_eapp : forall el1 el2 : even_list, | |
| 492 elength (eapp el1 el2) = plus (elength el1) (elength el2). | |
| 493 induction el1; crush. | |
| 494 | |
| 495 (** One goal remains: [[ | |
| 496 | |
| 497 n : nat | |
| 498 o : odd_list | |
| 499 el2 : even_list | |
| 500 ============================ | |
| 501 S (olength (oapp o el2)) = S (plus (olength o) (elength el2)) | |
| 502 ]] | |
| 503 | |
| 504 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. *) | |
| 505 | |
| 506 Abort. | |
| 507 Check even_list_ind. | |
| 508 (** [[ | |
| 509 | |
| 510 even_list_ind | |
| 511 : forall P : even_list -> Prop, | |
| 512 P ENil -> | |
| 513 (forall (n : nat) (o : odd_list), P (ECons n o)) -> | |
| 514 forall e : even_list, P e | |
| 515 ]] | |
| 516 | |
| 517 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. *) | |
| 518 | |
| 519 Scheme even_list_mut := Induction for even_list Sort Prop | |
| 520 with odd_list_mut := Induction for odd_list Sort Prop. | |
| 521 | |
| 522 Check even_list_mut. | |
| 523 (** [[ | |
| 524 | |
| 525 even_list_mut | |
| 526 : forall (P : even_list -> Prop) (P0 : odd_list -> Prop), | |
| 527 P ENil -> | |
| 528 (forall (n : nat) (o : odd_list), P0 o -> P (ECons n o)) -> | |
| 529 (forall (n : nat) (e : even_list), P e -> P0 (OCons n e)) -> | |
| 530 forall e : even_list, P e | |
| 531 ]] | |
| 532 | |
| 533 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. *) | |
| 534 | |
| 535 Theorem n_plus_O' : forall n : nat, plus n O = n. | |
| 536 apply (nat_ind (fun n => plus n O = n)); crush. | |
| 537 Qed. | |
| 538 | |
| 539 (** From this example, we can see that [induction] is not magic. It only does some bookkeeping for us to make it easy to apply a theorem, which we can do directly with the [apply] tactic. We apply not just an identifier but a partial application of it, specifying the predicate we mean to prove holds for all naturals. | |
| 540 | |
| 541 This technique generalizes to our mutual example: *) | |
| 542 | |
| 543 Theorem elength_eapp : forall el1 el2 : even_list, | |
| 544 elength (eapp el1 el2) = plus (elength el1) (elength el2). | |
| 545 apply (even_list_mut | |
| 546 (fun el1 : even_list => forall el2 : even_list, | |
| 547 elength (eapp el1 el2) = plus (elength el1) (elength el2)) | |
| 548 (fun ol : odd_list => forall el : even_list, | |
| 549 olength (oapp ol el) = plus (olength ol) (elength el))); crush. | |
| 550 Qed. | |
| 551 | |
| 552 (** We simply need to specify two predicates, one for each of the mutually inductive types. In general, it would not be a good idea to assume that a proof assistant could infer extra predicates, so this way of applying mutual induction is about as straightforward as we could hope for. *) |