Mercurial > cpdt > repo
comparison src/DataStruct.v @ 406:fc03a67810e8
Typesetting pass over DataStruct
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Fri, 08 Jun 2012 14:31:17 -0400 |
parents | 05efde66559d |
children | 539ed97750bb |
comparison
equal
deleted
inserted
replaced
405:f0f76356de9c | 406:fc03a67810e8 |
---|---|
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 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 [[ | 48 [[ |
49 Fixpoint get n (ls : ilist n) : fin n -> A := | 49 Fixpoint get n (ls : ilist n) : fin n -> A := |
170 match ls with | 170 match ls with |
171 | Nil => Nil | 171 | Nil => Nil |
172 | Cons _ x ls' => Cons (f x) (imap ls') | 172 | Cons _ x ls' => Cons (f x) (imap ls') |
173 end. | 173 end. |
174 | 174 |
175 (** It is easy to prove that [get] %``%#"#distributes over#"#%''% [imap] calls. The only tricky bit is remembering to use our [dep_destruct] tactic in place of plain [destruct] when faced with a baffling tactic error message. *) | 175 (** It is easy to prove that [get] %``%#"#distributes over#"#%''% [imap] calls. *) |
176 | 176 |
177 (* EX: Prove that [get] distributes over [imap]. *) | 177 (* EX: Prove that [get] distributes over [imap]. *) |
178 | 178 |
179 (* begin thide *) | 179 (* begin thide *) |
180 Theorem get_imap : forall n (idx : fin n) (ls : ilist A n), | 180 Theorem get_imap : forall n (idx : fin n) (ls : ilist A n), |
182 induction ls; dep_destruct idx; crush. | 182 induction ls; dep_destruct idx; crush. |
183 Qed. | 183 Qed. |
184 (* end thide *) | 184 (* end thide *) |
185 End ilist_map. | 185 End ilist_map. |
186 | 186 |
187 (** The only tricky bit is remembering to use our [dep_destruct] tactic in place of plain [destruct] when faced with a baffling tactic error message. *) | |
187 | 188 |
188 (** * Heterogeneous Lists *) | 189 (** * Heterogeneous Lists *) |
189 | 190 |
190 (** Programmers who move to statically typed functional languages from scripting languages often complain about the requirement that every element of a list have the same type. With fancy type systems, we can partially lift this requirement. We can index a list type with a %``%#"#type-level#"#%''% list that explains what type each element of the list should have. This has been done in a variety of ways in Haskell using type classes, and we can do it much more cleanly and directly in Coq. *) | 191 (** Programmers who move to statically typed functional languages from scripting languages often complain about the requirement that every element of a list have the same type. With fancy type systems, we can partially lift this requirement. We can index a list type with a %``%#"#type-level#"#%''% list that explains what type each element of the list should have. This has been done in a variety of ways in Haskell using type classes, and we can do it much more cleanly and directly in Coq. *) |
191 | 192 |
389 match n with | 390 match n with |
390 | O => Empty_set | 391 | O => Empty_set |
391 | S n' => option (ffin n') | 392 | S n' => option (ffin n') |
392 end. | 393 end. |
393 | 394 |
394 (** We express that there are no index values when [n = O], by defining such indices as type [Empty_set]; and we express that, at [n = S n'], there is a choice between picking the first element of the list (represented as [None]) or choosing a later element (represented by [Some idx], where [idx] is an index into the list tail). For instance, the three values of type [ffin 3] are [None], [Some None], and [Some (][Some None)]. *) | 395 (** We express that there are no index values when [n = O], by defining such indices as type [Empty_set]; and we express that, at [n = S n'], there is a choice between picking the first element of the list (represented as [None]) or choosing a later element (represented by [Some idx], where [idx] is an index into the list tail). For instance, the three values of type [ffin 3] are [None], [Some None], and [Some (Some None)]. *) |
395 | 396 |
396 Fixpoint fget (n : nat) : filist n -> ffin n -> A := | 397 Fixpoint fget (n : nat) : filist n -> ffin n -> A := |
397 match n with | 398 match n with |
398 | O => fun _ idx => match idx with end | 399 | O => fun _ idx => match idx with end |
399 | S n' => fun ls idx => | 400 | S n' => fun ls idx => |
805 match goal with | 806 match goal with |
806 | [ IHn : forall tests bodies, _, tests : _ -> _, bodies : _ -> _ |- _ ] => | 807 | [ IHn : forall tests bodies, _, tests : _ -> _, bodies : _ -> _ |- _ ] => |
807 specialize (IHn (fun idx => tests (Some idx)) (fun idx => bodies (Some idx))) | 808 specialize (IHn (fun idx => tests (Some idx)) (fun idx => bodies (Some idx))) |
808 end; | 809 end; |
809 repeat (match goal with | 810 repeat (match goal with |
810 | [ |- context[match ?E with | 811 | [ |- context[match ?E with NConst _ => _ | _ => _ end] ] => dep_destruct E |
811 | NConst _ => _ | |
812 | Plus _ _ => _ | |
813 | Eq _ _ => _ | |
814 | BConst _ => _ | |
815 | Cond _ _ _ _ _ => _ | |
816 end] ] => dep_destruct E | |
817 | [ |- context[if ?B then _ else _] ] => destruct B | 812 | [ |- context[if ?B then _ else _] ] => destruct B |
818 end; crush). | 813 end; crush). |
819 Qed. | 814 Qed. |
820 | 815 |
821 (** It is also useful to know that the result of a call to [cond] is not changed by substituting new tests and bodies functions, so long as the new functions have the same input-output behavior as the old. It turns out that, in Coq, it is not possible to prove in general that functions related in this way are equal. We treat this issue with our discussion of axioms in a later chapter. For now, it suffices to prove that the particular function [cond] is _extensional_; that is, it is unaffected by substitution of functions with input-output equivalents. *) | 816 (** It is also useful to know that the result of a call to [cond] is not changed by substituting new tests and bodies functions, so long as the new functions have the same input-output behavior as the old. It turns out that, in Coq, it is not possible to prove in general that functions related in this way are equal. We treat this issue with our discussion of axioms in a later chapter. For now, it suffices to prove that the particular function [cond] is _extensional_; that is, it is unaffected by substitution of functions with input-output equivalents. *) |
853 | 848 |
854 (** It is not always clear which of these representation techniques to apply in a particular situation, but I will try to summarize the pros and cons of each. | 849 (** It is not always clear which of these representation techniques to apply in a particular situation, but I will try to summarize the pros and cons of each. |
855 | 850 |
856 Inductive types are often the most pleasant to work with, after someone has spent the time implementing some basic library functions for them, using fancy [match] annotations. Many aspects of Coq's logic and tactic support are specialized to deal with inductive types, and you may miss out if you use alternate encodings. | 851 Inductive types are often the most pleasant to work with, after someone has spent the time implementing some basic library functions for them, using fancy [match] annotations. Many aspects of Coq's logic and tactic support are specialized to deal with inductive types, and you may miss out if you use alternate encodings. |
857 | 852 |
858 Recursive types usually involve much less initial effort, but they can be less convenient to use with proof automation. For instance, the [simpl] tactic (which is among the ingredients in [crush]) will sometimes be overzealous in simplifying uses of functions over recursive types. Consider a call [get l f], where variable [l] has type [filist A (][S n)]. The type of [l] would be simplified to an explicit pair type. In a proof involving many recursive types, this kind of unhelpful %``%#"#simplification#"#%''% can lead to rapid bloat in the sizes of subgoals. Even worse, it can prevent syntactic pattern-matching, like in cases where [filist] is expected but a pair type is found in the %``%#"#simplified#"#%''% version. The same problem applies to applications of recursive functions to values in recursive types: the recursive function call may %``%#"#simplify#"#%''% when the top-level structure of the type index but not the recursive value is known, because such functions are generally defined by recursion on the index, not the value. | 853 Recursive types usually involve much less initial effort, but they can be less convenient to use with proof automation. For instance, the [simpl] tactic (which is among the ingredients in [crush]) will sometimes be overzealous in simplifying uses of functions over recursive types. Consider a call [get l f], where variable [l] has type [filist A (S n)]. The type of [l] would be simplified to an explicit pair type. In a proof involving many recursive types, this kind of unhelpful %``%#"#simplification#"#%''% can lead to rapid bloat in the sizes of subgoals. Even worse, it can prevent syntactic pattern-matching, like in cases where [filist] is expected but a pair type is found in the %``%#"#simplified#"#%''% version. The same problem applies to applications of recursive functions to values in recursive types: the recursive function call may %``%#"#simplify#"#%''% when the top-level structure of the type index but not the recursive value is known, because such functions are generally defined by recursion on the index, not the value. |
859 | 854 |
860 Another disadvantage of recursive types is that they only apply to type families whose indices determine their %``%#"#skeletons.#"#%''% This is not true for all data structures; a good counterexample comes from the richly typed programming language syntax types we have used several times so far. The fact that a piece of syntax has type [Nat] tells us nothing about the tree structure of that syntax. | 855 Another disadvantage of recursive types is that they only apply to type families whose indices determine their %``%#"#skeletons.#"#%''% This is not true for all data structures; a good counterexample comes from the richly typed programming language syntax types we have used several times so far. The fact that a piece of syntax has type [Nat] tells us nothing about the tree structure of that syntax. |
861 | 856 |
862 Finally, Coq type inference can be more helpful in constructing values in inductive types. Application of a particular constructor of that type tells Coq what to expect from the arguments, while, for instance, forming a generic pair does not make clear an intention to interpret the value as belonging to a particular recursive type. This downside can be mitigated to an extent by writing %``%#"#constructor#"#%''% functions for a recursive type, mirroring the definition of the corresponding inductive type. | 857 Finally, Coq type inference can be more helpful in constructing values in inductive types. Application of a particular constructor of that type tells Coq what to expect from the arguments, while, for instance, forming a generic pair does not make clear an intention to interpret the value as belonging to a particular recursive type. This downside can be mitigated to an extent by writing %``%#"#constructor#"#%''% functions for a recursive type, mirroring the definition of the corresponding inductive type. |
863 | 858 |