From 7508af658c85b26d0af929c85069bae18bc6546a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 21 Aug 2009 18:11:10 +0000 Subject: [PATCH] Towards a simplified proof. --- .../matita/nlibrary/datatypes/pairs.ma | 20 +++++ helm/software/matita/nlibrary/depends | 5 +- .../matita/nlibrary/sets/partitions.ma | 86 ++++++++++++++++--- 3 files changed, 95 insertions(+), 16 deletions(-) create mode 100644 helm/software/matita/nlibrary/datatypes/pairs.ma diff --git a/helm/software/matita/nlibrary/datatypes/pairs.ma b/helm/software/matita/nlibrary/datatypes/pairs.ma new file mode 100644 index 000000000..dfff0c3f8 --- /dev/null +++ b/helm/software/matita/nlibrary/datatypes/pairs.ma @@ -0,0 +1,20 @@ +(**************************************************************************) +(* ___ *) +(* ||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". + +nrecord pair (A,B: Type[0]) : Type[0] ≝ + { fst: A; + snd: B + }. \ No newline at end of file diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends index 9e293ea0a..f39678fb8 100644 --- a/helm/software/matita/nlibrary/depends +++ b/helm/software/matita/nlibrary/depends @@ -5,6 +5,7 @@ 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 +datatypes/pairs.ma logic/pts.ma algebra/abelian_magmas.ma algebra/magmas.ma nat/plus.ma algebra/abelian_magmas.ma algebra/unital_magmas.ma nat/big_ops.ma nat/minus.ma nat/order.ma @@ -14,7 +15,7 @@ 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 +nat/order.ma nat/nat.ma sets/sets.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 +sets/partitions.ma datatypes/pairs.ma nat/compare.ma nat/minus.ma nat/plus.ma sets/sets.ma diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma index 13aeb028e..d87ccd3a9 100644 --- a/helm/software/matita/nlibrary/sets/partitions.ma +++ b/helm/software/matita/nlibrary/sets/partitions.ma @@ -16,6 +16,7 @@ include "sets/sets.ma". include "nat/plus.ma". include "nat/compare.ma". include "nat/minus.ma". +include "datatypes/pairs.ma". alias symbol "eq" = "setoid eq". alias symbol "eq" = "setoid1 eq". @@ -29,6 +30,7 @@ alias symbol "eq" = "setoid eq". alias symbol "eq" = "setoid1 eq". alias symbol "eq" = "setoid eq". alias symbol "eq" = "setoid1 eq". +alias symbol "eq" = "setoid eq". nrecord partition (A: setoid) : Type[1] ≝ { support: setoid; indexes: qpowerclass support; @@ -40,6 +42,76 @@ nrecord partition (A: setoid) : Type[1] ≝ naxiom daemon: False. +nlet rec iso_nat_nat_union (s: nat → nat) m index on index : pair nat nat ≝ + match ltb m (s index) with + [ true ⇒ mk_pair … index m + | false ⇒ + match index with + [ O ⇒ (* dummy value: it could be an elim False: *) mk_pair … O O + | S index' ⇒ iso_nat_nat_union s (minus m (s index)) index']]. + +alias symbol "eq" = "leibnitz's equality". +naxiom plus_n_O: ∀n. plus n O = n. +naxiom ltb_t: ∀n,m. n < m → ltb n m = true. +naxiom ltb_f: ∀n,m. ¬ (n < m) → ltb n m = false. +naxiom ltb_cases: ∀n,m. (n < m ∧ ltb n m = true) ∨ (¬ (n < m) ∧ ltb n m = false). +naxiom minus_canc: ∀n. minus n n = O. +naxiom ad_hoc9: ∀a,b,c. a < b + c → a - b < c. +naxiom ad_hoc10: ∀a,b,c. a - b = c → a = b + c. +naxiom ad_hoc11: ∀a,b. a - b ≤ S a - b. +naxiom ad_hoc12: ∀a,b. b ≤ a → S a - b - (a - b) = S O. +naxiom ad_hoc13: ∀a,b. b ≤ a → (O + (a - b)) + b = a. +naxiom ad_hoc14: ∀a,b,c,d,e. c ≤ a → a - c = b + d + e → a = b + (c + d) + e. +naxiom not_lt_to_le: ∀a,b. ¬ (a < b) → b ≤ a. +naxiom split_big_plus: + ∀n,m,f. m ≤ n → + big_plus n f = big_plus m (λi,p.f i ?) + big_plus (n - m) (λi.λp.f (i + m) ?). + nelim daemon. +nqed. + +ntheorem iso_nat_nat_union_char: + ∀n:nat. ∀s: nat → nat. ∀m:nat. m < big_plus (S n) (λi.λ_.s i) → + let p ≝ iso_nat_nat_union s m n in + m = big_plus (n - fst … p) (λi.λ_.s (S (i + fst … p))) + snd … p ∧ + fst … p ≤ n ∧ snd … p < s (fst … p). + #n; #s; nelim n + [ #m; nwhd in ⊢ (??% → let p ≝ % in ?); nwhd in ⊢ (??(??%) → ?); + nrewrite > (plus_n_O (s O)); #H; nrewrite > (ltb_t … H); nnormalize; + napply conj [ napply conj [ napply refl | napply le_n ] ##| nassumption ] +##| #n'; #Hrec; #m; nwhd in ⊢ (??% → let p ≝ % in ?); #H; + ncases (ltb_cases m (s (S n'))); *; #H1; #H2; nrewrite > H2; + nwhd in ⊢ (let p ≝ % in ?); nwhd + [ napply conj [napply conj + [ nwhd in ⊢ (????(?(?%(λ_.λ_:(??%).?))%)); nrewrite > (minus_canc n'); napply refl + | nnormalize; napply le_n] + ##| nnormalize; nassumption ] + ##| nchange in H with (m < s (S n') + big_plus (S n') (λi.λ_.s i)); + ngeneralize in match (Hrec (m - s (S n')) ?) in ⊢ ? + [##2: napply ad_hoc9; nassumption] *; *; #Hrec1; #Hrec2; #Hrec3; napply conj + [##2: nassumption + |napply conj + [napply (eq_rect_CProp0_r ?? (λx.λ_. m = x + snd … (iso_nat_nat_union s (m - s (S n')) n')) ?? + (split_big_plus + (S n' - fst … (iso_nat_nat_union s (m - s (S n')) n')) + (n' - fst … (iso_nat_nat_union s (m - s (S n')) n')) + (λi.λ_.s (S (i + fst … (iso_nat_nat_union s (m - s (S n')) n'))))?)) + [##2: napply ad_hoc11] + napply (eq_rect_CProp0_r ?? (λx.λ_. ? = ? + big_plus x (λ_.λ_:? < x.?) + ?) + ?? (ad_hoc12 n' (fst … (iso_nat_nat_union s (m - s (S n')) n')) ?)) + [##2: nassumption] + nwhd in ⊢ (???(?(??%)?)); + nrewrite > (ad_hoc13 n' (fst … (iso_nat_nat_union s (m - s (S n')) n')) ?) + [##2: nassumption] + napply ad_hoc14 [ napply not_lt_to_le; nassumption ] + nwhd in ⊢ (???(?(??%)?)); + napply (eq_rect_CProp0_r ?? (λx.λ_. ? = x + ?) ?? + (plus_n_O (big_plus (n' - fst … (iso_nat_nat_union s (m - s (S n')) n')) + (λi.λ_.s (S (i + fst … (iso_nat_nat_union s (m - s (S n')) n'))))))); + nassumption + | napply le_S; nassumption ]##]##]##] +nqed. + + nlet rec partition_splits_card_map 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 @@ -59,7 +131,6 @@ naxiom big_union_preserves_iso: naxiom le_to_lt_or_eq: ∀n,m. n ≤ m → n < m ∨ n = m. alias symbol "eq" = "leibnitz's equality". -naxiom minus_canc: ∀n. O = minus n n. naxiom lt_to_ltb_t: ∀n,m. ∀P: bool → CProp[0]. P true → n < m → P (ltb n m). naxiom lt_to_ltb_f: ∀n,m. ∀P: bool → CProp[0]. P false → ¬ (n < m) → P (ltb n m). naxiom lt_to_minus: ∀n,m. n < m → S (minus (minus m n) (S O)) = minus m n. @@ -69,9 +140,6 @@ naxiom minus_lt_to_lt: ∀n,m,p. n < p → minus n m < p. naxiom minus_O_n: ∀n. O = minus O n. naxiom le_O_to_eq: ∀n. n ≤ O → n=O. naxiom lt_to_minus_to_S: ∀n,m. m < n → ∃k. minus n m = S k. -naxiom ltb_t: ∀n,m. n < m → ltb n m = true. -naxiom ltb_f: ∀n,m. ¬ (n < m) → ltb n m = false. -naxiom plus_n_O: ∀n. plus n O = n. naxiom not_lt_plus: ∀n,m. ¬ (plus n m < n). naxiom lt_to_lt_plus: ∀n,m,l. n < m → n < m + l. naxiom S_plus: ∀n,m. S (n + m) = n + S m. @@ -87,16 +155,6 @@ naxiom ad_hoc6: ∀a,b. b ≤ a → a - b + b = a. naxiom ad_hoc7: ∀a,b,c. a + (b + O) + c - b = a + c. naxiom ad_hoc8: ∀a,b,c. ¬ (a + (b + O) + c < b). naxiom ltb_elim_CProp0: ∀n,m. ∀P: bool → CProp[0]. (n < m → P true) → (¬ (n < m) → P false) → P (ltb n m). -naxiom ltb_cases: ∀n,m. (n < m ∧ ltb n m = true) ∨ (¬ (n < m) ∧ ltb n m = false). -naxiom ad_hoc9: ∀a,b,c. a ≤ b + c → a - b ≤ c. -naxiom not_lt_to_le: ∀a,b. ¬ (a < b) → b ≤ a. - - -naxiom split_big_plus: - ∀n,m,f. m ≤ n → - big_plus n f = big_plus m (λi,p.f i ?) + big_plus (n - m) (λi.λp.f (i + m) ?). - nelim daemon. -nqed. nlemma partition_splits_card_output: ∀A. ∀P:partition A. ∀n,s. -- 2.39.2