diff options
| -rw-r--r-- | tactics/rewrite.ml4 | 162 | ||||
| -rw-r--r-- | theories/Classes/Functions.v | 14 | ||||
| -rw-r--r-- | theories/Classes/Morphisms.v | 126 | ||||
| -rw-r--r-- | theories/Classes/Morphisms_Prop.v | 30 | ||||
| -rw-r--r-- | theories/Classes/Morphisms_Relations.v | 12 | ||||
| -rw-r--r-- | theories/Classes/SetoidClass.v | 18 | ||||
| -rw-r--r-- | theories/Classes/SetoidTactics.v | 8 | ||||
| -rw-r--r-- | theories/FSets/FMapFacts.v | 18 | ||||
| -rw-r--r-- | theories/FSets/FSetFacts.v | 2 | ||||
| -rw-r--r-- | theories/Setoids/Setoid.v | 2 |
10 files changed, 200 insertions, 192 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index df4851443..5f19d08de 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -55,13 +55,13 @@ let init_setoid () = if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then () else check_required_library ["Coq";"Setoids";"Setoid"] -let morphism_class = - lazy (class_info (Nametab.global (Qualid (dummy_loc, qualid_of_string "Coq.Classes.Morphisms.Morphism")))) +let proper_class = + lazy (class_info (Nametab.global (Qualid (dummy_loc, qualid_of_string "Coq.Classes.Morphisms.Proper")))) -let morphism_proxy_class = - lazy (class_info (Nametab.global (Qualid (dummy_loc, qualid_of_string "Coq.Classes.Morphisms.MorphismProxy")))) +let proper_proxy_class = + lazy (class_info (Nametab.global (Qualid (dummy_loc, qualid_of_string "Coq.Classes.Morphisms.ProperProxy")))) -let respect_proj = lazy (mkConst (Option.get (snd (List.hd (Lazy.force morphism_class).cl_projs)))) +let proper_proj = lazy (mkConst (Option.get (snd (List.hd (Lazy.force proper_class).cl_projs)))) let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) @@ -122,7 +122,7 @@ let coq_relationT = lazy (gen_constant ["Classes";"Relations"] "relationT") let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "Equivalence_Reflexive") let setoid_equiv = lazy (gen_constant ["Classes"; "SetoidClass"] "equiv") -let setoid_morphism = lazy (gen_constant ["Classes"; "SetoidClass"] "setoid_morphism") +let setoid_proper = lazy (gen_constant ["Classes"; "SetoidClass"] "setoid_proper") let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "Equivalence_Reflexive") let setoid_relation = lazy (gen_constant ["Classes"; "SetoidTactics"] "SetoidRelation") @@ -136,9 +136,9 @@ let arrow_morphism a b = let setoid_refl pars x = applistc (Lazy.force setoid_refl_proj) (pars @ [x]) -let morphism_type = lazy (constr_of_global (Lazy.force morphism_class).cl_impl) +let proper_type = lazy (constr_of_global (Lazy.force proper_class).cl_impl) -let morphism_proxy_type = lazy (constr_of_global (Lazy.force morphism_proxy_class).cl_impl) +let proper_proxy_type = lazy (constr_of_global (Lazy.force proper_proxy_class).cl_impl) let is_applied_setoid_relation t = match kind_of_term t with @@ -200,9 +200,9 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy. t, rel, [t, Some rel]) in aux env m cstrs -let morphism_proof env evars carrier relation x = +let proper_proof env evars carrier relation x = let goal = - mkApp (Lazy.force morphism_proxy_type, [| carrier ; relation; x |]) + mkApp (Lazy.force proper_proxy_type, [| carrier ; relation; x |]) in Evarutil.e_new_evar evars env goal let find_class_proof proof_type proof_method env evars carrier relation = @@ -421,7 +421,7 @@ let resolve_morphism env sigma oldt m ?(fnewt=fun x -> x) args args' cstr evars let cstrs = List.map (function None -> None | Some r -> Some (r.rew_car, r.rew_rel)) (Array.to_list morphobjs') in let appmtype', signature, sigargs = build_signature evars env appmtype cstrs cstr (fun (a,r) -> r) in let cl_args = [| appmtype' ; signature ; appm |] in - let app = mkApp (Lazy.force morphism_type, cl_args) in + let app = mkApp (Lazy.force proper_type, cl_args) in let morph = Evarutil.e_new_evar evars env app in morph, morph, sigargs, appm, morphobjs, morphobjs' in @@ -433,7 +433,7 @@ let resolve_morphism env sigma oldt m ?(fnewt=fun x -> x) args args' cstr evars | Some relation -> (match y with | None -> - let proof = morphism_proof env evars carrier relation x in + let proof = proper_proof env evars carrier relation x in [ proof ; x ; x ] @ acc, sigargs, x :: typeargs' | Some r -> [ r.rew_prf; r.rew_to; x ] @ acc, sigargs, r.rew_to :: typeargs') @@ -617,7 +617,7 @@ module Strategies = | Some r -> evars, r in let evars, proof = - let mty = mkApp (Lazy.force morphism_proxy_type, [| ty ; rel; t |]) in + let mty = mkApp (Lazy.force proper_proxy_type, [| ty ; rel; t |]) in Evarutil.new_evar evars env mty in Some (Some { rew_car = ty; rew_rel = rel; rew_from = t; rew_to = t; @@ -728,64 +728,58 @@ let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl = let eq = apply_strategy strat env sigma concl (Some (Lazy.lazy_from_val cstr)) evars in match eq with | Some (Some (p, (_, _, oldt, newt))) -> - (try - evars := Typeclasses.resolve_typeclasses env ~split:false ~fail:true !evars; - let p = Evarutil.nf_isevar !evars p in - let newt = Evarutil.nf_isevar !evars newt in - let undef = Evd.undefined_evars !evars in - let abs = Option.map (fun (x, y) -> Evarutil.nf_isevar !evars x, - Evarutil.nf_isevar !evars y) abs in - let rewtac = - match is_hyp with - | Some id -> - let term = - match abs with - | None -> p + (try + evars := Typeclasses.resolve_typeclasses env ~split:false ~fail:true !evars; + let p = Evarutil.nf_isevar !evars p in + let newt = Evarutil.nf_isevar !evars newt in + let undef = Evd.undefined_evars !evars in + let abs = Option.map (fun (x, y) -> Evarutil.nf_isevar !evars x, + Evarutil.nf_isevar !evars y) abs in + let rewtac = + match is_hyp with + | Some id -> + let term = + match abs with + | None -> p + | Some (t, ty) -> + mkApp (mkLambda (Name (id_of_string "lemma"), ty, p), [| t |]) + in + cut_replacing id newt + (fun x -> Tacmach.refine_no_check (mkApp (term, [| mkVar id |]))) + | None -> + (match abs with + | None -> + let name = next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in + tclTHENLAST + (Tacmach.internal_cut_no_check false name newt) + (tclTHEN (Tactics.revert [name]) (Tacmach.refine_no_check p)) | Some (t, ty) -> - mkApp (mkLambda (Name (id_of_string "lemma"), ty, p), [| t |]) - in - cut_replacing id newt - (fun x -> Tacmach.refine_no_check (mkApp (term, [| mkVar id |]))) - | None -> - (match abs with - | None -> - let name = next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in - tclTHENLAST - (Tacmach.internal_cut_no_check false name newt) - (tclTHEN (Tactics.revert [name]) (Tacmach.refine_no_check p)) - | Some (t, ty) -> - Tacmach.refine_no_check - (mkApp (mkLambda (Name (id_of_string "newt"), newt, - mkLambda (Name (id_of_string "lemma"), ty, - mkApp (p, [| mkRel 2 |]))), - [| mkMeta goal_meta; t |]))) - in - let evartac = - let evd = undef in - if not (evd = Evd.empty) then Refiner.tclEVARS (Evd.merge sigma evd) + Tacmach.refine_no_check + (mkApp (mkLambda (Name (id_of_string "newt"), newt, + mkLambda (Name (id_of_string "lemma"), ty, + mkApp (p, [| mkRel 2 |]))), + [| mkMeta goal_meta; t |]))) + in + let evartac = + if not (undef = Evd.empty) then Refiner.tclEVARS (Evd.merge sigma undef) else tclIDTAC - in tclTHENLIST [evartac; rewtac] gl + in tclTHENLIST [evartac; rewtac] gl with | Stdpp.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e))) | TypeClassError (env, (UnsatisfiableConstraints _ as e)) -> tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints." ++ fnl () ++ Himsg.explain_typeclass_error env e) gl) - (* | Not_found -> *) - (* tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints.") gl) *) | Some None -> tclFAIL 0 (str"setoid rewrite failed: no progress made") gl - | None -> -(* let {l2r=l2r; c1=x; c2=y} = !hypinfo in *) -(* raise (Pretype_errors.PretypeError *) -(* (pf_env gl, *) -(* Pretype_errors.NoOccurrenceFound ((if l2r then x else y), is_hyp))) *) - tclFAIL 0 (str"setoid rewrite failed") gl - + | None -> raise Not_found + let cl_rewrite_clause_strat strat clause gl = init_setoid (); let meta = Evarutil.new_meta() in let gl = { gl with sigma = Typeclasses.mark_unresolvables gl.sigma } in - cl_rewrite_clause_aux strat meta clause gl + try cl_rewrite_clause_aux strat meta clause gl + with Not_found -> + tclFAIL 0 (str"setoid rewrite failed: strategy failed") gl let cl_rewrite_clause l left2right occs clause gl = cl_rewrite_clause_strat (rewrite_with l left2right occs) clause gl @@ -1065,18 +1059,18 @@ let cHole = CHole (dummy_loc, None) open Entries open Libnames -let respect_projection r ty = +let proper_projection r ty = let ctx, inst = decompose_prod_assum ty in let mor, args = destApp inst in let instarg = mkApp (r, rel_vect 0 (List.length ctx)) in - let app = mkApp (Lazy.force respect_proj, + let app = mkApp (Lazy.force proper_proj, Array.append args [| instarg |]) in it_mkLambda_or_LetIn app ctx let declare_projection n instance_id r = let ty = Global.type_of_global r in let c = constr_of_global r in - let term = respect_projection c ty in + let term = proper_projection c ty in let typ = Typing.type_of (Global.env ()) Evd.empty term in let ctx, typ = decompose_prod_assum typ in let typ = @@ -1129,7 +1123,7 @@ let build_morphism_signature m = evars in let morph = - mkApp (Lazy.force morphism_type, [| t; sig_; m |]) + mkApp (Lazy.force proper_type, [| t; sig_; m |]) in let evd = Typeclasses.resolve_typeclasses ~fail:true ~onlyargs:false env !isevars in @@ -1144,10 +1138,10 @@ let default_morphism sign m = build_signature isevars env t (fst sign) (snd sign) (fun (ty, rel) -> rel) in let morph = - mkApp (Lazy.force morphism_type, [| t; sign; m |]) + mkApp (Lazy.force proper_type, [| t; sign; m |]) in let mor = resolve_one_typeclass env !isevars morph in - mor, respect_projection mor morph + mor, proper_projection mor morph let add_setoid binders a aeq t n = init_setoid (); @@ -1163,13 +1157,13 @@ let add_setoid binders a aeq t n = let add_morphism_infer m n = init_setoid (); - let instance_id = add_suffix n "_Morphism" in + let instance_id = add_suffix n "_Proper" in let instance = build_morphism_signature m in if Lib.is_modtype () then let cst = Declare.declare_internal_constant instance_id (Entries.ParameterEntry (instance,false), Decl_kinds.IsAssumption Decl_kinds.Logical) in - add_instance (Typeclasses.new_instance (Lazy.force morphism_class) None false cst); + add_instance (Typeclasses.new_instance (Lazy.force proper_class) None false cst); declare_projection n instance_id (ConstRef cst) else let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in @@ -1179,7 +1173,7 @@ let add_morphism_infer m n = (fun _ -> function Libnames.ConstRef cst -> add_instance (Typeclasses.new_instance - (Lazy.force morphism_class) None false cst); + (Lazy.force proper_class) None false cst); declare_projection n instance_id (ConstRef cst) | _ -> assert false); Pfedit.by (Tacinterp.interp <:tactic< Coq.Classes.SetoidTactics.add_morphism_tactic>>)) (); @@ -1187,11 +1181,11 @@ let add_morphism_infer m n = let add_morphism binders m s n = init_setoid (); - let instance_id = add_suffix n "_Morphism" in + let instance_id = add_suffix n "_Proper" in let instance = ((dummy_loc,Name instance_id), Explicit, CAppExpl (dummy_loc, - (None, Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Classes.Morphisms.Morphism")), + (None, Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper")), [cHole; s; m])) in let tac = Tacinterp.interp <:tactic<add_morphism_tactic>> in @@ -1278,12 +1272,17 @@ let apply_lemma gl (evm,c) cl l2r occs = let app = apply_rule hypinfo occs in let rec aux () = Strategies.choice app (subterm true general_rewrite_flags (fun env -> aux () env)) - in !hypinfo.abs, aux () + in !hypinfo, aux () let general_s_rewrite cl l2r occs c ~new_goals gl = let meta = Evarutil.new_meta() in - let abs, strat = apply_lemma gl c cl l2r occs in - cl_rewrite_clause_aux ~abs strat meta cl gl + let hypinfo, strat = apply_lemma gl c cl l2r occs in + try cl_rewrite_clause_aux ~abs:hypinfo.abs strat meta cl gl + with Not_found -> + let {l2r=l2r; c1=x; c2=y} = hypinfo in + raise (Pretype_errors.PretypeError + (pf_env gl, + Pretype_errors.NoOccurrenceFound ((if l2r then x else y), cl))) let general_s_rewrite_clause x = init_setoid (); @@ -1385,3 +1384,22 @@ END TACTIC EXTEND setoid_transitivity [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity t ] END + +let implify id gl = + let (_, b, ctype) = pf_get_hyp gl id in + let binders,concl = decompose_prod_assum ctype in + let ctype' = + match binders with + | (_, None, ty as hd) :: tl when not (dependent (mkRel 1) concl) -> + let env = Environ.push_rel_context tl (pf_env gl) in + let sigma = project gl in + let tyhd = Typing.type_of env sigma ty + and tyconcl = Typing.type_of (Environ.push_rel hd env) sigma concl in + let app = mkApp (arrow_morphism tyhd (subst1 mkProp tyconcl), [| ty; (subst1 mkProp concl) |]) in + it_mkProd_or_LetIn app tl + | _ -> ctype + in convert_hyp_no_check (id, b, ctype') gl + +TACTIC EXTEND implify +[ "implify" hyp(n) ] -> [ implify n ] +END diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v index 602b7b09d..b92e4d174 100644 --- a/theories/Classes/Functions.v +++ b/theories/Classes/Functions.v @@ -20,22 +20,22 @@ Require Import Coq.Classes.Morphisms. Set Implicit Arguments. Unset Strict Implicit. -Class Injective `(m : Morphism (A -> B) (RA ++> RB) f) : Prop := +Class Injective `(m : Proper (A -> B) (RA ++> RB) f) : Prop := injective : forall x y : A, RB (f x) (f y) -> RA x y. -Class Surjective `(m : Morphism (A -> B) (RA ++> RB) f) : Prop := +Class Surjective `(m : Proper (A -> B) (RA ++> RB) f) : Prop := surjective : forall y, exists x : A, RB y (f x). -Definition Bijective `(m : Morphism (A -> B) (RA ++> RB) (f : A -> B)) := +Definition Bijective `(m : Proper (A -> B) (RA ++> RB) (f : A -> B)) := Injective m /\ Surjective m. -Class MonoMorphism `(m : Morphism (A -> B) (eqA ++> eqB)) := +Class MonoMorphism `(m : Proper (A -> B) (eqA ++> eqB)) := monic :> Injective m. -Class EpiMorphism `(m : Morphism (A -> B) (eqA ++> eqB)) := +Class EpiMorphism `(m : Proper (A -> B) (eqA ++> eqB)) := epic :> Surjective m. -Class IsoMorphism `(m : Morphism (A -> B) (eqA ++> eqB)) := +Class IsoMorphism `(m : Proper (A -> B) (eqA ++> eqB)) := { monomorphism :> MonoMorphism m ; epimorphism :> EpiMorphism m }. -Class AutoMorphism `(m : Morphism (A -> A) (eqA ++> eqA)) {I : IsoMorphism m}. +Class AutoMorphism `(m : Proper (A -> A) (eqA ++> eqA)) {I : IsoMorphism m}. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index e2ab8b118..65d6687ea 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -24,15 +24,15 @@ Require Export Coq.Classes.RelationClasses. (** * Morphisms. - We now turn to the definition of [Morphism] and declare standard instances. + We now turn to the definition of [Proper] and declare standard instances. These will be used by the [setoid_rewrite] tactic later. *) -(** A morphism on a relation [R] is an object respecting the relation (in its kernel). +(** A morphism for a relation [R] is a proper element of the relation. The relation [R] will be instantiated by [respectful] and [A] by an arrow type for usual morphisms. *) -Class Morphism {A} (R : relation A) (m : A) : Prop := - respect : R m m. +Class Proper {A} (R : relation A) (m : A) : Prop := + proper : R m m. (** Respectful morphisms. *) @@ -56,10 +56,10 @@ Definition respectful {A B : Type} Delimit Scope signature_scope with signature. -Arguments Scope Morphism [type_scope signature_scope]. +Arguments Scope Proper [type_scope signature_scope]. Arguments Scope respectful [type_scope type_scope signature_scope signature_scope]. -Module MorphismNotations. +Module ProperNotations. Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature)) (right associativity, at level 55) : signature_scope. @@ -70,9 +70,9 @@ Module MorphismNotations. Notation " R --> R' " := (@respectful _ _ (inverse (R%signature)) (R'%signature)) (right associativity, at level 55) : signature_scope. -End MorphismNotations. +End ProperNotations. -Export MorphismNotations. +Export ProperNotations. Open Local Scope signature_scope. @@ -113,30 +113,30 @@ Program Instance respectful_per `(PER A (R : relation A), PER B (R' : relation B (** Subrelations induce a morphism on the identity. *) -Instance subrelation_id_morphism `(subrelation A R₁ R₂) : Morphism (R₁ ==> R₂) id. +Instance subrelation_id_proper `(subrelation A R₁ R₂) : Proper (R₁ ==> R₂) id. Proof. firstorder. Qed. (** The subrelation property goes through products as usual. *) -Instance morphisms_subrelation_respectful `(subl : subrelation A R₂ R₁, subr : subrelation B S₁ S₂) : +Instance subrelation_respectful `(subl : subrelation A R₂ R₁, subr : subrelation B S₁ S₂) : subrelation (R₁ ==> S₁) (R₂ ==> S₂). Proof. simpl_relation. apply subr. apply H. apply subl. apply H0. Qed. (** And of course it is reflexive. *) -Instance morphisms_subrelation_refl : ! subrelation A R R. +Instance subrelation_refl : ! subrelation A R R. Proof. simpl_relation. Qed. -(** [Morphism] is itself a covariant morphism for [subrelation]. *) +(** [Proper] is itself a covariant morphism for [subrelation]. *) -Lemma subrelation_morphism `(mor : Morphism A R₁ m, unc : Unconvertible (relation A) R₁ R₂, - sub : subrelation A R₁ R₂) : Morphism R₂ m. +Lemma subrelation_proper `(mor : Proper A R₁ m, unc : Unconvertible (relation A) R₁ R₂, + sub : subrelation A R₁ R₂) : Proper R₂ m. Proof. intros. apply sub. apply mor. Qed. -Instance morphism_subrelation_morphism : - Morphism (subrelation ++> @eq _ ==> impl) (@Morphism A). +Instance proper_subrelation_proper : + Proper (subrelation ++> @eq _ ==> impl) (@Proper A). Proof. reduce. subst. firstorder. Qed. (** We use an external tactic to manage the application of subrelation, which is otherwise @@ -149,11 +149,11 @@ Inductive normalization_done : Prop := did_normalization. Ltac subrelation_tac := match goal with | [ _ : subrelation_done |- _ ] => fail 1 - | [ |- @Morphism _ _ _ ] => let H := fresh "H" in - set(H:=did_subrelation) ; eapply @subrelation_morphism + | [ |- @Proper _ _ _ ] => let H := fresh "H" in + set(H:=did_subrelation) ; eapply @subrelation_proper end. -Hint Extern 5 (@Morphism _ _ _) => subrelation_tac : typeclass_instances. +Hint Extern 5 (@Proper _ _ _) => subrelation_tac : typeclass_instances. (** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *) @@ -167,11 +167,11 @@ Instance pointwise_subrelation {A} `(sub : subrelation B R R') : subrelation (pointwise_relation A R) (pointwise_relation A R') | 4. Proof. reduce. unfold pointwise_relation in *. apply sub. apply H. Qed. -(** The complement of a relation conserves its morphisms. *) +(** The complement of a relation conserves its proper elements. *) -Program Instance complement_morphism - `(mR : Morphism (A -> A -> Prop) (RA ==> RA ==> iff) R) : - Morphism (RA ==> RA ==> iff) (complement R). +Program Instance complement_proper + `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) : + Proper (RA ==> RA ==> iff) (complement R). Next Obligation. Proof. @@ -182,9 +182,9 @@ Program Instance complement_morphism (** The [inverse] too, actually the [flip] instance is a bit more general. *) -Program Instance flip_morphism - `(mor : Morphism (A -> B -> C) (RA ==> RB ==> RC) f) : - Morphism (RB ==> RA ==> RC) (flip f). +Program Instance flip_proper + `(mor : Proper (A -> B -> C) (RA ==> RB ==> RC) f) : + Proper (RB ==> RA ==> RC) (flip f). Next Obligation. Proof. @@ -195,7 +195,7 @@ Program Instance flip_morphism contravariant in the first argument, covariant in the second. *) Program Instance trans_contra_co_morphism - `(Transitive A R) : Morphism (R --> R ++> impl) R. + `(Transitive A R) : Proper (R --> R ++> impl) R. Next Obligation. Proof with auto. @@ -203,10 +203,10 @@ Program Instance trans_contra_co_morphism transitivity x0... Qed. -(** Morphism declarations for partial applications. *) +(** Proper declarations for partial applications. *) Program Instance trans_contra_inv_impl_morphism - `(Transitive A R) : Morphism (R --> inverse impl) (R x) | 3. + `(Transitive A R) : Proper (R --> inverse impl) (R x) | 3. Next Obligation. Proof with auto. @@ -214,7 +214,7 @@ Program Instance trans_contra_inv_impl_morphism Qed. Program Instance trans_co_impl_morphism - `(Transitive A R) : Morphism (R ==> impl) (R x) | 3. + `(Transitive A R) : Proper (R ==> impl) (R x) | 3. Next Obligation. Proof with auto. @@ -222,7 +222,7 @@ Program Instance trans_co_impl_morphism Qed. Program Instance trans_sym_co_inv_impl_morphism - `(PER A R) : Morphism (R ==> inverse impl) (R x) | 2. + `(PER A R) : Proper (R ==> inverse impl) (R x) | 2. Next Obligation. Proof with auto. @@ -230,7 +230,7 @@ Program Instance trans_sym_co_inv_impl_morphism Qed. Program Instance trans_sym_contra_impl_morphism - `(PER A R) : Morphism (R --> impl) (R x) | 2. + `(PER A R) : Proper (R --> impl) (R x) | 2. Next Obligation. Proof with auto. @@ -238,7 +238,7 @@ Program Instance trans_sym_contra_impl_morphism Qed. Program Instance per_partial_app_morphism - `(PER A R) : Morphism (R ==> iff) (R x) | 1. + `(PER A R) : Proper (R ==> iff) (R x) | 1. Next Obligation. Proof with auto. @@ -252,7 +252,7 @@ Program Instance per_partial_app_morphism to get an [R y z] goal. *) Program Instance trans_co_eq_inv_impl_morphism - `(Transitive A R) : Morphism (R ==> (@eq A) ==> inverse impl) R | 2. + `(Transitive A R) : Proper (R ==> (@eq A) ==> inverse impl) R | 2. Next Obligation. Proof with auto. @@ -261,7 +261,7 @@ Program Instance trans_co_eq_inv_impl_morphism (** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *) -Program Instance PER_morphism `(PER A R) : Morphism (R ==> R ==> iff) R | 1. +Program Instance PER_morphism `(PER A R) : Proper (R ==> R ==> iff) R | 1. Next Obligation. Proof with auto. @@ -274,8 +274,8 @@ Program Instance PER_morphism `(PER A R) : Morphism (R ==> R ==> iff) R | 1. Lemma symmetric_equiv_inverse `(Symmetric A R) : relation_equivalence R (flip R). Proof. firstorder. Qed. -Program Instance compose_morphism A B C R₀ R₁ R₂ : - Morphism ((R₁ ==> R₂) ==> (R₀ ==> R₁) ==> (R₀ ==> R₂)) (@compose A B C). +Program Instance compose_proper A B C R₀ R₁ R₂ : + Proper ((R₁ ==> R₂) ==> (R₀ ==> R₁) ==> (R₀ ==> R₂)) (@compose A B C). Next Obligation. Proof. @@ -293,7 +293,7 @@ Proof. simpl_relation. Qed. (** [respectful] is a morphism for relation equivalence. *) Instance respectful_morphism : - Morphism (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B). + Proper (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B). Proof. reduce. unfold respectful, relation_equivalence, predicate_equivalence in * ; simpl in *. @@ -313,25 +313,25 @@ Qed. (** Every element in the carrier of a reflexive relation is a morphism for this relation. We use a proxy class for this case which is used internally to discharge reflexivity constraints. The [Reflexive] instance will almost always be used, but it won't apply in general to any kind of - [Morphism (A -> B) _ _] goal, making proof-search much slower. A cleaner solution would be to be able + [Proper (A -> B) _ _] goal, making proof-search much slower. A cleaner solution would be to be able to set different priorities in different hint bases and select a particular hint database for resolution of a type class constraint.*) -Class MorphismProxy {A} (R : relation A) (m : A) : Prop := - respect_proxy : R m m. +Class ProperProxy {A} (R : relation A) (m : A) : Prop := + proper_proxy : R m m. -Instance reflexive_morphism_proxy - `(Reflexive A R) (x : A) : MorphismProxy R x | 1. +Instance reflexive_proper_proxy + `(Reflexive A R) (x : A) : ProperProxy R x | 1. Proof. firstorder. Qed. -Instance morphism_morphism_proxy - `(Morphism A R x) : MorphismProxy R x | 2. +Instance proper_proper_proxy + `(Proper A R x) : ProperProxy R x | 2. Proof. firstorder. Qed. (** [R] is Reflexive, hence we can build the needed proof. *) -Lemma Reflexive_partial_app_morphism `(Morphism (A -> B) (R ==> R') m, MorphismProxy A R x) : - Morphism R' (m x). +Lemma Reflexive_partial_app_morphism `(Proper (A -> B) (R ==> R') m, ProperProxy A R x) : + Proper R' (m x). Proof. simpl_relation. Qed. Class Params {A : Type} (of : A) (arity : nat). @@ -367,7 +367,7 @@ Ltac partial_application_tactic := | [ _ : subrelation_done |- _ ] => fail 1 | [ _ : normalization_done |- _ ] => fail 1 | [ _ : @Params _ _ _ |- _ ] => fail 1 - | [ |- @Morphism ?T _ (?m ?x) ] => + | [ |- @Proper ?T _ (?m ?x) ] => match goal with | [ _ : PartialApplication |- _ ] => eapply @Reflexive_partial_app_morphism @@ -378,7 +378,7 @@ Ltac partial_application_tactic := end end. -Hint Extern 4 (@Morphism _ _ _) => partial_application_tactic : typeclass_instances. +Hint Extern 4 (@Proper _ _ _) => partial_application_tactic : typeclass_instances. Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B), relation_equivalence (inverse (R ==> R')) (inverse R ==> inverse R'). @@ -429,13 +429,13 @@ Hint Extern 1 (subrelation _ (flip _)) => eapply @inverse2 : typeclass_instances (** Once we have normalized, we will apply this instance to simplify the problem. *) -Definition morphism_inverse_morphism `(mor : Morphism A R m) : Morphism (inverse R) m := mor. +Definition proper_inverse_proper `(mor : Proper A R m) : Proper (inverse R) m := mor. -Hint Extern 2 (@Morphism _ (flip _) _) => eapply @morphism_inverse_morphism : typeclass_instances. +Hint Extern 2 (@Proper _ (flip _) _) => eapply @proper_inverse_proper : typeclass_instances. (** Bootstrap !!! *) -Instance morphism_morphism : Morphism (relation_equivalence ==> @eq _ ==> iff) (@Morphism A). +Instance proper_proper : Proper (relation_equivalence ==> @eq _ ==> iff) (@Proper A). Proof. simpl_relation. reduce in H. @@ -446,37 +446,37 @@ Proof. apply H0. Qed. -Lemma morphism_releq_morphism `(Normalizes A R R', Morphism _ R' m) : Morphism R m. +Lemma proper_releq_proper `(Normalizes A R R', Proper _ R' m) : Proper R m. Proof. intros. - pose respect as r. + pose proper as r. pose normalizes as norm. setoid_rewrite norm. assumption. Qed. -Ltac morphism_normalization := +Ltac proper_normalization := match goal with | [ _ : subrelation_done |- _ ] => fail 1 | [ _ : normalization_done |- _ ] => fail 1 - | [ |- @Morphism _ _ _ ] => let H := fresh "H" in - set(H:=did_normalization) ; eapply @morphism_releq_morphism + | [ |- @Proper _ _ _ ] => let H := fresh "H" in + set(H:=did_normalization) ; eapply @proper_releq_proper end. -Hint Extern 6 (@Morphism _ _ _) => morphism_normalization : typeclass_instances. +Hint Extern 6 (@Proper _ _ _) => proper_normalization : typeclass_instances. (** Every reflexive relation gives rise to a morphism, only for immediately solving goals without variables. *) -Lemma reflexive_morphism `{Reflexive A R} (x : A) - : Morphism R x. +Lemma reflexive_proper `{Reflexive A R} (x : A) + : Proper R x. Proof. firstorder. Qed. -Ltac morphism_reflexive := +Ltac proper_reflexive := match goal with | [ _ : normalization_done |- _ ] => fail 1 | [ _ : subrelation_done |- _ ] => fail 1 - | [ |- @Morphism _ _ _ ] => eapply @reflexive_morphism + | [ |- @Proper _ _ _ ] => eapply @reflexive_proper end. -Hint Extern 7 (@Morphism _ _ _) => morphism_reflexive : typeclass_instances. +Hint Extern 7 (@Proper _ _ _) => proper_reflexive : typeclass_instances. diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v index 3bbd56cfd..b62e7d413 100644 --- a/theories/Classes/Morphisms_Prop.v +++ b/theories/Classes/Morphisms_Prop.v @@ -6,10 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Morphism instances for propositional connectives. +(* [Proper] instances for propositional connectives. Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud + Institution: LRI, CNRS UMR 8623 - Université Paris Sud 91405 Orsay, France *) Require Import Coq.Classes.Morphisms. @@ -21,34 +21,34 @@ Require Import Coq.Program.Tactics. (** Logical negation. *) Program Instance not_impl_morphism : - Morphism (impl --> impl) not. + Proper (impl --> impl) not. Program Instance not_iff_morphism : - Morphism (iff ++> iff) not. + Proper (iff ++> iff) not. (** Logical conjunction. *) Program Instance and_impl_morphism : - Morphism (impl ==> impl ==> impl) and. + Proper (impl ==> impl ==> impl) and. Program Instance and_iff_morphism : - Morphism (iff ==> iff ==> iff) and. + Proper (iff ==> iff ==> iff) and. (** Logical disjunction. *) Program Instance or_impl_morphism : - Morphism (impl ==> impl ==> impl) or. + Proper (impl ==> impl ==> impl) or. Program Instance or_iff_morphism : - Morphism (iff ==> iff ==> iff) or. + Proper (iff ==> iff ==> iff) or. (** 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 : Proper (iff ==> iff ==> iff) impl. (** Morphisms for quantifiers *) -Program Instance ex_iff_morphism {A : Type} : Morphism (pointwise_relation A iff ==> iff) (@ex A). +Program Instance ex_iff_morphism {A : Type} : Proper (pointwise_relation A iff ==> iff) (@ex A). Next Obligation. Proof. @@ -62,7 +62,7 @@ Program Instance ex_iff_morphism {A : Type} : Morphism (pointwise_relation A iff Qed. Program Instance ex_impl_morphism {A : Type} : - Morphism (pointwise_relation A impl ==> impl) (@ex A). + Proper (pointwise_relation A impl ==> impl) (@ex A). Next Obligation. Proof. @@ -71,7 +71,7 @@ Program Instance ex_impl_morphism {A : Type} : Qed. Program Instance ex_inverse_impl_morphism {A : Type} : - Morphism (pointwise_relation A (inverse impl) ==> inverse impl) (@ex A). + Proper (pointwise_relation A (inverse impl) ==> inverse impl) (@ex A). Next Obligation. Proof. @@ -80,7 +80,7 @@ Program Instance ex_inverse_impl_morphism {A : Type} : Qed. Program Instance all_iff_morphism {A : Type} : - Morphism (pointwise_relation A iff ==> iff) (@all A). + Proper (pointwise_relation A iff ==> iff) (@all A). Next Obligation. Proof. @@ -89,7 +89,7 @@ Program Instance all_iff_morphism {A : Type} : Qed. Program Instance all_impl_morphism {A : Type} : - Morphism (pointwise_relation A impl ==> impl) (@all A). + Proper (pointwise_relation A impl ==> impl) (@all A). Next Obligation. Proof. @@ -98,7 +98,7 @@ Program Instance all_impl_morphism {A : Type} : Qed. Program Instance all_inverse_impl_morphism {A : Type} : - Morphism (pointwise_relation A (inverse impl) ==> inverse impl) (@all A). + Proper (pointwise_relation A (inverse impl) ==> inverse impl) (@all A). Next Obligation. Proof. diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v index 4654e654a..b603a2e41 100644 --- a/theories/Classes/Morphisms_Relations.v +++ b/theories/Classes/Morphisms_Relations.v @@ -18,11 +18,11 @@ Require Import Coq.Program.Program. (** Morphisms for relations *) -Instance relation_conjunction_morphism : Morphism (relation_equivalence (A:=A) ==> +Instance relation_conjunction_morphism : Proper (relation_equivalence (A:=A) ==> relation_equivalence ==> relation_equivalence) relation_conjunction. Proof. firstorder. Qed. -Instance relation_disjunction_morphism : Morphism (relation_equivalence (A:=A) ==> +Instance relation_disjunction_morphism : Proper (relation_equivalence (A:=A) ==> relation_equivalence ==> relation_equivalence) relation_disjunction. Proof. firstorder. Qed. @@ -31,22 +31,22 @@ Instance relation_disjunction_morphism : Morphism (relation_equivalence (A:=A) = Require Import List. Lemma predicate_equivalence_pointwise (l : list Type) : - Morphism (@predicate_equivalence l ==> pointwise_lifting iff l) id. + Proper (@predicate_equivalence l ==> pointwise_lifting iff l) id. Proof. do 2 red. unfold predicate_equivalence. auto. Qed. Lemma predicate_implication_pointwise (l : list Type) : - Morphism (@predicate_implication l ==> pointwise_lifting impl l) id. + Proper (@predicate_implication l ==> pointwise_lifting impl l) id. Proof. do 2 red. unfold predicate_implication. auto. Qed. (** The instanciation at relation allows to rewrite applications of relations [R x y] to [R' x y] *) (* when [R] and [R'] are in [relation_equivalence]. *) Instance relation_equivalence_pointwise : - Morphism (relation_equivalence ==> pointwise_relation A (pointwise_relation A iff)) id. + Proper (relation_equivalence ==> pointwise_relation A (pointwise_relation A iff)) id. Proof. intro. apply (predicate_equivalence_pointwise (cons A (cons A nil))). Qed. Instance subrelation_pointwise : - Morphism (subrelation ==> pointwise_relation A (pointwise_relation A impl)) id. + Proper (subrelation ==> pointwise_relation A (pointwise_relation A impl)) id. Proof. intro. apply (predicate_implication_pointwise (cons A (cons A nil))). Qed. diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index 3e4e58ace..063b42928 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -119,21 +119,11 @@ Ltac setoidify := repeat setoidify_tac. (** Every setoid relation gives rise to a morphism, in fact every partial setoid does. *) -Program Instance setoid_morphism `(sa : Setoid A) : Morphism (equiv ++> equiv ++> iff) equiv := - respect. +Program Instance setoid_morphism `(sa : Setoid A) : Proper (equiv ++> equiv ++> iff) equiv := + proper. -Program Instance setoid_partial_app_morphism `(sa : Setoid A) (x : A) : Morphism (equiv ++> iff) (equiv x) := - respect. - -Ltac morphism_tac := try red ; unfold arrow ; intros ; program_simpl ; try tauto. - -Ltac obligation_tactic ::= morphism_tac. - -(** These are morphisms used to rewrite at the top level of a proof, - 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 setoid_partial_app_morphism `(sa : Setoid A) (x : A) : Proper (equiv ++> iff) (equiv x) := + proper. (** Partial setoids don't require reflexivity so we can build a partial setoid on the function space. *) diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index 9e66ef2a0..226dfbd22 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -19,7 +19,7 @@ Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop. Require Export Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions. Require Import Coq.Classes.Equivalence Coq.Program.Basics. -Export MorphismNotations. +Export ProperNotations. Set Implicit Arguments. Unset Strict Implicit. @@ -165,9 +165,9 @@ Ltac red_subst_eq_morphism concl := | _ => idtac end. -Ltac destruct_morphism := +Ltac destruct_proper := match goal with - | [ |- @Morphism ?A ?R ?m ] => red + | [ |- @Proper ?A ?R ?m ] => red end. Ltac reverse_arrows x := @@ -179,7 +179,7 @@ Ltac reverse_arrows x := Ltac default_add_morphism_tactic := unfold flip ; intros ; - (try destruct_morphism) ; + (try destruct_proper) ; match goal with | [ |- (?x ==> ?y) _ _ ] => red_subst_eq_morphism (x ==> y) ; reverse_arrows (x ==> y) end. diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 58e81f357..1ff9fbf20 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -1034,8 +1034,8 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). (** This is more convenient than a [compat_op eqke ...]. In fact, every [compat_op], [compat_bool], etc, should - become a [Morphism] someday. *) - Hypothesis Comp : Morphism (E.eq==>Leibniz==>eqA==>eqA) f. + become a [Proper] someday. *) + Hypothesis Comp : Proper (E.eq==>Leibniz==>eqA==>eqA) f. Lemma fold_init : forall m i i', eqA i i' -> eqA (fold f m i) (fold f m i'). @@ -1272,7 +1272,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). Section Specs. Variable f : key -> elt -> bool. - Hypothesis Hf : Morphism (E.eq==>Leibniz==>Leibniz) f. + Hypothesis Hf : Proper (E.eq==>Leibniz==>Leibniz) f. Lemma filter_iff : forall m k e, MapsTo k e (filter f m) <-> MapsTo k e m /\ f k e = true. @@ -1365,7 +1365,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). Section Partition. Variable f : key -> elt -> bool. - Hypothesis Hf : Morphism (E.eq==>Leibniz==>Leibniz) f. + Hypothesis Hf : Proper (E.eq==>Leibniz==>Leibniz) f. Lemma partition_iff_1 : forall m m1 k e, m1 = fst (partition f m) -> @@ -1494,7 +1494,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). Lemma Partition_fold : forall (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA)(f:key->elt->A->A), - Morphism (E.eq==>Leibniz==>eqA==>eqA) f -> + Proper (E.eq==>Leibniz==>eqA==>eqA) f -> transpose_neqkey eqA f -> forall m m1 m2 i, Partition m m1 m2 -> @@ -1557,7 +1557,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). Equal m1 (fst (partition f m)) /\ Equal m2 (snd (partition f m)). Proof. intros m m1 m2 Hm f. - assert (Hf : Morphism (E.eq==>Leibniz==>Leibniz) f). + assert (Hf : Proper (E.eq==>Leibniz==>Leibniz) f). intros k k' Hk e e' _; unfold f; rewrite Hk; auto. set (m1':= fst (partition f m)). set (m2':= snd (partition f m)). @@ -2150,7 +2150,7 @@ Module OrdProperties (M:S). Lemma fold_Equal : forall m1 m2 (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA) (f:key->elt->A->A)(i:A), - Morphism (E.eq==>Leibniz==>eqA==>eqA) f -> + Proper (E.eq==>Leibniz==>eqA==>eqA) f -> Equal m1 m2 -> eqA (fold f m1 i) (fold f m2 i). Proof. @@ -2164,7 +2164,7 @@ Module OrdProperties (M:S). Lemma fold_Add_Above : forall m1 m2 x e (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA) (f:key->elt->A->A)(i:A), - Morphism (E.eq==>Leibniz==>eqA==>eqA) f -> + Proper (E.eq==>Leibniz==>eqA==>eqA) f -> Above x m1 -> Add x e m1 m2 -> eqA (fold f m2 i) (f x e (fold f m1 i)). Proof. @@ -2181,7 +2181,7 @@ Module OrdProperties (M:S). Lemma fold_Add_Below : forall m1 m2 x e (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA) (f:key->elt->A->A)(i:A), - Morphism (E.eq==>Leibniz==>eqA==>eqA) f -> + Proper (E.eq==>Leibniz==>eqA==>eqA) f -> Below x m1 -> Add x e m1 m2 -> eqA (fold f m2 i) (fold f m1 (f x e i)). Proof. diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v index c99107939..a96def34a 100644 --- a/theories/FSets/FSetFacts.v +++ b/theories/FSets/FSetFacts.v @@ -424,7 +424,7 @@ Add Relation t Subset transitivity proved by Subset_trans as SubsetSetoid. -Instance In_s_m : Morphisms.Morphism (E.eq ==> Subset ++> Basics.impl) In | 1. +Instance In_s_m : Morphisms.Proper (E.eq ==> Subset ++> Basics.impl) In | 1. Proof. simpl_relation. eauto with set. Qed. diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index 8d241d894..9eef2bc1d 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -10,7 +10,7 @@ Require Export Coq.Classes.SetoidTactics. -Export Morphisms.MorphismNotations. +Export Morphisms.ProperNotations. (** For backward compatibility *) |