aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/base_include3
-rw-r--r--dev/top_printers.ml4
-rw-r--r--parsing/printer.ml16
-rw-r--r--parsing/printer.mli7
-rw-r--r--tactics/auto.ml25
-rw-r--r--tactics/class_tactics.ml42
-rw-r--r--tactics/eauto.ml417
-rw-r--r--theories/Classes/Morphisms.v20
-rw-r--r--theories/Ints/num/GenMul.v10
-rw-r--r--theories/Sets/Powerset_Classical_facts.v1
10 files changed, 88 insertions, 17 deletions
diff --git a/dev/base_include b/dev/base_include
index d3301c88b..255e28a66 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -32,6 +32,9 @@
#install_printer (* constr *) print_pure_constr;;
#install_printer (* patch *) ppripos;;
#install_printer (* values *) ppvalues;;
+#install_printer (* Idpred.t *) pp_idpred;;
+#install_printer (* Cpred.t *) pp_cpred;;
+#install_printer (* transparent_state *) pp_transparent_state;;
#install_printer ppzipper;;
#install_printer ppstack;;
#install_printer ppatom;;
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index c67307d36..a63c6c2dd 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -93,6 +93,10 @@ let ppj j = pp (genppj pr_ljudge j)
let prsubst s = pp (Mod_subst.debug_pr_subst s)
+let pp_idpred s = pp (pr_idpred s)
+let pp_cpred s = pp (pr_cpred s)
+let pp_transparent_state s = pp (pr_transparent_state s)
+
(* proof printers *)
let ppmetas metas = pp(pr_metaset metas)
let ppevm evd = pp(pr_evar_map evd)
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 3e13e1392..521dad6a0 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -244,6 +244,22 @@ let pr_restricted_named_context among env =
pps)
env ~init:(mt ()))
+
+let pr_predicate pr_elt (b, elts) =
+ let pr_elts = prlist_with_sep spc pr_elt elts in
+ if b then
+ str"all" ++
+ (if elts = [] then mt () else str" except: " ++ pr_elts)
+ else
+ if elts = [] then str"none" else pr_elts
+
+let pr_cpred p = pr_predicate pr_con (Cpred.elements p)
+let pr_idpred p = pr_predicate Nameops.pr_id (Idpred.elements p)
+
+let pr_transparent_state (ids, csts) =
+ hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++
+ str"CONSTANTS: " ++ pr_cpred csts ++ fnl ())
+
let pr_subgoal_metas metas env=
let pr_one (meta,typ) =
str "?" ++ int meta ++ str " : " ++
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 0e25f1bd0..338bff3b3 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -91,6 +91,13 @@ val pr_rel_context : env -> rel_context -> std_ppcmds
val pr_rel_context_of : env -> std_ppcmds
val pr_context_of : env -> std_ppcmds
+(* Predicates *)
+
+val pr_predicate : ('a -> std_ppcmds) -> (bool * 'a list) -> std_ppcmds
+val pr_cpred : Cpred.t -> std_ppcmds
+val pr_idpred : Idpred.t -> std_ppcmds
+val pr_transparent_state : transparent_state -> std_ppcmds
+
(* Proofs *)
val pr_goal : goal -> std_ppcmds
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 2709502c6..66fde8f6b 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -543,7 +543,10 @@ let print_applicable_hint () =
print_hint_term (pf_concl gl)
(* displays the whole hint database db *)
-let print_hint_db db =
+let print_hint_db ((ids, csts),db) =
+ msg (hov 0
+ (str"Unfoldable variable definitions: " ++ pr_idpred ids ++ fnl () ++
+ str"Unfoldable constant definitions: " ++ pr_cpred csts ++ fnl ()));
Hint_db.iter
(fun head hintlist ->
msg (hov 0
@@ -553,14 +556,14 @@ let print_hint_db db =
let print_hint_db_by_name dbname =
try
- let db = snd (searchtable_map dbname) in print_hint_db db
+ let db = searchtable_map dbname in print_hint_db db
with Not_found ->
error (dbname^" : No such Hint database")
(* displays all the hints of all databases *)
let print_searchtable () =
Hintdbmap.iter
- (fun name (_, db) ->
+ (fun name db ->
msg (str "In the database " ++ str name ++ fnl ());
print_hint_db db)
!searchtable
@@ -591,7 +594,7 @@ let auto_unif_flags = {
let unify_resolve st (c,clenv) gls =
let clenv' = connect_clenv gls clenv in
let _ = clenv_unique_resolver false ~flags:{auto_unif_flags with modulo_delta = st} clenv' gls in
- h_simplest_apply c gls
+ h_apply true false (c,NoBindings) gls
(* builds a hint database from a constr signature *)
(* typically used with (lid, ltyp) = pf_hyps_types <some goal> *)
@@ -633,6 +636,9 @@ let conclPattern concl pat tac gl =
(* Papageno : cette fonction a été pas mal simplifiée depuis que la base
de Hint impérative a été remplacée par plusieurs bases fonctionnelles *)
+let transparent_state_union (xids, xcsts) (yids, ycsts) =
+ (Idpred.union xids yids, Cpred.union xcsts ycsts)
+
let rec trivial_fail_db db_list local_db gl =
let intro_tac =
tclTHEN intro
@@ -649,11 +655,16 @@ and my_find_search db_list local_db hdc concl =
let tacl =
if occur_existential concl then
list_map_append
- (fun (st, db) -> List.map (fun x -> (st,x)) (Hint_db.map_all hdc db))
+ (fun (st, db) ->
+ List.map (fun x -> (st,x)) (Hint_db.map_all hdc db))
(local_db::db_list)
else
- list_map_append (fun (st, db) ->
- List.map (fun x -> (st,x)) (Hint_db.map_auto (hdc,concl) db))
+ list_map_append (fun ((ids, csts as st), db) ->
+ let l =
+(* if Idpred.is_empty ids && Cpred.is_empty csts *)
+(* then *)Hint_db.map_auto (hdc,concl) db
+(* else Hint_db.map_all hdc db *)
+ in List.map (fun x -> (st,x)) l)
(local_db::db_list)
in
List.map
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index b79c24df2..d6de5e69d 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -414,7 +414,7 @@ let resolve_all_evars debug m env p oevd =
VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings
| [ "Typeclasses" "unfold" reference_list(cl) ] -> [
- add_hints true ["typeclass_instances"] (Vernacexpr.HintsUnfold cl)
+ add_hints false ["typeclass_instances"] (Vernacexpr.HintsUnfold cl)
]
END
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 0facf2393..03b29d523 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -384,3 +384,20 @@ TACTIC EXTEND dfs_eauto
hintbases(db) ] ->
[ gen_eauto false (true, make_depth p) lems db ]
END
+
+let autosimpl db cl =
+ let unfold_of_elts constr (b, elts) =
+ if not b then
+ List.map (fun c -> [], constr c) elts
+ else []
+ in
+ let unfolds = List.concat (List.map (fun dbname ->
+ let ((ids, csts), _) = searchtable_map dbname in
+ unfold_of_elts (fun x -> EvalConstRef x) (Cpred.elements csts) @
+ unfold_of_elts (fun x -> EvalVarRef x) (Idpred.elements ids)) db)
+ in unfold_option unfolds cl
+
+TACTIC EXTEND autosimpl
+| [ "autosimpl" hintbases(db) ] ->
+ [ autosimpl (match db with None -> ["core"] | Some x -> "core"::x) None ]
+END
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index e2d3f21c7..4b5b71a19 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -334,10 +334,6 @@ Proof. firstorder. Qed.
(* eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3. *)
(* Proof. simpl_relation. Qed. *)
-Instance [ Reflexive A R ] (x : A) =>
- reflexive_morphism : Morphism R x | 4.
-Proof. firstorder. Qed.
-
(** [R] is Reflexive, hence we can build the needed proof. *)
Program Instance [ Morphism (A -> B) (R ==> R') m, MorphismProxy A R x ] =>
@@ -407,8 +403,24 @@ Inductive normalization_done : Prop := did_normalization.
Ltac morphism_normalization :=
match goal with
| [ _ : normalization_done |- _ ] => fail
+(* | [ _ : subrelation_done |- _ ] => fail (* avoid useless interleavings. *) *)
| [ |- @Morphism _ _ _ ] => let H := fresh "H" in
set(H:=did_normalization) ; eapply @morphism_releq_morphism
end.
Hint Extern 5 (@Morphism _ _ _) => morphism_normalization : typeclass_instances.
+
+(** Every reflexive relation gives rise to a morphism, only for immediately solving goals without variables. *)
+
+Lemma reflexive_morphism [ Reflexive A R ] (x : A)
+ : Morphism R x.
+Proof. firstorder. Qed.
+
+Ltac morphism_reflexive :=
+ match goal with
+ | [ _ : normalization_done |- _ ] => fail
+ | [ _ : subrelation_done |- _ ] => fail
+ | [ |- @Morphism _ _ _ ] => eapply @reflexive_morphism
+ end.
+
+Hint Extern 4 (@Morphism _ _ _) => morphism_reflexive : typeclass_instances. \ No newline at end of file
diff --git a/theories/Ints/num/GenMul.v b/theories/Ints/num/GenMul.v
index 5522e41bf..c7ac1ea3e 100644
--- a/theories/Ints/num/GenMul.v
+++ b/theories/Ints/num/GenMul.v
@@ -406,8 +406,9 @@ Section GenMul.
intros z Hz; rewrite <- Hz; unfold interp_carry; assert (Hz1 := (spec_ww_to_Z z)).
generalize (spec_w_compare xl xh); case (w_compare xl xh); intros Hxlh;
try rewrite Hxlh; try rewrite spec_w_0; try (ring; fail).
- generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh;
- try rewrite Hylh; try rewrite spec_w_0; try (ring; fail).
+ generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh.
+ rewrite Hylh; rewrite spec_w_0; try (ring; fail).
+ rewrite spec_w_0; try (ring; fail).
repeat (rewrite spec_ww_sub || rewrite spec_w_sub || rewrite spec_w_mul_c).
repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
split; auto with zarith.
@@ -425,8 +426,8 @@ Section GenMul.
rewrite spec_w_1; unfold interp_carry in Hz2; rewrite Hz2;
repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
- generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh;
- try rewrite Hylh; try rewrite spec_w_0; try (ring; fail).
+ generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh.
+ rewrite Hylh; rewrite spec_w_0; try (ring; fail).
match goal with |- context[ww_add_c ?x ?y] =>
generalize (spec_ww_add_c x y); case (ww_add_c x y); try rewrite spec_w_0;
intros z1 Hz2
@@ -436,6 +437,7 @@ Section GenMul.
rewrite spec_w_1; unfold interp_carry in Hz2; rewrite Hz2;
repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
+ rewrite spec_w_0; try (ring; fail).
repeat (rewrite spec_ww_sub || rewrite spec_w_sub || rewrite spec_w_mul_c).
repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
split.
diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v
index 8116045b6..ac3664054 100644
--- a/theories/Sets/Powerset_Classical_facts.v
+++ b/theories/Sets/Powerset_Classical_facts.v
@@ -101,7 +101,6 @@ Section Sets_as_an_algebra.
intros X x H'; red in |- *.
intros x0 H'0; try assumption.
elim (classic (x = x0)); intro K; auto with sets.
- elim K; auto with sets.
Qed.
Lemma add_soustr_1 :
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-14 07:32:11 +0000