From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 21 Aug 2009 16:26:56 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~3526
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e1320ba487853135dc2706d5b7864dbc46706495;p=helm.git

...
---

diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma
index acdd6a687..13aeb028e 100644
--- a/helm/software/matita/nlibrary/sets/partitions.ma
+++ b/helm/software/matita/nlibrary/sets/partitions.ma
@@ -28,6 +28,7 @@ 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".
 nrecord partition (A: setoid) : Type[1] ≝ 
  { support: setoid;
    indexes: qpowerclass support;
@@ -85,7 +86,11 @@ 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 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 →
@@ -93,6 +98,24 @@ naxiom split_big_plus:
  nelim daemon.
 nqed.
 
+nlemma partition_splits_card_output:
+ ∀A. ∀P:partition A. ∀n,s.
+  ∀f:isomorphism ?? (Nat_ (S n)) (indexes ? P).
+   ∀fi:∀i. isomorphism ?? (Nat_ (s i)) (class ? P (iso_f ???? f i)).
+    ∀x. x ∈ Nat_ (big_plus (S n) (λi.λ_.s i)) →
+     ∃i1.∃i2. partition_splits_card_map A P (S n) s f fi x n = iso_f ???? (fi i1) i2.
+ #A; #P; #n; #s; #f; #fi;
+ nelim n in ⊢ (? → % → ??(λ_.??(λ_.???(????????%)?)))
+  [ #x; nnormalize in ⊢ (% → ?); nrewrite > (plus_n_O (s O)); nchange in ⊢ (% → ?) with (x < s O);
+    #H; napply (ex_intro … O); napply (ex_intro … x); nwhd in ⊢ (???%?);
+    nrewrite > (ltb_t … H); nwhd in ⊢ (???%?); napply refl
+  | #n'; #Hrec; #x; #Hx; nwhd in ⊢ (??(λ_.??(λ_.???%?))); nwhd in Hx; nwhd in Hx: (??%);
+    nelim (ltb_cases x (s (S n'))); *; #K1; #K2; nrewrite > K2; nwhd in ⊢ (??(λ_.??(λ_.???%?)))
+     [ napply (ex_intro … (S n')); napply (ex_intro … x); napply refl
+     | napply (Hrec (x - s (S n')) ?); nwhd; nrewrite < (minus_S x (s (S n')) ?)
+       [ napply ad_hoc9; nassumption | napply not_lt_to_le; nassumption ]##]
+nqed.
+
 nlemma partition_splits_card:
  ∀A. ∀P:partition A. ∀n,s.
   ∀f:isomorphism ?? (Nat_ n) (indexes ? P).
@@ -198,8 +221,21 @@ nlemma partition_splits_card:
                 nnormalize in ⊢ (?(?(?(??%)?)?));
                 nrewrite > (ad_hoc6 … K');
                 napply ad_hoc8]##]##]##]
-##| #x; #x'; nnormalize in ⊢ (? → ? → %);
-    nelim daemon
+##| #x; #x'; nnormalize in ⊢ (? → ? → %); #Hx; #Hx';
+    nelim (partition_splits_card_output A P n s f fi x Hx); #i1x; *; #i2x; #Ex;
+    nelim (partition_splits_card_output A P n s f fi x' Hx'); #i1x'; *; #i2x'; #Ex';
+    ngeneralize in match (? :
+     iso_f ???? fi i1x(* ≬ iso_f ???? (fi i1x'))*)) in ⊢ ?;
+    #E; napply (f_inj ???? (fi i1x));
+    
+    nelim n in ⊢ (% → % → (???(????????%)(????????%)) → ?)
+     [ nnormalize in ⊢ (% → % → ?); nrewrite > (plus_n_O (s O));
+       nchange in ⊢ (% → ?) with (x < s O);
+       nchange in ⊢ (? → % → ?) with (x' < s O);
+       #H1; #H2; nwhd in ⊢ (???%% → ?);
+       nrewrite > (ltb_t … H1); nrewrite > (ltb_t … H2); nwhd in ⊢ (???%% → ?);
+       napply f_inj; nassumption
+     | #n'; #Hrec; #Hx; #Hx'; nwhd in ⊢ (???%% → ?);
   ]
 nqed.