Debug implementation of dependent induction/dependent destruction and document it.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10490 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 382 insertions, 9 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 6276b547b..4a2dad8ca 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1547,6 +1547,86 @@ non dependent} premises of the goal. More generally, any combination of an
 
 \end{Variant}
 
+\subsection{\tt dependent induction \ident
+  \tacindex{dependent induction}
+  \label{DepInduction}}
+
+The \emph{experimental} tactic \texttt{dependent induction} performs
+induction-inversion on an instantiated inductive predicate.
+One needs to first require the {\tt Coq.Program.Equality} module to use
+this tactic. The tactic is based on the BasicElim tactic by Conor
+McBride \cite{DBLP:conf/types/McBride00} and the work of Cristina Cornes
+around inversion \cite{DBLP:conf/types/CornesT95}. From an instantiated
+inductive predicate and a goal it generates an equivalent goal where the
+hypothesis has been generalised over its indices which are then
+constrained by equalities to be the right instances. This permits to
+state lemmas without resorting to manually adding these equalities and
+still get enough information in the proofs. 
+A simple example is the following:
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+\begin{coq_example}
+Lemma le_minus : forall n:nat, n < 1 -> n = 0.
+intros n H ; induction H.
+\end{coq_example}
+
+Here we didn't get any information on the indices to help fullfill this
+proof. The problem is that when we use the \texttt{induction} tactic
+we lose information on the hypothesis instance, notably that the second
+argument is \texttt{1} here. Dependent induction solves this problem by
+adding the corresponding equality to the context.
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+\begin{coq_example}
+Require Import Coq.Program.Equality.
+Lemma le_minus : forall n:nat, n < 1 -> n = 0.
+intros n H ; dependent induction H.
+\end{coq_example}
+
+The subgoal is cleaned up as the tactic tries to automatically
+simplify the subgoals with respect to the generated equalities.
+In this enriched context it becomes possible to solve this subgoal.
+\begin{coq_example}
+reflexivity.
+\end{coq_example}
+
+Now we are in a contradictory context and the proof can be solved.
+\begin{coq_example}
+inversion H.
+\end{coq_example}
+
+This technique works with any inductive predicate.
+In fact, the \texttt{dependent induction} tactic is just a wrapper around
+the \texttt{induction} tactic. One can make its own variant by just
+writing a new tactic based on the definition found in
+\texttt{Coq.Program.Equality}. Common useful variants are the following,
+defined in the same file:
+
+\begin{Variants}
+\item {\tt dependent induction {\ident} generalizing {\ident$_1$} \dots
+    {\ident$_n$}}\tacindex{dependent induction ... generalizing}
+  
+  Does dependent induction on the hypothesis {\ident} but first
+  generalizes the goal by the given variables so that they are
+  universally quantified in the goal. This is generally what one wants
+  to do with the variables that are inside some constructors in the
+  induction hypothesis. The other ones need not be further generalized.
+
+\item {\tt dependent destruction}\tacindex{dependent destruction}
+  
+  Does the generalization of the instance but uses {\tt destruct}
+  instead of {\tt induction} on the generalized hypothesis. This gives
+  results equivalent to {\tt inversion} or {\tt dependent inversion} if
+  the hypothesis is dependent.
+\end{Variants}
+
+A larger example of dependent induction and an explanation of the
+underlying technique are developed in section~\ref{dependent-induction-example}.
+
 \subsection{\tt decompose [ {\qualid$_1$} \dots\ {\qualid$_n$} ] \term
 \label{decompose}
 \tacindex{decompose}}
diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex
index 9837c8ba3..4377c7ddd 100644
--- a/doc/refman/RefMan-tacex.tex
+++ b/doc/refman/RefMan-tacex.tex
@@ -276,7 +276,8 @@ Scheme tree_forest_ind := Induction for tree Sort Prop
   with forest_tree_ind := Induction for forest Sort Prop.
 \end{coq_example}
 
-Then we can build the combined induction principle:
+Then we can build the combined induction principle which gives the
+conjunction of the conclusions of each individual principle:
 \begin{coq_example}
 Combined Scheme tree_forest_mutind from tree_forest_ind, forest_tree_ind.
 \end{coq_example}
@@ -586,6 +587,247 @@ inversion H using leminv.
 Reset Initial.
 \end{coq_eval}
 
+\section[\tt dependent induction]{\tt dependent induction\label{dependent-induction-example}}
+\def\depind{{\tt dependent induction}~}
+\def\depdestr{{\tt dependent destruction}~}
+
+The tactics \depind and \depdestr are another solution for inverting
+inductive predicate instances and potentially doing induction at the
+same time. It is based on the Basic Elim tactic of Conor McBride which
+work by abstracting each argument of an inductive instance by a variable
+and constraining it by equalities afterwards. This way, the usual 
+{\tt induction} and {\tt destruct} tactics can be applied to the
+abstracted instance and after simplification of the equalities we get
+the expected goals.
+
+The abstracting tactic is called {\tt generalize\_eqs} and it takes as
+argument an hypothesis to generalize. It uses the {\tt JMeq} datatype
+defined in {\tt Coq.Logic.JMeq}, hence we need to require it before.
+For example, revisiting the first example of the inversion documentation above:
+
+\begin{coq_example*}
+Require Import Coq.Logic.JMeq.
+\end{coq_example*}
+
+\begin{coq_eval}
+Inductive Le : nat -> nat -> Set :=
+  | LeO : forall n:nat, Le 0 n
+  | LeS : forall n m:nat, Le n m -> Le (S n) (S m).
+Variable P : nat -> nat -> Prop.
+Variable Q : forall n m:nat, Le n m -> Prop.
+\end{coq_eval}
+
+\begin{coq_example*}
+Lemma ex : forall n m:nat, Le (S n) m -> P n m.
+intros n m H.
+\end{coq_example*}
+\begin{coq_example}
+generalize_eqs H.
+\end{coq_example}
+
+The index {\tt S n} gets abstracted by a variable here, but a
+corresponding equality is added under the abstract instance so that no
+information is actually lost. The goal is now ammenable to do induction
+or case analysis. Note that the abstract instance is also related to the
+original one using an heterogeneous equality that will become a regular
+one once the equalities are substituted. In the non-dependent case where
+the hypothesis does not appear in the goal, this equality is actually
+not needed and we can make it disappear, along with the original
+hypothesis:
+
+\begin{coq_example}
+intros gen_x gen_H _ ; clear H.
+\end{coq_example}
+
+One drawback is that in the branches one will have to
+substitute the equalities back into the instance to get the right
+assumptions. Sometimes injection of constructors will also be needed to
+recover the needed equalities. Also, some subgoals should be directly
+solved because of inconsistent contexts arising from the constraints on 
+ indices. The nice thing is that we can make a tactic based on
+discriminate and injection to automatically do such simplifications in
+any context. This is what the {\tt simpl\_depind} tactic from
+{\tt Coq.Program.Equality} does. For example, compare:
+\begin{coq_example*}
+Require Import Coq.Program.Equality.
+\end{coq_example*}
+\begin{coq_example}
+destruct gen_H.
+\end{coq_example}
+and
+\begin{coq_eval}
+Undo.
+\end{coq_eval}
+\begin{coq_example}
+destruct gen_H ; intros ; simpl_depind.
+\end{coq_example}
+
+The higher-order tactic {\tt do\_depind} defined in {\tt
+  Coq.Program.Equality} takes a tactic and combines the
+building blocks we've seen with it: generalizing by equalities, cleaning
+the goal if it's not dependent, calling the given tactic with the
+generalized induction hypothesis as argument and cleaning the subgoals
+with respect to equalities. Its most important instantiations are
+\depind and \depdestr that do induction or simply case analysis on the
+generalized hypothesis. For example we can redo what we've done manually
+with \depdestr:
+
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
+\begin{coq_example*}
+Require Import Coq.Program.Equality.
+Lemma ex : forall n m:nat, Le (S n) m -> P n m.
+intros n m H.
+\end{coq_example*}
+\begin{coq_example}
+dependent destruction H.
+\end{coq_example}
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
+
+This gives essentially the same result as inversion. Now if the
+destructed hypothesis actually appeared in the goal, the tactic would
+still be able to invert it, contrary to {\tt dependent
+ inversion}. Consider the following example on vectors:
+
+\begin{coq_example*}
+Require Import Coq.Program.Equality.
+Set Implicit Arguments.
+Variable A : Set.
+Inductive vector : nat -> Type := 
+| vnil : vector 0 
+| vcons : A -> forall n, vector n -> vector (S n).
+Goal forall n, forall v : vector (S n), 
+  exists v' : vector n, exists a : A, v = vcons a v'.
+  intros n v.
+\end{coq_example*}
+\begin{coq_example}
+  dependent destruction v.
+\end{coq_example}
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
+
+In this case, the {\tt v} variable can be replaced in the goal by the
+generalized hypothesis only when it has a type of the form {\tt vector
+ (S n)}, that is only in the second case of the {\tt destruct}. The
+first one is dismissed because {\tt S n <> 0}.
+
+This technique also works with {\tt induction} on inductive
+predicates. We will now develop an example application to the
+theory of simply-typed lambda-calculus in a dependently-typed style:
+
+\begin{coq_example*}
+Inductive type : Type :=
+| base : type
+| arrow : type -> type -> type.
+Notation " t --> t' " := (arrow t t') (at level 20, t' at next level).
+Inductive ctx : Type :=
+| empty : ctx
+| snoc : ctx -> type -> ctx.
+Notation " G , tau " := (snoc G tau) (at level 20, t at next level).
+Fixpoint conc (G D : ctx) : ctx :=
+  match D with
+    | empty => G
+    | snoc D' x => snoc (conc G D') x
+  end.
+Notation " G ; D " := (conc G D) (at level 20).
+Inductive term : ctx -> type -> Type :=
+| ax : forall G tau, term (G, tau) tau
+| weak : forall G tau, 
+  term G tau -> forall tau', term (G, tau') tau
+| abs : forall G tau tau', 
+  term (G , tau) tau' -> term G (tau --> tau')
+| app : forall G tau tau', 
+  term G (tau --> tau') -> term G tau -> term G tau'.
+\end{coq_example*}
+
+We have defined types and contexts which are snoc-lists of types. We
+also have a {\tt conc} operation that concatenates two contexts.
+The {\tt term} datatype represents in fact the possible typing
+derivations of the calculus, which are isomorphic to the well-typed
+terms, hence the name. A term is either an application of:
+\begin{itemize}
+\item the axiom rule to type a reference to the first variable in a context,
+\item the weakening rule to type an object in a larger context
+\item the abstraction or lambda rule to type a function
+\item the application to type an application of a function to an argument
+\end{itemize}
+
+Once we have this datatype we want to do proofs on it, like weakening:
+
+\begin{coq_example*}
+Lemma weakening : forall G D tau, term (G ; D) tau -> 
+  forall tau', term (G , tau' ; D) tau.
+\end{coq_example*}
+\begin{coq_eval}
+  Abort.
+\end{coq_eval}
+
+The problem here is that we can't just use {\tt induction} on the typing
+derivation because it will forget about the {\tt G ; D} constraint
+appearing in the instance. A solution would be to rewrite the goal as:
+\begin{coq_example*}
+Lemma weakening' : forall G' tau, term G' tau -> 
+  forall G D, (G ; D) = G' ->
+  forall tau', term (G, tau' ; D) tau.
+\end{coq_example*}
+\begin{coq_eval}
+  Abort.
+\end{coq_eval}
+
+With this proper separation of the index from the instance and the right
+induction loading (putting {\tt G} and {\tt D} after the inducted-on
+hypothesis), the proof will go through, but it is a very tedious
+process. One is also forced to make a wrapper lemma to get back the
+more natural statement. The \depind tactic aleviates this trouble by
+doing all of this plumbing of generalizing and substituting back automatically.
+Indeed we can simply write:
+
+\begin{coq_example*}
+Require Import Coq.Program.Tactics.
+Lemma weakening : forall G D tau, term (G ; D) tau -> 
+  forall tau', term (G , tau' ; D) tau.
+Proof with simpl in * ; simpl_depind ; auto.
+  intros G D tau H.
+  dependent induction H generalizing G D.
+\end{coq_example*}
+
+This call to \depind has an additional arguments which is a list of
+variables appearing in the instance that should be generalized in the
+goal, so that they can vary in the induction hypotheses. Generally, all
+variables appearing inside constructors of the instantiated hypothesis
+should be generalized. 
+
+\begin{coq_example}
+  Show.
+\end{coq_example}
+
+The {\tt simpl\_depind} tactic includes an automatic tactic that tries
+to simplify equalities appearing at the beginning of induction
+hypotheses, generally using trivial applications of
+reflexiviy. In some cases though, one must help the automation by giving
+some arguments first, using the {\tt narrow} tactic from  
+{\tt Coq.Init.Tactics}.
+
+\begin{coq_example*}
+destruct D... apply weak ; apply ax. apply ax.
+destruct D...
+\end{coq_example*}
+\begin{coq_example}
+Show.
+\end{coq_example}
+\begin{coq_example}
+  narrow IHterm with G empty.
+\end{coq_example}
+
+Then the automation can find that the needed equality {\tt G = G} to
+narrow the induction hypothesis further. This concludes our example.
+
+\SeeAlso The induction \ref{elim}, case \ref{case} and inversion \ref{inversion} tactics.
+
 \section[\tt autorewrite]{\tt autorewrite\label{autorewrite-example}}
 
 Here are two examples of {\tt autorewrite} use. The first one ({\em Ackermann
diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
index f8e225bd4..cce04b4e2 100644
--- a/doc/refman/biblio.bib
+++ b/doc/refman/biblio.bib
@@ -1,7 +1,7 @@
 @String{jfp   = "Journal of Functional Programming"}
 @String{lncs  = "Lecture Notes in Computer Science"}
 @String{lnai  = "Lecture Notes in Artificial Intelligence"}
-@String{SV    = "{Sprin\-ger-Verlag}"}
+@String{SV    = "{Sprin­ger-Verlag}"}
 
 @InProceedings{Aud91,
   author      = {Ph. Audebaud},
@@ -426,7 +426,7 @@ s},
   editor      = {G. Huet and G. Plotkin},
   pages       = {59--79},
   publisher   = {Cambridge University Press},
-  title       = {Inductive sets and families in {Martin-L{\"o}f's}
+  title       = {Inductive sets and families in {Martin-Löf's}
  Type Theory and their set-theoretic semantics: An inversion principle for {Martin-L\"of's} type theory}, 
   volume      = {14},
   year        = {1991}
@@ -446,7 +446,7 @@ s},
   author      = {J.-C. Filli\^atre},
   month       = sep,
   school      = {DEA d'Informatique, ENS Lyon},
-  title       = {Une proc\'edure de d\'ecision pour le Calcul des Pr\'edicats Direct. {\'E}tude et impl\'ementation dans le syst\`eme {\Coq}},
+  title       = {Une proc\'edure de d\'ecision pour le Calcul des Pr\'edicats Direct. Étude et impl\'ementation dans le syst\`eme {\Coq}},
   year        = {1994}
 }
 
@@ -460,7 +460,7 @@ s},
 }
 
 @Article{Filliatre03jfp,
-  author      = {J.-C. Filli{\^a}tre},
+  author      = {J.-C. Filliâtre},
   title       = {Verification of Non-Functional Programs 
                  using Interpretations in Type Theory},
   journal     = jfp,
@@ -478,7 +478,7 @@ s},
 @PhDThesis{Filliatre99,
   author      = {J.-C. Filli\^atre},
   title       = {Preuve de programmes imp\'eratifs en th\'eorie des types},
-  type        = {Th{\`e}se de Doctorat},
+  type        = {Thèse de Doctorat},
   school      = {Universit\'e Paris-Sud},
   year        = 1999,
   month       = {July},
@@ -597,7 +597,7 @@ s},
   author      = {D. Hirschkoff},
   month       = sep,
   school      = {DEA IARFA, Ecole des Ponts et Chauss\'ees, Paris},
-  title       = {{\'E}criture d'une tactique arithm\'etique pour le syst\`eme {\Coq}},
+  title       = {Écriture d'une tactique arithm\'etique pour le syst\`eme {\Coq}},
   year        = {1994}
 }
 
@@ -870,7 +870,7 @@ Intersection Types and Subtyping},
 }
 
 @MastersThesis{Mun94,
-  author      = {C. Mu{\~n}oz},
+  author      = {C. Muñoz},
   month       = sep,
   school      = {DEA d'Informatique Fondamentale, Universit\'e Paris 7},
   title       = {D\'emonstration automatique dans la logique propositionnelle intuitionniste},
@@ -980,7 +980,7 @@ the Calculus of Inductive Constructions}},
   institution = {INRIA},
   month       = nov,
   number      = {1795},
-  title       = {{D{\'e}veloppement de l'Algorithme d'Unification dans le Calcul des Constructions}},
+  title       = {{Développement de l'Algorithme d'Unification dans le Calcul des Constructions}},
   year        = {1992}
 }
 
@@ -1153,6 +1153,57 @@ Languages},
   year        = {1987}
 }
 
+@inproceedings{DBLP:conf/types/CornesT95,
+  author    = {Cristina Cornes and
+               Delphine Terrasse},
+  title     = {Automating Inversion of Inductive Predicates in Coq},
+  booktitle = {TYPES},
+  year      = {1995},
+  pages     = {85-104},
+  crossref  = {DBLP:conf/types/1995},
+  bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+@proceedings{DBLP:conf/types/1995,
+  editor    = {Stefano Berardi and
+               Mario Coppo},
+  title     = {Types for Proofs and Programs, International Workshop TYPES'95,
+               Torino, Italy, June 5-8, 1995, Selected Papers},
+  booktitle = {TYPES},
+  publisher = {Springer},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {1158},
+  year      = {1996},
+  isbn      = {3-540-61780-9},
+  bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@inproceedings{DBLP:conf/types/McBride00,
+  author    = {Conor McBride},
+  title     = {Elimination with a Motive},
+  booktitle = {TYPES},
+  year      = {2000},
+  pages     = {197-216},
+  ee        = {http://link.springer.de/link/service/series/0558/bibs/2277/22770197.htm},
+  crossref  = {DBLP:conf/types/2000},
+  bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@proceedings{DBLP:conf/types/2000,
+  editor    = {Paul Callaghan and
+               Zhaohui Luo and
+               James McKinna and
+               Robert Pollack},
+  title     = {Types for Proofs and Programs, International Workshop, TYPES
+               2000, Durham, UK, December 8-12, 2000, Selected Papers},
+  booktitle = {TYPES},
+  publisher = {Springer},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {2277},
+  year      = {2002},
+  isbn      = {3-540-43287-6},
+  bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
 @Comment{cross-references, must be at end}
 
 @Book{Bastad92,