diff options
39 files changed, 636 insertions, 357 deletions
@@ -121,6 +121,8 @@ Libraries (DOC TO CHECK) instead of strictly positive (see lemmas with name ending by "_full"). An alternative file ZOdiv proposes a different behavior (the one of Ocaml) when dividing by negative numbers. +- Changes in Arith: EqNat and Wf_nat now exported from Arith, some + constructions on nat that were outside Arith are now in (e.g. iter_nat). - In SetoidList, eqlistA now expresses that two lists have similar elements at the same position, while the predicate previously called eqlistA is now equivlistA (this one only states that the lists contain the same @@ -203,7 +205,11 @@ Tactics - Application of "f_equal"-style lemmas works better. - Tactics elim, case, destruct and induction now support variants eelim, ecase, edestruct and einduction. -- Tactics destruct and induction now support option "with". +- Tactics destruct and induction now support the "with" option and the + "in" clause option. If the option "in" is used, an equality is added + to remember the term to which the induction or case analysis applied + (possible source of parsing incompatibilities when destruct or induction is + part of a let-in expression in Ltac; extra parentheses are then required). - Some new intro patterns: * intro pattern "?A" genererates a fresh name based on A. Caveat about a slight loss of compatibility: @@ -238,6 +244,8 @@ Tactics matching lemma among the components of the conjunction; tactic apply also able to apply lemmas of conclusion an empty type. - Tactics "set" and "pose" can set functions using notation "(f x1..xn := c)". +- Tactic "generalize" now supports "at" options to specify occurrences + and "as" options to name the hypothesis. - New tactic "specialize H with a" or "specialize (H a)" allows to transform in-place a universally-quantified hypothesis (H : forall x, T x) into its instantiated form (H : T a). Nota: "specialize" was in fact there in earlier @@ -247,14 +255,16 @@ Tactics If H is already a negation, say ~T, then a proof of T is asked. If the current goal is a negation, say ~U, then U is saved in H afterwards, hence this new tactic "contradict" extends earlier tactic "swap", which is - now obsolete. -- tactics f_equal is now done in ML instead of Ltac: it now works on any - equality of functions, regardless of the arity of the function. -- some more debug of reflexive omega (romega), and internal clarifications. + now obsolete. +- Tactics f_equal is now done in ML instead of Ltac: it now works on any + equality of functions, regardless of the arity of the function. +- Some more debug of reflexive omega (romega), and internal clarifications. Moreover, romega now has a variant "romega with *" that can be also used on non-Z goals (nat, N, positive) via a call to a translation tactic named zify (its purpose is to Z-ify your goal...). This zify may also be used independantly of romega. +- Tactic "remember" now supports an "in" clause to remember only selected + occurrences of a term. Program @@ -369,23 +379,29 @@ Extraction corresponding to decidability of equalities are now linear instead of quadratic. -Tools +CoqIDE -- New stand-alone .vo files verifier "coqchk". - CoqIDE font defaults to monospace so as indentation to be meaningful. -- CoqIDE supports Definition/Parameter/Inductive in middle of a proof. +- CoqIDE supports nested goals and any other kind of declaration in the middle + of a proof. - Undoing non-tactic commands in CoqIDE works faster. - New CoqIDE menu for activating display of various implicit informations. +- Added the possibility to choose the location of tabs in coqide: + (in Edit->Preferences->Misc) - New Open and Save As dialogs in CoqIDE which filter *.v files. +Tools + +- New stand-alone .vo files verifier "coqchk". + Miscellaneous -- Syntax of "Test Printing Let ref" and "Test Printing If ref" changed into - "Test Printing Let for ref" and "Test Printing If for ref". -- Added the possibility to choose the location of tabs in coqide: - (in Edit->Preferences->Misc) +- Coq installation provides enough files so that Ocaml's extensions need not + the Coq sources to be compiled. - New commands "Set Whelp Server" and "Set Whelp Getter" to customize the Whelp search tool. +- Syntax of "Test Printing Let ref" and "Test Printing If ref" changed into + "Test Printing Let for ref" and "Test Printing If for ref". - An overhauled build system (new Makefiles); see dev/doc/build-system.txt Changes from V8.1gamma to V8.1 diff --git a/contrib/funind/g_indfun.ml4 b/contrib/funind/g_indfun.ml4 index 71f483fb6..dae76f2dd 100644 --- a/contrib/funind/g_indfun.ml4 +++ b/contrib/funind/g_indfun.ml4 @@ -317,7 +317,7 @@ let mkEq typ c1 c2 = let poseq_unsafe idunsafe cstr gl = let typ = Tacmach.pf_type_of gl cstr in tclTHEN - (Tactics.letin_tac true (Name idunsafe) cstr allClauses) + (Tactics.letin_tac None (Name idunsafe) cstr allClauses) (tclTHENFIRST (Tactics.assert_as true IntroAnonymous (mkEq typ (mkVar idunsafe) cstr)) Tactics.reflexivity) diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index a071add63..a6cbb3211 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -120,7 +120,8 @@ let functional_induction with_clean c princl pat = princ_infos args_as_induction_constr princ' - pat) + pat + None) subst_and_reduce g diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml index be4f9c091..dd40c5cc3 100644 --- a/contrib/interface/depends.ml +++ b/contrib/interface/depends.ml @@ -295,16 +295,18 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of | TacCut c -> depends_of_'constr c acc | TacAssert (taco, _, c) -> Option.fold_right depends_of_'tac taco (depends_of_'constr c acc) - | TacGeneralize cl -> list_union_map depends_of_'constr cl acc + | TacGeneralize cl -> + list_union_map depends_of_'constr (List.map (fun ((_,c),_) -> c) cl) + acc | TacGeneralizeDep c -> depends_of_'constr c acc - | TacLetTac (_,c,_) -> depends_of_'constr c acc + | TacLetTac (_,c,_,_) -> depends_of_'constr c acc (* Derived basic tactics *) | TacSimpleInduction _ | TacSimpleDestruct _ | TacDoubleInduction _ -> acc - | TacNewInduction (_, cwbial, cwbo, _) - | TacNewDestruct (_, cwbial, cwbo, _) -> + | TacNewInduction (_, cwbial, cwbo, _, _) + | TacNewDestruct (_, cwbial, cwbo, _, _) -> list_union_map (depends_of_'a_induction_arg depends_of_'constr_with_bindings) cwbial (Option.fold_right depends_of_'constr_with_bindings cwbo acc) diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml index c16cde7d7..ac152f906 100644 --- a/contrib/interface/pbp.ml +++ b/contrib/interface/pbp.ml @@ -166,7 +166,7 @@ let make_pbp_atomic_tactic = function TacAtom (zz, TacSplit (false,true,ImplicitBindings [make_pbp_pattern x])) | PbpGeneralize (h,args) -> let l = List.map make_pbp_pattern args in - TacAtom (zz, TacGeneralize [make_app (make_var h) l]) + TacAtom (zz, TacGeneralize [([],make_app (make_var h) l),Anonymous]) | PbpLeft -> TacAtom (zz, TacLeft (false,NoBindings)) | PbpRight -> TacAtom (zz, TacRight (false,NoBindings)) | PbpIntros l -> TacAtom (zz, TacIntroPattern l) diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml index 7f2019681..a2a504fb4 100644 --- a/contrib/interface/showproof.ml +++ b/contrib/interface/showproof.ml @@ -1185,7 +1185,7 @@ let rec natural_ntree ig ntree = | TacFix (_,n) -> natural_fix ig lh g gs n ltree | TacSplit (_,_,NoBindings) -> natural_split ig lh g gs ge [] ltree | TacSplit(_,_,ImplicitBindings l) -> natural_split ig lh g gs ge (List.map snd l) ltree - | TacGeneralize l -> natural_generalize ig lh g gs ge (List.map snd l) ltree + | TacGeneralize l -> natural_generalize ig lh g gs ge l ltree | TacRight _ -> natural_right ig lh g gs ltree | TacLeft _ -> natural_left ig lh g gs ltree | (* "Simpl" *)TacReduce (r,cl) -> @@ -1652,7 +1652,7 @@ and natural_split ig lh g gs ge la ltree = | _ -> assert false and natural_generalize ig lh g gs ge la ltree = match la with - [arg] -> + [(_,(_,arg)),_] -> let _env= (gLOB ge) in let arg1= (*dbize env*) arg in let _type_arg=type_of (Global.env()) Evd.empty arg in diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index c2569a142..b041272c1 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1151,9 +1151,12 @@ and xlate_tac = | TacSpecialize (nopt, (c,sl)) -> CT_specialize (xlate_int_opt nopt, xlate_formula c, xlate_bindings sl) | TacGeneralize [] -> xlate_error "" - | TacGeneralize (first :: cl) -> + | TacGeneralize ((([],first),Anonymous) :: cl) + when List.for_all (fun ((o,_),na) -> o = [] & na = Anonymous) cl -> CT_generalize - (CT_formula_ne_list (xlate_formula first, List.map xlate_formula cl)) + (CT_formula_ne_list (xlate_formula first, + List.map (fun ((_,c),_) -> xlate_formula c) cl)) + | TacGeneralize _ -> xlate_error "TODO: Generalize at and as" | TacGeneralizeDep c -> CT_generalize_dependent (xlate_formula c) | TacElimType c -> CT_elim_type (xlate_formula c) @@ -1163,7 +1166,7 @@ and xlate_tac = | TacCase (false,(c1,sl)) -> CT_casetac (xlate_formula c1, xlate_bindings sl) | TacElim (true,_,_) | TacCase (true,_) - | TacNewDestruct (true,_,_,_) | TacNewInduction (true,_,_,_) -> + | TacNewDestruct (true,_,_,_,_) | TacNewInduction (true,_,_,_,_) -> xlate_error "TODO: eelim, ecase, edestruct, einduction" | TacSimpleInduction h -> CT_induction (xlate_quantified_hypothesis h) | TacSimpleDestruct h -> CT_destruct (xlate_quantified_hypothesis h) @@ -1207,24 +1210,27 @@ and xlate_tac = CT_dauto(xlate_int_or_var_opt_to_int_opt a, xlate_int_opt b) | TacDAuto (a, b, _) -> xlate_error "TODO: dauto using" - | TacNewDestruct(false,a,b,c) -> + | TacNewDestruct(false,a,b,c,None) -> CT_new_destruct (List.map xlate_int_or_constr a, xlate_using b, xlate_with_names c) - | TacNewInduction(false,a,b,c) -> + | TacNewInduction(false,a,b,c,None) -> CT_new_induction (List.map xlate_int_or_constr a, xlate_using b, xlate_with_names c) + | TacNewDestruct(false,a,b,c,_) -> xlate_error "TODO: destruct in" + | TacNewInduction(false,a,b,c,_) ->xlate_error "TODO: induction in" (*| TacInstantiate (a, b, cl) -> CT_instantiate(CT_int a, xlate_formula b, assert false) *) - | TacLetTac (na, c, cl) when cl = nowhere -> + | TacLetTac (na, c, cl, true) when cl = nowhere -> CT_pose(xlate_id_opt_aux na, xlate_formula c) - | TacLetTac (na, c, cl) -> + | TacLetTac (na, c, cl, true) -> CT_lettac(xlate_id_opt ((0,0),na), xlate_formula c, (* TODO LATER: This should be shared with Unfold, but the structures are different *) xlate_clause cl) + | TacLetTac (na, c, cl, false) -> xlate_error "TODO: remember" | TacAssert (None, IntroIdentifier id, c) -> CT_assert(xlate_id_opt ((0,0),Name id), xlate_formula c) | TacAssert (None, IntroAnonymous, c) -> diff --git a/dev/base_include b/dev/base_include index 255e28a66..398f60d2b 100644 --- a/dev/base_include +++ b/dev/base_include @@ -89,6 +89,7 @@ open Indrec open Typing open Inductiveops open Unification +open Matching open Constrextern open Constrintern diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index d8cdf738d..b50a3d72b 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -9,6 +9,8 @@ A few differences in Coq ML interfaces between Coq V8.0 and V8.1 Eauto: e_resolve_constr, vernac_e_resolve_constr -> simplest_eapply Tactics: apply_with_bindings -> apply_with_bindings_wo_evars +Tactics: boolean argument of letin_tac changed its meaning (false now + means use Leibniz equality instead of a local definition) Eauto.simplest_apply -> Hiddentac.h_simplest_apply Evarutil.define_evar_as_arrow -> define_evar_as_product diff --git a/doc/common/macros.tex b/doc/common/macros.tex index 6b6c158b5..1c4fa7e1f 100755 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -125,7 +125,9 @@ \newcommand{\caseitem}{\nterm{match\_item}} \newcommand{\eqn}{\nterm{equation}} \newcommand{\ifitem}{\nterm{dep\_ret\_type}} -\newcommand{\letclauses}{\nterm{letclauses}} +\newcommand{\convclause}{\nterm{conversion\_clause}} +\newcommand{\occclause}{\nterm{occurrence\_clause}} +\newcommand{\occset}{\nterm{occurrence\_set}} \newcommand{\params}{\nterm{params}} % vernac \newcommand{\returntype}{\nterm{return\_type}} \newcommand{\idparams}{\nterm{ident\_with\_params}} diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index 71e87b3f3..e319bdbb1 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -1002,14 +1002,23 @@ syntax %{\tt preident} $|$ {\tt ident} $|$ {\tt simple\_intropattern} $|$ -{\tt hyp} \\ & $|$ & -% {\tt quantified\_hypothesis} $|$ -{\tt reference} $|$ -{\tt constr} \\ & $|$ & +{\tt reference} \\ & $|$ & +{\tt hyp} $|$ +{\tt hyp\_list} $|$ +{\tt ne\_hyp\_list} \\ & $|$ & +% {\tt quantified\_hypothesis} \\ & $|$ & +{\tt constr} $|$ +{\tt constr\_list} $|$ +{\tt ne\_constr\_list} \\ & $|$ & %{\tt castedopenconstr} $|$ {\tt integer} $|$ -{\tt int\_or\_var} \\ & $|$ & +{\tt integer\_list} $|$ +{\tt ne\_integer\_list} \\ & $|$ & +{\tt int\_or\_var} $|$ +{\tt int\_or\_var\_list} $|$ +{\tt ne\_int\_or\_var\_list} \\ & $|$ & {\tt tactic} $|$ {\tt tactic$n$} \qquad\mbox{(for $0\leq n\leq 5$)} + \end{tabular} \medskip @@ -1034,7 +1043,7 @@ use the corresponding kind of argument. \noindent \begin{tabular}{l|l|l|l} Tactic argument type & parsed as & interpreted as & as in tactic \\ -\hline \\ +\hline & & & \\ {\tt\small ident} & identifier & a user-given name & {\tt intro} \\ {\tt\small simple\_intropattern} & intro\_pattern & an intro\_pattern & {\tt intros}\\ {\tt\small hyp} & identifier & an hypothesis defined in context & {\tt clear}\\ @@ -1046,8 +1055,10 @@ Tactic argument type & parsed as & interpreted as & as in tactic \\ %%{\tt\small castedopenconstr} & term & a term with its sign. of exist. var. & {\tt refine}\\ {\tt\small integer} & integer & an integer & \\ {\tt\small int\_or\_var} & identifier or integer & an integer & {\tt do} \\ -{\tt\small tactic} & tactic at level 5 & a tactic & \\ +{\tt\small tactic} & tactic at level 5 & a tactic & \\ {\tt\small tactic$n$} & tactic at level $n$ & a tactic & \\ +{\tt\small {\nterm{entry}}\_list} & list of {\nterm{entry}} & a list of how {\nterm{entry}} is interpreted & \\ +{\tt\small ne\_{\nterm{entry}}\_list} & non-empty list of {\nterm{entry}} & a list of how {\nterm{entry}} is interpreted& \\ \end{tabular} \Rem In order to be bound in tactic definitions, each syntactic entry @@ -1059,6 +1070,12 @@ for {\tt integer}. This is the reason for introducing a special entry syntactically includes identifiers in order to be usable in tactic definitions. +\Rem The {\tt {\nterm{entry}}\_list} and {\tt ne\_{\nterm{entry}}\_list} +entries can be used in primitive tactics or in other notations at +places where a list of the underlying entry can be used: {\nterm{entry}} is +either {\tt\small constr}, {\tt\small hyp}, {\tt\small integer} or +{\tt\small int\_or\_var}. + % $Id$ %%% Local Variables: diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 3a8f6ca52..45993dd23 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -437,7 +437,8 @@ Section~\ref{pattern} to transform the goal so that it gets the form \subsection{{\tt set ( {\ident} {\tt :=} {\term} \tt )} \label{tactic:set} \tacindex{set} -\tacindex{pose}} +\tacindex{pose} +\tacindex{remember}} This replaces {\term} by {\ident} in the conclusion or in the hypotheses of the current goal and adds the new definition {\ident @@ -446,81 +447,45 @@ replacement only in the conclusion. \begin{Variants} -\item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in *}\\ - {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in * |- *}\\ - - This behaves as above but substitutes {\term} - everywhere in the goal (both in conclusion and hypotheses). - -\item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in * |-} - - This behaves the same but substitutes {\term} in - the hypotheses only (not in the conclusion). - -\item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in |- *} - - This is equivalent to {\tt set ( } {\ident} {\tt :=} {\term} {\tt - )}, i.e. it substitutes {\term} in the conclusion only. - -\item {\tt set ( {\ident$_0$} {\tt :=} {\term} {\tt ) in} {\ident$_1$}} - - This behaves the same but substitutes {\term} only in - the hypothesis named {\ident$_1$}. - -\item {\tt set (} {\ident$_0$} {\tt :=} {\term} {\tt ) in} - {\ident$_1$} {\tt at} {\num$_1$} \dots\ {\num$_n$} +\item {\tt set (} {\ident} {\tt :=} {\term} {\tt ) in {\occset}} This notation allows to specify which occurrences of {\term} have to -be substituted in the hypothesis named {\ident$_1$}. The occurrences -are numbered from left to right and are meaningful on a pure -expression using no implicit argument, notation or coercion. A -negative occurrence number means an occurrence which should not be -substituted. As an exception of the left-to-right order, the -occurrences in the {\tt return} subexpression of a {\tt match} are -considered {\em before} the occurrences in the matched term. - -For expressions using notations, or hiding implicit arguments or -coercions, it is recommended to make explicit all occurrences in -order by using {\tt Set Printing All} (see -section~\ref{SetPrintingAll}). - -\item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in |- * at} - {\num$_1$} \dots\ {\num$_n$} - -This allows to specify which occurrences of the conclusion are concerned. - -\item {\tt set (} {\ident$_0$} {\tt :=} {\term} {\tt ) in} - {\ident$_1$} {\tt at} {\num$_1^1$} \dots\ {\num$_{n_1}^1$}, \dots - {\ident$_m$} {\tt at} {\num$_1^m$} \dots {\num$_{n_m}^m$} - - It substitutes {\term} at occurrences {\num$_1^i$} \dots\ - {\num$_{n_i}^i$} of hypothesis {\ident$_i$}. Each {\tt at} part is - optional. +be substituted in the context. The {\tt in {\occset}} clause is an +occurrence clause whose syntax and behavior is described in +Section~\ref{Occurrences clauses}. \item {\tt set (} {\ident} \nelist{\binder}{} {\tt :=} {\term} {\tt )} This is equivalent to {\tt set (} {\ident} {\tt :=} {\tt fun} \nelist{\binder}{} {\tt =>} {\term} {\tt )}. -\item {\tt set (} {\ident$_0$} \nelist{\binder}{} {\tt :=} {\term} {\tt ) in} - {\ident$_1$} {\tt at} {\num$_1^1$} \dots\ {\num$_{n_1}^1$}, \dots - {\ident$_m$} {\tt at} {\num$_1^m$} \dots {\num$_{n_m}^m$} - {\tt |- *} {\tt at} {\num$'_1$} \dots\ {\num$'_n$} - - This is the more general form which combines all the previous - possibilities. - \item {\tt set } {\term} This behaves as {\tt set (} {\ident} := {\term} {\tt )} but {\ident} - is generated by {\Coq}. This variant is available for the - forms with {\tt in} too. + is generated by {\Coq}. This variant also supports an occurrence clause. + +\item {\tt set (} {\ident$_0$} \nelist{\binder}{} {\tt :=} {\term} + {\tt ) in {\occset}}\\ + {\tt set {\term} in {\occset}} + + These are the general forms which combine the previous possibilities. + +\item {\tt remember {\term} {\tt as} {\ident}} + + This behaves as {\tt set (} {\ident} := {\term} {\tt ) in *} and using a + logical (Leibniz's) equality instead of a local definition. + +\item {\tt remember {\term} {\tt as} {\ident} in {\occset}} + + This is a more general form of {\tt remember} that remembers the + occurrences of {\term} specified by an occurrences set. \item {\tt pose ( {\ident} {\tt :=} {\term} {\tt )}} This adds the local definition {\ident} := {\term} to the current context without performing any replacement in the goal or in the - hypotheses. + hypotheses. It is equivalent to {\tt set ( {\ident} {\tt :=} + {\term} {\tt ) in |-}}. \item {\tt pose (} {\ident} \nelist{\binder}{} {\tt :=} {\term} {\tt )} @@ -528,7 +493,7 @@ This allows to specify which occurrences of the conclusion are concerned. \nelist{\binder}{} {\tt =>} {\term} {\tt )}. \item{\tt pose {\term}} - + This behaves as {\tt pose (} {\ident} := {\term} {\tt )} but {\ident} is generated by {\Coq}. @@ -687,11 +652,31 @@ where $G'$ is obtained from $G$ by replacing all occurrences of $t$ by to $T$. \begin{Variants} -\item {\tt generalize \term$_1$ \dots\ \term$_n$} +\item {\tt generalize {\term$_1$ , \dots\ , \term$_n$}} Is equivalent to {\tt generalize \term$_n$; \dots\ ; generalize \term$_1$}. Note that the sequence of \term$_i$'s are processed from $n$ to $1$. + +\item {\tt generalize {\term} at {\num$_1$ \dots\ \num$_i$}} + + Is equivalent to {\tt generalize \term} but generalizing only over + the specified occurrences of {\term} (counting from left to right on the + expression printed using option {\tt Set Printing All}). + +\item {\tt generalize {\term} as {\ident}} + + Is equivalent to {\tt generalize \term} but use {\ident} to name the + generalized hypothesis. + +\item {\tt generalize {\term$_1$} at {\num$_{11}$ \dots\ \num$_{1i_1}$} + as {\ident$_1$} + , {\ldots} , + {\term$_n$} at {\num$_{n1}$ \dots\ \num$_{ni_n}$} + as {\ident$_2$}} + + This is the most general form of {\tt generalize} that combines the + previous behaviors. \item {\tt generalize dependent \term} \tacindex{generalize dependent} @@ -701,7 +686,7 @@ to $T$. \item {\tt revert \ident$_1$ \dots\ \ident$_n$}\tacindex{revert} This is equivalent to a {\tt generalize} followed by a {\tt clear} - on the given hypotheses. This tactic can be seem as reciprocal to + on the given hypotheses. This tactic can be seen as reciprocal to {\tt intros}. \end{Variants} @@ -748,44 +733,6 @@ This tactic applies to any goal. It implements the rule \end{Variants} \SeeAlso \ref{Conversion-tactics} -\subsection{Bindings list -\index{Binding list} -\label{Binding-list}} - -Tactics that take a term as argument may also support bindings list so -as to instantiate some parameters of the term by name or position. -The general form of a term equipped with a bindings list is {\tt -{\term} with {\bindinglist}} where {\bindinglist} may be of two -different forms: - -\begin{itemize} -\item In a bindings list of the form {\tt (\vref$_1$ := \term$_1$) - \dots\ (\vref$_n$ := \term$_n$)}, {\vref} is either an {\ident} or a - {\num}. The references are determined according to the type of - {\term}. If \vref$_i$ is an identifier, this identifier has to be - bound in the type of {\term} and the binding provides the tactic - with an instance for the parameter of this name. If \vref$_i$ is - some number $n$, this number denotes the $n$-th non dependent - premise of the {\term}, as determined by the type of {\term}. - - \ErrMsg \errindex{No such binder} - -\item A bindings list can also be a simple list of terms {\tt - \term$_1$ \term$_2$ \dots\term$_n$}. In that case the references to - which these terms correspond are determined by the tactic. In case - of {\tt induction}, {\tt destruct}, {\tt elim} and {\tt case} (see - Section~\ref{elim}) the terms have to provide instances for all the - dependent products in the type of \term\ while in the case of {\tt - apply}, or of {\tt constructor} and its variants, only instances for - the dependent products which are not bound in the conclusion of the - type are required. - - \ErrMsg \errindex{Not the right number of missing arguments} - -\end{itemize} - - - \subsection{\tt evar (\ident:\term) \tacindex{evar} \label{evar}} @@ -887,6 +834,101 @@ simultaneously proved are respectively {\tt forall} \end{Variants} +\subsection{Bindings list +\index{Binding list} +\label{Binding-list}} + +Tactics that take a term as argument may also support bindings list so +as to instantiate some parameters of the term by name or position. +The general form of a term equipped with a bindings list is {\tt +{\term} with {\bindinglist}} where {\bindinglist} may be of two +different forms: + +\begin{itemize} +\item In a bindings list of the form {\tt (\vref$_1$ := \term$_1$) + \dots\ (\vref$_n$ := \term$_n$)}, {\vref} is either an {\ident} or a + {\num}. The references are determined according to the type of + {\term}. If \vref$_i$ is an identifier, this identifier has to be + bound in the type of {\term} and the binding provides the tactic + with an instance for the parameter of this name. If \vref$_i$ is + some number $n$, this number denotes the $n$-th non dependent + premise of the {\term}, as determined by the type of {\term}. + + \ErrMsg \errindex{No such binder} + +\item A bindings list can also be a simple list of terms {\tt + \term$_1$ \dots\term$_n$}. In that case the references to + which these terms correspond are determined by the tactic. In case + of {\tt induction}, {\tt destruct}, {\tt elim} and {\tt case} (see + Section~\ref{elim}) the terms have to provide instances for all the + dependent products in the type of \term\ while in the case of {\tt + apply}, or of {\tt constructor} and its variants, only instances for + the dependent products which are not bound in the conclusion of the + type are required. + + \ErrMsg \errindex{Not the right number of missing arguments} + +\end{itemize} + +\subsection{Occurrences sets and occurrences clauses} +\label{Occurrences clauses} +\index{Occurrences clauses} + +An occurrences clause is a modifier to some tactics that obeys the +following syntax: + +$\!\!\!$\begin{tabular}{lcl} +{\occclause} & ::= & {\tt in} {\occset} \\ +{\occset} & ::= & + \zeroone{{\ident$_1$} \zeroone{{\tt at} {\num$_1^1$} \dots\ {\num$_{n_1}^1$}} {\tt ,} {\dots} {\tt ,} + {\ident$_m$} \zeroone{{\tt at} {\num$_1^m$} \dots {\num$_{n_m}^m$}}}\\ +& & + \zeroone{{\tt |-} + \zeroone{{\tt *} \zeroone{{\tt at} {\num$'_1$} \dots\ {\num$'_n$}}}}\\ +& | & + {\tt *} {\tt |-} + \zeroone{{\tt *} \zeroone{{\tt at} {\num$'_1$} \dots\ {\num$'_n$}}}\\ +& | & + {\tt *}\\ +\end{tabular} + +The role of an occurrence clause is to select a set of occurrences of +a {\term} in a goal. In the first case, the {{\ident$_i$} +\zeroone{{\tt at} {\num$_1^i$} \dots\ {\num$_{n_i}^i$}}} parts +indicate that occurrences have to be selected in the hypotheses named +{\ident$_i$}. If no numbers are given for hypothesis {\ident$_i$}, +then all occurrences of {\term} in the hypothesis are selected. If +numbers are given, they refer to occurrences of {\term} when the term +is printed using option {\tt Set Printing All} (see +Section~\ref{SetPrintingAll}), counting from left to right. In +particular, occurrences of {\term} in implicit arguments (see +Section~\ref{Implicit Arguments}) or coercions (see +Section~\ref{Coercions}) are counted. + +A negative occurrence number means an occurrence which should not be +substituted. As an exception to the left-to-right order, the +occurrences in the {\tt return} subexpression of a {\tt match} are +considered {\em before} the occurrences in the matched term. + +In the second case, the {\tt *} on the left of {\tt |-} means that +all occurrences of {\term} are selected in every hypothesis. + +In the first and second case, if {\tt *} is mentioned on the right of +{\tt |-}, the occurrences of the conclusion of the goal have to be +selected. If some numbers are given, then only the occurrences denoted +by these numbers are selected. In no numbers are given, all +occurrences of {\term} in the goal are selected. + +Finally, the last notation is an abbreviation for {\tt * |- *}. Note +also that {\tt |-} is optional in the first case when no {\tt *} is +given. + +Here are some tactics that understand occurrences clauses: +{\tt set}, {\tt remember}, {\tt induction}, {\tt destruct}. + +\SeeAlso~Sections~\ref{tactic:set}, \ref{Tac-induction}, \ref{SetPrintingAll}. + + \section{Negation and contradiction} \subsection{\tt absurd \term @@ -945,32 +987,35 @@ tactic \texttt{change}. All conversion tactics (including \texttt{change}) can be parameterized by the parts of the goal where the conversion can -occur. The specification of such parts are called \emph{clauses}. It -can be either the conclusion, or an hypothesis. In the case of a -defined hypothesis it is possible to specify if the conversion should -occur on the type part, the body part or both (default). - -\index{Clauses} Clauses are written after a conversion tactic (tactics +occur. This is done using \emph{goal clauses} which consists in a list +of hypotheses and, optionally, of a reference to the conclusion of the +goal. For defined hypothesis it is possible to specify if the +conversion should occur on the type part, the body part or both +(default). + +\index{Clauses} +\index{Goal clauses} +Goal clauses are written after a conversion tactic (tactics \texttt{set}~\ref{tactic:set}, \texttt{rewrite}~\ref{rewrite}, \texttt{replace}~\ref{tactic:replace} and \texttt{autorewrite}~\ref{tactic:autorewrite} also use clauses) and -are introduced by the keyword \texttt{in}. If no clause is provided, +are introduced by the keyword \texttt{in}. If no goal clause is provided, the default is to perform the conversion only in the conclusion. -The syntax and description of the various clauses follows: +The syntax and description of the various goal clauses is the following: \begin{description} -\item[\texttt{in H$_1$ $\ldots$ H$_n$ |- }] only in hypotheses $H_1 - $\ldots$ H_n$ -\item[\texttt{in H$_1$ $\ldots$ H$_n$ |- *}] in hypotheses $H_1 \ldots - H_n$ and in the conclusion -\item[\texttt{in * |-}] in every hypothesis -\item[\texttt{in *}] (equivalent to \texttt{in * |- *}) everywhere -\item[\texttt{in (type of H$_1$) (value of H$_2$) $\ldots$ |-}] in - type part of $H_1$, in the value part of $H_2$, etc. +\item[]\texttt{in {\ident}$_1$ $\ldots$ {\ident}$_n$ |- } only in hypotheses {\ident}$_1$ + \ldots {\ident}$_n$ +\item[]\texttt{in {\ident}$_1$ $\ldots$ {\ident}$_n$ |- *} in hypotheses {\ident}$_1$ \ldots + {\ident}$_n$ and in the conclusion +\item[]\texttt{in * |-} in every hypothesis +\item[]\texttt{in *} (equivalent to \texttt{in * |- *}) everywhere +\item[]\texttt{in (type of {\ident}$_1$) (value of {\ident}$_2$) $\ldots$ |-} in + type part of {\ident}$_1$, in the value part of {\ident}$_2$, etc. \end{description} -For backward compatibility, the notation \texttt{in}~$H_1\ldots H_n$ -performs the conversion in hypotheses $H_1\ldots H_n$. +For backward compatibility, the notation \texttt{in}~{\ident}$_1$\ldots {\ident}$_n$ +performs the conversion in hypotheses {\ident}$_1$\ldots {\ident}$_n$. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %voir reduction__conv_x : histoires d'univers. @@ -1451,12 +1496,28 @@ induction n. with complex predicates as the induction principles generated by {\tt Function} or {\tt Functional Scheme} may be. -\item{\tt induction {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$}}\\ - {\tt einduction {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$}} +\item \texttt{induction {\term} in *} + + This syntax tells to keep an equation between {\term} and the value + it gets in each case of the induction. + +\item \texttt{induction {\term} in {\occset}} + + This syntax is used for selecting which occurrences of {\term} the + induction has to be carried on. The {\tt in {\occset}} clause is an + occurrence clause whose syntax and behavior is described in + Section~\ref{Occurrences clause}. - This is the most general form of {\tt induction} and {\tt einduction}. - It combines the effects of the {\tt with}, {\tt as}, and {\tt - using} clauses. + When an occurrence clause is given, an equation between {\term} and + the value it gets in each case of the induction is added to the + context of the subgoals corresponding to the induction cases. + +\item{\tt induction {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occset}}\\ + {\tt einduction {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occset}} + + This is the most general form of {\tt induction} and {\tt + einduction}. It combines the effects of the {\tt with}, {\tt as}, + {\tt using}, and {\tt in} clauses. \item {\tt elim \term}\label{elim} @@ -1611,12 +1672,28 @@ last introduced hypothesis. These are synonyms of {\tt induction {\term$_1$} using {\term$_2$}} and {\tt induction {\term$_1$} using {\term$_2$} with {\bindinglist}}. -\item{\tt destruct {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$}}\\ - {\tt edestruct {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$}}\\ +\item \texttt{destruct {\term} in *} + + This syntax tells to keep an equation between {\term} and the value + it gets in each cases of the analysis. + +\item \texttt{destruct {\term} in {\occset}} + + This syntax is used for selecting which occurrences of {\term} the + case analysis has to be done on. The {\tt in {\occset}} clause is an + occurrence clause whose syntax and behavior is described in + Section~\ref{Occurrences clauses}. + + When an occurrence clause is given, an equation between {\term} and + the value it gets in each cases of the analysis is added to the + context of the subgoals corresponding to the cases. + +\item{\tt destruct {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occset}}\\ + {\tt edestruct {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occset}} This is the most general form of {\tt destruct} and {\tt edestruct}. - It combines the effects of the {\tt with}, {\tt as}, and {\tt - using} clauses. + It combines the effects of the {\tt with}, {\tt as}, {\tt using}, + and {\tt in} clauses. \item{\tt case \term}\label{case}\tacindex{case} @@ -1627,10 +1704,12 @@ last introduced hypothesis. \item{\tt case\_eq \term}\label{case_eq}\tacindex{case\_eq} The tactic {\tt case\_eq} is a variant of the {\tt case} tactic that - allow to perform case analysis on a term without completely - forgetting its original form. This is done by generating - equalities between the original form of the term and the outcomes of - the case analysis. + allow to perform case analysis on a term without completely + forgetting its original form. This is done by generating equalities + between the original form of the term and the outcomes of the case + analysis. The effect of this tactic is similar to the effect of {\tt + destruct {\term} in |- *} to the exception that no new hypotheses + is introduced in the context. \item {\tt case {\term} with {\bindinglist}} @@ -2063,7 +2142,7 @@ This happens if \term$_1$ does not occur in the goal. Rewrite only the given occurrences of \term$_1'$. Occurrences are specified from left to right as for \texttt{pattern} (\S \ref{pattern}). The rewrite is always performed using setoid - rewriting, even for leibniz equality, so one has to + rewriting, even for Leibniz's equality, so one has to \texttt{Import Setoid} to use this variant. \item {\tt rewrite {\term} by {\tac}} @@ -2379,7 +2458,7 @@ Abort. Beware that \texttt{injection} yields always an equality in a sigma type whenever the injected object has a dependent type. -\Rem There is a special case for dependant pairs. If we have a decidable +\Rem There is a special case for dependent pairs. If we have a decidable equality over the type of the first argument, then it is safe to do the projection on the second one, and so {\tt injection} will work fine. To define such an equality, you have to use the {\tt Scheme} command @@ -2521,7 +2600,7 @@ latter is first introduced in the local context using on the equalities it generates), the corresponding name $p_{ij}$ in the list must be replaced by a sublist of the form {\tt [$p_{ij1}$ \ldots $p_{ijq}$]} (or, equivalently, {\tt ($p_{ij1}$, - \ldots, $p_{ijq}$)}) where $q$ is the number of subequations + \ldots, $p_{ijq}$)}) where $q$ is the number of subequalities obtained from splitting the original equation. Here is an example. \begin{coq_eval} @@ -3502,7 +3581,7 @@ Require Import List. \end{coq_example*} \begin{coq_example} Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => - generalize X1 X2; decide equality : eqdec. + generalize X1, X2; decide equality : eqdec. Goal forall a b:list (nat * nat), {a = b} + {a <> b}. info auto with eqdec. @@ -3774,7 +3853,7 @@ general principle of mutual induction for objects in type {\term$_i$}. \subsection{Automatic declaration of schemes} \comindex{Set Equality Scheme} \comindex{Set Elimination Schemes} -It is possible to desactive the automatic declaration of the induction +It is possible to deactivate the automatic declaration of the induction principles when defining a new inductive type with the {\tt UnSet Elimination Schemes} command. It may be reactivated at any time with {\tt Set Elimination Schemes}. @@ -3782,7 +3861,7 @@ reactivated at any time with {\tt Set Elimination Schemes}. You can also activate the automatic declaration of those boolean equalities (see the second variant of {\tt Scheme}) with the {\tt Set Equality Scheme} - command. However you have to be carefull with this option since + command. However you have to be careful with this option since \Coq~ may now reject well-defined inductive types because it cannot compute a boolean equality for them. diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 73614797a..ecc48dfe2 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -102,7 +102,8 @@ let init_id = id_of_string "Init" let arith_id = id_of_string "Arith" let datatypes_id = id_of_string "Datatypes" -let logic_module = make_dir ["Coq";"Init";"Logic"] +let logic_module_name = ["Coq";"Init";"Logic"] +let logic_module = make_dir logic_module_name let logic_type_module = make_dir ["Coq";"Init";"Logic_Type"] let datatypes_module = make_dir ["Coq";"Init";"Datatypes"] let arith_module = make_dir ["Coq";"Arith";"Arith"] @@ -202,7 +203,8 @@ let coq_eq_congr = lazy_init_constant ["Logic"] "f_equal" let coq_eq_sym = lazy_init_constant ["Logic"] "sym_eq" let coq_f_equal2 = lazy_init_constant ["Logic"] "f_equal2" -let build_coq_eq_data () = { +let build_coq_eq_data () = + let _ = check_required_library logic_module_name in { eq = Lazy.force coq_eq_eq; refl = Lazy.force coq_eq_refl; ind = Lazy.force coq_eq_ind; diff --git a/lib/util.ml b/lib/util.ml index 5a5905859..4089dc03d 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -42,6 +42,11 @@ let located_iter2 f (_,a) (_,b) = f a b exception Error_in_file of string * (bool * string * loc) * exn +(* Mapping under pairs *) + +let on_fst f (a,b) = (f a,b) +let on_snd f (a,b) = (a,f b) + (* Projections from triplets *) let pi1 (a,_,_) = a @@ -552,6 +557,13 @@ let list_unique_index x = | [] -> raise Not_found in index_x 1 +let list_fold_right_i f i l = + let rec it_list_f i l a = match l with + | [] -> a + | b::l -> f (i-1) b (it_list_f (i-1) l a) + in + it_list_f (List.length l + i) l + let list_fold_left_i f = let rec it_list_f i a = function | [] -> a @@ -1169,6 +1181,7 @@ let pr_semicolon () = str ";" ++ spc () let pr_bar () = str "|" ++ spc () let pr_arg pr x = spc () ++ pr x let pr_opt pr = function None -> mt () | Some x -> pr_arg pr x +let pr_opt_no_spc pr = function None -> mt () | Some x -> pr x let nth n = str (ordinal n) diff --git a/lib/util.mli b/lib/util.mli index e715feca3..bc1a9cc26 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -52,6 +52,11 @@ val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit exception Error_in_file of string * (bool * string * loc) * exn +(* Mapping under pairs *) + +val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c +val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b + (*s Projections from triplets *) val pi1 : 'a * 'b * 'c -> 'a @@ -121,6 +126,7 @@ val list_unique_index : 'a -> 'a list -> int val list_index0 : 'a -> 'a list -> int val list_iter3 : ('a -> 'b -> 'c -> unit) -> 'a list -> 'b list -> 'c list -> unit val list_iter_i : (int -> 'a -> unit) -> 'a list -> unit +val list_fold_right_i : (int -> 'a -> 'b -> 'b) -> int -> 'a list -> 'b -> 'b val list_fold_left_i : (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a val list_fold_right_and_left : ('a -> 'b -> 'b list -> 'a) -> 'b list -> 'a -> 'a @@ -257,6 +263,7 @@ val pr_semicolon : unit -> std_ppcmds val pr_bar : unit -> std_ppcmds val pr_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds +val pr_opt_no_spc : ('a -> std_ppcmds) -> 'a option -> std_ppcmds val nth : int -> std_ppcmds val prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index ebf28e8eb..5ab401550 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -113,6 +113,13 @@ let guess_lpar_coloneq = let guess_lpar_colon = Gram.Entry.of_parser "guess_lpar_colon" (guess_lpar_ipat ":") +let lookup_at_as_coma = + Gram.Entry.of_parser "lookup_at_as_coma" + (fun strm -> + match Stream.npeek 1 strm with + | [("",(","|"at"|"as"))] -> () + | _ -> raise Stream.Failure) + open Constr open Prim open Tactic @@ -286,7 +293,7 @@ GEXTEND Gram | IDENT "vm_compute" -> CbvVm | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul | IDENT "fold"; cl = LIST1 constr -> Fold cl - | IDENT "pattern"; pl = LIST1 pattern_occ SEP","-> Pattern pl ] ] + | IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> Pattern pl ] ] ; (* This is [red_tactic] including possible extensions *) red_expr: @@ -299,7 +306,7 @@ GEXTEND Gram | IDENT "vm_compute" -> CbvVm | IDENT "unfold"; ul = LIST1 unfold_occ -> Unfold ul | IDENT "fold"; cl = LIST1 constr -> Fold cl - | IDENT "pattern"; pl = LIST1 pattern_occ -> Pattern pl + | IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> Pattern pl | s = IDENT -> ExtraRedExpr s ] ] ; hypident: @@ -314,19 +321,27 @@ GEXTEND Gram hypident_occ: [ [ (id,l)=hypident; occs=occs -> ((occs,id),l) ] ] ; - clause: - [ [ "in"; "*"; occs=occs -> + in_clause: + [ [ "*"; occs=occs -> {onhyps=None; onconcl=true; concl_occs=occs} - | "in"; "*"; "|-"; (b,occs)=concl_occ -> + | "*"; "|-"; (b,occs)=concl_occ -> {onhyps=None; onconcl=b; concl_occs=occs} - | "in"; hl=LIST0 hypident_occ SEP","; "|-"; (b,occs)=concl_occ -> + | hl=LIST0 hypident_occ SEP","; "|-"; (b,occs)=concl_occ -> {onhyps=Some hl; onconcl=b; concl_occs=occs} - | "in"; hl=LIST0 hypident_occ SEP"," -> - {onhyps=Some hl; onconcl=false; concl_occs=[]} - | occs=occs -> - {onhyps=Some[]; onconcl=true; concl_occs=occs} - | -> - {onhyps=Some[]; onconcl=true; concl_occs=[]} ] ] + | hl=LIST0 hypident_occ SEP"," -> + {onhyps=Some hl; onconcl=false; concl_occs=[]} ] ] + ; + clause_dft_concl: + [ [ "in"; cl = in_clause -> cl + | occs=occs -> {onhyps=Some[]; onconcl=true; concl_occs=occs} + | -> {onhyps=Some[]; onconcl=true; concl_occs=[]} ] ] + ; + clause_dft_all: + [ [ "in"; cl = in_clause -> cl + | -> {onhyps=None; onconcl=true; concl_occs=[]} ] ] + ; + opt_clause: + [ [ "in"; cl = in_clause -> Some cl | -> None ] ] ; concl_occ: [ [ "*"; occs = occs -> (true,occs) @@ -377,6 +392,9 @@ GEXTEND Gram with_names: [ [ "as"; ipat = simple_intropattern -> ipat | -> IntroAnonymous ] ] ; + as_name: + [ [ "as"; id = ident -> Names.Name id | -> Names.Anonymous ] ] + ; by_tactic: [ [ IDENT "by"; tac = tactic_expr LEVEL "3" -> TacComplete tac | -> TacId [] ] ] @@ -451,13 +469,15 @@ GEXTEND Gram TacMutualCofix (false,id,List.map mk_cofix_tac fd) | IDENT "pose"; (id,b) = bindings_with_parameters -> - TacLetTac (Names.Name id,b,nowhere) - | IDENT "pose"; b = constr -> - TacLetTac (Names.Anonymous,b,nowhere) - | IDENT "set"; (id,c) = bindings_with_parameters; p = clause -> - TacLetTac (Names.Name id,c,p) - | IDENT "set"; c = constr; p = clause -> - TacLetTac (Names.Anonymous,c,p) + TacLetTac (Names.Name id,b,nowhere,true) + | IDENT "pose"; b = constr; na = as_name -> + TacLetTac (na,b,nowhere,true) + | IDENT "set"; (id,c) = bindings_with_parameters; p = clause_dft_concl -> + TacLetTac (Names.Name id,c,p,true) + | IDENT "set"; c = constr; na = as_name; p = clause_dft_concl -> + TacLetTac (na,c,p,true) + | IDENT "remember"; c = constr; na = as_name; p = clause_dft_all -> + TacLetTac (na,c,p,false) (* Begin compatibility *) | IDENT "assert"; id = lpar_id_coloneq; c = lconstr; ")" -> @@ -472,7 +492,14 @@ GEXTEND Gram TacAssert (None,ipat,c) | IDENT "cut"; c = constr -> TacCut c - | IDENT "generalize"; lc = LIST1 constr -> TacGeneralize lc + | IDENT "generalize"; c = constr -> + TacGeneralize [(([],c),Names.Anonymous)] + | IDENT "generalize"; c = constr; l = LIST1 constr -> + TacGeneralize (List.map (fun c -> (([],c),Names.Anonymous)) (c::l)) + | IDENT "generalize"; c = constr; lookup_at_as_coma; nl = occs; + na = as_name; + l = LIST0 [","; c = pattern_occ; na = as_name -> (c,na)] -> + TacGeneralize (((nl,c),na)::l) | IDENT "generalize"; IDENT "dependent"; c = constr -> TacGeneralizeDep c | IDENT "specialize"; n = OPT natural; lcb = constr_with_bindings -> @@ -483,17 +510,21 @@ GEXTEND Gram | IDENT "simple"; IDENT"induction"; h = quantified_hypothesis -> TacSimpleInduction h | IDENT "induction"; lc = LIST1 induction_arg; ids = with_names; - el = OPT eliminator -> TacNewInduction (false,lc,el,ids) + el = OPT eliminator; cl = opt_clause -> + TacNewInduction (false,lc,el,ids,cl) | IDENT "einduction"; lc = LIST1 induction_arg; ids = with_names; - el = OPT eliminator -> TacNewInduction (true,lc,el,ids) + el = OPT eliminator; cl = opt_clause -> + TacNewInduction (true,lc,el,ids,cl) | IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis; h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2) | IDENT "simple"; IDENT "destruct"; h = quantified_hypothesis -> TacSimpleDestruct h | IDENT "destruct"; lc = LIST1 induction_arg; ids = with_names; - el = OPT eliminator -> TacNewDestruct (false,lc,el,ids) + el = OPT eliminator; cl = opt_clause -> + TacNewDestruct (false,lc,el,ids,cl) | IDENT "edestruct"; lc = LIST1 induction_arg; ids = with_names; - el = OPT eliminator -> TacNewDestruct (true,lc,el,ids) + el = OPT eliminator; cl = opt_clause -> + TacNewDestruct (true,lc,el,ids,cl) | IDENT "decompose"; IDENT "record" ; c = constr -> TacDecomposeAnd c | IDENT "decompose"; IDENT "sum"; c = constr -> TacDecomposeOr c | IDENT "decompose"; "["; l = LIST1 smart_global; "]"; c = constr @@ -544,14 +575,14 @@ GEXTEND Gram (* Equivalence relations *) | IDENT "reflexivity" -> TacReflexivity - | IDENT "symmetry"; cls = clause -> TacSymmetry cls + | IDENT "symmetry"; cl = clause_dft_concl -> TacSymmetry cl | IDENT "transitivity"; c = constr -> TacTransitivity c (* Equality and inversion *) - | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause; t=opt_by_tactic -> - TacRewrite (false,l,cl,t) - | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause; t=opt_by_tactic -> - TacRewrite (true,l,cl,t) + | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; + cl = clause_dft_concl; t=opt_by_tactic -> TacRewrite (false,l,cl,t) + | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ","; + cl = clause_dft_concl; t=opt_by_tactic -> TacRewrite (true,l,cl,t) | IDENT "dependent"; k = [ IDENT "simple"; IDENT "inversion" -> SimpleInversion | IDENT "inversion" -> FullInversion @@ -573,9 +604,10 @@ GEXTEND Gram TacInversion (InversionUsing (c,cl), hyp) (* Conversion *) - | r = red_tactic; cl = clause -> TacReduce (r, cl) + | r = red_tactic; cl = clause_dft_concl -> TacReduce (r, cl) (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *) - | IDENT "change"; (oc,c) = conversion; cl = clause -> TacChange (oc,c,cl) + | IDENT "change"; (oc,c) = conversion; cl = clause_dft_concl -> + TacChange (oc,c,cl) ] ] ; END;; diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 57f1e80bd..c0dbc0eff 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -370,6 +370,13 @@ let pr_with_names = function | IntroAnonymous -> mt () | ipat -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat) +let pr_as_name = function + | Anonymous -> mt () + | Name id -> str "as " ++ pr_lident (dummy_loc,id) + +let pr_pose_as_style prc na c = + spc() ++ prc c ++ pr_as_name na + let pr_pose prlc prc na c = match na with | Anonymous -> spc() ++ prc c | Name id -> spc() ++ surround (pr_id id ++ str " :=" ++ spc() ++ prlc c) @@ -706,14 +713,18 @@ and pr_atom1 = function pr_assertion pr_lconstr pr_constr ipat c) | TacGeneralize l -> hov 1 (str "generalize" ++ spc () ++ - prlist_with_sep spc pr_constr l) + prlist_with_sep pr_coma (fun (cl,na) -> + pr_with_occurrences pr_constr cl ++ pr_as_name na) + l) | TacGeneralizeDep c -> hov 1 (str "generalize" ++ spc () ++ str "dependent" ++ pr_constrarg c) - | TacLetTac (na,c,cl) when cl = nowhere -> + | TacLetTac (na,c,cl,true) when cl = nowhere -> hov 1 (str "pose" ++ pr_pose pr_lconstr pr_constr na c) - | TacLetTac (na,c,cl) -> - hov 1 (str "set" ++ pr_pose pr_lconstr pr_constr na c ++ + | TacLetTac (na,c,cl,b) -> + hov 1 ((if b then str "set" else str "remember") ++ + (if b then pr_pose pr_lconstr else pr_pose_as_style) + pr_constr na c ++ pr_clauses pr_ident cl) (* | TacInstantiate (n,c,ConclLocation ()) -> hov 1 (str "instantiate" ++ spc() ++ @@ -728,18 +739,20 @@ and pr_atom1 = function (* Derived basic tactics *) | TacSimpleInduction h -> hov 1 (str "simple induction" ++ pr_arg pr_quantified_hypothesis h) - | TacNewInduction (ev,h,e,ids) -> + | TacNewInduction (ev,h,e,ids,cl) -> hov 1 (str (with_evars ev "induction") ++ spc () ++ prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++ pr_with_names ids ++ - pr_opt pr_eliminator e) + pr_opt pr_eliminator e ++ + pr_opt_no_spc (pr_clauses pr_ident) cl) | TacSimpleDestruct h -> hov 1 (str "simple destruct" ++ pr_arg pr_quantified_hypothesis h) - | TacNewDestruct (ev,h,e,ids) -> + | TacNewDestruct (ev,h,e,ids,cl) -> hov 1 (str (with_evars ev "destruct") ++ spc () ++ prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++ pr_with_names ids ++ - pr_opt pr_eliminator e) + pr_opt pr_eliminator e ++ + pr_opt_no_spc (pr_clauses pr_ident) cl) | TacDoubleInduction (h1,h2) -> hov 1 (str "double induction" ++ diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index a8ddfadb2..5c31fcee6 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -337,29 +337,30 @@ let rec mlexpr_of_atomic_tactic = function <:expr< Tacexpr.TacAssert $mlexpr_of_option mlexpr_of_tactic t$ $ipat$ $mlexpr_of_constr c$ >> | Tacexpr.TacGeneralize cl -> - <:expr< Tacexpr.TacGeneralize $mlexpr_of_list mlexpr_of_constr cl$ >> + <:expr< Tacexpr.TacGeneralize + $mlexpr_of_list + (mlexpr_of_pair mlexpr_of_occ_constr mlexpr_of_name) cl$ >> | Tacexpr.TacGeneralizeDep c -> <:expr< Tacexpr.TacGeneralizeDep $mlexpr_of_constr c$ >> - | Tacexpr.TacLetTac (na,c,cl) -> + | Tacexpr.TacLetTac (na,c,cl,b) -> let na = mlexpr_of_name na in let cl = mlexpr_of_clause_pattern cl in - <:expr< Tacexpr.TacLetTac $na$ $mlexpr_of_constr c$ $cl$ >> + <:expr< Tacexpr.TacLetTac $na$ $mlexpr_of_constr c$ $cl$ + $mlexpr_of_bool b$ >> (* Derived basic tactics *) | Tacexpr.TacSimpleInduction h -> <:expr< Tacexpr.TacSimpleInduction ($mlexpr_of_quantified_hypothesis h$) >> - | Tacexpr.TacNewInduction (false,cl,cbo,ids) -> + | Tacexpr.TacNewInduction (false,cl,cbo,ids,cls) -> let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in let ids = mlexpr_of_intro_pattern ids in -(* let ids = mlexpr_of_option mlexpr_of_intro_pattern ids in *) -(* <:expr< Tacexpr.TacNewInduction $mlexpr_of_induction_arg c$ $cbo$ $ids$>> *) - <:expr< Tacexpr.TacNewInduction False $mlexpr_of_list mlexpr_of_induction_arg cl$ $cbo$ $ids$>> + <:expr< Tacexpr.TacNewInduction False $mlexpr_of_list mlexpr_of_induction_arg cl$ $cbo$ $ids$ $mlexpr_of_option mlexpr_of_clause cls$ >> | Tacexpr.TacSimpleDestruct h -> <:expr< Tacexpr.TacSimpleDestruct $mlexpr_of_quantified_hypothesis h$ >> - | Tacexpr.TacNewDestruct (false,c,cbo,ids) -> + | Tacexpr.TacNewDestruct (false,c,cbo,ids,cls) -> let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in let ids = mlexpr_of_intro_pattern ids in - <:expr< Tacexpr.TacNewDestruct False $mlexpr_of_list mlexpr_of_induction_arg c$ $cbo$ $ids$ >> + <:expr< Tacexpr.TacNewDestruct False $mlexpr_of_list mlexpr_of_induction_arg c$ $cbo$ $ids$ $mlexpr_of_option mlexpr_of_clause cls$ >> (* Context management *) | Tacexpr.TacClear (b,l) -> diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 22a370aaf..bc483cfc3 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -131,16 +131,16 @@ val subst_term : constr -> constr -> constr (* [replace_term d e c] replaces [d] by [e] in [c] *) val replace_term : constr -> constr -> constr -> constr -(* [subst_term_occ occl c d] replaces occurrences of [Rel 1] at - positions [occl] by [c] in [d] *) +(* [subst_term_occ_gen occl n c d] replaces occurrences of [c] at + positions [occl], counting from [n], by [Rel 1] in [d] *) val subst_term_occ_gen : int list -> int -> constr -> types -> int * types -(* [subst_term_occ occl c d] replaces occurrences of [Rel 1] at - positions [occl] by [c] in [d] (see also Note OCC) *) +(* [subst_term_occ occl c d] replaces occurrences of [c] at + positions [occl] by [Rel 1] in [d] (see also Note OCC) *) val subst_term_occ : int list -> constr -> constr -> constr -(* [subst_term_occ_decl occl c decl] replaces occurrences of [Rel 1] at - positions [occl] by [c] in [decl] *) +(* [subst_term_occ_decl occl c decl] replaces occurrences of [c] at + positions [occl] by [Rel 1] in [decl] *) val subst_term_occ_decl : int list -> constr -> named_declaration -> named_declaration diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index 34699c5fd..d0b015552 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -27,6 +27,7 @@ type rec_flag = bool (* true = recursive false = not recursive *) type advanced_flag = bool (* true = advanced false = basic *) type split_flag = bool (* true = exists false = split *) type hidden_flag = bool (* true = internal use false = user-level *) +type letin_flag = bool (* true = use local def false = use Leibniz *) type raw_red_flag = | FBeta @@ -147,17 +148,17 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacMutualCofix of hidden_flag * identifier * (identifier * 'constr) list | TacCut of 'constr | TacAssert of 'tac option * intro_pattern_expr * 'constr - | TacGeneralize of 'constr list + | TacGeneralize of ('constr with_occurrences * name) list | TacGeneralizeDep of 'constr - | TacLetTac of name * 'constr * 'id gclause + | TacLetTac of name * 'constr * 'id gclause * letin_flag (* Derived basic tactics *) | TacSimpleInduction of quantified_hypothesis | TacNewInduction of evars_flag * 'constr with_bindings induction_arg list * - 'constr with_bindings option * intro_pattern_expr + 'constr with_bindings option * intro_pattern_expr * 'id gclause option | TacSimpleDestruct of quantified_hypothesis | TacNewDestruct of evars_flag * 'constr with_bindings induction_arg list * - 'constr with_bindings option * intro_pattern_expr + 'constr with_bindings option * intro_pattern_expr * 'id gclause option | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis | TacDecomposeAnd of 'constr diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index c4b7ad13c..133524ba7 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id:$ *) +(* $Id$ *) open Util open Pp @@ -261,7 +261,8 @@ let add_justification_hyps keep items gls = | _ -> let id=pf_get_new_id local_hyp_prefix gls in keep:=Idset.add id !keep; - letin_tac false (Names.Name id) c Tacexpr.nowhere gls in + tclTHEN (letin_tac None (Names.Name id) c Tacexpr.nowhere) + (thin_body [id]) gls in tclMAP add_aux items gls let prepare_goal items gls = @@ -807,7 +808,7 @@ let rec build_function args body = let define_tac id args body gls = let t = build_function args body in - letin_tac true (Name id) t Tacexpr.nowhere gls + letin_tac None (Name id) t Tacexpr.nowhere gls (* tactics for reconsider *) diff --git a/tactics/equality.ml b/tactics/equality.ml index b8e868f37..b0c5a29eb 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1181,7 +1181,7 @@ let subst_one x gl = let introtac = function (id,None,_) -> intro_using id | (id,Some hval,htyp) -> - letin_tac true (Name id) + letin_tac None (Name id) (mkCast(replace_term varx rhs hval,DEFAULTcast, replace_term varx rhs htyp)) nowhere in diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index a9a8da193..bb279b5ba 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -75,5 +75,5 @@ let let_evar name typ gls = let evd = Evd.create_goal_evar_defs gls.sigma in let evd',evar = Evarutil.new_evar evd (pf_env gls) typ in Refiner.tclTHEN (Refiner.tclEVARS (evars_of evd')) - (Tactics.letin_tac true name evar nowhere) gls + (Tactics.letin_tac None name evar nowhere) gls diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index c3b7e0a8b..0a9ed111f 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -61,13 +61,16 @@ let h_mutual_cofix b id l = (mutual_cofix id l) let h_cut c = abstract_tactic (TacCut (inj_open c)) (cut c) -let h_generalize cl = - abstract_tactic (TacGeneralize (List.map inj_open cl)) - (generalize cl) +let h_generalize_gen cl = + abstract_tactic (TacGeneralize (List.map (on_fst inj_occ) cl)) + (generalize_gen (List.map (on_fst Redexpr.out_with_occurrences) cl)) +let h_generalize cl = + h_generalize_gen (List.map (fun c -> (([],c),Names.Anonymous)) cl) let h_generalize_dep c = abstract_tactic (TacGeneralizeDep (inj_open c))(generalize_dep c) -let h_let_tac na c cl = - abstract_tactic (TacLetTac (na,inj_open c,cl)) (letin_tac true na c cl) +let h_let_tac b na c cl = + let with_eq = if b then None else Some true in + abstract_tactic (TacLetTac (na,inj_open c,cl,b)) (letin_tac with_eq na c cl) let h_instantiate n c ido = (Evar_tactics.instantiate n c ido) (* abstract_tactic (TacInstantiate (n,c,cls)) @@ -78,12 +81,12 @@ let h_simple_induction h = abstract_tactic (TacSimpleInduction h) (simple_induct h) let h_simple_destruct h = abstract_tactic (TacSimpleDestruct h) (simple_destruct h) -let h_new_induction ev c e idl = - abstract_tactic (TacNewInduction (ev,List.map inj_ia c,Option.map inj_open_wb e,idl)) - (new_induct ev c e idl) -let h_new_destruct ev c e idl = - abstract_tactic (TacNewDestruct (ev,List.map inj_ia c,Option.map inj_open_wb e,idl)) - (new_destruct ev c e idl) +let h_new_induction ev c e idl cl = + abstract_tactic (TacNewInduction (ev,List.map inj_ia c,Option.map inj_open_wb e,idl,cl)) + (new_induct ev c e idl cl) +let h_new_destruct ev c e idl cl = + abstract_tactic (TacNewDestruct (ev,List.map inj_ia c,Option.map inj_open_wb e,idl,cl)) + (new_destruct ev c e idl cl) let h_specialize n d = abstract_tactic (TacSpecialize (n,inj_open_wb d)) (specialize n d) let h_lapply c = abstract_tactic (TacLApply (inj_open c)) (cut_and_apply c) diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 49415649b..bb88518c9 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -52,8 +52,10 @@ val h_cofix : identifier option -> tactic val h_cut : constr -> tactic val h_generalize : constr list -> tactic +val h_generalize_gen : (constr with_occurrences * name) list -> tactic val h_generalize_dep : constr -> tactic -val h_let_tac : name -> constr -> Tacticals.clause -> tactic +val h_let_tac : letin_flag -> name -> constr -> + Tacticals.clause -> tactic val h_instantiate : int -> Rawterm.rawconstr -> (identifier * hyp_location_flag, unit) location -> tactic @@ -63,10 +65,12 @@ val h_simple_induction : quantified_hypothesis -> tactic val h_simple_destruct : quantified_hypothesis -> tactic val h_new_induction : evars_flag -> constr with_ebindings induction_arg list -> - constr with_ebindings option -> intro_pattern_expr -> tactic + constr with_ebindings option -> intro_pattern_expr -> + Tacticals.clause option -> tactic val h_new_destruct : evars_flag -> constr with_ebindings induction_arg list -> - constr with_ebindings option -> intro_pattern_expr -> tactic + constr with_ebindings option -> intro_pattern_expr -> + Tacticals.clause option -> tactic val h_specialize : int option -> constr with_ebindings -> tactic val h_lapply : constr -> tactic diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 58d7e358c..5fb45299f 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -587,15 +587,15 @@ let intern_unfold ist (l,qid) = (l,intern_evaluable ist qid) let intern_flag ist red = { red with rConst = List.map (intern_evaluable ist) red.rConst } -let intern_constr_occurrence ist (l,c) = (l,intern_constr ist c) +let intern_constr_with_occurrences ist (l,c) = (l,intern_constr ist c) let intern_red_expr ist = function | Unfold l -> Unfold (List.map (intern_unfold ist) l) | Fold l -> Fold (List.map (intern_constr ist) l) | Cbv f -> Cbv (intern_flag ist f) | Lazy f -> Lazy (intern_flag ist f) - | Pattern l -> Pattern (List.map (intern_constr_occurrence ist) l) - | Simpl o -> Simpl (Option.map (intern_constr_occurrence ist) o) + | Pattern l -> Pattern (List.map (intern_constr_with_occurrences ist) l) + | Simpl o -> Simpl (Option.map (intern_constr_with_occurrences ist) o) | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r ) -> r @@ -711,12 +711,15 @@ let rec intern_atomic lf ist x = TacAssert (Option.map (intern_tactic ist) otac, intern_intro_pattern lf ist ipat, intern_constr_gen (otac<>None) ist c) - | TacGeneralize cl -> TacGeneralize (List.map (intern_constr ist) cl) + | TacGeneralize cl -> + TacGeneralize (List.map (fun (c,na) -> + intern_constr_with_occurrences ist c, + intern_name lf ist na) cl) | TacGeneralizeDep c -> TacGeneralizeDep (intern_constr ist c) - | TacLetTac (na,c,cls) -> + | TacLetTac (na,c,cls,b) -> let na = intern_name lf ist na in TacLetTac (na,intern_constr ist c, - (clause_app (intern_hyp_location ist) cls)) + (clause_app (intern_hyp_location ist) cls),b) (* Automation tactics *) | TacTrivial (lems,l) -> TacTrivial (List.map (intern_constr ist) lems,l) @@ -734,16 +737,18 @@ let rec intern_atomic lf ist x = (* Derived basic tactics *) | TacSimpleInduction h -> TacSimpleInduction (intern_quantified_hypothesis ist h) - | TacNewInduction (ev,lc,cbo,ids) -> + | TacNewInduction (ev,lc,cbo,ids,cls) -> TacNewInduction (ev,List.map (intern_induction_arg ist) lc, Option.map (intern_constr_with_bindings ist) cbo, - (intern_intro_pattern lf ist ids)) + intern_intro_pattern lf ist ids, + Option.map (clause_app (intern_hyp_location ist)) cls) | TacSimpleDestruct h -> TacSimpleDestruct (intern_quantified_hypothesis ist h) - | TacNewDestruct (ev,c,cbo,ids) -> + | TacNewDestruct (ev,c,cbo,ids,cls) -> TacNewDestruct (ev,List.map (intern_induction_arg ist) c, Option.map (intern_constr_with_bindings ist) cbo, - (intern_intro_pattern lf ist ids)) + intern_intro_pattern lf ist ids, + Option.map (clause_app (intern_hyp_location ist)) cls) | TacDoubleInduction (h1,h2) -> let h1 = intern_quantified_hypothesis ist h1 in let h2 = intern_quantified_hypothesis ist h2 in @@ -777,7 +782,7 @@ let rec intern_atomic lf ist x = | TacReduce (r,cl) -> TacReduce (intern_red_expr ist r, clause_app (intern_hyp_location ist) cl) | TacChange (occl,c,cl) -> - TacChange (Option.map (intern_constr_occurrence ist) occl, + TacChange (Option.map (intern_constr_with_occurrences ist) occl, (if occl = None & cl.onhyps = None & cl.concl_occs = [] then intern_type ist c else intern_constr ist c), clause_app (intern_hyp_location ist) cl) @@ -1462,7 +1467,8 @@ let interp_flag ist env red = let interp_pattern ist sigma env (l,c) = (interp_int_or_var_list ist l, interp_constr ist sigma env c) -let pf_interp_pattern ist gl = interp_pattern ist (project gl) (pf_env gl) +let pf_interp_constr_with_occurrences ist gl = + interp_pattern ist (project gl) (pf_env gl) let interp_red_expr ist sigma env = function | Unfold l -> Unfold (List.map (interp_unfold ist env) l) @@ -2072,11 +2078,15 @@ and interp_atomic ist gl = function abstract_tactic (TacAssert (t,ipat,inj_open c)) (Tactics.forward (Option.map (interp_tactic ist) t) (interp_intro_pattern ist gl ipat) c) - | TacGeneralize cl -> h_generalize (pf_interp_constr_list ist gl cl) + | TacGeneralize cl -> + h_generalize_gen + (List.map (fun (c,na) -> + pf_interp_constr_with_occurrences ist gl c, + interp_fresh_name ist gl na) cl) | TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c) - | TacLetTac (na,c,clp) -> + | TacLetTac (na,c,clp,b) -> let clp = interp_clause ist gl clp in - h_let_tac (interp_fresh_name ist gl na) (pf_interp_constr ist gl c) clp + h_let_tac b (interp_fresh_name ist gl na) (pf_interp_constr ist gl c) clp (* Automation tactics *) | TacTrivial (lems,l) -> @@ -2097,16 +2107,18 @@ and interp_atomic ist gl = function (* Derived basic tactics *) | TacSimpleInduction h -> h_simple_induction (interp_quantified_hypothesis ist h) - | TacNewInduction (ev,lc,cbo,ids) -> + | TacNewInduction (ev,lc,cbo,ids,cls) -> h_new_induction ev (List.map (interp_induction_arg ist gl) lc) (Option.map (interp_constr_with_bindings ist gl) cbo) (interp_intro_pattern ist gl ids) + (Option.map (interp_clause ist gl) cls) | TacSimpleDestruct h -> h_simple_destruct (interp_quantified_hypothesis ist h) - | TacNewDestruct (ev,c,cbo,ids) -> + | TacNewDestruct (ev,c,cbo,ids,cls) -> h_new_destruct ev (List.map (interp_induction_arg ist gl) c) (Option.map (interp_constr_with_bindings ist gl) cbo) (interp_intro_pattern ist gl ids) + (Option.map (interp_clause ist gl) cls) | TacDoubleInduction (h1,h2) -> let h1 = interp_quantified_hypothesis ist h1 in let h2 = interp_quantified_hypothesis ist h2 in @@ -2145,7 +2157,7 @@ and interp_atomic ist gl = function | TacReduce (r,cl) -> h_reduce (pf_interp_red_expr ist gl r) (interp_clause ist gl cl) | TacChange (occl,c,cl) -> - h_change (Option.map (pf_interp_pattern ist gl) occl) + h_change (Option.map (pf_interp_constr_with_occurrences ist gl) occl) (if occl = None & cl.onhyps = None & cl.concl_occs = [] then pf_interp_type ist gl c else pf_interp_constr ist gl c) @@ -2351,15 +2363,15 @@ let subst_unfold subst (l,e) = let subst_flag subst red = { red with rConst = List.map (subst_evaluable subst) red.rConst } -let subst_constr_occurrence subst (l,c) = (l,subst_rawconstr subst c) +let subst_constr_with_occurrences subst (l,c) = (l,subst_rawconstr subst c) let subst_redexp subst = function | Unfold l -> Unfold (List.map (subst_unfold subst) l) | Fold l -> Fold (List.map (subst_rawconstr subst) l) | Cbv f -> Cbv (subst_flag subst f) | Lazy f -> Lazy (subst_flag subst f) - | Pattern l -> Pattern (List.map (subst_constr_occurrence subst) l) - | Simpl o -> Simpl (Option.map (subst_constr_occurrence subst) o) + | Pattern l -> Pattern (List.map (subst_constr_with_occurrences subst) l) + | Simpl o -> Simpl (Option.map (subst_constr_with_occurrences subst) o) | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> r let subst_raw_may_eval subst = function @@ -2401,9 +2413,10 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacCut c -> TacCut (subst_rawconstr subst c) | TacAssert (b,na,c) -> TacAssert (Option.map (subst_tactic subst) b,na,subst_rawconstr subst c) - | TacGeneralize cl -> TacGeneralize (List.map (subst_rawconstr subst) cl) + | TacGeneralize cl -> + TacGeneralize (List.map (on_fst (subst_constr_with_occurrences subst))cl) | TacGeneralizeDep c -> TacGeneralizeDep (subst_rawconstr subst c) - | TacLetTac (id,c,clp) -> TacLetTac (id,subst_rawconstr subst c,clp) + | TacLetTac (id,c,clp,b) -> TacLetTac (id,subst_rawconstr subst c,clp,b) (* Automation tactics *) | TacTrivial (lems,l) -> TacTrivial (List.map (subst_rawconstr subst) lems,l) @@ -2416,13 +2429,13 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with (* Derived basic tactics *) | TacSimpleInduction h as x -> x - | TacNewInduction (ev,lc,cbo,ids) -> + | TacNewInduction (ev,lc,cbo,ids,cls) -> TacNewInduction (ev,List.map (subst_induction_arg subst) lc, - Option.map (subst_raw_with_bindings subst) cbo, ids) + Option.map (subst_raw_with_bindings subst) cbo, ids, cls) | TacSimpleDestruct h as x -> x - | TacNewDestruct (ev,c,cbo,ids) -> + | TacNewDestruct (ev,c,cbo,ids,cls) -> TacNewDestruct (ev,List.map (subst_induction_arg subst) c, - Option.map (subst_raw_with_bindings subst) cbo, ids) + Option.map (subst_raw_with_bindings subst) cbo, ids, cls) | TacDoubleInduction (h1,h2) as x -> x | TacDecomposeAnd c -> TacDecomposeAnd (subst_rawconstr subst c) | TacDecomposeOr c -> TacDecomposeOr (subst_rawconstr subst c) @@ -2449,7 +2462,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with (* Conversion *) | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl) | TacChange (occl,c,cl) -> - TacChange (Option.map (subst_constr_occurrence subst) occl, + TacChange (Option.map (subst_constr_with_occurrences subst) occl, subst_rawconstr subst c, cl) (* Equivalence relations *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9812b5f82..c81d7f317 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1131,24 +1131,50 @@ let true_cut = assert_tac true (* Generalize tactics *) (**************************) -let generalize_goal gl c cl = +let generalized_name c t cl = function + | Name id as na -> na + | Anonymous -> + match kind_of_term c with + | Var id -> + (* Keep the name even if not occurring: may be used by intros later *) + Name id + | _ -> + if noccurn 1 cl then Anonymous else + (* On ne s'etait pas casse la tete : on avait pris pour nom de + variable la premiere lettre du type, meme si "c" avait ete une + constante dont on aurait pu prendre directement le nom *) + named_hd (Global.env()) t Anonymous + +let generalize_goal gl i ((occs,c),na) cl = let t = pf_type_of gl c in - match kind_of_term c with + let decls,cl = decompose_prod_n_assum i cl in + let dummy_prod = it_mkProd_or_LetIn mkProp decls in + let newdecls,_ = decompose_prod_n_assum i (subst_term c dummy_prod) in + let cl' = subst_term_occ occs c (it_mkProd_or_LetIn cl newdecls) in + let na = generalized_name c t cl' na in + mkProd (na,t,cl') + +(* + match kind_of_term cl with + | App (f,[|a|]) when isLambda f & eq_constr a c -> + (* Assume tactic pattern has been applied first *) + let na = match kind_of_term c with Var id -> Name id | _ -> Anonymous in + mkProd_name (pf_env gl) (na,t,mkApp (f,[|mkRel 1|])) + | _ -> + match kind_of_term c with | Var id -> (* The choice of remembering or not a non dependent name has an impact on the future Intro naming strategy! *) (* if dependent c cl then mkNamedProd id t cl else mkProd (Anonymous,t,cl) *) - mkNamedProd id t cl + mkNamedProd id t cl | _ -> let cl' = subst_term c cl in if noccurn 1 cl' then mkProd (Anonymous,t,cl) - (* On ne se casse pas la tete : on prend pour nom de variable - la premiere lettre du type, meme si "ci" est une - constante et qu'on pourrait prendre directement son nom *) - else - prod_name (Global.env()) (Anonymous, t, cl') + else + mkProd_name (pf_env gl) (Anonymous, t, cl') +*) let generalize_dep c gl = let env = pf_env gl in @@ -1171,16 +1197,19 @@ let generalize_dep c gl = | _ -> tothin in let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in - let cl'' = generalize_goal gl c cl' in + let cl'' = generalize_goal gl 0 (([],c),Anonymous) cl' in let args = Array.to_list (instance_from_named_context to_quantify_rev) in tclTHEN (apply_type cl'' (c::args)) (thin (List.rev tothin')) gl - -let generalize lconstr gl = - let newcl = List.fold_right (generalize_goal gl) lconstr (pf_concl gl) in - apply_type newcl lconstr gl + +let generalize_gen lconstr gl = + let newcl = + list_fold_right_i (generalize_goal gl) 0 lconstr (pf_concl gl) in + apply_type newcl (List.map (fun ((_,c),_) -> c) lconstr) gl + +let generalize l = generalize_gen (List.map (fun c -> (([],c),Anonymous)) l) let revert hyps gl = tclTHEN (generalize (List.map mkVar hyps)) (clear hyps) gl @@ -1203,7 +1232,7 @@ let quantify lconstr = [letin_tac b na c (occ_hyp,occ_ccl) gl] transforms [...x1:T1(c),...,x2:T2(c),... |- G(c)] into - [...x:T;x1:T1(x),...,x2:T2(x),... |- G(x)] if [b] is false or + [...x:T;Heqx:(x=c);x1:T1(x),...,x2:T2(x),... |- G(x)] if [b] is false or [...x:=c:T;x1:T1(x),...,x2:T2(x),... |- G(x)] if [b] is true [occ_hyp,occ_ccl] tells which occurrences of [c] have to be substituted; @@ -1325,11 +1354,21 @@ let letin_tac with_eq name c occs gl = error ("The variable "^(string_of_id x)^" is already declared") in let (depdecls,lastlhyp,ccl)= letin_abstract id c occs gl in let t = pf_type_of gl c in - let newcl = mkNamedLetIn id c t ccl in + let newcl,eq_tac = match with_eq with + | Some lr -> + let heq = fresh_id [] (add_prefix "Heq" id) gl in + let eqdata = build_coq_eq_data () in + let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in + let eq = applist (eqdata.eq,args) in + let refl = applist (eqdata.refl, [t;mkVar id]) in + mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)), + tclTHEN (intro_gen (IntroMustBe heq) lastlhyp true) (thin_body [heq;id]) + | None -> + mkNamedLetIn id c t ccl, tclIDTAC in tclTHENLIST [ convert_concl_no_check newcl DEFAULTcast; intro_gen (IntroMustBe id) lastlhyp true; - if with_eq then tclIDTAC else thin_body [id]; + eq_tac; tclMAP convert_hyp_no_check depdecls ] gl (* Tactics "pose proof" (usetac=None) and "assert" (otherwise) *) @@ -1506,14 +1545,14 @@ let atomize_param_of_ind (indref,nparams) hyp0 gl = | Var id -> let x = fresh_id [] id gl in tclTHEN - (letin_tac true (Name x) (mkVar id) allClauses) + (letin_tac None (Name x) (mkVar id) allClauses) (atomize_one (i-1) ((mkVar x)::avoid)) gl | _ -> let id = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) Anonymous in let x = fresh_id [] id gl in tclTHEN - (letin_tac true (Name x) c allClauses) + (letin_tac None (Name x) c allClauses) (atomize_one (i-1) ((mkVar x)::avoid)) gl else tclIDTAC gl @@ -2439,18 +2478,19 @@ let induction_without_atomization isrec with_evars elim names lid gl = then error "Not the right number of induction arguments" else induction_from_context_l isrec with_evars elim_info lid names gl -let new_induct_gen isrec with_evars elim names (c,lbind) gl = +let new_induct_gen isrec with_evars elim names (c,lbind) cls gl = match kind_of_term c with | Var id when not (mem_named_context id (Global.named_context())) - & lbind = NoBindings & not with_evars -> + & lbind = NoBindings & not with_evars & cls = None -> induction_with_atomization_of_ind_arg isrec with_evars elim names (id,lbind) gl | _ -> let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) Anonymous in let id = fresh_id [] x gl in + let with_eq = if cls <> None then Some (not (isVar c)) else None in tclTHEN - (letin_tac true (Name id) c allClauses) + (letin_tac with_eq (Name id) c (Option.default allClauses cls)) (induction_with_atomization_of_ind_arg isrec with_evars elim names (id,lbind)) gl @@ -2467,7 +2507,8 @@ let new_induct_gen_l isrec with_evars elim names lc gl = | [] -> tclIDTAC gl | c::l' -> match kind_of_term c with - | Var id when not (mem_named_context id (Global.named_context())) -> + | Var id when not (mem_named_context id (Global.named_context())) + & not with_evars -> let _ = newlc:= id::!newlc in atomize_list l' gl @@ -2480,7 +2521,7 @@ let new_induct_gen_l isrec with_evars elim names lc gl = let _ = newlc:=id::!newlc in let _ = letids:=id::!letids in tclTHEN - (letin_tac true (Name id) c allClauses) + (letin_tac None (Name id) c allClauses) (atomize_list newl') gl in tclTHENLIST [ @@ -2495,10 +2536,10 @@ let new_induct_gen_l isrec with_evars elim names lc gl = gl -let induct_destruct_l isrec with_evars lc elim names = +let induct_destruct_l isrec with_evars lc elim names cls = (* Several induction hyps: induction scheme is mandatory *) let _ = - if elim = None + if elim = None then error ("Induction scheme must be given when several induction hypothesis.\n" ^ "Example: induction x1 x2 x3 using my_scheme.") in @@ -2509,6 +2550,9 @@ let induct_destruct_l isrec with_evars lc elim names = | ElimOnConstr (x,NoBindings) -> x | _ -> error "don't know where to find some argument") lc in + if cls <> None then + error + "'in' clause not supported when several induction hypothesis are given"; new_induct_gen_l isrec with_evars elim names newlc @@ -2517,27 +2561,28 @@ let induct_destruct_l isrec with_evars lc elim names = principles). TODO: really unify induction with one and induction with several args *) -let induct_destruct isrec with_evars lc elim names = +let induct_destruct isrec with_evars lc elim names cls = assert (List.length lc > 0); (* ensured by syntax, but if called inside caml? *) if List.length lc = 1 then (* induction on one arg: use old mechanism *) try let c = List.hd lc in match c with - | ElimOnConstr c -> new_induct_gen isrec with_evars elim names c + | ElimOnConstr c -> new_induct_gen isrec with_evars elim names c cls | ElimOnAnonHyp n -> tclTHEN (intros_until_n n) (tclLAST_HYP (fun c -> - new_induct_gen isrec with_evars elim names (c,NoBindings))) + new_induct_gen isrec with_evars elim names (c,NoBindings) cls)) (* Identifier apart because id can be quantified in goal and not typable *) | ElimOnIdent (_,id) -> tclTHEN (tclTRY (intros_until_id id)) - (new_induct_gen isrec with_evars elim names (mkVar id,NoBindings)) + (new_induct_gen isrec with_evars elim names + (mkVar id,NoBindings) cls) with (* If this fails, try with new mechanism but if it fails too, then the exception is the first one. *) | x -> - (try induct_destruct_l isrec with_evars lc elim names + (try induct_destruct_l isrec with_evars lc elim names cls with _ -> raise x) - else induct_destruct_l isrec with_evars lc elim names + else induct_destruct_l isrec with_evars lc elim names cls diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 1b2b7b38f..bfb49cba7 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -251,7 +251,7 @@ val elim : val simple_induct : quantified_hypothesis -> tactic val new_induct : evars_flag -> constr with_ebindings induction_arg list -> - constr with_ebindings option -> intro_pattern_expr -> tactic + constr with_ebindings option -> intro_pattern_expr -> clause option -> tactic (*s Case analysis tactics. *) @@ -260,7 +260,7 @@ val simplest_case : constr -> tactic val simple_destruct : quantified_hypothesis -> tactic val new_destruct : evars_flag -> constr with_ebindings induction_arg list -> - constr with_ebindings option -> intro_pattern_expr -> tactic + constr with_ebindings option -> intro_pattern_expr -> clause option -> tactic (*s Eliminations giving the type instead of the proof. *) @@ -323,11 +323,11 @@ val cut_in_parallel : constr list -> tactic val assert_as : bool -> intro_pattern_expr -> constr -> tactic val forward : tactic option -> intro_pattern_expr -> constr -> tactic - +val letin_tac : bool option -> name -> constr -> clause -> tactic val true_cut : name -> constr -> tactic -val letin_tac : bool -> name -> constr -> clause -> tactic val assert_tac : bool -> name -> constr -> tactic val generalize : constr list -> tactic +val generalize_gen : ((int list * constr) * name) list -> tactic val generalize_dep : constr -> tactic val tclABSTRACT : identifier option -> tactic -> tactic diff --git a/test-suite/success/pattern.v b/test-suite/success/pattern.v new file mode 100644 index 000000000..28d0bd556 --- /dev/null +++ b/test-suite/success/pattern.v @@ -0,0 +1,7 @@ +(* Test pattern with dependent occurrences; Note that it does not + behave as the succession of three generalize because each + quantification introduces new occurrences that are automatically + abstracted with the numbering still based on the original statement *) + +Goal (id true,id false)=(id true,id true). +generalize bool at 2 4 6 8 10 as B, true at 3 as tt, false as ff. diff --git a/theories/Arith/Arith_base.v b/theories/Arith/Arith_base.v index b076de2af..2d54f0e8d 100644 --- a/theories/Arith/Arith_base.v +++ b/theories/Arith/Arith_base.v @@ -18,3 +18,5 @@ Require Export Between. Require Export Peano_dec. Require Export Compare_dec. Require Export Factorial. +Require Export EqNat. +Require Export Wf_nat. diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v index f5c3260de..1bf6102e9 100644 --- a/theories/Arith/Minus.v +++ b/theories/Arith/Minus.v @@ -51,11 +51,18 @@ Qed. (** * Diagonal *) -Lemma minus_n_n : forall n, 0 = n - n. +Lemma minus_diag : forall n, n - n = 0. Proof. induction n; simpl in |- *; auto with arith. Qed. -Hint Resolve minus_n_n: arith v62. + +Lemma minus_diag_reverse : forall n, 0 = n - n. +Proof. + auto using minus_diag. +Qed. +Hint Resolve minus_diag_reverse: arith v62. + +Notation minus_n_n := minus_diag_reverse. (** * Simplification *) diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index 5e7ee4153..e87901080 100644 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v @@ -257,3 +257,22 @@ Proof. repeat split; assumption || intros n' (HPn',Hminn'); apply le_antisym; auto. Qed. + +Unset Implicit Arguments. + +(** [n]th iteration of the function [f] *) + +Fixpoint iter_nat (n:nat) (A:Type) (f:A -> A) (x:A) {struct n} : A := + match n with + | O => x + | S n' => f (iter_nat n' A f x) + end. + +Theorem iter_nat_plus : + forall (n m:nat) (A:Type) (f:A -> A) (x:A), + iter_nat (n + m) A f x = iter_nat n A f (iter_nat m A f x). +Proof. + simple induction n; + [ simpl in |- *; auto with arith + | intros; simpl in |- *; apply f_equal with (f := f); apply H ]. +Qed. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 25316c278..17a645c8f 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -388,7 +388,7 @@ Class [ equ : Equivalence A eqA, PreOrder A R ] => PartialOrder := Instance partial_order_antisym [ PartialOrder A eqA R ] : ! Antisymmetric A eqA R. Proof with auto. - reduce_goal. pose partial_order_equivalence as poe. do 3 red in poe. + reduce_goal. pose proof partial_order_equivalence as poe. do 3 red in poe. apply <- poe. firstorder. Qed. diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 602b11900..705fb3bdf 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -77,15 +77,6 @@ Ltac case_eq x := generalize (refl_equal x); pattern x at -1; case x. Tactic Notation "rewrite_all" constr(eq) := repeat rewrite eq in *. Tactic Notation "rewrite_all" "<-" constr(eq) := repeat rewrite <- eq in *. -(* Keeping a copy of an expression *) - -Ltac remembertac x a := - let x := fresh x in - let H := fresh "Heq" x in - (set (x:=a) in *; assert (H: x=a) by reflexivity; clearbody x). - -Tactic Notation "remember" constr(c) "as" ident(x) := remembertac x c. - (** Tactics for applying equivalences. The following code provides tactics "apply -> t", "apply <- t", diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index 59c2029a3..12c0cc264 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -11,6 +11,7 @@ (*i $Id$ i*) Require Import NaryFunctions. +Require Import Wf_nat. Require Export ZArith. Require Export DoubleType. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index c8c0c8b16..946fdf618 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -26,8 +26,8 @@ Ltac destruct_pairs := repeat (destruct_one_pair). (** Destruct one existential package, keeping the name of the hypothesis for the first component. *) Ltac destruct_one_ex := - let tac H := let ph := fresh "H" in destruct H as [H ph] in - let tacT H := let ph := fresh "X" in destruct H as [H ph] in + let tac H := let ph := fresh "H" in (destruct H as [H ph]) in + let tacT H := let ph := fresh "X" in (destruct H as [H ph]) in match goal with | [H : (ex _) |- _] => tac H | [H : (sig ?P) |- _ ] => tac H @@ -120,20 +120,20 @@ Ltac on_call f tac := (* Destructs calls to f in hypothesis or conclusion, useful if f creates a subset object. *) Ltac destruct_call f := - let tac t := destruct t in on_call f tac. + let tac t := (destruct t) in on_call f tac. Ltac destruct_calls f := repeat destruct_call f. Ltac destruct_call_in f H := - let tac t := destruct t in + let tac t := (destruct t) in let T := type of H in on_application f tac T. Ltac destruct_call_as f l := - let tac t := destruct t as l in on_call f tac. + let tac t := (destruct t as l) in on_call f tac. Ltac destruct_call_as_in f l H := - let tac t := destruct t as l in + let tac t := (destruct t as l) in let T := type of H in on_application f tac T. @@ -200,8 +200,6 @@ Ltac add_hypothesis H' p := end end. -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 := diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v index b05acd730..c99582a25 100644 --- a/theories/ZArith/Zmisc.v +++ b/theories/ZArith/Zmisc.v @@ -8,6 +8,7 @@ (*i $Id$ i*) +Require Import Wf_nat. Require Import BinInt. Require Import Zcompare. Require Import Zorder. @@ -18,11 +19,6 @@ Open Local Scope Z_scope. (** Iterators *) (** [n]th iteration of the function [f] *) -Fixpoint iter_nat (n:nat) (A:Type) (f:A -> A) (x:A) {struct n} : A := - match n with - | O => x - | S n' => f (iter_nat n' A f x) - end. Fixpoint iter_pos (n:positive) (A:Type) (f:A -> A) (x:A) {struct n} : A := match n with @@ -38,15 +34,6 @@ Definition iter (n:Z) (A:Type) (f:A -> A) (x:A) := | Zneg p => x end. -Theorem iter_nat_plus : - forall (n m:nat) (A:Type) (f:A -> A) (x:A), - iter_nat (n + m) A f x = iter_nat n A f (iter_nat m A f x). -Proof. - simple induction n; - [ simpl in |- *; auto with arith - | intros; simpl in |- *; apply f_equal with (f := f); apply H ]. -Qed. - Theorem iter_nat_of_P : forall (p:positive) (A:Type) (f:A -> A) (x:A), iter_pos p A f x = iter_nat (nat_of_P p) A f x. diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v index f3f357de1..7ee8b9766 100644 --- a/theories/ZArith/Zpower.v +++ b/theories/ZArith/Zpower.v @@ -8,6 +8,7 @@ (*i $Id$ i*) +Require Import Wf_nat. Require Import ZArith_base. Require Export Zpow_def. Require Import Omega. diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 92ca06647..a6ae7240c 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -514,12 +514,14 @@ let compute_bl_tact ind lnamesparrec nparrec = new_induct false [ (Tacexpr.ElimOnConstr ((mkVar freshn), Rawterm.NoBindings))] None - Genarg.IntroAnonymous; + Genarg.IntroAnonymous + None; intro_using freshm; new_destruct false [ (Tacexpr.ElimOnConstr ((mkVar freshm), Rawterm.NoBindings))] None - Genarg.IntroAnonymous; + Genarg.IntroAnonymous + None; intro_using freshz; intros; tclTRY ( @@ -541,7 +543,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). None ( Genarg.IntroOrAndPattern [[ Genarg.IntroIdentifier fresht; - Genarg.IntroIdentifier freshz]])) gl + Genarg.IntroIdentifier freshz]]) None) gl ]); (* Ci a1 ... an = Ci b1 ... bn @@ -629,12 +631,14 @@ let compute_lb_tact ind lnamesparrec nparrec = new_induct false [Tacexpr.ElimOnConstr ((mkVar freshn),Rawterm.NoBindings)] None - Genarg.IntroAnonymous; + Genarg.IntroAnonymous + None; intro_using freshm; new_destruct false [Tacexpr.ElimOnConstr ((mkVar freshm),Rawterm.NoBindings)] None - Genarg.IntroAnonymous; + Genarg.IntroAnonymous + None; intro_using freshz; intros; tclTRY ( @@ -748,7 +752,8 @@ let compute_dec_tact ind lnamesparrec nparrec = (new_destruct false [Tacexpr.ElimOnConstr (eqbnm,Rawterm.NoBindings)] None - Genarg.IntroAnonymous) + Genarg.IntroAnonymous + None) Auto.default_auto ); Pfedit.by ( @@ -759,7 +764,7 @@ let compute_dec_tact ind lnamesparrec nparrec = None (Genarg.IntroOrAndPattern [ [Genarg.IntroAnonymous]; - [Genarg.IntroIdentifier freshH2]]) + [Genarg.IntroIdentifier freshH2]]) None ); let arfresh = Array.of_list fresh_first_intros in let xargs = Array.sub arfresh 0 (2*nparrec) in |