aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/class_tactics.ml412
-rw-r--r--tactics/equality.ml51
-rw-r--r--tactics/equality.mli6
-rw-r--r--tactics/rewrite.ml462
4 files changed, 67 insertions, 64 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index b163ed32a..e9dfce78b 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -399,9 +399,10 @@ let resolve_one_typeclass env ?(sigma=Evd.empty) gl =
let gls = { it = Evd.make_evar (Environ.named_context_val env) gl; sigma = sigma } in
let gls', v = eauto [searchtable_map typeclasses_db] gls in
let term = v [] in
- let term = fst (Refiner.extract_open_proof (sig_sig gls') term) in
- let term = Evarutil.nf_evar (sig_sig gls') term in
- if occur_existential term then raise Not_found else term
+ let evd = sig_sig gls' in
+ let term = fst (Refiner.extract_open_proof evd term) in
+ let term = Evarutil.nf_evar evd term in
+ evd, term
let _ =
Typeclasses.solve_instanciation_problem := (fun x y z -> resolve_one_typeclass x ~sigma:y z)
@@ -457,7 +458,8 @@ let resolve_all_evars debug m env p oevd do_split fail =
let res = try aux 1 (p comp) evd with Not_found -> None in
match res with
| None ->
- if fail then
+ if fail then
+ let evd = Evarutil.nf_evars evd in
(* Unable to satisfy the constraints. *)
let evm = if do_split then select_evars comp evd else evd in
let _, ev = Evd.fold
@@ -469,7 +471,7 @@ let resolve_all_evars debug m env p oevd do_split fail =
else b, None
else b, acc) evm (false, None)
in
- Typeclasses_errors.unsatisfiable_constraints env (Evd.evars_reset_evd evm evd) ev
+ Typeclasses_errors.unsatisfiable_constraints (Evarutil.nf_env_evar evm env) evm ev
else (* Best effort: do nothing *) oevd
| Some evd' -> docomp evd' comps
in docomp oevd split
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 699f33441..076f05f24 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -155,17 +155,17 @@ let general_elim_clause with_evars tac cls sigma c t l l2r elim gl =
else tclMAP try_clause cs gl
(* The next function decides in particular whether to try a regular
- rewrite or a setoid rewrite.
+ rewrite or a generalized rewrite.
Approach is to break everything, if [eq] appears in head position
- then regular rewrite else try setoid rewrite.
- If occurrences are set, use setoid_rewrite.
+ then regular rewrite else try general rewrite.
+ If occurrences are set, use general rewrite.
*)
-let general_setoid_rewrite_clause = ref (fun _ -> assert false)
-let register_general_setoid_rewrite_clause = (:=) general_setoid_rewrite_clause
+let general_rewrite_clause = ref (fun _ -> assert false)
+let register_general_rewrite_clause = (:=) general_rewrite_clause
-let is_applied_setoid_relation = ref (fun _ -> false)
-let register_is_applied_setoid_relation = (:=) is_applied_setoid_relation
+let is_applied_rewrite_relation = ref (fun _ _ _ _ -> None)
+let register_is_applied_rewrite_relation = (:=) is_applied_rewrite_relation
(* find_elim determines which elimination principle is necessary to
eliminate lbeq on sort_of_gl. *)
@@ -190,12 +190,12 @@ let adjust_rewriting_direction args lft2rgt =
(* other equality *)
lft2rgt
-let setoid_side_tac tac sidetac = side_tac tac (Option.map fst sidetac)
+let rewrite_side_tac tac sidetac = side_tac tac (Option.map fst sidetac)
let general_rewrite_ebindings_clause cls lft2rgt occs ?tac
((c,l) : open_constr with_bindings) with_evars gl =
if occs <> all_occurrences then (
- setoid_side_tac (!general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[]) tac gl)
+ rewrite_side_tac (!general_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac gl)
else
let env = pf_env gl in
let sigma, c' = c in
@@ -208,24 +208,21 @@ let general_rewrite_ebindings_clause cls lft2rgt occs ?tac
leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c' (it_mkProd_or_LetIn t rels)
l with_evars gl hdcncl
| None ->
- let env' = push_rel_context rels env in
- let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *)
- match match_with_equality_type t' with
- | Some (hdcncl,args) -> (* Maybe a setoid relation with eq inside *)
- let lft2rgt = adjust_rewriting_direction args lft2rgt in
- if l = NoBindings && !is_applied_setoid_relation t then
- setoid_side_tac (!general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[]) tac gl
- else
- (try leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c'
- (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars gl hdcncl
- with e ->
- try setoid_side_tac (!general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[]) tac gl
- with _ -> raise e)
- | None -> (* Can't be leibniz, try setoid *)
- if l = NoBindings
- then setoid_side_tac (!general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[]) tac gl
- else error "The term provided does not end with an equation."
-
+ match !is_applied_rewrite_relation env sigma rels t with
+ | Some _ ->
+ rewrite_side_tac (!general_rewrite_clause cls
+ lft2rgt occs (c,l) ~new_goals:[]) tac gl
+ | None ->
+ let env' = push_rel_context rels env in
+ let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *)
+ match match_with_equality_type t' with
+ | Some (hdcncl,args) ->
+ let lft2rgt = adjust_rewriting_direction args lft2rgt in
+ leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c'
+ (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars gl hdcncl
+ | None ->
+ error "The provided term does not end with an equality or a declared rewrite relation."
+
let general_rewrite_ebindings =
general_rewrite_ebindings_clause None
diff --git a/tactics/equality.mli b/tactics/equality.mli
index d694491b9..9d5bcca7a 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -45,10 +45,10 @@ val rewriteRL : ?tac:(tactic * conditions) -> constr -> tactic
(* Warning: old [general_rewrite_in] is now [general_rewrite_bindings_in] *)
-val register_general_setoid_rewrite_clause :
+val register_general_rewrite_clause :
(identifier option -> orientation ->
- occurrences -> open_constr -> new_goals:constr list -> tactic) -> unit
-val register_is_applied_setoid_relation : (constr -> bool) -> unit
+ occurrences -> open_constr with_bindings -> new_goals:constr list -> tactic) -> unit
+val register_is_applied_rewrite_relation : (env -> evar_defs -> rel_context -> constr -> open_constr option) -> unit
val general_rewrite_ebindings_clause : identifier option ->
orientation -> occurrences -> ?tac:(tactic * conditions) -> open_constr with_bindings -> evars_flag -> tactic
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 384ba3b93..da8d59ba8 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -127,7 +127,8 @@ let setoid_equiv = lazy (gen_constant ["Classes"; "SetoidClass"] "equiv")
let setoid_proper = lazy (gen_constant ["Classes"; "SetoidClass"] "setoid_proper")
let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "Equivalence_Reflexive")
-let setoid_relation = lazy (gen_constant ["Classes"; "SetoidTactics"] "SetoidRelation")
+let rewrite_relation_class = lazy (gen_constant ["Classes"; "RelationClasses"] "RewriteRelation")
+let rewrite_relation = lazy (gen_constant ["Classes"; "RelationClasses"] "rewrite_relation")
let arrow_morphism a b =
if isprop a && isprop b then
@@ -142,21 +143,24 @@ let proper_type = lazy (constr_of_global (Lazy.force proper_class).cl_impl)
let proper_proxy_type = lazy (constr_of_global (Lazy.force proper_proxy_class).cl_impl)
-let is_applied_setoid_relation t =
+let is_applied_rewrite_relation env sigma rels t =
match kind_of_term t with
| App (c, args) when Array.length args >= 2 ->
let head = if isApp c then fst (destApp c) else c in
- if eq_constr (Lazy.force coq_eq) head then false
- else (try
- let evd, evar = Evarutil.new_evar Evd.empty (Global.env()) (new_Type ()) in
- let inst = mkApp (Lazy.force setoid_relation, [| evar; c |]) in
- ignore(Typeclasses.resolve_one_typeclass (Global.env()) evd inst);
- true
- with _ -> false)
- | _ -> false
+ if eq_constr (Lazy.force coq_eq) head then None
+ else
+ (try
+ let params, args = array_chop (Array.length args - 2) args in
+ let env' = Environ.push_rel_context rels env in
+ let evd, evar = Evarutil.new_evar sigma env' (new_Type ()) in
+ let inst = mkApp (Lazy.force rewrite_relation_class, [| evar; mkApp (c, params) |]) in
+ let _ = Typeclasses.resolve_one_typeclass env' evd inst in
+ Some (sigma, it_mkProd_or_LetIn t rels)
+ with _ -> None)
+ | _ -> None
let _ =
- Equality.register_is_applied_setoid_relation is_applied_setoid_relation
+ Equality.register_is_applied_rewrite_relation is_applied_rewrite_relation
let split_head = function
hd :: tl -> hd, tl
@@ -218,7 +222,7 @@ let proper_proof env evars carrier relation x =
let find_class_proof proof_type proof_method env evars carrier relation =
try
let goal = mkApp (Lazy.force proof_type, [| carrier ; relation |]) in
- let c = Typeclasses.resolve_one_typeclass env evars goal in
+ let evars, c = Typeclasses.resolve_one_typeclass env evars goal in
mkApp (Lazy.force proof_method, [| carrier; relation; c |])
with e when Logic.catchable_exception e -> raise Not_found
@@ -1010,7 +1014,7 @@ let constr_tac = Tacinterp.interp (Tacexpr.TacAtom (dummy_loc, Tacexpr.TacAnyCon
let declare_relation ?(binders=[]) a aeq n refl symm trans =
init_setoid ();
- let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.SetoidTactics.SetoidRelation"
+ let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation"
in ignore(anew_instance binders instance []);
match (refl,symm,trans) with
(None, None, None) -> ()
@@ -1215,14 +1219,14 @@ let default_morphism sign m =
let morph =
mkApp (Lazy.force proper_type, [| t; sign; m |])
in
- let mor = resolve_one_typeclass env (merge_evars evars) morph in
+ let evars, mor = resolve_one_typeclass env (merge_evars evars) morph in
mor, proper_projection mor morph
let add_setoid binders a aeq t n =
init_setoid ();
let _lemma_refl = declare_instance_refl binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in
let _lemma_sym = declare_instance_sym binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
- let _lemma_trans = declare_instance_trans binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in
+ let _lemma_trans = declare_instance_trans binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in
let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
in ignore(
anew_instance binders instance
@@ -1242,18 +1246,18 @@ let add_morphism_infer glob m n =
declare_projection n instance_id (ConstRef cst)
else
let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
- Flags.silently
- (fun () ->
- Command.start_proof instance_id kind instance
- (fun _ -> function
- Libnames.ConstRef cst ->
- add_instance (Typeclasses.new_instance (Lazy.force proper_class) None
- glob cst);
- declare_projection n instance_id (ConstRef cst)
- | _ -> assert false);
- Pfedit.by (Tacinterp.interp <:tactic< Coq.Classes.SetoidTactics.add_morphism_tactic>>)) ();
- Flags.if_verbose (fun x -> msg (Printer.pr_open_subgoals x)) ()
-
+ Flags.silently
+ (fun () ->
+ Command.start_proof instance_id kind instance
+ (fun _ -> function
+ Libnames.ConstRef cst ->
+ add_instance (Typeclasses.new_instance (Lazy.force proper_class) None
+ glob cst);
+ declare_projection n instance_id (ConstRef cst)
+ | _ -> assert false);
+ Pfedit.by (Tacinterp.interp <:tactic< Coq.Classes.SetoidTactics.add_morphism_tactic>>)) ();
+ Flags.if_verbose (fun x -> msg (Printer.pr_open_subgoals x)) ()
+
let add_morphism glob binders m s n =
init_setoid ();
let instance_id = add_suffix n "_Proper" in
@@ -1351,7 +1355,7 @@ let apply_lemma gl (evm,c) cl l2r occs =
Strategies.choice app (subterm true general_rewrite_flags (fun env -> aux () env))
in !hypinfo, aux ()
-let general_s_rewrite cl l2r occs c ~new_goals gl =
+let general_s_rewrite cl l2r occs (c,l) ~new_goals gl =
let meta = Evarutil.new_meta() in
let hypinfo, strat = apply_lemma gl c cl l2r occs in
try cl_rewrite_clause_aux ~abs:hypinfo.abs strat meta cl gl
@@ -1367,7 +1371,7 @@ let general_s_rewrite_clause x =
| None -> general_s_rewrite None
| Some id -> general_s_rewrite (Some id)
-let _ = Equality.register_general_setoid_rewrite_clause general_s_rewrite_clause
+let _ = Equality.register_general_rewrite_clause general_s_rewrite_clause
let is_loaded d =
let d' = List.map id_of_string d in
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-26 21:07:36 +0000