theorem pad_bigop: ∀k,n,p,B,nil,op.∀f:nat→B. n ≤ k →
\big[op,nil]_{i < n | p i}(f i)
- = \big[op,nil]_{i < k | if_then_else ? (leb n i) false (p i)}(f i).
+ = \big[op,nil]_{i < k | if leb n i then false else p i}(f i).
#k #n #p #B #nil #op #f #lenk (elim lenk)
[@same_bigop #i #lti // >(not_le_to_leb_false …) /2/
|#j #leup #Hind >bigop_Sfalse >(le_to_leb_true … leup) //
theorem bigop_sum: ∀k1,k2,p1,p2,B.∀nil.∀op:Aop B nil.∀f,g:nat→B.
op (\big[op,nil]_{i<k1|p1 i}(f i)) \big[op,nil]_{i<k2|p2 i}(g i) =
- \big[op,nil]_{i<k1+k2|if_then_else ? (leb k2 i) (p1 (i-k2)) (p2 i)}
- (if_then_else ? (leb k2 i) (f (i-k2)) (g i)).
+ \big[op,nil]_{i<k1+k2|if leb k2 i then p1 (i-k2) else p2 i}
+ (if leb k2 i then f (i-k2) else g i).
#k1 #k2 #p1 #p2 #B #nil #op #f #g (elim k1)
[normalize >nill @same_bigop #i #lti
>(lt_to_leb_false … lti) normalize /2/
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)) in ⊢ (??%?); /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
#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/ normalize //
+ #eqi [|#H] >eqi in ⊢ (???%);
+ >div_plus_times /2/ >Hp1 >(mod_plus_times …) /2/
|>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 in ⊢ (???%); >div_plus_times /2/
]
qed.
#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 in ⊢ (???%); @eq_f >assoc >comm in ⊢ (??(????%?)?);
<assoc @eq_f @Hind
|>bigop_Sfalse // >bigop_Sfalse // >bigop_Sfalse //
]
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 lapply p2 (elim i)
[(elim n2) // #m #Hind #p2 #_ #sub1 #sub2
>bigop_Sfalse
[@(Hind ? (le_O_n ?)) [/2/ | @(transitive_sub … (sub_lt …) sub2) //]
|#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 lapply p2j @eqb_elim
normalize /2/
]
|>bigop_Sfalse // @(Hind ? len)
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]