Mercurial > cpdt > repo

comparison src/InductiveTypes.v @ 205:f05514cc6c0d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
'make doc' works with 8.2
author Adam Chlipala <adamc@hcoop.net>
date Fri, 06 Nov 2009 12:15:05 -0500
parents 8caa3b3f8fc0
children b9e9ff52913c
comparison
equal deleted inserted replaced
204:cbf2f74a5130 205:f05514cc6c0d
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
67 ]]
68
66 ...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 ...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.
67 70
68 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: *)
69 72
70 Check unit_ind. 73 Check unit_ind.
663 Definition uhoh (t : term) : term := 666 Definition uhoh (t : term) : term :=
664 match t with 667 match t with
665 | Abs f => f t 668 | Abs f => f t
666 | _ => t 669 | _ => t
667 end. 670 end.
671
672 ]]
668 673
669 Using an informal idea of Coq's semantics, it is easy to verify that the application [uhoh (Abs uhoh)] will run forever. This would be a mere curiosity in OCaml and Haskell, where non-termination is commonplace, though the fact that we have a non-terminating program without explicit recursive function definitions is unusual. 674 Using an informal idea of Coq's semantics, it is easy to verify that the application [uhoh (Abs uhoh)] will run forever. This would be a mere curiosity in OCaml and Haskell, where non-termination is commonplace, though the fact that we have a non-terminating program without explicit recursive function definitions is unusual.
670 675
671 For Coq, however, this would be a disaster. The possibility of writing such a function would destroy all our confidence that proving a theorem means anything. Since Coq combines programs and proofs in one language, we would be able to prove every theorem with an infinite loop. 676 For Coq, however, this would be a disaster. The possibility of writing such a function would destroy all our confidence that proving a theorem means anything. Since Coq combines programs and proofs in one language, we would be able to prove every theorem with an infinite loop.
672 677
941 match ls return (All P ls) with 946 match ls return (All P ls) with
942 | Nil => I 947 | Nil => I
943 | 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)
944 end. 949 end.
945 950
951 ]]
952
946 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. *) 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. *)
947 954
948 Fixpoint nat_tree_ind' (tr : nat_tree) : P tr := 955 Fixpoint nat_tree_ind' (tr : nat_tree) : P tr :=
949 match tr return (P tr) with 956 match tr return (P tr) with
950 | NLeaf' => NLeaf'_case 957 | NLeaf' => NLeaf'_case