From 67e9cef251a291fab7f656f3dd0b9f2c0bde5a59 Mon Sep 17 00:00:00 2001 From: msozeau Date: Thu, 31 Jan 2008 15:24:52 +0000 Subject: 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 --- doc/refman/RefMan-tac.tex | 80 +++++++++++++++ doc/refman/RefMan-tacex.tex | 244 +++++++++++++++++++++++++++++++++++++++++++- doc/refman/biblio.bib | 67 ++++++++++-- 3 files changed, 382 insertions(+), 9 deletions(-) (limited to 'doc') 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, -- cgit v1.2.3