X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Farithmetics%2Fbigops.ma;h=6bcd62a653b38465021da0bb395700089e4afd70;hb=b4681c749d6e8812fe86d5a9adbf4d4acbc3df06;hp=3211814db099d89326c46bbc9dfb6d5cde551f21;hpb=53452958508001e7af3090695b619fe92135fb9e;p=helm.git

diff --git a/matita/matita/lib/arithmetics/bigops.ma b/matita/matita/lib/arithmetics/bigops.ma
index 3211814db..6bcd62a65 100644
--- a/matita/matita/lib/arithmetics/bigops.ma
+++ b/matita/matita/lib/arithmetics/bigops.ma
@@ -67,7 +67,7 @@ for @{'bigop ($b-$a) $op $nil (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
   
 notation "\big  [ op , nil ]_{ ident j ∈ [a,b[ } f"
   with precedence 80
-for @{'bigop ($b-$a) $op $nil (λ${ident j}.((λ${ident j}.$true) (${ident j}+$a)))
+for @{'bigop ($b-$a) $op $nil (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.  
  
 (* notation "\big  [ op , nil ]_{( term 50) a ≤ ident j < b | p } f"
@@ -142,13 +142,29 @@ a ≤ b → b ≤ c →
       \big[op,nil]_{i ∈ [a,b[ |p i}(f i).
 #a #b # c #p #B #nil #op #f #leab #lebc 
 >(plus_minus_m_m (c-a) (b-a)) in ⊢ (??%?) /2/
->minus_minus >(commutative_plus a) <plus_minus_m_m //
+>minus_plus >(commutative_plus a) <plus_minus_m_m //
 >bigop_sum (cut (∀i. b -a ≤ i → i+a = i-(b-a)+b))
   [#i #lei >plus_minus // <plus_minus1 
      [@eq_f @sym_eq @plus_to_minus /2/ | /2/]] 
 #H @same_bigop #i #ltic @leb_elim normalize // #lei <H //
 qed.   
 
+theorem bigop_a: ∀a,b,B.∀nil.∀op:Aop B nil.∀f:nat→B. a ≤ b →
+\big[op,nil]_{i∈[a,S b[ }(f i) = 
+  op (\big[op,nil]_{i ∈ [a,b[ }(f (S i))) (f a).
+#a #b #B #nil #op #f #leab 
+>(bigop_sumI a (S a) (S b)) [|@le_S_S //|//] @eq_f2 
+  [@same_bigop // |<minus_Sn_n normalize @nilr]
+qed.
+  
+theorem bigop_0: ∀n,B.∀nil.∀op:Aop B nil.∀f:nat→B.
+\big[op,nil]_{i < S n}(f i) = 
+  op (\big[op,nil]_{i < n}(f (S i))) (f 0).
+#n #B #nil #op #f 
+<bigop_I >bigop_a [|//] @eq_f2 [|//] <minus_n_O 
+@same_bigop //
+qed.    
+
 theorem bigop_prod: ∀k1,k2,p1,p2,B.∀nil.∀op:Aop B nil.∀f: nat →nat → B.
 \big[op,nil]_{x<k1|p1 x}(\big[op,nil]_{i<k2|p2 x i}(f x i)) =
   \big[op,nil]_{i<k1*k2|andb (p1 (div i k2)) (p2 (div i k2) (i \mod k2))}
@@ -169,7 +185,19 @@ record ACop (A:Type[0]) (nil:A) : Type[0] ≝
   {aop :> Aop A nil; 
    comm: ∀a,b.aop a b = aop b a
   }.
-  
+ 
+lemma bigop_op: ∀k,p,B.∀nil.∀op:ACop B nil.∀f,g: nat → B.
+op (\big[op,nil]_{i<k|p i}(f i)) (\big[op,nil]_{i<k|p i}(g i)) =
+  \big[op,nil]_{i<k|p i}(op (f i) (g i)).
+#k #p #B #nil #op #f #g (elim k) [normalize @nill]
+-k #k #Hind (cases (true_or_false (p k))) #H
+  [>bigop_Strue // >bigop_Strue // >bigop_Strue //
+   normalize <assoc <assoc in ⊢ (???%) @eq_f >assoc >comm in ⊢ (??(????%?)?) 
+   <assoc @eq_f @Hind
+  |>bigop_Sfalse // >bigop_Sfalse // >bigop_Sfalse //
+  ]
+qed.
+
 lemma bigop_diff: ∀p,B.∀nil.∀op:ACop B nil.∀f:nat → B.∀i,n.
   i < n → p i = true →
   \big[op,nil]_{x<n|p x}(f x)=
@@ -181,7 +209,7 @@ lemma bigop_diff: ∀p,B.∀nil.∀op:ACop B nil.∀f:nat → B.∀i,n.
       [>(not_eq_to_eqb_false … (lt_to_not_eq … Hi)) //] #Hcut
      cases (true_or_false (p n)) #pn 
       [>bigop_Strue // >bigop_Strue //
-       >assoc >(comm ?? op (f i) (f n)) <assoc >Hind //
+       normalize >assoc >(comm ?? op (f i) (f n)) <assoc >Hind //
       |>bigop_Sfalse // >bigop_Sfalse // >Hind //  
       ]
     |<Hi >bigop_Strue // @eq_f >bigop_Sfalse  
@@ -265,7 +293,30 @@ theorem bigop_iso: ∀n1,n2,p1,p2,B.∀nil.∀op:ACop B nil.∀f1,f2.
   ]
 qed.
 
-(* Sigma e Pi *)
+(* distributivity *)
+
+record Dop (A:Type[0]) (nil:A): Type[0] ≝
+  {sum : ACop A nil; 
+   prod: A → A →A;
+   null: \forall a. prod a nil = nil; 
+   distr: ∀a,b,c:A. prod a (sum b c) = sum (prod a b) (prod a c)
+  }.
+  
+theorem bigop_distr: ∀n,p,B,nil.∀R:Dop B nil.\forall f,a.
+  let aop \def  sum B nil R in
+  let mop \def prod B nil R in
+  mop a \big[aop,nil]_{i<n|p i}(f i) = 
+   \big[aop,nil]_{i<n|p i}(mop a (f i)).
+#n #p #B #nil #R #f #a normalize (elim n) [@null]
+#n #Hind (cases (true_or_false (p n))) #H
+  [>bigop_Strue // >bigop_Strue // >(distr B nil R) >Hind //
+  |>bigop_Sfalse // >bigop_Sfalse //
+  ]
+qed.
+  
+(* Sigma e Pi 
+
+
 notation "Σ_{ ident i < n | p } f"
   with precedence 80
 for @{'bigop $n plus 0 (λ${ident i}.p) (λ${ident i}. $f)}.
@@ -301,7 +352,8 @@ notation "Π_{ ident j ∈ [a,b[ | p } f"
   with precedence 80
 for @{'bigop ($b-$a) times 1 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
- 
+
+*)
 (*
     
 definition p_ord_times \def
@@ -720,44 +772,7 @@ cut (O < p)
 ]
 qed.
     
-(*distributive property for iter_p_gen*)
-theorem distributive_times_plus_iter_p_gen: \forall A:Type.
-\forall plusA: A \to A \to A. \forall basePlusA: A.
-\forall timesA: A \to A \to A. 
-\forall n:nat. \forall k:A. \forall p:nat \to bool. \forall g:nat \to A.
-(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  basePlusA) = a) \to
-(symmetric A timesA) \to (distributive A timesA plusA) \to
-(\forall a:A. (timesA a basePlusA) = basePlusA)
- 
-  \to
 
-((timesA k (iter_p_gen n p A g basePlusA plusA)) = 
- (iter_p_gen n p A (\lambda i:nat.(timesA k (g i))) basePlusA plusA)).
-intros.
-elim n
-[ simplify.
-  apply H5
-| cut( (p n1) = true \lor (p n1) = false)
-  [ elim Hcut
-    [ rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H7).
-      rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H7) in \vdash (? ? ? %).
-      rewrite > (H4).
-      rewrite > (H3 k (g n1)).
-      apply eq_f.
-      assumption
-    | rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H7).
-      rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H7) in \vdash (? ? ? %).
-      assumption
-    ]
-  | elim ((p n1))
-    [ left.
-      reflexivity
-    | right.
-      reflexivity
-    ]
-  ]
-]
-qed.
 
 theorem iter_p_gen_2_eq: 
 \forall A:Type.