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 generalize in match H.
 202 elim n
 203   [apply le_n.
 204   |apply (bool_elim ? (p n1));intros
 205     [rewrite > true_to_pi_p_Sn
 206       [rewrite > true_to_pi_p_Sn in ⊢ (? ? %)
 207         [apply le_times
 208           [apply H2[apply le_n|assumption]
 209           |apply H1.
 210            intros.
 211            apply H2[apply le_S.assumption|assumption]
 212           ]
 213         |assumption
 214         ]
 215       |assumption
 216       ]
 217     |rewrite > false_to_pi_p_Sn
 218       [rewrite > false_to_pi_p_Sn in ⊢ (? ? %)
 219         [apply H1.
 220          intros.
 221          apply H2[apply le_S.assumption|assumption]
 222         |assumption
 223         ]
 224       |assumption
 225       ]
 226     ]
 227   ]
 228 qed.
 229
 230 theorem exp_sigma_p: \forall n,a,p.
 231 pi_p n p (\lambda x.a) = (exp a (sigma_p n p (\lambda x.S O))).
 232 intros.
 233 elim n
 234   [reflexivity
 235   |apply (bool_elim ? (p n1))
 236     [intro.
 237      rewrite > true_to_pi_p_Sn
 238       [rewrite > true_to_sigma_p_Sn
 239         [simplify.
 240          rewrite > H.
 241          reflexivity.
 242         |assumption
 243         ]
 244       |assumption
 245       ]
 246     |intro.
 247      rewrite > false_to_pi_p_Sn
 248       [rewrite > false_to_sigma_p_Sn
 249         [simplify.assumption
 250         |assumption
 251         ]
 252       |assumption
 253       ]
 254     ]
 255   ]
 256 qed.
 257
 258 theorem exp_sigma_p1: \forall n,a,p,f.
 259 pi_p n p (\lambda x.(exp a (f x))) = (exp a (sigma_p n p f)).
 260 intros.
 261 elim n
 262   [reflexivity
 263   |apply (bool_elim ? (p n1))
 264     [intro.
 265      rewrite > true_to_pi_p_Sn
 266       [rewrite > true_to_sigma_p_Sn
 267         [simplify.
 268          rewrite > H.
 269          rewrite > exp_plus_times.
 270          reflexivity.
 271         |assumption
 272         ]
 273       |assumption
 274       ]
 275     |intro.
 276      rewrite > false_to_pi_p_Sn
 277       [rewrite > false_to_sigma_p_Sn
 278         [simplify.assumption
 279         |assumption
 280         ]
 281       |assumption
 282       ]
 283     ]
 284   ]
 285 qed.
 286
 287 theorem times_pi_p: \forall n,p,f,g.
 288 pi_p n p (\lambda x.f x*g x) = pi_p n p f * pi_p n p  g.
 289 intros.
 290 elim n
 291   [simplify.reflexivity
 292   |apply (bool_elim ? (p n1))
 293     [intro.
 294      rewrite > true_to_pi_p_Sn
 295       [rewrite > true_to_pi_p_Sn
 296         [rewrite > true_to_pi_p_Sn
 297           [rewrite > H.autobatch
 298           |assumption
 299           ]
 300         |assumption
 301         ]
 302       |assumption
 303       ]
 304     |intro.
 305      rewrite > false_to_pi_p_Sn
 306       [rewrite > false_to_pi_p_Sn
 307         [rewrite > false_to_pi_p_Sn;assumption
 308         |assumption
 309         ]
 310       |assumption
 311       ]
 312     ]
 313   ]
 314 qed.
 315
 316 theorem pi_p_SO: \forall n,p.
 317 pi_p n p (\lambda i.S O) = S O.
 318 intros.elim n
 319   [reflexivity
 320   |simplify.elim (p n1)
 321     [simplify.rewrite < plus_n_O.assumption
 322     |simplify.assumption
 323     ]
 324   ]
 325 qed.
 326
 327 theorem exp_pi_p: \forall n,m,p,f.
 328 pi_p n p (\lambda x.exp (f x) m) = exp (pi_p n p f) m.
 329 intros.
 330 elim m
 331   [simplify.apply pi_p_SO
 332   |simplify.
 333    rewrite > times_pi_p.
 334    rewrite < H.
 335    reflexivity
 336   ]
 337 qed.
 338
 339 theorem exp_times_pi_p: \forall n,m,k,p,f.
 340 pi_p n p (\lambda x.exp k (m*(f x))) =
 341 exp (pi_p n p (\lambda x.exp k (f x))) m.
 342 intros.
 343 apply (trans_eq ? ? (pi_p n p (\lambda x.(exp (exp k (f x)) m))))
 344   [apply eq_pi_p;intros
 345     [reflexivity
 346     |apply sym_eq.rewrite > sym_times.
 347      apply exp_exp_times
 348     ]
 349   |apply exp_pi_p
 350   ]
 351 qed.
 352
 353
 354 theorem pi_p_knm:
 355 \forall g: nat \to nat.
 356 \forall h2:nat \to nat \to nat.
 357 \forall h11,h12:nat \to nat.
 358 \forall k,n,m.
 359 \forall p1,p21:nat \to bool.
 360 \forall p22:nat \to nat \to bool.
 361 (\forall x. x < k \to p1 x = true \to
 362 p21 (h11 x) = true \land p22 (h11 x) (h12 x) = true
 363 \land h2 (h11 x) (h12 x) = x
 364 \land (h11 x) < n \land (h12 x) < m) \to
 365 (\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to
 366 p1 (h2 i j) = true \land
 367 h11 (h2 i j) = i \land h12 (h2 i j) = j
 368 \land h2 i j < k) \to
 369 pi_p k p1 g =
 370 pi_p n p21 (\lambda x:nat.pi_p m (p22 x) (\lambda y. g (h2 x y))).
 371 intros.
 372 unfold pi_p.unfold pi_p.
 373 apply (iter_p_gen_knm nat (S O) times sym_times assoc_times ? ? ? h11 h12)
 374   [intros.apply sym_eq.apply times_n_SO.
 375   |assumption
 376   |assumption
 377   ]
 378 qed.
 379
 380 theorem pi_p_pi_p:
 381 \forall g: nat \to nat \to nat.
 382 \forall h11,h12,h21,h22: nat \to nat \to nat.
 383 \forall n1,m1,n2,m2.
 384 \forall p11,p21:nat \to bool.
 385 \forall p12,p22:nat \to nat \to bool.
 386 (\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to
 387 p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
 388 \land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
 389 \land h11 i j < n1 \land h12 i j < m1) \to
 390 (\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to
 391 p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
 392 \land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
 393 \land (h21 i j) < n2 \land (h22 i j) < m2) \to
 394 pi_p n1 p11
 395      (\lambda x:nat .pi_p m1 (p12 x) (\lambda y. g x y)) =
 396 pi_p n2 p21
 397     (\lambda x:nat .pi_p m2 (p22 x)  (\lambda y. g (h11 x y) (h12 x y))).
 398 intros.
 399 unfold pi_p.unfold pi_p.
 400 apply (iter_p_gen_2_eq ? ? ? sym_times assoc_times ? ? ? ? h21 h22)
 401   [intros.apply sym_eq.apply times_n_SO.
 402   |assumption
 403   |assumption
 404   ]
 405 qed.
 406
 407 theorem pi_p_pi_p1:
 408 \forall g: nat \to nat \to nat.
 409 \forall n,m.
 410 \forall p11,p21:nat \to bool.
 411 \forall p12,p22:nat \to nat \to bool.
 412 (\forall x,y. x < n \to y < m \to
 413  (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to
 414 pi_p n p11 (\lambda x:nat.pi_p m (p12 x) (\lambda y. g x y)) =
 415 pi_p m p21 (\lambda y:nat.pi_p n (p22 y) (\lambda x. g x y)).
 416 intros.
 417 unfold pi_p.unfold pi_p.
 418 apply (iter_p_gen_iter_p_gen ? ? ? sym_times assoc_times)
 419   [intros.apply sym_eq.apply times_n_SO.
 420   |assumption
 421   ]
 422 qed.