Mercurial > cpdt > repo

comparison src/DataStruct.v @ 294:1b6c81e51799

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fixes added while proofreading JFR camera-ready
author Adam Chlipala <adam@chlipala.net>
date Thu, 09 Dec 2010 13:44:57 -0500
parents 693897f8e0cb
children 559ec7328410
comparison
equal deleted inserted replaced
293:e2dbc0f1c1e8 294:1b6c81e51799
790 exp'Denote (cfoldCond default tests bodies) 790 exp'Denote (cfoldCond default tests bodies)
791 = exp'Denote (Cond n tests bodies default). 791 = exp'Denote (Cond n tests bodies default).
792 induction n; crush; 792 induction n; crush;
793 match goal with 793 match goal with
794 | [ IHn : forall tests bodies, _, tests : _ -> _, bodies : _ -> _ |- _ ] => 794 | [ IHn : forall tests bodies, _, tests : _ -> _, bodies : _ -> _ |- _ ] =>
795 generalize (IHn (fun idx => tests (Some idx)) (fun idx => bodies (Some idx))); 795 specialize (IHn (fun idx => tests (Some idx)) (fun idx => bodies (Some idx)))
796 clear IHn; intro IHn
797 end; 796 end;
798 repeat (match goal with 797 repeat (match goal with
799 | [ |- context[match ?E with 798 | [ |- context[match ?E with
800 | NConst _ => _ 799 | NConst _ => _
801 | Plus _ _ => _ 800 | Plus _ _ => _
842 841
843 (** 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. 842 (** 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.
844 843
845 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. 844 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.
846 845
847 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. 846 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.
848 847
849 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. 848 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.
850 849
851 Reflexive encodings of data types are seen relatively rarely. As our examples demonstrated, manipulating index values manually can lead to hard-to-read code. A normal inductive type is generally easier to work with, once someone has gone through the trouble of implementing an induction principle manually with the techniques we studied in Chapter 3. For small developments, avoiding that kind of coding can justify the use of reflexive data structures. There are also some useful instances of co-inductive definitions with nested data structures (e.g., lists of values in the co-inductive type) that can only be deconstructed effectively with reflexive encoding of the nested structures. *) 850 Reflexive encodings of data types are seen relatively rarely. As our examples demonstrated, manipulating index values manually can lead to hard-to-read code. A normal inductive type is generally easier to work with, once someone has gone through the trouble of implementing an induction principle manually with the techniques we studied in Chapter 3. For small developments, avoiding that kind of coding can justify the use of reflexive data structures. There are also some useful instances of co-inductive definitions with nested data structures (e.g., lists of values in the co-inductive type) that can only be deconstructed effectively with reflexive encoding of the nested structures. *)
852 851