matita/matita/lib/arithmetics/sigma_pi.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 "arithmetics/primes.ma".
  13 include "arithmetics/bigops.ma".
  14
  15 (* Sigma e Pi *)
  16
  17 notation "∑_{ ident i < n | p } f"
  18   with precedence 80
  19 for @{'bigop $n plus 0 (λ${ident i}. $p) (λ${ident i}. $f)}.
  20
  21 notation "∑_{ ident i < n } f"
  22   with precedence 80
  23 for @{'bigop $n plus 0 (λ${ident i}.true) (λ${ident i}. $f)}.
  24
  25 notation "∑_{ ident j ∈ [a,b[ } f"
  26   with precedence 80
  27 for @{'bigop ($b-$a) plus 0 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
  28   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
  29
  30 notation "∑_{ ident j ∈ [a,b[ | p } f"
  31   with precedence 80
  32 for @{'bigop ($b-$a) plus 0 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
  33   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
  34
  35 notation "∏_{ ident i < n | p} f"
  36   with precedence 80
  37 for @{'bigop $n times 1 (λ${ident i}.$p) (λ${ident i}. $f)}.
  38
  39 notation "∏_{ ident i < n } f"
  40   with precedence 80
  41 for @{'bigop $n times 1 (λ${ident i}.true) (λ${ident i}. $f)}.
  42
  43 notation "∏_{ ident j ∈ [a,b[ } f"
  44   with precedence 80
  45 for @{'bigop ($b-$a) times 1 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
  46   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
  47
  48 notation "∏_{ ident j ∈ [a,b[ | p } f"
  49   with precedence 80
  50 for @{'bigop ($b-$a) times 1 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
  51   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
  52
  53 (* instances of associative and commutative operations *)
  54
  55 definition plusA ≝ mk_Aop nat 0 plus (λa.refl ? a) (λn.sym_eq ??? (plus_n_O n))
  56    (λa,b,c.sym_eq ??? (associative_plus a b c)).
  57
  58 definition plusAC ≝ mk_ACop nat 0 plusA commutative_plus.
  59
  60 definition timesA ≝ mk_Aop nat 1 times
  61    (λa.sym_eq ??? (plus_n_O a)) (λn.sym_eq ??? (times_n_1 n))
  62    (λa,b,c.sym_eq ??? (associative_times a b c)).
  63
  64 definition timesAC ≝ mk_ACop nat 1 timesA commutative_times.
  65
  66 definition natD ≝ mk_Dop nat 0 plusAC times (λn.(sym_eq ??? (times_n_O n)))
  67    distributive_times_plus.
  68
  69 (********************************************************)
  70
  71 theorem sigma_const: ∀n:nat. ∑_{i<n} 1 = n.
  72 #n elim n // #n1 >bigop_Strue //
  73 qed.
  74
  75 (* monotonicity; these roperty should be expressed at a more
  76 genral level *)
  77
  78 theorem le_sigma:
  79 ∀n:nat. ∀p1,p2:nat → bool. ∀g1,g2:nat → nat.
  80 (∀i. i < n → p1 i = true → p2 i = true ) →
  81 (∀i. i < n → p1 i = true → g1 i ≤ g2 i ) →
  82  ∑_{i < n | p1 i} (g1 i) ≤ ∑_{i < n | p2 i} (g2 i).
  83 #n #p1 #p2 #g1 #g2 elim n
  84   [#_ #_ @le_n
  85   |#n1 #Hind #H1 #H2
  86    lapply (Hind ??)
  87      [#j #ltin1 #Hgj @(H2 … Hgj) @le_S //
  88      |#j #ltin1 #Hp1j @(H1 … Hp1j) @le_S //
  89      ] -Hind #Hind
  90    cases (true_or_false (p2 n1)) #Hp2
  91     [>bigop_Strue in ⊢ (??%); [2:@Hp2]
  92      cases (true_or_false (p1 n1)) #Hp1
  93       [>bigop_Strue [2:@Hp1] @(le_plus … Hind) @H2 //
  94       |>bigop_Sfalse [2:@Hp1] @le_plus_a //
  95       ]
  96     |cut (p1 n1 = false)
  97       [cases (true_or_false (p1 n1)) #Hp1
  98         [>(H1 … (le_n ?) Hp1) in Hp2; #H destruct (H) | //]
  99       ] #Hp1
 100      >bigop_Sfalse [2:@Hp1] >bigop_Sfalse [2:@Hp2] //
 101     ]
 102   ]
 103 qed.
 104
 105 theorem lt_sigma_p:
 106 ∀n:nat. ∀p1,p2:nat → bool. ∀g1,g2:nat → nat.
 107 (∀i. i < n → p1 i = true → p2 i = true) →
 108 (∀i. i < n → p1 i = true → g1 i ≤ g2 i ) →
 109 (∃i. i < n ∧ ((p1 i = true) ∧ (g1 i < g2 i)
 110               ∨ (p1 i = false ∧ (p2 i = true) ∧ (0 < g2 i)))) →
 111   ∑_{i < n | p1 i} (g1 i) < ∑_{i < n | p2 i} (g2 i).
 112 #n #p1 #p2 #g1 #g2 #H1 #H2 * #k * #ltk *
 113   [* #p1k #gk
 114    lapply (H1 k ltk p1k) #p2k
 115    >(bigop_diff p1 ?? plusAC … ltk p1k)
 116    >(bigop_diff p2 ?? plusAC … ltk p2k) whd
 117    cut (∀a,b. S a + b = S(a +b)) [//] #Hplus <Hplus @le_plus
 118     [@gk
 119     |@le_sigma
 120       [#i #ltin #H @true_to_andb_true
 121         [@(andb_true_l … H) | @(H1 i ltin) @(andb_true_r … H)]
 122       |#i #ltin #H @(H2 i ltin) @(andb_true_r … H)
 123       ]
 124     ]
 125   |* * #p1k #p2k #posg2
 126    >(bigop_diff p2 ?? plusAC … ltk p2k) whd
 127    cut (∀a. S 0 + a = S a) [//] #H0 <(H0 (bigop n ?????)) @le_plus
 128     [@posg2
 129     |@le_sigma
 130       [#i #ltin #H @true_to_andb_true
 131         [cases (true_or_false (eqb k i)) #Hc >Hc
 132           [normalize <H <p1k >(eqb_true_to_eq … Hc) //|//]
 133         |@(H1 i ltin) @H]
 134       |#i #ltin #H @(H2 i ltin) @H
 135       ]
 136     ]
 137 qed.
 138
 139 theorem le_pi:
 140 ∀n.∀p:nat → bool.∀g1,g2:nat → nat.
 141   (∀i.i<n → p i = true → g1 i ≤ g2 i ) →
 142   ∏_{i < n | p i} (g1 i) ≤ ∏_{i < n | p i} (g2 i).
 143 #n #p #g1 #g2 elim n
 144   [#_ @le_n
 145   |#n1 #Hind #Hle cases (true_or_false (p n1)) #Hcase
 146     [ >bigop_Strue // >bigop_Strue // @le_times
 147       [@Hle // |@Hind #i #lti #Hpi @Hle [@lt_to_le @le_S_S @lti|@Hpi]]
 148     |>bigop_Sfalse // >bigop_Sfalse // @Hind
 149      #i #lti #Hpi @Hle [@lt_to_le @le_S_S @lti|@Hpi]
 150     ]
 151   ]
 152 qed.
 153
 154 theorem exp_sigma: ∀n,a,p.
 155   ∏_{i < n | p i} a = exp a (∑_{i < n | p i} 1).
 156 #n #a #p elim n // #n1 cases (true_or_false (p n1)) #Hcase
 157   [>bigop_Strue // >bigop_Strue // |>bigop_Sfalse // >bigop_Sfalse //]
 158 qed.
 159
 160 theorem times_pi: ∀n,p,f,g.
 161   ∏_{i<n|p i}(f i*g i) = ∏_{i<n|p i}(f i) * ∏_{i<n|p i}(g i).
 162 #n #p #f #g elim n // #n1 cases (true_or_false (p n1)) #Hcase #Hind
 163   [>bigop_Strue // >bigop_Strue // >bigop_Strue //
 164   |>bigop_Sfalse // >bigop_Sfalse // >bigop_Sfalse //
 165   ]
 166 qed.
 167
 168 theorem pi_1: ∀n,p.
 169   ∏_{i < n | p i} 1 = 1.
 170 #n #p elim n // #n1 #Hind cases (true_or_false (p n1)) #Hc
 171   [>bigop_Strue >Hind // |>bigop_Sfalse // ]
 172 qed.
 173
 174 theorem exp_pi: ∀n,m,p,f.
 175   ∏_{i < n | p i}(exp (f i) m) = exp (∏_{i < n | p i}(f i)) m.
 176 #n #m #p #f elim m
 177   [@pi_1
 178   |#m1 #Hind >times_pi >Hind %
 179   ]
 180 qed.
 181
 182 theorem exp_sigma_l: ∀n,a,p,f.
 183   ∏_{i < n | p i} (exp a (f i)) = exp a (∑_{i < n | p i}(f i)).
 184 #n #a #p #f elim n // #i #Hind cases (true_or_false (p i)) #Hc
 185   [>bigop_Strue [>bigop_Strue [>Hind >exp_plus_times // |//] |//]
 186   |>bigop_Sfalse [>bigop_Sfalse [@Hind|//] | //]
 187   ]
 188 qed.