From d70944c1513aa63e6494e58595fcc4214a2f6c68 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 20 Aug 2009 13:33:48 +0000
Subject: [PATCH] - Bug fixed in definition of big_op. - ltb now goes to
 booleans - the meaning of big_x n is to sum from 0 to (pred n);   in
 particular big_x O is the neutral element.   Thus the isomorphism is broken.

---
 helm/software/matita/nlibrary/nat/big_ops.ma  |  2 +-
 helm/software/matita/nlibrary/nat/compare.ma  | 12 +--
 .../matita/nlibrary/sets/partitions.ma        | 94 ++++++++++++++++---
 3 files changed, 90 insertions(+), 18 deletions(-)

diff --git a/helm/software/matita/nlibrary/nat/big_ops.ma b/helm/software/matita/nlibrary/nat/big_ops.ma
index bda7d7e6b..1d2a0e27a 100644
--- a/helm/software/matita/nlibrary/nat/big_ops.ma
+++ b/helm/software/matita/nlibrary/nat/big_ops.ma
@@ -22,5 +22,5 @@ nlet rec big_op (M: magma_type) (n: nat) (f: ∀m. lt m n → M) (v: M) on n : M
    [ O ⇒ λ_.v
    | S n' ⇒ λp.op ? (f n' ?) (big_op M n' ? v) ]) (refl ? n).
 ##[ nrewrite > p; napply le_n
-  | #m; #H; napply (f n'); nrewrite > p; napply le_n]
+  | #m; #H; napply (f m); nrewrite > p; napply le_S; nassumption]
 nqed.
\ No newline at end of file
diff --git a/helm/software/matita/nlibrary/nat/compare.ma b/helm/software/matita/nlibrary/nat/compare.ma
index 2014d2aa4..354e61a5a 100644
--- a/helm/software/matita/nlibrary/nat/compare.ma
+++ b/helm/software/matita/nlibrary/nat/compare.ma
@@ -18,14 +18,14 @@ include "datatypes/bool.ma".
 naxiom decompose1: ¬(lt O O).
 naxiom decompose2: ∀n. ¬(lt (S n) O).
 
-ndefinition ltb: ∀n,m:nat. lt n m ∨ ¬(lt n m).
+ndefinition ltb: nat → nat → bool.
  #n; nelim n
   [ #m; ncases m
-    [ napply or_intror; #H; napply (decompose1 H)
-    | #m'; napply or_introl; napply lt_O_Sn ]
+    [ napply false
+    | #m'; napply true ]
 ##| #n'; #Hn'; #m; ncases m
-    [ napply or_intror; #H; napply (decompose2 … H)
+    [ napply false
     | #m'; ncases (Hn' m')
-       [ #H; napply or_introl; napply le_S_S; napply H
-       | #H; napply or_intror; #K; napply H; napply le_S_S_to_le; napply K]##]
+       [ napply true
+       | napply false]##]
 nqed.
diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma
index 23fd3ecea..f62c7281d 100644
--- a/helm/software/matita/nlibrary/sets/partitions.ma
+++ b/helm/software/matita/nlibrary/sets/partitions.ma
@@ -23,6 +23,8 @@ 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".
+alias symbol "eq" = "setoid1 eq".
 nrecord partition (A: setoid) : Type[1] ≝ 
  { support: setoid;
    indexes: qpowerclass support;
@@ -39,8 +41,8 @@ nlet rec partition_splits_card_map
  (fi: ∀i. isomorphism ?? (Nat_ (s i)) (class ? P (iso_f ???? f i))) m index
  on index : A ≝
  match ltb m (s index) with
-  [ or_introl _ ⇒ iso_f ???? (fi index) m
-  | or_intror _ ⇒
+  [ true ⇒ iso_f ???? (fi index) m
+  | false ⇒
      match index with
       [ O ⇒ (* dummy value: it could be an elim False: *) iso_f ???? (fi O) O
       | S index' ⇒
@@ -52,17 +54,18 @@ naxiom big_union_preserves_iso:
    big_union A B T f = big_union A' B T' (λx.f (iso_f ???? g x)).
 
 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: n < m ∨ ¬ (n < m) → CProp[0].
-  (∀H: n < m. P (or_introl ?? H)) → n < m → P (ltb n m).
-naxiom lt_to_ltb_f:
- ∀n,m. ∀P: n < m ∨ ¬ (n < m) → CProp[0].
-  (∀H: ¬ (n < m). P (or_intror ?? H)) → ¬ (n < m) → P (ltb n m).
+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.
 naxiom not_lt_O: ∀n. ¬ (n < O).
 naxiom minus_S: ∀n,m. m ≤ n → minus (S n) m = S (minus n m).
-naxiom minus_lt_to_lt: ∀n,m,p. n < p → minus n m < p. 
+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. 
 
 nlemma partition_splits_card:
  ∀A. ∀P:partition A. ∀n,s.
@@ -92,8 +95,77 @@ nlemma partition_splits_card:
      [ nwhd in Hni1; nwhd; nelim daemon
      | nwhd in ⊢ (???%?);
        nchange in Hni1 with (nindex < S n);
-       ngeneralize in match (le_S_S_to_le … Hni1) in ⊢ ?; #K;
-       nwhd in ⊢ (???(???????%?)?);
+       ngeneralize in match (le_S_S_to_le … Hni1) in ⊢ ?;
+       nwhd in ⊢ (? → ???(???????%?)?);
+       napply (nat_rect_CProp0
+        (λx. nindex ≤ x →
+          partition_splits_card_map A P (S n) s f fi
+           (plus
+             match minus x nindex with
+              [ O ⇒ O | S nn ⇒ big_plus nn (λi.λ_.s (S (plus i nindex)))]
+             nindex2) x = y) ?? n)
+        [ #K; nrewrite < (minus_O_n nindex); nwhd in ⊢ (???(???????%?)?);
+          nwhd in ⊢ (???%?); nchange in Hni21 with (nindex2 < s nindex);
+          ngeneralize in match (le_O_to_eq … K) in ⊢ ?; #K';
+          ngeneralize in match Hni21 in ⊢ ?;
+          ngeneralize in match Hni22 in ⊢ ?;
+          nrewrite > K' in ⊢ (% → % → ?); #K1; #K2;
+          nrewrite > (ltb_t … K2);
+          nwhd in ⊢ (???%?); nassumption
+        | #n'; #Hrec; #HH; nelim (le_to_lt_or_eq … HH)
+           [##2: #K; nrewrite < K; nrewrite < (minus_canc nindex);
+            nwhd in ⊢ (???(???????%?)?);
+            (*???????*)
+         ##| #K; nwhd in ⊢ (???%?);
+             nrewrite > (minus_S n' nindex ?) [##2: napply le_S_S_to_le; nassumption]
+             ngeneralize in match (? :
+              match S (minus n' nindex) with [O ⇒ O | S nn ⇒ big_plus nn (λi.λ_.s (S (plus i nindex)))]
+              = big_plus (minus n' nindex) (λi.λ_.s (S (plus i nindex)))) in ⊢ ? [##2: napply refl]
+             #He; napply (eq_rect_CProp0_r ??
+              (λx.λ_.
+                match ltb (plus x nindex2) (s (S n')) with
+                 [ true ⇒ iso_f ???? (fi (S n')) (plus x nindex2)
+                 | false ⇒ ?(*partition_splits_card_map A P (S n) s f fi
+                     (minus (plus x nindex2) (s (S n'))) n'*)
+                 ] = y)
+              ?? He);
+             ngeneralize in match (? :
+              ltb (plus (big_plus (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);
+                    nwhd in ⊢ (??(?%?)? → ?);
+                    nrewrite > E in Hni21; #E'; nchange in E' with (nindex2 < s n'); 
+                    ngeneralize in match Hni21 in ⊢ ?;
+                    
+               
+                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');
-- 
2.39.2