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 theorem true_to_pi_p_Sn:
  26 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat.
  27 p n = true \to pi_p (S n) p g = (g n)*(pi_p n p g).
  28 intros.
  29 unfold pi_p.
  30 apply true_to_iter_p_gen_Sn.
  31 assumption.
  32 qed.
  33
  34 theorem false_to_pi_p_Sn:
  35 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat.
  36 p n = false \to pi_p (S n) p g = pi_p n p g.
  37 intros.
  38 unfold pi_p.
  39 apply false_to_iter_p_gen_Sn.
  40 assumption.
  41 qed.
  42
  43 theorem eq_pi_p: \forall p1,p2:nat \to bool.
  44 \forall g1,g2: nat \to nat.\forall n.
  45 (\forall x.  x < n \to p1 x = p2 x) \to
  46 (\forall x.  x < n \to g1 x = g2 x) \to
  47 pi_p n p1 g1 = pi_p n p2 g2.
  48 intros.
  49 unfold pi_p.
  50 apply eq_iter_p_gen;
  51 assumption.
  52 qed.
  53
  54 theorem eq_pi_p1: \forall p1,p2:nat \to bool.
  55 \forall g1,g2: nat \to nat.\forall n.
  56 (\forall x.  x < n \to p1 x = p2 x) \to
  57 (\forall x.  x < n \to p1 x = true \to g1 x = g2 x) \to
  58 pi_p n p1 g1 = pi_p n p2 g2.
  59 intros.
  60 unfold pi_p.
  61 apply eq_iter_p_gen1;
  62 assumption.
  63 qed.
  64
  65 theorem pi_p_false:
  66 \forall g: nat \to nat.\forall n.pi_p n (\lambda x.false) g = S O.
  67 intros.
  68 unfold pi_p.
  69 apply iter_p_gen_false.
  70 qed.
  71
  72 theorem pi_p_times: \forall n,k:nat.\forall p:nat \to bool.
  73 \forall g: nat \to nat.
  74 pi_p (k+n) p g
  75 = pi_p k (\lambda x.p (x+n)) (\lambda x.g (x+n)) * pi_p n p g.
  76 intros.
  77 unfold pi_p.
  78 apply (iter_p_gen_plusA nat n k p g (S O) times)
  79 [ apply sym_times.
  80 | intros.
  81   apply sym_eq.
  82   apply times_n_SO
  83 | apply associative_times
  84 ]
  85 qed.
  86
  87 theorem false_to_eq_pi_p: \forall n,m:nat.n \le m \to
  88 \forall p:nat \to bool.
  89 \forall g: nat \to nat. (\forall i:nat. n \le i \to i < m \to
  90 p i = false) \to pi_p m p g = pi_p n p g.
  91 intros.
  92 unfold pi_p.
  93 apply (false_to_eq_iter_p_gen);
  94 assumption.
  95 qed.
  96
  97 theorem or_false_eq_SO_to_eq_pi_p:
  98 \forall n,m:nat.\forall p:nat \to bool.
  99 \forall g: nat \to nat.
 100 n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false \lor g i = S O)
 101 \to pi_p m p g = pi_p n p g.
 102 intros.
 103 unfold pi_p.
 104 apply or_false_eq_baseA_to_eq_iter_p_gen
 105   [intros.simplify.rewrite < plus_n_O.reflexivity
 106   |assumption
 107   |assumption
 108   ]
 109 qed.
 110
 111 theorem pi_p2 :
 112 \forall n,m:nat.
 113 \forall p1,p2:nat \to bool.
 114 \forall g: nat \to nat \to nat.
 115 pi_p (n*m)
 116   (\lambda x.andb (p1 (div x m)) (p2 (mod x m)))
 117   (\lambda x.g (div x m) (mod x m)) =
 118 pi_p n p1
 119   (\lambda x.pi_p m p2 (g x)).
 120 intros.
 121 unfold pi_p.
 122 apply (iter_p_gen2 n m p1 p2 nat g (S O) times)
 123 [ apply sym_times
 124 | apply associative_times
 125 | intros.
 126   apply sym_eq.
 127   apply times_n_SO
 128 ]
 129 qed.
 130
 131 theorem pi_p2' :
 132 \forall n,m:nat.
 133 \forall p1:nat \to bool.
 134 \forall p2:nat \to nat \to bool.
 135 \forall g: nat \to nat \to nat.
 136 pi_p (n*m)
 137   (\lambda x.andb (p1 (div x m)) (p2 (div x m) (mod x  m)))
 138   (\lambda x.g (div x m) (mod x m)) =
 139 pi_p n p1
 140   (\lambda x.pi_p m (p2 x) (g x)).
 141 intros.
 142 unfold pi_p.
 143 apply (iter_p_gen2' n m p1 p2 nat g (S O) times)
 144 [ apply sym_times
 145 | apply associative_times
 146 | intros.
 147   apply sym_eq.
 148   apply times_n_SO
 149 ]
 150 qed.
 151
 152 lemma pi_p_gi: \forall g: nat \to nat.
 153 \forall n,i.\forall p:nat \to bool.i < n \to p i = true \to
 154 pi_p n p g = g i * pi_p n (\lambda x. andb (p x) (notb (eqb x i))) g.
 155 intros.
 156 unfold pi_p.
 157 apply (iter_p_gen_gi)
 158 [ apply sym_times
 159 | apply associative_times
 160 | intros.
 161   apply sym_eq.
 162   apply times_n_SO
 163 | assumption
 164 | assumption
 165 ]
 166 qed.
 167
 168 theorem eq_pi_p_gh:
 169 \forall g,h,h1: nat \to nat.\forall n,n1.
 170 \forall p1,p2:nat \to bool.
 171 (\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
 172 (\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to
 173 (\forall i. i < n \to p1 i = true \to h i < n1) \to
 174 (\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
 175 (\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to
 176 (\forall j. j < n1 \to p2 j = true \to h1 j < n) \to
 177 pi_p n p1 (\lambda x.g(h x)) = pi_p n1 p2 g.
 178 intros.
 179 unfold pi_p.
 180 apply (eq_iter_p_gen_gh nat (S O) times ? ? ? g h h1 n n1 p1 p2)
 181 [ apply sym_times
 182 | apply associative_times
 183 | intros.
 184   apply sym_eq.
 185   apply times_n_SO
 186 | assumption
 187 | assumption
 188 | assumption
 189 | assumption
 190 | assumption
 191 | assumption
 192 ]
 193 qed.
 194
 195 (* monotonicity *)
 196 theorem le_pi_p:
 197 \forall n:nat. \forall p:nat \to bool. \forall g1,g2:nat \to nat.
 198 (\forall i. i < n \to p i = true \to g1 i \le g2 i ) \to
 199 pi_p n p g1 \le pi_p n p g2.
 200 intros.
 201 elim n in H ⊢ %
 202   [apply le_n.
 203   |apply (bool_elim ? (p n1));intros
 204     [rewrite > true_to_pi_p_Sn
 205       [rewrite > true_to_pi_p_Sn in ⊢ (? ? %)
 206         [apply le_times
 207           [apply H1[apply le_n|assumption]
 208           |apply H.
 209            intros.
 210            apply H1[apply le_S.assumption|assumption]
 211           ]
 212         |assumption
 213         ]
 214       |assumption
 215       ]
 216     |rewrite > false_to_pi_p_Sn
 217       [rewrite > false_to_pi_p_Sn in ⊢ (? ? %)
 218         [apply H.
 219          intros.
 220          apply H1[apply le_S.assumption|assumption]
 221         |assumption
 222         ]
 223       |assumption
 224       ]
 225     ]
 226   ]
 227 qed.
 228
 229 theorem exp_sigma_p: \forall n,a,p.
 230 pi_p n p (\lambda x.a) = (exp a (sigma_p n p (\lambda x.S O))).
 231 intros.
 232 elim n
 233   [reflexivity
 234   |apply (bool_elim ? (p n1))
 235     [intro.
 236      rewrite > true_to_pi_p_Sn
 237       [rewrite > true_to_sigma_p_Sn
 238         [simplify.
 239          rewrite > H.
 240          reflexivity.
 241         |assumption
 242         ]
 243       |assumption
 244       ]
 245     |intro.
 246      rewrite > false_to_pi_p_Sn
 247       [rewrite > false_to_sigma_p_Sn
 248         [simplify.assumption
 249         |assumption
 250         ]
 251       |assumption
 252       ]
 253     ]
 254   ]
 255 qed.
 256
 257 theorem exp_sigma_p1: \forall n,a,p,f.
 258 pi_p n p (\lambda x.(exp a (f x))) = (exp a (sigma_p n p f)).
 259 intros.
 260 elim n
 261   [reflexivity
 262   |apply (bool_elim ? (p n1))
 263     [intro.
 264      rewrite > true_to_pi_p_Sn
 265       [rewrite > true_to_sigma_p_Sn
 266         [simplify.
 267          rewrite > H.
 268          rewrite > exp_plus_times.
 269          reflexivity.
 270         |assumption
 271         ]
 272       |assumption
 273       ]
 274     |intro.
 275      rewrite > false_to_pi_p_Sn
 276       [rewrite > false_to_sigma_p_Sn
 277         [simplify.assumption
 278         |assumption
 279         ]
 280       |assumption
 281       ]
 282     ]
 283   ]
 284 qed.
 285
 286 theorem times_pi_p: \forall n,p,f,g.
 287 pi_p n p (\lambda x.f x*g x) = pi_p n p f * pi_p n p  g.
 288 intros.
 289 elim n
 290   [simplify.reflexivity
 291   |apply (bool_elim ? (p n1))
 292     [intro.
 293      rewrite > true_to_pi_p_Sn
 294       [rewrite > true_to_pi_p_Sn
 295         [rewrite > true_to_pi_p_Sn
 296           [rewrite > H.autobatch
 297           |assumption
 298           ]
 299         |assumption
 300         ]
 301       |assumption
 302       ]
 303     |intro.
 304      rewrite > false_to_pi_p_Sn
 305       [rewrite > false_to_pi_p_Sn
 306         [rewrite > false_to_pi_p_Sn;assumption
 307         |assumption
 308         ]
 309       |assumption
 310       ]
 311     ]
 312   ]
 313 qed.
 314
 315 theorem pi_p_SO: \forall n,p.
 316 pi_p n p (\lambda i.S O) = S O.
 317 intros.elim n
 318   [reflexivity
 319   |simplify.elim (p n1)
 320     [simplify.rewrite < plus_n_O.assumption
 321     |simplify.assumption
 322     ]
 323   ]
 324 qed.
 325
 326 theorem exp_pi_p: \forall n,m,p,f.
 327 pi_p n p (\lambda x.exp (f x) m) = exp (pi_p n p f) m.
 328 intros.
 329 elim m
 330   [simplify.apply pi_p_SO
 331   |simplify.
 332    rewrite > times_pi_p.
 333    rewrite < H.
 334    reflexivity
 335   ]
 336 qed.
 337
 338 theorem exp_times_pi_p: \forall n,m,k,p,f.
 339 pi_p n p (\lambda x.exp k (m*(f x))) =
 340 exp (pi_p n p (\lambda x.exp k (f x))) m.
 341 intros.
 342 apply (trans_eq ? ? (pi_p n p (\lambda x.(exp (exp k (f x)) m))))
 343   [apply eq_pi_p;intros
 344     [reflexivity
 345     |apply sym_eq.rewrite > sym_times.
 346      apply exp_exp_times
 347     ]
 348   |apply exp_pi_p
 349   ]
 350 qed.
 351
 352
 353 theorem pi_p_knm:
 354 \forall g: nat \to nat.
 355 \forall h2:nat \to nat \to nat.
 356 \forall h11,h12:nat \to nat.
 357 \forall k,n,m.
 358 \forall p1,p21:nat \to bool.
 359 \forall p22:nat \to nat \to bool.
 360 (\forall x. x < k \to p1 x = true \to
 361 p21 (h11 x) = true \land p22 (h11 x) (h12 x) = true
 362 \land h2 (h11 x) (h12 x) = x
 363 \land (h11 x) < n \land (h12 x) < m) \to
 364 (\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to
 365 p1 (h2 i j) = true \land
 366 h11 (h2 i j) = i \land h12 (h2 i j) = j
 367 \land h2 i j < k) \to
 368 pi_p k p1 g =
 369 pi_p n p21 (\lambda x:nat.pi_p m (p22 x) (\lambda y. g (h2 x y))).
 370 intros.
 371 unfold pi_p.unfold pi_p.
 372 apply (iter_p_gen_knm nat (S O) times sym_times assoc_times ? ? ? h11 h12)
 373   [intros.apply sym_eq.apply times_n_SO.
 374   |assumption
 375   |assumption
 376   ]
 377 qed.
 378
 379 theorem pi_p_pi_p:
 380 \forall g: nat \to nat \to nat.
 381 \forall h11,h12,h21,h22: nat \to nat \to nat.
 382 \forall n1,m1,n2,m2.
 383 \forall p11,p21:nat \to bool.
 384 \forall p12,p22:nat \to nat \to bool.
 385 (\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to
 386 p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
 387 \land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
 388 \land h11 i j < n1 \land h12 i j < m1) \to
 389 (\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to
 390 p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
 391 \land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
 392 \land (h21 i j) < n2 \land (h22 i j) < m2) \to
 393 pi_p n1 p11
 394      (\lambda x:nat .pi_p m1 (p12 x) (\lambda y. g x y)) =
 395 pi_p n2 p21
 396     (\lambda x:nat .pi_p m2 (p22 x)  (\lambda y. g (h11 x y) (h12 x y))).
 397 intros.
 398 unfold pi_p.unfold pi_p.
 399 apply (iter_p_gen_2_eq ? ? ? sym_times assoc_times ? ? ? ? h21 h22)
 400   [intros.apply sym_eq.apply times_n_SO.
 401   |assumption
 402   |assumption
 403   ]
 404 qed.
 405
 406 theorem pi_p_pi_p1:
 407 \forall g: nat \to nat \to nat.
 408 \forall n,m.
 409 \forall p11,p21:nat \to bool.
 410 \forall p12,p22:nat \to nat \to bool.
 411 (\forall x,y. x < n \to y < m \to
 412  (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to
 413 pi_p n p11 (\lambda x:nat.pi_p m (p12 x) (\lambda y. g x y)) =
 414 pi_p m p21 (\lambda y:nat.pi_p n (p22 y) (\lambda x. g x y)).
 415 intros.
 416 unfold pi_p.unfold pi_p.
 417 apply (iter_p_gen_iter_p_gen ? ? ? sym_times assoc_times)
 418   [intros.apply sym_eq.apply times_n_SO.
 419   |assumption
 420   ]
 421 qed.