aboutsummaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/interface/centaur.ml416
-rw-r--r--contrib/interface/dad.ml2
-rw-r--r--contrib/interface/xlate.ml8
-rw-r--r--contrib/omega/OmegaLemmas.v41
4 files changed, 55 insertions, 12 deletions
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index e7c7fde8dd..51dce4f766 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 8096bc3111..c2ab2dc8d0 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 02f36a8c88..ee48ee53b7 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 1f46178d36..fe8fcc9249 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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 16:09:20 +0000