From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 7 Jan 2007 18:17:56 +0000 (+0000)
Subject: Bug fixed in definition of cic:/.../setoids/make_compatibility_goal_aux.con:
X-Git-Tag: make_still_working~6534
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=964e55a1dcdec5a602ff7952d0fba7b7ff5981b0;p=helm.git

Bug fixed in definition of cic:/.../setoids/make_compatibility_goal_aux.con:
two generalizes were done in the wrong order, permuting the arguments and
making every relation change its variance!
---

diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma
index 5c19f925e..7b672ae63 100644
--- a/helm/software/matita/library/technicalities/setoids.ma
+++ b/helm/software/matita/library/technicalities/setoids.ma
@@ -107,8 +107,8 @@ definition make_compatibility_goal_aux:
  ∀In,Out.∀f,g:function_type_of_morphism_signature In Out.Prop.
  intros 2; 
  elim In (a); simplify in f f1;
- generalize in match f; clear f;
  generalize in match f1; clear f1;
+ generalize in match f; clear f;
   [ elim a; simplify in f f1;
      [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
      | elim t;
@@ -250,18 +250,24 @@ definition equality_morphism_of_symmetric_reflexive_transitive_relation:
   ]
 qed.
 
-(*
 definition equality_morphism_of_asymmetric_areflexive_transitive_relation:
- ∀(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; auto.
+ ∀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;
+ apply mk_Morphism_Theory;
+ [ simplify;
+   apply Aeq
+ | simplify;
+   intros;
+   whd;
+   intros;
+   auto
+ ].
 qed.
 
-definition equality_morphism_of_asymmetric_reflexive_transitive_relation:
+(*definition equality_morphism_of_asymmetric_reflexive_transitive_relation:
  ∀(A: Type)(Aeq: relation A)(refl: reflexive ? Aeq)(trans: transitive ? Aeq).
   let ASetoidClass1 := AsymmetricReflexive Contravariant refl in
   let ASetoidClass2 := AsymmetricReflexive Covariant refl in