diff options
| -rw-r--r-- | contrib/subtac/subtac_classes.ml | 5 | ||||
| -rw-r--r-- | contrib/subtac/subtac_classes.mli | 1 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.ml | 4 | ||||
| -rw-r--r-- | tactics/class_tactics.ml4 | 256 | ||||
| -rw-r--r-- | theories/Classes/Morphisms.v | 29 | ||||
| -rw-r--r-- | theories/Classes/SetoidClass.v | 2 | ||||
| -rw-r--r-- | theories/FSets/FMapFacts.v | 22 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NBase.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/NumPrelude.v | 4 | ||||
| -rw-r--r-- | toplevel/classes.ml | 26 | ||||
| -rw-r--r-- | toplevel/classes.mli | 7 |
11 files changed, 224 insertions, 134 deletions
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml index 4b4a6458b..cb3873bdf 100644 --- a/contrib/subtac/subtac_classes.ml +++ b/contrib/subtac/subtac_classes.ml @@ -100,7 +100,7 @@ let type_class_instance_params isevars env id n ctx inst subst = let substitution_of_constrs ctx cstrs = List.fold_right2 (fun c (na, _, _) acc -> (na, c) :: acc) cstrs ctx [] -let new_instance ctx (instid, bk, cl) props pri = +let new_instance ctx (instid, bk, cl) props ?(on_free_vars=Classes.default_on_free_vars) pri = let env = Global.env() in let isevars = ref (Evd.create_evar_defs Evd.empty) in let bound = Implicit_quantifiers.ids_of_list (Termops.ids_of_context env) in @@ -133,9 +133,10 @@ let new_instance ctx (instid, bk, cl) props pri = let ctx_bound = Idset.union bound (Implicit_quantifiers.ids_of_list fvs) in let gen_ids = Implicit_quantifiers.free_vars_of_constr_expr ~bound:ctx_bound tclass [] in let bound = Idset.union (Implicit_quantifiers.ids_of_list gen_ids) ctx_bound in + on_free_vars (List.rev (gen_ids @ fvs)); let gen_ctx = Implicit_quantifiers.binder_list_of_ids gen_ids in let ctx, avoid = Classes.name_typeclass_binders bound ctx in - let ctx = List.rev_append gen_ctx ctx in + let ctx = List.append ctx (List.rev gen_ctx) in let k, ctx', imps, subst = let c = Command.generalize_constr_expr tclass ctx in let c', imps = interp_type_evars_impls ~evdref:isevars env c in diff --git a/contrib/subtac/subtac_classes.mli b/contrib/subtac/subtac_classes.mli index 9a6730454..92a94cda6 100644 --- a/contrib/subtac/subtac_classes.mli +++ b/contrib/subtac/subtac_classes.mli @@ -36,5 +36,6 @@ val new_instance : Topconstr.local_binder list -> typeclass_constraint -> binder_def_list -> + ?on_free_vars:(identifier list -> unit) -> int option -> identifier diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 2610f1036..cf37efc77 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -71,12 +71,12 @@ let free_vars_of_binders ?(bound=Idset.empty) l (binders : local_binder list) = let rec aux bdvars l c = match c with ((LocalRawAssum (n, _, c)) :: tl) -> let bound = ids_of_names n in - let l' = bound @ free_vars_of_constr_expr c ~bound:bdvars l in + let l' = free_vars_of_constr_expr c ~bound:bdvars l in aux (Idset.union (ids_of_list bound) bdvars) l' tl | ((LocalRawDef (n, c)) :: tl) -> let bound = match snd n with Anonymous -> [] | Name n -> [n] in - let l' = bound @ free_vars_of_constr_expr c ~bound:bdvars l in + let l' = free_vars_of_constr_expr c ~bound:bdvars l in aux (Idset.union (ids_of_list bound) bdvars) l' tl | [] -> bdvars, l diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index f00515ab6..9b0bb188b 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -550,8 +550,8 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy. new_evar isevars env relty | Some x -> f x in - let rec aux t l = - let t = Reductionops.whd_betadeltaiota env (Evd.evars_of !isevars) t in + let rec aux ty l = + let t = Reductionops.whd_betadeltaiota env (Evd.evars_of !isevars) ty in match kind_of_term t, l with | Prod (na, ty, b), obj :: cstrs -> let (b, arg, evars) = aux b cstrs in @@ -563,7 +563,7 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy. | _, [] -> (match finalcstr with None -> - let t = Reductionops.nf_betaiota t in + let t = Reductionops.nf_betaiota ty in let rel = mk_relty t None in t, rel, [t, rel] | Some codom -> let (t, rel) = Lazy.force codom in @@ -680,7 +680,7 @@ let rewrite2_unif_flags = { (* let unification_rewrite c1 c2 cl but gl = *) (* let (env',c1) = *) (* try *) -(* (\* ~flags:(false,true) to allow to mark occurences that must not be *) +(* (\* ~flags:(false,true) to allow to mark occurrences that must not be *) (* rewritten simply by replacing them with let-defined definitions *) (* in the context *\) *) (* w_unify_to_subterm ~flags:rewrite_unif_flags (pf_env gl) (c1,but) cl.evd *) @@ -989,10 +989,10 @@ open Genarg open Extraargs TACTIC EXTEND class_rewrite -| [ "clrewrite" orient(o) constr(c) "in" hyp(id) "at" occurences(occ) ] -> [ cl_rewrite_clause c o occ (Some (([],id), [])) ] -| [ "clrewrite" orient(o) constr(c) "at" occurences(occ) "in" hyp(id) ] -> [ cl_rewrite_clause c o occ (Some (([],id), [])) ] +| [ "clrewrite" orient(o) constr(c) "in" hyp(id) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o occ (Some (([],id), [])) ] +| [ "clrewrite" orient(o) constr(c) "at" occurrences(occ) "in" hyp(id) ] -> [ cl_rewrite_clause c o occ (Some (([],id), [])) ] | [ "clrewrite" orient(o) constr(c) "in" hyp(id) ] -> [ cl_rewrite_clause c o [] (Some (([],id), [])) ] -| [ "clrewrite" orient(o) constr(c) "at" occurences(occ) ] -> [ cl_rewrite_clause c o occ None ] +| [ "clrewrite" orient(o) constr(c) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o occ None ] | [ "clrewrite" orient(o) constr(c) ] -> [ cl_rewrite_clause c o [] None ] END @@ -1084,25 +1084,31 @@ TACTIC EXTEND setoid_rewrite -> [ cl_rewrite_clause c o [] None ] | [ "setoid_rewrite" orient(o) constr(c) "in" hyp(id) ] -> [ cl_rewrite_clause c o [] (Some (([],id), []))] - | [ "setoid_rewrite" orient(o) constr(c) "at" occurences(occ) ] -> + | [ "setoid_rewrite" orient(o) constr(c) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o occ None] - | [ "setoid_rewrite" orient(o) constr(c) "at" occurences(occ) "in" hyp(id)] -> + | [ "setoid_rewrite" orient(o) constr(c) "at" occurrences(occ) "in" hyp(id)] -> [ cl_rewrite_clause c o occ (Some (([],id), []))] - | [ "setoid_rewrite" orient(o) constr(c) "in" hyp(id) "at" occurences(occ)] -> + | [ "setoid_rewrite" orient(o) constr(c) "in" hyp(id) "at" occurrences(occ)] -> [ cl_rewrite_clause c o occ (Some (([],id), []))] END (* let solve_obligation lemma = *) (* tclTHEN (Tacinterp.interp (Tacexpr.TacAtom (dummy_loc, Tacexpr.TacAnyConstructor None))) *) (* (eapply_with_bindings (Constrintern.interp_constr Evd.empty (Global.env()) lemma, NoBindings)) *) - + let mkappc s l = CAppExpl (dummy_loc,(None,(Libnames.Ident (dummy_loc,id_of_string s))),l) -let declare_instance a aeq n s = ((dummy_loc,Name n), Explicit, - CAppExpl (dummy_loc, (None, Qualid (dummy_loc, qualid_of_string s)), - [a;aeq])) +let declare_an_instance n s args = + ((dummy_loc,Name n), Explicit, + CAppExpl (dummy_loc, (None, Qualid (dummy_loc, qualid_of_string s)), + args)) -let anew_instance instance fields = new_instance [] instance fields None +let declare_instance a aeq n s = declare_an_instance n s [a;aeq] + +let anew_instance binders instance fields = + new_instance binders instance fields + ~on_free_vars:Classes.fail_on_free_vars + None let require_library dirpath = let qualid = (dummy_loc, Libnames.qualid_of_dirpath (Libnames.dirpath_of_string dirpath)) in @@ -1111,75 +1117,85 @@ let require_library dirpath = let check_required_library d = let d' = List.map id_of_string d in let dir = make_dirpath (List.rev d') in - if not (Library.library_is_opened dir) || not (Library.library_is_loaded dir) then + if (* not (Library.library_is_opened dir) || *)not (Library.library_is_loaded dir) then error ("Library "^(list_last d)^" has to be required first") let init_setoid () = check_required_library ["Coq";"Setoids";"Setoid"] -let declare_instance_refl a aeq n lemma = +let declare_instance_refl binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_refl") "Coq.Classes.RelationClasses.Reflexive" - in anew_instance instance + in anew_instance binders instance [((dummy_loc,id_of_string "reflexivity"),[],lemma)] -let declare_instance_sym a aeq n lemma = +let declare_instance_sym binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_sym") "Coq.Classes.RelationClasses.Symmetric" - in anew_instance instance + in anew_instance binders instance [((dummy_loc,id_of_string "symmetry"),[],lemma)] -let declare_instance_trans a aeq n lemma = +let declare_instance_trans binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_trans") "Coq.Classes.RelationClasses.Transitive" - in anew_instance instance + in anew_instance binders instance [((dummy_loc,id_of_string "transitivity"),[],lemma)] let constr_tac = Tacinterp.interp (Tacexpr.TacAtom (dummy_loc, Tacexpr.TacAnyConstructor None)) -let declare_relation a aeq n refl symm trans = +let declare_relation ?(binders=[]) a aeq n refl symm trans = init_setoid (); match (refl,symm,trans) with (None, None, None) -> - let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.DefaultRelation" - in ignore(anew_instance instance []) + let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.DefaultRelation" + in ignore(anew_instance binders instance []) | (Some lemma1, None, None) -> - ignore (declare_instance_refl a aeq n lemma1) + ignore (declare_instance_refl binders a aeq n lemma1) | (None, Some lemma2, None) -> - ignore (declare_instance_sym a aeq n lemma2) + ignore (declare_instance_sym binders a aeq n lemma2) | (None, None, Some lemma3) -> - ignore (declare_instance_trans a aeq n lemma3) + ignore (declare_instance_trans binders a aeq n lemma3) | (Some lemma1, Some lemma2, None) -> - ignore (declare_instance_refl a aeq n lemma1); - ignore (declare_instance_sym a aeq n lemma2) + ignore (declare_instance_refl binders a aeq n lemma1); + ignore (declare_instance_sym binders a aeq n lemma2) | (Some lemma1, None, Some lemma3) -> - let lemma_refl = declare_instance_refl a aeq n lemma1 in - let lemma_trans = declare_instance_trans a aeq n lemma3 in + let lemma_refl = declare_instance_refl binders a aeq n lemma1 in + let lemma_trans = declare_instance_trans binders a aeq n lemma3 in let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in ignore( - anew_instance instance + anew_instance binders instance [((dummy_loc,id_of_string "preorder_refl"), [], mkIdentC lemma_refl); ((dummy_loc,id_of_string "preorder_trans"),[], mkIdentC lemma_trans)]) | (None, Some lemma2, Some lemma3) -> - let lemma_sym = declare_instance_sym a aeq n lemma2 in - let lemma_trans = declare_instance_trans a aeq n lemma3 in + let lemma_sym = declare_instance_sym binders a aeq n lemma2 in + let lemma_trans = declare_instance_trans binders a aeq n lemma3 in let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in ignore( - anew_instance instance + anew_instance binders instance [((dummy_loc,id_of_string "per_sym"), [], mkIdentC lemma_sym); ((dummy_loc,id_of_string "per_trans"),[], mkIdentC lemma_trans)]) | (Some lemma1, Some lemma2, Some lemma3) -> - let lemma_refl = declare_instance_refl a aeq n lemma1 in - let lemma_sym = declare_instance_sym a aeq n lemma2 in - let lemma_trans = declare_instance_trans a aeq n lemma3 in + let lemma_refl = declare_instance_refl binders a aeq n lemma1 in + let lemma_sym = declare_instance_sym binders a aeq n lemma2 in + let lemma_trans = declare_instance_trans binders a aeq n lemma3 in let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in ignore( - anew_instance instance - [((dummy_loc,id_of_string "equiv_refl"), [], mkIdentC lemma_refl); - ((dummy_loc,id_of_string "equiv_sym"), [], mkIdentC lemma_sym); - ((dummy_loc,id_of_string "equiv_trans"),[], mkIdentC lemma_trans)]) + anew_instance binders instance + [((dummy_loc,id_of_string "equiv_refl"), [], mkIdentC lemma_refl); + ((dummy_loc,id_of_string "equiv_sym"), [], mkIdentC lemma_sym); + ((dummy_loc,id_of_string "equiv_trans"),[], mkIdentC lemma_trans)]) + +type 'a binders_let_argtype = (local_binder list, 'a) Genarg.abstract_argument_type + +let (wit_binders_let : Genarg.tlevel binders_let_argtype), + (globwit_binders_let : Genarg.glevel binders_let_argtype), + (rawwit_binders_let : Genarg.rlevel binders_let_argtype) = + Genarg.create_arg "binders_let" + +open Pcoq.Constr VERNAC COMMAND EXTEND AddRelation - [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> [ declare_relation a aeq n (Some lemma1) (Some lemma2) None ] + | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "as" ident(n) ] -> [ declare_relation a aeq n (Some lemma1) None None ] @@ -1208,6 +1224,40 @@ VERNAC COMMAND EXTEND AddRelation3 [ declare_relation a aeq n None None (Some lemma3) ] END +VERNAC COMMAND EXTEND AddParametricRelation + | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) + "reflexivity" "proved" "by" constr(lemma1) + "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> + [ declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) None ] + | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) + "reflexivity" "proved" "by" constr(lemma1) + "as" ident(n) ] -> + [ declare_relation ~binders:b a aeq n (Some lemma1) None None ] + | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "as" ident(n) ] -> + [ declare_relation ~binders:b a aeq n None None None ] +END + +VERNAC COMMAND EXTEND AddParametricRelation2 + [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) + "as" ident(n) ] -> + [ declare_relation ~binders:b a aeq n None (Some lemma2) None ] + | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> + [ declare_relation ~binders:b a aeq n None (Some lemma2) (Some lemma3) ] +END + +VERNAC COMMAND EXTEND AddParametricRelation3 + [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> + [ declare_relation ~binders:b a aeq n (Some lemma1) None (Some lemma3) ] + | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) + "as" ident(n) ] -> + [ declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) ] + | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) + "as" ident(n) ] -> + [ declare_relation ~binders:b a aeq n None None (Some lemma3) ] +END + let mk_qualid s = Libnames.Qualid (dummy_loc, Libnames.qualid_of_string s) @@ -1271,10 +1321,10 @@ let build_morphism_signature m = in aux t in let t', sig_, evars = build_signature isevars env t cstrs None snd in - let _ = List.iter + let _ = List.iter (fun (ty, rel) -> let default = mkApp (Lazy.force default_relation, [| ty; rel |]) in - ignore(Evarutil.e_new_evar isevars env default)) + ignore (Evarutil.e_new_evar isevars env default)) evars in let morph = @@ -1283,7 +1333,7 @@ let build_morphism_signature m = let evd = resolve_all_evars_once false (true, 15) env (fun x evi -> class_of_constr evi.Evd.evar_concl <> None) !isevars in Evarutil.nf_isevar evd morph - + let default_morphism sign m = let env = Global.env () in let isevars = ref (Evd.create_evar_defs Evd.empty) in @@ -1297,55 +1347,67 @@ let default_morphism sign m = let mor = resolve_one_typeclass env morph in mor, respect_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 instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" + in ignore( + anew_instance binders instance + [((dummy_loc,id_of_string "equiv_refl"), [], mkIdentC lemma_refl); + ((dummy_loc,id_of_string "equiv_sym"), [], mkIdentC lemma_sym); + ((dummy_loc,id_of_string "equiv_trans"),[], mkIdentC lemma_trans)]) + +let add_morphism_infer m n = + init_setoid (); + let instance_id = add_suffix n "_Morphism" in + let instance = build_morphism_signature m in + if Lib.is_modtype () then + let cst = Declare.declare_internal_constant instance_id + (Entries.ParameterEntry (instance,false), Decl_kinds.IsAssumption Decl_kinds.Logical) + in + add_instance { is_class = Lazy.force morphism_class ; is_pri = None; is_impl = cst }; + 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 { is_class = Lazy.force morphism_class ; is_pri = None; is_impl = cst }; + declare_projection n instance_id (ConstRef cst) + | _ -> assert false); + Pfedit.by (Tacinterp.interp <:tactic<add_morphism_tactic>>)) (); + Flags.if_verbose (fun x -> msg (Printer.pr_open_subgoals x)) () + +let add_morphism binders m s n = + init_setoid (); + let instance_id = add_suffix n "_Morphism" in + let instance = + ((dummy_loc,Name instance_id), Explicit, + CAppExpl (dummy_loc, + (None, Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Classes.Morphisms.Morphism")), + [cHole; s; m])) + in + let tac = Tacinterp.interp <:tactic<add_morphism_tactic>> in + ignore(new_instance binders instance [] + ~on_free_vars:Classes.fail_on_free_vars + ~tac ~hook:(fun cst -> declare_projection n instance_id (ConstRef cst)) + None) + VERNAC COMMAND EXTEND AddSetoid1 [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> - [ init_setoid (); - let lemma_refl = declare_instance_refl a aeq n (mkappc "Seq_refl" [a;aeq;t]) in - let lemma_sym = declare_instance_sym a aeq n (mkappc "Seq_sym" [a;aeq;t]) in - let lemma_trans = declare_instance_trans 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 instance - [((dummy_loc,id_of_string "equiv_refl"), [], mkIdentC lemma_refl); - ((dummy_loc,id_of_string "equiv_sym"), [], mkIdentC lemma_sym); - ((dummy_loc,id_of_string "equiv_trans"),[], mkIdentC lemma_trans)])] + [ add_setoid [] a aeq t n ] + | [ "Add" "Parametric" "Setoid" binders_let(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> + [ add_setoid binders a aeq t n ] | [ "Add" "Morphism" constr(m) ":" ident(n) ] -> - [ init_setoid (); - let instance_id = add_suffix n "_Morphism" in - let instance = build_morphism_signature m in - if Lib.is_modtype () then - let cst = Declare.declare_internal_constant instance_id - (Entries.ParameterEntry (instance,false), Decl_kinds.IsAssumption Decl_kinds.Logical) - in - add_instance { is_class = Lazy.force morphism_class ; is_pri = None; is_impl = cst }; - 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 { is_class = Lazy.force morphism_class ; is_pri = None; is_impl = cst }; - declare_projection n instance_id (ConstRef cst) - | _ -> assert false); - Pfedit.by (Tacinterp.interp <:tactic<add_morphism_tactic>>)) (); - Flags.if_verbose (fun x -> msg (Printer.pr_open_subgoals x)) () ] - + [ add_morphism_infer m n ] | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] -> - [ init_setoid (); - let instance_id = add_suffix n "_Morphism" in - let instance = - ((dummy_loc,Name instance_id), Explicit, - CAppExpl (dummy_loc, - (None, Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Classes.Morphisms.Morphism")), - [cHole; s; m])) - in - let tac = Tacinterp.interp <:tactic<add_morphism_tactic>> in - ignore(new_instance [] instance [] - ~tac ~hook:(fun cst -> declare_projection n instance_id (ConstRef cst)) - None) - ] + [ add_morphism [] m s n ] + | [ "Add" "Parametric" "Morphism" binders_let(binders) ":" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] -> + [ add_morphism binders m s n ] END (** Bind to "rewrite" too *) @@ -1375,7 +1437,7 @@ let check_evar_map_of_evars_defs evd = let unification_rewrite l2r c1 c2 cl rel but gl = let (env',c') = try - (* ~flags:(false,true) to allow to mark occurences that must not be + (* ~flags:(false,true) to allow to mark occurrences that must not be rewritten simply by replacing them with let-defined definitions in the context *) Unification.w_unify_to_subterm ~flags:rewrite_unif_flags (pf_env gl) ((if l2r then c1 else c2),but) cl.evd @@ -1408,15 +1470,15 @@ let get_hyp gl c clause l2r = let general_rewrite_flags = { under_lambdas = false; on_morphisms = false } -let general_s_rewrite l2r c ~new_goals gl = +let general_s_rewrite l2r occs c ~new_goals gl = let meta = Evarutil.new_meta() in let hypinfo = ref (get_hyp gl c None l2r) in - cl_rewrite_clause_aux ~flags:general_rewrite_flags hypinfo meta [] None gl + cl_rewrite_clause_aux ~flags:general_rewrite_flags hypinfo meta occs None gl -let general_s_rewrite_in id l2r c ~new_goals gl = +let general_s_rewrite_in id l2r occs c ~new_goals gl = let meta = Evarutil.new_meta() in let hypinfo = ref (get_hyp gl c (Some id) l2r) in - cl_rewrite_clause_aux ~flags:general_rewrite_flags hypinfo meta [] (Some (([],id), [])) gl + cl_rewrite_clause_aux ~flags:general_rewrite_flags hypinfo meta occs (Some (([],id), [])) gl let classes_dirpath = make_dirpath (List.map id_of_string ["Classes";"Coq"]) diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 975dcf1dd..552ff996a 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -128,9 +128,9 @@ Proof. firstorder. Qed. Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl). Proof. firstorder. Qed. -Instance [ subrelation A R R' ] => pointwise_subrelation : +Instance [ sub : subrelation A R R' ] => pointwise_subrelation : subrelation (pointwise_relation (A:=B) R) (pointwise_relation R') | 4. -Proof. reduce. unfold pointwise_relation in *. apply subrelation0. apply H. Qed. +Proof. reduce. unfold pointwise_relation in *. apply sub. apply H. Qed. (** The complement of a relation conserves its morphisms. *) @@ -186,7 +186,7 @@ Program Instance [ Transitive A R ] => (** Morphism declarations for partial applications. *) -Program Instance [ Transitive A R ] (x : A) => +Program Instance [ Transitive A R ] => trans_contra_inv_impl_morphism : Morphism (R --> inverse impl) (R x). Next Obligation. @@ -194,7 +194,7 @@ Program Instance [ Transitive A R ] (x : A) => transitivity y... Qed. -Program Instance [ Transitive A R ] (x : A) => +Program Instance [ Transitive A R ] => trans_co_impl_morphism : Morphism (R ==> impl) (R x). Next Obligation. @@ -202,7 +202,7 @@ Program Instance [ Transitive A R ] (x : A) => transitivity x0... Qed. -Program Instance [ Transitive A R, Symmetric A R ] (x : A) => +Program Instance [ Transitive A R, Symmetric A R ] => trans_sym_co_inv_impl_morphism : Morphism (R ==> inverse impl) (R x). Next Obligation. @@ -210,7 +210,7 @@ Program Instance [ Transitive A R, Symmetric A R ] (x : A) => transitivity y... Qed. -Program Instance [ Transitive A R, Symmetric _ R ] (x : A) => +Program Instance [ Transitive A R, Symmetric _ R ] => trans_sym_contra_impl_morphism : Morphism (R --> impl) (R x). Next Obligation. @@ -218,7 +218,7 @@ Program Instance [ Transitive A R, Symmetric _ R ] (x : A) => transitivity x0... Qed. -Program Instance [ Equivalence A R ] (x : A) => +Program Instance [ Equivalence A R ] => equivalence_partial_app_morphism : Morphism (R ==> iff) (R x). Next Obligation. @@ -231,7 +231,7 @@ Program Instance [ Equivalence A R ] (x : A) => (** [R] is Reflexive, hence we can build the needed proof. *) -Program Instance [ Morphism (A -> B) (R ==> R') m, Reflexive _ R ] (x : A) => +Program Instance [ Morphism (A -> B) (R ==> R') m, Reflexive _ R ] => Reflexive_partial_app_morphism : Morphism R' (m x) | 4. (** Every Transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof @@ -294,7 +294,7 @@ Program Instance inverse_iff_impl_id : (** Coq functions are morphisms for leibniz equality, applied only if really needed. *) -Instance (A : Type) [ Reflexive B R ] (m : A -> B) => +Instance (A : Type) [ Reflexive B R ] => eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3. Proof. simpl_relation. Qed. @@ -305,7 +305,7 @@ Proof. simpl_relation. Qed. (** [respectful] is a morphism for relation equivalence. *) Instance respectful_morphism : - Morphism (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B). + Morphism (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B). Proof. reduce. unfold respectful, relation_equivalence, predicate_equivalence in * ; simpl in *. @@ -335,14 +335,14 @@ Qed. Class (A : Type) => Normalizes (m : relation A) (m' : relation A) : Prop := normalizes : relation_equivalence m m'. -Instance (A : Type) (R : relation A) (B : Type) (R' : relation B) => - inverse_respectful_norm : Normalizes _ (inverse R ==> inverse R') (inverse (R ==> R')) . +Instance inverse_respectful_norm : + Normalizes (A -> B) (inverse R ==> inverse R') (inverse (R ==> R')) . Proof. firstorder. Qed. (* If not an inverse on the left, do a double inverse. *) -Instance (A : Type) (R : relation A) (B : Type) (R' : relation B) => - not_inverse_respectful_norm : Normalizes _ (R ==> inverse R') (inverse (inverse R ==> R')) | 4. +Instance not_inverse_respectful_norm : + Normalizes (A -> B) (R ==> inverse R') (inverse (inverse R ==> R')) | 4. Proof. firstorder. Qed. Instance [ Normalizes B R' (inverse R'') ] => @@ -391,4 +391,3 @@ Ltac morphism_normalization := end. Hint Extern 5 (@Morphism _ _ _) => morphism_normalization : typeclass_instances. - diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index f7f460123..526264612 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -131,7 +131,7 @@ Implicit Arguments setoid_morphism [[!sa]]. Existing Instance setoid_morphism. Program Definition setoid_partial_app_morphism [ sa : Setoid A ] (x : A) : Morphism (equiv ++> iff) (equiv x) := - Reflexive_partial_app_morphism x. + Reflexive_partial_app_morphism. Existing Instance setoid_partial_app_morphism. diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 617ea6f4f..e033343d1 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -662,19 +662,19 @@ Add Relation key E.eq Implicit Arguments Equal [[elt]]. -Add Relation (t elt) Equal +Add Parametric Relation (elt : Type) : (t elt) Equal reflexivity proved by (@Equal_refl elt) symmetry proved by (@Equal_sym elt) transitivity proved by (@Equal_trans elt) as EqualSetoid. -Add Morphism (@In elt) with signature E.eq ==> Equal ==> iff as In_m. +Add Parametric Morphism elt : (@In elt) with signature E.eq ==> Equal ==> iff as In_m. Proof. unfold Equal; intros k k' Hk m m' Hm. rewrite (In_iff m Hk), in_find_iff, in_find_iff, Hm; intuition. Qed. -Add Morphism (@MapsTo elt) +Add Parametric Morphism elt : (@MapsTo elt) with signature E.eq ==> @Logic.eq _ ==> Equal ==> iff as MapsTo_m. Proof. unfold Equal; intros k k' Hk e m m' Hm. @@ -682,26 +682,26 @@ rewrite (MapsTo_iff m e Hk), find_mapsto_iff, find_mapsto_iff, Hm; intuition. Qed. -Add Morphism (@Empty elt) with signature Equal ==> iff as Empty_m. +Add Parametric Morphism elt : (@Empty elt) with signature Equal ==> iff as Empty_m. Proof. unfold Empty; intros m m' Hm; intuition. rewrite <-Hm in H0; eauto. rewrite Hm in H0; eauto. Qed. -Add Morphism (@is_empty elt) with signature Equal ==> @Logic.eq _ as is_empty_m. +Add Parametric Morphism elt : (@is_empty elt) with signature Equal ==> @Logic.eq _ as is_empty_m. Proof. intros m m' Hm. rewrite eq_bool_alt, <-is_empty_iff, <-is_empty_iff, Hm; intuition. Qed. -Add Morphism (@mem elt) with signature E.eq ==> Equal ==> @Logic.eq _ as mem_m. +Add Parametric Morphism elt : (@mem elt) with signature E.eq ==> Equal ==> @Logic.eq _ as mem_m. Proof. intros k k' Hk m m' Hm. rewrite eq_bool_alt, <- mem_in_iff, <-mem_in_iff, Hk, Hm; intuition. Qed. -Add Morphism (@find elt) with signature E.eq ==> Equal ==> @Logic.eq _ as find_m. +Add Parametric Morphism elt : (@find elt) with signature E.eq ==> Equal ==> @Logic.eq _ as find_m. Proof. intros k k' Hk m m' Hm. generalize (find_mapsto_iff m k)(find_mapsto_iff m' k') @@ -712,7 +712,7 @@ rewrite <- H1, Hk, Hm, H2; auto. symmetry; rewrite <- H2, <-Hk, <-Hm, H1; auto. Qed. -Add Morphism (@add elt) with signature +Add Parametric Morphism elt : (@add elt) with signature E.eq ==> @Logic.eq _ ==> Equal ==> Equal as add_m. Proof. intros k k' Hk e m m' Hm y. @@ -721,7 +721,7 @@ elim n; rewrite <-Hk; auto. elim n; rewrite Hk; auto. Qed. -Add Morphism (@remove elt) with signature +Add Parametric Morphism elt : (@remove elt) with signature E.eq ==> Equal ==> Equal as remove_m. Proof. intros k k' Hk m m' Hm y. @@ -730,7 +730,7 @@ elim n; rewrite <-Hk; auto. elim n; rewrite Hk; auto. Qed. -Add Morphism (@map elt elt') with signature @Logic.eq _ ==> Equal ==> Equal as map_m. +Add Parametric Morphism elt elt' : (@map elt elt') with signature @Logic.eq _ ==> Equal ==> Equal as map_m. Proof. intros f m m' Hm y. rewrite map_o, map_o, Hm; auto. @@ -1104,7 +1104,7 @@ Module WProperties (E:DecidableType)(M:WSfun E). End Elt. - Add Morphism (@cardinal elt) with signature Equal ==> @Logic.eq _ as cardinal_m. + Add Parametric Morphism elt : (@cardinal elt) with signature Equal ==> @Logic.eq _ as cardinal_m. Proof. intros; apply Equal_cardinal; auto. Qed. End WProperties. diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index fc2cc81eb..1a11f7a13 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -81,7 +81,7 @@ function (by recursion) that maps 0 to false and the successor to true *) Definition if_zero (A : Set) (a b : A) (n : N) : A := recursion a (fun _ _ => b) n. -Add Morphism (if_zero A) with signature ((@eq (A:Set)) ==> (@eq A) ==> Neq ==> (@eq A)) as if_zero_wd. +Add Parametric Morphism (A : Set) : (if_zero A) with signature (@eq _ ==> @eq _ ==> Neq ==> @eq _) as if_zero_wd. Proof. intros; unfold if_zero. apply recursion_wd with (Aeq := (@eq A)). reflexivity. unfold fun2_eq; now intros. assumption. diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v index c063c7bc1..f042ab068 100644 --- a/theories/Numbers/NumPrelude.v +++ b/theories/Numbers/NumPrelude.v @@ -148,13 +148,13 @@ intros R1 R2 R3 H1 H2 x y; rewrite H1; apply H2. now symmetry. Qed. -Add Relation (A -> B -> Prop) (@relations_eq A B) +Add Parametric Relation (A B : Type) : (A -> B -> Prop) (@relations_eq A B) reflexivity proved by (proj1 (relations_eq_equiv A B)) symmetry proved by (proj2 (proj2 (relations_eq_equiv A B))) transitivity proved by (proj1 (proj2 (relations_eq_equiv A B))) as relations_eq_rel. -Add Morphism (@well_founded A) with signature (@relations_eq A A) ==> iff as well_founded_wd. +Add Parametric Morphism (A : Type) : (@well_founded A) with signature (@relations_eq A A) ==> iff as well_founded_wd. Proof. unfold relations_eq, well_founded; intros R1 R2 H; split; intros H1 a; induction (H1 a) as [x H2 H3]; constructor; diff --git a/toplevel/classes.ml b/toplevel/classes.ml index a539a87ba..db87d36ab 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -412,7 +412,25 @@ open Pp let ($$) g f = fun x -> g (f x) -let new_instance ctx (instid, bk, cl) props ?(tac:Proof_type.tactic option) ?(hook:(Names.constant -> unit) option) pri = +let default_on_free_vars = + Flags.if_verbose + (fun fvs -> + match fvs with + [] -> () + | l -> msgnl (str"Implicitly generalizing " ++ + prlist_with_sep (fun () -> str", ") Nameops.pr_id l ++ str".")) + +let fail_on_free_vars = function + [] -> () + | [fv] -> + errorlabstrm "Classes" + (str"Unbound variable " ++ Nameops.pr_id fv ++ str".") + | fvs -> errorlabstrm "Classes" + (str"Unbound variables " ++ + prlist_with_sep (fun () -> str", ") Nameops.pr_id fvs ++ str".") + +let new_instance ctx (instid, bk, cl) props ?(on_free_vars=default_on_free_vars) + ?(tac:Proof_type.tactic option) ?(hook:(Names.constant -> unit) option) pri = let env = Global.env() in let isevars = ref (Evd.create_evar_defs Evd.empty) in let bound = Implicit_quantifiers.ids_of_list (Termops.ids_of_context env) in @@ -444,10 +462,12 @@ let new_instance ctx (instid, bk, cl) props ?(tac:Proof_type.tactic option) ?(ho in let ctx_bound = Idset.union bound (Implicit_quantifiers.ids_of_list fvs) in let gen_ids = Implicit_quantifiers.free_vars_of_constr_expr ~bound:ctx_bound tclass [] in - let bound = Idset.union (Implicit_quantifiers.ids_of_list gen_ids) ctx_bound in + on_free_vars (List.rev fvs @ List.rev gen_ids); + let gen_idset = Implicit_quantifiers.ids_of_list gen_ids in + let bound = Idset.union gen_idset ctx_bound in let gen_ctx = Implicit_quantifiers.binder_list_of_ids gen_ids in let ctx, avoid = name_typeclass_binders bound ctx in - let ctx = List.rev_append gen_ctx ctx in + let ctx = List.append ctx (List.rev gen_ctx) in let k, ctx', subst = let c = Command.generalize_constr_expr tclass ctx in let _imps, c' = interp_type_evars isevars env c in diff --git a/toplevel/classes.mli b/toplevel/classes.mli index c25997141..be0c98743 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -39,10 +39,17 @@ val new_class : identifier located -> local_binder list -> binder_list -> unit +(* By default, print the free variables that are implicitely generalized. *) + +val default_on_free_vars : identifier list -> unit + +val fail_on_free_vars : identifier list -> unit + val new_instance : local_binder list -> typeclass_constraint -> binder_def_list -> + ?on_free_vars:(identifier list -> unit) -> ?tac:Proof_type.tactic -> ?hook:(constant -> unit) -> int option -> |