From 86d3a559b94a16c571ca05defdcada6bae4cc14d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 18 Aug 2009 10:59:30 +0000 Subject: [PATCH] ... --- .../matita/nlibrary/sets/partitions.ma | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma index 6b81ce60b..f1f64f881 100644 --- a/helm/software/matita/nlibrary/sets/partitions.ma +++ b/helm/software/matita/nlibrary/sets/partitions.ma @@ -20,10 +20,11 @@ include "nat/minus.ma". alias symbol "eq" = "setoid eq". alias symbol "eq" = "setoid1 eq". 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; + class: unary_morphism1 (setoid1_of_setoid support) (qpowerclass_setoid 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 @@ -55,7 +56,21 @@ nlemma partition_splits_card: ##| #y; #_; ngeneralize in match (covers ? P) in ⊢ ?; *; #_; #Hc; ngeneralize in match (Hc y I) in ⊢ ?; *; #index; *; #Hi1; #Hi2; - nelim daemon + ngeneralize in match (f_sur ???? f ? Hi1) in ⊢ ?; *; #nindex; *; #Hni1; #Hni2; + ngeneralize in match (f_sur ???? (fi nindex) y ?) in ⊢ ? + [##2: napply (. #‡(†?));##[##3: napply Hni2 |##2: ##skip | nassumption]##] + *; #nindex2; *; #Hni21; #Hni22; + napply (ex_intro … (plus (big_plus nindex (λi.λ_.s i)) nindex2)); napply conj + [ nwhd in Hni1; nelim daemon + | nwhd in ⊢ (???%?); + (* BEL POSTO DOVE FARE UN LEMMA *) + (* invariante: Hni1; altre premesse: Hni1, Hni22 *) + nchange in Hni1 with (nindex < n); ngeneralize in match Hni1 in ⊢ ?; + nelim n + [ #A (* decompose *) + | #index'; #Hrec; + ] + ] | #x; #x'; nnormalize in ⊢ (? → ? → %); nelim daemon ] -- 2.39.2