diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Classes/Equivalence.v | 16 | ||||
| -rw-r--r-- | theories/Classes/Functions.v | 14 | ||||
| -rw-r--r-- | theories/Classes/Morphisms.v | 53 | ||||
| -rw-r--r-- | theories/Classes/RelationClasses.v | 30 | ||||
| -rw-r--r-- | theories/Classes/SetoidDec.v | 10 |
5 files changed, 60 insertions, 63 deletions
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index 58aef9a7b6..d0c9991964 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -30,23 +30,23 @@ Open Local Scope signature_scope. (** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *) -Instance [ ! Equivalence A R ] => +Instance [ Equivalence A R ] => equivalence_default : DefaultRelation A R | 4. 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. @@ -81,7 +81,7 @@ 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. +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 (symmetry ; auto). @@ -89,7 +89,7 @@ Proof with auto. 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 (symmetry ; auto). @@ -116,12 +116,12 @@ Ltac equivify := repeat equivify_tac. (** Every equivalence relation gives rise to a morphism, as it is Transitive and Symmetric. *) -Instance [ sa : ! Equivalence ] => 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) => +Instance [ sa : Equivalence A ] (x : A) => equiv_partial_app_morphism : Morphism (equiv ++> iff) (equiv x) := respect := respect. diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v index 28fa55ee12..4750df6399 100644 --- a/theories/Classes/Functions.v +++ b/theories/Classes/Functions.v @@ -21,22 +21,22 @@ Require Import Coq.Classes.Morphisms. Set Implicit Arguments. Unset Strict Implicit. -Class [ m : ! Morphism (A -> B) (RA ++> RB) f ] => Injective : Prop := +Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Injective : Prop := injective : forall x y : A, RB (f x) (f y) -> RA x y. -Class [ m : ! Morphism (A -> B) (RA ++> RB) f ] => Surjective : Prop := +Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Surjective : 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 : 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 f4ec509891..eda2aecaa1 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -152,7 +152,7 @@ Proof. reduce. apply* H. apply* sub. assumption. Qed. -Lemma subrelation_morphism [ SubRelation A R₁ R₂, Morphism R₂ m ] : Morphism R₁ m. +Lemma subrelation_morphism [ SubRelation A R₁ R₂, ! Morphism R₂ m ] : Morphism R₁ m. Proof. intros. apply* H. apply H0. Qed. @@ -177,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. @@ -186,7 +186,7 @@ Program Instance [ ! Symmetric A R, Morphism (R ==> impl) m ] => Reflexive_impl_ (** The complement of a relation conserves its morphisms. *) -Program Instance {A} (RA : relation A) [ mR : Morphism (RA ==> RA ==> iff) R ] => +Program Instance [ mR : Morphism (A -> A -> Prop) (RA ==> RA ==> iff) R ] => complement_morphism : Morphism (RA ==> RA ==> iff) (complement R). Next Obligation. @@ -200,7 +200,7 @@ Program Instance {A} (RA : relation A) [ mR : Morphism (RA ==> RA ==> iff) R ] = (** The inverse too. *) -Program Instance {A} (RA : relation A) [ Morphism (RA ==> RA ==> iff) R ] => +Program Instance [ Morphism (A -> _) (RA ==> RA ==> iff) R ] => inverse_morphism : Morphism (RA ==> RA ==> iff) (inverse R). Next Obligation. @@ -208,7 +208,7 @@ 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) ] => +Program Instance [ Morphism (A -> B -> C) (RA ==> RB ==> RC) f ] => flip_morphism : Morphism (RB ==> RA ==> RC) (flip f). Next Obligation. @@ -219,7 +219,7 @@ Program Instance {A B C : Type} [ Morphism (RA ==> RB ==> RC) (f : A -> B -> C) (** 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 ] => trans_contra_co_morphism : Morphism (R --> R ++> impl) R. Next Obligation. @@ -230,7 +230,7 @@ Program Instance [ ! Transitive A (R : relation A) ] => (** Dually... *) -Program Instance [ ! Transitive A (R : relation A) ] => +Program Instance [ Transitive A R ] => trans_co_contra_inv_impl_morphism : Morphism (R ++> R --> inverse impl) R. Next Obligation. @@ -252,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. @@ -260,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. @@ -268,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 A R ] (x : A) => trans_sym_co_inv_impl_morphism : Morphism (R ==> inverse impl) (R x). Next Obligation. @@ -276,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. @@ -309,14 +309,13 @@ 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 R ] (x : A) => +Program Instance [ Morphism (A -> B) (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 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. @@ -324,7 +323,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. @@ -334,7 +333,7 @@ Program Instance [ ! Transitive A R ] => (** 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. @@ -421,11 +420,11 @@ 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 : 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' ] => +Instance (A : Type) [ Reflexive B R' ] => Reflexive (@Logic.eq A ==> R'). Proof. simpl_relation. Qed. @@ -469,9 +468,8 @@ Proof. symmetry ; apply inverse_respectful. Qed. -Instance (A : Type) (R : relation A) (B : Type) (R' R'' : relation B) - [ Normalizes relation_equivalence R' (inverse R'') ] => - Normalizes relation_equivalence (inverse R ==> R') (inverse (R ==> R'')) . +Instance [ Normalizes (relation B) relation_equivalence R' (inverse R'') ] => + ! Normalizes (relation (A -> B)) relation_equivalence (inverse R ==> R') (inverse (R ==> R'')) . Proof. red. pose normalizes. @@ -480,9 +478,8 @@ Proof. reflexivity. Qed. -Program Instance (A : Type) (R : relation A) - [ Morphism R m ] => morphism_inverse_morphism : - Morphism (inverse R) m | 2. +Program Instance [ Morphism A R m ] => + morphism_inverse_morphism : Morphism (inverse R) m | 2. (** Bootstrap !!! *) @@ -497,9 +494,9 @@ Proof. apply respect. Qed. -Lemma morphism_releq_morphism (A : Type) (R : relation A) (R' : relation A) - [ Normalizes relation_equivalence R R' ] - [ Morphism R' m ] : Morphism R m. +Lemma morphism_releq_morphism + [ Normalizes (relation A) relation_equivalence R R', + Morphism _ R' m ] : Morphism R m. Proof. intros. pose respect. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 492b8498a6..0ca0745893 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -75,48 +75,48 @@ 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. -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. -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) ] => +Program Instance [ Reflexive A (R : relation A) ] => Reflexive_complement_Irreflexive : Irreflexive (complement R). -Program Instance [ ! Irreflexive A (R : relation A) ] => +Program Instance [ Irreflexive A (R : relation A) ] => Irreflexive_complement_Reflexive : Reflexive (complement R). Next Obligation. @@ -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. @@ -210,10 +210,10 @@ Class Equivalence (carrier : Type) (equiv : relation carrier) := 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 ] => +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) ] => +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/SetoidDec.v b/theories/Classes/SetoidDec.v index 86a2bef80f..26e1ab244d 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -54,7 +54,7 @@ Open Local Scope program_scope. (** 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. *) @@ -62,10 +62,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). @@ -97,7 +97,7 @@ Program Instance unit_eqdec : EqDec (@eq_setoid unit) := reflexivity. Qed. -Program Instance [ EqDec (@eq_setoid A), EqDec (@eq_setoid 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 @@ -113,7 +113,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 in_left |