From: Claudio Sacerdoti Coen Date: Thu, 20 Aug 2009 18:26:54 +0000 (+0000) Subject: Injectivity proved! What a mess... X-Git-Tag: make_still_working~3527 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c8992252558a6fb61eb503a37ccdf29b5cbb3fc4;p=helm.git Injectivity proved! What a mess... --- diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma index d8ba34c5c..acdd6a687 100644 --- a/helm/software/matita/nlibrary/sets/partitions.ma +++ b/helm/software/matita/nlibrary/sets/partitions.ma @@ -81,6 +81,11 @@ 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 ad_hoc5: ∀a. S a - a = S O. +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 split_big_plus: ∀n,m,f. m ≤ n → @@ -171,111 +176,29 @@ nlemma partition_splits_card: 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 (? : - 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); - nnormalize in ⊢ (??(?%?)? → ?); - nrewrite > (plus_n_O (s (S nindex))); - nrewrite > (ltb_f (plus (s (S nindex)) nindex2) (s (S nindex)) ?); - - XXX; - - - ngeneralize in match (? : - minus (plus (big_plus (minus n' nindex) (λi.λ_.s (S (plus i nindex)))) nindex2) - (s (S n')) - = - plus - match minus n' nindex with - [ O ⇒ O | S nn ⇒ big_plus nn (λi.λ_.s (S (plus i nindex)))] nindex2) - in ⊢ ? - [ #F; nrewrite > F; napply Hrec; napply le_S_S_to_le; nassumption - | nelim (le_to_lt_or_eq … (le_S_S_to_le … K)) - [ - ##| #E; nrewrite < E; nrewrite < (minus_canc nindex); nnormalize; - - nwhd in ⊢ (???%); - ] - - - nrewrite > He; - - - nnormalize in ⊢ (???%?); - - - - nelim (le_to_lt_or_eq … K) - [##2: #K'; nrewrite > K'; nrewrite < (minus_canc n); nnormalize; - napply (eq_rect_CProp0 nat nindex (λx:nat.λ_.partition_splits_card_map A P (S n) s f fi nindex2 x = y) ? n K'); - nchange in Hni21 with (nindex2 < s nindex); ngeneralize in match Hni21 in ⊢ ?; - ngeneralize in match Hni22 in ⊢ ?; - nelim nindex - [ #X1; #X2; nwhd in ⊢ (??? % ?); - napply (lt_to_ltb_t ???? X2); #D; nwhd in ⊢ (??? % ?); nassumption - | #n0; #_; #X1; #X2; nwhd in ⊢ (??? % ?); - napply (lt_to_ltb_t ???? X2); #D; nwhd in ⊢ (??? % ?); nassumption] - ##| #K'; ngeneralize in match (lt_to_minus … K') in ⊢ ?; #K2; - napply (eq_rect_CProp0 ?? (λx.λ_.?) ? ? K2); (* uffa, ancora??? *) - nwhd in ⊢ (??? (???????(?%?)?) ?); - ngeneralize in match K' in ⊢ ?; - napply (nat_rect_CProp0 - (λx. nindex < x → - partition_splits_card_map A P (S n) s f fi - (plus (big_op plus_magma_type (minus (minus x nindex) (S O)) - (λi.λ_.s (S (plus i nindex))) O) nindex2) x = y) ?? n) - [ #A; nelim (not_lt_O … A) - | #n'; #Hrec; #X; nwhd in ⊢ (???%?); - ngeneralize in match - (? : ¬ ((plus (big_op plus_magma_type (minus (minus (S n') nindex) (S O)) - (λi.λ_.s (S (plus i nindex))) O) nindex2) < s (S n'))) in ⊢ ? - [ #B1; napply (lt_to_ltb_f ???? B1); #B1'; nwhd in ⊢ (???%?); - nrewrite > (minus_S n' nindex …) [##2: napply le_S_S_to_le; nassumption] - ngeneralize in match (le_S_S_to_le … X) in ⊢ ?; #X'; - nelim (le_to_lt_or_eq … X') - [##2: #X''; - nchange in Hni21 with (nindex2 < s nindex); ngeneralize in match Hni21 in ⊢ ?; - nrewrite > X''; nrewrite < (minus_canc n'); - nrewrite < (minus_canc (S O)); nnormalize in ⊢ (? → %); - nelim n' - [ #Y; nwhd in ⊢ (??? % ?); - ngeneralize in match (minus_lt_to_lt ? (s (S O)) ? Y) in ⊢ ?; #Y'; - napply (lt_to_ltb_t … Y'); #H; nwhd in ⊢ (???%?); - - nrewrite > (minus_S (minus n' nindex) (S O) …) [##2: - - XXX; - - nelim n in f K' ⊢ ? - [ #A; nelim daemon; - - (* BEL POSTO DOVE FARE UN LEMMA *) - (* invariante: Hni1; altre premesse: Hni1, Hni22 *) - nelim n in ⊢ (% → ??? (????????%) ?) - [ #A (* decompose *) - | #index'; #Hrec; #K; nwhd in ⊢ (???%?); - nelim (ltb xxx (s (S index'))); - #K1; nwhd in ⊢ (???%?) - [ - - nindex < S index' + 1 - +^{nindex} (s i) w < s (S index') - S index' == nindex - - | - ] - ] - ] - | #x; #x'; nnormalize in ⊢ (? → ? → %); + ngeneralize in match (?: + ¬ (big_plus (S n' - nindex) (λi,p.s (S (i+nindex))) + nindex2 < s (S n'))) in ⊢ ? + [ #N; nrewrite > (ltb_f … N); nwhd in ⊢ (???%?); + ngeneralize in match (Hrec K') in ⊢ ?; #Hrec'; + napply (eq_rect_CProp0_r ?? + (λx,p. eq_rel (carr A) (eq A) (partition_splits_card_map A P (S n) s f fi + (big_plus x ? + ? - ?) n') y) ?? (minus_S n' nindex K')); + nrewrite > (split_big_plus (S (n' - nindex)) (n' - nindex) + (λi,p.s (S (i+nindex))) (le_S ?? (le_n ?))); + nrewrite > (ad_hoc5 (n' - nindex)); + nnormalize in ⊢ (???(???????(?(?(??%)?)?)?)?); + nrewrite > (ad_hoc6 … K'); + nrewrite > (ad_hoc7 (big_plus (n' - nindex) (λi,p.s (S (i+nindex)))) + (s (S n')) nindex2); + nassumption + | nrewrite > (minus_S … K'); + nrewrite > (split_big_plus (S (n' - nindex)) (n' - nindex) + (λi,p.s (S (i+nindex))) (le_S ?? (le_n ?))); + nrewrite > (ad_hoc5 (n' - nindex)); + nnormalize in ⊢ (?(?(?(??%)?)?)); + nrewrite > (ad_hoc6 … K'); + napply ad_hoc8]##]##]##] +##| #x; #x'; nnormalize in ⊢ (? → ? → %); nelim daemon ] nqed. @@ -287,9 +210,11 @@ ndefinition partition_of_compatible_equivalence_relation: #A; #R; napply mk_partition [ napply (quotient ? R) | napply Full_set - | #a; napply mk_qpowerclass - [ napply {x | R x a} - | #x; #x'; #H; nnormalize; napply mk_iff; #K; nelim daemon] + | napply mk_unary_morphism1 + [ #a; napply mk_qpowerclass + [ napply {x | R x a} + | #x; #x'; #H; nnormalize; napply mk_iff; #K; nelim daemon] + ##| #a; #a'; #H; napply conj; #x; nnormalize; #K [ nelim daemon | nelim daemon]##] ##| #x; #_; nnormalize; napply (ex_intro … x); napply conj; napply refl | #x; #x'; #_; #_; nnormalize; *; #x''; *; #H1; #H2; napply (trans ?????? H2); napply sym; nassumption