diff options
| -rw-r--r-- | tactics/class_tactics.ml4 | 60 | ||||
| -rw-r--r-- | theories/Classes/Equivalence.v | 16 | ||||
| -rw-r--r-- | theories/Classes/Functions.v | 5 | ||||
| -rw-r--r-- | theories/Classes/Morphisms.v | 66 | ||||
| -rw-r--r-- | theories/Classes/RelationClasses.v | 98 | ||||
| -rw-r--r-- | theories/Classes/SetoidAxioms.v | 2 | ||||
| -rw-r--r-- | theories/Classes/SetoidClass.v | 16 | ||||
| -rw-r--r-- | theories/Classes/SetoidTactics.v | 4 | ||||
| -rw-r--r-- | theories/Setoids/Setoid.v | 3 |
9 files changed, 158 insertions, 112 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 79faadca6..a3baa1abb 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -1,3 +1,4 @@ +(* -*- compile-command: "make -C .. bin/coqtop.byte" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -423,6 +424,12 @@ let morphism_class = let respect_proj = lazy (mkConst (List.hd (Lazy.force morphism_class).cl_projs)) +let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) + +let try_find_reference dir s = + let sp = Libnames.make_path (make_dir ("Coq"::dir)) (id_of_string s) in + constr_of_global (Nametab.absolute_reference sp) + let gen_constant dir s = Coqlib.gen_constant "Class_setoid" dir s let coq_proj1 = lazy(gen_constant ["Init"; "Logic"] "proj1") let coq_proj2 = lazy(gen_constant ["Init"; "Logic"] "proj2") @@ -431,14 +438,14 @@ let impl = lazy (gen_constant ["Program"; "Basics"] "impl") let arrow = lazy (gen_constant ["Program"; "Basics"] "arrow") let coq_id = lazy (gen_constant ["Program"; "Basics"] "id") -let reflexive_type = lazy (gen_constant ["Classes"; "RelationClasses"] "reflexive") -let reflexive_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "reflexivity") +let reflexive_type = lazy (try_find_reference ["Classes"; "RelationClasses"] "Reflexive") +let reflexive_proof = lazy (try_find_reference ["Classes"; "RelationClasses"] "reflexivity") -let symmetric_type = lazy (gen_constant ["Classes"; "RelationClasses"] "symmetric") -let symmetric_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "symmetry") +let symmetric_type = lazy (try_find_reference ["Classes"; "RelationClasses"] "Symmetric") +let symmetric_proof = lazy (try_find_reference ["Classes"; "RelationClasses"] "symmetry") -let transitive_type = lazy (gen_constant ["Classes"; "RelationClasses"] "transitive") -let transitive_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "transitivity") +let transitive_type = lazy (try_find_reference ["Classes"; "RelationClasses"] "Transitive") +let transitive_proof = lazy (try_find_reference ["Classes"; "RelationClasses"] "transitivity") let inverse = lazy (gen_constant ["Classes"; "RelationClasses"] "inverse") let complement = lazy (gen_constant ["Classes"; "RelationClasses"] "complement") @@ -524,13 +531,13 @@ let reflexivity_proof_evar env evars carrier relation x = (* mkCast (mkMeta meta, DEFAULTcast, mkApp (relation, [| x; x |])) *) let find_class_proof proof_type proof_method env carrier relation = - let goal = - mkApp (Lazy.force proof_type, [| carrier ; relation |]) - in - try - let inst = resolve_one_typeclass env goal in - mkApp (Lazy.force proof_method, [| carrier ; relation ; inst |]) - with e when Logic.catchable_exception e -> raise Not_found + try + let goal = + mkApp (Lazy.force proof_type, [| carrier ; relation |]) + in + let inst = resolve_one_typeclass env goal in + mkApp (Lazy.force proof_method, [| carrier ; relation ; inst |]) + with e when Logic.catchable_exception e -> raise Not_found let reflexive_proof env = find_class_proof reflexive_type reflexive_proof env let symmetric_proof env = find_class_proof symmetric_type symmetric_proof env @@ -986,17 +993,17 @@ let init_setoid () = check_required_library ["Coq";"Setoids";"Setoid"] let declare_instance_refl a aeq n lemma = - let instance = declare_instance a aeq (add_suffix n "_refl") "Coq.Classes.RelationClasses.reflexive" + let instance = declare_instance a aeq (add_suffix n "_refl") "Coq.Classes.RelationClasses.Reflexive" in anew_instance instance [((dummy_loc,id_of_string "reflexivity"),[],lemma)] let declare_instance_sym a aeq n lemma = - let instance = declare_instance a aeq (add_suffix n "_sym") "Coq.Classes.RelationClasses.symmetric" + let instance = declare_instance a aeq (add_suffix n "_sym") "Coq.Classes.RelationClasses.Symmetric" in anew_instance instance [((dummy_loc,id_of_string "symmetry"),[],lemma)] let declare_instance_trans a aeq n lemma = - let instance = declare_instance a aeq (add_suffix n "_trans") "Coq.Classes.RelationClasses.transitive" + let instance = declare_instance a aeq (add_suffix n "_trans") "Coq.Classes.RelationClasses.Transitive" in anew_instance instance [((dummy_loc,id_of_string "transitivity"),[],lemma)] @@ -1302,6 +1309,15 @@ let relation_of_constr c = mkApp (f, relargs), args | _ -> error "Not an applied relation" +let is_loaded d = + let d' = List.map id_of_string d in + let dir = make_dirpath (List.rev d') in + Library.library_is_loaded dir + +let try_loaded f gl = + if is_loaded ["Coq";"Classes";"RelationClasses"] then f gl + else tclFAIL 0 (str"You need to require Coq.Classes.RelationClasses first") gl + let setoid_reflexivity gl = let env = pf_env gl in let rel, args = relation_of_constr (pf_concl gl) in @@ -1311,6 +1327,9 @@ let setoid_reflexivity gl = tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared reflexive relation") gl +(* let setoid_reflexivity gl = *) +(* try_loaded setoid_reflexivity gl *) + let setoid_symmetry gl = let env = pf_env gl in let rel, args = relation_of_constr (pf_concl gl) in @@ -1319,6 +1338,9 @@ let setoid_symmetry gl = with Not_found -> tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared symmetric relation") gl + +(* let setoid_symmetry gl = *) +(* try_loaded setoid_symmetry gl *) let setoid_transitivity c gl = let env = pf_env gl in @@ -1331,6 +1353,9 @@ let setoid_transitivity c gl = tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared transitive relation") gl +(* let setoid_transitivity c gl = *) +(* try_loaded (setoid_transitivity c) gl *) + let setoid_symmetry_in id gl = let ctype = pf_type_of gl (mkVar id) in let binders,concl = Sign.decompose_prod_assum ctype in @@ -1349,6 +1374,9 @@ let setoid_symmetry_in id gl = tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ] ] gl +(* let setoid_symmetry_in h gl = *) +(* try_loaded (setoid_symmetry_in h) gl *) + let _ = Tactics.register_setoid_reflexivity setoid_reflexivity let _ = Tactics.register_setoid_symmetry setoid_symmetry let _ = Tactics.register_setoid_symmetry_in setoid_symmetry_in diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index dd9cfbca5..58aef9a7b 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -19,13 +19,15 @@ Require Export Coq.Program.Basics. Require Import Coq.Program.Tactics. Require Import Coq.Classes.Init. -Require Export Coq.Classes.RelationClasses. +Require Import Relation_Definitions. +Require Import Coq.Classes.RelationClasses. Require Export Coq.Classes.Morphisms. -Require Export Coq.Classes.SetoidTactics. Set Implicit Arguments. Unset Strict Implicit. +Open Local Scope signature_scope. + (** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *) Instance [ ! Equivalence A R ] => @@ -35,16 +37,16 @@ Definition equiv [ Equivalence A R ] : relation A := R. (** Shortcuts to make proof search possible (unification won't unfold equiv). *) -Program Instance [ sa : ! Equivalence A ] => equiv_refl : reflexive equiv. +Program Instance [ sa : ! Equivalence A ] => equiv_refl : Reflexive equiv. -Program Instance [ sa : ! Equivalence A ] => equiv_sym : symmetric equiv. +Program Instance [ sa : ! Equivalence A ] => equiv_sym : Symmetric equiv. Next Obligation. Proof. symmetry ; auto. Qed. -Program Instance [ sa : ! Equivalence A ] => equiv_trans : transitive equiv. +Program Instance [ sa : ! Equivalence A ] => equiv_trans : Transitive equiv. Next Obligation. Proof. @@ -112,12 +114,12 @@ Ltac equivify_tac := Ltac equivify := repeat equivify_tac. -(** Every equivalence relation gives rise to a morphism, as it is transitive and symmetric. *) +(** Every equivalence relation gives rise to a morphism, as it is Transitive and Symmetric. *) Instance [ sa : ! Equivalence ] => equiv_morphism : Morphism (equiv ++> equiv ++> iff) equiv := respect := respect. -(** The partial application too as it is reflexive. *) +(** The partial application too as it is Reflexive. *) Instance [ sa : ! Equivalence A ] (x : A) => equiv_partial_app_morphism : Morphism (equiv ++> iff) (equiv x) := diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v index 2795e4218..28fa55ee1 100644 --- a/theories/Classes/Functions.v +++ b/theories/Classes/Functions.v @@ -15,9 +15,8 @@ (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) -Require Import Coq.Program.Program. -Require Export Coq.Classes.RelationClasses. -Require Export Coq.Classes.Morphisms. +Require Import Coq.Classes.RelationClasses. +Require Import Coq.Classes.Morphisms. Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index c752cae86..f4ec50989 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -17,6 +17,7 @@ Require Import Coq.Program.Basics. Require Import Coq.Program.Tactics. +Require Import Coq.Relations.Relation_Definitions. Require Export Coq.Classes.RelationClasses. Set Implicit Arguments. @@ -38,9 +39,20 @@ Definition respectful A B (R : relation A) (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 _ _ (inverse R) R') (right associativity, at level 20). +Delimit Scope signature_scope with signature. + +Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature)) + (right associativity, at level 55) : signature_scope. + +Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature)) + (right associativity, at level 55) : signature_scope. + +Notation " R --> R' " := (@respectful _ _ (inverse (R%signature)) (R'%signature)) + (right associativity, at level 55) : signature_scope. + +Arguments Scope respectful [type_scope type_scope signature_scope signature_scope]. + +Open Local Scope signature_scope. (** A morphism on a relation [R] is an object respecting the relation (in its kernel). The relation [R] will be instantiated by [respectful] and [A] by an arrow type @@ -49,6 +61,8 @@ Notation " R --> R' " := (@respectful _ _ (inverse R) R') (right associativity, Class Morphism A (R : relation A) (m : A) : Prop := respect : R m m. +Arguments Scope Morphism [type_scope signature_scope]. + (** Here we build an equivalence instance for functions which relates respectful ones only. *) Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] : Type := @@ -163,7 +177,7 @@ Program Instance iff_iff_iff_impl_morphism : Morphism (iff ==> iff ==> iff) impl (* Typeclasses eauto := debug. *) -Program Instance [ ! symmetric A R, Morphism (R ==> impl) m ] => reflexive_impl_iff : Morphism (R ==> iff) m. +Program Instance [ ! Symmetric A R, Morphism (R ==> impl) m ] => Reflexive_impl_iff : Morphism (R ==> iff) m. Next Obligation. Proof. @@ -202,10 +216,10 @@ Program Instance {A B C : Type} [ Morphism (RA ==> RB ==> RC) (f : A -> B -> C) apply respect ; auto. Qed. -(** Every transitive relation gives rise to a binary morphism on [impl], +(** Every Transitive relation gives rise to a binary morphism on [impl], contravariant in the first argument, covariant in the second. *) -Program Instance [ ! transitive A (R : relation A) ] => +Program Instance [ ! Transitive A (R : relation A) ] => trans_contra_co_morphism : Morphism (R --> R ++> impl) R. Next Obligation. @@ -216,7 +230,7 @@ Program Instance [ ! transitive A (R : relation A) ] => (** Dually... *) -Program Instance [ ! transitive A (R : relation A) ] => +Program Instance [ ! Transitive A (R : relation A) ] => trans_co_contra_inv_impl_morphism : Morphism (R ++> R --> inverse impl) R. Next Obligation. @@ -224,7 +238,7 @@ Program Instance [ ! transitive A (R : relation A) ] => apply* trans_contra_co_morphism ; eauto. eauto. Qed. -(* Program Instance [ transitive A (R : relation A), symmetric A R ] => *) +(* Program Instance [ Transitive A (R : relation A), Symmetric A R ] => *) (* trans_sym_contra_co_inv_impl_morphism : ? Morphism (R --> R ++> inverse impl) R. *) (* Next Obligation. *) @@ -238,7 +252,7 @@ Program Instance [ ! transitive A (R : relation A) ] => (** Morphism declarations for partial applications. *) -Program Instance [ ! transitive A R ] (x : A) => +Program Instance [ ! Transitive A R ] (x : A) => trans_contra_inv_impl_morphism : Morphism (R --> inverse impl) (R x). Next Obligation. @@ -246,7 +260,7 @@ Program Instance [ ! transitive A R ] (x : A) => transitivity y... Qed. -Program Instance [ ! transitive A R ] (x : A) => +Program Instance [ ! Transitive A R ] (x : A) => trans_co_impl_morphism : Morphism (R ==> impl) (R x). Next Obligation. @@ -254,7 +268,7 @@ Program Instance [ ! transitive A R ] (x : A) => transitivity x0... Qed. -Program Instance [ ! transitive A R, symmetric R ] (x : A) => +Program Instance [ ! Transitive A R, Symmetric R ] (x : A) => trans_sym_co_inv_impl_morphism : Morphism (R ==> inverse impl) (R x). Next Obligation. @@ -262,7 +276,7 @@ Program Instance [ ! transitive A R, symmetric R ] (x : A) => transitivity y... Qed. -Program Instance [ ! transitive A R, symmetric R ] (x : A) => +Program Instance [ ! Transitive A R, Symmetric R ] (x : A) => trans_sym_contra_impl_morphism : Morphism (R --> impl) (R x). Next Obligation. @@ -281,10 +295,10 @@ Program Instance [ Equivalence A R ] (x : A) => symmetry... Qed. -(** With symmetric relations, variance is no issue ! *) +(** 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 ] => *) +(* [ Morphism _ (R ==> R') m ] [ Symmetric A R ] => *) (* sym_contra_morphism : Morphism (R --> R') m. *) (* Next Obligation. *) @@ -293,16 +307,16 @@ Program Instance [ Equivalence A R ] (x : A) => (* sym... *) (* Qed. *) -(** [R] is reflexive, hence we can build the needed proof. *) +(** [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 R ] (x : A) => - reflexive_partial_app_morphism : Morphism R' (m x) | 3. + [ Morphism (R ==> R') m ] [ Reflexive R ] (x : A) => + Reflexive_partial_app_morphism : Morphism R' (m x) | 3. -(** Every transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof +(** 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 ] => +Program Instance [ ! Transitive A R ] => trans_co_eq_inv_impl_morphism : Morphism (R ==> (@eq A) ==> inverse impl) R. Next Obligation. @@ -310,7 +324,7 @@ Program Instance [ ! transitive A R ] => transitivity y... Qed. -Program Instance [ ! transitive A R ] => +Program Instance [ ! Transitive A R ] => trans_contra_eq_impl_morphism : Morphism (R --> (@eq A) ==> impl) R. Next Obligation. @@ -318,9 +332,9 @@ Program Instance [ ! transitive A R ] => transitivity x... Qed. -(** Every symmetric and transitive relation gives rise to an equivariant morphism. *) +(** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *) -Program Instance [ ! transitive A R, symmetric R ] => +Program Instance [ ! Transitive A R, Symmetric R ] => trans_sym_morphism : Morphism (R ==> R ==> iff) R. Next Obligation. @@ -407,12 +421,12 @@ Program Instance or_iff_morphism : (* red ; intros. subst ; split; trivial. *) (* Qed. *) -Instance (A B : Type) [ ! reflexive B R ] (m : A -> B) => - eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3. +Instance (A B : Type) [ ! Reflexive B R ] (m : A -> B) => + eq_Reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3. Proof. simpl_relation. Qed. -Instance (A B : Type) [ ! reflexive B R' ] => - reflexive (@Logic.eq A ==> R'). +Instance (A B : Type) [ ! Reflexive B R' ] => + Reflexive (@Logic.eq A ==> R'). Proof. simpl_relation. Qed. (** [respectful] is a morphism for relation equivalence. *) diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 53079674f..492b8498a 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -50,74 +50,74 @@ Proof. reflexivity. Qed. (** We rebind relations in separate classes to be able to overload each proof. *) -Class reflexive A (R : relation A) := +Class Reflexive A (R : relation A) := reflexivity : forall x, R x x. -Class irreflexive A (R : relation A) := +Class Irreflexive A (R : relation A) := irreflexivity : forall x, R x x -> False. -Class symmetric A (R : relation A) := +Class Symmetric A (R : relation A) := symmetry : forall x y, R x y -> R y x. -Class asymmetric A (R : relation A) := +Class Asymmetric A (R : relation A) := asymmetry : forall x y, R x y -> R y x -> False. -Class transitive A (R : relation A) := +Class Transitive A (R : relation A) := transitivity : forall x y z, R x y -> R y z -> R x z. -Implicit Arguments reflexive [A]. -Implicit Arguments irreflexive [A]. -Implicit Arguments symmetric [A]. -Implicit Arguments asymmetric [A]. -Implicit Arguments transitive [A]. +Implicit Arguments Reflexive [A]. +Implicit Arguments Irreflexive [A]. +Implicit Arguments Symmetric [A]. +Implicit Arguments Asymmetric [A]. +Implicit Arguments Transitive [A]. Hint Resolve @irreflexivity : ord. (** We can already dualize all these properties. *) -Program Instance [ ! reflexive A R ] => flip_reflexive : reflexive (flip R) := +Program Instance [ ! Reflexive A R ] => flip_Reflexive : Reflexive (flip R) := reflexivity := reflexivity (R:=R). -Program Instance [ ! irreflexive A R ] => flip_irreflexive : irreflexive (flip R) := +Program Instance [ ! Irreflexive A R ] => flip_Irreflexive : Irreflexive (flip R) := irreflexivity := irreflexivity (R:=R). -Program Instance [ ! symmetric A R ] => flip_symmetric : symmetric (flip R). +Program Instance [ ! Symmetric A R ] => flip_Symmetric : Symmetric (flip R). - Solve Obligations using unfold flip ; program_simpl ; clapply symmetric. + Solve Obligations using unfold flip ; program_simpl ; clapply Symmetric. -Program Instance [ ! asymmetric A R ] => flip_asymmetric : asymmetric (flip R). +Program Instance [ ! Asymmetric A R ] => flip_Asymmetric : Asymmetric (flip R). Solve Obligations using program_simpl ; unfold flip in * ; intros ; clapply asymmetry. -Program Instance [ ! transitive A R ] => flip_transitive : transitive (flip R). +Program Instance [ ! Transitive A R ] => flip_Transitive : Transitive (flip R). Solve Obligations using unfold flip ; program_simpl ; clapply transitivity. (** Have to do it again for Prop. *) -Program Instance [ ! reflexive A (R : relation A) ] => inverse_reflexive : reflexive (inverse R) := +Program Instance [ ! Reflexive A (R : relation A) ] => inverse_Reflexive : Reflexive (inverse R) := reflexivity := reflexivity (R:=R). -Program Instance [ ! irreflexive A (R : relation A) ] => inverse_irreflexive : irreflexive (inverse R) := +Program Instance [ ! Irreflexive A (R : relation A) ] => inverse_Irreflexive : Irreflexive (inverse R) := irreflexivity := irreflexivity (R:=R). -Program Instance [ ! symmetric A (R : relation A) ] => inverse_symmetric : symmetric (inverse R). +Program Instance [ ! Symmetric A (R : relation A) ] => inverse_Symmetric : Symmetric (inverse R). - Solve Obligations using unfold inverse, flip ; program_simpl ; clapply symmetric. + Solve Obligations using unfold inverse, flip ; program_simpl ; clapply Symmetric. -Program Instance [ ! asymmetric A (R : relation A) ] => inverse_asymmetric : asymmetric (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 asymmetry. -Program Instance [ ! transitive A (R : relation A) ] => inverse_transitive : transitive (inverse R). +Program Instance [ ! Transitive A (R : relation A) ] => inverse_Transitive : Transitive (inverse R). Solve Obligations using unfold inverse, flip ; program_simpl ; clapply transitivity. -Program Instance [ ! reflexive A (R : relation A) ] => - reflexive_complement_irreflexive : irreflexive (complement R). +Program Instance [ ! Reflexive A (R : relation A) ] => + Reflexive_complement_Irreflexive : Irreflexive (complement R). -Program Instance [ ! irreflexive A (R : relation A) ] => - irreflexive_complement_reflexive : reflexive (complement R). +Program Instance [ ! Irreflexive A (R : relation A) ] => + Irreflexive_complement_Reflexive : Reflexive (complement R). Next Obligation. Proof. @@ -125,7 +125,7 @@ Program Instance [ ! irreflexive A (R : relation A) ] => apply (irreflexivity H). Qed. -Program Instance [ ! symmetric A (R : relation A) ] => complement_symmetric : symmetric (complement R). +Program Instance [ ! Symmetric A (R : relation A) ] => complement_Symmetric : Symmetric (complement R). Next Obligation. Proof. @@ -155,34 +155,34 @@ 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). (** Various combinations of reflexivity, symmetry and transitivity. *) -(** A [PreOrder] is both reflexive and transitive. *) +(** A [PreOrder] is both Reflexive and Transitive. *) Class PreOrder A (R : relation A) := - preorder_refl :> reflexive R ; - preorder_trans :> transitive R. + preorder_refl :> Reflexive R ; + preorder_trans :> Transitive R. -(** A partial equivalence relation is symmetric and transitive. *) +(** A partial equivalence relation is Symmetric and Transitive. *) Class PER (carrier : Type) (pequiv : relation carrier) := - per_sym :> symmetric pequiv ; - per_trans :> transitive pequiv. + per_sym :> Symmetric pequiv ; + per_trans :> Transitive pequiv. (** We can build a PER on the Coq function space if we have PERs on the domain and codomain. *) @@ -201,20 +201,20 @@ Program Instance [ PER A (R : relation A), PER B (R' : relation B) ] => (** The [Equivalence] typeclass. *) Class Equivalence (carrier : Type) (equiv : relation carrier) := - equiv_refl :> reflexive equiv ; - equiv_sym :> symmetric equiv ; - equiv_trans :> transitive equiv. + equiv_refl :> Reflexive equiv ; + equiv_sym :> Symmetric equiv ; + equiv_trans :> Transitive equiv. (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *) -Class [ Equivalence A eqA ] => antisymmetric (R : relation A) := +Class [ Equivalence A eqA ] => Antisymmetric (R : relation A) := antisymmetry : 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). -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). (** Leibinz equality [eq] is an equivalence relation. *) diff --git a/theories/Classes/SetoidAxioms.v b/theories/Classes/SetoidAxioms.v index 6b7881c9f..7cf2980c4 100644 --- a/theories/Classes/SetoidAxioms.v +++ b/theories/Classes/SetoidAxioms.v @@ -32,4 +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.
\ No newline at end of file + end. diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index d2ee4f443..e64cbd12c 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -15,15 +15,15 @@ (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) -Require Import Coq.Program.Program. -Require Import Coq.Classes.Init. - Set Implicit Arguments. Unset Strict Implicit. +Require Import Coq.Program.Program. + +Require Import Coq.Classes.Init. Require Export Coq.Classes.RelationClasses. Require Export Coq.Classes.Morphisms. -Require Export Coq.Classes.Functions. +Require Import Coq.Classes.Functions. (** A setoid wraps an equivalence. *) @@ -40,13 +40,13 @@ Typeclasses unfold @equiv. (** Shortcuts to make proof search easier. *) -Definition setoid_refl [ sa : Setoid A ] : reflexive equiv. +Definition setoid_refl [ sa : Setoid A ] : Reflexive equiv. Proof. eauto with typeclass_instances. Qed. -Definition setoid_sym [ sa : Setoid A ] : symmetric equiv. +Definition setoid_sym [ sa : Setoid A ] : Symmetric equiv. Proof. eauto with typeclass_instances. Qed. -Definition setoid_trans [ sa : Setoid A ] : transitive equiv. +Definition setoid_trans [ sa : Setoid A ] : Transitive equiv. Proof. eauto with typeclass_instances. Qed. Existing Instance setoid_refl. @@ -131,7 +131,7 @@ Implicit Arguments setoid_morphism [[!sa]]. Existing Instance setoid_morphism. Program Definition setoid_partial_app_morphism [ sa : Setoid A ] (x : A) : Morphism (equiv ++> iff) (equiv x) := - reflexive_partial_app_morphism. + Reflexive_partial_app_morphism. Existing Instance setoid_partial_app_morphism. diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index ee8c530fa..8d2be43cc 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -17,6 +17,8 @@ Require Export Coq.Classes.RelationClasses. Require Export Coq.Classes.Morphisms. +Require Export Coq.Classes.Equivalence. +Require Export Coq.Relations.Relation_Definitions. Set Implicit Arguments. Unset Strict Implicit. @@ -65,6 +67,8 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) Require Import Coq.Program.Tactics. +Open Local Scope signature_scope. + Ltac red_subst_eq_morphism concl := match concl with | @Logic.eq ?A ==> ?R' => red ; intros ; subst ; red_subst_eq_morphism R' diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index 34bff6354..983c651ab 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -10,8 +10,7 @@ Set Implicit Arguments. -Require Export Coq.Classes.Equivalence. -Require Export Coq.Relations.Relation_Definitions. +Require Export Coq.Classes.SetoidTactics. (** For backward compatibility *) |