helm/software/matita/library/nat/pi_p.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "nat/primes.ma".
  16 (* include "nat/ord.ma". *)
  17 include "nat/generic_iter_p.ma".
  18 (* include "nat/count.ma". necessary just to use bool_to_nat and bool_to_nat_andb*)
  19 include "nat/iteration2.ma".
  20
  21 (* pi_p on nautral numbers is a specialization of iter_p_gen *)
  22 definition pi_p: nat \to (nat \to bool) \to (nat \to nat) \to nat \def
  23 \lambda n, p, g. (iter_p_gen n p nat g (S O) times).
  24
  25 (*
  26 notation < "(mstyle scriptlevel 1 scriptsizemultiplier 1.7(Π)
  27              )
  28             \below
  29             (p
  30             \atop
  31             (ident i < n)) f"
  32 non associative with precedence 60 for
  33 @{ 'product $n (λ${ident i}:$xx1.$p) (λ${ident i}:$xx2.$f) }.
  34
  35 notation < "(mstyle scriptlevel 1 scriptsizemultiplier 1.7(Π)
  36              )
  37             \below
  38             ((ident i < n)) f"
  39 non associative with precedence 60 for
  40 @{ 'product $n (λ_:$xx1.$xx3) (λ${ident i}:$xx2.$f) }.
  41
  42 interpretation "big product" 'product n p f = (pi_p n p f).
  43
  44 notation > "'Pi' (ident x) < n | p . term 46 f"
  45 non associative with precedence 60
  46 for @{ 'product $n (λ${ident x}.$p) (λ${ident x}.$f) }.
  47
  48 notation > "'Pi' (ident x) ≤ n | p . term 46 f"
  49 non associative with precedence 60
  50 for @{ 'product (S $n) (λ${ident x}.$p) (λ${ident x}.$f) }.
  51
  52 notation > "'Pi' (ident x) < n . term 46 f"
  53 non associative with precedence 60
  54 for @{ 'product $n (λ_.true) (λ${ident x}.$f) }.
  55 *)
  56
  57 theorem true_to_pi_p_Sn: ∀n,p,g.
  58   p n = true \to pi_p (S n) p g = (g n)*(pi_p n p g).
  59 intros.
  60 unfold pi_p.
  61 apply true_to_iter_p_gen_Sn.
  62 assumption.
  63 qed.
  64
  65 theorem false_to_pi_p_Sn:
  66 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat.
  67 p n = false \to pi_p (S n) p g = pi_p n p g.
  68 intros.
  69 unfold pi_p.
  70 apply false_to_iter_p_gen_Sn.
  71 assumption.
  72 qed.
  73
  74 theorem eq_pi_p: \forall p1,p2:nat \to bool.
  75 \forall g1,g2: nat \to nat.\forall n.
  76 (\forall x.  x < n \to p1 x = p2 x) \to
  77 (\forall x.  x < n \to g1 x = g2 x) \to
  78 pi_p n p1 g1 = pi_p n p2 g2.
  79 intros.
  80 unfold pi_p.
  81 apply eq_iter_p_gen;
  82 assumption.
  83 qed.
  84
  85 theorem eq_pi_p1: \forall p1,p2:nat \to bool.
  86 \forall g1,g2: nat \to nat.\forall n.
  87 (\forall x.  x < n \to p1 x = p2 x) \to
  88 (\forall x.  x < n \to p1 x = true \to g1 x = g2 x) \to
  89 pi_p n p1 g1 = pi_p n p2 g2.
  90 intros.
  91 unfold pi_p.
  92 apply eq_iter_p_gen1;
  93 assumption.
  94 qed.
  95
  96 theorem pi_p_false:
  97 \forall g: nat \to nat.\forall n.pi_p n (\lambda x.false) g = S O.
  98 intros.
  99 unfold pi_p.
 100 apply iter_p_gen_false.
 101 qed.
 102
 103 theorem pi_p_times: \forall n,k:nat.\forall p:nat \to bool.
 104 \forall g: nat \to nat.
 105 pi_p (k+n) p g
 106 = pi_p k (\lambda x.p (x+n)) (\lambda x.g (x+n)) * pi_p n p g.
 107 intros.
 108 unfold pi_p.
 109 apply (iter_p_gen_plusA nat n k p g (S O) times)
 110 [ apply sym_times.
 111 | intros.
 112   apply sym_eq.
 113   apply times_n_SO
 114 | apply associative_times
 115 ]
 116 qed.
 117
 118 theorem false_to_eq_pi_p: \forall n,m:nat.n \le m \to
 119 \forall p:nat \to bool.
 120 \forall g: nat \to nat. (\forall i:nat. n \le i \to i < m \to
 121 p i = false) \to pi_p m p g = pi_p n p g.
 122 intros.
 123 unfold pi_p.
 124 apply (false_to_eq_iter_p_gen);
 125 assumption.
 126 qed.
 127
 128 theorem or_false_eq_SO_to_eq_pi_p:
 129 \forall n,m:nat.\forall p:nat \to bool.
 130 \forall g: nat \to nat.
 131 n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false \lor g i = S O)
 132 \to pi_p m p g = pi_p n p g.
 133 intros.
 134 unfold pi_p.
 135 apply or_false_eq_baseA_to_eq_iter_p_gen
 136   [intros.simplify.rewrite < plus_n_O.reflexivity
 137   |assumption
 138   |assumption
 139   ]
 140 qed.
 141
 142 theorem pi_p2 :
 143 \forall n,m:nat.
 144 \forall p1,p2:nat \to bool.
 145 \forall g: nat \to nat \to nat.
 146 pi_p (n*m)
 147   (\lambda x.andb (p1 (div x m)) (p2 (mod x m)))
 148   (\lambda x.g (div x m) (mod x m)) =
 149 pi_p n p1
 150   (\lambda x.pi_p m p2 (g x)).
 151 intros.
 152 unfold pi_p.
 153 apply (iter_p_gen2 n m p1 p2 nat g (S O) times)
 154 [ apply sym_times
 155 | apply associative_times
 156 | intros.
 157   apply sym_eq.
 158   apply times_n_SO
 159 ]
 160 qed.
 161
 162 theorem pi_p2' :
 163 \forall n,m:nat.
 164 \forall p1:nat \to bool.
 165 \forall p2:nat \to nat \to bool.
 166 \forall g: nat \to nat \to nat.
 167 pi_p (n*m)
 168   (\lambda x.andb (p1 (div x m)) (p2 (div x m) (mod x  m)))
 169   (\lambda x.g (div x m) (mod x m)) =
 170 pi_p n p1
 171   (\lambda x.pi_p m (p2 x) (g x)).
 172 intros.
 173 unfold pi_p.
 174 apply (iter_p_gen2' n m p1 p2 nat g (S O) times)
 175 [ apply sym_times
 176 | apply associative_times
 177 | intros.
 178   apply sym_eq.
 179   apply times_n_SO
 180 ]
 181 qed.
 182
 183 lemma pi_p_gi: \forall g: nat \to nat.
 184 \forall n,i.\forall p:nat \to bool.i < n \to p i = true \to
 185 pi_p n p g = g i * pi_p n (\lambda x. andb (p x) (notb (eqb x i))) g.
 186 intros.
 187 unfold pi_p.
 188 apply (iter_p_gen_gi)
 189 [ apply sym_times
 190 | apply associative_times
 191 | intros.
 192   apply sym_eq.
 193   apply times_n_SO
 194 | assumption
 195 | assumption
 196 ]
 197 qed.
 198
 199 theorem eq_pi_p_gh:
 200 \forall g,h,h1: nat \to nat.\forall n,n1.
 201 \forall p1,p2:nat \to bool.
 202 (\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
 203 (\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to
 204 (\forall i. i < n \to p1 i = true \to h i < n1) \to
 205 (\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
 206 (\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to
 207 (\forall j. j < n1 \to p2 j = true \to h1 j < n) \to
 208 pi_p n p1 (\lambda x.g(h x)) = pi_p n1 p2 g.
 209 intros.
 210 unfold pi_p.
 211 apply (eq_iter_p_gen_gh nat (S O) times ? ? ? g h h1 n n1 p1 p2)
 212 [ apply sym_times
 213 | apply associative_times
 214 | intros.
 215   apply sym_eq.
 216   apply times_n_SO
 217 | assumption
 218 | assumption
 219 | assumption
 220 | assumption
 221 | assumption
 222 | assumption
 223 ]
 224 qed.
 225
 226 (* monotonicity *)
 227 theorem le_pi_p:
 228 \forall n:nat. \forall p:nat \to bool. \forall g1,g2:nat \to nat.
 229 (\forall i. i < n \to p i = true \to g1 i \le g2 i ) \to
 230 pi_p n p g1 \le pi_p n p g2.
 231 intros.
 232 elim n in H ⊢ %
 233   [apply le_n.
 234   |apply (bool_elim ? (p n1));intros
 235     [rewrite > true_to_pi_p_Sn
 236       [rewrite > true_to_pi_p_Sn in ⊢ (? ? %)
 237         [apply le_times
 238           [apply H1[apply le_n|assumption]
 239           |apply H.
 240            intros.
 241            apply H1[apply le_S.assumption|assumption]
 242           ]
 243         |assumption
 244         ]
 245       |assumption
 246       ]
 247     |rewrite > false_to_pi_p_Sn
 248       [rewrite > false_to_pi_p_Sn in ⊢ (? ? %)
 249         [apply H.
 250          intros.
 251          apply H1[apply le_S.assumption|assumption]
 252         |assumption
 253         ]
 254       |assumption
 255       ]
 256     ]
 257   ]
 258 qed.
 259
 260 theorem exp_sigma_p: \forall n,a,p.
 261 pi_p n p (\lambda x.a) = (exp a (sigma_p n p (\lambda x.S O))).
 262 intros.
 263 elim n
 264   [reflexivity
 265   |apply (bool_elim ? (p n1))
 266     [intro.
 267      rewrite > true_to_pi_p_Sn
 268       [rewrite > true_to_sigma_p_Sn
 269         [simplify.
 270          rewrite > H.
 271          reflexivity.
 272         |assumption
 273         ]
 274       |assumption
 275       ]
 276     |intro.
 277      rewrite > false_to_pi_p_Sn
 278       [rewrite > false_to_sigma_p_Sn
 279         [simplify.assumption
 280         |assumption
 281         ]
 282       |assumption
 283       ]
 284     ]
 285   ]
 286 qed.
 287
 288 theorem exp_sigma_p1: \forall n,a,p,f.
 289 pi_p n p (\lambda x.(exp a (f x))) = (exp a (sigma_p n p f)).
 290 intros.
 291 elim n
 292   [reflexivity
 293   |apply (bool_elim ? (p n1))
 294     [intro.
 295      rewrite > true_to_pi_p_Sn
 296       [rewrite > true_to_sigma_p_Sn
 297         [simplify.
 298          rewrite > H.
 299          rewrite > exp_plus_times.
 300          reflexivity.
 301         |assumption
 302         ]
 303       |assumption
 304       ]
 305     |intro.
 306      rewrite > false_to_pi_p_Sn
 307       [rewrite > false_to_sigma_p_Sn
 308         [simplify.assumption
 309         |assumption
 310         ]
 311       |assumption
 312       ]
 313     ]
 314   ]
 315 qed.
 316
 317 theorem times_pi_p: \forall n,p,f,g.
 318 pi_p n p (\lambda x.f x*g x) = pi_p n p f * pi_p n p  g.
 319 intros.
 320 elim n
 321   [simplify.reflexivity
 322   |apply (bool_elim ? (p n1))
 323     [intro.
 324      rewrite > true_to_pi_p_Sn
 325       [rewrite > true_to_pi_p_Sn
 326         [rewrite > true_to_pi_p_Sn
 327           [rewrite > H.autobatch
 328           |assumption
 329           ]
 330         |assumption
 331         ]
 332       |assumption
 333       ]
 334     |intro.
 335      rewrite > false_to_pi_p_Sn
 336       [rewrite > false_to_pi_p_Sn
 337         [rewrite > false_to_pi_p_Sn;assumption
 338         |assumption
 339         ]
 340       |assumption
 341       ]
 342     ]
 343   ]
 344 qed.
 345
 346 theorem pi_p_SO: \forall n,p.
 347 pi_p n p (\lambda i.S O) = S O.
 348 intros.elim n
 349   [reflexivity
 350   |simplify.elim (p n1)
 351     [simplify.rewrite < plus_n_O.assumption
 352     |simplify.assumption
 353     ]
 354   ]
 355 qed.
 356
 357 theorem exp_pi_p: \forall n,m,p,f.
 358 pi_p n p (\lambda x.exp (f x) m) = exp (pi_p n p f) m.
 359 intros.
 360 elim m
 361   [simplify.apply pi_p_SO
 362   |simplify.
 363    rewrite > times_pi_p.
 364    rewrite < H.
 365    reflexivity
 366   ]
 367 qed.
 368
 369 theorem exp_times_pi_p: \forall n,m,k,p,f.
 370 pi_p n p (\lambda x.exp k (m*(f x))) =
 371 exp (pi_p n p (\lambda x.exp k (f x))) m.
 372 intros.
 373 apply (trans_eq ? ? (pi_p n p (\lambda x.(exp (exp k (f x)) m))))
 374   [apply eq_pi_p;intros
 375     [reflexivity
 376     |apply sym_eq.rewrite > sym_times.
 377      apply exp_exp_times
 378     ]
 379   |apply exp_pi_p
 380   ]
 381 qed.
 382
 383
 384 theorem pi_p_knm:
 385 \forall g: nat \to nat.
 386 \forall h2:nat \to nat \to nat.
 387 \forall h11,h12:nat \to nat.
 388 \forall k,n,m.
 389 \forall p1,p21:nat \to bool.
 390 \forall p22:nat \to nat \to bool.
 391 (\forall x. x < k \to p1 x = true \to
 392 p21 (h11 x) = true ∧ p22 (h11 x) (h12 x) = true
 393 \land h2 (h11 x) (h12 x) = x
 394 \land (h11 x) < n \land (h12 x) < m) \to
 395 (\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to
 396 p1 (h2 i j) = true \land
 397 h11 (h2 i j) = i \land h12 (h2 i j) = j
 398 \land h2 i j < k) →
 399 (*
 400 Pi z < k | p1 z. g z =
 401 Pi x < n | p21 x. Pi y < m | p22 x y.g (h2 x y).
 402 *)
 403 pi_p k p1 g =
 404 pi_p n p21 (\lambda x:nat.pi_p m (p22 x) (\lambda y. g (h2 x y))).
 405 intros.
 406 unfold pi_p.unfold pi_p.
 407 apply (iter_p_gen_knm nat (S O) times sym_times assoc_times ? ? ? h11 h12)
 408   [intros.apply sym_eq.apply times_n_SO.
 409   |assumption
 410   |assumption
 411   ]
 412 qed.
 413
 414 theorem pi_p_pi_p:
 415 \forall g: nat \to nat \to nat.
 416 \forall h11,h12,h21,h22: nat \to nat \to nat.
 417 \forall n1,m1,n2,m2.
 418 \forall p11,p21:nat \to bool.
 419 \forall p12,p22:nat \to nat \to bool.
 420 (\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to
 421 p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
 422 \land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
 423 \land h11 i j < n1 \land h12 i j < m1) \to
 424 (\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to
 425 p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
 426 \land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
 427 \land (h21 i j) < n2 \land (h22 i j) < m2) \to
 428 pi_p n1 p11
 429      (\lambda x:nat .pi_p m1 (p12 x) (\lambda y. g x y)) =
 430 pi_p n2 p21
 431     (\lambda x:nat .pi_p m2 (p22 x)  (\lambda y. g (h11 x y) (h12 x y))).
 432 intros.
 433 unfold pi_p.unfold pi_p.
 434 apply (iter_p_gen_2_eq ? ? ? sym_times assoc_times ? ? ? ? h21 h22)
 435   [intros.apply sym_eq.apply times_n_SO.
 436   |assumption
 437   |assumption
 438   ]
 439 qed.
 440
 441 theorem pi_p_pi_p1:
 442 \forall g: nat \to nat \to nat.
 443 \forall n,m.
 444 \forall p11,p21:nat \to bool.
 445 \forall p12,p22:nat \to nat \to bool.
 446 (\forall x,y. x < n \to y < m \to
 447  (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to
 448 pi_p n p11 (\lambda x:nat.pi_p m (p12 x) (\lambda y. g x y)) =
 449 pi_p m p21 (\lambda y:nat.pi_p n (p22 y) (\lambda x. g x y)).
 450 intros.
 451 unfold pi_p.unfold pi_p.
 452 apply (iter_p_gen_iter_p_gen ? ? ? sym_times assoc_times)
 453   [intros.apply sym_eq.apply times_n_SO.
 454   |assumption
 455   ]
 456 qed.