X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fbigops.ma;h=5e34160fe91a4998ac11014e1d75db94467c6ef4;hb=ddc80515997a3f56085c6234d4db326141e189aa;hp=6bcd62a653b38465021da0bb395700089e4afd70;hpb=31e8729021717072f88d250ef41527da3488289e;p=helm.git

diff --git a/matita/matita/lib/arithmetics/bigops.ma b/matita/matita/lib/arithmetics/bigops.ma
index 6bcd62a65..5e34160fe 100644
--- a/matita/matita/lib/arithmetics/bigops.ma
+++ b/matita/matita/lib/arithmetics/bigops.ma
@@ -141,7 +141,7 @@ a ≤ b → b ≤ c →
   op (\big[op,nil]_{i ∈ [b,c[ |p i}(f i)) 
       \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/
+>(plus_minus_m_m (c-a) (b-a)) {⊢ (??%?)} /2/
 >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 
@@ -173,11 +173,11 @@ theorem bigop_prod: ∀k1,k2,p1,p2,B.∀nil.∀op:Aop B nil.∀f: nat →nat →
 #n #Hind cases(true_or_false (p1 n)) #Hp1
   [>bigop_Strue // >Hind >bigop_sum @same_bigop
    #i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2/
-   #eqi [|#H] (>eqi in ⊢ (???%))
-     >div_plus_times /2/ >Hp1 >(mod_plus_times …) /2/
+   #eqi [|#H] >eqi {⊢ (???%)}
+     >div_plus_times /2/ >Hp1 >(mod_plus_times …) /2/ normalize //
   |>bigop_Sfalse // >Hind >(pad_bigop (S n*k2)) // @same_bigop
    #i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2/
-   #eqi >eqi in ⊢ (???%) >div_plus_times /2/ 
+   #eqi >eqi {⊢ (???%)} >div_plus_times /2/ 
   ]
 qed.
 
@@ -192,7 +192,7 @@ op (\big[op,nil]_{i<k|p i}(f i)) (\big[op,nil]_{i<k|p 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 ⊢ (??(????%?)?) 
+   normalize <assoc <assoc {⊢ (???%)} @eq_f >assoc >comm {⊢ (??(????%?)?)}
    <assoc @eq_f @Hind
   |>bigop_Sfalse // >bigop_Sfalse // >bigop_Sfalse //
   ]
@@ -263,7 +263,7 @@ theorem bigop_iso: ∀n1,n2,p1,p2,B.∀nil.∀op:ACop B nil.∀f1,f2.
   iso B (mk_range B f1 n1 p1) (mk_range B f2 n2 p2) →
   \big[op,nil]_{i<n1|p1 i}(f1 i) = \big[op,nil]_{i<n2|p2 i}(f2 i).
 #n1 #n2 #p1 #p2 #B #nil #op #f1 #f2 * #h * #k * * #same
-@(le_gen ? n1) #i (generalize in match p2) (elim i) 
+@(le_gen ? n1) #i generalize {match p2} (elim i) 
   [(elim n2) // #m #Hind #p2 #_ #sub1 #sub2
    >bigop_Sfalse 
     [@(Hind ? (le_O_n ?)) [/2/ | @(transitive_sub … (sub_lt …) sub2) //]
@@ -280,7 +280,7 @@ theorem bigop_iso: ∀n1,n2,p1,p2,B.∀nil.∀op:ACop B nil.∀f1,f2.
       |#j #ltj #p2j (cases (sub2 j ltj (andb_true_r …p2j))) * 
        #ltkj #p1kj #eqj % // % // 
        (cases (le_to_or_lt_eq …(le_S_S_to_le …ltkj))) //
-       #eqkj @False_ind generalize in match p2j @eqb_elim 
+       #eqkj @False_ind generalize {match p2j} @eqb_elim 
        normalize /2/
       ]
     |>bigop_Sfalse // @(Hind ? len) 
@@ -298,13 +298,13 @@ qed.
 record Dop (A:Type[0]) (nil:A): Type[0] ≝
   {sum : ACop A nil; 
    prod: A → A →A;
-   null: \forall a. prod a nil = nil; 
+   null: ∀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
+theorem bigop_distr: ∀n,p,B,nil.∀R:Dop B nil.∀f,a.
+  let aop ≝ sum B nil R in
+  let mop ≝ 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]