### comparison src/DataStruct.v @ 480:f38a3af9dd17

Batch of changes based on proofreader feedback
comparison
equal 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.