Mercurial > cpdt > repo

comparison src/DataStruct.v @ 501:28c2fa8af4eb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pass through Chapter 9
author Adam Chlipala <adam@chlipala.net>
date Tue, 05 Feb 2013 12:38:25 -0500
parents 31258618ef73
children ed829eaa91b2
comparison
equal deleted inserted replaced
500:8303abe4a61f 501:28c2fa8af4eb
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 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))]. 44 (** An instance of [fin] is essentially a more richly typed copy of a prefix 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))].
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
274 (** We can also build indexed lists of pairs in this way. *) 274 (** We can also build indexed lists of pairs in this way. *)
275 275
276 Example somePairs : hlist (fun T : Set => T * T)%type someTypes := 276 Example somePairs : hlist (fun T : Set => T * T)%type someTypes :=
277 HCons (1, 2) (HCons (true, false) HNil). 277 HCons (1, 2) (HCons (true, false) HNil).
278 278
279 (** There are many more useful applications of heterogeneous lists, based on different choices of the first argument to [hlist]. *) 279 (** There are many other useful applications of heterogeneous lists, based on different choices of the first argument to [hlist]. *)
280 280
281 (* end thide *) 281 (* end thide *)
282 282
283 283
284 (** ** A Lambda Calculus Interpreter *) 284 (** ** A Lambda Calculus Interpreter *)
568 << 568 <<
569 Error: Non strictly positive occurrence of "tree" in 569 Error: Non strictly positive occurrence of "tree" in
570 "forall n : nat, filist tree n -> tree" 570 "forall n : nat, filist tree n -> tree"
571 >> 571 >>
572 572
573 The special-case rule for nested datatypes only works with nested uses of other inductive types, which could be replaced with uses of new mutually inductive types. We defined [filist] recursively, so it may not be used for nested recursion. 573 The special-case rule for nested datatypes only works with nested uses of other inductive types, which could be replaced with uses of new mutually inductive types. We defined [filist] recursively, so it may not be used in nested inductive definitions.
574 574
575 Our final solution uses yet another of the inductive definition techniques introduced in Chapter 3, %\index{reflexive inductive type}%reflexive types. Instead of merely using [fin] to get elements out of [ilist], we can _define_ [ilist] in terms of [fin]. For the reasons outlined above, it turns out to be easier to work with [ffin] in place of [fin]. *) 575 Our final solution uses yet another of the inductive definition techniques introduced in Chapter 3, %\index{reflexive inductive type}%reflexive types. Instead of merely using [fin] to get elements out of [ilist], we can _define_ [ilist] in terms of [fin]. For the reasons outlined above, it turns out to be easier to work with [ffin] in place of [fin]. *)
576 576
577 Inductive tree : Set := 577 Inductive tree : Set :=
578 | Leaf : A -> tree 578 | Leaf : A -> tree