diff options
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 80 | ||||
| -rw-r--r-- | doc/refman/RefMan-tacex.tex | 244 | ||||
| -rw-r--r-- | doc/refman/biblio.bib | 67 | ||||
| -rw-r--r-- | tactics/tactics.ml | 49 | ||||
| -rw-r--r-- | test-suite/success/dependentind.v | 52 | ||||
| -rw-r--r-- | theories/Classes/SetoidClass.v | 12 | ||||
| -rw-r--r-- | theories/Program/Equality.v | 56 | ||||
| -rw-r--r-- | theories/Program/Subset.v | 16 | ||||
| -rw-r--r-- | theories/Program/Tactics.v | 31 |
9 files changed, 502 insertions, 105 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 6276b547b4..4a2dad8cab 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 9837c8ba3b..4377c7ddd1 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 f8e225bd4c..cce04b4e24 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 = "{Springer-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, diff --git a/tactics/tactics.ml b/tactics/tactics.ml index dbd3aacbff..3be4f0f137 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1708,15 +1708,17 @@ let lift_together l = lift_togethern 0 l let lift_list l = List.map (lift 1) l -let make_abstract_generalize gl id concl ctx c eqs args refls coe = +let make_abstract_generalize gl id concl ctx c eqs args refls = let meta = Evarutil.new_meta() in let cstr = - (* Substitute the coerced term using equalities into the conclusion. *) - let concl = subst1 coe (subst_var id concl) in (* Abstract by equalitites *) let abseqs = it_mkProd_or_LetIn ~init:concl (List.map (fun x -> (Anonymous, None, x)) eqs) in - (* Abstract by the "generalized" hypothesis *) - let abshyp = mkProd (Name id, c, abseqs) in + (* Abstract by the "generalized" hypothesis and its equality proof *) + let term, typ = mkVar id, pf_get_hyp_typ gl id in + let abshyp = + let abshypeq = mkProd (Anonymous, mkHEq (lift 1 c) (mkRel 1) typ term, lift 1 abseqs) in + mkProd (Name id, c, abshypeq) + in (* Abstract by the extension of the context *) let genctyp = it_mkProd_or_LetIn ~init:abshyp ctx in (* The goal will become this product. *) @@ -1725,7 +1727,9 @@ let make_abstract_generalize gl id concl ctx c eqs args refls coe = let instc = mkApp (genc, Array.of_list args) in (* Then apply to the original instanciated hyp. *) let newc = mkApp (instc, [| mkVar id |]) in - (* Finaly, apply the reflexivity proofs, to get a term of type gl again *) + (* Apply the reflexivity proof for the original hyp. *) + let newc = mkApp (newc, [| mkHRefl typ term |]) in + (* Finaly, apply the remaining reflexivity proofs on the index, to get a term of type gl again *) let appeqs = mkApp (newc, Array.of_list refls) in appeqs in cstr @@ -1781,40 +1785,15 @@ let abstract_args gl id = let arity, ctx, ctxenv, c', args, eqs, refls, finalargs, env = Array.fold_left aux (pf_type_of gl f,[],env,f,[],[],[],[],env) args in - let _, _, _, coe = - let alleqslen = List.length eqs in - let ctxlen = List.length ctx in - let n_lift = alleqslen + ctxlen + 1 in - let aux (prod, c, eqsrel, coe) (name, arg, oldarg) after = - let (name, ty, arity) = destProd prod in - match kind_of_term oldarg with - | Var _ | Rel _ -> - (subst1 arg arity, mkApp (c, [|arg|]), eqsrel, coe) - | _ -> - let c' = mkApp (c, [|arg|]) in - let pred = - mkLambda (name, ty, applist (lift 1 c, (mkRel 1) :: - List.map (fun (_, x, _) -> lift 1 x) after)) - in - let coe' = - mkCoe ty arg pred coe oldarg (mkRel eqsrel) - in - (arity, c', eqsrel - 1, coe') - in - let rec fold acc l = - match l with - | hd :: tl -> fold (aux acc hd tl) tl - | [] -> acc - in - fold (lift n_lift (pf_type_of gl f), lift n_lift f, alleqslen, mkRel (succ alleqslen)) - (List.rev_map (fun (x, y, z) -> x, lift (alleqslen + 1) y, lift (alleqslen + 1) z) finalargs) - in let eqs = lift_togethern 1 eqs in let args, refls = List.rev args, List.rev refls in - Some (make_abstract_generalize gl id concl ctx c' eqs args refls coe) + Some (make_abstract_generalize gl id concl ctx c' eqs args refls) | _ -> None let abstract_generalize id gl = + Coqlib.check_required_library ["Coq";"Logic";"JMeq"]; +(* let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string "Coq.Logic.JMeq")) in *) +(* Library.require_library [qualid] None; *) let newc = abstract_args gl id in match newc with | None -> tclIDTAC gl diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v index 78edda65e1..f45b592af8 100644 --- a/test-suite/success/dependentind.v +++ b/test-suite/success/dependentind.v @@ -9,8 +9,7 @@ Inductive vector : nat -> Type := vnil : vector 0 | vcons : A -> forall n, vecto Goal forall n, forall v : vector (S n), vector n. Proof. intros n H. - dependent induction H. - autoinjection. + dependent destruction H. assumption. Save. @@ -19,11 +18,7 @@ Require Import ProofIrrelevance. Goal forall n, forall v : vector (S n), exists v' : vector n, exists a : A, v = vcons a v'. Proof. intros n H. - - dependent induction H generalizing n. - inversion H0. subst. - rewrite (UIP_refl _ _ H0). - simpl. + dependent destruction H. exists H ; exists a. reflexivity. Save. @@ -34,15 +29,13 @@ 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. -Inductive term : ctx -> type -> Type := -| ax : forall G tau, term (snoc G tau) tau -| weak : forall G tau, term G tau -> forall tau', term (snoc G tau') tau -| abs : forall G tau tau', term (snoc G tau) tau' -> term G (arrow tau tau') -| app : forall G tau tau', term G (arrow tau tau') -> term G tau -> term G tau'. +Notation " G , tau " := (snoc G tau) (at level 20, t at next level). Fixpoint conc (G D : ctx) : ctx := match D with @@ -50,25 +43,32 @@ Fixpoint conc (G D : ctx) : ctx := | snoc D' x => snoc (conc G D') x end. -Hint Unfold conc. - Notation " G ; D " := (conc G D) (at level 20). -Notation " G , D " := (snoc G D) (at level 20, D at next level). + +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'. Lemma weakening : forall G D tau, term (G ; D) tau -> forall tau', term (G , tau' ; D) tau. -Proof with simpl in * ; program_simpl ; simpl_IHs_eqs. +Proof with simpl in * ; auto ; simpl_depind. intros G D tau H. - dependent induction H generalizing G D... + dependent induction H generalizing G D. destruct D... apply weak ; apply ax. apply ax. - + destruct D... - do 2 apply weak... + narrow IHterm with G empty... + apply weak... apply weak... @@ -76,15 +76,15 @@ Proof with simpl in * ; program_simpl ; simpl_IHs_eqs. apply weak ; apply abs ; apply H. apply abs... - refine_hyp (IHterm G0 (D, t, tau))... + narrow IHterm with G0 (D, t, tau)... apply app with tau... Qed. Lemma exchange : forall G D alpha bet tau, term (G, alpha, bet ; D) tau -> term (G, bet, alpha ; D) tau. -Proof with simpl in * ; program_simpl ; simpl_IHs_eqs. - intros G D alpha bet tau H. - dependent induction H generalizing G D alpha bet. +Proof with simpl in * ; simpl_depind ; auto. + intros until 1. + dependent induction H generalizing G D alpha bet... destruct D... apply weak ; apply ax. @@ -96,8 +96,8 @@ Proof with simpl in * ; program_simpl ; simpl_IHs_eqs. apply weak... - apply abs. - refine_hyp (IHterm G0 (D, tau))... + apply abs... + narrow IHterm with G0 (D, tau)... eapply app with tau... -Qed.
\ No newline at end of file +Save. diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index c5befaa115..f61b4a4159 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -223,17 +223,21 @@ Program Instance [ sa : Setoid a R, sb : Setoid b R' ] => (** We redefine respect for binary and ternary morphims because we cannot get a satisfying instance of [Setoid (a -> b)] from some arbitrary domain and codomain setoids. We can define it on respectful Coq functions though, see [arrow_setoid] above. *) -Definition binary_respectful [ sa : Setoid a eqa, sb : Setoid b eqb, Setoid c eqc ] (m : a -> b -> c) : Prop := +Definition binary_respectful [ sa : Setoid a eqa, sb : Setoid b eqb, Setoid c eqc ] + (m : a -> b -> c) : Prop := forall x y, eqa x y -> forall z w, eqb z w -> eqc (m x z) (m y w). -Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc ] => BinaryMorphism (m : a -> b -> c) := +Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc ] => + BinaryMorphism (m : a -> b -> c) := respect2 : binary_respectful m. -Definition ternary_respectful [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, Setoid d eqd ] (m : a -> b -> c -> d) : Prop := +Definition ternary_respectful [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, Setoid d eqd ] + (m : a -> b -> c -> d) : Prop := forall x y, eqa x y -> forall z w, eqb z w -> forall u v, eqc u v -> eqd (m x z u) (m y w v). -Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, sd : Setoid d eqd ] => TernaryMorphism (m : a -> b -> c -> d) := +Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, sd : Setoid d eqd ] => + TernaryMorphism (m : a -> b -> c -> d) := respect3 : ternary_respectful m. (** Definition of the usual morphisms in [Prop]. *) diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index c570aa9836..46a1b5cf25 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -30,9 +30,7 @@ Ltac on_JMeq tac := (** Try to apply [JMeq_eq] to get back a regular equality when the two types are equal. *) Ltac simpl_one_JMeq := - on_JMeq - ltac:(fun H => let H' := fresh "H" in - assert (H' := JMeq_eq H) ; clear H ; rename H' into H). + on_JMeq ltac:(fun H => replace_hyp H (JMeq_eq H)). (** Repeat it for every possible hypothesis. *) @@ -176,10 +174,21 @@ Ltac simplify_eqs := (** A tactic that tries to remove trivial equality guards in induction hypotheses coming from [dependent induction]/[generalize_eqs] invocations. *) + Ltac simpl_IH_eq H := match type of H with - | JMeq _ _ -> _ => - refine_hyp (H (JMeq_refl _)) + | @JMeq _ ?x _ _ -> _ => + refine_hyp (H (JMeq_refl x)) + | _ -> @JMeq _ ?x _ _ -> _ => + refine_hyp (H _ (JMeq_refl x)) + | _ -> _ -> @JMeq _ ?x _ _ -> _ => + refine_hyp (H _ _ (JMeq_refl x)) + | _ -> _ -> _ -> @JMeq _ ?x _ _ -> _ => + refine_hyp (H _ _ _ (JMeq_refl x)) + | _ -> _ -> _ -> _ -> @JMeq _ ?x _ _ -> _ => + refine_hyp (H _ _ _ _ (JMeq_refl x)) + | _ -> _ -> _ -> _ -> _ -> @JMeq _ ?x _ _ -> _ => + refine_hyp (H _ _ _ _ _ (JMeq_refl x)) | ?x = _ -> _ => refine_hyp (H (refl_equal x)) | _ -> ?x = _ -> _ => @@ -198,22 +207,49 @@ Ltac simpl_IH_eqs H := repeat simpl_IH_eq H. Ltac do_simpl_IHs_eqs := match goal with - | [ H : context [ JMeq _ _ -> _ ] |- _ ] => progress (simpl_IH_eqs H) + | [ H : context [ @JMeq _ _ _ _ -> _ ] |- _ ] => progress (simpl_IH_eqs H) | [ H : context [ _ = _ -> _ ] |- _ ] => progress (simpl_IH_eqs H) end. Ltac simpl_IHs_eqs := repeat do_simpl_IHs_eqs. +Ltac simpl_depind := subst* ; autoinjections ; try discriminates ; simpl_JMeq ; simpl_IHs_eqs. + (** The following tactics allow to do induction on an already instantiated inductive predicate by first generalizing it and adding the proper equalities to the context, in a maner similar to the BasicElim tactic of "Elimination with a motive" by Conor McBride. *) +(** First a tactic to prepare for a dependent induction on an hypothesis [H]. *) + +Ltac prepare_depind H := + let oldH := fresh "old" H in + generalize_eqs H ; rename H into oldH ; (intros until H || intros until 1) ; + generalize dependent oldH ; + try (intros _ _) (* If the goal is not dependent on the hyp, we can prove a stronger statement *). + +(** The [do_depind] higher-order tactic takes an induction tactic as argument and an hypothesis + and starts a dependent induction using this tactic. *) + +Ltac do_depind tac H := + prepare_depind H ; tac H ; simpl_depind. + +(** Calls [destruct] on the generalized hypothesis, results should be similar to inversion. *) + +Tactic Notation "dependent" "destruction" ident(H) := + do_depind ltac:(fun H => destruct H ; intros) H ; subst*. + +(** Then we have wrappers for usual calls to induction. One can customize the induction tactic by + writting another wrapper calling do_depind. *) + Tactic Notation "dependent" "induction" ident(H) := - generalize_eqs H ; clear H ; (intros until 1 || intros until H) ; - induction H ; intros ; subst* ; try discriminates ; simpl_IHs_eqs. + do_depind ltac:(fun H => induction H ; intros) H. (** This tactic also generalizes the goal by the given variables before the induction. *) Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) := - generalize_eqs H ; clear H ; (intros until 1 || intros until H) ; - generalize l ; clear l ; induction H ; intros ; subst* ; try discriminates ; simpl_IHs_eqs. + do_depind ltac:(fun H => generalize l ; clear l ; induction H ; intros) H. + +(** This tactic also generalizes the goal by the given variables before the induction. *) + +Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := + do_depind ltac:(fun H => generalize l ; clear l ; induction H using c ; intros) H. diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index 54d830c899..c414dc9cd6 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -65,22 +65,6 @@ Ltac pi_subset_proof := on_subset_proof pi_subset_proof_hyp. Ltac pi_subset_proofs := repeat pi_subset_proof. -(** Clear duplicated hypotheses *) - -Ltac clear_dup := - match goal with - | [ H : ?X |- _ ] => - match goal with - | [ H' : X |- _ ] => - match H' with - | H => fail 2 - | _ => clear H' || clear H - end - end - end. - -Ltac clear_dups := repeat clear_dup. - (** The two preceding tactics in sequence. *) Ltac clear_subset_proofs := diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index bb06f37b5a..df2393ace2 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -69,6 +69,22 @@ Ltac revert_last := Ltac reverse := repeat revert_last. +(** Clear duplicated hypotheses *) + +Ltac clear_dup := + match goal with + | [ H : ?X |- _ ] => + match goal with + | [ H' : X |- _ ] => + match H' with + | H => fail 2 + | _ => clear H' || clear H + end + end + end. + +Ltac clear_dups := repeat clear_dup. + (** A non-failing subst that substitutes as much as possible. *) Tactic Notation "subst" "*" := @@ -122,7 +138,7 @@ Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) := destruc (** Try to inject any potential constructor equality hypothesis. *) Ltac autoinjection := - let tac H := inversion H ; subst ; clear H in + let tac H := progress (inversion H ; subst ; clear_dups) ; clear H in match goal with | [ H : ?f ?a = ?f' ?a' |- _ ] => tac H | [ H : ?f ?a ?b = ?f' ?a' ?b' |- _ ] => tac H @@ -169,11 +185,16 @@ Ltac add_hypothesis H' p := Tactic Notation "pose" constr(c) "as" ident(H) := assert(H:=c). +(** A tactic to replace an hypothesis by another term. *) + +Ltac replace_hyp H c := + let H' := fresh "H" in + assert(H' := c) ; clear H ; rename H' into H. + (** A tactic to refine an hypothesis by supplying some of its arguments. *) Ltac refine_hyp c := - let H' := fresh "H" in - let tac H := assert(H' := c) ; clear H ; rename H' into H in + let tac H := replace_hyp H c in match c with | ?H _ => tac H | ?H _ _ => tac H @@ -190,8 +211,8 @@ Ltac refine_hyp c := possibly using [program_simplify] to use standard goal-cleaning tactics. *) Ltac program_simplify := - simpl ; intros ; destruct_conjs ; simpl proj1_sig in * ; subst* ; try autoinjection ; try discriminates ; - try (solve [ red ; intros ; destruct_conjs ; try autoinjection ; discriminates ]). + simpl ; intros ; destruct_conjs ; simpl proj1_sig in * ; subst* ; autoinjections ; try discriminates ; + try (solve [ red ; intros ; destruct_conjs ; autoinjections ; discriminates ]). Ltac program_simpl := program_simplify ; auto with *. |