diff options
| -rw-r--r-- | pretyping/typeclasses.mli | 4 | ||||
| -rw-r--r-- | tactics/class_tactics.ml4 | 12 | ||||
| -rw-r--r-- | tactics/equality.ml | 51 | ||||
| -rw-r--r-- | tactics/equality.mli | 6 | ||||
| -rw-r--r-- | tactics/rewrite.ml4 | 62 | ||||
| -rw-r--r-- | theories/Classes/RelationClasses.v | 57 | ||||
| -rw-r--r-- | theories/Classes/SetoidTactics.v | 13 | ||||
| -rw-r--r-- | theories/FSets/FMapFacts.v | 2 | ||||
| -rw-r--r-- | theories/FSets/FMapPositive.v | 1 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 2 |
10 files changed, 111 insertions, 99 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index d5f5d6182..c2f046440 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -84,10 +84,10 @@ val is_class_evar : evar_map -> evar_info -> bool val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool -> env -> evar_defs -> evar_defs -val resolve_one_typeclass : env -> evar_map -> types -> constr +val resolve_one_typeclass : env -> evar_map -> types -> open_constr val register_add_instance_hint : (constant -> int option -> unit) -> unit val add_instance_hint : constant -> int option -> unit val solve_instanciations_problem : (env -> evar_defs -> bool -> bool -> bool -> evar_defs) ref -val solve_instanciation_problem : (env -> evar_map -> types -> constr) ref +val solve_instanciation_problem : (env -> evar_map -> types -> open_constr) ref 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 diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 1a966ded5..4f69b52c2 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -77,31 +77,32 @@ Proof. tauto. Qed. Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances. -Program Instance flip_Irreflexive `(Irreflexive A R) : Irreflexive (flip R) := +Program Definition flip_Irreflexive `(Irreflexive A R) : Irreflexive (flip R) := irreflexivity (R:=R). -Program Instance flip_Symmetric `(Symmetric A R) : Symmetric (flip R). +Program Definition flip_Symmetric `(Symmetric A R) : Symmetric (flip R) := + fun x y H => symmetry (R:=R) H. - Solve Obligations using unfold flip ; intros ; eapply symmetry ; assumption. - -Program Instance flip_Asymmetric `(Asymmetric A R) : Asymmetric (flip R). +Program Definition flip_Asymmetric `(Asymmetric A R) : Asymmetric (flip R) := + fun x y H H' => asymmetry (R:=R) H H'. - Solve Obligations using program_simpl ; unfold flip in * ; intros ; eapply asymmetry ; eauto. - -Program Instance flip_Transitive `(Transitive A R) : Transitive (flip R). +Program Definition flip_Transitive `(Transitive A R) : Transitive (flip R) := + fun x y z H H' => transitivity (R:=R) H' H. - Solve Obligations using unfold flip ; program_simpl ; eapply transitivity ; eauto. +Hint Extern 3 (Irreflexive (flip _)) => class_apply flip_Irreflexive : typeclass_instances. +Hint Extern 3 (Symmetric (flip _)) => class_apply flip_Symmetric : typeclass_instances. +Hint Extern 3 (Asymmetric (flip _)) => class_apply flip_Asymmetric : typeclass_instances. +Hint Extern 3 (Transitive (flip _)) => class_apply flip_Transitive : typeclass_instances. -Program Instance Reflexive_complement_Irreflexive `(Reflexive A (R : relation A)) +Definition Reflexive_complement_Irreflexive `(Reflexive A (R : relation A)) : Irreflexive (complement R). +Proof. firstorder. Qed. - Next Obligation. - Proof. firstorder. Qed. +Definition complement_Symmetric `(Symmetric A (R : relation A)) : Symmetric (complement R). +Proof. firstorder. Qed. -Program Instance complement_Symmetric `(Symmetric A (R : relation A)) : Symmetric (complement R). - - Next Obligation. - Proof. firstorder. Qed. +Hint Extern 3 (Symmetric (complement _)) => class_apply complement_Symmetric : typeclass_instances. +Hint Extern 3 (Irreflexive (complement _)) => class_apply Reflexive_complement_Irreflexive : typeclass_instances. (** * Standard instances. *) @@ -180,8 +181,9 @@ Instance Equivalence_PER `(Equivalence A R) : PER R | 10 := Class Antisymmetric A eqA `{equ : Equivalence A eqA} (R : relation A) := antisymmetry : forall x y, R x y -> R y x -> eqA x y. -Program Instance flip_antiSymmetric `(Antisymmetric A eqA R) : - ! Antisymmetric A eqA (flip R). +Program Definition flip_antiSymmetric `(Antisymmetric A eqA R) : + Antisymmetric A eqA (flip R). +Proof. firstorder. Qed. (** Leibinz equality [eq] is an equivalence relation. The instance has low priority as it is always applicable @@ -392,3 +394,22 @@ Program Instance subrelation_partial_order : Typeclasses Opaque arrows predicate_implication predicate_equivalence relation_equivalence pointwise_lifting. + +(** Rewrite relation on a given support: declares a relation as a rewrite + relation for use by the generalized rewriting tactic. + It helps choosing if a rewrite should be handled + by the generalized or the regular rewriting tactic using leibniz equality. + Users can declare an [RewriteRelation A RA] anywhere to declare default + relations. This is also done automatically by the [Declare Relation A RA] + commands. *) + +Class RewriteRelation {A : Type} (RA : relation A). + +Instance: RewriteRelation impl. +Instance: RewriteRelation iff. +Instance: RewriteRelation (@relation_equivalence A). + +(** Any [Equivalence] declared in the context is automatically considered + a rewrite relation. *) + +Instance equivalence_rewrite_relation `(Equivalence A eqA) : RewriteRelation eqA.
\ No newline at end of file diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index 226dfbd22..d009a456e 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -1,4 +1,3 @@ -(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.SetoidTactics") -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -24,18 +23,6 @@ Export ProperNotations. Set Implicit Arguments. Unset Strict Implicit. -(** Setoid relation on a given support: declares a relation as a setoid - for use with rewrite. It helps choosing if a rewrite should be handled - by setoid_rewrite or the regular rewrite using leibniz equality. - Users can declare an [SetoidRelation A RA] anywhere to declare default - relations. This is also done automatically by the [Declare Relation A RA] - commands. *) - -Class SetoidRelation A (R : relation A). - -Instance impl_setoid_relation : SetoidRelation impl. -Instance iff_setoid_relation : SetoidRelation iff. - (** Default relation on a given support. Can be used by tactics to find a sensible default relation on any carrier. Users can declare an [Instance def : DefaultRelation A RA] anywhere to diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index e116067af..e09db9b6e 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -1021,7 +1021,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). case_eq (find k' m'); auto; intros e'; rewrite <- find_mapsto_iff. intro; elim (Heq k' e'); auto. intros k e a m' m'' _ _ Hadd Heq k'. - rewrite Hadd, 2 add_o, Heq; auto. + red in Heq. rewrite Hadd, 2 add_o, Heq; auto. Qed. Section Fold_More. diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index 37cacbc75..10c7ce4a8 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -703,6 +703,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. intros; intro. generalize (mem_1 H0). rewrite mem_find. + red in H. rewrite H. rewrite grs. intros; discriminate. diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 2d2a86ef0..11a821b7c 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -342,7 +342,7 @@ module Latex = struct (* This is broken if we are in math mode, but coqdoc currently isn't tracking that *) - let start_emph () = printf "\\textit{ " + let start_emph () = printf "\\textit{" let stop_emph () = printf "}" |