Mercurial > cpdt > repo

comparison src/InductiveTypes.v @ 493:4a663981b699

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pass through Chapter 3
author Adam Chlipala <adam@chlipala.net>
date Fri, 18 Jan 2013 15:12:03 -0500
parents 31258618ef73
children ed829eaa91b2
comparison
equal deleted inserted replaced
492:fa2eb72446a8 493:4a663981b699
67 One of the first types we introduce will be [bool], with constructors [true] and [false]. Newcomers to Coq often wonder about the distinction between [True] and [true] and the distinction between [False] and [false]. One glib answer is that [True] and [False] are types, but [true] and [false] are not. A more useful answer is that Coq's metatheory guarantees that any term of type [bool] _evaluates_ to either [true] or [false]. This means that we have an _algorithm_ for answering any question phrased as an expression of type [bool]. Conversely, most propositions do not evaluate to [True] or [False]; the language of inductively defined propositions is much richer than that. We ought to be glad that we have no algorithm for deciding our formalized version of mathematical truth, since otherwise it would be clear that we could not formalize undecidable properties, like almost any interesting property of general-purpose programs. *) 67 One of the first types we introduce will be [bool], with constructors [true] and [false]. Newcomers to Coq often wonder about the distinction between [True] and [true] and the distinction between [False] and [false]. One glib answer is that [True] and [False] are types, but [true] and [false] are not. A more useful answer is that Coq's metatheory guarantees that any term of type [bool] _evaluates_ to either [true] or [false]. This means that we have an _algorithm_ for answering any question phrased as an expression of type [bool]. Conversely, most propositions do not evaluate to [True] or [False]; the language of inductively defined propositions is much richer than that. We ought to be glad that we have no algorithm for deciding our formalized version of mathematical truth, since otherwise it would be clear that we could not formalize undecidable properties, like almost any interesting property of general-purpose programs. *)
68 68
69 69
70 (** * Enumerations *) 70 (** * Enumerations *)
71 71
72 (** Coq inductive types generalize the %\index{algebraic datatypes}%algebraic datatypes found in %\index{Haskell}%Haskell and %\index{ML}%ML. Confusingly enough, inductive types also generalize %\index{generalized algebraic datatypes}%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. 72 (** Coq inductive types generalize the %\index{algebraic datatypes}%algebraic datatypes found in %\index{Haskell}%Haskell and %\index{ML}%ML. Confusingly enough, inductive types also generalize %\index{generalized algebraic datatypes}%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.
73 73
74 The singleton type [unit] is an inductive type:%\index{Gallina terms!unit}\index{Gallina terms!tt}% *) 74 The singleton type [unit] is an inductive type:%\index{Gallina terms!unit}\index{Gallina terms!tt}% *)
75 75
76 Inductive unit : Set := 76 Inductive unit : Set :=
77 | tt. 77 | tt.
149 149
150 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]: *) 150 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]: *)
151 151
152 Definition e2u (e : Empty_set) : unit := match e with end. 152 Definition e2u (e : Empty_set) : unit := match e with end.
153 153
154 (** We employ [match] pattern matching as in the last chapter. Since we match on a value whose type has no constructors, there is no need to provide any branches. This idiom may look familiar; we employed it with proofs of [False] in the last section. In fact, [Empty_set] is the Curry-Howard equivalent of [False]. As for why [Empty_set] starts with a capital letter and not a lowercase letter like [unit] does, we must refer the reader to the authors of the Coq standard library, to which we try to be faithful. 154 (** We employ [match] pattern matching as in the last chapter. Since we match on a value whose type has no constructors, there is no need to provide any branches. It turns out that [Empty_set] is the Curry-Howard equivalent of [False]. As for why [Empty_set] starts with a capital letter and not a lowercase letter like [unit] does, we must refer the reader to the authors of the Coq standard library, to which we try to be faithful.
155 155
156 %\medskip% 156 %\medskip%
157 157
158 Moving up the ladder of complexity, we can define the Booleans:%\index{Gallina terms!bool}\index{Gallina terms!true}\index{Gallina terms!false}% *) 158 Moving up the ladder of complexity, we can define the Booleans:%\index{Gallina terms!bool}\index{Gallina terms!true}\index{Gallina terms!false}% *)
159 159
799 end 799 end
800 : forall P : nat -> Type, 800 : forall P : nat -> Type,
801 P O -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n 801 P O -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
802 ]] 802 ]]
803 803
804 The only new wrinkle heres are, first, an anonymous recursive function definition, using the %\index{Gallina terms!fix}%[fix] keyword of Gallina (which is like [fun] with recursion supported); and, second, the annotations on the [match] expression. This is a%\index{dependent pattern matching}% _dependently typed_ pattern match, because the _type_ of the expression depends on the _value_ being matched on. We will meet more involved examples later, especially in Part II of the book. 804 The only new wrinkles here are, first, an anonymous recursive function definition, using the %\index{Gallina terms!fix}%[fix] keyword of Gallina (which is like [fun] with recursion supported); and, second, the annotations on the [match] expression. This is a%\index{dependent pattern matching}% _dependently typed_ pattern match, because the _type_ of the expression depends on the _value_ being matched on. We will meet more involved examples later, especially in Part II of the book.
805 805
806 %\index{type inference}%Type inference for dependent pattern matching is undecidable, which can be proved by reduction from %\index{higher-order unification}%higher-order unification%~\cite{HOU}%. Thus, we often find ourselves needing to annotate our programs in a way that explains dependencies to the type checker. In the example of [nat_rect], we have an %\index{Gallina terms!as}%[as] clause, which binds a name for the discriminee; and a %\index{Gallina terms!return}%[return] clause, which gives a way to compute the [match] result type as a function of the discriminee. 806 %\index{type inference}%Type inference for dependent pattern matching is undecidable, which can be proved by reduction from %\index{higher-order unification}%higher-order unification%~\cite{HOU}%. Thus, we often find ourselves needing to annotate our programs in a way that explains dependencies to the type checker. In the example of [nat_rect], we have an %\index{Gallina terms!as}%[as] clause, which binds a name for the discriminee; and a %\index{Gallina terms!return}%[return] clause, which gives a way to compute the [match] result type as a function of the discriminee.
807 807
808 To prove that [nat_rect] is nothing special, we can reimplement it manually. *) 808 To prove that [nat_rect] is nothing special, we can reimplement it manually. *)
809 809