From: Claudio Sacerdoti Coen Date: Fri, 14 Aug 2009 17:24:45 +0000 (+0000) Subject: ... X-Git-Tag: make_still_working~3542 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c6d3537eee27d05490a9555cc7326bc954b356c5;p=helm.git ... --- diff --git a/helm/software/matita/nlibrary/datatypes/bool.ma b/helm/software/matita/nlibrary/datatypes/bool.ma new file mode 100644 index 000000000..be42b597a --- /dev/null +++ b/helm/software/matita/nlibrary/datatypes/bool.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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/pts.ma". + +ninductive bool: Type[0] ≝ + true: bool + | false: bool. \ No newline at end of file diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends index 27fb3e081..9e293ea0a 100644 --- a/helm/software/matita/nlibrary/depends +++ b/helm/software/matita/nlibrary/depends @@ -1,14 +1,20 @@ sets/sets.ma logic/connectives.ma logic/cprop.ma properties/relations1.ma sets/setoids1.ma logic/cprop.ma sets/setoids1.ma +datatypes/bool.ma logic/pts.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 properties/relations.ma logic/connectives.ma logic/pts.ma algebra/abelian_magmas.ma algebra/magmas.ma -nat/plus.ma algebra/abelian_magmas.ma algebra/unital_magmas.ma nat/nat.ma +nat/plus.ma algebra/abelian_magmas.ma algebra/unital_magmas.ma nat/big_ops.ma +nat/minus.ma nat/order.ma algebra/magmas.ma sets/sets.ma nat/nat.ma logic/equality.ma sets/setoids.ma +nat/big_ops.ma algebra/magmas.ma nat/order.ma properties/relations1.ma logic/pts.ma +nat/compare.ma datatypes/bool.ma nat/order.ma properties/relations.ma logic/pts.ma +nat/order.ma nat/nat.ma algebra/unital_magmas.ma algebra/magmas.ma logic/pts.ma +sets/partitions.ma nat/compare.ma nat/minus.ma nat/plus.ma sets/sets.ma diff --git a/helm/software/matita/nlibrary/nat/big_ops.ma b/helm/software/matita/nlibrary/nat/big_ops.ma new file mode 100644 index 000000000..bda7d7e6b --- /dev/null +++ b/helm/software/matita/nlibrary/nat/big_ops.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 "nat/order.ma". +include "algebra/magmas.ma". + +alias symbol "eq" = "leibnitz's equality". +alias id "refl" = "cic:/matita/ng/logic/equality/eq.con(0,1,2)". +nlet rec big_op (M: magma_type) (n: nat) (f: ∀m. lt m n → M) (v: M) on n : M ≝ + (match n return λx.∀p:n=x.? with + [ O ⇒ λ_.v + | S n' ⇒ λp.op ? (f n' ?) (big_op M n' ? v) ]) (refl ? n). +##[ nrewrite > p; napply le_n + | #m; #H; napply (f n'); nrewrite > p; napply le_n] +nqed. \ No newline at end of file diff --git a/helm/software/matita/nlibrary/nat/compare.ma b/helm/software/matita/nlibrary/nat/compare.ma new file mode 100644 index 000000000..2014d2aa4 --- /dev/null +++ b/helm/software/matita/nlibrary/nat/compare.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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/order.ma". +include "datatypes/bool.ma". + +naxiom decompose1: ¬(lt O O). +naxiom decompose2: ∀n. ¬(lt (S n) O). + +ndefinition ltb: ∀n,m:nat. lt n m ∨ ¬(lt n m). + #n; nelim n + [ #m; ncases m + [ napply or_intror; #H; napply (decompose1 H) + | #m'; napply or_introl; napply lt_O_Sn ] +##| #n'; #Hn'; #m; ncases m + [ napply or_intror; #H; napply (decompose2 … H) + | #m'; ncases (Hn' m') + [ #H; napply or_introl; napply le_S_S; napply H + | #H; napply or_intror; #K; napply H; napply le_S_S_to_le; napply K]##] +nqed. diff --git a/helm/software/matita/nlibrary/nat/minus.ma b/helm/software/matita/nlibrary/nat/minus.ma new file mode 100644 index 000000000..f800cc058 --- /dev/null +++ b/helm/software/matita/nlibrary/nat/minus.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 "nat/order.ma". + +nlet rec minus (n:nat) (m:nat) on m : nat ≝ + match m with + [ O ⇒ n + | S m' ⇒ + match n with + [ O ⇒ O + | S n' ⇒ minus n' m']]. + +naxiom le_minus: ∀n,m,p. le n m → le (minus n p) m. +naxiom lt_minus: ∀n,m,p. lt n m → lt (minus n p) m. \ No newline at end of file diff --git a/helm/software/matita/nlibrary/nat/nat.ma b/helm/software/matita/nlibrary/nat/nat.ma index 0fc9e3a6b..362a5ad36 100644 --- a/helm/software/matita/nlibrary/nat/nat.ma +++ b/helm/software/matita/nlibrary/nat/nat.ma @@ -23,4 +23,4 @@ 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 +unification hint 0 ((λx,y.True) (carr NAT) nat). diff --git a/helm/software/matita/nlibrary/nat/order.ma b/helm/software/matita/nlibrary/nat/order.ma new file mode 100644 index 000000000..dd8c544ae --- /dev/null +++ b/helm/software/matita/nlibrary/nat/order.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||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". + +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. + +nlemma le_O_n: ∀n. le O n. + #n; nelim n [ napply le_n | #n'; #H; napply le_S; nassumption ] +nqed. + +(* needs decompose *) +naxiom le_S_S: ∀n,m. le n m → le (S n) (S m). +naxiom le_S_S_to_le: ∀n,m. le (S n) (S m) → le n m. +naxiom lt_Sn_m: ∀n,m. lt (S n) m → lt n m. + +nlemma lt_O_Sn: ∀n. lt O (S n). + #n; napply le_S_S; napply le_O_n. +nqed. diff --git a/helm/software/matita/nlibrary/nat/plus.ma b/helm/software/matita/nlibrary/nat/plus.ma index 809288f2a..75268ffcb 100644 --- a/helm/software/matita/nlibrary/nat/plus.ma +++ b/helm/software/matita/nlibrary/nat/plus.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "nat/nat.ma". +include "nat/big_ops.ma". include "algebra/unital_magmas.ma". include "algebra/abelian_magmas.ma". @@ -50,4 +50,6 @@ ndefinition plus_unital_magma_type: unital_magma_type. | napply O | #x; napply refl | #x; (* qua manca ancora l'hint *) napply (symm plus_abelian_magma_type) ] -nqed. \ No newline at end of file +nqed. + +ndefinition big_plus ≝ λn.λf.big_op plus_magma_type n f O. \ No newline at end of file diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma new file mode 100644 index 000000000..43940e1f9 --- /dev/null +++ b/helm/software/matita/nlibrary/sets/partitions.ma @@ -0,0 +1,65 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "sets/sets.ma". +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. +*) + +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 (H1: lt m (big_plus ? s)) index (p: lt index (card ? P)) on index : A ≝ + match index return λx. lt x (card ? P) → ? with + [ O ⇒ λp'.f ??? (H O p') m ? + | S index' ⇒ λp'. + match ltb m (s index p) with + [ or_introl K ⇒ f ??? (H index p) m K + | or_intror _ ⇒ partition_splits_card_map A P s H (minus m (s index p)) ? index' ? ]] p. +##[##2: napply lt_minus; nassumption + |##3: napply lt_Sn_m; nassumption + | +nqed. + +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; napply mk_has_card + [ #m; #H1; napply partition_splits_card_map A P s H m H1 (pred (card ? P)) + | + ] +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 f94c94d9c..239d97659 100644 --- a/helm/software/matita/nlibrary/sets/sets.ma +++ b/helm/software/matita/nlibrary/sets/sets.ma @@ -211,30 +211,3 @@ 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. - -(************************** 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