Mercurial > cpdt > repo
comparison src/DataStruct.v @ 480:f38a3af9dd17
Batch of changes based on proofreader feedback
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Fri, 30 Nov 2012 11:57:55 -0500 |
parents | f02b698aadb1 |
children | 31258618ef73 |
comparison
equal
deleted
inserted
replaced
479:40a9a36844d6 | 480:f38a3af9dd17 |
---|---|
39 (* begin thide *) | 39 (* begin thide *) |
40 Inductive fin : nat -> Set := | 40 Inductive fin : nat -> Set := |
41 | First : forall n, fin (S n) | 41 | First : forall n, fin (S n) |
42 | Next : forall n, fin n -> fin (S n). | 42 | Next : forall n, fin n -> fin (S n). |
43 | 43 |
44 (** An instance of [fin] is essentially a more richly typed copy of the natural numbers. Every element is a [First] iterated through applying [Next] a number of times that indicates which number is being selected. For instance, the three values of type [fin 3] are [First 2], [Next (First 1)], and [Next (Next (First 0))]. | 44 (** An instance of [fin] is essentially a more richly typed copy of a prefix of the natural numbers. The type [fin n] is isomorphic to [{m : nat | m < n}]. Every element is a [First] iterated through applying [Next] a number of times that indicates which number is being selected. For instance, the three values of type [fin 3] are [First 2], [Next (First 1)], and [Next (Next (First 0))]. |
45 | 45 |
46 Now it is easy to pick a [Prop]-free type for a selection function. As usual, our first implementation attempt will not convince the type checker, and we will attack the deficiencies one at a time. | 46 Now it is easy to pick a [Prop]-free type for a selection function. As usual, our first implementation attempt will not convince the type checker, and we will attack the deficiencies one at a time. |
47 [[ | 47 [[ |
48 Fixpoint get n (ls : ilist n) : fin n -> A := | 48 Fixpoint get n (ls : ilist n) : fin n -> A := |
49 match ls with | 49 match ls with |
53 | First _ => x | 53 | First _ => x |
54 | Next _ idx' => get ls' idx' | 54 | Next _ idx' => get ls' idx' |
55 end | 55 end |
56 end. | 56 end. |
57 ]] | 57 ]] |
58 %\vspace{-.15in}%We apply the usual wisdom of delaying arguments in [Fixpoint]s so that they may be included in [return] clauses. This still leaves us with a quandary in each of the [match] cases. First, we need to figure out how to take advantage of the contradiction in the [Nil] case. Every [fin] has a type of the form [S n], which cannot unify with the [O] value that we learn for [n] in the [Nil] case. The solution we adopt is another case of [match]-within-[return]. | 58 %\vspace{-.15in}%We apply the usual wisdom of delaying arguments in [Fixpoint]s so that they may be included in [return] clauses. This still leaves us with a quandary in each of the [match] cases. First, we need to figure out how to take advantage of the contradiction in the [Nil] case. Every [fin] has a type of the form [S n], which cannot unify with the [O] value that we learn for [n] in the [Nil] case. The solution we adopt is another case of [match]-within-[return], with the [return] clause chosen carefully so that it returns the proper type [A] in case the [fin] index is [O], which we know is true here; and so that it returns an easy-to-inhabit type [unit] in the remaining, impossible cases, which nonetheless appear explicitly in the body of the [match]. |
59 [[ | 59 [[ |
60 Fixpoint get n (ls : ilist n) : fin n -> A := | 60 Fixpoint get n (ls : ilist n) : fin n -> A := |
61 match ls with | 61 match ls with |
62 | Nil => fun idx => | 62 | Nil => fun idx => |
63 match idx in fin n' return (match n' with | 63 match idx in fin n' return (match n' with |
198 (* begin thide *) | 198 (* begin thide *) |
199 Inductive hlist : list A -> Type := | 199 Inductive hlist : list A -> Type := |
200 | HNil : hlist nil | 200 | HNil : hlist nil |
201 | HCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls). | 201 | HCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls). |
202 | 202 |
203 (** We can implement a variant of the last section's [get] function for [hlist]s. To get the dependent typing to work out, we will need to index our element selectors by the types of data that they point to.%\index{Gallina terms!member}% *) | 203 (** We can implement a variant of the last section's [get] function for [hlist]s. To get the dependent typing to work out, we will need to index our element selectors (in type family [member]) by the types of data that they point to.%\index{Gallina terms!member}% *) |
204 | 204 |
205 (* end thide *) | 205 (* end thide *) |
206 (* EX: Define an analogue to [get] for [hlist]s. *) | 206 (* EX: Define an analogue to [get] for [hlist]s. *) |
207 | 207 |
208 (* begin thide *) | 208 (* begin thide *) |
246 | 246 |
247 Implicit Arguments HFirst [A elm ls]. | 247 Implicit Arguments HFirst [A elm ls]. |
248 Implicit Arguments HNext [A elm x ls]. | 248 Implicit Arguments HNext [A elm x ls]. |
249 (* end thide *) | 249 (* end thide *) |
250 | 250 |
251 (** By putting the parameters [A] and [B] in [Type], we allow some very higher-order uses. For instance, one use of [hlist] is for the simple heterogeneous lists that we referred to earlier. *) | 251 (** By putting the parameters [A] and [B] in [Type], we enable fancier kinds of polymorphism than in mainstream functional languages. For instance, one use of [hlist] is for the simple heterogeneous lists that we referred to earlier. *) |
252 | 252 |
253 Definition someTypes : list Set := nat :: bool :: nil. | 253 Definition someTypes : list Set := nat :: bool :: nil. |
254 | 254 |
255 (* begin thide *) | 255 (* begin thide *) |
256 | 256 |
368 (** We are starting to develop the tools behind dependent typing's amazing advantage over alternative approaches in several important areas. Here, we have implemented complete syntax, typing rules, and evaluation semantics for simply typed lambda calculus without even needing to define a syntactic substitution operation. We did it all without a single line of proof, and our implementation is manifestly executable. Other, more common approaches to language formalization often state and prove explicit theorems about type safety of languages. In the above example, we got type safety, termination, and other meta-theorems for free, by reduction to CIC, which we know has those properties. *) | 368 (** We are starting to develop the tools behind dependent typing's amazing advantage over alternative approaches in several important areas. Here, we have implemented complete syntax, typing rules, and evaluation semantics for simply typed lambda calculus without even needing to define a syntactic substitution operation. We did it all without a single line of proof, and our implementation is manifestly executable. Other, more common approaches to language formalization often state and prove explicit theorems about type safety of languages. In the above example, we got type safety, termination, and other meta-theorems for free, by reduction to CIC, which we know has those properties. *) |
369 | 369 |
370 | 370 |
371 (** * Recursive Type Definitions *) | 371 (** * Recursive Type Definitions *) |
372 | 372 |
373 (** %\index{recursive type definition}%There is another style of datatype definition that leads to much simpler definitions of the [get] and [hget] definitions above. Because Coq supports "type-level computation," we can redo our inductive definitions as _recursive_ definitions. *) | 373 (** %\index{recursive type definition}%There is another style of datatype definition that leads to much simpler definitions of the [get] and [hget] definitions above. Because Coq supports "type-level computation," we can redo our inductive definitions as _recursive_ definitions. Here we will preface type names with the letter [f] to indicate that they are based on explicit recursive _function_ definitions. *) |
374 | 374 |
375 (* EX: Come up with an alternate [ilist] definition that makes it easier to write [get]. *) | 375 (* EX: Come up with an alternate [ilist] definition that makes it easier to write [get]. *) |
376 | 376 |
377 Section filist. | 377 Section filist. |
378 Variable A : Set. | 378 Variable A : Set. |