From 7002fb8d9d0102e9baa410935fdabc9be0f8690d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 20 Aug 2009 17:50:05 +0000 Subject: [PATCH] ... --- helm/software/matita/nlibrary/nat/minus.ma | 4 +- helm/software/matita/nlibrary/nat/plus.ma | 4 +- .../matita/nlibrary/sets/partitions.ma | 98 ++++++++++++++----- 3 files changed, 79 insertions(+), 27 deletions(-) diff --git a/helm/software/matita/nlibrary/nat/minus.ma b/helm/software/matita/nlibrary/nat/minus.ma index f800cc058..86a4b1df2 100644 --- a/helm/software/matita/nlibrary/nat/minus.ma +++ b/helm/software/matita/nlibrary/nat/minus.ma @@ -22,5 +22,7 @@ nlet rec minus (n:nat) (m:nat) on m : nat ≝ [ O ⇒ O | S n' ⇒ minus n' m']]. +interpretation "natural minus" 'minus x y = (minus x y). + 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 +naxiom lt_minus: ∀n,m,p. lt n m → lt (minus n p) m. diff --git a/helm/software/matita/nlibrary/nat/plus.ma b/helm/software/matita/nlibrary/nat/plus.ma index 75268ffcb..8bbc71b9c 100644 --- a/helm/software/matita/nlibrary/nat/plus.ma +++ b/helm/software/matita/nlibrary/nat/plus.ma @@ -21,6 +21,8 @@ nlet rec plus (n:nat) (m:nat) on n : nat ≝ [ O ⇒ m | S n' ⇒ S (plus n' m) ]. +interpretation "natural plus" 'plus x y = (plus x y). + ndefinition plus_magma_type: magma_type. napply mk_magma_type [ napply NAT @@ -52,4 +54,4 @@ ndefinition plus_unital_magma_type: unital_magma_type. | #x; (* qua manca ancora l'hint *) napply (symm plus_abelian_magma_type) ] nqed. -ndefinition big_plus ≝ λn.λf.big_op plus_magma_type n f O. \ No newline at end of file +ndefinition big_plus ≝ λn.λf.big_op plus_magma_type n f O. diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma index f62c7281d..d8ba34c5c 100644 --- a/helm/software/matita/nlibrary/sets/partitions.ma +++ b/helm/software/matita/nlibrary/sets/partitions.ma @@ -25,6 +25,9 @@ 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". +alias symbol "eq" = "setoid1 eq". +alias symbol "eq" = "setoid eq". nrecord partition (A: setoid) : Type[1] ≝ { support: setoid; indexes: qpowerclass support; @@ -65,7 +68,25 @@ 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_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. +naxiom big_plus_ext: ∀n,f,f'. (∀i,p. f i p = f' i p) → big_plus n f = big_plus n f'. +naxiom ad_hoc1: ∀n,m,l. n + (m + l) = l + (n + m). +naxiom assoc: ∀n,m,l. n + m + l = n + (m + l). +naxiom lt_canc: ∀n,m,p. n < m → p + n < p + m. +naxiom ad_hoc2: ∀a,b. a < b → b - a - (b - S a) = S O. +naxiom ad_hoc3: ∀a,b. b < a → S (O + (a - S b) + b) = a. +naxiom ad_hoc4: ∀a,b. a - S b ≤ a - b. + +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: ∀A. ∀P:partition A. ∀n,s. @@ -90,20 +111,50 @@ nlemma partition_splits_card: ngeneralize in match (f_sur ???? (fi nindex) y ?) in ⊢ ? [##2: napply (. #‡(†?));##[##3: napply Hni2 |##2: ##skip | nassumption]##] *; #nindex2; *; #Hni21; #Hni22; - nletin xxx ≝ (plus match minus n nindex return λ_.nat with [ O ⇒ O | S nn ⇒ big_plus nn (λi.λ_.s (S (plus i nindex)))] nindex2); + nletin xxx ≝ (plus (big_plus (minus n nindex) (λi.λ_.s (S (plus i nindex)))) nindex2); napply (ex_intro … xxx); napply conj - [ nwhd in Hni1; nwhd; nelim daemon - | nwhd in ⊢ (???%?); + [ nwhd in Hni1; nwhd; nwhd in ⊢ (?(? %)%); + nchange with (? < plus (s n) (big_plus n ?)); + nelim (le_to_lt_or_eq … (le_S_S_to_le … Hni1)) + [##2: #E; nrewrite < E; nrewrite < (minus_canc nindex); + nwhd in ⊢ (?%?); nrewrite < E; napply lt_to_lt_plus; nassumption + | #L; nrewrite > (split_big_plus n (S nindex) (λm.λ_.s m) L); + nrewrite > (split_big_plus (n - nindex) (n - S nindex) (λi.λ_.s (S (i+nindex))) ?) + [ ngeneralize in match (big_plus_ext (n - S nindex) + (λi,p.s (S (i+nindex))) (λi,p.s (i + S nindex)) ?) in ⊢ ? + [ #E; + napply (eq_rect_CProp0_r ?? + (λx:nat.λ_. x + big_plus (n - nindex - (n - S nindex)) + (λi,p.s (S (i + (n - S nindex)+nindex))) + nindex2 < + s n + (big_plus (S nindex) (λi,p.s i) + + big_plus (n - S nindex) (λi,p. s (i + S nindex)))) ? ? E); + nrewrite > (ad_hoc1 (s n) (big_plus (S nindex) (λi,p.s i)) + (big_plus (n - S nindex) (λi,p. s (i + S nindex)))); + napply (eq_rect_CProp0_r + ?? (λx.λ_.x < ?) ?? (assoc + (big_plus (n - S nindex) (λi,p.s (i + S nindex))) + (big_plus (n - nindex - (n - S nindex)) + (λi,p.s (S (i + (n - S nindex)+nindex)))) + nindex2)); + napply lt_canc; + nrewrite > (ad_hoc2 … L); nwhd in ⊢ (?(?%?)?); + nrewrite > (ad_hoc3 … L); + napply (eq_rect_CProp0_r ?? (λx.λ_.x < ?) ?? (assoc …)); + napply lt_canc; nnormalize in ⊢ (?%?); nwhd in ⊢ (??%); + napply lt_to_lt_plus; nassumption + ##|##2: #i; #_; nrewrite > (S_plus i nindex); napply refl] + ##| napply ad_hoc4]##] + ##| nwhd in ⊢ (???%?); nchange in Hni1 with (nindex < S n); ngeneralize in match (le_S_S_to_le … Hni1) in ⊢ ?; nwhd in ⊢ (? → ???(???????%?)?); napply (nat_rect_CProp0 (λx. nindex ≤ x → - partition_splits_card_map A P (S n) s f fi + eq_rel (carr A) (eq A) + (partition_splits_card_map A P (S n) s f fi (plus - match minus x nindex with - [ O ⇒ O | S nn ⇒ big_plus nn (λi.λ_.s (S (plus i nindex)))] - nindex2) x = y) ?? n) + (big_plus (minus x nindex) (λi.λ_:i < minus x nindex.s (S (plus i nindex)))) + nindex2) x) y) ?? n) [ #K; nrewrite < (minus_O_n nindex); nwhd in ⊢ (???(???????%?)?); nwhd in ⊢ (???%?); nchange in Hni21 with (nindex2 < s nindex); ngeneralize in match (le_O_to_eq … K) in ⊢ ?; #K'; @@ -115,31 +166,28 @@ nlemma partition_splits_card: | #n'; #Hrec; #HH; nelim (le_to_lt_or_eq … HH) [##2: #K; nrewrite < K; nrewrite < (minus_canc nindex); nwhd in ⊢ (???(???????%?)?); - (*???????*) - ##| #K; nwhd in ⊢ (???%?); + nrewrite > K; + nwhd in ⊢ (???%?); nrewrite < K; nrewrite > (ltb_t … Hni21); + nwhd in ⊢ (???%?); nassumption + ##| #K; ngeneralize in match (le_S_S_to_le … K) in ⊢ ?; #K'; + nwhd in ⊢ (???%?); + + + XXX; nrewrite > (minus_S n' nindex ?) [##2: napply le_S_S_to_le; nassumption] ngeneralize in match (? : - match S (minus n' nindex) with [O ⇒ O | S nn ⇒ big_plus nn (λi.λ_.s (S (plus i nindex)))] - = big_plus (minus n' nindex) (λi.λ_.s (S (plus i nindex)))) in ⊢ ? [##2: napply refl] - #He; napply (eq_rect_CProp0_r ?? - (λx.λ_. - match ltb (plus x nindex2) (s (S n')) with - [ true ⇒ iso_f ???? (fi (S n')) (plus x nindex2) - | false ⇒ ?(*partition_splits_card_map A P (S n) s f fi - (minus (plus x nindex2) (s (S n'))) n'*) - ] = y) - ?? He); - ngeneralize in match (? : - ltb (plus (big_plus (minus n' nindex) (λi.λ_.s (S (plus i nindex)))) nindex2) + ltb (plus (big_plus (S (minus n' nindex)) (λi.λ_.s (S (plus i nindex)))) nindex2) (s (S n')) = false) in ⊢ ? [ #Hc; nrewrite > Hc; nwhd in ⊢ (???%?); nelim (le_to_lt_or_eq … (le_S_S_to_le … K)) [ ##| #E; ngeneralize in match Hc in ⊢ ?; nrewrite < E; nrewrite < (minus_canc nindex); - nwhd in ⊢ (??(?%?)? → ?); - nrewrite > E in Hni21; #E'; nchange in E' with (nindex2 < s n'); - ngeneralize in match Hni21 in ⊢ ?; + nnormalize in ⊢ (??(?%?)? → ?); + nrewrite > (plus_n_O (s (S nindex))); + nrewrite > (ltb_f (plus (s (S nindex)) nindex2) (s (S nindex)) ?); + + XXX; ngeneralize in match (? : -- 2.39.2