Mercurial > cpdt > repo

changeset 314:d5787b70cf48

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Rename Tactics; change 'principal typing' to 'principal types'
author Adam Chlipala <adam@chlipala.net>
date Wed, 07 Sep 2011 13:47:24 -0400
parents 44f9ca08e173
children 72bffb046797
files Makefile src/Coinductive.v src/CpdtTactics.v src/DataStruct.v src/DeBruijn.v src/DepList.v src/Equality.v src/Extensional.v src/Firstorder.v src/Generic.v src/Hoas.v src/InductiveTypes.v src/Intensional.v src/Interps.v src/Intro.v src/Large.v src/Match.v src/MoreDep.v src/OpSem.v src/Predicates.v src/Reflection.v src/StackMachine.v src/Subset.v src/Tactics.v src/Universes.v staging/updates.rss
diffstat 26 files changed, 228 insertions(+), 212 deletions(-) [+]
line wrap: on
line diff
--- a/Makefile	Thu Sep 01 11:33:55 2011 -0400
+++ b/Makefile	Wed Sep 07 13:47:24 2011 -0400
@@ -1,4 +1,4 @@
-MODULES_NODOC := Tactics MoreSpecif DepList
+MODULES_NODOC := CpdtTactics MoreSpecif DepList
 MODULES_PROSE := Intro
 MODULES_CODE  := StackMachine InductiveTypes Predicates Coinductive Subset \
 	MoreDep DataStruct Equality Generic Universes Match Reflection \
--- a/src/Coinductive.v	Thu Sep 01 11:33:55 2011 -0400
+++ b/src/Coinductive.v	Wed Sep 07 13:47:24 2011 -0400
@@ -10,7 +10,7 @@
 (* begin hide *)
 Require Import List.
 
-Require Import Tactics.
+Require Import CpdtTactics.
 
 Set Implicit Arguments.
 (* end hide *)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/CpdtTactics.v	Wed Sep 07 13:47:24 2011 -0400
@@ -0,0 +1,187 @@
+(* Copyright (c) 2008-2011, Adam Chlipala
+ * 
+ * This work is licensed under a
+ * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
+ * Unported License.
+ * The license text is available at:
+ *   http://creativecommons.org/licenses/by-nc-nd/3.0/
+ *)
+
+Require Import Eqdep List.
+
+Require Omega.
+
+Set Implicit Arguments.
+
+
+Ltac inject H := injection H; clear H; intros; try subst.
+
+Ltac appHyps f :=
+  match goal with
+    | [ H : _ |- _ ] => f H
+  end.
+
+Ltac inList x ls :=
+  match ls with
+    | x => idtac
+    | (_, x) => idtac
+    | (?LS, _) => inList x LS
+  end.
+
+Ltac app f ls :=
+  match ls with
+    | (?LS, ?X) => f X || app f LS || fail 1
+    | _ => f ls
+  end.
+
+Ltac all f ls :=
+  match ls with
+    | (?LS, ?X) => f X; all f LS
+    | (_, _) => fail 1
+    | _ => f ls
+  end.
+
+Ltac simplHyp invOne :=
+  let invert H F :=
+    inList F invOne; (inversion H; fail)
+    || (inversion H; [idtac]; clear H; try subst) in
+  match goal with
+    | [ H : ex _ |- _ ] => destruct H
+
+    | [ H : ?F ?X = ?F ?Y |- ?G ] =>
+      (assert (X = Y); [ assumption | fail 1 ])
+      || (injection H;
+        match goal with
+          | [ |- X = Y -> G ] =>
+            try clear H; intros; try subst
+        end)
+    | [ H : ?F ?X ?U = ?F ?Y ?V |- ?G ] =>
+      (assert (X = Y); [ assumption
+        | assert (U = V); [ assumption | fail 1 ] ])
+      || (injection H;
+        match goal with
+          | [ |- U = V -> X = Y -> G ] =>
+            try clear H; intros; try subst
+        end)
+
+    | [ H : ?F _ |- _ ] => invert H F
+    | [ H : ?F _ _ |- _ ] => invert H F
+    | [ H : ?F _ _ _ |- _ ] => invert H F
+    | [ H : ?F _ _ _ _ |- _ ] => invert H F
+    | [ H : ?F _ _ _ _ _ |- _ ] => invert H F
+
+    | [ H : existT _ ?T _ = existT _ ?T _ |- _ ] => generalize (inj_pair2 _ _ _ _ _ H); clear H
+    | [ H : existT _ _ _ = existT _ _ _ |- _ ] => inversion H; clear H
+
+    | [ H : Some _ = Some _ |- _ ] => injection H; clear H
+  end.
+
+Ltac rewriteHyp :=
+  match goal with
+    | [ H : _ |- _ ] => rewrite H; auto; [idtac]
+  end.
+
+Ltac rewriterP := repeat (rewriteHyp; autorewrite with cpdt in *).
+
+Ltac rewriter := autorewrite with cpdt in *; rewriterP.
+
+Hint Rewrite app_ass : cpdt.
+
+Definition done (T : Type) (x : T) := True.
+
+Ltac inster e trace :=
+  match type of e with
+    | forall x : _, _ =>
+      match goal with
+        | [ H : _ |- _ ] =>
+          inster (e H) (trace, H)
+        | _ => fail 2
+      end
+    | _ =>
+      match trace with
+        | (_, _) =>
+          match goal with
+            | [ H : done (trace, _) |- _ ] => fail 1
+            | _ =>
+              let T := type of e in
+                match type of T with
+                  | Prop =>
+                    generalize e; intro;
+                      assert (done (trace, tt)); [constructor | idtac]
+                  | _ =>
+                    all ltac:(fun X =>
+                      match goal with
+                        | [ H : done (_, X) |- _ ] => fail 1
+                        | _ => idtac
+                      end) trace;
+                    let i := fresh "i" in (pose (i := e);
+                      assert (done (trace, i)); [constructor | idtac])
+                end
+          end
+      end
+  end.
+
+Ltac un_done :=
+  repeat match goal with
+           | [ H : done _ |- _ ] => clear H
+         end.
+
+Require Import JMeq.
+
+Ltac crush' lemmas invOne :=
+  let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence in
+    let rewriter := autorewrite with cpdt in *;
+      repeat (match goal with
+                | [ H : ?P |- _ ] =>
+                  match P with
+                    | context[JMeq] => fail 1
+                    | _ => (rewrite H; [])
+                      || (rewrite H; [ | solve [ crush' lemmas invOne ] ])
+                        || (rewrite H; [ | solve [ crush' lemmas invOne ] | solve [ crush' lemmas invOne ] ])
+                  end
+              end; autorewrite with cpdt in *)
+    in (sintuition; rewriter;
+        match lemmas with
+          | false => idtac
+          | _ => repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
+            repeat (simplHyp invOne; intuition)); un_done
+        end; sintuition; rewriter; sintuition; try omega; try (elimtype False; omega)).
+
+Ltac crush := crush' false fail.
+
+Require Import Program.Equality.
+
+Ltac dep_destruct E :=
+  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
+          end.
+
+Ltac clear_all :=
+  repeat match goal with
+           | [ H : _ |- _ ] => clear H
+         end.
+
+Ltac guess v H :=
+  repeat match type of H with
+           | forall x : ?T, _ =>
+             match type of T with
+               | Prop =>
+                 (let H' := fresh "H'" in
+                   assert (H' : T); [
+                     solve [ eauto 6 ]
+                     | generalize (H H'); clear H H'; intro H ])
+                 || fail 1
+               | _ =>
+                 (generalize (H v); clear H; intro H)
+                 || let x := fresh "x" in
+                   evar (x : T);
+                   let x' := eval cbv delta [x] in x in
+                     clear x; generalize (H x'); clear H; intro H
+             end
+         end.
+
+Ltac guessKeep v H :=
+  let H' := fresh "H'" in
+    generalize H; intro H'; guess v H'.
--- a/src/DataStruct.v	Thu Sep 01 11:33:55 2011 -0400
+++ b/src/DataStruct.v	Wed Sep 07 13:47:24 2011 -0400
@@ -10,7 +10,7 @@
 (* begin hide *)
 Require Import Arith List.
 
-Require Import Tactics.
+Require Import CpdtTactics.
 
 Set Implicit Arguments.
 (* end hide *)
--- a/src/DeBruijn.v	Thu Sep 01 11:33:55 2011 -0400
+++ b/src/DeBruijn.v	Wed Sep 07 13:47:24 2011 -0400
@@ -12,7 +12,7 @@
 
 Require Import Eqdep.
 
-Require Import DepList Tactics.
+Require Import DepList CpdtTactics.
 (* end hide *)
 
 (** remove printing * *)
--- a/src/DepList.v	Thu Sep 01 11:33:55 2011 -0400
+++ b/src/DepList.v	Wed Sep 07 13:47:24 2011 -0400
@@ -9,7 +9,7 @@
 
 (* Dependent list types presented in Chapter 8 *)
 
-Require Import Arith List Tactics.
+Require Import Arith List CpdtTactics.
 
 Set Implicit Arguments.
 
--- a/src/Equality.v	Thu Sep 01 11:33:55 2011 -0400
+++ b/src/Equality.v	Wed Sep 07 13:47:24 2011 -0400
@@ -10,7 +10,7 @@
 (* begin hide *)
 Require Import Eqdep JMeq List.
 
-Require Import Tactics.
+Require Import CpdtTactics.
 
 Set Implicit Arguments.
 (* end hide *)
--- a/src/Extensional.v	Thu Sep 01 11:33:55 2011 -0400
+++ b/src/Extensional.v	Wed Sep 07 13:47:24 2011 -0400
@@ -10,7 +10,7 @@
 (* begin hide *)
 Require Import String List.
 
-Require Import Tactics DepList.
+Require Import CpdtTactics DepList.
 
 Set Implicit Arguments.
 (* end hide *)
--- a/src/Firstorder.v	Thu Sep 01 11:33:55 2011 -0400
+++ b/src/Firstorder.v	Wed Sep 07 13:47:24 2011 -0400
@@ -10,7 +10,7 @@
 (* begin hide *)
 Require Import Arith String List.
 
-Require Import Tactics.
+Require Import CpdtTactics.
 
 Set Implicit Arguments.
 (* end hide *)
--- a/src/Generic.v	Thu Sep 01 11:33:55 2011 -0400
+++ b/src/Generic.v	Wed Sep 07 13:47:24 2011 -0400
@@ -10,7 +10,7 @@
 (* begin hide *)
 Require Import String List.
 
-Require Import Tactics DepList.
+Require Import CpdtTactics DepList.
 
 Set Implicit Arguments.
 (* end hide *)
--- a/src/Hoas.v	Thu Sep 01 11:33:55 2011 -0400
+++ b/src/Hoas.v	Wed Sep 07 13:47:24 2011 -0400
@@ -10,7 +10,7 @@
 (* begin hide *)
 Require Import Eqdep String List FunctionalExtensionality.
 
-Require Import Tactics.
+Require Import CpdtTactics.
 
 Set Implicit Arguments.
 (* end hide *)
--- a/src/InductiveTypes.v	Thu Sep 01 11:33:55 2011 -0400
+++ b/src/InductiveTypes.v	Wed Sep 07 13:47:24 2011 -0400
@@ -10,7 +10,7 @@
 (* begin hide *)
 Require Import List.
 
-Require Import Tactics.
+Require Import CpdtTactics.
 
 Set Implicit Arguments.
 (* end hide *)
--- a/src/Intensional.v	Thu Sep 01 11:33:55 2011 -0400
+++ b/src/Intensional.v	Wed Sep 07 13:47:24 2011 -0400
@@ -10,7 +10,7 @@
 (* begin hide *)
 Require Import Arith Eqdep List FunctionalExtensionality.
 
-Require Import DepList Tactics.
+Require Import DepList CpdtTactics.
 
 Set Implicit Arguments.
 (* end hide *)
--- a/src/Interps.v	Thu Sep 01 11:33:55 2011 -0400
+++ b/src/Interps.v	Wed Sep 07 13:47:24 2011 -0400
@@ -10,7 +10,7 @@
 (* begin hide *)
 Require Import String List FunctionalExtensionality.
 
-Require Import Tactics.
+Require Import CpdtTactics.
 
 Set Implicit Arguments.
 (* end hide *)
--- a/src/Intro.v	Thu Sep 01 11:33:55 2011 -0400
+++ b/src/Intro.v	Wed Sep 07 13:47:24 2011 -0400
@@ -175,7 +175,7 @@
 (**
 To make it possible to start from fancy proof automation, rather than working up to it, I have included with the book source a library of %\emph{%#<i>#tactics#</i>#%}%, or programs that find proofs, since the built-in Coq tactics do not support a high enough level of automation.  I use these tactics even from the first chapter with code examples.
 
-Some readers have asked about the pragmatics of using this tactic library in their own developments.  My position there is that this tactic library was designed with the specific examples of the book in mind; I do not recommend using it in other settings.  Part III should impart the necessary skills to reimplement these tactics and beyond.  One generally deals with undecidable problems in interactive theorem proving, so there can be no tactic that solves all goals, though the %\index{tactics!crush}%[crush] tactic that we will meet soon may sometimes feel like that!  There are still very useful tricks found in the implementations of [crush] and its cousins, so it may be useful to examine the commented source file %\texttt{%#<tt>#Tactics.v#</tt>.#%}.~\footnote{It's not actually commented yet. \texttt{;-)}}%  I implement a new tactic library for each new project, since each project involves a different mix of undecidable theories where a different set of heuristics turns out to work well; and that is what I recommend others do, too.
+Some readers have asked about the pragmatics of using this tactic library in their own developments.  My position there is that this tactic library was designed with the specific examples of the book in mind; I do not recommend using it in other settings.  Part III should impart the necessary skills to reimplement these tactics and beyond.  One generally deals with undecidable problems in interactive theorem proving, so there can be no tactic that solves all goals, though the %\index{tactics!crush}%[crush] tactic that we will meet soon may sometimes feel like that!  There are still very useful tricks found in the implementations of [crush] and its cousins, so it may be useful to examine the commented source file %\texttt{%#<tt>#CpdtTactics.v#</tt>.#%}.~\footnote{It's not actually commented yet. \texttt{;-)}}%  I implement a new tactic library for each new project, since each project involves a different mix of undecidable theories where a different set of heuristics turns out to work well; and that is what I recommend others do, too.
 *)
 
 (** ** Installation and Emacs Set-Up *)
--- a/src/Large.v	Thu Sep 01 11:33:55 2011 -0400
+++ b/src/Large.v	Wed Sep 07 13:47:24 2011 -0400
@@ -10,7 +10,7 @@
 (* begin hide *)
 Require Import Arith.
 
-Require Import Tactics.
+Require Import CpdtTactics.
 
 Set Implicit Arguments.
 (* end hide *)
--- a/src/Match.v	Thu Sep 01 11:33:55 2011 -0400
+++ b/src/Match.v	Wed Sep 07 13:47:24 2011 -0400
@@ -10,7 +10,7 @@
 (* begin hide *)
 Require Import List.
 
-Require Import Tactics.
+Require Import CpdtTactics.
 
 Set Implicit Arguments.
 (* end hide *)
--- a/src/MoreDep.v	Thu Sep 01 11:33:55 2011 -0400
+++ b/src/MoreDep.v	Wed Sep 07 13:47:24 2011 -0400
@@ -10,7 +10,7 @@
 (* begin hide *)
 Require Import Arith Bool List.
 
-Require Import Tactics MoreSpecif.
+Require Import CpdtTactics MoreSpecif.
 
 Set Implicit Arguments.
 (* end hide *)
--- a/src/OpSem.v	Thu Sep 01 11:33:55 2011 -0400
+++ b/src/OpSem.v	Wed Sep 07 13:47:24 2011 -0400
@@ -10,7 +10,7 @@
 (* begin hide *)
 Require Import Arith List.
 
-Require Import Tactics.
+Require Import CpdtTactics.
 
 Set Implicit Arguments.
 (* end hide *)
--- a/src/Predicates.v	Thu Sep 01 11:33:55 2011 -0400
+++ b/src/Predicates.v	Wed Sep 07 13:47:24 2011 -0400
@@ -10,7 +10,7 @@
 (* begin hide *)
 Require Import List.
 
-Require Import Tactics.
+Require Import CpdtTactics.
 
 Set Implicit Arguments.
 (* end hide *)
--- a/src/Reflection.v	Thu Sep 01 11:33:55 2011 -0400
+++ b/src/Reflection.v	Wed Sep 07 13:47:24 2011 -0400
@@ -10,7 +10,7 @@
 (* begin hide *)
 Require Import List.
 
-Require Import Tactics MoreSpecif.
+Require Import CpdtTactics MoreSpecif.
 
 Set Implicit Arguments.
 (* end hide *)
--- a/src/StackMachine.v	Thu Sep 01 11:33:55 2011 -0400
+++ b/src/StackMachine.v	Wed Sep 07 13:47:24 2011 -0400
@@ -10,7 +10,7 @@
 (* begin hide *)
 Require Import Bool Arith List.
 
-Require Import Tactics.
+Require Import CpdtTactics.
 
 Set Implicit Arguments.
 (* end hide *)
@@ -21,7 +21,15 @@
 
 (** I will start off by jumping right in to a fully-worked set of examples, building certified compilers from increasingly complicated source languages to stack machines.  We will meet a few useful tactics and see how they can be used in manual proofs, and we will also see how easily these proofs can be automated instead.  This chapter is not meant to give full explanations of the features that are employed.  Rather, it is meant more as an advertisement of what is possible.  Later chapters will introduce all of the concepts in bottom-up fashion.
 
-As always, you can step through the source file %\texttt{%#<tt>#StackMachine.v#</tt>#%}% for this chapter interactively in Proof General.  Alternatively, to get a feel for the whole lifecycle of creating a Coq development, you can enter the pieces of source code in this chapter in a new %\texttt{%#<tt>#.v#</tt>#%}% file in an Emacs buffer.  If you do the latter, include two lines %\index{Vernacular commands!Require}%[Require Import Bool] #<span class="inlinecode"><span class="id" type="var">#%\coqdocconstructor{%Arith%}%#</span></span># #<span class="inlinecode"><span class="id" type="var">#%\coqdocconstructor{%List%}%#</span></span># [Tactics.] and %\index{Vernacular commands!Set Implicit Arguments}%[Set Implicit] #<span class="inlinecode"><span class="id" type="keyword">#%\coqdockw{%Arguments%}%#</span></span>#[.] at the start of the file, to match some code hidden in this rendering of the chapter source.  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 some imports of other modules, followed by [Set Implicit] #<span class="inlinecode"><span class="id" type="keyword">#%\coqdockw{%Arguments%}%#</span></span>#[.], where the latter affects the default behavior of definitions regarding type inference.
+As always, you can step through the source file %\texttt{%#<tt>#StackMachine.v#</tt>#%}% for this chapter interactively in Proof General.  Alternatively, to get a feel for the whole lifecycle of creating a Coq development, you can enter the pieces of source code in this chapter in a new %\texttt{%#<tt>#.v#</tt>#%}% file in an Emacs buffer.  If you do the latter, include two lines
+
+%\index{Vernacular commands!Require}%[Require Import Bool] #<span class="inlinecode"><span class="id" type="var">#%\coqdocconstructor{%Arith%}%#</span></span># #<span class="inlinecode"><span class="id" type="var">#%\coqdocconstructor{%List%}%#</span></span># [CpdtTactics.]
+
+%\noindent{}%and
+
+%\index{Vernacular commands!Set Implicit Arguments}%[Set Implicit] #<span class="inlinecode"><span class="id" type="keyword">#%\coqdockw{%Arguments%}%#</span></span>#[.]
+
+%\noindent{}%at the start of the file, to match some code hidden in this rendering of the chapter source.  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 some imports of other modules, followed by [Set Implicit] #<span class="inlinecode"><span class="id" type="keyword">#%\coqdockw{%Arguments%}%#</span></span>#[.], where the latter affects the default behavior of definitions regarding type inference.
 *)
 
 
@@ -77,7 +85,7 @@
 
 ]]
 
-Languages like Haskell and ML have a convenient %\index{principal typing}\index{type inference}\emph{%#<i>#principal typing#</i>#%}% property, which gives us strong guarantees about how effective type inference will be.  Unfortunately, Coq's type system is so expressive that any kind of %``%#"#complete#"#%''% type inference is impossible, and the task even seems to be hard heuristically in practice.  Nonetheless, Coq includes some very helpful heuristics, many of them copying the workings of Haskell and ML type-checkers for programs that fall in simple fragments of Coq's language.
+Languages like Haskell and ML have a convenient %\index{principal types}\index{type inference}\emph{%#<i>#principal types#</i>#%}% property, which gives us strong guarantees about how effective type inference will be.  Unfortunately, Coq's type system is so expressive that any kind of %``%#"#complete#"#%''% type inference is impossible, and the task even seems to be hard heuristically in practice.  Nonetheless, Coq includes some very helpful heuristics, many of them copying the workings of Haskell and ML type-checkers for programs that fall in simple fragments of Coq's language.
 
 This is as good a time as any to mention the preponderance of different languages associated with Coq.  The theoretical foundation of Coq is a formal system called the %\index{Calculus of Inductive Constructions}\index{CIC|see{Calculus of Inductive Constructions}}\emph{%#<i>#Calculus of Inductive Constructions (CIC)#</i>#%}~\cite{CIC}%, which is an extension of the older %\index{Calculus of Constructions}\index{CoC|see{Calculus of Constructions}}\emph{%#<i>#Calculus of Constructions (CoC)#</i>#%}~\cite{CoC}%.  CIC is quite a spartan foundation, which is helpful for proving metatheory but not so helpful for real development.  Still, it is nice to know that it has been proved that CIC enjoys properties like %\index{strong normalization}\emph{%#<i>#strong normalization#</i>#%}~\cite{CIC}%, meaning that every program (and, more importantly, every proof term) terminates; and %\index{relative consistency}\emph{%#<i>#relative consistency#</i>#%}~\cite{SetsInTypes}% with systems like versions of %\index{Zermelo-Fraenkel set theory}%Zermelo-Fraenkel set theory, which roughly means that you can believe that Coq proofs mean that the corresponding propositions are %``%#"#really true,#"#%''% if you believe in set theory.
 
--- a/src/Subset.v	Thu Sep 01 11:33:55 2011 -0400
+++ b/src/Subset.v	Wed Sep 07 13:47:24 2011 -0400
@@ -10,7 +10,7 @@
 (* begin hide *)
 Require Import List.
 
-Require Import Tactics.
+Require Import CpdtTactics.
 
 Set Implicit Arguments.
 (* end hide *)
--- a/src/Tactics.v	Thu Sep 01 11:33:55 2011 -0400
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,187 +0,0 @@
-(* Copyright (c) 2008-2011, Adam Chlipala
- * 
- * This work is licensed under a
- * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
- * Unported License.
- * The license text is available at:
- *   http://creativecommons.org/licenses/by-nc-nd/3.0/
- *)
-
-Require Import Eqdep List.
-
-Require Omega.
-
-Set Implicit Arguments.
-
-
-Ltac inject H := injection H; clear H; intros; try subst.
-
-Ltac appHyps f :=
-  match goal with
-    | [ H : _ |- _ ] => f H
-  end.
-
-Ltac inList x ls :=
-  match ls with
-    | x => idtac
-    | (_, x) => idtac
-    | (?LS, _) => inList x LS
-  end.
-
-Ltac app f ls :=
-  match ls with
-    | (?LS, ?X) => f X || app f LS || fail 1
-    | _ => f ls
-  end.
-
-Ltac all f ls :=
-  match ls with
-    | (?LS, ?X) => f X; all f LS
-    | (_, _) => fail 1
-    | _ => f ls
-  end.
-
-Ltac simplHyp invOne :=
-  let invert H F :=
-    inList F invOne; (inversion H; fail)
-    || (inversion H; [idtac]; clear H; try subst) in
-  match goal with
-    | [ H : ex _ |- _ ] => destruct H
-
-    | [ H : ?F ?X = ?F ?Y |- ?G ] =>
-      (assert (X = Y); [ assumption | fail 1 ])
-      || (injection H;
-        match goal with
-          | [ |- X = Y -> G ] =>
-            try clear H; intros; try subst
-        end)
-    | [ H : ?F ?X ?U = ?F ?Y ?V |- ?G ] =>
-      (assert (X = Y); [ assumption
-        | assert (U = V); [ assumption | fail 1 ] ])
-      || (injection H;
-        match goal with
-          | [ |- U = V -> X = Y -> G ] =>
-            try clear H; intros; try subst
-        end)
-
-    | [ H : ?F _ |- _ ] => invert H F
-    | [ H : ?F _ _ |- _ ] => invert H F
-    | [ H : ?F _ _ _ |- _ ] => invert H F
-    | [ H : ?F _ _ _ _ |- _ ] => invert H F
-    | [ H : ?F _ _ _ _ _ |- _ ] => invert H F
-
-    | [ H : existT _ ?T _ = existT _ ?T _ |- _ ] => generalize (inj_pair2 _ _ _ _ _ H); clear H
-    | [ H : existT _ _ _ = existT _ _ _ |- _ ] => inversion H; clear H
-
-    | [ H : Some _ = Some _ |- _ ] => injection H; clear H
-  end.
-
-Ltac rewriteHyp :=
-  match goal with
-    | [ H : _ |- _ ] => rewrite H; auto; [idtac]
-  end.
-
-Ltac rewriterP := repeat (rewriteHyp; autorewrite with cpdt in *).
-
-Ltac rewriter := autorewrite with cpdt in *; rewriterP.
-
-Hint Rewrite app_ass : cpdt.
-
-Definition done (T : Type) (x : T) := True.
-
-Ltac inster e trace :=
-  match type of e with
-    | forall x : _, _ =>
-      match goal with
-        | [ H : _ |- _ ] =>
-          inster (e H) (trace, H)
-        | _ => fail 2
-      end
-    | _ =>
-      match trace with
-        | (_, _) =>
-          match goal with
-            | [ H : done (trace, _) |- _ ] => fail 1
-            | _ =>
-              let T := type of e in
-                match type of T with
-                  | Prop =>
-                    generalize e; intro;
-                      assert (done (trace, tt)); [constructor | idtac]
-                  | _ =>
-                    all ltac:(fun X =>
-                      match goal with
-                        | [ H : done (_, X) |- _ ] => fail 1
-                        | _ => idtac
-                      end) trace;
-                    let i := fresh "i" in (pose (i := e);
-                      assert (done (trace, i)); [constructor | idtac])
-                end
-          end
-      end
-  end.
-
-Ltac un_done :=
-  repeat match goal with
-           | [ H : done _ |- _ ] => clear H
-         end.
-
-Require Import JMeq.
-
-Ltac crush' lemmas invOne :=
-  let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence in
-    let rewriter := autorewrite with cpdt in *;
-      repeat (match goal with
-                | [ H : ?P |- _ ] =>
-                  match P with
-                    | context[JMeq] => fail 1
-                    | _ => (rewrite H; [])
-                      || (rewrite H; [ | solve [ crush' lemmas invOne ] ])
-                        || (rewrite H; [ | solve [ crush' lemmas invOne ] | solve [ crush' lemmas invOne ] ])
-                  end
-              end; autorewrite with cpdt in *)
-    in (sintuition; rewriter;
-        match lemmas with
-          | false => idtac
-          | _ => repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
-            repeat (simplHyp invOne; intuition)); un_done
-        end; sintuition; rewriter; sintuition; try omega; try (elimtype False; omega)).
-
-Ltac crush := crush' false fail.
-
-Require Import Program.Equality.
-
-Ltac dep_destruct E :=
-  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
-          end.
-
-Ltac clear_all :=
-  repeat match goal with
-           | [ H : _ |- _ ] => clear H
-         end.
-
-Ltac guess v H :=
-  repeat match type of H with
-           | forall x : ?T, _ =>
-             match type of T with
-               | Prop =>
-                 (let H' := fresh "H'" in
-                   assert (H' : T); [
-                     solve [ eauto 6 ]
-                     | generalize (H H'); clear H H'; intro H ])
-                 || fail 1
-               | _ =>
-                 (generalize (H v); clear H; intro H)
-                 || let x := fresh "x" in
-                   evar (x : T);
-                   let x' := eval cbv delta [x] in x in
-                     clear x; generalize (H x'); clear H; intro H
-             end
-         end.
-
-Ltac guessKeep v H :=
-  let H' := fresh "H'" in
-    generalize H; intro H'; guess v H'.
--- a/src/Universes.v	Thu Sep 01 11:33:55 2011 -0400
+++ b/src/Universes.v	Wed Sep 07 13:47:24 2011 -0400
@@ -8,7 +8,7 @@
  *)
 
 (* begin hide *)
-Require Import DepList Tactics.
+Require Import DepList CpdtTactics.
 
 Set Implicit Arguments.
 (* end hide *)
--- a/staging/updates.rss	Thu Sep 01 11:33:55 2011 -0400
+++ b/staging/updates.rss	Wed Sep 07 13:47:24 2011 -0400
@@ -12,6 +12,14 @@
 <docs>http://blogs.law.harvard.edu/tech/rss</docs>
 
 <item>
+        <title>Renamed "Tactics" module to "CpdtTactics"</title>
+        <pubDate>Wed, 7 Sep 2011 13:45:31 EDT</pubDate>
+        <link>http://adam.chlipala.net/cpdt/</link>
+        <author>adamc@csail.mit.edu</author>
+	<description>This avoids a name clash with a module included with Coq.</description>
+</item>
+
+<item>
         <title>A pass through Chapter 2</title>
         <pubDate>Thu, 1 Sep 2011 11:32:42 EDT</pubDate>
         <link>http://adam.chlipala.net/cpdt/</link>