* New syntactic sugar: Add Relation ... transitivity proved by ...

  now declares both the relation and the relation as a morphism, computing
  the appropriate signature (depending on the reflexivity of the relation).
* New parameter "as ..." to Add Relation (to be able to compute the
  morphism name).


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

1 files changed, 70 insertions, 30 deletions

diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index bde24eded..c0ab8aa55 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -138,22 +138,22 @@ Definition morphism_theory_of_function :
     intro; apply (IHIn (X x)).
 Defined.
 
-(* THE Prop RELATION CLASS *)
+(* THE iff RELATION CLASS *)
 
-Add Relation Prop iff reflexivity proved by iff_refl symmetry proved by iff_sym.
+Add Relation Prop iff reflexivity proved by iff_refl symmetry proved by iff_sym as iff_relation.
 
-Definition Prop_Relation_Class : Relation_Class.
+Definition Iff_Relation_Class : Relation_Class.
  eapply (@SymmetricReflexive unit _ iff).
  exact iff_sym.
  exact iff_refl.
 Defined.
 
-(* every predicate is  morphism from Leibniz+ to Prop_Relation_Class *)
+(* every predicate is  morphism from Leibniz+ to Iff_Relation_Class *)
 Definition morphism_theory_of_predicate :
  forall (In: nelistT Type),
   let In' := list_of_Leibniz_of_list_of_types In in
-   function_type_of_morphism_signature In' Prop_Relation_Class ->
-    Morphism_Theory In' Prop_Relation_Class.
+   function_type_of_morphism_signature In' Iff_Relation_Class ->
+    Morphism_Theory In' Iff_Relation_Class.
   intros.
   exists X.
   induction In;  unfold make_compatibility_goal; simpl.
@@ -161,6 +161,25 @@ Definition morphism_theory_of_predicate :
     intro; apply (IHIn (X x)).
 Defined.
 
+(* THE impl RELATION CLASS *)
+
+Definition impl (A B: Prop) := A -> B.
+
+Theorem impl_refl: reflexive _ impl.
+ hnf; unfold impl; tauto.
+Qed.
+
+Theorem impl_trans: transitive _ impl.
+ hnf; unfold impl; tauto.
+Qed.
+
+Add Relation Prop impl reflexivity proved by impl_refl as impl_relation.
+
+Definition Impl_Relation_Class : Relation_Class.
+ eapply (@AsymmetricReflexive unit tt _ impl).
+ exact impl_refl.
+Defined.
+
 (* THE CIC PART OF THE REFLEXIVE TACTIC (SETOID REWRITE) *)
 
 Inductive rewrite_direction : Type :=
@@ -566,7 +585,7 @@ Definition equality_morphism_of_setoid_theory:
  forall (A: Type) (Aeq: relation A) (ST: Setoid_Theory Aeq),
    let ASetoidClass := argument_class_of_setoid_theory ST in 
     (Morphism_Theory (cons ASetoidClass (singl ASetoidClass))
-      Prop_Relation_Class).
+      Iff_Relation_Class).
  intros.
  exists Aeq.
  pose (sym   := Seq_sym ST);  clearbody sym.
@@ -574,56 +593,77 @@ Definition equality_morphism_of_setoid_theory:
  unfold make_compatibility_goal; simpl; split; eauto.
 Defined.
 
-Lemma eq_setoid : forall R, Setoid_Theory (@eq R).
-Proof
-  (fun R =>
-    Build_Setoid_Theory (@eq R) (@refl_equal R) (@sym_eq R) (@trans_eq R)).
+Definition equality_morphism_of_symmetric_areflexive_transitive_relation:
+ forall (A: Type)(Aeq: relation A)(sym: symmetric _ Aeq)(trans: transitive _ Aeq),
+  let ASetoidClass := SymmetricAreflexive _ sym in
+   (Morphism_Theory (cons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class).
+ intros.
+ exists Aeq.
+ unfold make_compatibility_goal; simpl; split; eauto.
+Defined.
+
+Definition equality_morphism_of_symmetric_reflexive_transitive_relation:
+ forall (A: Type)(Aeq: relation A)(refl: reflexive _ Aeq)(sym: symmetric _ Aeq)
+  (trans: transitive _ Aeq), let ASetoidClass := SymmetricReflexive _ sym refl in
+   (Morphism_Theory (cons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class).
+ intros.
+ exists Aeq.
+ unfold make_compatibility_goal; simpl; split; eauto.
+Defined.
+
+Definition equality_morphism_of_asymmetric_areflexive_transitive_relation:
+ forall (A: Type)(Aeq: relation A)(trans: transitive _ Aeq),
+  let ASetoidClass1 := AsymmetricAreflexive Contravariant Aeq in
+  let ASetoidClass2 := AsymmetricAreflexive Covariant Aeq in
+   (Morphism_Theory (cons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class).
+ intros.
+ exists Aeq.
+ unfold make_compatibility_goal; simpl; unfold impl; eauto.
+Defined.
+
+Definition equality_morphism_of_asymmetric_reflexive_transitive_relation:
+ forall (A: Type)(Aeq: relation A)(refl: reflexive _ Aeq)(trans: transitive _ Aeq),
+  let ASetoidClass1 := AsymmetricReflexive Contravariant refl in
+  let ASetoidClass2 := AsymmetricReflexive Covariant refl in
+   (Morphism_Theory (cons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class).
+ intros.
+ exists Aeq.
+ unfold make_compatibility_goal; simpl; unfold impl; eauto.
+Defined.
 
 (* END OF UTILITY/BACKWARD COMPATIBILITY PART *)
 
-(* A FEW EXAMPLES *)
+(* A FEW EXAMPLES ON iff *)
 
-Add Morphism iff : Iff_Morphism.
+Add Morphism iff with signature iff ==> iff ==> iff as Iff_Morphism.
  tauto.
 Qed.
 
 (* impl IS A MORPHISM *)
 
-Definition impl (A B: Prop) := A -> B.
-
-Add Morphism impl : Impl_Morphism.
+Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism.
 unfold impl; tauto.
 Qed.
 
 (* and IS A MORPHISM *)
 
-Add Morphism and : And_Morphism.
+Add Morphism and with signature iff ==> iff ==> iff as And_Morphism.
  tauto.
 Qed.
 
 (* or IS A MORPHISM *)
 
-Add Morphism or : Or_Morphism.
+Add Morphism or with signature iff ==> iff ==> iff as Or_Morphism.
  tauto.
 Qed.
 
 (* not IS A MORPHISM *)
 
-Add Morphism not : Not_Morphism.
+Add Morphism not with signature iff ==> iff as Not_Morphism.
  tauto.
 Qed.
 
-Theorem impl_refl: reflexive _ impl.
- hnf; unfold impl; tauto.
-Qed.
-
-Theorem impl_trans: transitive _ impl.
- hnf; unfold impl; tauto.
-Qed.
-
-(* THE ASYMMETRIC AREFLEXIVE RELATION impl WITH A FEW MORPHISMS *)
-
-Add Relation Prop impl reflexivity proved by impl_refl.
+(* THE SAME EXAMPLES ON impl *)
 
 Add Morphism impl with signature impl --> impl ++> impl as Impl_Morphism2.
  unfold impl; tauto.