- A little cleanup in Classes/*. Separate standard morphisms on

relf/sym/trans relations from morphisms on prop connectives and
relations.
- Add general order theory on predicates, instantiated for relations.
Derives equivalence, implication, conjunction and disjunction as
liftings from propositional connectives. Can be used for n-ary
homogeneous predicates thanks to a bit of metaprogramming with lists of
types. 
- Rebind Setoid_Theory to use the Equivalence record type instead of
declaring an isomorphic one. One needs to do "red" after constructor to
get the same statements when building objects of type Setoid_Theory, so
scripts break.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10765 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 47 insertions, 0 deletions

diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
new file mode 100644
index 000000000..284810e94
--- /dev/null
+++ b/theories/Classes/Morphisms_Relations.v
@@ -0,0 +1,47 @@
+(* -*- 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 *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Morphism instances for relations.
+ 
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+   91405 Orsay, France *)
+
+(** Morphisms for relations *)
+
+Instance relation_conjunction_morphism : Morphism (relation_equivalence (A:=A) ==>
+  relation_equivalence ==> relation_equivalence) relation_conjunction.
+  Proof. firstorder. Qed.
+
+Instance relation_disjunction_morphism : Morphism (relation_equivalence (A:=A) ==>
+  relation_equivalence ==> relation_equivalence) relation_disjunction.
+  Proof. firstorder. Qed.
+
+(* Predicate equivalence is exactly the same as the pointwise lifting of [iff]. *)
+
+Require Import List.
+
+Lemma predicate_equivalence_pointwise (l : list Type) :
+  Morphism (@predicate_equivalence l ==> lift_pointwise l iff) id.
+Proof. do 2 red. unfold predicate_equivalence. auto. Qed.
+
+Lemma predicate_implication_pointwise (l : list Type) :
+  Morphism (@predicate_implication l ==> lift_pointwise l impl) 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:=A) (pointwise_relation (A:=A) iff)) id.
+Proof. apply (predicate_equivalence_pointwise (l:=(cons A (cons A nil)))). Qed.
+
+Instance subrelation_pointwise :
+  Morphism (subrelation ==> pointwise_relation (A:=A) (pointwise_relation (A:=A) impl)) id.
+Proof. apply (predicate_implication_pointwise (l:=(cons A (cons A nil)))). Qed.