From 899222fb394af9ee449cd6618e6e38ce30b45ca8 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 18 Jan 2010 12:40:38 +0000 Subject: [PATCH] More // everywhere. --- .../matita/nlibrary/sets/partitions.ma | 79 +++++++------------ 1 file changed, 29 insertions(+), 50 deletions(-) diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma index de29e796c..84d320e7f 100644 --- a/helm/software/matita/nlibrary/sets/partitions.ma +++ b/helm/software/matita/nlibrary/sets/partitions.ma @@ -72,46 +72,29 @@ ntheorem iso_nat_nat_union_char: 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 refl | napply le_n ] ##| nassumption ] + nrewrite > (plus_n_O (s O)); #H; nrewrite > (ltb_t … H); nnormalize; @; /2/ ##| #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)); - nlapply (Hrec (m - s (S n')) ?) - [ napply ad_hoc9; nassumption] *; *; #Hrec1; #Hrec2; #Hrec3; @ - [##2: nassumption - |@ - [nrewrite > (split_big_plus …); ##[##2:napply ad_hoc11;##|##3:##skip] - nrewrite > (ad_hoc12 …); ##[##2: nassumption] - nwhd in ⊢ (???(?(??%)?)); - nrewrite > (ad_hoc13 …);##[##2: nassumption] - napply ad_hoc14 [ napply not_lt_to_le; nassumption ] - nwhd in ⊢ (???(?(??%)?)); - nrewrite > (plus_n_O …); - nassumption; - ##| napply le_S; nassumption ]##]##]##] + [ napply conj [napply conj; //; + nwhd in ⊢ (???(?(?%(λ_.λ_:(??%).?))%)); nrewrite > (minus_canc n'); // + ##| nnormalize; // ] +##| nchange in H with (m < s (S n') + big_plus (S n') (λi.λ_.s i)); + nlapply (Hrec (m - s (S n')) ?); /2/; *; *; #Hrec1; #Hrec2; #Hrec3; @; //; @; /2/; + nrewrite > (split_big_plus …); ##[##2:napply ad_hoc11;##|##3:##skip] + nrewrite > (ad_hoc12 …); //; + nwhd in ⊢ (???(?(??%)?)); + nrewrite > (ad_hoc13 …); //; + napply ad_hoc14; /2/; + nwhd in ⊢ (???(?(??%)?)); + nrewrite > (plus_n_O …); // ##]##] nqed. ntheorem iso_nat_nat_union_pre: ∀n:nat. ∀s: nat → nat. ∀i1,i2. i1 ≤ n → i2 < s i1 → big_plus (n - i1) (λi.λ_.s (S (i + i1))) + i2 < big_plus (S n) (λi.λ_.s i). - #n; #s; #i1; #i2; #H1; #H2; - nrewrite > (split_big_plus (S n) (S i1) (λi.λ_.s i) ?) - [##2: napply le_to_le_S_S; nassumption] - napply ad_hoc15 - [ nwhd in ⊢ (???(?%?)); - napply big_plus_preserves_ext; #i; #_; - nrewrite > (plus_n_S i i1); napply refl - | nrewrite > (split_big_plus (S i1) i1 (λi.λ_.s i) ?) [##2: napply le_S; napply le_n] - napply ad_hoc16; nrewrite > (minus_S i1); nnormalize; nrewrite > (plus_n_O (s i1) …); - nassumption ] -nqed. +/2/. nqed. ntheorem iso_nat_nat_union_uniq: ∀n:nat. ∀s: nat → nat. @@ -159,24 +142,22 @@ napply (. #‡(†?));##[##2: napply Hni2 |##1: ##skip | nassumption]##] *; *; #K1; #K2; #K3; nlapply (iso_nat_nat_union_uniq n s nindex (fst … (iso_nat_nat_union s xxx n)) - nindex2 (snd … (iso_nat_nat_union s xxx n)) ?????) - [##6: *; #E1; #E2; nrewrite > E1; nrewrite > E2; napply refl - |##5: napply le_S_S_to_le; nassumption - |##*: nassumption]##] + nindex2 (snd … (iso_nat_nat_union s xxx n)) ?????); /2/ + [##2: *; #E1; #E2; nrewrite > E1; nrewrite > E2; // + | nassumption ]##] ##| #x; #x'; nnormalize in ⊢ (? → ? → %); #Hx; #Hx'; #E; ncut(∀i1,i2,i1',i2'. i1 ∈ Nat_ (S n) → i1' ∈ Nat_ (S n) → i2 ∈ Nat_ (s i1) → i2' ∈ Nat_ (s i1') → eq_rel (carr A) (eq A) (fi i1 i2) (fi i1' i2') → i1=i1' ∧ i2=i2'); ##[ #i1; #i2; #i1'; #i2'; #Hi1; #Hi1'; #Hi2; #Hi2'; #E; nlapply(disjoint … P (f i1) (f i1') ???) - [##2,3: napply f_closed; nassumption + [##2,3: napply f_closed; // |##1: @ (fi i1 i2); @; - ##[ napply f_closed; nassumption ##| alias symbol "refl" = "refl1". + ##[ napply f_closed; // ##| alias symbol "refl" = "refl1". napply (. E‡#); - nwhd; napply f_closed; nassumption]##] - #E'; ncut(i1 = i1'); ##[ napply (f_inj … E'); nassumption; ##] - #E''; nrewrite < E''; @; - ##[ @; - ##| nrewrite < E'' in E; #E'''; napply (f_inj … E''') - [ nassumption | nrewrite > E''; nassumption ]##]##] + nwhd; napply f_closed; //]##] + #E'; ncut(i1 = i1'); ##[ napply (f_inj … E'); // ##] + #E''; nrewrite < E''; @; //; + nrewrite < E'' in E; #E'''; napply (f_inj … E'''); //; + nrewrite > E''; // ]##] ##] #K; nelim (iso_nat_nat_union_char n s x Hx); *; #i1x; #i2x; #i3x; nelim (iso_nat_nat_union_char n s x' Hx'); *; #i1x'; #i2x'; #i3x'; @@ -186,7 +167,7 @@ napply (. E‡#); *; #K1; #K2; napply (eq_rect_CProp0_r ?? (λX.λ_.? = X) ?? i1x'); napply (eq_rect_CProp0_r ?? (λX.λ_.X = ?) ?? i1x); - nrewrite > K1; nrewrite > K2; napply refl ] + nrewrite > K1; nrewrite > K2; napply refl. nqed. (************** equivalence relations vs partitions **********************) @@ -201,9 +182,7 @@ ndefinition partition_of_compatible_equivalence_relation: [ 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 - | nnormalize; napply conj - [ #a; #_; napply I | #a; #_; napply (ex_intro … a); napply conj [ napply I | napply refl]##] -nqed. +##| #x; #_; nnormalize; /3/ + | #x; #x'; #_; #_; nnormalize; *; #x''; *; /3/ + | nnormalize; napply conj; /4/ ] +nqed. \ No newline at end of file -- 2.39.2