diff options
33 files changed, 226 insertions, 177 deletions
@@ -76,8 +76,8 @@ Vernacular commands or axioms a theorem or definition relies on. - "Add Rec LoadPath" now provides references to libraries using partially qualified names (this holds also for coqtop/coqc option -R). -- SearchAbout supports negated search criteria and reference to logical objects - by their notation. +- SearchAbout supports negated search criteria, reference to logical objects + by their notation, and more generally search of subterms. - "Declare ML Module" now allows to import .cmxs files when Coq is compiled in native code with a version of OCaml that supports native Dynlink (>= 3.11). diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4 index e7c7fde8d..51dce4f76 100644 --- a/contrib/interface/centaur.ml4 +++ b/contrib/interface/centaur.ml4 @@ -545,7 +545,9 @@ let solve_hook n = let abort_hook s = output_results_nl (ctf_AbortedMessage !global_request_id s) let interp_search_about_item = function - | SearchRef qid -> GlobSearchRef (Nametab.global qid) + | SearchSubPattern pat -> + let _,pat = Constrintern.intern_constr_pattern Evd.empty (Global.env()) pat in + GlobSearchSubPattern pat | SearchString (s,_) -> warning "Notation case not taken into account"; GlobSearchString s @@ -563,10 +565,10 @@ let pcoq_search s l = raw_search_about (filter_by_module_from_list l) add_search (List.map (on_snd interp_search_about_item) sl) | SearchPattern c -> - let _,pat = interp_constrpattern Evd.empty (Global.env()) c in + let _,pat = intern_constr_pattern Evd.empty (Global.env()) c in raw_pattern_search (filter_by_module_from_list l) add_search pat | SearchRewrite c -> - let _,pat = interp_constrpattern Evd.empty (Global.env()) c in + let _,pat = intern_constr_pattern Evd.empty (Global.env()) c in raw_search_rewrite (filter_by_module_from_list l) add_search pat; | SearchHead locqid -> filtered_search @@ -581,7 +583,7 @@ let rec hyp_pattern_filter pat name a c = | Prod(_, hyp, c2) -> (try (* let _ = msgnl ((str "WHOLE ") ++ (Printer.pr_lconstr c)) in - let _ = msgnl ((str "PAT ") ++ (Printer.pr_pattern pat)) in *) + let _ = msgnl ((str "PAT ") ++ (Printer.pr_constr_pattern pat)) in *) if Matching.is_matching pat hyp then (msgnl (str "ok"); true) else @@ -591,7 +593,7 @@ let rec hyp_pattern_filter pat name a c = | _ -> false;; let hyp_search_pattern c l = - let _, pat = interp_constrpattern Evd.empty (Global.env()) c in + let _, pat = intern_constr_pattern Evd.empty (Global.env()) c in ctv_SEARCH_LIST := []; gen_filtered_search (fun s a c -> (filter_by_module_from_list l s a c && @@ -640,8 +642,8 @@ let pcoq_term_pr = { * Except with right bool/env which I'll get :) *) pr_lconstr_expr = (fun c -> fFORMULA (xlate_formula c) ++ str "(pcoq_lconstr_expr of " ++ (default_term_pr.pr_lconstr_expr c) ++ str ")"); - pr_pattern_expr = (fun c -> str "pcoq_pattern_expr\n" ++ (default_term_pr.pr_pattern_expr c)); - pr_lpattern_expr = (fun c -> str "pcoq_constr_expr\n" ++ (default_term_pr.pr_lpattern_expr c)) + pr_constr_pattern_expr = (fun c -> str "pcoq_pattern_expr\n" ++ (default_term_pr.pr_constr_pattern_expr c)); + pr_lconstr_pattern_expr = (fun c -> str "pcoq_constr_expr\n" ++ (default_term_pr.pr_lconstr_pattern_expr c)) } let start_pcoq_trees () = diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml index 8096bc311..c2ab2dc8d 100644 --- a/contrib/interface/dad.ml +++ b/contrib/interface/dad.ml @@ -99,7 +99,7 @@ let rec find_cmd (l:(string * dad_rule) list) env constr p p1 p2 = with Failure s -> failwith "internal" in let _, constr_pat = - interp_constrpattern Evd.empty (Global.env()) + intern_constr_pattern Evd.empty (Global.env()) ((*ct_to_ast*) pat) in let subst = matches constr_pat term_to_match in if (is_prefix p_f (p_r@p1)) & (is_prefix p_l (p_r@p2)) then diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 02f36a8c8..ee48ee53b 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1958,12 +1958,14 @@ let rec xlate_vernac = let xlate_search_about_item (b,it) = if not b then xlate_error "TODO: negative searchabout constraint"; match it with - SearchRef x -> + SearchSubPattern (CRef x) -> CT_coerce_ID_to_ID_OR_STRING(loc_qualid_to_ct_ID x) | SearchString (s,None) -> CT_coerce_STRING_to_ID_OR_STRING(CT_string s) - | SearchString (s,_) -> - xlate_error "TODO: notation with explicit scope" in + | SearchString _ | SearchSubPattern _ -> + xlate_error + "TODO: search subpatterns or notation with explicit scope" + in CT_search_about (CT_id_or_string_ne_list(xlate_search_about_item a, List.map xlate_search_about_item l), diff --git a/contrib/omega/OmegaLemmas.v b/contrib/omega/OmegaLemmas.v index 1f46178d3..fe8fcc924 100644 --- a/contrib/omega/OmegaLemmas.v +++ b/contrib/omega/OmegaLemmas.v @@ -11,7 +11,46 @@ Require Import ZArith_base. Open Local Scope Z_scope. -(** These are specific variants of theorems dedicated for the Omega tactic *) +(** Factorization lemmas *) + +Theorem Zred_factor0 : forall n:Z, n = n * 1. + intro x; rewrite (Zmult_1_r x); reflexivity. +Qed. + +Theorem Zred_factor1 : forall n:Z, n + n = n * 2. +Proof. + exact Zplus_diag_eq_mult_2. +Qed. + +Theorem Zred_factor2 : forall n m:Z, n + n * m = n * (1 + m). +Proof. + intros x y; pattern x at 1 in |- *; rewrite <- (Zmult_1_r x); + rewrite <- Zmult_plus_distr_r; trivial with arith. +Qed. + +Theorem Zred_factor3 : forall n m:Z, n * m + n = n * (1 + m). +Proof. + intros x y; pattern x at 2 in |- *; rewrite <- (Zmult_1_r x); + rewrite <- Zmult_plus_distr_r; rewrite Zplus_comm; + trivial with arith. +Qed. + +Theorem Zred_factor4 : forall n m p:Z, n * m + n * p = n * (m + p). +Proof. + intros x y z; symmetry in |- *; apply Zmult_plus_distr_r. +Qed. + +Theorem Zred_factor5 : forall n m:Z, n * 0 + m = m. +Proof. + intros x y; rewrite <- Zmult_0_r_reverse; auto with arith. +Qed. + +Theorem Zred_factor6 : forall n:Z, n = n + 0. +Proof. + intro; rewrite Zplus_0_r; trivial with arith. +Qed. + +(** Other specific variants of theorems dedicated for the Omega tactic *) Lemma new_var : forall x : Z, exists y : Z, x = y. intros x; exists x; trivial with arith. diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 9488f1dea..cae948a00 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -18,6 +18,9 @@ Eauto.simplest_apply -> Hiddentac.h_simplest_apply Evarutil.define_evar_as_arrow -> define_evar_as_product Old version of Tactics.assert_tac disappears Tactics.true_cut renamed into Tactics.assert_tac +Constrintern.interp_constrpattern -> intern_constr_pattern +Hipattern.match_with_conjunction is a bit more restrictive +Hipattern.match_with_disjunction is a bit more restrictive ** Universe names (univ.mli) diff --git a/doc/common/macros.tex b/doc/common/macros.tex index be5980fe4..89b7350f3 100755 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -47,6 +47,7 @@ \newcommand{\Rem}{\medskip \noindent {\bf Remark: }} \newcommand{\Rems}{\medskip \noindent {\bf Remarks: }} \newcommand{\Example}{\medskip \noindent {\bf Example: }} +\newcommand{\Examples}{\medskip \noindent {\bf Examples: }} \newcommand{\Warning}{\medskip \noindent {\bf Warning: }} \newcommand{\Warns}{\medskip \noindent {\bf Warnings: }} \newcounter{ex} @@ -60,8 +61,6 @@ \newenvironment{ErrMsgs}{\ErrMsgx\begin{enumerate}}{\end{enumerate}} \newenvironment{Remarks}{\Rems\begin{enumerate}}{\end{enumerate}} \newenvironment{Warnings}{\Warns\begin{enumerate}}{\end{enumerate}} -\newenvironment{Examples}{\medskip\noindent{\bf Examples:} -\begin{enumerate}}{\end{enumerate}} %\newcommand{\bd}{\noindent\bf} %\newcommand{\sbd}{\vspace{8pt}\noindent\bf} @@ -191,11 +190,12 @@ \newcommand{\nestedpattern}{\nterm{nested\_pattern}} \newcommand{\name}{\nterm{name}} \newcommand{\num}{\nterm{num}} -\newcommand{\pattern}{\nterm{pattern}} +\newcommand{\pattern}{\nterm{pattern}} % pattern for pattern-matching \newcommand{\orpattern}{\nterm{or\_pattern}} \newcommand{\intropattern}{\nterm{intro\_pattern}} \newcommand{\disjconjintropattern}{\nterm{disj\_conj\_intro\_pattern}} \newcommand{\namingintropattern}{\nterm{naming\_intro\_pattern}} +\newcommand{\termpattern}{\nterm{term\_pattern}} % term with holes \newcommand{\pat}{\nterm{pat}} \newcommand{\pgs}{\nterm{pgms}} \newcommand{\pg}{\nterm{pgm}} diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 3f1e517d6..3168f7737 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -134,6 +134,8 @@ environment}\\ There is no constant in the environment named \qualid. \end{ErrMsgs} +\newcommand{\termpatternorstr}{{\termpattern}\textrm{\textsl{-}}{\str}} + \begin{Variants} \item {\tt SearchAbout {\str}.} @@ -151,30 +153,32 @@ The string {\str} must be a notation or the main symbol of a notation which is then interpreted in the scope bound to the delimiting key {\delimkey} (see Section~\ref{scopechange}). -\item {\tt SearchAbout [ \nelist{\zeroone{-}\textrm{\textsl{qualid-or-string}}}{} -].}\\ -\noindent where {\textrm{\textsl{qualid-or-string}}} is a {\qualid} or -a {\str}, or a {\str} followed by a scope delimiting key -{\tt \%{\delimkey}}. +\item {\tt SearchAbout {\termpattern}.} -This generalization of {\tt SearchAbout} searches for all objects -whose statement mentions all of {\qualid} (or {\str} if {\str} is the -notation for a reference) and whose name contains all {\str} that -correspond to valid identifiers. If a {\qualid} or a {\str} is -prefixed by ``-'', the search excludes the objects that mention that -{\qualid} or that {\str}. +This searches for all statements or types of definition that contains +a subterm that matches the pattern {\termpattern} (holes of the +pattern are either denoted by ``{\texttt \_}'' or +by ``{\texttt ?{\ident}}'' when non linear patterns are expected). -\Example +\item {\tt SearchAbout [ \nelist{\zeroone{-}{\termpatternorstr}}{} +].}\\ -\begin{coq_example} -Require Import ZArith. -SearchAbout [ Zmult Zplus "distr" ]. -\end{coq_example} +\noindent where {\termpatternorstr} is a +{\termpattern} or a {\str}, or a {\str} followed by a scope +delimiting key {\tt \%{\delimkey}}. + +This generalization of {\tt SearchAbout} searches for all objects +whose statement or type contains a subterm matching {\termpattern} (or +{\qualid} if {\str} is the notation for a reference {\qualid}) and +whose name contains all {\str} of the request that correspond to valid +identifiers. If a {\termpattern} or a {\str} is prefixed by ``-'', the +search excludes the objects that mention that {\termpattern} or that +{\str}. \item \begin{tabular}[t]{@{}l} - {\tt SearchAbout {\term} inside {\module$_1$} \ldots{} {\module$_n$}.} \\ - {\tt SearchAbout [ \nelist{\textrm{\textsl{qualid-or-string}}}{} ] + {\tt SearchAbout {\termpatternorstr} inside {\module$_1$} \ldots{} {\module$_n$}.} \\ + {\tt SearchAbout [ \nelist{{\termpatternorstr}}{} ] inside {\module$_1$} \ldots{} {\module$_n$}.} \end{tabular} @@ -183,8 +187,8 @@ This restricts the search to constructions defined in modules \item \begin{tabular}[t]{@{}l} - {\tt SearchAbout {\term} outside {\module$_1$}...{\module$_n$}.} \\ - {\tt SearchAbout [ \nelist{\textrm{\textsl{qualid-or-string}}}{} ] + {\tt SearchAbout {\termpatternorstr} outside {\module$_1$}...{\module$_n$}.} \\ + {\tt SearchAbout [ \nelist{{\termpatternorstr}}{} ] outside {\module$_1$}...{\module$_n$}.} \end{tabular} @@ -193,11 +197,25 @@ This restricts the search to constructions not defined in modules \end{Variants} -\subsection[\tt SearchPattern {\term}.]{\tt SearchPattern {\term}.\comindex{SearchPattern}} +\Examples + +\begin{coq_example*} +Require Import ZArith. +\end{coq_example*} +\begin{coq_example} +SearchAbout [ Zmult Zplus "distr" ]. +SearchAbout [ "+"%Z "*"%Z "distr" -positive -Prop]. +SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas. +\end{coq_example} + +\subsection[\tt SearchPattern {\termpattern}.]{\tt SearchPattern {\term}.\comindex{SearchPattern}} This command displays the name and type of all theorems of the current context whose statement's conclusion matches the expression {\term} -where holes in the latter are denoted by ``{\texttt \_}''. +where holes in the latter are denoted by ``{\texttt \_}''. It is a +variant of {\tt SearchAbout {\termpattern}} that does not look for +subterms but searches for statements whose conclusion has exactly the +expected form. \begin{coq_example} Require Import Arith. @@ -215,13 +233,12 @@ SearchPattern (?X1 + _ = _ + ?X1). \begin{Variants} \item {\tt SearchPattern {\term} inside -{\module$_1$} \ldots{} {\module$_n$}.}\comindex{SearchPattern \ldots{} inside -\ldots{}} +{\module$_1$} \ldots{} {\module$_n$}.} This restricts the search to constructions defined in modules {\module$_1$} \ldots{} {\module$_n$}. -\item {\tt SearchPattern {\term} outside {\module$_1$} \ldots{} {\module$_n$}.}\comindex{SearchPattern \ldots{} outside \ldots{}} +\item {\tt SearchPattern {\term} outside {\module$_1$} \ldots{} {\module$_n$}.} This restricts the search to constructions not defined in modules {\module$_1$} \ldots{} {\module$_n$}. @@ -232,7 +249,7 @@ This restricts the search to constructions not defined in modules This command displays the name and type of all theorems of the current context whose statement's conclusion is an equality of which one side matches -the expression {\term =}. Holes in {\term} are denoted by ``{\texttt \_}''. +the expression {\term}. Holes in {\term} are denoted by ``{\texttt \_}''. \begin{coq_example} Require Import Arith. diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 07d9df9c5..f5568455f 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1269,9 +1269,9 @@ $\beta\iota\zeta$-reduction rules. \tacindex{hnf}} This tactic applies to any goal. It replaces the current goal with its -head normal form according to the $\beta\delta\iota\zeta$-reduction rules. -{\tt hnf} does not produce a real head normal form but either a -product or an applicative term in head normal form or a variable. +head normal form according to the $\beta\delta\iota\zeta$-reduction +rules, i.e. it reduces the head of the goal until it becomes a +product or an irreducible term. \Example The term \verb+forall n:nat, (plus (S n) (S n))+ is not reduced by {\tt hnf}. diff --git a/interp/constrintern.ml b/interp/constrintern.ml index a8dad2216..357ce4377 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1277,8 +1277,9 @@ let interp_constr_judgment_evars evdref env c = type ltac_sign = identifier list * unbound_ltac_var_map -let interp_constrpattern sigma env c = - pattern_of_rawconstr (intern_gen false sigma env ~allow_patvar:true c) +let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=([],[])) c = + let c = intern_gen as_type ~allow_patvar:true ~ltacvars sigma env c in + pattern_of_rawconstr c let interp_aconstr impls (vars,varslist) a = let env = Global.env () in diff --git a/interp/constrintern.mli b/interp/constrintern.mli index a646b6314..6410c9b2e 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -113,8 +113,9 @@ val interp_constr_judgment : evar_map -> env -> constr_expr -> unsafe_judgment (* Interprets constr patterns *) -val interp_constrpattern : - evar_map -> env -> constr_expr -> patvar list * constr_pattern +val intern_constr_pattern : + evar_map -> env -> ?as_type:bool -> ?ltacvars:ltac_sign -> + constr_pattern_expr -> patvar list * constr_pattern val interp_reference : ltac_sign -> reference -> rawconstr diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 2cbe53981..6bee22f6c 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -675,6 +675,8 @@ and recursion_order_expr = | CWfRec of constr_expr | CMeasureRec of constr_expr +type constr_pattern_expr = constr_expr + (***********************) (* For binders parsing *) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 2d293eacb..cecea239c 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -172,6 +172,8 @@ type typeclass_constraint = name located * binding_kind * constr_expr and typeclass_context = typeclass_constraint list +type constr_pattern_expr = constr_expr + (**********************************************************************) (* Utilities on constr_expr *) diff --git a/library/libobject.ml b/library/libobject.ml index 684607b4b..90636dbee 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -148,8 +148,9 @@ let apply_dyn_fun deflt f lobj = if !relax_flag then failwith "local to_apply_dyn_fun" else - anomaly - ("Cannot find library functions for an object with tag "^tag) in + error + ("Cannot find library functions for an object with tag "^tag^ + " (maybe a plugin is missing)") in f dodecl with Failure "local to_apply_dyn_fun" -> deflt;; diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 48a7a7a5a..bcb2f7a57 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -615,11 +615,12 @@ GEXTEND Gram | IDENT "SearchAbout"; sl = [ "["; l = LIST1 [ - b = positive_search_mark; r = global -> b,SearchRef r - | b = positive_search_mark; s = ne_string; sc = OPT scope - -> b,SearchString (s,sc) + b = positive_search_mark; s = ne_string; sc = OPT scope + -> b, SearchString (s,sc) + | b = positive_search_mark; p = constr_pattern + -> b, SearchSubPattern p ]; "]" -> l - | qid = global -> [true,SearchRef qid] + | p = constr_pattern -> [true,SearchSubPattern p] | s = ne_string; sc = OPT scope -> [true,SearchString (s,sc)] ]; l = in_or_out_modules -> VernacSearch (SearchAbout sl, l) diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index f5fe151ed..e16641a83 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -666,15 +666,15 @@ let rec strip_context n iscast t = type term_pr = { pr_constr_expr : constr_expr -> std_ppcmds; pr_lconstr_expr : constr_expr -> std_ppcmds; - pr_pattern_expr : Tacexpr.pattern_expr -> std_ppcmds; - pr_lpattern_expr : Tacexpr.pattern_expr -> std_ppcmds + pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds; + pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds } let default_term_pr = { pr_constr_expr = pr lsimple; pr_lconstr_expr = pr ltop; - pr_pattern_expr = pr lsimple; - pr_lpattern_expr = pr ltop + pr_constr_pattern_expr = pr lsimple; + pr_lconstr_pattern_expr = pr ltop } let term_pr = ref default_term_pr @@ -683,8 +683,8 @@ let set_term_pr = (:=) term_pr let pr_constr_expr c = !term_pr.pr_constr_expr c let pr_lconstr_expr c = !term_pr.pr_lconstr_expr c -let pr_pattern_expr c = !term_pr.pr_pattern_expr c -let pr_lpattern_expr c = !term_pr.pr_lpattern_expr c +let pr_constr_pattern_expr c = !term_pr.pr_constr_pattern_expr c +let pr_lconstr_pattern_expr c = !term_pr.pr_lconstr_pattern_expr c let pr_cases_pattern_expr = pr_patt ltop diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli index b9bf933eb..d7fdd1ed9 100644 --- a/parsing/ppconstr.mli +++ b/parsing/ppconstr.mli @@ -66,8 +66,8 @@ val pr_may_eval : val pr_rawsort : rawsort -> std_ppcmds val pr_binders : local_binder list -> std_ppcmds -val pr_pattern_expr : Tacexpr.pattern_expr -> std_ppcmds -val pr_lpattern_expr : Tacexpr.pattern_expr -> std_ppcmds +val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds +val pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds val pr_constr_expr : constr_expr -> std_ppcmds val pr_lconstr_expr : constr_expr -> std_ppcmds val pr_cases_pattern_expr : cases_pattern_expr -> std_ppcmds @@ -75,8 +75,8 @@ val pr_cases_pattern_expr : cases_pattern_expr -> std_ppcmds type term_pr = { pr_constr_expr : constr_expr -> std_ppcmds; pr_lconstr_expr : constr_expr -> std_ppcmds; - pr_pattern_expr : Tacexpr.pattern_expr -> std_ppcmds; - pr_lpattern_expr : Tacexpr.pattern_expr -> std_ppcmds + pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds; + pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds } val set_term_pr : term_pr -> unit diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 7cb93d108..2f102488f 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -1024,7 +1024,7 @@ let rec raw_printers = (pr_raw_tactic_level, drop_env pr_constr_expr, drop_env pr_lconstr_expr, - pr_lpattern_expr, + pr_lconstr_pattern_expr, drop_env (pr_or_by_notation pr_reference), drop_env (pr_or_by_notation pr_reference), pr_reference, diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index a3eed62b7..df4eee8aa 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -136,7 +136,7 @@ let pr_in_out_modules = function let pr_search_about (b,c) = (if b then str "-" else mt()) ++ match c with - | SearchRef r -> pr_reference r + | SearchSubPattern p -> pr_constr_pattern_expr p | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc let pr_search a b pr_p = match a with @@ -819,7 +819,7 @@ let rec pr_vernac = function | VernacCreateHintDb (local,dbname,b) -> hov 1 (str "Create " ++ pr_locality local ++ str "HintDb " ++ str dbname ++ (if b then str" discriminated" else mt ())) | VernacHints (local,dbnames,h) -> - pr_hints local dbnames h pr_constr pr_pattern_expr + pr_hints local dbnames h pr_constr pr_constr_pattern_expr | VernacSyntacticDefinition (id,(ids,c),local,onlyparsing) -> hov 2 (str"Notation " ++ pr_locality local ++ pr_lident id ++ @@ -912,7 +912,7 @@ let rec pr_vernac = function term *) | PrintAssumptions qid -> str"Print Assumptions"++spc()++pr_reference qid in pr_printable p - | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_pattern_expr + | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_constr_pattern_expr | VernacLocate loc -> let pr_locate =function | LocateTerm qid -> pr_reference qid diff --git a/parsing/printer.ml b/parsing/printer.ml index bfb571b23..e2150fcbf 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -89,14 +89,14 @@ let pr_cases_pattern t = pr_cases_pattern_expr (extern_cases_pattern Idset.empty t) let pr_lconstr_pattern_env env c = - pr_lconstr_expr (extern_constr_pattern (names_of_rel_context env) c) + pr_lconstr_pattern_expr (extern_constr_pattern (names_of_rel_context env) c) let pr_constr_pattern_env env c = - pr_constr_expr (extern_constr_pattern (names_of_rel_context env) c) + pr_constr_pattern_expr (extern_constr_pattern (names_of_rel_context env) c) let pr_lconstr_pattern t = - pr_lconstr_expr (extern_constr_pattern empty_names_context t) + pr_lconstr_pattern_expr (extern_constr_pattern empty_names_context t) let pr_constr_pattern t = - pr_constr_expr (extern_constr_pattern empty_names_context t) + pr_constr_pattern_expr (extern_constr_pattern empty_names_context t) let pr_sort s = pr_rawsort (extern_sort s) diff --git a/parsing/search.ml b/parsing/search.ml index 49682ee48..94270ee13 100644 --- a/parsing/search.ml +++ b/parsing/search.ml @@ -165,15 +165,6 @@ let raw_search_rewrite extra_filter display_function pattern = (pattern_filter (mk_rewrite_pattern2 gref_eq pattern) s a c)) && extra_filter s a c) display_function gref_eq -(* - ; - filtered_search - (fun s a c -> - ((pattern_filter (mk_rewrite_pattern1 gref_eqT pattern) s a c) || - (pattern_filter (mk_rewrite_pattern2 gref_eqT pattern) s a c)) - && extra_filter s a c) - display_function gref_eqT -*) let text_pattern_search extra_filter = raw_pattern_search extra_filter plain_display @@ -204,11 +195,11 @@ let gen_filtered_search filter_function display_function = let name_of_reference ref = string_of_id (id_of_global ref) type glob_search_about_item = - | GlobSearchRef of global_reference + | GlobSearchSubPattern of constr_pattern | GlobSearchString of string let search_about_item (itemref,typ) = function - | GlobSearchRef ref -> Termops.occur_term (constr_of_global ref) typ + | GlobSearchSubPattern pat -> is_matching_appsubterm ~closed:false pat typ | GlobSearchString s -> string_string_contains (name_of_reference itemref) s let raw_search_about filter_modules display_function l = diff --git a/parsing/search.mli b/parsing/search.mli index 356c5b469..fc2ea925f 100644 --- a/parsing/search.mli +++ b/parsing/search.mli @@ -19,7 +19,7 @@ open Nametab (*s Search facilities. *) type glob_search_about_item = - | GlobSearchRef of global_reference + | GlobSearchSubPattern of constr_pattern | GlobSearchString of string val search_by_head : global_reference -> dir_path list * bool -> unit diff --git a/pretyping/matching.ml b/pretyping/matching.ml index 091aa0b8b..870db85ee 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -217,36 +217,37 @@ let pmatches c p = snd (matches_core None true c p) let special_meta = (-1) (* Tells if it is an authorized occurrence and if the instance is closed *) -let authorized_occ pat c mk_ctx next = +let authorized_occ closed pat c mk_ctx next = try let sigma = extended_matches pat c in - if not (List.for_all (fun (_,c) -> closed0 c) (snd sigma)) then next () + if closed && not (List.for_all (fun (_,c) -> closed0 c) (snd sigma)) + then next () else sigma, mk_ctx (mkMeta special_meta), next with PatternMatchingFailure -> next () (* Tries to match a subterm of [c] with [pat] *) -let rec sub_match ?(partial_app=false) pat c = +let sub_match ?(partial_app=false) ?(closed=true) pat c = let rec aux c mk_ctx next = match kind_of_term c with | Cast (c1,k,c2) -> - authorized_occ pat c mk_ctx (fun () -> + authorized_occ closed pat c mk_ctx (fun () -> let mk_ctx lc = mk_ctx (mkCast (List.hd lc, k,c2)) in try_aux [c1] mk_ctx next) | Lambda (x,c1,c2) -> - authorized_occ pat c mk_ctx (fun () -> + authorized_occ closed pat c mk_ctx (fun () -> let mk_ctx lc = mk_ctx (mkLambda (x,List.hd lc,List.nth lc 1)) in try_aux [c1;c2] mk_ctx next) | Prod (x,c1,c2) -> - authorized_occ pat c mk_ctx (fun () -> + authorized_occ closed pat c mk_ctx (fun () -> let mk_ctx lc = mk_ctx (mkProd (x,List.hd lc,List.nth lc 1)) in try_aux [c1;c2] mk_ctx next) | LetIn (x,c1,t,c2) -> - authorized_occ pat c mk_ctx (fun () -> + authorized_occ closed pat c mk_ctx (fun () -> let mk_ctx = function [c1;c2] -> mkLetIn (x,c1,t,c2) | _ -> assert false in try_aux [c1;c2] mk_ctx next) | App (c1,lc) -> - authorized_occ pat c mk_ctx (fun () -> + authorized_occ closed pat c mk_ctx (fun () -> let topdown = true in if partial_app then if topdown then @@ -274,13 +275,13 @@ let rec sub_match ?(partial_app=false) pat c = mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in try_aux (c1::Array.to_list lc) mk_ctx next) | Case (ci,hd,c1,lc) -> - authorized_occ pat c mk_ctx (fun () -> + authorized_occ closed pat c mk_ctx (fun () -> let mk_ctx le = mk_ctx (mkCase (ci,hd,List.hd le,Array.of_list (List.tl le))) in try_aux (c1::Array.to_list lc) mk_ctx next) | Construct _ | Fix _ | Ind _|CoFix _ |Evar _|Const _ | Rel _|Meta _|Var _|Sort _ -> - authorized_occ pat c mk_ctx next + authorized_occ closed pat c mk_ctx next (* Tries [sub_match] for all terms in the list *) and try_aux lc mk_ctx next = @@ -302,8 +303,12 @@ let match_appsubterm pat c = sub_match ~partial_app:true pat c let match_subterm_gen app pat c = sub_match ~partial_app:app pat c -let is_matching pat n = - try let _ = matches pat n in true +let is_matching pat c = + try let _ = matches pat c in true + with PatternMatchingFailure -> false + +let is_matching_appsubterm ?(closed=true) pat c = + try let _ = sub_match ~partial_app:true ~closed pat c in true with PatternMatchingFailure -> false let matches_conv env sigma c p = diff --git a/pretyping/matching.mli b/pretyping/matching.mli index 574a4bbd2..4b3bc6c05 100644 --- a/pretyping/matching.mli +++ b/pretyping/matching.mli @@ -69,6 +69,10 @@ val match_appsubterm : constr_pattern -> constr -> subterm_matching_result val match_subterm_gen : bool (* true = with app context *) -> constr_pattern -> constr -> subterm_matching_result +(* [is_matching_appsubterm pat c] tells if a subterm of [c] matches + against [pat] taking partial subterms into consideration *) +val is_matching_appsubterm : ?closed:bool -> constr_pattern -> constr -> bool + (* [is_matching_conv env sigma pat c] tells if [c] matches against [pat] up to conversion for constants in patterns *) val is_matching_conv : diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index 3f66ddcbc..2413e73ec 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -127,8 +127,6 @@ type multi = | RepeatStar | RepeatPlus -type pattern_expr = constr_expr - (* Type of patterns *) type 'a match_pattern = | Term of 'a @@ -283,7 +281,7 @@ and glob_tactic_expr = type raw_tactic_expr = (constr_expr, - pattern_expr, + constr_pattern_expr, reference or_by_notation, reference or_by_notation, reference, @@ -292,7 +290,7 @@ type raw_tactic_expr = type raw_atomic_tactic_expr = (constr_expr, (* constr *) - pattern_expr, (* pattern *) + constr_pattern_expr, (* pattern *) reference or_by_notation, (* evaluable reference *) reference or_by_notation, (* inductive *) reference, (* ltac reference *) @@ -301,7 +299,7 @@ type raw_atomic_tactic_expr = type raw_tactic_arg = (constr_expr, - pattern_expr, + constr_pattern_expr, reference or_by_notation, reference or_by_notation, reference, diff --git a/tactics/auto.ml b/tactics/auto.ml index 0dd90246d..ec3a8d6c9 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -581,7 +581,7 @@ let add_hints local dbnames0 h = add_resolves env sigma lcons local dbnames in List.iter add_one lqid | HintsExtern (pri, patcom, tacexp) -> - let pat = Option.map (Constrintern.interp_constrpattern Evd.empty (Global.env())) patcom in + let pat = Option.map (Constrintern.intern_constr_pattern Evd.empty (Global.env())) patcom in let tacexp = !forward_intern_tac (match pat with None -> [] | Some (l, _) -> l) tacexp in add_externs pri pat tacexp local dbnames | HintsDestruct(na,pri,loc,pat,code) -> diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index 6622ccb60..b7929b29a 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -249,7 +249,7 @@ let add_destructor_hint local na loc pat pri code = errorlabstrm "add_destructor_hint" (str "The tactic should be a function of the hypothesis name.") end in - let (_,pat) = Constrintern.interp_constrpattern Evd.empty (Global.env()) pat + let (_,pat) = Constrintern.intern_constr_pattern Evd.empty (Global.env()) pat in let pat = match loc with | HypLocation b -> diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index bf0534167..568b6ea42 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -615,18 +615,15 @@ let intern_inversion_strength lf ist = function let intern_hyp_location ist (((b,occs),id),hl) = (((b,List.map (intern_or_var ist) occs),intern_hyp_or_metaid ist id), hl) -let interp_constrpattern_gen sigma env ?(as_type=false) ltacvar c = - let c = intern_gen as_type ~allow_patvar:true ~ltacvars:(ltacvar,[]) - sigma env c in - pattern_of_rawconstr c - (* Reads a pattern *) let intern_pattern sigma env ?(as_type=false) lfun = function | Subterm (b,ido,pc) -> - let (metas,pat) = interp_constrpattern_gen sigma env lfun pc in + let ltacvars = (lfun,[]) in + let (metas,pat) = intern_constr_pattern sigma env ~ltacvars pc in ido, metas, Subterm (b,ido,pat) | Term pc -> - let (metas,pat) = interp_constrpattern_gen sigma env ~as_type lfun pc in + let ltacvars = (lfun,[]) in + let (metas,pat) = intern_constr_pattern sigma env ~as_type ~ltacvars pc in None, metas, Term pat let intern_constr_may_eval ist = function diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c43f829fd..44f07d37b 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1129,12 +1129,29 @@ let intro_or_and_pattern loc b ll l' tac = nv (Array.of_list ll)) gl) -let clear_if_atomic l2r id gl = - let eq = pf_type_of gl (mkVar id) in - let (_,lhs,rhs) = snd (find_eq_data_decompose eq) in - if l2r & isVar lhs then tclTRY (clear [destVar lhs;id]) gl - else if not l2r & isVar rhs then tclTRY (clear [destVar rhs;id]) gl - else tclIDTAC gl +let rewrite_hyp l2r id gl = + let rew_on l2r = + !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) in + let clear_var_and_eq c = + tclTRY (tclTHEN (clear [id]) (tclTRY (clear [destVar c]))) in + let t = pf_whd_betadeltaiota gl (pf_type_of gl (mkVar id)) in + (* TODO: detect setoid equality? better detect the different equalities *) + match match_with_equality_type t with + | Some (hdcncl,[_;lhs;rhs]) -> + if l2r & isVar lhs & not (occur_var (pf_env gl) (destVar lhs) rhs) then + tclTHEN (rew_on l2r allClauses) (clear_var_and_eq lhs) gl + else if not l2r & isVar rhs & not (occur_var (pf_env gl) (destVar rhs) lhs) then + tclTHEN (rew_on l2r allClauses) (clear_var_and_eq rhs) gl + else + tclTHEN (rew_on l2r onConcl) (tclTRY (clear [id])) gl + | Some (hdcncl,[c]) -> + let l2r = not l2r in (* equality of the form eq_true *) + if isVar c then + tclTHEN (rew_on l2r allClauses) (clear_var_and_eq c) gl + else + tclTHEN (rew_on l2r onConcl) (tclTRY (clear [id])) gl + | _ -> + error "Cannot find a known equation." let rec explicit_intro_names = function | (_, IntroIdentifier id) :: l -> @@ -1181,11 +1198,9 @@ let rec intros_patterns b avoid thin destopt = function tclTHEN (intro_gen loc (IntroAvoid(avoid@explicit_intro_names l)) no_move true) (onLastHyp (fun id -> - tclTHENLIST [ - !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) - allClauses; - clear_if_atomic l2r id; - intros_patterns b avoid thin destopt l ])) + tclTHEN + (rewrite_hyp l2r id) + (intros_patterns b avoid thin destopt l))) | [] -> clear_wildcards thin let intros_pattern = intros_patterns false [] [] diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 3d85f6560..1c75059b8 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -234,13 +234,18 @@ let rec tauto_intuit t_reduce solver ist = || $t_solver ) >> - + + (* The unfolding of "iff" below is a priori too strong since it + reduces all occurrences in subterms even if not necessary to do + so. However we cannot renounce to them (even with iff dealt with + in "simplif") w/o breaking some intro naming. This is because, a + "and" or an "iff" can arrive in the scope of an inductive type, + say "{x:A|P x}" and "case"ing on a such an hypothesis will name P + x "a" or "i" depending on whether "P" is an "and" or a "iff". + (idem for "not" if "simplif" has a primitive treatment *) + let reduction_not _ist = - <:tactic<repeat - match goal with - | |- _ => progress unfold Coq.Init.Logic.not - | H:_ |- _ => progress unfold Coq.Init.Logic.not in H - end >> + <:tactic< unfold Coq.Init.Logic.not, Coq.Init.Logic.iff in * >> let t_reduction_not = tacticIn reduction_not diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v index 18b49f4bb..5edf68013 100644 --- a/theories/ZArith/auxiliary.v +++ b/theories/ZArith/auxiliary.v @@ -91,46 +91,6 @@ Proof. rewrite Zplus_opp_r; trivial. Qed. -(**********************************************************************) -(** * Factorization lemmas *) - -Theorem Zred_factor0 : forall n:Z, n = n * 1. - intro x; rewrite (Zmult_1_r x); reflexivity. -Qed. - -Theorem Zred_factor1 : forall n:Z, n + n = n * 2. -Proof. - exact Zplus_diag_eq_mult_2. -Qed. - -Theorem Zred_factor2 : forall n m:Z, n + n * m = n * (1 + m). -Proof. - intros x y; pattern x at 1 in |- *; rewrite <- (Zmult_1_r x); - rewrite <- Zmult_plus_distr_r; trivial with arith. -Qed. - -Theorem Zred_factor3 : forall n m:Z, n * m + n = n * (1 + m). -Proof. - intros x y; pattern x at 2 in |- *; rewrite <- (Zmult_1_r x); - rewrite <- Zmult_plus_distr_r; rewrite Zplus_comm; - trivial with arith. -Qed. - -Theorem Zred_factor4 : forall n m p:Z, n * m + n * p = n * (m + p). -Proof. - intros x y z; symmetry in |- *; apply Zmult_plus_distr_r. -Qed. - -Theorem Zred_factor5 : forall n m:Z, n * 0 + m = m. -Proof. - intros x y; rewrite <- Zmult_0_r_reverse; auto with arith. -Qed. - -Theorem Zred_factor6 : forall n:Z, n = n + 0. -Proof. - intro; rewrite Zplus_0_r; trivial with arith. -Qed. - Theorem Zle_mult_approx : forall n m p:Z, n > 0 -> p > 0 -> 0 <= m -> 0 <= m * n + p. Proof. diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 42a06308c..465c55a4b 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1123,14 +1123,17 @@ open Search let is_ident s = try ignore (check_ident s); true with UserError _ -> false let interp_search_about_item = function - | SearchRef r -> GlobSearchRef (global_with_alias r) - | SearchString (s,None) when is_ident s -> GlobSearchString s + | SearchSubPattern pat -> + let _,pat = intern_constr_pattern Evd.empty (Global.env()) pat in + GlobSearchSubPattern pat + | SearchString (s,None) when is_ident s -> + GlobSearchString s | SearchString (s,sc) -> try let ref = Notation.interp_notation_as_global_reference dummy_loc (fun _ -> true) s sc in - GlobSearchRef ref + GlobSearchSubPattern (Pattern.PRef ref) with UserError _ -> error ("Unable to interp \""^s^"\" either as a reference or as an identifier component") @@ -1140,10 +1143,10 @@ let vernac_search s r = if !pcoq <> None then (Option.get !pcoq).search s r else match s with | SearchPattern c -> - let _,pat = interp_constrpattern Evd.empty (Global.env()) c in + let _,pat = intern_constr_pattern Evd.empty (Global.env()) c in Search.search_pattern pat r | SearchRewrite c -> - let _,pat = interp_constrpattern Evd.empty (Global.env()) c in + let _,pat = intern_constr_pattern Evd.empty (Global.env()) c in Search.search_rewrite pat r | SearchHead ref -> Search.search_by_head (global_with_alias ref) r diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index d8084c966..e7a66203c 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -69,12 +69,12 @@ type printable = | PrintAssumptions of reference type search_about_item = - | SearchRef of reference + | SearchSubPattern of constr_pattern_expr | SearchString of string * scope_name option type searchable = - | SearchPattern of pattern_expr - | SearchRewrite of pattern_expr + | SearchPattern of constr_pattern_expr + | SearchRewrite of constr_pattern_expr | SearchHead of reference | SearchAbout of (bool * search_about_item) list |