From a0c0e92cee3ed99995e12b02f18e30f018d946ea Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 12 Aug 2009 15:04:04 +0000 Subject: [PATCH] A very little bit of arithmetic. --- helm/software/matita/nlibrary/depends | 6 ++- .../matita/nlibrary/logic/equality.ma | 11 ++++- helm/software/matita/nlibrary/nat/nat.ma | 26 ++++++++++++ helm/software/matita/nlibrary/nat/plus.ma | 29 +++++++++++++ helm/software/matita/nlibrary/sets/sets.ma | 41 ++++++++++++++++++- 5 files changed, 108 insertions(+), 5 deletions(-) create mode 100644 helm/software/matita/nlibrary/nat/nat.ma create mode 100644 helm/software/matita/nlibrary/nat/plus.ma diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends index bd4b2744b..a7952ea4d 100644 --- 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 1da7e1b0b..6de962747 100644 --- 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 index 000000000..0fc9e3a6b --- /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 index 000000000..62fe4917a --- /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 a7e033c15..f94c94d9c 100644 --- 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 -- 2.39.2