## 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 |