A very little bit of arithmetic.

diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends
index bd4b2744bbf6c5b285c210da0acbd6d6fbf35f09..a7952ea4d575ee9b0d6e453c7983a80722db32e6 100644 (file)
--- a/helm/software/matita/nlibrary/depends
+++ b/helm/software/matita/nlibrary/depends
@@ -1,10 +1,12 @@
-sets/sets.ma logic/cprop.ma
+sets/sets.ma logic/connectives.ma logic/cprop.ma properties/relations1.ma sets/setoids1.ma
 logic/cprop.ma sets/setoids1.ma
 sets/setoids1.ma properties/relations1.ma sets/setoids.ma
 sets/setoids.ma logic/connectives.ma properties/relations.ma
-logic/equality.ma logic/connectives.ma
+logic/equality.ma logic/connectives.ma properties/relations.ma
 logic/connectives.ma logic/pts.ma
+nat/plus.ma algebra/magmas.ma nat/nat.ma
 algebra/magmas.ma sets/sets.ma
+nat/nat.ma logic/equality.ma sets/setoids.ma
 properties/relations1.ma logic/pts.ma
 properties/relations.ma logic/pts.ma
 logic/pts.ma 

diff --git a/helm/software/matita/nlibrary/logic/equality.ma b/helm/software/matita/nlibrary/logic/equality.ma
index 1da7e1b0be4ec611643009b61780a08a09505cd8..6de962747e31baa5776de06e853ec5ad87cdbe45 100644 (file)
--- a/helm/software/matita/nlibrary/logic/equality.ma
+++ b/helm/software/matita/nlibrary/logic/equality.ma
@@ -13,10 +13,19 @@
 (**************************************************************************)
 
 include "logic/connectives.ma".
+include "properties/relations.ma".
 
-ninductive eq (A: Type) (a: A) : A → CProp ≝
+ninductive eq (A: Type[0]) (a: A) : A → CProp[0] ≝
  refl: eq A a a.
 
 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
 
 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
+
+ndefinition EQ: ∀A:Type[0]. equivalence_relation A.
+ #A; napply mk_equivalence_relation
+  [ napply eq
+  | napply refl
+  | #x; #y; #H; nrewrite < H; napply refl
+  | #x; #y; #z; #Hyx; #Hxz; nrewrite < Hxz; nassumption]
+nqed.

diff --git a/helm/software/matita/nlibrary/nat/nat.ma b/helm/software/matita/nlibrary/nat/nat.ma
new file mode 100644 (file)
index 0000000..0fc9e3a
--- /dev/null
+++ b/helm/software/matita/nlibrary/nat/nat.ma
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "logic/equality.ma".
+include "sets/setoids.ma".
+
+ninductive nat: Type[0] ≝
+   O: nat
+ | S: nat → nat.
+
+ndefinition NAT: setoid.
+ napply mk_setoid [ napply nat | napply EQ]
+nqed.
+
+unification hint 0 ((λx,y.True) (carr NAT) nat).
\ No newline at end of file

diff --git a/helm/software/matita/nlibrary/nat/plus.ma b/helm/software/matita/nlibrary/nat/plus.ma
new file mode 100644 (file)
index 0000000..62fe491
--- /dev/null
+++ b/helm/software/matita/nlibrary/nat/plus.ma
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "nat/nat.ma".
+include "algebra/magmas.ma".
+
+nlet rec plus (n:nat) (m:nat) on n : nat ≝
+ match n with
+  [ O ⇒ m
+  | S n' ⇒ S (plus n' m) ].
+
+ndefinition plus_magma_type: magma_type.
+ napply mk_magma_type
+  [ napply NAT
+  | napply mk_binary_morphism
+     [ napply plus
+     | #a; #a'; #b; #b'; #Ha; #Hb; nrewrite < Ha; nrewrite < Hb; napply refl ]##]
+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 a7e033c15c43119ecec9380f98fa0769fc2c7236..f94c94d9cba79e2c7ad10d8a25753a3e408ade0a 100644 (file)
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -34,6 +34,14 @@ 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_intersection ≝ λA.λT:Type[0].λf:T → Ω \sup A.{ x | ∀i. x ∈ f i }.
+
+ndefinition full_set: ∀A. Ω \sup A ≝ λA.{ x | True }.
+(* bug dichiarazione coercion qui *)
+(* ncoercion full_set : ∀A:Type[0]. Ω \sup A ≝ full_set on _A: Type[0] to (Ω \sup ?). *)
+
 nlemma subseteq_refl: ∀A.∀S: Ω \sup A. S ⊆ S.
  #A; #S; #x; #H; nassumption.
 nqed.
@@ -59,7 +67,9 @@ ndefinition powerclass_setoid: Type[0] → setoid1.
  #A; napply mk_setoid1
   [ napply (Ω \sup A)
   | napply seteq ]
-nqed. 
+nqed.
+
+unification hint 0 (∀A. (λx,y.True) (carr1 (powerclass_setoid A)) (Ω \sup A)).
 
 (************ SETS OVER SETOIDS ********************)
 
@@ -200,4 +210,31 @@ 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.
-nqed.
\ No newline at end of file
+nqed.
+
+(************************** partitions ****************************)
+
+nrecord partition (A: Type[0]) : Type[1] ≝ 
+ { index_set: setoid;
+   class: index_set → Ω \sup A;
+   disjoint: ∀i,j. ¬ (i = j) → ¬(class i ≬ class j);
+   covers: big_union ?? class = full_set A
+ }.
+
+(*
+nrecord has_card (A: Type[0]) (S: Ω \sup A) (n: nat) : Prop ≝
+ { f: ∀m:nat. m < n → 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.
+
+nlemma partition_splits_card:
+ ∀A. ∀P: partition A. ∀s: index_set P → nat.
+  (∀i. has_card ? (class i) = s i) →
+   has_card ? (full_subset A) (big_plus ? (λi. s i)).
+nqed.
+*)
\ No newline at end of file