From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 18 Aug 2009 08:29:25 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~3535
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2dc6ec0db2156431948014a6498c9901f8759e39;p=helm.git

...
---

diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma
index e588fd2bc..6b81ce60b 100644
--- a/helm/software/matita/nlibrary/sets/partitions.ma
+++ b/helm/software/matita/nlibrary/sets/partitions.ma
@@ -19,6 +19,7 @@ include "nat/minus.ma".
 
 alias symbol "eq" = "setoid eq".
 alias symbol "eq" = "setoid1 eq".
+alias symbol "eq" = "setoid eq".
 nrecord partition (A: setoid) : Type[1] ≝ 
  { support: setoid;
    indexes: qpowerclass support;
@@ -58,4 +59,21 @@ nlemma partition_splits_card:
   | #x; #x'; nnormalize in ⊢ (? → ? → %);
     nelim daemon
   ]
+nqed.
+
+(************** equivalence relations vs partitions **********************)
+
+ndefinition partition_of_compatible_equivalence_relation:
+ ∀A:setoid. compatible_equivalence_relation A → partition A.
+ #A; #R; napply mk_partition
+  [ napply (quotient ? R)
+  | napply Full_set
+  | #a; napply mk_qpowerclass
+     [ napply {x | R x a}
+     | #x; #x'; #H; nnormalize; napply mk_iff; #K; nelim daemon]
+##| #x; #_; nnormalize; napply (ex_intro … x); napply conj; napply refl
+  | #x; #x'; #_; #_; nnormalize; *; #x''; *; #H1; #H2; napply (trans ?????? H2);
+    napply sym; nassumption
+  | nnormalize; napply conj
+     [ #a; #_; napply I | #a; #_; napply (ex_intro … a); napply conj [ napply I | napply refl]##]
 nqed.
\ No newline at end of file