helm/software/matita/library/nat/iteration2.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 set "baseuri" "cic:/matita/nat/iteration2".
  16
  17 include "nat/primes.ma".
  18 include "nat/ord.ma".
  19 include "nat/generic_sigma_p.ma".
  20 include "nat/count.ma".(*necessary just to use bool_to_nat and bool_to_nat_andb*)
  21
  22
  23 (* sigma_p on nautral numbers is a specialization of sigma_p_gen *)
  24 definition sigma_p: nat \to (nat \to bool) \to (nat \to nat) \to nat \def
  25 \lambda n, p, g. (sigma_p_gen n p nat g O plus).
  26
  27 theorem symmetricIntPlus: symmetric nat plus.
  28 change with (\forall a,b:nat. (plus a b) = (plus b a)).
  29 intros.
  30 rewrite > sym_plus.
  31 reflexivity.
  32 qed.
  33
  34 (*the following theorems on sigma_p in N are obtained by the more general ones
  35  * in sigma_p_gen.ma
  36  *)
  37 theorem true_to_sigma_p_Sn:
  38 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat.
  39 p n = true \to sigma_p (S n) p g =
  40 (g n)+(sigma_p n p g).
  41 intros.
  42 unfold sigma_p.
  43 apply true_to_sigma_p_Sn_gen.
  44 assumption.
  45 qed.
  46
  47 theorem false_to_sigma_p_Sn:
  48 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat.
  49 p n = false \to sigma_p (S n) p g = sigma_p n p g.
  50 intros.
  51 unfold sigma_p.
  52 apply false_to_sigma_p_Sn_gen.
  53 assumption.
  54
  55 qed.
  56
  57 theorem eq_sigma_p: \forall p1,p2:nat \to bool.
  58 \forall g1,g2: nat \to nat.\forall n.
  59 (\forall x.  x < n \to p1 x = p2 x) \to
  60 (\forall x.  x < n \to g1 x = g2 x) \to
  61 sigma_p n p1 g1 = sigma_p n p2 g2.
  62 intros.
  63 unfold sigma_p.
  64 apply eq_sigma_p_gen;
  65   assumption.
  66 qed.
  67
  68 theorem eq_sigma_p1: \forall p1,p2:nat \to bool.
  69 \forall g1,g2: nat \to nat.\forall n.
  70 (\forall x.  x < n \to p1 x = p2 x) \to
  71 (\forall x.  x < n \to p1 x = true \to g1 x = g2 x) \to
  72 sigma_p n p1 g1 = sigma_p n p2 g2.
  73 intros.
  74 unfold sigma_p.
  75 apply eq_sigma_p1_gen;
  76   assumption.
  77 qed.
  78
  79 theorem sigma_p_false:
  80 \forall g: nat \to nat.\forall n.sigma_p n (\lambda x.false) g = O.
  81 intros.
  82 unfold sigma_p.
  83 apply sigma_p_false_gen.
  84 qed.
  85
  86 theorem sigma_p_plus: \forall n,k:nat.\forall p:nat \to bool.
  87 \forall g: nat \to nat.
  88 sigma_p (k+n) p g
  89 = sigma_p k (\lambda x.p (x+n)) (\lambda x.g (x+n)) + sigma_p n p g.
  90 intros.
  91 unfold sigma_p.
  92 apply (sigma_p_plusA_gen nat n k p g O plus)
  93 [ apply symmetricIntPlus.
  94 | intros.
  95   apply sym_eq.
  96   apply plus_n_O
  97 | apply associative_plus
  98 ]
  99 qed.
 100
 101 theorem false_to_eq_sigma_p: \forall n,m:nat.n \le m \to
 102 \forall p:nat \to bool.
 103 \forall g: nat \to nat. (\forall i:nat. n \le i \to i < m \to
 104 p i = false) \to sigma_p m p g = sigma_p n p g.
 105 intros.
 106 unfold sigma_p.
 107 apply (false_to_eq_sigma_p_gen);
 108   assumption.
 109 qed.
 110
 111 theorem sigma_p2 :
 112 \forall n,m:nat.
 113 \forall p1,p2:nat \to bool.
 114 \forall g: nat \to nat \to nat.
 115 sigma_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 sigma_p n p1
 119   (\lambda x.sigma_p m p2 (g x)).
 120 intros.
 121 unfold sigma_p.
 122 apply (sigma_p2_gen n m p1 p2 nat g O plus)
 123 [ apply symmetricIntPlus
 124 | apply associative_plus
 125 | intros.
 126   apply sym_eq.
 127   apply plus_n_O
 128 ]
 129 qed.
 130
 131 theorem sigma_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 sigma_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 sigma_p n p1
 140   (\lambda x.sigma_p m (p2 x) (g x)).
 141 intros.
 142 unfold sigma_p.
 143 apply (sigma_p2_gen' n m p1 p2 nat g O plus)
 144 [ apply symmetricIntPlus
 145 | apply associative_plus
 146 | intros.
 147   apply sym_eq.
 148   apply plus_n_O
 149 ]
 150 qed.
 151
 152 lemma sigma_p_gi: \forall g: nat \to nat.
 153 \forall n,i.\forall p:nat \to bool.i < n \to p i = true \to
 154 sigma_p n p g = g i + sigma_p n (\lambda x. andb (p x) (notb (eqb x i))) g.
 155 intros.
 156 unfold sigma_p.
 157 apply (sigma_p_gi_gen)
 158 [ apply symmetricIntPlus
 159 | apply associative_plus
 160 | intros.
 161   apply sym_eq.
 162   apply plus_n_O
 163 | assumption
 164 | assumption
 165 ]
 166 qed.
 167
 168 theorem eq_sigma_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 sigma_p n p1 (\lambda x.g(h x)) = sigma_p n1 (\lambda x.p2 x) g.
 178 intros.
 179 unfold sigma_p.
 180 apply (eq_sigma_p_gh_gen nat O plus ? ? ? g h h1 n n1 p1 p2)
 181 [ apply symmetricIntPlus
 182 | apply associative_plus
 183 | intros.
 184   apply sym_eq.
 185   apply plus_n_O
 186 | assumption
 187 | assumption
 188 | assumption
 189 | assumption
 190 | assumption
 191 | assumption
 192 ]
 193 qed.
 194
 195
 196 theorem sigma_p_divides:
 197 \forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to
 198 \forall g: nat \to nat.
 199 sigma_p (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) g =
 200 sigma_p (S n) (\lambda x.divides_b x n)
 201   (\lambda x.sigma_p (S m) (\lambda y.true) (\lambda y.g (x*(exp p y)))).
 202 intros.
 203 unfold sigma_p.
 204 apply (sigma_p_divides_gen nat O plus n m p ? ? ? g)
 205 [ assumption
 206 | assumption
 207 | assumption
 208 | apply symmetricIntPlus
 209 | apply associative_plus
 210 | intros.
 211   apply sym_eq.
 212   apply plus_n_O
 213 ]
 214 qed.
 215
 216 theorem distributive_times_plus_sigma_p: \forall n,k:nat. \forall p:nat \to bool. \forall g:nat \to nat.
 217 k*(sigma_p n p g) = sigma_p n p (\lambda i:nat.k * (g i)).
 218 intros.
 219 apply (distributive_times_plus_sigma_p_generic nat plus O times n k p g)
 220 [ apply symmetricIntPlus
 221 | apply associative_plus
 222 | intros.
 223   apply sym_eq.
 224   apply plus_n_O
 225 | apply symmetric_times
 226 | apply distributive_times_plus
 227 | intros.
 228   rewrite < (times_n_O a).
 229   reflexivity
 230 ]
 231 qed.
 232
 233 (*some properties of sigma_p invoked with an "always true" predicate (in this
 234   way sigma_p just counts the elements, without doing any control) or with
 235   the nat \to nat function which always returns (S O).
 236   It 's not easily possible proving these theorems in a general form
 237   in generic_sigma_p.ma
 238  *)
 239
 240 theorem sigma_p_true: \forall n:nat.
 241 (sigma_p n (\lambda x.true) (\lambda x.S O)) = n.
 242 intros.
 243 elim n
 244 [ simplify.
 245   reflexivity
 246 | rewrite > (true_to_sigma_p_Sn n1 (\lambda x:nat.true) (\lambda x:nat.S O))
 247   [ rewrite > H.
 248     simplify.
 249     reflexivity
 250   | reflexivity
 251   ]
 252 ]
 253 qed.
 254
 255 theorem sigma_P_SO_to_sigma_p_true: \forall n:nat. \forall g:nat \to bool.
 256 sigma_p n g (\lambda n:nat. (S O)) =
 257 sigma_p n (\lambda x:nat.true) (\lambda i:nat.bool_to_nat (g i)).
 258 intros.
 259 elim n
 260 [ simplify.
 261   reflexivity
 262 | cut ((g n1) = true \lor (g n1) = false)
 263   [ rewrite > true_to_sigma_p_Sn in \vdash (? ? ? %)
 264     [ elim Hcut
 265       [ rewrite > H1.
 266         rewrite > true_to_sigma_p_Sn in \vdash (? ? % ?)
 267         [ simplify.
 268           apply eq_f.
 269           assumption
 270         | assumption
 271         ]
 272       | rewrite > H1.
 273         rewrite > false_to_sigma_p_Sn in \vdash (? ? % ?)
 274         [ simplify.
 275           assumption
 276         | assumption
 277         ]
 278       ]
 279     | reflexivity
 280     ]
 281   | elim (g n1)
 282     [ left.
 283       reflexivity
 284     | right.
 285       reflexivity
 286     ]
 287   ]
 288 ]
 289 qed.
 290
 291 (* I introduce an equivalence in the form map_iter_i in order to use
 292  * the existing result about permutation in that part of the library.
 293  *)
 294
 295 theorem eq_map_iter_i_sigma_p_alwaysTrue:  \forall n:nat.\forall g:nat \to nat.
 296 map_iter_i n g plus O = sigma_p (S n) (\lambda c:nat.true) g.
 297 intros.
 298 elim n
 299 [ simplify.
 300   rewrite < plus_n_O.
 301   reflexivity
 302 | rewrite > true_to_sigma_p_Sn
 303   [ simplify in \vdash (? ? % ?).
 304     rewrite < plus_n_O.
 305     apply eq_f.
 306     assumption
 307   | reflexivity
 308   ]
 309 ]
 310 qed.
 311
 312 theorem sigma_p_plus_1: \forall n:nat. \forall f,g:nat \to nat.
 313 sigma_p n (\lambda b:nat. true) (\lambda a:nat.(f a) + (g a)) =
 314 sigma_p n (\lambda b:nat. true) f + sigma_p n (\lambda b:nat. true) g.
 315 intros.
 316 elim n
 317 [ simplify.
 318   reflexivity
 319 | rewrite > true_to_sigma_p_Sn
 320   [ rewrite > (true_to_sigma_p_Sn n1 (\lambda c:nat.true) f)
 321     [ rewrite > (true_to_sigma_p_Sn n1 (\lambda c:nat.true) g)
 322       [ rewrite > assoc_plus in \vdash (? ? ? %).
 323         rewrite < assoc_plus in \vdash (? ? ? (? ? %)).
 324         rewrite < sym_plus in \vdash (? ? ? (? ? (? % ?))).
 325         rewrite > assoc_plus in \vdash (? ? ? (? ? %)).
 326         rewrite < assoc_plus in \vdash (? ? ? %).
 327         apply eq_f.
 328         assumption
 329       | reflexivity
 330       ]
 331     | reflexivity
 332     ]
 333   | reflexivity
 334   ]
 335 ]
 336 qed.
 337
 338
 339 theorem eq_sigma_p_sigma_p_times1 : \forall n,m:nat.\forall f:nat \to nat.
 340 sigma_p (n*m) (\lambda x:nat.true) f =
 341 sigma_p m (\lambda x:nat.true)
 342     (\lambda a.(sigma_p n (\lambda x:nat.true) (\lambda b.f (b*m + a)))).
 343 intro.
 344 elim n
 345 [ simplify.
 346   elim m
 347   [ simplify.
 348     reflexivity
 349   | rewrite > true_to_sigma_p_Sn
 350     [ rewrite < H.
 351       reflexivity
 352     | reflexivity
 353     ]
 354   ]
 355 | change in \vdash (? ? ? (? ? ? (\lambda a:?.%))) with ((f ((n1*m)+a)) +
 356   (sigma_p n1 (\lambda x:nat.true) (\lambda b:nat.f (b*m +a)))).
 357   rewrite > sigma_p_plus_1 in \vdash (? ? ? %).
 358   rewrite > (sym_times (S n1) m).
 359   rewrite < (times_n_Sm m  n1).
 360   rewrite > sigma_p_plus in \vdash (? ? % ?).
 361   apply eq_f2
 362   [ rewrite < (sym_times m n1).
 363     apply eq_sigma_p
 364     [ intros.
 365       reflexivity
 366     | intros.
 367       rewrite < (sym_plus ? (m * n1)).
 368       reflexivity
 369     ]
 370   | rewrite > (sym_times m n1).
 371     apply H
 372   ]
 373 ]
 374 qed.
 375
 376 theorem eq_sigma_p_sigma_p_times2 : \forall n,m:nat.\forall f:nat \to nat.
 377 sigma_p (n *m) (\lambda c:nat.true) f =
 378 sigma_p  n (\lambda c:nat.true)
 379   (\lambda a.(sigma_p m (\lambda c:nat.true) (\lambda b:nat.f (b* n + a)))).
 380 intros.
 381 rewrite > sym_times.
 382 apply eq_sigma_p_sigma_p_times1.
 383 qed.
 384
 385
 386 theorem sigma_p_times:\forall n,m:nat.
 387 \forall f,f1,f2:nat \to bool.
 388 \forall g:nat \to nat \to nat.
 389 \forall g1,g2: nat \to nat.
 390 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g b a) < (S n)*(S m)) \to
 391 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g1 (g b a)) = a) \to
 392 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g2 (g b a)) = b) \to
 393 (\forall a,b:nat. a < (S n) \to b < (S m) \to f (g b a) = andb (f2 b) (f1 a)) \to
 394 (sigma_p ((S n) * (S m)) f (\lambda c:nat.(S O))) =
 395 sigma_p (S n) f1 (\lambda c:nat.(S O)) * sigma_p (S m) f2 (\lambda c:nat.(S O)).
 396 intros.
 397
 398 rewrite > (sigma_P_SO_to_sigma_p_true ).
 399 rewrite > (S_pred ((S n)*(S m))) in \vdash (? ? (? % ? ?) ?)
 400 [ rewrite < (eq_map_iter_i_sigma_p_alwaysTrue (pred ((S n)* (S m)))).
 401   rewrite > (permut_to_eq_map_iter_i plus assoc_plus sym_plus ? ? ?
 402            (\lambda i.g (div i (S n)) (mod i (S n))))
 403   [ rewrite > eq_map_iter_i_sigma_p_alwaysTrue.
 404     rewrite < S_pred
 405     [ rewrite > eq_sigma_p_sigma_p_times2.
 406       apply (trans_eq ? ? (sigma_p (S n)  (\lambda c:nat.true)
 407         (\lambda a. sigma_p (S m) (\lambda c:nat.true)
 408                 (\lambda b.(bool_to_nat (f2 b))*(bool_to_nat (f1 a))))))
 409       [ apply eq_sigma_p;intros
 410         [ reflexivity
 411         | apply eq_sigma_p;intros
 412           [ reflexivity
 413           |
 414             rewrite > (div_mod_spec_to_eq (x1*(S n) + x) (S n) ((x1*(S n) + x)/(S n))
 415                                                   ((x1*(S n) + x) \mod (S n)) x1 x)
 416             [ rewrite > (div_mod_spec_to_eq2 (x1*(S n) + x) (S n) ((x1*(S n) + x)/(S n))
 417                                                   ((x1*(S n) + x) \mod (S n)) x1 x)
 418               [ rewrite > H3
 419                 [ apply bool_to_nat_andb
 420                 | assumption
 421                 | assumption
 422                 ]
 423               | apply div_mod_spec_div_mod.
 424                 apply lt_O_S
 425               | constructor 1
 426                 [ assumption
 427                 | reflexivity
 428                 ]
 429               ]
 430             | apply div_mod_spec_div_mod.
 431               apply lt_O_S
 432             | constructor 1
 433               [ assumption
 434               | reflexivity
 435               ]
 436             ]
 437           ]
 438         ]
 439       | apply (trans_eq ? ?
 440          (sigma_p (S n) (\lambda c:nat.true) (\lambda n.((bool_to_nat (f1 n)) *
 441          (sigma_p (S m) (\lambda c:nat.true) (\lambda n.bool_to_nat (f2 n)))))))
 442         [ apply eq_sigma_p;intros
 443           [ reflexivity
 444           | rewrite > distributive_times_plus_sigma_p.
 445             apply eq_sigma_p;intros
 446             [ reflexivity
 447             | rewrite > sym_times.
 448               reflexivity
 449             ]
 450           ]
 451         | apply sym_eq.
 452           rewrite > sigma_P_SO_to_sigma_p_true.
 453           rewrite > sigma_P_SO_to_sigma_p_true in \vdash (? ? (? ? %) ?).
 454           rewrite > sym_times.
 455           rewrite > distributive_times_plus_sigma_p.
 456           apply eq_sigma_p;intros
 457           [ reflexivity
 458           | rewrite > distributive_times_plus_sigma_p.
 459             rewrite < sym_times.
 460             rewrite > distributive_times_plus_sigma_p.
 461             apply eq_sigma_p;
 462               intros; reflexivity
 463           ]
 464         ]
 465       ]
 466     | apply lt_O_times_S_S
 467     ]
 468
 469   | unfold permut.
 470     split
 471     [ intros.
 472       rewrite < plus_n_O.
 473       apply le_S_S_to_le.
 474       rewrite < S_pred in \vdash (? ? %)
 475       [ change with ((g (i/(S n)) (i \mod (S n))) \lt (S n)*(S m)).
 476         apply H
 477         [ apply lt_mod_m_m.
 478           unfold lt.
 479           apply le_S_S.
 480           apply le_O_n
 481         | apply (lt_times_to_lt_l n).
 482           apply (le_to_lt_to_lt ? i)
 483           [ rewrite > (div_mod i (S n)) in \vdash (? ? %)
 484             [ rewrite > sym_plus.
 485               apply le_plus_n
 486             | unfold lt.
 487               apply le_S_S.
 488               apply le_O_n
 489             ]
 490           | unfold lt.
 491             rewrite > S_pred in \vdash (? ? %)
 492             [ apply le_S_S.
 493               rewrite > plus_n_O in \vdash (? ? %).
 494               rewrite > sym_times.
 495               assumption
 496             | apply lt_O_times_S_S
 497             ]
 498           ]
 499         ]
 500       | apply lt_O_times_S_S
 501       ]
 502     | rewrite < plus_n_O.
 503       unfold injn.
 504       intros.
 505       cut (i < (S n)*(S m))
 506       [ cut (j < (S n)*(S m))
 507         [ cut ((i \mod (S n)) < (S n))
 508           [ cut ((i/(S n)) < (S m))
 509             [ cut ((j \mod (S n)) < (S n))
 510               [ cut ((j/(S n)) < (S m))
 511                 [ rewrite > (div_mod i (S n))
 512                   [ rewrite > (div_mod j (S n))
 513                     [ rewrite < (H1 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3).
 514                       rewrite < (H2 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3) in \vdash (? ? (? % ?) ?).
 515                       rewrite < (H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5).
 516                       rewrite < (H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5) in \vdash (? ? ? (? % ?)).
 517                       rewrite > H6.
 518                       reflexivity
 519                     | unfold lt.
 520                       apply le_S_S.
 521                       apply le_O_n
 522                     ]
 523                   | unfold lt.
 524                     apply le_S_S.
 525                     apply le_O_n
 526                   ]
 527                 | apply (lt_times_to_lt_l n).
 528                   apply (le_to_lt_to_lt ? j)
 529                   [ rewrite > (div_mod j (S n)) in \vdash (? ? %)
 530                     [ rewrite > sym_plus.
 531                       apply le_plus_n
 532                     | unfold lt. apply le_S_S.
 533                       apply le_O_n
 534                     ]
 535                   | rewrite < sym_times.
 536                     assumption
 537                   ]
 538                 ]
 539               | apply lt_mod_m_m.
 540                 unfold lt.
 541                 apply le_S_S.
 542                 apply le_O_n
 543               ]
 544             | apply (lt_times_to_lt_l n).
 545               apply (le_to_lt_to_lt ? i)
 546               [ rewrite > (div_mod i (S n)) in \vdash (? ? %)
 547                 [ rewrite > sym_plus.
 548                   apply le_plus_n
 549                 | unfold lt.
 550                   apply le_S_S.
 551                   apply le_O_n
 552                 ]
 553               | rewrite < sym_times.
 554                 assumption
 555               ]
 556             ]
 557           | apply lt_mod_m_m.
 558             unfold lt.
 559             apply le_S_S.
 560             apply le_O_n
 561           ]
 562         | unfold lt.
 563           rewrite > S_pred in \vdash (? ? %)
 564           [ apply le_S_S.
 565             assumption
 566           | apply lt_O_times_S_S
 567           ]
 568         ]
 569       | unfold lt.
 570         rewrite > S_pred in \vdash (? ? %)
 571         [ apply le_S_S.
 572           assumption
 573         | apply lt_O_times_S_S
 574         ]
 575       ]
 576     ]
 577   | intros.
 578     apply False_ind.
 579     apply (not_le_Sn_O m1 H4)
 580   ]
 581 | apply lt_O_times_S_S
 582 ]
 583 qed.