Certified Programming with Dependent Types: src/InductiveTypes.v comparison

comparison src/InductiveTypes.v @ 279:fabbc71abd80

Incorporate PC's comments on InductiveTypes

author	Adam Chlipala <adam@chlipala.net>
date	Fri, 01 Oct 2010 14:19:20 -0400
parents	c4b1c0de7af9
children	4146889930c5

comparison

equal deleted inserted replaced

-:e7ed2fddd29a
+:fabbc71abd80
 (** %\part{Basic Programming and Proving}
 \chapter{Introducing Inductive Types}% *)
-(** In a sense, CIC is built from just two relatively straightforward features: function types and inductive types.  From this modest foundation, we can prove effectively all of the theorems of math and carry out effectively all program verifications, with enough effort expended.  This chapter introduces induction and recursion for functional programming in Coq. *)
+(** In a sense, CIC is built from just two relatively straightforward features: function types and inductive types.  From this modest foundation, we can prove effectively all of the theorems of math and carry out effectively all program verifications, with enough effort expended.  This chapter introduces induction and recursion for functional programming in Coq.  Most of our examples reproduce functionality from the Coq standard library, and we have tried to copy the standard library's choices of identifiers, where possible, so many of the definitions here are already available in the default Coq environment. *)
 (** * Enumerations *)
 (** Coq inductive types generalize the algebraic datatypes found in Haskell and ML.  Confusingly enough, inductive types also generalize generalized algebraic datatypes (GADTs), by adding the possibility for type dependency.  Even so, it is worth backing up from the examples of the last chapter and going over basic, algebraic datatype uses of inductive datatypes, because the chance to prove things about the values of these types adds new wrinkles beyond usual practice in Haskell and ML.
 | true
 | false.
 (** We can use less vacuous pattern matching to define boolean negation. *)
-Definition not (b : bool) : bool :=
+Definition negb (b : bool) : bool :=
 match b with
 | true => false
 | false => true
 end.
 (** An alternative definition desugars to the above: *)
-Definition not' (b : bool) : bool :=
+Definition negb' (b : bool) : bool :=
 if b then false else true.
-(** We might want to prove that [not] is its own inverse operation. *)
+(** We might want to prove that [negb] is its own inverse operation. *)
-Theorem not_inverse : forall b : bool, not (not b) = b.
+Theorem negb_inverse : forall b : bool, negb (negb b) = b.
 (* begin thide *)
 destruct b.
 (** After we case-analyze on [b], we are left with one subgoal for each constructor of [bool].
 [[
 2 subgoals
 ============================
-not (not true) = true
+negb (negb true) = true
 ]]
 [[
 subgoal 2 is:
-not (not false) = false
+negb (negb false) = false
 ]]
 The first subgoal follows by Coq's rules of computation, so we can dispatch it easily: *)
 Qed.
 (* end thide *)
 (** Another theorem about booleans illustrates another useful tactic. *)
-Theorem not_ineq : forall b : bool, not b <> b.
+Theorem negb_ineq : forall b : bool, negb b <> b.
 (* begin thide *)
 destruct b; discriminate.
 Qed.
 (* end thide *)
 | Cons tr rest => conj (nat_tree_ind' tr) (list_nat_tree_ind rest)
 end.
 ]]
-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. *)
+Coq rejects this definition, saying "Recursive call to nat_tree_ind' has principal argument equal to "tr" instead of rest."  There is no deep theoretical reason why this program should be rejected; Coq applies incomplete termination-checking heuristics, and it is necessary to learn a few of the most important rules.  The term "nested inductive type" hints at the solution to this particular problem.  Just like true mutually-inductive types require mutually-recursive induction principles, nested types require nested recursion. *)
 Fixpoint nat_tree_ind' (tr : nat_tree) : P tr :=
 match tr with
 | NLeaf' => NLeaf'_case
 | NNode' n ls => NNode'_case n ls
 | Nil => I
 | Cons tr rest => conj (nat_tree_ind' tr) (list_nat_tree_ind rest)
 end) ls)
 end.
-(** We include an anonymous [fix] version of [list_nat_tree_ind] that is literally %\textit{%#<i>#nested#</i>#%}% inside the definition of the recursive function corresponding to the inductive definition that had the nested use of [list]. *)
+(** We include an anonymous [fix] version of [list_nat_tree_ind] that is literally %\textit{%#<i>#nested#</i>#%}% inside the definition of the recursive function corresponding to the inductive definition that had the nested use of [list].   *)
 End nat_tree_ind'.
 (** We can try our induction principle out by defining some recursive functions on [nat_tree]s and proving a theorem about them.  First, we define some helper functions that operate on lists. *)

Mercurial > cpdt > repo

comparison src/InductiveTypes.v @ 279:fabbc71abd80