Mercurial > cpdt > repo

changeset 534:ed829eaa91b2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Builds with Coq 8.5beta2
author Adam Chlipala <adam@chlipala.net>
date Wed, 05 Aug 2015 14:46:55 -0400
parents 8921cfa2f503
children dac7a2705b00
files .hgignore Makefile src/Coinductive.v src/CpdtTactics.v src/DataStruct.v src/DepList.v src/Equality.v src/Exercises.v src/GeneralRec.v src/Generic.v src/InductiveTypes.v src/Intro.v src/Large.v src/LogicProg.v src/Match.v src/MoreDep.v src/MoreSpecif.v src/Predicates.v src/ProgLang.v src/Reflection.v src/StackMachine.v src/Subset.v src/Universes.v
diffstat 23 files changed, 124 insertions(+), 69 deletions(-) [+]
line wrap: on
line diff
--- a/.hgignore	Tue Apr 07 18:59:24 2015 -0400
+++ b/.hgignore	Wed Aug 05 14:46:55 2015 -0400
@@ -36,3 +36,4 @@
 *.pdf
 *.ind
 *.out
+src/.coq-native
--- a/Makefile	Tue Apr 07 18:59:24 2015 -0400
+++ b/Makefile	Wed Aug 05 14:46:55 2015 -0400
@@ -17,8 +17,8 @@
 
 Makefile.coq: Makefile $(VS)
 	coq_makefile $(VS) \
-		COQC = "coqc -I src" \
-		COQDEP = "coqdep -I src" \
+		COQC = "coqc -R src Cpdt" \
+		COQDEP = "coqdep -R src Cpdt" \
 		-o Makefile.coq
 
 clean:: Makefile.coq
--- a/src/Coinductive.v	Tue Apr 07 18:59:24 2015 -0400
+++ b/src/Coinductive.v	Wed Aug 05 14:46:55 2015 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2012, Adam Chlipala
+(* Copyright (c) 2008-2012, 2015, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -10,11 +10,12 @@
 (* begin hide *)
 Require Import List.
 
-Require Import CpdtTactics.
+Require Import Cpdt.CpdtTactics.
 
 Definition bad : unit := tt.
 
 Set Implicit Arguments.
+Set Asymmetric Patterns.
 (* end hide *)
 
 
--- a/src/CpdtTactics.v	Tue Apr 07 18:59:24 2015 -0400
+++ b/src/CpdtTactics.v	Wed Aug 05 14:46:55 2015 -0400
@@ -7,9 +7,7 @@
  *   http://creativecommons.org/licenses/by-nc-nd/3.0/
  *)
 
-Require Import Eqdep List.
-
-Require Omega.
+Require Import Eqdep List Omega.
 
 Set Implicit Arguments.
 
--- a/src/DataStruct.v	Tue Apr 07 18:59:24 2015 -0400
+++ b/src/DataStruct.v	Wed Aug 05 14:46:55 2015 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2012, Adam Chlipala
+(* Copyright (c) 2008-2012, 2015, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -10,9 +10,10 @@
 (* begin hide *)
 Require Import Arith List.
 
-Require Import CpdtTactics.
+Require Import Cpdt.CpdtTactics.
 
 Set Implicit Arguments.
+Set Asymmetric Patterns.
 (* end hide *)
 
 
@@ -489,6 +490,11 @@
 
 (** %\index{index function}%Indexed lists can be useful in defining other inductive types with constructors that take variable numbers of arguments.  In this section, we consider parameterized trees with arbitrary branching factor. *)
 
+(* begin hide *)
+Definition red_herring := O.
+(* working around a bug in Coq 8.5! *)
+(* end hide *)
+
 Section tree.
   Variable A : Set.
 
@@ -553,6 +559,10 @@
 Abort.
 
 Reset tree.
+(* begin hide *)
+Reset red_herring.
+(* working around a bug in Coq 8.5! *)
+(* end hide *)
 
 (** First, let us try using our recursive definition of [ilist]s instead of the inductive version. *)
 
--- a/src/DepList.v	Tue Apr 07 18:59:24 2015 -0400
+++ b/src/DepList.v	Wed Aug 05 14:46:55 2015 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2009, Adam Chlipala
+(* Copyright (c) 2008-2009, 2015, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -9,9 +9,10 @@
 
 (* Dependent list types presented in Chapter 9 *)
 
-Require Import Arith List CpdtTactics.
+Require Import Arith List Cpdt.CpdtTactics.
 
 Set Implicit Arguments.
+Set Asymmetric Patterns.
 
 
 Section ilist.
--- a/src/Equality.v	Tue Apr 07 18:59:24 2015 -0400
+++ b/src/Equality.v	Wed Aug 05 14:46:55 2015 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2012, Adam Chlipala
+(* Copyright (c) 2008-2012, 2015, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -10,9 +10,10 @@
 (* begin hide *)
 Require Import Eqdep JMeq List.
 
-Require Import CpdtTactics.
+Require Import Cpdt.CpdtTactics.
 
 Set Implicit Arguments.
+Set Asymmetric Patterns.
 (* end hide *)
 
 
@@ -832,18 +833,17 @@
        P x -> forall y : A, y = x -> P y
 ]]
 
-The corresponding lemma used for [JMeq] in the proof of [pair_cong] is %\index{Gallina terms!internal\_JMeq\_rew\_r}%[internal_JMeq_rew_r], which, confusingly, is defined by [rewrite] as needed, so it is not available for checking until after we apply it. *)
+The corresponding lemma used for [JMeq] in the proof of [pair_cong] is defined internally by [rewrite as needed, but its type happens to be the following. *)
 
-Check internal_JMeq_rew_r.
 (** %\vspace{-.15in}%[[
 internal_JMeq_rew_r
      : forall (A : Type) (x : A) (B : Type) (b : B)
          (P : forall B0 : Type, B0 -> Type), P B b -> x == b -> P A x
 ]]
 
-The key difference is that, where the [eq] lemma is parameterized on a predicate of type [A -> Prop], the [JMeq] lemma is parameterized on a predicate of type more like [forall A : Type, A -> Prop].  To apply [eq_ind_r] with a proof of [x = y], it is only necessary to rearrange the goal into an application of a [fun] abstraction to [y].  In contrast, to apply [internal_JMeq_rew_r], it is necessary to rearrange the goal to an application of a [fun] abstraction to both [y] and _its type_.  In other words, the predicate must be _polymorphic_ in [y]'s type; any type must make sense, from a type-checking standpoint.  There may be cases where the former rearrangement is easy to do in a type-correct way, but the second rearrangement done %\%naive%{}%ly leads to a type error.
+The key difference is that, where the [eq] lemma is parameterized on a predicate of type [A -> Prop], the [JMeq] lemma is parameterized on a predicate of type more like [forall A : Type, A -> Prop].  To apply [eq_ind_r] with a proof of [x = y], it is only necessary to rearrange the goal into an application of a [fun] abstraction to [y].  In contrast, to apply the alternative principle, it is necessary to rearrange the goal to an application of a [fun] abstraction to both [y] and _its type_.  In other words, the predicate must be _polymorphic_ in [y]'s type; any type must make sense, from a type-checking standpoint.  There may be cases where the former rearrangement is easy to do in a type-correct way, but the second rearrangement done %\%naive%{}%ly leads to a type error.
 
-When [rewrite] cannot figure out how to apply [internal_JMeq_rew_r] for [x == y] where [x] and [y] have the same type, the tactic can instead use an alternate theorem, which is easy to prove as a composition of [eq_ind_r] and [JMeq_eq]. *)
+When [rewrite] cannot figure out how to apply the alternative principle for [x == y] where [x] and [y] have the same type, the tactic can instead use an alternate theorem, which is easy to prove as a composition of [eq_ind_r] and [JMeq_eq]. *)
 
 Check JMeq_ind_r.
 (** %\vspace{-.15in}%[[
@@ -852,7 +852,7 @@
        P x -> forall y : A, y == x -> P y
 ]]
 
-Ironically, where in the proof of [fhapp_assoc'] we used [rewrite app_assoc] to make it clear that a use of [JMeq] was actually homogeneously typed, we created a situation where [rewrite] applied the axiom-based [JMeq_ind_r] instead of the axiom-free [internal_JMeq_rew_r]!
+Ironically, where in the proof of [fhapp_assoc'] we used [rewrite app_assoc] to make it clear that a use of [JMeq] was actually homogeneously typed, we created a situation where [rewrite] applied the axiom-based [JMeq_ind_r] instead of the axiom-free principle!
 
 For another simple example, consider this theorem that applies a heterogeneous equality to prove a congruence fact. *)
 
@@ -874,7 +874,7 @@
 *)
   apply JMeq_ind_r with (x := m); auto.
 
-  (** However, we run into trouble trying to get the goal into a form compatible with [internal_JMeq_rew_r.] *)
+  (** However, we run into trouble trying to get the goal into a form compatible with the alternative principle. *)
 
   Undo 2.
 (** %\vspace{-.15in}%[[
--- a/src/Exercises.v	Tue Apr 07 18:59:24 2015 -0400
+++ b/src/Exercises.v	Wed Aug 05 14:46:55 2015 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2012, Adam Chlipala
+(* Copyright (c) 2008-2012, 2015, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -10,7 +10,7 @@
 (* begin hide *)
 Require Import List.
 
-Require Import CpdtTactics.
+Require Import Cpdt.CpdtTactics.
 (* end hide *)
 
 (** These exercises were originally included inline in the text, but my latest feeling is that I don't have the time to maintain the exercises at a sufficient quality level to match the level I'm targetting for the rest of the book.  I'm including them in this file for now. *)
--- a/src/GeneralRec.v	Tue Apr 07 18:59:24 2015 -0400
+++ b/src/GeneralRec.v	Wed Aug 05 14:46:55 2015 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2006, 2011-2012, Adam Chlipala
+(* Copyright (c) 2006, 2011-2012, 2015, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -8,11 +8,12 @@
  *)
 
 (* begin hide *)
-Require Import Arith List.
+Require Import Arith List Omega.
 
-Require Import CpdtTactics Coinductive.
+Require Import Cpdt.CpdtTactics Cpdt.Coinductive.
 
 Set Implicit Arguments.
+Set Asymmetric Patterns.
 (* end hide *)
 
 
--- a/src/Generic.v	Tue Apr 07 18:59:24 2015 -0400
+++ b/src/Generic.v	Wed Aug 05 14:46:55 2015 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2010, 2012, Adam Chlipala
+(* Copyright (c) 2008-2010, 2012, 2015, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -10,9 +10,10 @@
 (* begin hide *)
 Require Import String List.
 
-Require Import CpdtTactics DepList.
+Require Import Cpdt.CpdtTactics Cpdt.DepList.
 
 Set Implicit Arguments.
+Set Asymmetric Patterns.
 (* end hide *)
 
 (** printing ~> $\leadsto$ *)
--- a/src/InductiveTypes.v	Tue Apr 07 18:59:24 2015 -0400
+++ b/src/InductiveTypes.v	Wed Aug 05 14:46:55 2015 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2012, Adam Chlipala
+(* Copyright (c) 2008-2012, 2015, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -10,9 +10,10 @@
 (* begin hide *)
 Require Import List.
 
-Require Import CpdtTactics.
+Require Import Cpdt.CpdtTactics.
 
 Set Implicit Arguments.
+Set Asymmetric Patterns.
 (* end hide *)
 
 
@@ -394,11 +395,11 @@
 Qed.
 (* end thide *)
 
+Hint Rewrite n_plus_O plus_assoc.
+
 Theorem nsize_nsplice : forall tr1 tr2 : nat_btree, nsize (nsplice tr1 tr2)
   = plus (nsize tr2) (nsize tr1).
 (* begin thide *)
-  Hint Rewrite n_plus_O plus_assoc.
-
   induction tr1; crush.
 Qed.
 (* end thide *)
@@ -1082,11 +1083,11 @@
 
 (** Now we begin the proof of the theorem, adding the lemma [plus_S] as a hint. *)
 
+Hint Rewrite plus_S.
+
 Theorem ntsize_ntsplice : forall tr1 tr2 : nat_tree, ntsize (ntsplice tr1 tr2)
   = plus (ntsize tr2) (ntsize tr1).
 (* begin thide *)
-  Hint Rewrite plus_S.
-
   (** We know that the standard induction principle is insufficient for the task, so we need to provide a %\index{tactics!using}%[using] clause for the [induction] tactic to specify our alternate principle. *)
 
   induction tr1 using nat_tree_ind'; crush.
@@ -1115,7 +1116,7 @@
   (** We can go further in automating the proof by exploiting the hint mechanism.%\index{Vernacular commands!Hint Extern}% *)
 
   Restart.
-
+  
   Hint Extern 1 (ntsize (match ?LS with Nil => _ | Cons _ _ => _ end) = _) =>
     destruct LS; crush.
   induction tr1 using nat_tree_ind'; crush.
--- a/src/Intro.v	Tue Apr 07 18:59:24 2015 -0400
+++ b/src/Intro.v	Wed Aug 05 14:46:55 2015 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2013, Adam Chlipala
+(* Copyright (c) 2008-2013, 2015, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -186,7 +186,7 @@
 (** ** Installation and Emacs Set-Up *)
 
 (**
-At the start of the next chapter, I assume that you have installed Coq and Proof General.  The code in this book is tested with Coq versions 8.4 and 8.4pl1.  Though parts may work with other versions, it is expected that the book source will fail to build with _earlier_ versions.
+At the start of the next chapter, I assume that you have installed Coq and Proof General.  The code in this book is tested with Coq versions 8.4pl5 and 8.5beta2.  Though parts may work with other versions, it is expected that the book source will fail to build with _earlier_ versions.
 
 %\index{Proof General|(}%To set up your Proof General environment to process the source to the next chapter, a few simple steps are required.
 
--- a/src/Large.v	Tue Apr 07 18:59:24 2015 -0400
+++ b/src/Large.v	Wed Aug 05 14:46:55 2015 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2009-2012, Adam Chlipala
+(* Copyright (c) 2009-2012, 2015, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -10,9 +10,10 @@
 (* begin hide *)
 Require Import Arith.
 
-Require Import CpdtTactics.
+Require Import Cpdt.CpdtTactics.
 
 Set Implicit Arguments.
+Set Asymmetric Patterns.
 (* end hide *)
 
 
@@ -390,7 +391,7 @@
 
 (** We can take the final tactic and move it into the initial part of the proof script, arriving at a nicely automated proof. *)
 
-Reset t.
+Reset cfold_correct.
 
 Theorem cfold_correct : forall t (e : exp t), expDenote e = expDenote (cfold e).
   induction e; crush;
--- a/src/LogicProg.v	Tue Apr 07 18:59:24 2015 -0400
+++ b/src/LogicProg.v	Wed Aug 05 14:46:55 2015 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2011-2012, Adam Chlipala
+(* Copyright (c) 2011-2012, 2015, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -9,12 +9,12 @@
 
 (* begin hide *)
 
-Require Import List.
+Require Import List Omega.
 
-Require Import CpdtTactics.
+Require Import Cpdt.CpdtTactics.
 
 Set Implicit Arguments.
-
+Set Asymmetric Patterns.
 (* end hide *)
 
 (** %\part{Proof Engineering}
@@ -685,12 +685,6 @@
 Qed.
 (* end thide *)
 
-(* begin hide *)
-(* begin thide *)
-Definition e1s := eval1'_subproof.
-(* end thide *)
-(* end hide *)
-
 Print eval1'.
 (** %\vspace{-.15in}%[[
 eval1' = 
--- a/src/Match.v	Tue Apr 07 18:59:24 2015 -0400
+++ b/src/Match.v	Wed Aug 05 14:46:55 2015 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2012, Adam Chlipala
+(* Copyright (c) 2008-2012, 2015, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -10,9 +10,10 @@
 (* begin hide *)
 Require Import List.
 
-Require Import CpdtTactics.
+Require Import Cpdt.CpdtTactics.
 
 Set Implicit Arguments.
+Set Asymmetric Patterns.
 (* end hide *)
 
 
@@ -359,6 +360,9 @@
    The problem is that Ltac treats the expression [S (length ls')] as an invocation of a tactic [S] with argument [length ls'].  We need to use a special annotation to "escape into" the Gallina parsing nonterminal.%\index{tactics!constr}% *)
 
 (* begin thide *)
+(* begin hide *)
+Definition red_herring := O.
+(* end hide *)
 Ltac length ls :=
   match ls with
     | nil => O
@@ -383,9 +387,15 @@
 Abort.
 
 Reset length.
+(* begin hide *)
+Reset red_herring.
+(* end hide *)
 
 (** The thing to remember is that Gallina terms built by tactics must be bound explicitly via [let] or a similar technique, rather than inserting Ltac calls directly in other Gallina terms. *)
 
+(* begin hide *)
+Definition red_herring := O.
+(* end hide *)
 Ltac length ls :=
   match ls with
     | nil => O
@@ -452,7 +462,13 @@
 
 (* begin thide *)
 Reset length.
+(* begin hide *)
+Reset red_herring.
+(* end hide *)
 
+(* begin hide *)
+Definition red_herring := O.
+(* end hide *)
 Ltac length ls :=
   idtac ls;
   match ls with
@@ -484,6 +500,9 @@
    The solution is like in Haskell: we must "monadify" our pure program to give it access to side effects.  The trouble is that the embedded tactic language has no [return] construct.  Proof scripts are about proving theorems, not calculating results.  We can apply a somewhat awkward workaround that requires translating our program into%\index{continuation-passing style}% _continuation-passing style_ %\cite{continuations}%, a program structuring idea popular in functional programming. *)
 
 Reset length.
+(* begin hide *)
+Reset red_herring.
+(* end hide *)
 
 Ltac length ls k :=
   idtac ls;
@@ -811,6 +830,9 @@
 
 (** Now we can write a tactic that encapsulates the pattern we just employed, instantiating all quantifiers of a particular hypothesis. *)
 
+(* begin hide *)
+Definition red_herring := O.
+(* end hide *)
 Ltac insterU H :=
   repeat match type of H with
            | forall x : ?T, _ =>
@@ -923,6 +945,9 @@
 End t7.
 
 Reset insterU.
+(* begin hide *)
+Reset red_herring.
+(* end hide *)
 
 (** We can redefine [insterU] to treat implications differently.  In particular, we pattern-match on the type of the type [T] in [forall x : ?T, ...].  If [T] has type [Prop], then [x]'s instantiation should be thought of as a proof.  Thus, instead of picking a new unification variable for it, we instead apply a user-supplied tactic [tac].  It is important that we end this special [Prop] case with [|| fail 1], so that, if [tac] fails to prove [T], we abort the instantiation, rather than continuing on to the default quantifier handling.  Also recall that the tactic form %\index{tactics!solve}%[solve [ t ]] fails if [t] does not completely solve the goal. *)
 
--- a/src/MoreDep.v	Tue Apr 07 18:59:24 2015 -0400
+++ b/src/MoreDep.v	Wed Aug 05 14:46:55 2015 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2012, Adam Chlipala
+(* Copyright (c) 2008-2012, 2015, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -8,11 +8,12 @@
  *)
 
 (* begin hide *)
-Require Import Arith Bool List.
+Require Import Arith Bool List Omega.
 
-Require Import CpdtTactics MoreSpecif.
+Require Import Cpdt.CpdtTactics Cpdt.MoreSpecif.
 
 Set Implicit Arguments.
+Set Asymmetric Patterns.
 (* end hide *)
 
 
--- a/src/MoreSpecif.v	Tue Apr 07 18:59:24 2015 -0400
+++ b/src/MoreSpecif.v	Wed Aug 05 14:46:55 2015 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008, 2011, Adam Chlipala
+(* Copyright (c) 2008, 2011, 2015, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -10,6 +10,7 @@
 (* Types and notations presented in Chapter 6 *)
 
 Set Implicit Arguments.
+Set Asymmetric Patterns.
 
 
 Notation "!" := (False_rec _ _) : specif_scope.
--- a/src/Predicates.v	Tue Apr 07 18:59:24 2015 -0400
+++ b/src/Predicates.v	Wed Aug 05 14:46:55 2015 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2012, Adam Chlipala
+(* Copyright (c) 2008-2012, 2015, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -10,9 +10,10 @@
 (* begin hide *)
 Require Import List.
 
-Require Import CpdtTactics.
+Require Import Cpdt.CpdtTactics.
 
 Set Implicit Arguments.
+Set Asymmetric Patterns.
 
 (* Extra definitions to get coqdoc to choose the right fonts. *)
 
--- a/src/ProgLang.v	Tue Apr 07 18:59:24 2015 -0400
+++ b/src/ProgLang.v	Wed Aug 05 14:46:55 2015 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2011-2012, Adam Chlipala
+(* Copyright (c) 2011-2012, 2015, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -10,9 +10,10 @@
 (* begin hide *)
 Require Import FunctionalExtensionality List.
 
-Require Import CpdtTactics DepList.
+Require Import Cpdt.CpdtTactics Cpdt.DepList.
 
 Set Implicit Arguments.
+Set Asymmetric Patterns.
 (* end hide *)
 
 (** %\chapter{A Taste of Reasoning About Programming Language Syntax}% *)
@@ -23,10 +24,13 @@
 
    I apologize in advance to those readers not familiar with the theory of programming language semantics.  I will make a few remarks intended to relate the material here with common ideas in semantics, but these remarks should be safe for others to skip.
 
-   We will define a small programming language and reason about its semantics, expressed as an interpreter into Coq terms, much as we have done in examples throughout the book.  It will be helpful to build a slight extension of [crush] that tries to apply %\index{functional extensionality}%functional extensionality, an axiom we met in Chapter 12, which says that two functions are equal if they map equal inputs to equal outputs. *)
+   We will define a small programming language and reason about its semantics, expressed as an interpreter into Coq terms, much as we have done in examples throughout the book.  It will be helpful to build a slight extension of [crush] that tries to apply %\index{functional extensionality}%functional extensionality, an axiom we met in Chapter 12, which says that two functions are equal if they map equal inputs to equal outputs.  We also use [f_equal] to simplify goals of a particular form that will come up with the term denotation function that we define shortly. *)
 
 Ltac ext := let x := fresh "x" in extensionality x.
-Ltac pl := crush; repeat (ext || f_equal; crush).
+Ltac pl := crush; repeat (match goal with
+                            | [ |- (fun x => _) = (fun y => _) ] => ext
+                            | [ |- _ _ _ ?E _ = _ _ _ ?E _ ] => f_equal
+                          end; crush).
 
 (** At this point in the book source, some auxiliary proofs also appear. *)
 
--- a/src/Reflection.v	Tue Apr 07 18:59:24 2015 -0400
+++ b/src/Reflection.v	Wed Aug 05 14:46:55 2015 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2012, Adam Chlipala
+(* Copyright (c) 2008-2012, 2015, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -10,9 +10,10 @@
 (* begin hide *)
 Require Import List.
 
-Require Import CpdtTactics MoreSpecif.
+Require Import Cpdt.CpdtTactics Cpdt.MoreSpecif.
 
 Set Implicit Arguments.
+Set Asymmetric Patterns.
 (* end hide *)
 
 
@@ -793,6 +794,9 @@
 
 (** Here is a %\%naive%{}% first attempt at a reification tactic. *)
 
+(* begin hide *)
+Definition red_herring := O.
+(* end hide *)
 Ltac refl' e :=
   match e with
     | ?E1 + ?E2 =>
@@ -812,6 +816,10 @@
    To handle functions in general, we will use the pattern variable form [@?X], which allows [X] to mention newly introduced variables that are declared explicitly.  A use of [@?X] must be followed by a list of the local variables that may be mentioned.  The variable [X] then comes to stand for a Gallina function over the values of those variables.  For instance: *)
 
 Reset refl'.
+(* begin hide *)
+Reset red_herring.
+Definition red_herring := O.
+(* end hide *)
 Ltac refl' e :=
   match e with
     | ?E1 + ?E2 =>
@@ -829,6 +837,9 @@
 (** Now, in the abstraction case, we bind [E1] as a function from an [x] value to the value of the abstraction body.  Unfortunately, our recursive call there is not destined for success.  It will match the same abstraction pattern and trigger another recursive call, and so on through infinite recursion.  One last refactoring yields a working procedure.  The key idea is to consider every input to [refl'] as _a function over the values of variables introduced during recursion_. *)
 
 Reset refl'.
+(* begin hide *)
+Reset red_herring.
+(* end hide *)
 Ltac refl' e :=
   match eval simpl in e with
     | fun x : ?T => @?E1 x + @?E2 x =>
@@ -838,7 +849,7 @@
 
     | fun (x : ?T) (y : nat) => @?E1 x y =>
       let r1 := refl' (fun p : T * nat => E1 (fst p) (snd p)) in
-        constr:(fun x => Abs (fun y => r1 (x, y)))
+        constr:(fun u => Abs (fun v => r1 (u, v)))
 
     | _ => constr:(fun x => Const (e x))
   end.
--- a/src/StackMachine.v	Tue Apr 07 18:59:24 2015 -0400
+++ b/src/StackMachine.v	Wed Aug 05 14:46:55 2015 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2012, Adam Chlipala
+(* Copyright (c) 2008-2012, 2015, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -16,6 +16,7 @@
 
 Require Import Bool Arith List CpdtTactics.
 Set Implicit Arguments.
+Set Asymmetric Patterns.
 
 (* begin hide *)
 (* begin thide *)
@@ -23,7 +24,7 @@
 (* end thide *)
 (* end hide *)
 
-(** In general, similar commands will be hidden in the book rendering of each chapter's source code, so you will need to insert them in from-scratch replayings of the code that is presented.  To be more specific, every chapter begins with the above two lines, with the import list tweaked as appropriate, considering which definitions the chapter uses.  The second command above affects the default behavior of definitions regarding type inference. *)
+(** In general, similar commands will be hidden in the book rendering of each chapter's source code, so you will need to insert them in from-scratch replayings of the code that is presented.  To be more specific, every chapter begins with the above three lines, with the import list tweaked as appropriate, considering which definitions the chapter uses.  The second command above affects the default behavior of definitions regarding type inference, and the third allows for more concise pattern-matching syntax in Coq versions 8.5 and higher (having no effect in earlier versions). *)
 
 
 (** * Arithmetic Expressions Over Natural Numbers *)
--- a/src/Subset.v	Tue Apr 07 18:59:24 2015 -0400
+++ b/src/Subset.v	Wed Aug 05 14:46:55 2015 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2012, Adam Chlipala
+(* Copyright (c) 2008-2012, 2015, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -10,9 +10,10 @@
 (* begin hide *)
 Require Import List.
 
-Require Import CpdtTactics.
+Require Import Cpdt.CpdtTactics.
 
 Set Implicit Arguments.
+Set Asymmetric Patterns.
 (* end hide *)
 
 (** printing <-- $\longleftarrow$ *)
--- a/src/Universes.v	Tue Apr 07 18:59:24 2015 -0400
+++ b/src/Universes.v	Wed Aug 05 14:46:55 2015 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2009-2012, Adam Chlipala
+(* Copyright (c) 2009-2012, 2015, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -10,9 +10,10 @@
 (* begin hide *)
 Require Import List.
 
-Require Import DepList CpdtTactics.
+Require Import DepList Cpdt.CpdtTactics.
 
 Set Implicit Arguments.
+Set Asymmetric Patterns.
 (* end hide *)
 
 (** printing $ %({}*% #(<a/>*# *)