...

diff --git a/helm/software/matita/nlibrary/nat/order.ma b/helm/software/matita/nlibrary/nat/order.ma
index 4587e84351aa7ffbd756ca1a73860be6fae27510..fba54a26f7c5b728f60846ffdf1093c26bfe7340 100644 (file)
--- a/helm/software/matita/nlibrary/nat/order.ma
+++ b/helm/software/matita/nlibrary/nat/order.ma
@@ -13,12 +13,19 @@
 (**************************************************************************)
 
 include "nat/nat.ma".
+include "sets/sets.ma".
 
 ninductive le (n: nat) : nat → CProp[0] ≝
    le_n: le n n
  | le_S: ∀m. le n m → le n (S m).
 
-ndefinition lt ≝ λn,m. le (S n) m.
+interpretation "natural 'less or equal to'" 'leq x y = (le x y).
+interpretation "natural 'neither less nor equal to'" 'nleq x y = (Not (le x y)).
+
+ndefinition lt ≝ λn,m. S n ≤ m.
+
+interpretation "natural 'less than'" 'lt x y = (lt x y).
+interpretation "natural 'not less than'" 'nless x y = (Not (lt x y)).
 
 nlemma le_O_n: ∀n. le O n.
  #n; nelim n [ napply le_n | #n'; #H; napply le_S; nassumption ]
@@ -34,3 +41,9 @@ naxiom lt_le_trans: ∀n,m,p. lt n m → le m p → lt n p.
 nlemma lt_O_Sn: ∀n. lt O (S n).
  #n; napply le_S_S; napply le_O_n.
 nqed. 
+
+ndefinition Nat_: nat → qpowerclass NAT.
+ #n; napply mk_qpowerclass
+  [ napply {m | m < n}
+  | #x; #x'; #H; nrewrite < H; napply mk_iff; #K; nassumption (* refl non va *) ]
+nqed.

diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma
index 0ef3fa8c4a4b5d44ac35219a17a626e71a47b6b7..e588fd2bc2273d91b1e4122697ec7c0d0717da3b 100644 (file)
--- a/helm/software/matita/nlibrary/sets/partitions.ma
+++ b/helm/software/matita/nlibrary/sets/partitions.ma
@@ -17,59 +17,45 @@ include "nat/plus.ma".
 include "nat/compare.ma".
 include "nat/minus.ma".
 
-(* sbaglia a fare le proiezioni *)
-nrecord finite_partition (A: Type[0]) : Type[1] ≝ 
- { card: nat;
-   class: ∀n. lt n card → Ω \sup A;
-   inhabited: ∀i,p. class i p ≬ class i p(*;
-   disjoint: ∀i,j,p,p'. class i p ≬ class j p' → i=j;
-   covers: big_union ?? class = full_set A*)
- }.
-
-nrecord has_card (A: Type[0]) (S: Ω \sup A) (n: nat) : CProp[0] ≝
- { f: ∀m:nat. lt m n → A;
-   in_S: ∀m.∀p:lt m n. f ? p ∈ S (*;
-   f_inj: injective ?? f;
-   f_sur: surjective ?? f*)
- }.
-
-(*
-nlemma subset_of_finite:
- ∀A. ∃n. has_card ? (full_subset A) n → ∀S. ∃m. has_card ? S m.
-nqed.
-*)
+alias symbol "eq" = "setoid eq".
+alias symbol "eq" = "setoid1 eq".
+nrecord partition (A: setoid) : Type[1] ≝ 
+ { support: setoid;
+   indexes: qpowerclass support;
+   class: support → qpowerclass A;
+   inhabited: ∀i. i ∈ indexes → class i ≬ class i;
+   disjoint: ∀i,j. i ∈ indexes → j ∈ indexes → class i ≬ class j → i=j;
+   covers: big_union support ? ? (λx.class x) = full_set A
+ }. napply indexes; nqed.
 
 naxiom daemon: False.
 
 nlet rec partition_splits_card_map
- A (P: finite_partition A) (s: ∀i. lt i (card ? P) → nat)
-  (H:∀i.∀p: lt i (card ? P). has_card ? (class ? P i p) (s i p))
-  m index on index:
-  le (S index) (card ? P) → lt m (big_plus (S index) (λi,p. s i ?)) → lt index (card ? P) → A ≝
- match index return λx. le (S x) (card ? P) → lt m (big_plus (S x) ?) → lt x (card ? P) → ? with
-  [ O ⇒ λL,H1,p.f ??? (H O p) m ?
-  | S index' ⇒ λL,H1,p.
-     match ltb m (s (S index') p) with
-      [ or_introl K ⇒ f ??? (H (S index') p) m K 
-      | or_intror _ ⇒ partition_splits_card_map A P s H (minus m (s (S index') p)) index' ??? ]].
-##[##3: napply lt_minus; nelim daemon (*nassumption*)
-  |##4: napply lt_Sn_m; nassumption
-  |##5: napply (lt_le_trans … p); nassumption
-##|##2: napply lt_to_le; nassumption
-##|##1: nnormalize in H1; nelim daemon ]
-nqed.
-(*
+ A (P:partition A) n s (f:isomorphism ?? (Nat_ n) (indexes ? P))
+ (fi: ∀i. isomorphism ?? (Nat_ (s i)) (class ? P (iso_f ???? f i))) m index
+ on index : A ≝
+ match ltb m (s index) with
+  [ or_introl _ ⇒ iso_f ???? (fi index) m
+  | or_intror _ ⇒
+     match index with
+      [ O ⇒ (* dummy value: it could be an elim False: *) iso_f ???? (fi O) O
+      | S index' ⇒
+         partition_splits_card_map A P n s f fi (minus m (s index)) index']].  
+
 nlemma partition_splits_card:
- ∀A. ∀P: finite_partition A. ∀s: ∀i. lt i (card ? P) → nat.
-  (∀i.∀p: lt i (card ? P). has_card ? (class ? P i p) (s i p)) →
-   has_card A (full_set A) (big_plus (card ? P) s).
- #A; #P; #s; #H; ncases (card A P)
-  [ nnormalize; napply mk_has_card
-     [ #m; #H; nelim daemon
-     | #m; #H; nelim daemon ]
-##| #c; napply mk_has_card
-  [ #m; #H1; napply partition_splits_card_map A P s H m H1 (pred (card ? P))
-  |
+ ∀A. ∀P:partition A. ∀n,s.
+  ∀f:isomorphism ?? (Nat_ n) (indexes ? P).
+   (∀i. isomorphism ?? (Nat_ (s i)) (class ? P (iso_f ???? f i))) →
+    (isomorphism ?? (Nat_ (big_plus n (λi.λ_.s i))) (Full_set A)).
+ #A; #P; #n; #s; #f; #fi; napply mk_isomorphism
+  [ napply mk_unary_morphism
+     [ napply (λm.partition_splits_card_map A P n s f fi m n)
+     | #a; #a'; #H; nrewrite < H; napply refl ]
+##| #y; #_;
+    ngeneralize in match (covers ? P) in ⊢ ?; *; #_; #Hc;
+    ngeneralize in match (Hc y I) in ⊢ ?; *; #index; *; #Hi1; #Hi2;
+    nelim daemon
+  | #x; #x'; nnormalize in ⊢ (? → ? → %);
+    nelim daemon
   ]
-nqed.
-*)
\ No newline at end of file
+nqed.
\ No newline at end of file

diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index 239d9765989b05867a552d217c32acc564002152..3e63bf8f2574fee8eba104a243c6176e83832e39 100644 (file)
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -34,9 +34,9 @@ interpretation "intersect" 'intersects U V = (intersect ? U V).
 ndefinition union ≝ λA.λU,V:Ω \sup A.{ x | x ∈ U ∨ x ∈ V }.
 interpretation "union" 'union U V = (union ? U V).
 
-ndefinition big_union ≝ λA.λT:Type[0].λf:T → Ω \sup A.{ x | ∃i. x ∈ f i }.
+ndefinition big_union ≝ λA,B.λT:Ω \sup A.λf:A → Ω \sup B.{ x | ∃i. i ∈ T ∧ x ∈ f i }.
 
-ndefinition big_intersection ≝ λA.λT:Type[0].λf:T → Ω \sup A.{ x | ∀i. x ∈ f i }.
+ndefinition big_intersection ≝ λA,B.λT:Ω \sup A.λf:A → Ω \sup B.{ x | ∀i. i ∈ T → x ∈ f i }.
 
 ndefinition full_set: ∀A. Ω \sup A ≝ λA.{ x | True }.
 (* bug dichiarazione coercion qui *)
@@ -80,6 +80,13 @@ nrecord qpowerclass (A: setoid) : Type[1] ≝
    mem_ok': ∀x,x':A. x=x' → (x ∈ pc) = (x' ∈ pc) 
  }.
 
+ndefinition Full_set: ∀A. qpowerclass A.
+ #A; napply mk_qpowerclass
+  [ napply (full_set A)
+  | #x; #x'; #H; nnormalize in ⊢ (?%?%%); (* bug universi qui napply refl1;*)
+    napply mk_iff; #K; nassumption ]
+nqed.
+
 ndefinition qseteq: ∀A. equivalence_relation1 (qpowerclass A).
  #A; napply mk_equivalence_relation1
   [ napply (λS,S':qpowerclass A. eq_rel1 ? (eq1 (powerclass_setoid A)) S S')
@@ -198,16 +205,27 @@ nlemma first_omomorphism_theorem_functions1:
  #A; #B; #f; #x; napply refl;
 nqed.
 
-ndefinition surjective ≝ λA,B.λf:unary_morphism A B. ∀y.∃x. f x = y.
+ndefinition surjective ≝
+ λA,B.λS: qpowerclass A.λT: qpowerclass B.λf:unary_morphism A B.
+  ∀y. y ∈ T → ∃x. x ∈ S ∧ f x = y.
 
-ndefinition injective ≝ λA,B.λf:unary_morphism A B. ∀x,x'. f x = f x' → x = x'.
+ndefinition injective ≝
+ λA,B.λS: qpowerclass A.λf:unary_morphism A B.
+  ∀x,x'. x ∈ S → x' ∈ S → f x = f x' → x = x'.
 
 nlemma first_omomorphism_theorem_functions2:
- ∀A,B.∀f: unary_morphism A B. surjective ?? (canonical_proj ? (eqrel_of_morphism ?? f)).
- #A; #B; #f; nwhd; #y; napply (ex_intro … y); napply refl.
+ ∀A,B.∀f: unary_morphism A B. surjective ?? (Full_set ?) (Full_set ?) (canonical_proj ? (eqrel_of_morphism ?? f)).
+ #A; #B; #f; nwhd; #y; #Hy; napply (ex_intro … y); napply conj
+  [ napply I | napply refl]
 nqed.
 
 nlemma first_omomorphism_theorem_functions3:
- ∀A,B.∀f: unary_morphism A B. injective ?? (quotiented_mor ?? f).
- #A; #B; #f; nwhd; #x; #x'; #H; nassumption.
+ ∀A,B.∀f: unary_morphism A B. injective ?? (Full_set ?) (quotiented_mor ?? f).
+ #A; #B; #f; nwhd; #x; #x'; #Hx; #Hx'; #K; nassumption.
 nqed.
+
+nrecord isomorphism (A) (B) (S: qpowerclass A) (T: qpowerclass B) : CProp[0] ≝
+ { iso_f:> unary_morphism A B;
+   f_sur: surjective ?? S T iso_f;
+   f_inj: injective ?? S iso_f
+ }.