From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 21 Aug 2009 18:11:10 +0000 (+0000)
Subject: Towards a simplified proof.
X-Git-Tag: make_still_working~3525
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7508af658c85b26d0af929c85069bae18bc6546a;p=helm.git

Towards a simplified proof.
---

diff --git a/helm/software/matita/nlibrary/datatypes/pairs.ma b/helm/software/matita/nlibrary/datatypes/pairs.ma
new file mode 100644
index 000000000..dfff0c3f8
--- /dev/null
+++ b/helm/software/matita/nlibrary/datatypes/pairs.ma
@@ -0,0 +1,20 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "logic/pts.ma".
+
+nrecord pair (A,B: Type[0]) : Type[0] ≝
+ { fst: A;
+   snd: B
+ }.
\ No newline at end of file
diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends
index 9e293ea0a..f39678fb8 100644
--- a/helm/software/matita/nlibrary/depends
+++ b/helm/software/matita/nlibrary/depends
@@ -5,6 +5,7 @@ sets/setoids1.ma properties/relations1.ma sets/setoids.ma
 sets/setoids.ma logic/connectives.ma properties/relations.ma
 logic/equality.ma logic/connectives.ma properties/relations.ma
 logic/connectives.ma logic/pts.ma
+datatypes/pairs.ma logic/pts.ma
 algebra/abelian_magmas.ma algebra/magmas.ma
 nat/plus.ma algebra/abelian_magmas.ma algebra/unital_magmas.ma nat/big_ops.ma
 nat/minus.ma nat/order.ma
@@ -14,7 +15,7 @@ nat/big_ops.ma algebra/magmas.ma nat/order.ma
 properties/relations1.ma logic/pts.ma
 nat/compare.ma datatypes/bool.ma nat/order.ma
 properties/relations.ma logic/pts.ma
-nat/order.ma nat/nat.ma
+nat/order.ma nat/nat.ma sets/sets.ma
 algebra/unital_magmas.ma algebra/magmas.ma
 logic/pts.ma 
-sets/partitions.ma nat/compare.ma nat/minus.ma nat/plus.ma sets/sets.ma
+sets/partitions.ma datatypes/pairs.ma nat/compare.ma nat/minus.ma nat/plus.ma sets/sets.ma
diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma
index 13aeb028e..d87ccd3a9 100644
--- a/helm/software/matita/nlibrary/sets/partitions.ma
+++ b/helm/software/matita/nlibrary/sets/partitions.ma
@@ -16,6 +16,7 @@ include "sets/sets.ma".
 include "nat/plus.ma".
 include "nat/compare.ma".
 include "nat/minus.ma".
+include "datatypes/pairs.ma".
 
 alias symbol "eq" = "setoid eq".
 alias symbol "eq" = "setoid1 eq".
@@ -29,6 +30,7 @@ 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;
@@ -40,6 +42,76 @@ nrecord partition (A: setoid) : Type[1] ≝
 
 naxiom daemon: False.
 
+nlet rec iso_nat_nat_union (s: nat → nat) m index on index : pair nat nat ≝
+ match ltb m (s index) with
+  [ true ⇒ mk_pair … index m
+  | false ⇒
+     match index with
+      [ O ⇒ (* dummy value: it could be an elim False: *) mk_pair … O O
+      | S index' ⇒ iso_nat_nat_union s (minus m (s index)) index']].
+
+alias symbol "eq" = "leibnitz's equality".
+naxiom plus_n_O: ∀n. plus n O = n.
+naxiom ltb_t: ∀n,m. n < m → ltb n m = true.
+naxiom ltb_f: ∀n,m. ¬ (n < m) → ltb n m = false.
+naxiom ltb_cases: ∀n,m. (n < m ∧ ltb n m = true) ∨ (¬ (n < m) ∧ ltb n m = false).
+naxiom minus_canc: ∀n. minus n n = O.
+naxiom ad_hoc9: ∀a,b,c. a < b + c → a - b < c.
+naxiom ad_hoc10: ∀a,b,c. a - b = c → a = b + c.
+naxiom ad_hoc11: ∀a,b. a - b ≤ S a - b.
+naxiom ad_hoc12: ∀a,b. b ≤ a → S a - b - (a - b) = S O.
+naxiom ad_hoc13: ∀a,b. b ≤ a → (O + (a - b)) + b = a.
+naxiom ad_hoc14: ∀a,b,c,d,e. c ≤ a → a - c = b + d + e → a = b + (c + d) + e.
+naxiom not_lt_to_le: ∀a,b. ¬ (a < b) → b ≤ a.
+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.
+
+ntheorem iso_nat_nat_union_char:
+ ∀n:nat. ∀s: nat → nat. ∀m:nat. m < big_plus (S n) (λi.λ_.s i) →
+  let p ≝ iso_nat_nat_union s m n in
+   m = big_plus (n - fst … p) (λi.λ_.s (S (i + fst … p))) + snd … p ∧
+    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 conj [ napply conj [ napply refl | napply le_n ] ##| nassumption ]
+##| #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));
+       ngeneralize in match (Hrec (m - s (S n')) ?) in ⊢ ?
+        [##2: napply ad_hoc9; nassumption] *; *; #Hrec1; #Hrec2; #Hrec3; napply conj
+        [##2: nassumption
+        |napply conj
+         [napply (eq_rect_CProp0_r ?? (λx.λ_. m = x + snd … (iso_nat_nat_union s (m - s (S n')) n')) ??
+           (split_big_plus
+            (S n' - fst … (iso_nat_nat_union s (m - s (S n')) n'))
+            (n' - fst … (iso_nat_nat_union s (m - s (S n')) n'))
+            (λi.λ_.s (S (i + fst … (iso_nat_nat_union s (m - s (S n')) n'))))?))
+           [##2: napply ad_hoc11]
+          napply (eq_rect_CProp0_r ?? (λx.λ_. ? = ? + big_plus x (λ_.λ_:? < x.?) + ?)
+           ?? (ad_hoc12 n' (fst … (iso_nat_nat_union s (m - s (S n')) n')) ?))
+            [##2: nassumption]
+          nwhd in ⊢ (???(?(??%)?));
+          nrewrite > (ad_hoc13 n' (fst … (iso_nat_nat_union s (m - s (S n')) n')) ?)
+           [##2: nassumption]
+          napply ad_hoc14 [ napply not_lt_to_le; nassumption ]
+          nwhd in ⊢ (???(?(??%)?));
+          napply (eq_rect_CProp0_r ?? (λx.λ_. ? = x + ?) ??
+           (plus_n_O (big_plus (n' - fst … (iso_nat_nat_union s (m - s (S n')) n'))
+            (λi.λ_.s (S (i + fst … (iso_nat_nat_union s (m - s (S n')) n')))))));
+          nassumption
+        | napply le_S; nassumption ]##]##]##]
+nqed.
+
+
 nlet rec partition_splits_card_map
  A (P:partition A) n s (f:isomorphism ?? (Nat_ n) (indexes ? P))
  (fi: ∀i. isomorphism ?? (Nat_ (s i)) (class ? P (iso_f ???? f i))) m index
@@ -59,7 +131,6 @@ naxiom big_union_preserves_iso:
 
 naxiom le_to_lt_or_eq: ∀n,m. n ≤ m → n < m ∨ n = m.
 alias symbol "eq" = "leibnitz's equality".
-naxiom minus_canc: ∀n. O = minus n n.
 naxiom lt_to_ltb_t: ∀n,m. ∀P: bool → CProp[0]. P true → n < m → P (ltb n m).
 naxiom lt_to_ltb_f: ∀n,m. ∀P: bool → CProp[0]. P false → ¬ (n < m) → P (ltb n m).
 naxiom lt_to_minus: ∀n,m. n < m →  S (minus (minus m n) (S O)) = minus m n.
@@ -69,9 +140,6 @@ 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_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.
@@ -87,16 +155,6 @@ 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 →
-   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_output:
  ∀A. ∀P:partition A. ∀n,s.