diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-09 16:43:04 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-09 16:43:04 +0000 |
| commit | 67021c6861020d5b0969a6c5856304e2486fb56d (patch) | |
| tree | 6dc8d87fb02f568e576e8398adb2b5950030a03d /theories/Classes | |
| parent | 85af5bb1ec5b2f080e267b8a8bb4438f8f640eb1 (diff) | |
Add a missing morphism declaration that turns morphisms on R ==> R' to
morphisms on R --> inverse R' for any R, R' (report by N. Tabareau).
Better implementation of unfolding for impl that does it only where
necessary to keep the goal in the same shape as the user gave.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10648 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Classes')
| -rw-r--r-- | theories/Classes/Morphisms.v | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 1ba1f585a..0087916c3 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -241,8 +241,21 @@ Program Instance {A B C : Type} [ Morphism (RA ==> RB ==> RC) (f : A -> B -> C) (* apply respect. *) (* Qed. *) +(** Every morphism gives rise to a morphism on the inverse relation. *) -(** Morpshism declarations for partial applications. *) +Program Instance (A : Type) (R : relation A) (B : Type) (R' : relation B) + [ Morphism (R ==> R') m ] => morphism_inverse_morphism : + Morphism (inverse R ==> inverse R') m. + + Next Obligation. + Proof. + unfold inverse in *. + pose respect. + unfold respectful in r. + apply r ; auto. + Qed. + +(** Morphism declarations for partial applications. *) Program Instance [ ! Transitive A R ] (x : A) => trans_contra_inv_impl_morphism : Morphism (R --> inverse impl) (R x). |