From 07ffd30a82ebfe35811ca43d71aeacdb86f4cc87 Mon Sep 17 00:00:00 2001 From: msozeau Date: Thu, 6 Mar 2008 14:56:08 +0000 Subject: Syntax changes in typeclasses, remove "?" for usual implicit arguments binding, add "!" syntax for the new binders which require parameters and not superclasses. Change backquotes for curly braces for user-given implicit arguments, following tradition. This requires a hack a la lpar-id-coloneq. Change ident to global for typeclass names in class binders. Also requires a similar hack to distinguish between [ C t1 tn ] and [ c : C t1 tn ]. Update affected theories. While hacking the parsing of { wf }, factorized the two versions of fix annotation parsing that were present in g_constr and g_vernac. Add the possibility of the user optionaly giving the priority for resolve and exact hints (used by type classes). Syntax not fixed yet: a natural after the list of lemmas in "Hint Resolve" syntax, a natural after a "|" after the instance constraint in Instance declarations (ex in Morphisms.v). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10628 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/interface/blast.ml | 1 + contrib/interface/xlate.ml | 21 ++- contrib/subtac/subtac.ml | 4 +- contrib/subtac/subtac_classes.ml | 5 +- contrib/subtac/subtac_classes.mli | 1 + contrib/subtac/subtac_pretyping_F.ml | 6 +- parsing/g_constr.ml4 | 107 +++++++----- parsing/g_proofs.ml4 | 3 +- parsing/g_vernac.ml4 | 23 ++- parsing/pcoq.ml4 | 1 + parsing/pcoq.mli | 1 + parsing/ppvernac.ml | 7 +- pretyping/pretyping.ml | 6 +- pretyping/typeclasses.ml | 47 ++++-- pretyping/typeclasses.mli | 15 +- tactics/auto.ml | 30 ++-- tactics/auto.mli | 12 +- theories/Classes/Equivalence.v | 112 ++++++++----- theories/Classes/Functions.v | 14 +- theories/Classes/Morphisms.v | 242 ++++++++++++++++------------ theories/Classes/Relations.v | 58 ++++--- theories/Classes/SetoidClass.v | 2 +- theories/Classes/SetoidDec.v | 20 +-- theories/Classes/SetoidTactics.v | 3 +- theories/Program/Basics.v | 29 ++-- theories/Program/FunctionalExtensionality.v | 1 + toplevel/classes.ml | 60 +++++-- toplevel/classes.mli | 8 +- toplevel/record.ml | 3 +- toplevel/vernacentries.ml | 6 +- toplevel/vernacexpr.ml | 5 +- 31 files changed, 507 insertions(+), 346 deletions(-) diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index 82fbe9c691..7cc43e4ce8 100644 --- a/contrib/interface/blast.ml +++ b/contrib/interface/blast.ml @@ -467,6 +467,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal = try [make_apply_entry (pf_env g') (project g') (true,false) + None (mkVar hid,htyp)] with Failure _ -> [] in diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index db8963554b..4d28a22a98 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1727,7 +1727,7 @@ let rec xlate_vernac = CT_id_ne_list(n1, names), dblist) | HintsExtern (n, c, t) -> CT_hint_extern(CT_int n, xlate_formula c, xlate_tactic t, dblist) - | HintsResolve l | HintsImmediate l -> + | HintsImmediate l -> let f1, formulas = match List.map xlate_formula l with a :: tl -> a, tl | _ -> failwith "" in @@ -1744,6 +1744,23 @@ let rec xlate_vernac = HintsResolve _ -> CT_hints_resolve(l', dblist) | HintsImmediate _ -> CT_hints_immediate(l', dblist) | _ -> assert false) + | HintsResolve l -> + let f1, formulas = match List.map xlate_formula (List.map snd l) with + a :: tl -> a, tl + | _ -> failwith "" in + let l' = CT_formula_ne_list(f1, formulas) in + if local then + (match h with + HintsResolve _ -> + CT_local_hints_resolve(l', dblist) + | HintsImmediate _ -> + CT_local_hints_immediate(l', dblist) + | _ -> assert false) + else + (match h with + HintsResolve _ -> CT_hints_resolve(l', dblist) + | HintsImmediate _ -> CT_hints_immediate(l', dblist) + | _ -> assert false) | HintsUnfold l -> let n1, names = match List.map loc_qualid_to_ct_ID l with n1 :: names -> n1, names @@ -2083,7 +2100,7 @@ let rec xlate_vernac = (* TypeClasses *) | VernacDeclareInstance _|VernacContext _| - VernacInstance (_, _, _)|VernacClass (_, _, _, _, _) -> + VernacInstance (_, _, _, _)|VernacClass (_, _, _, _, _) -> xlate_error "TODO: Type Classes commands" | VernacResetName id -> CT_reset (xlate_ident (snd id)) diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index e9c2ed4e52..2d1be640b1 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -148,8 +148,8 @@ let subtac (loc, command) = | VernacAssumption (stre,nl,l) -> vernac_assumption env isevars stre l nl - | VernacInstance (sup, is, props) -> - ignore(Subtac_classes.new_instance sup is props) + | VernacInstance (sup, is, props, pri) -> + ignore(Subtac_classes.new_instance sup is props pri) | VernacCoFixpoint (l, b) -> let _ = trace (str "Building cofixpoint") in diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml index e439021635..a2184a557e 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 = +let new_instance ctx (instid, bk, cl) props 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 @@ -211,11 +211,10 @@ let new_instance ctx (instid, bk, cl) props = let hook cst = let inst = { is_class = k; - is_name = id; + is_pri = pri; is_impl = cst; } in - Classes.add_instance_hint id; Impargs.declare_manual_implicits false (ConstRef cst) false imps; Typeclasses.add_instance inst in diff --git a/contrib/subtac/subtac_classes.mli b/contrib/subtac/subtac_classes.mli index 12a6e29549..c621f1516f 100644 --- a/contrib/subtac/subtac_classes.mli +++ b/contrib/subtac/subtac_classes.mli @@ -36,4 +36,5 @@ val new_instance : Topconstr.local_binder list -> typeclass_constraint -> binder_def_list -> + int option -> identifier diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index 5bcbf4db6c..730b12605e 100644 --- a/contrib/subtac/subtac_pretyping_F.ml +++ b/contrib/subtac/subtac_pretyping_F.ml @@ -572,11 +572,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | IsType -> (pretype_type empty_valcon env isevars lvar c).utj_val in let evd,_ = consider_remaining_unif_problems env !isevars in - let evd = nf_evar_defs evd in let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~all:false env (evars_of evd) evd in - let c' = nf_evar (evars_of evd) c' in - isevars := evd; - c' + isevars:=evd; + nf_evar (evars_of !isevars) c' (* TODO: comment faire remonter l'information si le typage a resolu des variables du sigma original. il faudrait que la fonction de typage diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 9972d9e248..68389c54a4 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -99,10 +99,34 @@ let lpar_id_coloneq = | _ -> raise Stream.Failure) | _ -> raise Stream.Failure) +let impl_ident = + Gram.Entry.of_parser "impl_ident" + (fun strm -> + match Stream.npeek 1 strm with + | [("IDENT",("wf"|"struct"|"measure"))] -> + raise Stream.Failure + | [("IDENT",s)] -> + Stream.junk strm; + Names.id_of_string s + | _ -> raise Stream.Failure) + +let ident_eq = + Gram.Entry.of_parser "ident_eq" + (fun strm -> + match Stream.npeek 1 strm with + | [("IDENT",s)] -> + (match Stream.npeek 2 strm with + | [_; ("", ":")] -> + Stream.junk strm; Stream.junk strm; + Names.id_of_string s + | _ -> raise Stream.Failure) + | _ -> raise Stream.Failure) + GEXTEND Gram GLOBAL: binder_constr lconstr constr operconstr sort global constr_pattern lconstr_pattern Constr.ident - binder binder_let binders_let delimited_binder_let delimited_binders_let typeclass_constraint pattern; + binder binder_let binders_let delimited_binder_let delimited_binders_let + binders_let_fixannot typeclass_constraint pattern; Constr.ident: [ [ id = Prim.ident -> id @@ -244,16 +268,16 @@ GEXTEND Gram | "cofix" -> false ] ] ; fix_decl: - [ [ id=identref; bl=LIST0 binder_let; ann=fixannot; ty=type_cstr; ":="; - c=operconstr LEVEL "200" -> (id,bl,ann,c,ty) ] ] - ; - fixannot: - [ [ "{"; IDENT "struct"; id=name; "}" -> (Some id, CStructRec) - | "{"; IDENT "wf"; rel=constr; id=OPT name; "}" -> (id, CWfRec rel) - | "{"; IDENT "measure"; rel=constr; id=OPT name; "}" -> (id, CMeasureRec rel) - | -> (None, CStructRec) - ] ] - ; + [ [ id=identref; bl=binders_let_fixannot; ty=type_cstr; ":="; + c=operconstr LEVEL "200" -> (id,fst bl,snd bl,c,ty) ] ] + ; +(* fixannot: *) +(* [ [ "{"; IDENT "struct"; id=name; "}" -> (Some id, CStructRec) *) +(* | "{"; IDENT "wf"; rel=constr; id=OPT name; "}" -> (id, CWfRec rel) *) +(* | "{"; IDENT "measure"; rel=constr; id=OPT name; "}" -> (id, CMeasureRec rel) *) +(* | -> (None, CStructRec) *) +(* ] ] *) +(* ; *) match_constr: [ [ "match"; ci=LIST1 case_item SEP ","; ty=OPT case_type; "with"; br=branches; "end" -> CCases(loc,ty,ci,br) ] ] @@ -332,53 +356,62 @@ GEXTEND Gram ctx @ bl | cl = LIST0 binder_let -> cl ] ] ; + binders_let_fixannot: + [ [ "{"; IDENT "struct"; id=name; "}" -> [], (Some id, CStructRec) + | "{"; IDENT "wf"; rel=constr; id=OPT name; "}" -> [], (id, CWfRec rel) + | "{"; IDENT "measure"; rel=constr; id=OPT name; "}" -> [], (id, CMeasureRec rel) + | b = binder_let; bl = binders_let_fixannot -> + b :: fst bl, snd bl + | -> [], (None, CStructRec) + ] ] + ; + binder_let: [ [ id=name -> LocalRawAssum ([id],Default Explicit,CHole (loc, None)) - | "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" -> + | "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" -> LocalRawAssum (id::idl,Default Explicit,c) - | "("; id=name; ":"; c=lconstr; ")" -> + | "("; id=name; ":"; c=lconstr; ")" -> LocalRawAssum ([id],Default Explicit,c) - | "`"; id=name; "`" -> + | "{"; id=name; "}" -> LocalRawAssum ([id],Default Implicit,CHole (loc, None)) - | "`"; id=name; idl=LIST1 name; ":"; c=lconstr; "`" -> + | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" -> LocalRawAssum (id::idl,Default Implicit,c) - | "`"; id=name; ":"; c=lconstr; "`" -> + | "{"; id=name; ":"; c=lconstr; "}" -> LocalRawAssum ([id],Default Implicit,c) - | "`"; id=name; idl=LIST1 name; "`" -> + | "{"; id=name; idl=LIST1 name; "}" -> LocalRawAssum (id::idl,Default Implicit,CHole (loc, None)) | "("; id=name; ":="; c=lconstr; ")" -> LocalRawDef (id,c) - | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> + | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t))) | "["; tc = typeclass_constraint_binder; "]" -> tc ] ] -(* | b = delimited_binder_let -> b ] ] *) ; delimited_binder_let: [ [ "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" -> LocalRawAssum (id::idl,Default Explicit,c) | "("; id=name; ":"; c=lconstr; ")" -> LocalRawAssum ([id],Default Explicit,c) - | "`"; id=name; "`" -> - LocalRawAssum ([id],Default Implicit,CHole (loc, None)) - | "`"; id=name; idl=LIST1 name; ":"; c=lconstr; "`" -> - LocalRawAssum (id::idl,Default Implicit,c) - | "`"; id=name; ":"; c=lconstr; "`" -> - LocalRawAssum ([id],Default Implicit,c) - | "`"; id=name; idl=LIST1 name; "`" -> - LocalRawAssum (id::idl,Default Implicit,CHole (loc, None)) | "("; id=name; ":="; c=lconstr; ")" -> LocalRawDef (id,c) | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t))) + | "{"; id=name; "}" -> + LocalRawAssum ([id],Default Implicit,CHole (loc, None)) + | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" -> + LocalRawAssum (id::idl,Default Implicit,c) + | "{"; id=name; ":"; c=lconstr; "}" -> + LocalRawAssum ([id],Default Implicit,c) + | "{"; id=name; idl=LIST1 name; "}" -> + LocalRawAssum (id::idl,Default Implicit,CHole (loc, None)) | "["; tc = typeclass_constraint_binder; "]" -> tc ] ] ; binder: [ [ id=name -> ([id],Default Explicit,CHole (loc, None)) | "("; idl=LIST1 name; ":"; c=lconstr; ")" -> (idl,Default Explicit,c) - | "`"; idl=LIST1 name; ":"; c=lconstr; "`" -> (idl,Default Implicit,c) + | "{"; idl=LIST1 name; ":"; c=lconstr; "}" -> (idl,Default Implicit,c) ] ] ; typeclass_constraint_binder: @@ -388,22 +421,22 @@ GEXTEND Gram ] ] ; typeclass_constraint: - [ [ id=identref ; cl = LIST0 typeclass_param -> - (loc, Anonymous), Explicit, CApp (loc, (None, mkIdentC (snd id)), cl) - | "?" ; id=identref ; cl = LIST0 typeclass_param -> - (loc, Anonymous), Implicit, CApp (loc, (None, mkIdentC (snd id)), cl) - | iid=identref ; ":" ; id=typeclass_name ; cl = LIST0 typeclass_param -> - (fst iid, Name (snd iid)), (fst id), CApp (loc, (None, mkIdentC (snd (snd id))), cl) + [ [ "!" ; qid=global ; cl = LIST0 typeclass_param -> + (loc, Anonymous), Explicit, CApp (loc, (None, mkRefC qid), cl) + | iid=ident_eq ; qid=typeclass_name ; cl = LIST0 typeclass_param -> + (loc, Name iid), (fst qid), CApp (loc, (None, mkRefC (snd qid)), cl) + | qid=global ; cl = LIST0 typeclass_param -> + (loc, Anonymous), Implicit, CApp (loc, (None, mkRefC qid), cl) ] ] ; typeclass_name: - [ [ id=identref -> (Explicit, id) - | "?"; id = identref -> (Implicit, id) + [ [ id=global -> (Implicit, id) + | "!"; id=global -> (Explicit, id) ] ] ; typeclass_param: - [ [ id = identref -> CRef (Libnames.Ident id), None + [ [ id = global -> CRef id, None | c = sort -> CSort (loc, c), None | id = lpar_id_coloneq; c=lconstr; ")" -> (c,Some (loc,ExplByName id)) diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 796636c0e0..32a2427ed1 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -105,7 +105,8 @@ GEXTEND Gram [ [ IDENT "Local" -> true | -> false ] ] ; hint: - [ [ IDENT "Resolve"; lc = LIST1 constr -> HintsResolve lc + [ [ IDENT "Resolve"; lc = LIST1 constr; n = OPT [ n = natural -> n ] -> + HintsResolve (List.map (fun x -> (n, x)) lc) | IDENT "Immediate"; lc = LIST1 constr -> HintsImmediate lc | IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 5c34f2e884..3b67407311 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -256,17 +256,19 @@ GEXTEND Gram ; (* (co)-fixpoints *) rec_definition: - [ [ id = ident; bl = LIST1 binder_let; - annot = rec_annotation; ty = type_cstr; + [ [ id = ident; b = binder_let; + bl = binders_let_fixannot; + ty = type_cstr; ":="; def = lconstr; ntn = decl_notation -> + let bl, annot = (b :: fst bl, snd bl) in let names = List.map snd (names_of_local_assums bl) in let ni = match fst annot with - Some id -> - (try Some (list_index0 (Name id) names) + Some (_, id) -> + (try Some (list_index0 id names) with Not_found -> Util.user_err_loc (loc,"Fixpoint", - Pp.str "No argument named " ++ Nameops.pr_id id)) + Pp.str "No argument named " ++ Nameops.pr_name id)) | None -> (* If there is only one argument, it is the recursive one, otherwise, we search the recursive index later *) @@ -279,13 +281,6 @@ GEXTEND Gram def = lconstr; ntn = decl_notation -> ((id,bl,ty,def),ntn) ] ] ; - rec_annotation: - [ [ "{"; IDENT "struct"; id=IDENT; "}" -> (Some (id_of_string id), CStructRec) - | "{"; IDENT "wf"; rel=constr; id=OPT IDENT; "}" -> (Option.map id_of_string id, CWfRec rel) - | "{"; IDENT "measure"; rel=constr; id=OPT IDENT; "}" -> (Option.map id_of_string id, CMeasureRec rel) - | -> (None, CStructRec) - ] ] - ; type_cstr: [ [ ":"; c=lconstr -> c | -> CHole (loc, None) ] ] @@ -495,9 +490,9 @@ GEXTEND Gram VernacContext c | IDENT "Instance"; sup = OPT [ l = delimited_binders_let ; "=>" -> l ]; - is = typeclass_constraint ; props = typeclass_field_defs -> + is = typeclass_constraint ; pri = OPT [ "|"; i = natural -> i ] ; props = typeclass_field_defs -> let sup = match sup with None -> [] | Some l -> l in - VernacInstance (sup, is, props) + VernacInstance (sup, is, props, pri) | IDENT "Existing"; IDENT "Instance"; is = identref -> VernacDeclareInstance is diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 68ddc19292..9976e07cc8 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -436,6 +436,7 @@ module Constr = let binder_let = Gram.Entry.create "constr:binder_let" let delimited_binder_let = Gram.Entry.create "constr:delimited_binder_let" let binders_let = Gram.Entry.create "constr:binders_let" + let binders_let_fixannot = Gram.Entry.create "constr:binders_let_fixannot" let delimited_binders_let = Gram.Entry.create "constr:delimited_binders_let" let typeclass_constraint = Gram.Entry.create "constr:typeclass_constraint" end diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index d5cffd35bd..4fb9d03594 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -165,6 +165,7 @@ module Constr : val binder_let : local_binder Gram.Entry.e val delimited_binder_let : local_binder Gram.Entry.e val binders_let : local_binder list Gram.Entry.e + val binders_let_fixannot : (local_binder list * (name located option * recursion_order_expr)) Gram.Entry.e val delimited_binders_let : local_binder list Gram.Entry.e val typeclass_constraint : (name located * binding_kind * constr_expr) Gram.Entry.e end diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 0daccbba53..92d56e078d 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -191,7 +191,10 @@ let pr_hints local db h pr_c pr_pat = let pph = match h with | HintsResolve l -> - str "Resolve " ++ prlist_with_sep sep pr_c l + str "Resolve " ++ prlist_with_sep sep + (fun (pri, c) -> pr_c c ++ + match pri with Some x -> spc () ++ str"(" ++ int x ++ str")" | None -> mt ()) + l | HintsImmediate l -> str"Immediate" ++ spc() ++ prlist_with_sep sep pr_c l | HintsUnfold l -> @@ -703,7 +706,7 @@ let rec pr_vernac = function prlist_with_sep (fun () -> str";" ++ spc()) (fun (lid,oc,c) -> pr_lident_constr ((if oc then str" :>" else str" :") ++ spc()) (lid,c)) props ) - | VernacInstance (sup, (instid, bk, cl), props) -> + | VernacInstance (sup, (instid, bk, cl), props, pri) -> hov 1 ( str"Instance" ++ spc () ++ pr_and_type_binders_arg sup ++ diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 3992648592..ee5acffd98 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -157,7 +157,7 @@ sig rawconstr -> unsafe_type_judgment val pretype_gen : - evar_defs ref -> env -> + evar_defs ref -> env -> var_map * (identifier * identifier option) list -> typing_constraint -> rawconstr -> constr @@ -667,11 +667,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct | IsType -> (pretype_type empty_valcon env evdref lvar c).utj_val in let evd,_ = consider_remaining_unif_problems env !evdref in - let evd = nf_evar_defs evd in let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~all:false env (evars_of evd) evd in - let c' = nf_evar (evars_of evd) c' in evdref := evd; - c' + nf_evar (evars_of evd) c' (* TODO: comment faire remonter l'information si le typage a resolu des variables du sigma original. il faudrait que la fonction de typage diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 7a95f9c35e..c18b0e0450 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -10,6 +10,7 @@ (*i*) open Names +open Libnames open Decl_kinds open Term open Sign @@ -48,12 +49,8 @@ type typeclasses = (identifier, typeclass) Gmap.t type instance = { is_class: typeclass; - is_name: identifier; (* Name of the instance *) -(* is_params: named_context; (\* Context of the parameters, instanciated *\) *) -(* is_super: named_context; (\* The corresponding superclasses *\) *) -(* is_defs: named_context; (\* Context of the definitions, instanciated *\) *) + is_pri: int option; is_impl: constant; -(* is_add_hint : unit -> unit; (\* Hook to add an hint for the instance *\) *) } type instances = (identifier, instance list) Gmap.t @@ -81,19 +78,20 @@ let _ = { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; Summary.init_function = init; - Summary.survive_module = true; + Summary.survive_module = false; Summary.survive_section = true } let gmap_merge old ne = Gmap.fold (fun k v acc -> Gmap.add k v acc) ne old -let gmap_list_merge old ne = +let gmap_list_merge old upd ne = let ne = Gmap.fold (fun k v acc -> let oldv = try Gmap.find k old with Not_found -> [] in let v' = List.fold_left (fun acc x -> - if not (List.exists (fun y -> y.is_name = x.is_name) v) then x :: acc else acc) + if not (List.exists (fun y -> y.is_impl = x.is_impl) v) then + (x :: acc) else acc) v oldv in Gmap.add k v' acc) ne Gmap.empty @@ -102,15 +100,24 @@ let gmap_list_merge old ne = let newv = try Gmap.find k ne with Not_found -> [] in let v' = List.fold_left (fun acc x -> - if not (List.exists (fun y -> y.is_name = x.is_name) acc) then x :: acc else acc) + if not (List.exists (fun y -> y.is_impl = x.is_impl) acc) then x :: acc else acc) newv v in Gmap.add k v' acc) old ne +let add_instance_hint_ref = ref (fun id pri -> assert false) +let register_add_instance_hint = (:=) add_instance_hint_ref +let add_instance_hint id = !add_instance_hint_ref id + +let qualid_of_con c = + Qualid (dummy_loc, shortest_qualid_of_global Idset.empty (ConstRef c)) + let cache (_, (cl, m, inst)) = classes := gmap_merge !classes cl; methods := gmap_merge !methods m; - instances := gmap_list_merge !instances inst + instances := gmap_list_merge !instances + (fun i -> add_instance_hint (qualid_of_con i.is_impl)) + inst open Libobject @@ -137,8 +144,11 @@ let subst (_,subst,(cl,m,inst)) = in let subst_inst classes insts = List.map (fun is -> - { is with is_class = Gmap.find is.is_class.cl_name classes; - is_impl = do_subst_con is.is_impl }) insts + let is' = + { is_class = Gmap.find is.is_class.cl_name classes; + is_pri = is.is_pri; + is_impl = do_subst_con is.is_impl } + in if is' = is then is else is') insts in let classes = Gmap.map subst_class cl in let instances = Gmap.map (subst_inst classes) inst in @@ -149,8 +159,9 @@ let discharge (_,(cl,m,inst)) = { cl with cl_impl = Lib.discharge_inductive cl.cl_impl } in let subst_inst classes insts = - List.map (fun is -> { is with is_impl = Lib.discharge_con is.is_impl; - is_class = Gmap.find is.is_class.cl_name classes; }) insts + List.map (fun is -> { is_impl = Lib.discharge_con is.is_impl; + is_pri = is.is_pri; + is_class = Gmap.find is.is_class.cl_name classes; }) insts in let classes = Gmap.map subst_class cl in let instances = Gmap.map (subst_inst classes) inst in @@ -202,8 +213,12 @@ let instances_of c = try Gmap.find c.cl_name !instances with Not_found -> [] let add_instance i = - instances := gmapl_add i.is_class.cl_name i !instances; - update () + try + let cl = Gmap.find i.is_class.cl_name !classes in + instances := gmapl_add cl.cl_name { i with is_class = cl } !instances; + add_instance_hint (qualid_of_con i.is_impl) i.is_pri; + update () + with Not_found -> unbound_class (Global.env ()) (dummy_loc, i.is_class.cl_name) open Libnames diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index f231c7406d..c06006ad05 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -10,6 +10,7 @@ (*i*) open Names +open Libnames open Decl_kinds open Term open Sign @@ -41,8 +42,8 @@ type typeclass = { type instance = { is_class: typeclass; - is_name: identifier; (* Name of the instance *) - is_impl: constant; + is_pri : int option; + is_impl: constant; } val instances : Libnames.reference -> instance list @@ -50,6 +51,9 @@ val typeclasses : unit -> typeclass list val add_class : typeclass -> unit val add_instance : instance -> unit +val register_add_instance_hint : (reference -> int option -> unit) -> unit +val add_instance_hint : reference -> int option -> unit + val class_info : identifier -> typeclass (* raises Not_found *) val class_of_inductive : inductive -> typeclass (* raises Not_found *) @@ -75,3 +79,10 @@ val substitution_of_named_context : val nf_substitution : evar_map -> substitution -> substitution val is_implicit_arg : hole_kind -> bool + + +val subst : 'a * Mod_subst.substitution * + ((Names.identifier, typeclass) Gmap.t * 'b * ('c, instance list) Gmap.t) -> + (Names.identifier, typeclass) Gmap.t * 'b * ('c, instance list) Gmap.t + +val qualid_of_con : Names.constant -> Libnames.reference diff --git a/tactics/auto.ml b/tactics/auto.ml index 92786e0896..fb7959a132 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -182,20 +182,20 @@ let try_head_pattern c = try head_pattern_bound c with BoundPattern -> error "Bound head variable" -let make_exact_entry (c,cty) = +let make_exact_entry pri (c,cty) = let cty = strip_outer_cast cty in match kind_of_term cty with | Prod (_,_,_) -> failwith "make_exact_entry" | _ -> (head_of_constr_reference (List.hd (head_constr cty)), - { pri=0; pat=None; code=Give_exact c }) + { pri=(match pri with Some pri -> pri | None -> 0); pat=None; code=Give_exact c }) let dummy_goal = {it = make_evar empty_named_context_val mkProp; sigma = empty} -let make_apply_entry env sigma (eapply,verbose) (c,cty) = +let make_apply_entry env sigma (eapply,verbose) pri (c,cty) = let cty = hnf_constr env sigma cty in match kind_of_term cty with | Prod _ -> @@ -211,12 +211,12 @@ let make_apply_entry env sigma (eapply,verbose) (c,cty) = warn (str "the hint: eapply " ++ pr_lconstr c ++ str " will only be used by eauto"); (hd, - { pri = nb_hyp cty + nmiss; + { pri = (match pri with None -> nb_hyp cty + nmiss | Some p -> p); pat = Some pat; code = ERes_pf(c,{ce with env=empty_env}) }) end else (hd, - { pri = nb_hyp cty; + { pri = (match pri with None -> nb_hyp cty | Some p -> p); pat = Some pat; code = Res_pf(c,{ce with env=empty_env}) }) | _ -> failwith "make_apply_entry" @@ -225,12 +225,12 @@ let make_apply_entry env sigma (eapply,verbose) (c,cty) = c is a constr cty is the type of constr *) -let make_resolves env sigma eap c = +let make_resolves env sigma eap pri c = let cty = type_of env sigma c in let ents = map_succeed (fun f -> f (c,cty)) - [make_exact_entry; make_apply_entry env sigma (eap,Flags.is_verbose())] + [make_exact_entry pri; make_apply_entry env sigma (eap,Flags.is_verbose()) pri] in if ents = [] then errorlabstrm "Hint" @@ -241,8 +241,8 @@ let make_resolves env sigma eap c = (* used to add an hypothesis to the local hint database *) let make_resolve_hyp env sigma (hname,_,htyp) = try - [make_apply_entry env sigma (true, false) - (mkVar hname, htyp)] + [make_apply_entry env sigma (true, false) None + (mkVar hname, htyp)] with | Failure _ -> [] | e when Logic.catchable_exception e -> anomaly "make_resolve_hyp" @@ -364,7 +364,7 @@ let add_resolves env sigma clist local dbnames = Lib.add_anonymous_leaf (inAutoHint (local,dbname, - List.flatten (List.map (make_resolves env sigma true) clist)))) + List.flatten (List.map (fun (x, y) -> make_resolves env sigma true x y) clist)))) dbnames @@ -408,7 +408,7 @@ let add_hints local dbnames0 h = let f = Constrintern.interp_constr sigma env in match h with | HintsResolve lhints -> - add_resolves env sigma (List.map f lhints) local dbnames + add_resolves env sigma (List.map (fun (pri, x) -> pri, f x) lhints) local dbnames | HintsImmediate lhints -> add_trivials env sigma (List.map f lhints) local dbnames | HintsUnfold lhints -> @@ -430,7 +430,7 @@ let add_hints local dbnames0 h = let isp = inductive_of_reference qid in let consnames = (snd (Global.lookup_inductive isp)).mind_consnames in let lcons = list_tabulate - (fun i -> mkConstruct (isp,i+1)) (Array.length consnames) in + (fun i -> None, mkConstruct (isp,i+1)) (Array.length consnames) in add_resolves env sigma lcons local dbnames in List.iter add_one lqid | HintsExtern (pri, patcom, tacexp) -> @@ -580,7 +580,7 @@ let unify_resolve (c,clenv) gls = let make_local_hint_db lems g = let sign = pf_hyps g in let hintlist = list_map_append (pf_apply make_resolve_hyp g) sign in - let hintlist' = list_map_append (pf_apply make_resolves g true) lems in + let hintlist' = list_map_append (pf_apply make_resolves g true None) lems in Hint_db.add_list hintlist' (Hint_db.add_list hintlist Hint_db.empty) (* Serait-ce possible de compiler d'abord la tactique puis de faire la @@ -741,7 +741,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal = let hintl = try [make_apply_entry (pf_env g') (project g') - (true,false) + (true,false) None (mkVar hid, htyp)] with Failure _ -> [] in @@ -833,7 +833,7 @@ let make_resolve_any_hyp env sigma (id,_,ty) = let ents = map_succeed (fun f -> f (mkVar id,ty)) - [make_exact_entry; make_apply_entry env sigma (true,false)] + [make_exact_entry None; make_apply_entry env sigma (true,false) None] in ents diff --git a/tactics/auto.mli b/tactics/auto.mli index ac4f126f38..de3814630d 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -72,19 +72,19 @@ val print_hint_ref : global_reference -> unit val print_hint_db_by_name : hint_db_name -> unit -(* [make_exact_entry hint_name (c, ctyp)]. +(* [make_exact_entry pri (c, ctyp)]. [c] is the term given as an exact proof to solve the goal; - [ctyp] is the type of [hc]. *) + [ctyp] is the type of [c]. *) -val make_exact_entry : constr * constr -> global_reference * pri_auto_tactic +val make_exact_entry : int option -> constr * constr -> global_reference * pri_auto_tactic -(* [make_apply_entry (eapply,verbose) (c,cty)]. +(* [make_apply_entry (eapply,verbose) pri (c,cty)]. [eapply] is true if this hint will be used only with EApply; [c] is the term given as an exact proof to solve the goal; [cty] is the type of [hc]. *) val make_apply_entry : - env -> evar_map -> bool * bool -> constr * constr + env -> evar_map -> bool * bool -> int option -> constr * constr -> global_reference * pri_auto_tactic (* A constr which is Hint'ed will be: @@ -95,7 +95,7 @@ val make_apply_entry : has missing arguments. *) val make_resolves : - env -> evar_map -> bool -> constr -> + env -> evar_map -> bool -> int option -> constr -> (global_reference * pri_auto_tactic) list (* [make_resolve_hyp hname htyp]. diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index bd525e0356..bf26021800 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -16,26 +16,27 @@ (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) +Require Export Coq.Program.Basics. Require Import Coq.Program.Program. + Require Import Coq.Classes.Init. +Require Export Coq.Classes.Relations. +Require Export Coq.Classes.Morphisms. Set Implicit Arguments. Unset Strict Implicit. -Require Export Coq.Classes.Relations. -Require Export Coq.Classes.Morphisms. - Definition equiv [ Equivalence A R ] : relation A := R. (** Shortcuts to make proof search possible (unification won't unfold equiv). *) -Definition equivalence_refl [ sa : Equivalence A ] : Reflexive equiv. +Definition equivalence_refl [ sa : ! Equivalence A ] : Reflexive equiv. Proof. eauto with typeclass_instances. Qed. -Definition equivalence_sym [ sa : Equivalence A ] : Symmetric equiv. +Definition equivalence_sym [ sa : ! Equivalence A ] : Symmetric equiv. Proof. eauto with typeclass_instances. Qed. -Definition equivalence_trans [ sa : Equivalence A ] : Transitive equiv. +Definition equivalence_trans [ sa : ! Equivalence A ] : Transitive equiv. Proof. eauto with typeclass_instances. Qed. (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *) @@ -43,20 +44,22 @@ Proof. eauto with typeclass_instances. Qed. (** Subset objects should be first coerced to their underlying type, but that notation doesn't work in the standard case then. *) (* Notation " x == y " := (equiv (x :>) (y :>)) (at level 70, no associativity) : type_scope. *) -Notation " x == y " := (equiv x y) (at level 70, no associativity) : type_scope. +Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope. + +Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : equiv_scope. -Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : type_scope. +Open Local Scope equiv_scope. (** Use the [clsubstitute] command which substitutes an equality in every hypothesis. *) Ltac clsubst H := match type of H with - ?x == ?y => clsubstitute H ; clear H x + ?x === ?y => clsubstitute H ; clear H x end. Ltac clsubst_nofail := match goal with - | [ H : ?x == ?y |- _ ] => clsubst H ; clsubst_nofail + | [ H : ?x === ?y |- _ ] => clsubst H ; clsubst_nofail | _ => idtac end. @@ -64,29 +67,62 @@ Ltac clsubst_nofail := Tactic Notation "clsubst" "*" := clsubst_nofail. -Lemma nequiv_equiv_trans : forall [ Equivalence A ] (x y z : A), x =/= y -> y == z -> x =/= z. +Ltac setoidreplace H t := + let Heq := fresh "Heq" in + cut(H) ; [ intro Heq ; setoid_rewrite Heq ; clear Heq | unfold equiv ; t ]. + +Ltac setoidreplacein H H' t := + let Heq := fresh "Heq" in + cut(H) ; [ intro Heq ; setoid_rewrite Heq in H' ; clear Heq | unfold equiv ; t ]. + +Tactic Notation "setoid_replace" constr(x) "with" constr(y) := + setoidreplace (x === y) idtac. + +Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) := + setoidreplacein (x === y) id idtac. + +Tactic Notation "setoid_replace" constr(x) "with" constr(y) "by" tactic(t) := + setoidreplace (x === y) ltac:t. + +Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) "by" tactic(t) := + setoidreplacein (x === y) id ltac:t. + +Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) := + setoidreplace (rel x y) idtac. + +Tactic Notation "setoid_replace" constr(x) "with" constr(y) + "using" "relation" constr(rel) "by" tactic(t) := + setoidreplace (rel x y) ltac:t. + +Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) + "using" "relation" constr(rel) := + setoidreplacein (rel x y) id idtac. + +Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) + "using" "relation" constr(rel) "by" tactic(t) := + setoidreplacein (rel x y) id ltac:t. + +Lemma nequiv_equiv_trans : forall [ ! Equivalence A ] (x y z : A), x =/= y -> y === z -> x =/= z. Proof with auto. intros; intro. - assert(z == y) by relation_sym. - assert(x == y) by relation_trans. + assert(z === y) by relation_sym. + assert(x === y) by relation_trans. contradiction. Qed. -Lemma equiv_nequiv_trans : forall [ Equivalence A ] (x y z : A), x == y -> y =/= z -> x =/= z. +Lemma equiv_nequiv_trans : forall [ ! Equivalence A ] (x y z : A), x === y -> y =/= z -> x =/= z. Proof. intros; intro. - assert(y == x) by relation_sym. - assert(y == z) by relation_trans. + assert(y === x) by relation_sym. + assert(y === z) by relation_trans. contradiction. Qed. -Open Scope type_scope. - Ltac equiv_simplify_one := match goal with - | [ H : ?x == ?x |- _ ] => clear H - | [ H : ?x == ?y |- _ ] => clsubst H - | [ |- ?x =/= ?y ] => let name:=fresh "Hneq" in intro name + | [ H : (?x === ?x)%type |- _ ] => clear H + | [ H : (?x === ?y)%type |- _ ] => clsubst H + | [ |- (?x =/= ?y)%type ] => let name:=fresh "Hneq" in intro name end. Ltac equiv_simplify := repeat equiv_simplify_one. @@ -101,13 +137,13 @@ Ltac equivify := repeat equivify_tac. (** Every equivalence relation gives rise to a morphism, as it is transitive and symmetric. *) -Instance [ sa : Equivalence A ] => equiv_morphism : ? Morphism (equiv ++> equiv ++> iff) equiv := +Instance [ sa : ! Equivalence ] => equiv_morphism : Morphism (equiv ++> equiv ++> iff) equiv := respect := respect. (** The partial application too as it is reflexive. *) -Instance [ sa : Equivalence A ] (x : A) => - equiv_partial_app_morphism : ? Morphism (equiv ++> iff) (equiv x) := +Instance [ sa : ! Equivalence A ] (x : A) => + equiv_partial_app_morphism : Morphism (equiv ++> iff) (equiv x) := respect := respect. Definition type_eq : relation Type := @@ -125,24 +161,11 @@ Ltac obligations_tactic ::= morphism_tac. using [iff_impl_id_morphism] if the proof is in [Prop] and [eq_arrow_id_morphism] if it is in Type. *) -Program Instance iff_impl_id_morphism : ? Morphism (iff ++> impl) id. +Program Instance iff_impl_id_morphism : + Morphism (iff ++> impl) id. (* Program Instance eq_arrow_id_morphism : ? Morphism (eq +++> arrow) id. *) -(* Definition compose_respect (A B C : Type) (R : relation (A -> B)) (R' : relation (B -> C)) *) -(* (x y : A -> C) : Prop := forall (f : A -> B) (g : B -> C), R f f -> R' g g. *) - -(* Program Instance (A B C : Type) (R : relation (A -> B)) (R' : relation (B -> C)) *) -(* [ mg : ? Morphism R' g ] [ mf : ? Morphism R f ] => *) -(* compose_morphism : ? Morphism (compose_respect R R') (g o f). *) - -(* Next Obligation. *) -(* Proof. *) -(* apply (respect (m0:=mg)). *) -(* apply (respect (m0:=mf)). *) -(* assumption. *) -(* Qed. *) - (** Partial equivs don't require reflexivity so we can build a partial equiv on the function space. *) Class PartialEquivalence (carrier : Type) (pequiv : relation carrier) := @@ -155,3 +178,14 @@ Class PartialEquivalence (carrier : Type) (pequiv : relation carrier) := (** Reset the default Program tactic. *) Ltac obligations_tactic ::= program_simpl. + +(** Default relation on a given support. *) + +Class DefaultRelation A := default_relation : relation A. + +(** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *) + +Instance [ ! Equivalence A R ] => + equivalence_default : DefaultRelation A | 4 := + default_relation := R. + diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v index 7942d36427..c08dee76f3 100644 --- a/theories/Classes/Functions.v +++ b/theories/Classes/Functions.v @@ -22,22 +22,22 @@ Require Export Coq.Classes.Morphisms. Set Implicit Arguments. Unset Strict Implicit. -Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Injective := +Class [ m : ! Morphism (A -> B) (RA ++> RB) f ] => Injective := injective : forall x y : A, RB (f x) (f y) -> RA x y. -Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Surjective := +Class [ m : ! Morphism (A -> B) (RA ++> RB) f ] => Surjective := surjective : forall y, exists x : A, RB y (f x). -Definition Bijective [ m : Morphism (A -> B) (RA ++> RB) (f : A -> B) ] := +Definition Bijective [ m : ! Morphism (A -> B) (RA ++> RB) (f : A -> B) ] := Injective m /\ Surjective m. -Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => MonoMorphism := +Class [ m : ! Morphism (A -> B) (eqA ++> eqB) ] => MonoMorphism := monic :> Injective m. -Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => EpiMorphism := +Class [ m : ! Morphism (A -> B) (eqA ++> eqB) ] => EpiMorphism := epic :> Surjective m. -Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => IsoMorphism := +Class [ m : ! Morphism (A -> B) (eqA ++> eqB) ] => IsoMorphism := monomorphism :> MonoMorphism m ; epimorphism :> EpiMorphism m. -Class [ m : Morphism (A -> A) (eqA ++> eqA), ? IsoMorphism m ] => AutoMorphism. +Class [ m : ! Morphism (A -> A) (eqA ++> eqA), IsoMorphism m ] => AutoMorphism. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 5d679d2c9a..fb0acb39ca 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -10,7 +10,7 @@ (* Typeclass-based morphisms with standard instances for equivalence relations. Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud + Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud 91405 Orsay, France *) (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) @@ -37,8 +37,8 @@ Definition respectful A (R : relation A) B (R' : relation B) : relation (A -> B) (** Notations reminiscent of the old syntax for declaring morphisms. *) -Notation " R ==> R' " := (@respectful _ R _ R') (right associativity, at level 20). Notation " R ++> R' " := (@respectful _ R _ R') (right associativity, at level 20). +Notation " R ==> R' " := (@respectful _ R _ R') (right associativity, at level 20). Notation " R --> R' " := (@respectful _ (inverse R) _ R') (right associativity, at level 20). (** A morphism on a relation [R] is an object respecting the relation (in its kernel). @@ -106,34 +106,87 @@ Qed. (* Program Definition arrow_morphism `A B` (m : A -> B) : Morphism (eq ++> eq) m. *) -(** Any binary morphism respecting some relations up to [iff] respects +(** Any morphism respecting some relations up to [iff] respects them up to [impl] in each way. Very important instances as we need [impl] morphisms at the top level when we rewrite. *) -Program Instance `A` (R : relation A) `B` (R' : relation B) - [ ? Morphism (R ++> R' ++> iff) m ] => +Class SubRelation A (R S : relation A) := + subrelation :> Morphism (S ==> R) (fun x => x). - iff_impl_binary_morphism : ? Morphism (R ++> R' ++> impl) m. +Instance iff_impl_subrelation : SubRelation Prop impl iff. +Proof. + constructor ; red ; intros. + tauto. +Qed. - Next Obligation. - Proof. - destruct respect with x y x0 y0 ; auto. - Qed. +Instance iff_inverse_impl_subrelation : SubRelation Prop (inverse impl) iff. +Proof. + constructor ; red ; intros. + tauto. +Qed. -Program Instance (A : Type) (R : relation A) `B` (R' : relation B) - [ ? Morphism (R ++> R' ++> iff) m ] => - iff_inverse_impl_binary_morphism : ? Morphism (R ++> R' ++> inverse impl) m. +Instance [ SubRelation A R₁ R₂ ] => + morphisms_subrelation : SubRelation (B -> A) (R ==> R₁) (R ==> R₂). +Proof. + constructor ; repeat red ; intros. + destruct subrelation. + red in respect0, H ; unfold id in *. + apply respect0. + apply H. + apply H0. +Qed. - Next Obligation. - Proof. - destruct respect with x y x0 y0 ; auto. - Qed. +(** High priority because it is always applicable and loops. *) + +Instance [ SubRelation A R₁ R₂, Morphism R₂ m ] => + subrelation_morphism : Morphism R₁ m | 4. +Proof. + destruct subrelation. + red in respect0. + unfold id in * ; apply respect0. + apply respect. +Qed. + +(* Program Instance `A` (R : relation A) `B` (R' : relation B) *) +(* [ ? Morphism (R ==> R' ==> iff) m ] => *) +(* iff_impl_binary_morphism : ? Morphism (R ==> R' ==> impl) m. *) + +(* Next Obligation. *) +(* Proof. *) +(* destruct respect with x y x0 y0 ; auto. *) +(* Qed. *) + +(* Program Instance `A` (R : relation A) `B` (R' : relation B) *) +(* [ ? Morphism (R ==> R' ==> iff) m ] => *) +(* iff_inverse_impl_binary_morphism : ? Morphism (R ==> R' ==> inverse impl) m. *) + +(* Next Obligation. *) +(* Proof. *) +(* destruct respect with x y x0 y0 ; auto. *) +(* Qed. *) + + +(* Program Instance [ Morphism (A -> Prop) (R ==> iff) m ] => *) +(* iff_impl_morphism : ? Morphism (R ==> impl) m. *) + +(* Next Obligation. *) +(* Proof. *) +(* destruct respect with x y ; auto. *) +(* Qed. *) + +(* Program Instance [ Morphism (A -> Prop) (R ==> iff) m ] => *) +(* iff_inverse_impl_morphism : ? Morphism (R ==> inverse impl) m. *) + +(* Next Obligation. *) +(* Proof. *) +(* destruct respect with x y ; auto. *) +(* Qed. *) (** Logical implication [impl] is a morphism for logical equivalence. *) -Program Instance iff_iff_iff_impl_morphism : ? Morphism (iff ++> iff ++> iff) impl. +Program Instance iff_iff_iff_impl_morphism : Morphism (iff ==> iff ==> iff) impl. -Lemma reflexive_impl_iff [ Symmetric A R, ? Morphism (R ++> impl) m ] : Morphism (R ==> iff) m. +Lemma reflexive_impl_iff [ ! Symmetric A R, Morphism (R ==> impl) m ] : Morphism (R ==> iff) m. Proof. intros. constructor. red ; intros. @@ -142,8 +195,8 @@ Qed. (** The complement of a relation conserves its morphisms. *) -Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => - complement_morphism : ? Morphism (RA ++> RA ++> iff) (complement R). +Program Instance {A} (RA : relation A) [ Morphism (RA ==> RA ==> iff) R ] => + complement_morphism : Morphism (RA ==> RA ==> iff) (complement R). Next Obligation. Proof. @@ -156,8 +209,8 @@ Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => (** The inverse too. *) -Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => - inverse_morphism : ? Morphism (RA ++> RA ++> iff) (inverse R). +Program Instance {A} (RA : relation A) [ Morphism (RA ==> RA ==> iff) R ] => + inverse_morphism : Morphism (RA ==> RA ==> iff) (inverse R). Next Obligation. Proof. @@ -165,8 +218,8 @@ Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => apply respect ; auto. Qed. -Program Instance (A B C : Type) [ ? Morphism (RA ++> RB ++> RC) (f : A -> B -> C) ] => - flip_morphism : ? Morphism (RB ++> RA ++> RC) (flip f). +Program Instance {A B C : Type} [ Morphism (RA ==> RB ==> RC) (f : A -> B -> C) ] => + flip_morphism : Morphism (RB ==> RA ==> RC) (flip f). Next Obligation. Proof. @@ -174,51 +227,13 @@ Program Instance (A B C : Type) [ ? Morphism (RA ++> RB ++> RC) (f : A -> B -> C apply respect ; auto. Qed. -(* Definition respectful' A (R : relation A) B (R' : relation B) (f : A -> B) : relation A := *) -(* fun x y => R x y -> R' (f x) (f y). *) - -(* Definition morphism_respectful' A R B (R' : relation B) (f : A -> B) *) -(* [ ? Morphism (R ++> R') f ] (x y : A) : respectful' R R' f x y. *) -(* intros. *) -(* destruct H. *) -(* red in respect0. *) -(* red. *) -(* apply respect0. *) -(* Qed. *) - -(* Existing Instance morphism_respectful'. *) - -(* Goal forall A [ Equivalence A (eqA : relation A) ] R [ ? Morphism (eqA ++> iff) m ] (x y : A) *) -(* [ ? Morphism (eqA ++> eqA) m' ] (m' : A -> A), eqA x y -> True. *) -(* intros. *) -(* cut (relation A) ; intros R'. *) -(* cut ((eqA ++> R') m' m') ; intros. *) -(* assert({ R' : relation A & Reflexive R' }). *) -(* econstructor. *) -(* typeclass_instantiation. *) - - -(* assert (exists R' : relation A, Morphism ((fun x y => eqA x y -> R' (m' x) (m' y)) ++> iff) m). *) -(* eapply ex_intro. *) -(* unfold respectful. *) -(* typeclass_instantiation. *) - - -(* assert (exists R', Morphism (R' ++> iff) m /\ Morphism (eqA ++> R') m'). *) -(* typeclass_instantiation. *) -(* Set Printing All. *) -(* Show Proof. *) - - -(* apply respect. *) - (** Partial applications are ok when a proof of refl is available. *) (** A proof of [R x x] is available. *) (* Program Instance (A : Type) R B (R' : relation B) *) -(* [ ? Morphism (R ++> R') m ] [ ? Morphism R x ] => *) -(* morphism_partial_app_morphism : ? Morphism R' (m x). *) +(* [ Morphism (R ==> R') m ] [ Morphism R x ] => *) +(* morphism_partial_app_morphism : Morphism R' (m x). *) (* Next Obligation. *) (* Proof with auto. *) @@ -229,24 +244,24 @@ Program Instance (A B C : Type) [ ? Morphism (RA ++> RB ++> RC) (f : A -> B -> C (** Morpshism declarations for partial applications. *) -Program Instance [ Transitive A R ] (x : A) => - trans_contra_inv_impl_morphism : ? Morphism (R --> inverse impl) (R x). +Program Instance [ ! Transitive A R ] (x : A) => + trans_contra_inv_impl_morphism : Morphism (R --> inverse impl) (R x). Next Obligation. Proof with auto. trans y... Qed. -Program Instance [ Transitive A R ] (x : A) => - trans_co_impl_morphism : ? Morphism (R ++> impl) (R x). +Program Instance [ ! Transitive A R ] (x : A) => + trans_co_impl_morphism : Morphism (R ==> impl) (R x). Next Obligation. Proof with auto. trans x0... Qed. -Program Instance [ Transitive A R, Symmetric A R ] (x : A) => - trans_sym_co_inv_impl_morphism : ? Morphism (R ++> inverse impl) (R x). +Program Instance [ ! Transitive A R, Symmetric R ] (x : A) => + trans_sym_co_inv_impl_morphism : Morphism (R ==> inverse impl) (R x). Next Obligation. Proof with auto. @@ -254,8 +269,8 @@ Program Instance [ Transitive A R, Symmetric A R ] (x : A) => sym... Qed. -Program Instance [ Transitive A R, Symmetric A R ] (x : A) => - trans_sym_contra_impl_morphism : ? Morphism (R --> impl) (R x). +Program Instance [ ! Transitive A R, Symmetric R ] (x : A) => + trans_sym_contra_impl_morphism : Morphism (R --> impl) (R x). Next Obligation. Proof with auto. @@ -264,7 +279,7 @@ Program Instance [ Transitive A R, Symmetric A R ] (x : A) => Qed. Program Instance [ Equivalence A R ] (x : A) => - equivalence_partial_app_morphism : ? Morphism (R ++> iff) (R x). + equivalence_partial_app_morphism : Morphism (R ==> iff) (R x). Next Obligation. Proof with auto. @@ -277,8 +292,8 @@ Program Instance [ Equivalence A R ] (x : A) => (** With symmetric relations, variance is no issue ! *) (* Program Instance (A B : Type) (R : relation A) (R' : relation B) *) -(* [ Morphism _ (R ++> R') m ] [ Symmetric A R ] => *) -(* sym_contra_morphism : ? Morphism (R --> R') m. *) +(* [ Morphism _ (R ==> R') m ] [ Symmetric A R ] => *) +(* sym_contra_morphism : Morphism (R --> R') m. *) (* Next Obligation. *) (* Proof with auto. *) @@ -289,8 +304,8 @@ Program Instance [ Equivalence A R ] (x : A) => (** [R] is reflexive, hence we can build the needed proof. *) Program Instance (A B : Type) (R : relation A) (R' : relation B) - [ ? Morphism (R ++> R') m ] [ Reflexive A R ] (x : A) => - reflexive_partial_app_morphism : ? Morphism R' (m x). + [ Morphism (R ==> R') m ] [ Reflexive R ] (x : A) => + reflexive_partial_app_morphism : Morphism R' (m x) | 3. Next Obligation. Proof with auto. @@ -302,8 +317,8 @@ Program Instance (A B : Type) (R : relation A) (R' : relation B) (** Every transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof to get an [R y z] goal. *) -Program Instance [ Transitive A R ] => - trans_co_eq_inv_impl_morphism : ? Morphism (R ++> eq ++> inverse impl) R. +Program Instance [ ! Transitive A R ] => + trans_co_eq_inv_impl_morphism : Morphism (R ==> eq ==> inverse impl) R. Next Obligation. Proof with auto. @@ -311,8 +326,8 @@ Program Instance [ Transitive A R ] => subst x0... Qed. -Program Instance [ Transitive A R ] => - trans_contra_eq_inv_impl_morphism : ? Morphism (R --> eq ++> impl) R. +Program Instance [ ! Transitive A R ] => + trans_contra_eq_impl_morphism : Morphism (R --> eq ==> impl) R. Next Obligation. Proof with auto. @@ -322,8 +337,8 @@ Program Instance [ Transitive A R ] => (** Every symmetric and transitive relation gives rise to an equivariant morphism. *) -Program Instance [ Transitive A R, Symmetric A R ] => - trans_sym_morphism : ? Morphism (R ++> R ++> iff) R. +Program Instance [ ! Transitive A R, Symmetric R ] => + trans_sym_morphism : Morphism (R ==> R ==> iff) R. Next Obligation. Proof with auto. @@ -334,7 +349,7 @@ Program Instance [ Transitive A R, Symmetric A R ] => Qed. Program Instance [ Equivalence A R ] => - equiv_morphism : ? Morphism (R ++> R ++> iff) R. + equiv_morphism : Morphism (R ==> R ==> iff) R. Next Obligation. Proof with auto. @@ -346,44 +361,65 @@ Program Instance [ Equivalence A R ] => (** In case the rewrite happens at top level. *) -Program Instance iff_inverse_impl_id : - ? Morphism (iff ++> inverse impl) id. +Program Instance iff_inverse_impl_id : + Morphism (iff ==> inverse impl) id. -Program Instance inverse_iff_inverse_impl_id : - ? Morphism (iff --> inverse impl) id. +Program Instance inverse_iff_inverse_impl_id : + Morphism (iff --> inverse impl) id. -Program Instance iff_impl_id : - ? Morphism (iff ++> impl) id. +Program Instance iff_impl_id : + Morphism (iff ==> impl) id. -Program Instance inverse_iff_impl_id : - ? Morphism (iff --> impl) id. +Program Instance inverse_iff_impl_id : + Morphism (iff --> impl) id. (** Standard instances for [iff] and [impl]. *) (** Logical conjunction. *) -Program Instance and_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) and. +Program Instance and_impl_iff_morphism : + Morphism (impl ==> iff ==> impl) and. -Program Instance and_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) and. +Program Instance and_iff_impl_morphism : + Morphism (iff ==> impl ==> impl) and. Program Instance and_inverse_impl_iff_morphism : - ? Morphism (inverse impl ++> iff ++> inverse impl) and. + Morphism (inverse impl ==> iff ==> inverse impl) and. Program Instance and_iff_inverse_impl_morphism : - ? Morphism (iff ++> inverse impl ++> inverse impl) and. + Morphism (iff ==> inverse impl ==> inverse impl) and. -Program Instance and_iff_morphism : ? Morphism (iff ++> iff ++> iff) and. +Program Instance and_iff_morphism : + Morphism (iff ==> iff ==> iff) and. (** Logical disjunction. *) -Program Instance or_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) or. +Program Instance or_impl_iff_morphism : + Morphism (impl ==> iff ==> impl) or. -Program Instance or_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) or. +Program Instance or_iff_impl_morphism : + Morphism (iff ==> impl ==> impl) or. Program Instance or_inverse_impl_iff_morphism : - ? Morphism (inverse impl ++> iff ++> inverse impl) or. + Morphism (inverse impl ==> iff ==> inverse impl) or. Program Instance or_iff_inverse_impl_morphism : - ? Morphism (iff ++> inverse impl ++> inverse impl) or. + Morphism (iff ==> inverse impl ==> inverse impl) or. + +Program Instance or_iff_morphism : + Morphism (iff ==> iff ==> iff) or. -Program Instance or_iff_morphism : ? Morphism (iff ++> iff ++> iff) or. +(** Coq functions are morphisms for leibniz equality, + applied only if really needed. *) + +Instance {A B : Type} (m : A -> B) => + any_eq_eq_morphism : Morphism (@Logic.eq A ==> @Logic.eq B) m | 4. +Proof. + red ; intros. subst ; reflexivity. +Qed. + +Instance {A : Type} (m : A -> Prop) => + any_eq_iff_morphism : Morphism (@Logic.eq A ==> iff) m | 4. +Proof. + red ; intros. subst ; reflexivity. +Qed. diff --git a/theories/Classes/Relations.v b/theories/Classes/Relations.v index 28f582c3d7..b14647d065 100644 --- a/theories/Classes/Relations.v +++ b/theories/Classes/Relations.v @@ -63,46 +63,46 @@ Hint Resolve @irreflexive : ord. (** We can already dualize all these properties. *) -Program Instance [ Reflexive A R ] => flip_reflexive : Reflexive A (flip R) := +Program Instance [ bla : ! Reflexive A R ] => flip_reflexive : Reflexive (flip R) := reflexive := reflexive (R:=R). -Program Instance [ Irreflexive A R ] => flip_irreflexive : Irreflexive A (flip R) := +Program Instance [ ! Irreflexive A R ] => flip_irreflexive : Irreflexive (flip R) := irreflexive := irreflexive (R:=R). -Program Instance [ Symmetric A R ] => flip_symmetric : Symmetric A (flip R). +Program Instance [ ! Symmetric A R ] => flip_symmetric : Symmetric (flip R). Solve Obligations using unfold flip ; program_simpl ; clapply symmetric. -Program Instance [ Asymmetric A R ] => flip_asymmetric : Asymmetric A (flip R). +Program Instance [ ! Asymmetric A R ] => flip_asymmetric : Asymmetric (flip R). Solve Obligations using program_simpl ; unfold flip in * ; intros ; clapply asymmetric. -Program Instance [ Transitive A R ] => flip_transitive : Transitive A (flip R). +Program Instance [ ! Transitive A R ] => flip_transitive : Transitive (flip R). Solve Obligations using unfold flip ; program_simpl ; clapply transitive. (** Have to do it again for Prop. *) -Program Instance [ Reflexive A (R : relation A) ] => inverse_reflexive : Reflexive A (inverse R) := +Program Instance [ ! Reflexive A (R : relation A) ] => inverse_reflexive : Reflexive (inverse R) := reflexive := reflexive (R:=R). -Program Instance [ Irreflexive A (R : relation A) ] => inverse_irreflexive : Irreflexive A (inverse R) := +Program Instance [ ! Irreflexive A (R : relation A) ] => inverse_irreflexive : Irreflexive (inverse R) := irreflexive := irreflexive (R:=R). -Program Instance [ Symmetric A (R : relation A) ] => inverse_symmetric : Symmetric A (inverse R). +Program Instance [ ! Symmetric A (R : relation A) ] => inverse_symmetric : Symmetric (inverse R). Solve Obligations using unfold inverse, flip ; program_simpl ; clapply symmetric. -Program Instance [ Asymmetric A (R : relation A) ] => inverse_asymmetric : Asymmetric A (inverse R). +Program Instance [ ! Asymmetric A (R : relation A) ] => inverse_asymmetric : Asymmetric (inverse R). Solve Obligations using program_simpl ; unfold inverse, flip in * ; intros ; clapply asymmetric. -Program Instance [ Transitive A (R : relation A) ] => inverse_transitive : Transitive A (inverse R). +Program Instance [ ! Transitive A (R : relation A) ] => inverse_transitive : Transitive (inverse R). Solve Obligations using unfold inverse, flip ; program_simpl ; clapply transitive. -Program Instance [ Reflexive A (R : relation A) ] => - reflexive_complement_irreflexive : Irreflexive A (complement R). +Program Instance [ ! Reflexive A (R : relation A) ] => + reflexive_complement_irreflexive : Irreflexive (complement R). Next Obligation. Proof. @@ -110,8 +110,8 @@ Program Instance [ Reflexive A (R : relation A) ] => apply reflexive. Qed. -Program Instance [ Irreflexive A (R : relation A) ] => - irreflexive_complement_reflexive : Reflexive A (complement R). +Program Instance [ ! Irreflexive A (R : relation A) ] => + irreflexive_complement_reflexive : Reflexive (complement R). Next Obligation. Proof. @@ -119,7 +119,7 @@ Program Instance [ Irreflexive A (R : relation A) ] => apply (irreflexive H). Qed. -Program Instance [ Symmetric A (R : relation A) ] => complement_symmetric : Symmetric A (complement R). +Program Instance [ ! Symmetric A (R : relation A) ] => complement_symmetric : Symmetric (complement R). Next Obligation. Proof. @@ -137,20 +137,20 @@ Ltac obligations_tactic ::= simpl_relation. (** Logical implication. *) -Program Instance impl_refl : ? Reflexive impl. -Program Instance impl_trans : ? Transitive impl. +Program Instance impl_refl : Reflexive impl. +Program Instance impl_trans : Transitive impl. (** Logical equivalence. *) -Program Instance iff_refl : ? Reflexive iff. -Program Instance iff_sym : ? Symmetric iff. -Program Instance iff_trans : ? Transitive iff. +Program Instance iff_refl : Reflexive iff. +Program Instance iff_sym : Symmetric iff. +Program Instance iff_trans : Transitive iff. (** Leibniz equality. *) -Program Instance eq_refl : ? Reflexive (@eq A). -Program Instance eq_sym : ? Symmetric (@eq A). -Program Instance eq_trans : ? Transitive (@eq A). +Program Instance eq_refl : Reflexive (@eq A). +Program Instance eq_sym : Symmetric (@eq A). +Program Instance eq_trans : Transitive (@eq A). (** ** General tactics to solve goals on relations. Each tactic comes in two flavors: @@ -298,9 +298,7 @@ Class PreOrder A (R : relation A) := preorder_refl :> Reflexive R ; preorder_trans :> Transitive R. -(** A [PreOrder] is both reflexive and transitive. *) - -(** The [PER] typeclass. *) +(** A partial equivalence relation is symmetric and transitive. *) Class PER (carrier : Type) (pequiv : relation carrier) := per_sym :> Symmetric pequiv ; @@ -332,13 +330,13 @@ Class Equivalence (carrier : Type) (equiv : relation carrier) := Class [ Equivalence A eqA ] => Antisymmetric (R : relation A) := antisymmetric : forall x y, R x y -> R y x -> eqA x y. -Program Instance [ eq : Equivalence A eqA, ? Antisymmetric eq R ] => - flip_antisymmetric : ? Antisymmetric eq (flip R). +Program Instance [ eq : Equivalence A eqA, Antisymmetric eq R ] => + flip_antisymmetric : Antisymmetric eq (flip R). Solve Obligations using unfold inverse, flip ; program_simpl ; eapply @antisymmetric ; eauto. -Program Instance [ eq : Equivalence A eqA, ? Antisymmetric eq (R : relation A) ] => - inverse_antisymmetric : ? Antisymmetric eq (inverse R). +Program Instance [ eq : Equivalence A eqA, Antisymmetric eq (R : relation A) ] => + inverse_antisymmetric : Antisymmetric eq (inverse R). Solve Obligations using unfold inverse, flip ; program_simpl ; eapply @antisymmetric ; eauto. diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index 571f65b627..9dd4f61812 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -149,7 +149,7 @@ Ltac obligations_tactic ::= morphism_tac. using [iff_impl_id_morphism] if the proof is in [Prop] and [eq_arrow_id_morphism] if it is in Type. *) -Program Instance iff_impl_id_morphism : ? Morphism (iff ++> impl) id. +Program Instance iff_impl_id_morphism : Morphism (iff ++> impl) id. (* Program Instance eq_arrow_id_morphism : ? Morphism (eq +++> arrow) id. *) diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index c385fc5b5c..8a435b4493 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -42,7 +42,7 @@ Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70) (** Use program to solve some obligations. *) -Definition swap_sumbool `A B` (x : { A } + { B }) : { B } + { A } := +Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } := match x with | left H => @right _ _ H | right H => @left _ _ H @@ -52,7 +52,7 @@ Require Import Coq.Program.Program. (** Invert the branches. *) -Program Definition nequiv_dec [ EqDec A ] (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y). +Program Definition nequiv_dec [ ! EqDec A ] (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y). (** Overloaded notation for inequality. *) @@ -60,10 +60,10 @@ Infix "=/=" := nequiv_dec (no associativity, at level 70). (** Define boolean versions, losing the logical information. *) -Definition equiv_decb [ EqDec A ] (x y : A) : bool := +Definition equiv_decb [ ! EqDec A ] (x y : A) : bool := if x == y then true else false. -Definition nequiv_decb [ EqDec A ] (x y : A) : bool := +Definition nequiv_decb [ ! EqDec A ] (x y : A) : bool := negb (equiv_decb x y). Infix "==b" := equiv_decb (no associativity, at level 70). @@ -78,15 +78,15 @@ Require Import Coq.Arith.Arith. Program Instance eq_setoid : Setoid A := equiv := eq ; setoid_equiv := eq_equivalence. -Program Instance nat_eq_eqdec : ? EqDec (@eq_setoid nat) := +Program Instance nat_eq_eqdec : EqDec (@eq_setoid nat) := equiv_dec := eq_nat_dec. Require Import Coq.Bool.Bool. -Program Instance bool_eqdec : ? EqDec (@eq_setoid bool) := +Program Instance bool_eqdec : EqDec (@eq_setoid bool) := equiv_dec := bool_dec. -Program Instance unit_eqdec : ? EqDec (@eq_setoid unit) := +Program Instance unit_eqdec : EqDec (@eq_setoid unit) := equiv_dec x y := left. Next Obligation. @@ -95,8 +95,8 @@ Program Instance unit_eqdec : ? EqDec (@eq_setoid unit) := reflexivity. Qed. -Program Instance [ ? EqDec (@eq_setoid A), ? EqDec (@eq_setoid B) ] => - prod_eqdec : ? EqDec (@eq_setoid (prod A B)) := +Program Instance [ EqDec (@eq_setoid A), EqDec (@eq_setoid B) ] => + prod_eqdec : EqDec (@eq_setoid (prod A B)) := equiv_dec x y := dest x as (x1, x2) in dest y as (y1, y2) in @@ -111,7 +111,7 @@ Program Instance [ ? EqDec (@eq_setoid A), ? EqDec (@eq_setoid B) ] => Require Import Coq.Program.FunctionalExtensionality. -Program Instance [ ? EqDec (@eq_setoid A) ] => bool_function_eqdec : ? EqDec (@eq_setoid (bool -> A)) := +Program Instance [ EqDec (@eq_setoid A) ] => bool_function_eqdec : EqDec (@eq_setoid (bool -> A)) := equiv_dec f g := if f true == g true then if f false == g false then left diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index 953296c28c..1277dcda9a 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -32,5 +32,4 @@ Axiom setoideq_eq : forall [ sa : Setoid a ] (x y : a), x == y -> x = y. Ltac setoid_extensionality := match goal with [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) (x:=X) (y:=Y)) - end. - + end. \ No newline at end of file diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index 8a3e5dccd9..ddc61a2dc0 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -21,11 +21,11 @@ Require Export Coq.Program.FunctionalExtensionality. Notation " 'λ' x : T , y " := (fun x:T => y) (at level 100, x,T,y at level 10, no associativity) : program_scope. -Open Scope program_scope. +Open Local Scope program_scope. -Definition id `A` := λ x : A, x. +Definition id {A} := λ x : A, x. -Definition compose `A B C` (g : B -> C) (f : A -> B) := λ x : A , g (f x). +Definition compose {A B C} (g : B -> C) (f : A -> B) := λ x : A , g (f x). Hint Unfold compose. @@ -58,11 +58,11 @@ Definition arrow (A B : Type) := A -> B. Definition impl (A B : Prop) : Prop := A -> B. -Notation " f '#' x " := (f x) (at level 100, x at level 200, only parsing). +(* Notation " f x " := (f x) (at level 100, x at level 200, only parsing) : program_scope. *) -Definition const `A B` (a : A) := fun x : B => a. +Definition const {A B} (a : A) := fun x : B => a. -Definition flip `A B C` (f : A -> B -> C) x y := f y x. +Definition flip {A B C} (f : A -> B -> C) x y := f y x. Lemma flip_flip : forall A B C (f : A -> B -> C), flip (flip f) = f. Proof. @@ -72,7 +72,7 @@ Proof. reflexivity. Qed. -Definition apply `A B` (f : A -> B) (x : A) := f x. +Definition apply {A B} (f : A -> B) (x : A) := f x. (** Notations for the unit type and value. *) @@ -94,10 +94,10 @@ Implicit Arguments right [[A] [B]]. (** Curryfication. *) -Definition curry `a b c` (f : a -> b -> c) (p : prod a b) : c := +Definition curry {a b c} (f : a -> b -> c) (p : prod a b) : c := let (x, y) := p in f x y. -Definition uncurry `a b c` (f : prod a b -> c) (x : a) (y : b) : c := +Definition uncurry {a b c} (f : prod a b -> c) (x : a) (y : b) : c := f (x, y). Lemma uncurry_curry : forall a b c (f : a -> b -> c), uncurry (curry f) = f. @@ -116,17 +116,6 @@ Proof. destruct x ; simpl ; reflexivity. Qed. -(** Useful implicits and notations for lists. *) - -Require Import Coq.Lists.List. - -Implicit Arguments nil [[A]]. -Implicit Arguments cons [[A]]. - -Notation " [] " := nil. -Notation " [ x ] " := (cons x nil). -Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..). - (** n-ary exists ! *) Notation " 'exists' x y , p" := (ex (fun x => (ex (fun y => p)))) diff --git a/theories/Program/FunctionalExtensionality.v b/theories/Program/FunctionalExtensionality.v index e890261e12..c2a6f3df6c 100644 --- a/theories/Program/FunctionalExtensionality.v +++ b/theories/Program/FunctionalExtensionality.v @@ -17,6 +17,7 @@ Require Import Coq.Program.Utils. Require Import Coq.Program.Wf. +Require Import Coq.Program.Equality. Set Implicit Arguments. Unset Strict Implicit. diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 1f2253d4f3..32803742a0 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -33,13 +33,27 @@ open Entries let hint_db = "typeclass_instances" -let add_instance_hint inst = - Auto.add_hints false [hint_db] - (Vernacexpr.HintsResolve [CAppExpl (dummy_loc, (None, Ident (dummy_loc, inst)), [])]) - -let declare_instance (_,id) = - add_instance_hint id - +let _ = + Typeclasses.register_add_instance_hint + (fun inst pri -> + Auto.add_hints false [hint_db] + (Vernacexpr.HintsResolve [pri, CAppExpl (dummy_loc, (None, inst), [])])) + +let declare_instance_constant con = + let instance = Typeops.type_of_constant (Global.env ()) con in + let _, r = decompose_prod_assum instance in + match class_of_constr r with + | Some tc -> add_instance { is_class = tc ; is_pri = None; is_impl = con } + | None -> error "Constant does not build instances of a declared type class" + +let declare_instance idl = + let con = + try (match global (Ident idl) with + | ConstRef x -> x + | _ -> raise Not_found) + with _ -> error "Instance definition not found" + in declare_instance_constant con + let mismatched_params env n m = mismatched_ctx_inst env Parameters n m (* let mismatched_defs env n m = mismatched_ctx_inst env Definitions n m *) let mismatched_props env n m = mismatched_ctx_inst env Properties n m @@ -110,7 +124,8 @@ let declare_implicit_proj c proj imps sub = aux 1 [] ctx in let expls = expls @ List.map (function (ExplByPos (i, n), f) -> (ExplByPos (succ len + i, n)), f | _ -> assert(false)) imps in - if sub then add_instance_hint (id_of_label (con_label proj)); + if sub then + declare_instance_constant proj; Impargs.declare_manual_implicits true (ConstRef proj) true expls let declare_implicits impls subs cl = @@ -263,7 +278,7 @@ let new_class id par ar sup props = let ce t = Evarutil.check_evars env0 Evd.empty isevars t in let kn = let idb = id_of_string ("Build_" ^ (string_of_id (snd id))) in - let params, subst = rel_of_named_context [] ctx_params (* @ ctx_super @ ctx_super_ctx) *) in + let params, subst = rel_of_named_context [] ctx_params in let fields, _ = rel_of_named_context subst ctx_props in List.iter (fun (_,c,t) -> ce t; match c with Some c -> ce c | None -> ()) (params @ fields); declare_structure env0 (snd id) idb params arity fields @@ -362,7 +377,7 @@ open Pp let ($$) g f = fun x -> g (f x) -let new_instance ctx (instid, bk, cl) props = +let new_instance ctx (instid, bk, cl) props pri hook = 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 @@ -472,13 +487,13 @@ let new_instance ctx (instid, bk, cl) props = let hook cst = let inst = { is_class = k; - is_name = id; + is_pri = pri; is_impl = cst; } in - add_instance_hint id; Impargs.declare_manual_implicits false (ConstRef cst) false imps; - Typeclasses.add_instance inst + Typeclasses.add_instance inst; + hook cst in let evm = Evd.evars_of (undefined_evars !isevars) in if evm = Evd.empty then @@ -518,7 +533,7 @@ let solve_by_tac env evd evar evi t = else evd, false else evd, false -let context l = +let context ?(hook=fun _ -> ()) l = let env = Global.env() in let isevars = ref (Evd.create_evar_defs Evd.empty) in let avoid = Termops.ids_of_context env in @@ -529,8 +544,21 @@ let context l = let sigma = Evd.evars_of !isevars in let fullctx = Evarutil.nf_named_context_evar sigma (l @ ctx) in List.iter (function (id,_,t) -> - Command.declare_one_assumption false (Local (* global *), Definitional) t - [] false (* inline *) (dummy_loc, id)) + if Lib.is_modtype () then + let cst = Declare.declare_internal_constant id + (ParameterEntry (t,false), IsAssumption Logical) + in + match class_of_constr t with + | Some tc -> + (add_instance { is_class = tc ; is_pri = None; is_impl = cst }); + hook (ConstRef cst) + | None -> () + else + (Command.declare_one_assumption false (Local (* global *), Definitional) t + [] false (* inline *) (dummy_loc, id); + match class_of_constr t with + None -> () + | Some tc -> hook (VarRef id))) (List.rev fullctx) open Libobject diff --git a/toplevel/classes.mli b/toplevel/classes.mli index d8f326698f..248ed8c956 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -43,11 +43,11 @@ val new_instance : local_binder list -> typeclass_constraint -> binder_def_list -> + int option -> + (constant -> unit) -> identifier - -val context : typeclass_context -> unit - -val add_instance_hint : identifier -> unit + +val context : ?hook:(Libnames.global_reference -> unit) -> typeclass_context -> unit val declare_instance : identifier located -> unit diff --git a/toplevel/record.ml b/toplevel/record.ml index 73e4e42f73..b94dffe1a0 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -138,7 +138,8 @@ let declare_projections indsp coers fields = let r = mkInd indsp in let rp = applist (r, extended_rel_list 0 paramdecls) in let paramargs = extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*) - let x = Termops.named_hd (Global.env()) r Anonymous in + let x = Name (next_ident_away mip.mind_typename (ids_of_context (Global.env()))) in + (* Termops.named_hd (Global.env()) r Anonymous *) let fields = instantiate_possibly_recursive_type indsp paramdecls fields in let lifted_fields = lift_rel_context 1 fields in let (_,kinds,sp_projs,_) = diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 770cc5ccf4..45a0f834ba 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -533,8 +533,8 @@ let vernac_identity_coercion stre id qids qidt = let vernac_class id par ar sup props = Classes.new_class id par ar sup props -let vernac_instance sup inst props = - ignore(Classes.new_instance sup inst props) +let vernac_instance sup inst props pri = + ignore(Classes.new_instance sup inst props pri (fun _ -> ())) let vernac_context l = Classes.context l @@ -1222,7 +1222,7 @@ let interp c = match c with (* Type classes *) | VernacClass (id, par, ar, sup, props) -> vernac_class id par ar sup props - | VernacInstance (sup, inst, props) -> vernac_instance sup inst props + | VernacInstance (sup, inst, props, pri) -> vernac_instance sup inst props pri | VernacContext sup -> vernac_context sup | VernacDeclareInstance id -> vernac_declare_instance id diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index a25cd09e74..ee0c42aa26 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -112,7 +112,7 @@ type comment = | CommentInt of int type hints = - | HintsResolve of constr_expr list + | HintsResolve of (int option * constr_expr) list | HintsImmediate of constr_expr list | HintsUnfold of reference list | HintsConstructors of reference list @@ -235,7 +235,8 @@ type vernac_expr = | VernacInstance of local_binder list * (* super *) typeclass_constraint * (* instance name, class name, params *) - (lident * lident list * constr_expr) list (* props *) + (lident * lident list * constr_expr) list * (* props *) + int option (* Priority *) | VernacContext of typeclass_context -- cgit v1.2.3