diff options
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 |