From 5f77bf2f56b180e268b6acaa81a2fbb82a8fe026 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 18 Aug 2009 07:58:58 +0000 Subject: [PATCH] ... --- helm/software/matita/nlibrary/nat/order.ma | 15 +++- .../matita/nlibrary/sets/partitions.ma | 86 ++++++++----------- helm/software/matita/nlibrary/sets/sets.ma | 34 ++++++-- 3 files changed, 76 insertions(+), 59 deletions(-) diff --git a/helm/software/matita/nlibrary/nat/order.ma b/helm/software/matita/nlibrary/nat/order.ma index 4587e8435..fba54a26f 100644 --- 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 0ef3fa8c4..e588fd2bc 100644 --- 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 239d97659..3e63bf8f2 100644 --- 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 + }. -- 2.39.2