matita/matita/lib/arithmetics/big_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_pi:
  79 ∀n.∀p:nat → bool.∀g1,g2:nat → nat.
  80   (∀i.i<n → p i = true → g1 i ≤ g2 i ) →
  81   ∏_{i < n | p i} (g1 i) ≤ ∏_{i < n | p i} (g2 i).
  82 #n #p #g1 #g2 elim n
  83   [#_ @le_n
  84   |#n1 #Hind #Hle cases (true_or_false (p n1)) #Hcase
  85     [ >bigop_Strue // >bigop_Strue // @le_times
  86       [@Hle // |@Hind #i #lti #Hpi @Hle [@lt_to_le @le_S_S @lti|@Hpi]]
  87     |>bigop_Sfalse // >bigop_Sfalse // @Hind
  88      #i #lti #Hpi @Hle [@lt_to_le @le_S_S @lti|@Hpi]
  89     ]
  90   ]
  91 qed.
  92
  93 theorem exp_sigma: ∀n,a,p.
  94   ∏_{i < n | p i} a = exp a (∑_{i < n | p i} 1).
  95 #n #a #p elim n // #n1 cases (true_or_false (p n1)) #Hcase
  96   [>bigop_Strue // >bigop_Strue // |>bigop_Sfalse // >bigop_Sfalse //]
  97 qed.
  98
  99 theorem times_pi: ∀n,p,f,g.
 100   ∏_{i<n|p i}(f i*g i) = ∏_{i<n|p i}(f i) * ∏_{i<n|p i}(g i).
 101 #n #p #f #g elim n // #n1 cases (true_or_false (p n1)) #Hcase #Hind
 102   [>bigop_Strue // >bigop_Strue // >bigop_Strue //
 103   |>bigop_Sfalse // >bigop_Sfalse // >bigop_Sfalse //
 104   ]
 105 qed.
 106
 107 theorem pi_1: ∀n,p.
 108   ∏_{i < n | p i} 1 = 1.
 109 #n #p elim n // #n1 #Hind cases (true_or_false (p n1)) #Hc
 110   [>bigop_Strue >Hind // |>bigop_Sfalse // ]
 111 qed.
 112
 113 theorem exp_pi: ∀n,m,p,f.
 114   ∏_{i < n | p i}(exp (f i) m) = exp (∏_{i < n | p i}(f i)) m.
 115 #n #m #p #f elim m
 116   [@pi_1
 117   |#m1 #Hind >times_pi >Hind %
 118   ]
 119 qed.