Mercurial > cpdt > repo

changeset 417:539ed97750bb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update for Coq trunk version intended for final 8.4 release
author Adam Chlipala <adam@chlipala.net>
date Tue, 17 Jul 2012 16:37:58 -0400
parents ded318830bb0
children eda5f4eb21b4
files src/CpdtTactics.v src/DataStruct.v src/InductiveTypes.v src/MoreDep.v src/StackMachine.v src/Universes.v
diffstat 6 files changed, 25 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/src/CpdtTactics.v	Wed Jun 13 11:14:00 2012 -0400
+++ b/src/CpdtTactics.v	Tue Jul 17 16:37:58 2012 -0400
@@ -214,7 +214,7 @@
   let x := fresh "x" in
     remember E as x; simpl in x; dependent destruction x;
       try match goal with
-            | [ H : _ = E |- _ ] => rewrite <- H in *; clear H
+            | [ H : _ = E |- _ ] => try rewrite <- H in *; clear H
           end.
 
 (** Nuke all hypotheses that we can get away with, without invalidating the goal statement. *)
--- a/src/DataStruct.v	Wed Jun 13 11:14:00 2012 -0400
+++ b/src/DataStruct.v	Tue Jul 17 16:37:58 2012 -0400
@@ -773,14 +773,14 @@
     | Plus e1 e2 =>
       let e1' := cfold e1 in
       let e2' := cfold e2 in
-      match e1', e2' return _ with
+      match e1', e2' return exp' Nat with
         | NConst n1, NConst n2 => NConst (n1 + n2)
         | _, _ => Plus e1' e2'
       end
     | Eq e1 e2 =>
       let e1' := cfold e1 in
       let e2' := cfold e2 in
-      match e1', e2' return _ with
+      match e1', e2' return exp' Bool with
         | NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false)
         | _, _ => Eq e1' e2'
       end
--- a/src/InductiveTypes.v	Wed Jun 13 11:14:00 2012 -0400
+++ b/src/InductiveTypes.v	Tue Jul 17 16:37:58 2012 -0400
@@ -342,7 +342,7 @@
 
 (** The [injection] tactic refers to a premise by number, adding new equalities between the corresponding arguments of equated terms that are formed with the same constructor.  We end up needing to prove [n = m -> n = m], so it is unsurprising that a tactic named [trivial] is able to finish the proof.
 
-There is also a very useful tactic called %\index{tactics!congruence}%[congruence] that can prove this theorem immediately.  [congruence] generalizes [discriminate] and [injection], and it also adds reasoning about the general properties of equality, such as that a function returns equal results on equal arguments.  That is, [congruence] is a%\index{theory of equality and uninterpreted functions}% _complete decision procedure for the theory of equality and uninterpreted functions_, plus some smarts about inductive types.
+There is also a very useful tactic called %\index{tactics!congruence}%[congruence] that can prove this theorem immediately.  The [congruence] tactic generalizes [discriminate] and [injection], and it also adds reasoning about the general properties of equality, such as that a function returns equal results on equal arguments.  That is, [congruence] is a%\index{theory of equality and uninterpreted functions}% _complete decision procedure for the theory of equality and uninterpreted functions_, plus some smarts about inductive types.
 
 %\medskip%
 
--- a/src/MoreDep.v	Wed Jun 13 11:14:00 2012 -0400
+++ b/src/MoreDep.v	Tue Jul 17 16:37:58 2012 -0400
@@ -280,7 +280,7 @@
 
 (** There is one important subtlety in this definition.  Coq allows us to use convenient ML-style pattern matching notation, but, internally and in proofs, we see that patterns are expanded out completely, matching one level of inductive structure at a time.  Thus, the default case in the [match] above expands out to one case for each constructor of [exp] besides [Pair], and the underscore in [pairOutDefault _] is resolved differently in each case.  From an ML or Haskell programmer's perspective, what we have here is type inference determining which code is run (returning either [None] or [tt]), which goes beyond what is possible with type inference guiding parametric polymorphism in Hindley-Milner languages%\index{Hindley-Milner}%, but is similar to what goes on with Haskell type classes%\index{type classes}%.
 
-With [pairOut] available, we can write [cfold] in a straightforward way.  There are really no surprises beyond that Coq verifies that this code has such an expressive type, given the small annotation burden.  In some places, we see that Coq's [match] annotation inference is too smart for its own good, and we have to turn that inference off by writing [return _]. *)
+With [pairOut] available, we can write [cfold] in a straightforward way.  There are really no surprises beyond that Coq verifies that this code has such an expressive type, given the small annotation burden.  In some places, we see that Coq's [match] annotation inference is too smart for its own good, and we have to turn that inference with explicit [return] clauses. *)
 
 Fixpoint cfold t (e : exp t) : exp t :=
   match e with
@@ -288,14 +288,14 @@
     | Plus e1 e2 =>
       let e1' := cfold e1 in
       let e2' := cfold e2 in
-      match e1', e2' return _ with
+      match e1', e2' return exp Nat with
         | NConst n1, NConst n2 => NConst (n1 + n2)
         | _, _ => Plus e1' e2'
       end
     | Eq e1 e2 =>
       let e1' := cfold e1 in
       let e2' := cfold e2 in
-      match e1', e2' return _ with
+      match e1', e2' return exp Bool with
         | NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false)
         | _, _ => Eq e1' e2'
       end
@@ -304,7 +304,7 @@
     | And e1 e2 =>
       let e1' := cfold e1 in
       let e2' := cfold e2 in
-      match e1', e2' return _ with
+      match e1', e2' return exp Bool with
         | BConst b1, BConst b2 => BConst (b1 && b2)
         | _, _ => And e1' e2'
       end
--- a/src/StackMachine.v	Wed Jun 13 11:14:00 2012 -0400
+++ b/src/StackMachine.v	Tue Jul 17 16:37:58 2012 -0400
@@ -51,7 +51,7 @@
 
 (** Now we define the type of arithmetic expressions.  We write that a constant may be built from one argument, a natural number; and a binary operation may be built from a choice of operator and two operand expressions.
 
-A note for readers following along in the PDF version: %\index{coqdoc}%coqdoc supports pretty-printing of tokens in LaTeX or HTML.  Where you see a right arrow character, the source contains the ASCII text %\texttt{%#<tt>#->#</tt>#%}%.  Other examples of this substitution appearing in this chapter are a double right arrow for %\texttt{%#<tt>#=>#</tt>#%}%, the inverted %`%#'#A' symbol for %\texttt{%#<tt>#forall#</tt>#%}%, and the Cartesian product %`%#'#X' for %\texttt{%#<tt>#*#</tt>#%}%.  When in doubt about the ASCII version of a symbol, you can consult the chapter source code.
+A note for readers following along in the PDF version: %\index{coqdoc}%coqdoc supports pretty-printing of tokens in %\LaTeX{}%#LaTeX# or HTML.  Where you see a right arrow character, the source contains the ASCII text %\texttt{%#<tt>#->#</tt>#%}%.  Other examples of this substitution appearing in this chapter are a double right arrow for %\texttt{%#<tt>#=>#</tt>#%}%, the inverted %`%#'#A' symbol for %\texttt{%#<tt>#forall#</tt>#%}%, and the Cartesian product %`%#'#X' for %\texttt{%#<tt>#*#</tt>#%}%.  When in doubt about the ASCII version of a symbol, you can consult the chapter source code.
 
 %\medskip%
 
@@ -508,7 +508,7 @@
 
   rewrite (app_nil_end (compile e)).
 
-(** This time, we explicitly specify the value of the variable [l] from the theorem statement, since multiple expressions of list type appear in the conclusion.  [rewrite] might choose the wrong place to rewrite if we did not specify which we want.
+(** This time, we explicitly specify the value of the variable [l] from the theorem statement, since multiple expressions of list type appear in the conclusion.  The [rewrite] tactic might choose the wrong place to rewrite if we did not specify which we want.
 
 [[
   e : exp
@@ -562,9 +562,9 @@
 
 ML and Haskell have indexed algebraic datatypes.  For instance, their list types are indexed by the type of data that the list carries.  However, compared to Coq, ML and Haskell 98 place two important restrictions on datatype definitions.
 
-First, the indices of the range of each data constructor must be type variables bound at the top level of the datatype definition.  There is no way to do what we did here, where we, for instance, say that [TPlus] is a constructor building a [tbinop] whose indices are all fixed at [Nat].  %\index{generalized algebraic datatypes}\index{GADTs|see{generalized algebraic datatypes}}% _Generalized algebraic datatypes_ (GADT's)%~\cite{GADT}% are a popular feature in %\index{GHC Haskell}%GHC Haskell and other languages that removes this first restriction.
+First, the indices of the range of each data constructor must be type variables bound at the top level of the datatype definition.  There is no way to do what we did here, where we, for instance, say that [TPlus] is a constructor building a [tbinop] whose indices are all fixed at [Nat].  %\index{generalized algebraic datatypes}\index{GADTs|see{generalized algebraic datatypes}}% _Generalized algebraic datatypes_ (GADTs)%~\cite{GADT}% are a popular feature in %\index{GHC Haskell}%GHC Haskell and other languages that removes this first restriction.
 
-The second restriction is not lifted by GADT's.  In ML and Haskell, indices of types must be types and may not be _expressions_.  In Coq, types may be indexed by arbitrary Gallina terms.  Type indices can live in the same universe as programs, and we can compute with them just like regular programs.  Haskell supports a hobbled form of computation in type indices based on %\index{Haskell}%multi-parameter type classes, and recent extensions like type functions bring Haskell programming even closer to %``%#"#real#"#%''% functional programming with types, but, without dependent typing, there must always be a gap between how one programs with types and how one programs normally.
+The second restriction is not lifted by GADTs.  In ML and Haskell, indices of types must be types and may not be _expressions_.  In Coq, types may be indexed by arbitrary Gallina terms.  Type indices can live in the same universe as programs, and we can compute with them just like regular programs.  Haskell supports a hobbled form of computation in type indices based on %\index{Haskell}%multi-parameter type classes, and recent extensions like type functions bring Haskell programming even closer to %``%#"#real#"#%''% functional programming with types, but, without dependent typing, there must always be a gap between how one programs with types and how one programs normally.
 *)
 
 (** We can define a similar type family for typed expressions, where a term of type [texp t] can be assigned object language type [t].  (It is conventional in the world of interactive theorem proving to call the language of the proof assistant the%\index{meta language}% _meta language_ and a language being formalized the%\index{object language}% _object language_.) *)
--- a/src/Universes.v	Wed Jun 13 11:14:00 2012 -0400
+++ b/src/Universes.v	Tue Jul 17 16:37:58 2012 -0400
@@ -238,8 +238,11 @@
 
   We are unable to instantiate the parameter [T] of [Const] with an [exp] type.  To see why, it is helpful to print the annotated version of [exp]'s inductive definition. *)
 
+(** [[
 Print exp.
-(** %\vspace{-.15in}% [[
+]]
+
+[[
 Inductive exp
               : Type $ Top.8 ^ ->
                 Type
@@ -268,8 +271,16 @@
 
 The next constraint, for [Top.15], is more complicated.  This is the universe of the second argument to the [Pair] constructor.  Not only must [Top.15] be less than [Top.8], but it also comes out that [Top.8] must be less than [Coq.Init.Datatypes.38].  What is this new universe variable?  It is from the definition of the [prod] inductive family, to which types of the form [A * B] are desugared. *)
 
+(* begin hide *)
+Inductive prod := pair.
+Reset prod.
+(* end hide *)
+
+(** [[
 Print prod.
-(** %\vspace{-.15in}% [[
+]]
+
+[[
 Inductive prod (A : Type $ Coq.Init.Datatypes.37 ^ )
           (B : Type $ Coq.Init.Datatypes.38 ^ )
             : Type $ max(Coq.Init.Datatypes.37, Coq.Init.Datatypes.38) ^ :=