matita/matita/lib/arithmetics/bigops.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "basics/types.ma".
  13 include "arithmetics/div_and_mod.ma".
  14
  15 definition sameF_upto: nat → ∀A.relation(nat→A)  ≝
  16 λk.λA.λf,g.∀i. i < k → f i = g i.
  17
  18 definition sameF_p: nat → (nat → bool) →∀A.relation(nat→A)  ≝
  19 λk,p,A,f,g.∀i. i < k → p i = true → f i = g i.
  20
  21 lemma sameF_upto_le: ∀A,f,g,n,m.
  22  n ≤m → sameF_upto m A f g → sameF_upto n A f g.
  23 #A #f #g #n #m #lenm #samef #i #ltin @samef /2 by lt_to_le_to_lt/
  24 qed.
  25
  26 lemma sameF_p_le: ∀A,p,f,g,n,m.
  27  n ≤m → sameF_p m p A f g → sameF_p n p A f g.
  28 #A #p #f #g #n #m #lenm #samef #i #ltin #pi @samef /2 by lt_to_le_to_lt/
  29 qed.
  30
  31 (*
  32 definition sumF ≝ λA.λf,g:nat → A.λn,i.
  33 if_then_else ? (leb n i) (g (i-n)) (f i).
  34
  35 lemma sumF_unfold: ∀A,f,g,n,i.
  36 sumF A f g n i = if_then_else ? (leb n i) (g (i-n)) (f i).
  37 // qed. *)
  38
  39 definition prodF ≝
  40  λA,B.λf:nat→A.λg:nat→B.λm,x.〈 f(div x m), g(mod x m) 〉.
  41
  42 (* bigop *)
  43 let rec bigop (n:nat) (p:nat → bool) (B:Type[0])
  44    (nil: B) (op: B → B → B)  (f: nat → B) ≝
  45   match n with
  46    [ O ⇒ nil
  47    | S k ⇒
  48       match p k with
  49       [true ⇒ op (f k) (bigop k p B nil op f)
  50       |false ⇒ bigop k p B nil op f]
  51    ].
  52
  53 notation "\big  [ op , nil ]_{ ident i < n | p } f"
  54   with precedence 80
  55 for @{'bigop $n $op $nil (λ${ident i}. $p) (λ${ident i}. $f)}.
  56
  57 notation "\big [ op , nil ]_{ ident i < n } f"
  58   with precedence 80
  59 for @{'bigop $n $op $nil (λ${ident i}.true) (λ${ident i}. $f)}.
  60
  61 interpretation "bigop" 'bigop n op nil p f = (bigop n p ? nil op f).
  62
  63 notation "\big  [ op , nil ]_{ ident j ∈ [a,b[ | p } f"
  64   with precedence 80
  65 for @{'bigop ($b-$a) $op $nil (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
  66   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
  67
  68 notation "\big  [ op , nil ]_{ ident j ∈ [a,b[ } f"
  69   with precedence 80
  70 for @{'bigop ($b-$a) $op $nil (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
  71   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
  72
  73 (* notation "\big  [ op , nil ]_{( term 55) a ≤ ident j < b | p } f"
  74   with precedence 80
  75 for @{\big[$op,$nil]_{${ident j} < ($b-$a) | ((λ${ident j}.$p) (${ident j}+$a))}((λ${ident j}.$f)(${ident j}+$a))}.
  76 *)
  77
  78 interpretation "bigop" 'bigop n op nil p f = (bigop n p ? nil op f).
  79
  80 lemma bigop_Strue: ∀k,p,B,nil,op.∀f:nat→B. p k = true →
  81   \big[op,nil]_{i < S k | p i}(f i) =
  82     op (f k) (\big[op,nil]_{i < k | p i}(f i)).
  83 #k #p #B #nil #op #f #H normalize >H // qed.
  84
  85 lemma bigop_Sfalse: ∀k,p,B,nil,op.∀f:nat→B. p k = false →
  86   \big[op,nil]_{ i < S k | p i}(f i) =
  87     \big[op,nil]_{i < k | p i}(f i).
  88 #k #p #B #nil #op #f #H normalize >H // qed.
  89
  90 lemma same_bigop : ∀k,p1,p2,B,nil,op.∀f,g:nat→B.
  91   sameF_upto k bool p1 p2 → sameF_p k p1 B f g →
  92   \big[op,nil]_{i < k | p1 i}(f i) =
  93     \big[op,nil]_{i < k | p2 i}(g i).
  94 #k #p1 #p2 #B #nil #op #f #g (elim k) //
  95 #n #Hind #samep #samef normalize >Hind /2/
  96 <(samep … (le_n …)) cases(true_or_false (p1 n)) #H1 >H1
  97 normalize // <(samef … (le_n …) H1) //
  98 qed.
  99
 100 theorem pad_bigop: ∀k,n,p,B,nil,op.∀f:nat→B. n ≤ k →
 101 \big[op,nil]_{i < n | p i}(f i)
 102   = \big[op,nil]_{i < k | if leb n i then false else p i}(f i).
 103 #k #n #p #B #nil #op #f #lenk (elim lenk)
 104   [@same_bigop #i #lti // >(not_le_to_leb_false …) /2/
 105   |#j #leup #Hind >bigop_Sfalse >(le_to_leb_true … leup) //
 106   ] qed.
 107
 108 theorem pad_bigop1: ∀k,n,p,B,nil,op.∀f:nat→B. n ≤ k →
 109   (∀i. n ≤ i → i < k → p i = false) →
 110   \big[op,nil]_{i < n | p i}(f i)
 111     = \big[op,nil]_{i < k | p i}(f i).
 112 #k #n #p #B #nil #op #f #lenk (elim lenk)
 113   [#_ @same_bigop #i #lti //
 114   |#j #leup #Hind #Hfalse >bigop_Sfalse
 115     [@Hind #i #leni #ltij @Hfalse // @le_S //
 116     |@Hfalse //
 117     ]
 118   ]
 119 qed.
 120
 121 theorem bigop_false: ∀n,B,nil,op.∀f:nat→B.
 122   \big[op,nil]_{i < n | false }(f i) = nil.
 123 #n #B #nil #op #f elim n // #n1 #Hind
 124 >bigop_Sfalse //
 125 qed.
 126
 127 record Aop (A:Type[0]) (nil:A) : Type[0] ≝
 128   {op :2> A → A → A;
 129    nill:∀a. op nil a = a;
 130    nilr:∀a. op a nil = a;
 131    assoc: ∀a,b,c.op a (op b c) = op (op a b) c
 132   }.
 133
 134 theorem pad_bigop_nil: ∀k,n,p,B,nil.∀op:Aop B nil.∀f:nat→B. n ≤ k →
 135   (∀i. n ≤ i → i < k → p i = false ∨ f i = nil) →
 136   \big[op,nil]_{i < n | p i}(f i)
 137     = \big[op,nil]_{i < k | p i}(f i).
 138 #k #n #p #B #nil #op #f #lenk (elim lenk)
 139   [#_ @same_bigop #i #lti //
 140   |#j #leup #Hind #Hfalse cases (true_or_false (p j)) #Hpj
 141     [>bigop_Strue //
 142      cut (f j = nil)
 143       [cases (Hfalse j leup (le_n … )) // >Hpj #H destruct (H)] #Hfj
 144      >Hfj >nill @Hind #i #leni #ltij
 145      cases (Hfalse i leni (le_S … ltij)) /2/
 146     |>bigop_Sfalse // @Hind #i #leni #ltij
 147      cases (Hfalse i leni (le_S … ltij)) /2/
 148     ]
 149   ]
 150 qed.
 151
 152 theorem bigop_sum: ∀k1,k2,p1,p2,B.∀nil.∀op:Aop B nil.∀f,g:nat→B.
 153 op (\big[op,nil]_{i<k1|p1 i}(f i)) \big[op,nil]_{i<k2|p2 i}(g i) =
 154       \big[op,nil]_{i<k1+k2|if leb k2 i then p1 (i-k2) else p2 i}
 155         (if leb k2 i then f (i-k2) else g i).
 156 #k1 #k2 #p1 #p2 #B #nil #op #f #g (elim k1)
 157   [normalize >nill @same_bigop #i #lti
 158    >(lt_to_leb_false … lti) normalize /2/
 159   |#i #Hind normalize <minus_plus_m_m (cases (p1 i))
 160    >(le_to_leb_true … (le_plus_n …)) normalize <Hind //
 161    <assoc //
 162   ]
 163 qed.
 164
 165 lemma plus_minus1: ∀a,b,c. c ≤ b → a + (b -c) = a + b -c.
 166 #a #b #c #lecb @sym_eq @plus_to_minus >(commutative_plus c)
 167 >associative_plus <plus_minus_m_m //
 168 qed.
 169
 170 theorem bigop_I: ∀n,p,B.∀nil.∀op:Aop B nil.∀f:nat→B.
 171 \big[op,nil]_{i∈[0,n[ |p i}(f i) = \big[op,nil]_{i < n|p i}(f i).
 172 #n #p #B #nil #op #f <minus_n_O @same_bigop //
 173 qed.
 174
 175 theorem bigop_I_gen: ∀a,b,p,B.∀nil.∀op:Aop B nil.∀f:nat→B. a ≤b →
 176 \big[op,nil]_{i∈[a,b[ |p i}(f i) = \big[op,nil]_{i < b|leb a i ∧ p i}(f i).
 177 #a #b elim b // -b #b #Hind #p #B #nil #op #f #lea
 178 cut (∀a,b. a ≤ b → S b - a = S (b -a))
 179   [#a #b cases a // #a1 #lta1 normalize >eq_minus_S_pred >S_pred
 180    /2 by lt_plus_to_minus_r/] #Hcut
 181 cases (le_to_or_lt_eq … lea) #Ha
 182   [cases (true_or_false (p b)) #Hcase
 183     [>bigop_Strue [2: >Hcase >(le_to_leb_true a b) // @le_S_S_to_le @Ha]
 184      >(Hcut … (le_S_S_to_le … Ha))
 185      >bigop_Strue
 186       [@eq_f2
 187         [@eq_f <plus_minus_m_m [//|@le_S_S_to_le //] @Hind
 188         |@Hind @le_S_S_to_le //
 189         ]
 190       |<plus_minus_m_m // @le_S_S_to_le //
 191       ]
 192    |>bigop_Sfalse [2: >Hcase cases (leb a b)//]
 193      >(Hcut … (le_S_S_to_le … Ha)) >bigop_Sfalse
 194       [@Hind @le_S_S_to_le // | <plus_minus_m_m // @le_S_S_to_le //]
 195     ]
 196   |<Ha <minus_n_n whd in ⊢ (??%?); <(bigop_false a B nil op f) in ⊢ (??%?);
 197    @same_bigop // #i #ltia >(not_le_to_leb_false a i) // @lt_to_not_le //
 198   ]
 199 qed.
 200
 201 theorem bigop_sumI: ∀a,b,c,p,B.∀nil.∀op:Aop B nil.∀f:nat→B.
 202 a ≤ b → b ≤ c →
 203 \big[op,nil]_{i∈[a,c[ |p i}(f i) =
 204   op (\big[op,nil]_{i ∈ [b,c[ |p i}(f i))
 205       \big[op,nil]_{i ∈ [a,b[ |p i}(f i).
 206 #a #b # c #p #B #nil #op #f #leab #lebc
 207 >(plus_minus_m_m (c-a) (b-a)) in ⊢ (??%?); /2/
 208 >minus_plus >(commutative_plus a) <plus_minus_m_m //
 209 >bigop_sum (cut (∀i. b -a ≤ i → i+a = i-(b-a)+b))
 210   [#i #lei >plus_minus // <plus_minus1
 211      [@eq_f @sym_eq @plus_to_minus /2/ | /2/]]
 212 #H @same_bigop #i #ltic @leb_elim normalize // #lei <H //
 213 qed.
 214
 215 theorem bigop_a: ∀a,b,B.∀nil.∀op:Aop B nil.∀f:nat→B. a ≤ b →
 216 \big[op,nil]_{i∈[a,S b[ }(f i) =
 217   op (\big[op,nil]_{i ∈ [a,b[ }(f (S i))) (f a).
 218 #a #b #B #nil #op #f #leab
 219 >(bigop_sumI a (S a) (S b)) [|@le_S_S //|//] @eq_f2
 220   [@same_bigop // |<minus_Sn_n normalize @nilr]
 221 qed.
 222
 223 theorem bigop_0: ∀n,B.∀nil.∀op:Aop B nil.∀f:nat→B.
 224 \big[op,nil]_{i < S n}(f i) =
 225   op (\big[op,nil]_{i < n}(f (S i))) (f 0).
 226 #n #B #nil #op #f
 227 <bigop_I >bigop_a [|//] @eq_f2 [|//] <minus_n_O
 228 @same_bigop //
 229 qed.
 230
 231 theorem bigop_prod: ∀k1,k2,p1,p2,B.∀nil.∀op:Aop B nil.∀f: nat →nat → B.
 232 \big[op,nil]_{x<k1|p1 x}(\big[op,nil]_{i<k2|p2 x i}(f x i)) =
 233   \big[op,nil]_{i<k1*k2|andb (p1 (i/k2)) (p2 (i/k2) (i \mod k2))}
 234      (f (i/k2) (i \mod k2)).
 235 #k1 #k2 #p1 #p2 #B #nil #op #f (elim k1) //
 236 #n #Hind cases(true_or_false (p1 n)) #Hp1
 237   [>bigop_Strue // >Hind >bigop_sum @same_bigop
 238    #i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2 by plus_minus/
 239    #eqi [|#H] >eqi in ⊢ (???%);
 240      >div_plus_times /2 by monotonic_lt_minus_l/
 241      >Hp1 >(mod_plus_times …) /2 by refl, monotonic_lt_minus_l, eq_f/
 242   |>bigop_Sfalse // >Hind >(pad_bigop (S n*k2)) // @same_bigop
 243    #i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2 by plus_minus/
 244    #eqi >eqi in ⊢ (???%); >div_plus_times
 245    /2 by refl, monotonic_lt_minus_l, trans_eq/
 246   ]
 247 qed.
 248
 249 record ACop (A:Type[0]) (nil:A) : Type[0] ≝
 250   {aop :> Aop A nil;
 251    comm: ∀a,b.aop a b = aop b a
 252   }.
 253
 254 lemma bigop_op: ∀k,p,B.∀nil.∀op:ACop B nil.∀f,g: nat → B.
 255 op (\big[op,nil]_{i<k|p i}(f i)) (\big[op,nil]_{i<k|p i}(g i)) =
 256   \big[op,nil]_{i<k|p i}(op (f i) (g i)).
 257 #k #p #B #nil #op #f #g (elim k) [normalize @nill]
 258 -k #k #Hind (cases (true_or_false (p k))) #H
 259   [>bigop_Strue // >bigop_Strue // >bigop_Strue //
 260    normalize <assoc <assoc in ⊢ (???%); @eq_f >assoc >comm in ⊢ (??(????%?)?);
 261    <assoc @eq_f @Hind
 262   |>bigop_Sfalse // >bigop_Sfalse // >bigop_Sfalse //
 263   ]
 264 qed.
 265
 266 lemma bigop_diff: ∀p,B.∀nil.∀op:ACop B nil.∀f:nat → B.∀i,n.
 267   i < n → p i = true →
 268   \big[op,nil]_{x<n|p x}(f x)=
 269     op (f i) (\big[op,nil]_{x<n|andb(notb(eqb i x))(p x)}(f x)).
 270 #p #B #nil #op #f #i #n (elim n)
 271   [#ltO @False_ind /2/
 272   |#n #Hind #lein #pi cases (le_to_or_lt_eq … (le_S_S_to_le …lein)) #Hi
 273     [cut (andb(notb(eqb i n))(p n) = (p n))
 274       [>(not_eq_to_eqb_false … (lt_to_not_eq … Hi)) //] #Hcut
 275      cases (true_or_false (p n)) #pn
 276       [>bigop_Strue // >bigop_Strue //
 277        normalize >assoc >(comm ?? op (f i) (f n)) <assoc >Hind //
 278       |>bigop_Sfalse // >bigop_Sfalse // >Hind //
 279       ]
 280     |<Hi >bigop_Strue // @eq_f >bigop_Sfalse
 281        [@same_bigop // #k #ltki >not_eq_to_eqb_false /2/
 282        |>eq_to_eqb_true //
 283        ]
 284      ]
 285    ]
 286 qed.
 287
 288 (* range *)
 289 record range (A:Type[0]): Type[0] ≝
 290   {enum:nat→A; upto:nat; filter:nat→bool}.
 291
 292 definition sub_hk: (nat→nat)→(nat→nat)→∀A:Type[0].relation (range A) ≝
 293 λh,k,A,I,J.∀i.i<(upto A I) → (filter A I i)=true →
 294   (h i < upto A J
 295   ∧ filter A J (h i) = true
 296   ∧ k (h i) = i).
 297
 298 definition iso: ∀A:Type[0].relation (range A) ≝
 299   λA,I,J.∃h,k.
 300     (∀i. i < (upto A I) → (filter A I i) = true →
 301        enum A I i = enum A J (h i)) ∧
 302     sub_hk h k A I J ∧ sub_hk k h A J I.
 303
 304 lemma sub_hkO: ∀h,k,A,I,J. upto A I = 0 → sub_hk h k A I J.
 305 #h #k #A #I #J #up0 #i #lti >up0 @False_ind /2/
 306 qed.
 307
 308 lemma sub0_to_false: ∀h,k,A,I,J. upto A I = 0 → sub_hk h k A J I →
 309   ∀i. i < upto A J → filter A J i = false.
 310 #h #k #A #I #J #up0 #sub #i #lti cases(true_or_false (filter A J i)) //
 311 #ptrue (cases (sub i lti ptrue)) * #hi @False_ind /2/
 312 qed.
 313
 314 lemma sub_lt: ∀A,e,p,n,m. n ≤ m →
 315   sub_hk (λx.x) (λx.x) A (mk_range A e n p) (mk_range A e m p).
 316 #A #e #f #n #m #lenm #i #lti #fi % // % /2 by lt_to_le_to_lt/
 317 qed.
 318
 319 theorem transitive_sub: ∀h1,k1,h2,k2,A,I,J,K.
 320   sub_hk h1 k1 A I J → sub_hk h2 k2 A J K →
 321     sub_hk (λx.h2(h1 x)) (λx.k1(k2 x)) A I K.
 322 #h1 #k1 #h2 #k2 #A #I #J #K #sub1 #sub2 #i #lti #fi
 323 cases(sub1 i lti fi) * #lth1i #fh1i #ei
 324 cases(sub2 (h1 i) lth1i fh1i) * #H1 #H2 #H3 % // % //
 325 qed.
 326
 327 theorem bigop_iso: ∀n1,n2,p1,p2,B.∀nil.∀op:ACop B nil.∀f1,f2.
 328   iso B (mk_range B f1 n1 p1) (mk_range B f2 n2 p2) →
 329   \big[op,nil]_{i<n1|p1 i}(f1 i) = \big[op,nil]_{i<n2|p2 i}(f2 i).
 330 #n1 #n2 #p1 #p2 #B #nil #op #f1 #f2 * #h * #k * * #same
 331 @(le_gen ? n1) #i lapply p2 (elim i)
 332   [(elim n2) // #m #Hind #p2 #_ #sub1 #sub2
 333    >bigop_Sfalse
 334     [@(Hind ? (le_O_n ?)) [/2/ | @(transitive_sub … (sub_lt …) sub2) //]
 335     |@(sub0_to_false … sub2) //
 336     ]
 337   |#n #Hind #p2 #ltn #sub1 #sub2 (cut (n ≤n1)) [/2/] #len
 338    cases(true_or_false (p1 n)) #p1n
 339     [>bigop_Strue // (cases (sub1 n (le_n …) p1n)) * #hn #p2hn #eqn
 340      >(bigop_diff … (h n) n2) // >same //
 341      @eq_f @(Hind ? len)
 342       [#i #ltin #p1i (cases (sub1 i (le_S … ltin) p1i)) *
 343        #h1i #p2h1i #eqi % // % // >not_eq_to_eqb_false normalize //
 344        @(not_to_not ??? (lt_to_not_eq ? ? ltin)) //
 345       |#j #ltj #p2j (cases (sub2 j ltj (andb_true_r …p2j))) *
 346        #ltkj #p1kj #eqj % // % //
 347        (cases (le_to_or_lt_eq …(le_S_S_to_le …ltkj))) //
 348        #eqkj @False_ind lapply p2j @eqb_elim
 349        normalize /2/
 350       ]
 351     |>bigop_Sfalse // @(Hind ? len)
 352       [@(transitive_sub … (sub_lt …) sub1) //
 353       |#i #lti #p2i cases(sub2 i lti p2i) * #ltki #p1ki #eqi
 354        % // % // cases(le_to_or_lt_eq …(le_S_S_to_le …ltki)) //
 355        #eqki @False_ind /2/
 356       ]
 357     ]
 358   ]
 359 qed.
 360
 361 (* commutation *)
 362 theorem bigop_commute: ∀n,m,p11,p12,p21,p22,B.∀nil.∀op:ACop B nil.∀f.
 363 0 < n → 0 < m →
 364 (∀i,j. i < n → j < m → (p11 i ∧ p12 i j) = (p21 j ∧ p22 i j)) →
 365 \big[op,nil]_{i<n|p11 i}(\big[op,nil]_{j<m|p12 i j}(f i j)) =
 366    \big[op,nil]_{j<m|p21 j}(\big[op,nil]_{i<n|p22 i j}(f i j)).
 367 #n #m #p11 #p12 #p21 #p22 #B #nil #op #f #posn #posm #Heq
 368 >bigop_prod >bigop_prod @bigop_iso
 369 %{(λi.(i\mod m)*n + i/m)} %{(λi.(i\mod n)*m + i/n)} %
 370   [%
 371     [#i #lti #Heq (* whd in ⊢ (???(?(?%?)?)); *) @eq_f2
 372       [@sym_eq @mod_plus_times /2 by lt_times_to_lt_div/
 373       |@sym_eq @div_plus_times /2 by lt_times_to_lt_div/
 374       ]
 375     |#i #lti #Hi
 376      cut ((i\mod m*n+i/m)\mod n=i/m)
 377       [@mod_plus_times @lt_times_to_lt_div //] #H1
 378      cut ((i\mod m*n+i/m)/n=i \mod m)
 379       [@div_plus_times @lt_times_to_lt_div //] #H2
 380      %[%[@(lt_to_le_to_lt ? (i\mod m*n+n))
 381           [whd >plus_n_Sm @monotonic_le_plus_r @lt_times_to_lt_div //
 382           |>commutative_plus @(le_times (S(i \mod m)) m n n) // @lt_mod_m_m //
 383           ]
 384         |lapply (Heq (i/m) (i \mod m) ??)
 385           [@lt_mod_m_m // |@lt_times_to_lt_div //|>Hi >H1 >H2 //]
 386         ]
 387       |>H1 >H2 //
 388       ]
 389     ]
 390   |#i #lti #Hi
 391    cut ((i\mod n*m+i/n)\mod m=i/n)
 392     [@mod_plus_times @lt_times_to_lt_div //] #H1
 393    cut ((i\mod n*m+i/n)/m=i \mod n)
 394     [@div_plus_times @lt_times_to_lt_div //] #H2
 395    %[%[@(lt_to_le_to_lt ? (i\mod n*m+m))
 396         [whd >plus_n_Sm @monotonic_le_plus_r @lt_times_to_lt_div //
 397         |>commutative_plus @(le_times (S(i \mod n)) n m m) // @lt_mod_m_m //
 398         ]
 399       |lapply (Heq (i \mod n) (i/n) ??)
 400         [@lt_times_to_lt_div // |@lt_mod_m_m // |>Hi >H1 >H2 //]
 401       ]
 402     |>H1 >H2 //
 403     ]
 404   ]
 405 qed.
 406
 407 (* distributivity *)
 408
 409 record Dop (A:Type[0]) (nil:A): Type[0] ≝
 410   {sum : ACop A nil;
 411    prod: A → A →A;
 412    null: \forall a. prod a nil = nil;
 413    distr: ∀a,b,c:A. prod a (sum b c) = sum (prod a b) (prod a c)
 414   }.
 415
 416 theorem bigop_distr: ∀n,p,B,nil.∀R:Dop B nil.∀f,a.
 417   let aop ≝ sum B nil R in
 418   let mop ≝ prod B nil R in
 419   mop a \big[aop,nil]_{i<n|p i}(f i) =
 420    \big[aop,nil]_{i<n|p i}(mop a (f i)).
 421 #n #p #B #nil #R #f #a normalize (elim n) [@null]
 422 #n #Hind (cases (true_or_false (p n))) #H
 423   [>bigop_Strue // >bigop_Strue // >(distr B nil R) >Hind //
 424   |>bigop_Sfalse // >bigop_Sfalse //
 425   ]
 426 qed.