diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Classes/Equivalence.v | 10 | ||||
| -rw-r--r-- | theories/Classes/Morphisms.v | 139 | ||||
| -rw-r--r-- | theories/Classes/RelationClasses.v | 25 |
3 files changed, 125 insertions, 49 deletions
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index b90fdc97e2..5543f615d8 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -26,6 +26,11 @@ Require Export Coq.Classes.SetoidTactics. Set Implicit Arguments. Unset Strict Implicit. +(** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *) + +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). *) @@ -152,8 +157,3 @@ Notation " x =~= y " := (pequiv x y) (at level 70, no associativity) : type_scop (** Reset the default Program tactic. *) Ltac obligations_tactic ::= program_simpl. - -(** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *) - -Instance [ ! Equivalence A R ] => - equivalence_default : DefaultRelation A R | 4. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index fbe90a9a94..a6ca6a0316 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *) +(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms") -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -220,52 +220,9 @@ Program Instance {A B C : Type} [ Morphism (RA ==> RB ==> RC) (f : A -> B -> C) Next Obligation. Proof. - unfold flip. apply respect ; auto. Qed. -(** 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). *) - -(* Next Obligation. *) -(* Proof with auto. *) -(* apply (respect (m:=m))... *) -(* apply respect. *) -(* Qed. *) - -(** Every morphism gives rise to a morphism on the inverse relation. *) - -Program Instance (A : Type) (R : relation A) (B : Type) (R' : relation B) - [ Morphism (R ==> R') m ] => morphism_inverse_morphism : - Morphism (R --> inverse R') m. - - Next Obligation. - Proof. - unfold inverse in *. - pose respect. - unfold respectful in r. - apply r ; auto. - Qed. - -(* Program Instance (A : Type) (R : relation A) (B : Type) (R' : relation B) (C : Type) (R'' : relation C) *) -(* [ Morphism (R ++> R' ++> R'') m ] => *) -(* morphism_inverse_inverse_morphism : *) -(* Morphism (R --> R' --> inverse R'') m. *) - -(* Next Obligation. *) -(* Proof. *) -(* unfold inverse in *. *) -(* pose respect. *) -(* unfold respectful in r. *) -(* apply r ; auto. *) -(* Qed. *) - - (** Every transitive relation gives rise to a binary morphism on [impl], contravariant in the first argument, covariant in the second. *) @@ -493,3 +450,97 @@ Proof. simpl_relation. Qed. Instance (A B : Type) [ ! Reflexive B R' ] => Reflexive (@Logic.eq A ==> R'). Proof. simpl_relation. Qed. + +(** [respectful] is a morphism for relation equivalence. *) + +Instance respectful_morphism : + Morphism (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B). +Proof. + do 2 red ; intros. + unfold respectful, relation_equivalence in *. + red ; intros. + split ; intros. + + rewrite <- H0. + apply H1. + rewrite H. + assumption. + + rewrite H0. + apply H1. + rewrite <- H. + assumption. +Qed. + +Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B), + inverse (R ==> R') ==rel (inverse R ==> inverse R'). +Proof. + intros. + unfold inverse, flip. + unfold respectful. + split ; intros ; intuition. +Qed. + +Class (A : Type) (R : relation A) => Normalizes (m : A) (m' : A) := + normalizes : R m m'. + +Instance (A : Type) (R : relation A) (B : Type) (R' : relation B) => + Normalizes relation_equivalence (inverse R ==> inverse R') (inverse (R ==> R')) . +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'')) . +Proof. + pose normalizes. + setoid_rewrite r. + setoid_rewrite inverse_respectful. + reflexivity. +Qed. + +Program Instance (A : Type) (R : relation A) + [ Morphism R m ] => morphism_inverse_morphism : + Morphism (inverse R) m | 2. + + Next Obligation. + Proof. + apply respect. + Qed. + +(** Bootstrap !!! *) + +Instance morphism_morphism : Morphism (relation_equivalence ==> @eq _ ==> iff) (@Morphism A). +Proof. + simpl_relation. + subst. + unfold relation_equivalence in H. + split ; constructor ; intros. + setoid_rewrite <- H. + apply respect. + setoid_rewrite H. + 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. +Proof. + intros. + pose respect. + assert(n:=normalizes). + setoid_rewrite n. + assumption. +Qed. + +Inductive normalization_done : Prop := did_normalization. + +Ltac morphism_normalization := + match goal with + | [ _ : normalization_done |- @Morphism _ _ _ ] => fail + | [ |- @Morphism _ _ _ ] => let H := fresh "H" in + set(H:=did_normalization) ; eapply @morphism_releq_morphism + end. + +Hint Extern 5 (@Morphism _ _ _) => morphism_normalization : typeclass_instances. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 20ac475b9e..68352abd0a 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -227,3 +227,28 @@ Program Instance [ sa : Equivalence a R, sb : Equivalence b R' ] => equiv_setoid (fun f g => forall (x y : a), R x y -> R' (f x) (g y)). *) +Definition relation_equivalence {A : Type} : relation (relation A) := + fun (R R' : relation A) => forall x y, R x y <-> R' x y. + +Infix "==rel" := relation_equivalence (at level 70). + +Program Instance relation_equivalence_equivalence : + Equivalence (relation A) relation_equivalence. + + Next Obligation. + Proof. + constructor ; red ; intros. + apply reflexive. + Qed. + + Next Obligation. + Proof. + constructor ; red ; intros. + apply symmetric ; apply H. + Qed. + + Next Obligation. + Proof. + constructor ; red ; intros. + apply transitive with (y x0 y0) ; [ apply H | apply H0 ]. + Qed. |