# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1257968064 18000
# Node ID 6601384e7e14384928383066aca81332a0900a0a
# Parent  d1464997078dbf0d1db6838b11c5ef4220203970
Touch-ups to DataStruct

diff -r d1464997078d -r 6601384e7e14 Makefile
--- a/Makefile	Wed Nov 11 14:28:47 2009 -0500
+++ b/Makefile	Wed Nov 11 14:34:24 2009 -0500
@@ -45,7 +45,7 @@
 	cd latex ; latex $* ; latex $*
 
 latex/%.pdf: latex/%.dvi
-	cd latex ; pdflatex $* ; pdflatex $*
+	cd latex ; pdflatex $*
 
 html: Makefile $(VS) src/toc.html
 	mkdir -p html
diff -r d1464997078d -r 6601384e7e14 src/DataStruct.v
--- a/src/DataStruct.v	Wed Nov 11 14:28:47 2009 -0500
+++ b/src/DataStruct.v	Wed Nov 11 14:34:24 2009 -0500
@@ -830,7 +830,7 @@
 
    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.
 
-   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 function [replace] of type [forall A, filist A n -> fin n -> A -> filist A n], such that [replace l f x] should substitute [x] for the element in position [f] of [l].  A call to [replace] on a variable [l] of type [filist A (S n)] would probably be simplified to an explicit pair, even though we know nothing about the structure of [l] beyond its type.  In a proof involving many recursive types, this kind of unhelpful "simplification" can lead to rapid bloat in the sizes of subgoals.
+   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)].  This expression would be simplified to an explicit pair, even though we know nothing about the structure of [l] beyond its type.  In a proof involving many recursive types, this kind of unhelpful "simplification" can lead to rapid bloat in the sizes of subgoals.
 
    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.