helm/software/matita/library/Q/frac.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 (*
  16 let rec nat_fact_to_fraction_inv l \def
  17   match l with
  18   [nf_last a \Rightarrow nn a
  19   |nf_cons a p \Rightarrow
  20     cons (neg_Z_of_nat a) (nat_fact_to_fraction_inv p)
  21   ]
  22 .
  23
  24 definition nat_fact_all_to_Q_inv \def
  25 \lambda n.
  26   match n with
  27   [nfa_zero \Rightarrow OQ
  28   |nfa_one \Rightarrow Qpos one
  29   |nfa_proper l \Rightarrow Qpos (frac (nat_fact_to_fraction_inv l))
  30   ]
  31 .
  32
  33 definition nat_to_Q_inv \def
  34 \lambda n. nat_fact_all_to_Q_inv (factorize n).
  35 *)
  36
  37 definition frac:nat \to nat \to Q \def
  38 \lambda p,q. Qtimes (nat_to_Q p) (Qinv (nat_to_Q q)).
  39
  40 let rec times_f h g \def
  41   match h with
  42   [nf_last a \Rightarrow
  43     match g with
  44     [nf_last b \Rightarrow nf_last (S (a+b))
  45     |nf_cons b g1 \Rightarrow nf_cons (S (a+b)) g1
  46     ]
  47   |nf_cons a h1 \Rightarrow
  48     match g with
  49     [nf_last b \Rightarrow nf_cons (S (a+b)) h1
  50     |nf_cons b g1 \Rightarrow nf_cons (a+b) (times_f h1 g1)
  51     ]
  52   ]
  53 .
  54
  55 definition times_fa \def
  56 \lambda f,g.
  57 match f with
  58 [nfa_zero \Rightarrow nfa_zero
  59 |nfa_one \Rightarrow g
  60 |nfa_proper f1 \Rightarrow match g with
  61   [nfa_zero \Rightarrow nfa_zero
  62   |nfa_one \Rightarrow nfa_proper f1
  63   |nfa_proper g1 \Rightarrow nfa_proper (times_f f1 g1)
  64   ]
  65 ]
  66 .
  67
  68 theorem eq_times_f_times1:\forall g,h,m. defactorize_aux (times_f g h) m
  69 =defactorize_aux g m*defactorize_aux h m.
  70 intro.elim g
  71   [elim h;simplify;autobatch
  72   |elim h
  73     [simplify;autobatch
  74     |simplify.rewrite > (H n3 (S m)).autobatch
  75     ]
  76   ]
  77 qed.
  78
  79 theorem eq_times_fa_times: \forall f,g.
  80 defactorize (times_fa f g) = defactorize f*defactorize g.
  81 intros.
  82 elim f
  83   [reflexivity
  84   |simplify.apply plus_n_O
  85   |elim g;simplify
  86     [apply times_n_O
  87     |apply times_n_SO
  88     |apply eq_times_f_times1
  89     ]
  90   ]
  91 qed.
  92
  93 theorem eq_times_times_fa: \forall n,m.
  94 factorize (n*m) = times_fa (factorize n) (factorize m).
  95 intros.
  96 rewrite <(factorize_defactorize (times_fa (factorize n) (factorize m))).
  97 rewrite > eq_times_fa_times.
  98 rewrite > defactorize_factorize.
  99 rewrite > defactorize_factorize.
 100 reflexivity.
 101 qed.
 102
 103
 104 theorem eq_plus_Zplus: \forall n,m:nat. Z_of_nat (n+m) =
 105 Z_of_nat n + Z_of_nat m.
 106 intro.cases n;intro
 107   [reflexivity
 108   |cases m
 109     [simplify.rewrite < plus_n_O.reflexivity
 110     |simplify.reflexivity.
 111     ]
 112   ]
 113 qed.
 114
 115 theorem times_f_ftimes: \forall n,m.
 116 frac (nat_fact_to_fraction (times_f n m))
 117 = ftimes (nat_fact_to_fraction n) (nat_fact_to_fraction m).
 118 intro.
 119 elim n
 120   [elim m
 121     [simplify.
 122      rewrite < plus_n_Sm.reflexivity
 123     |elim n2
 124       [simplify.rewrite < plus_n_O.reflexivity
 125       |simplify.reflexivity.
 126       ]
 127     ]
 128   |elim m
 129     [elim n1
 130       [simplify.reflexivity
 131       |simplify.rewrite < plus_n_Sm.reflexivity
 132       ]
 133     |simplify.
 134      cut (\exist h.ftimes (nat_fact_to_fraction n2) (nat_fact_to_fraction n4) = frac h)
 135       [elim Hcut.
 136        rewrite > H2.
 137        simplify.apply eq_f.
 138        apply eq_f2
 139         [apply eq_plus_Zplus
 140         |apply injective_frac.
 141          rewrite < H2.
 142          apply H
 143         ]
 144       |generalize in match n4.
 145        elim n2
 146         [cases n6;simplify;autobatch
 147         |cases n7;simplify
 148           [autobatch
 149           |elim (H2 n9).
 150            rewrite > H3.
 151            simplify.
 152            autobatch
 153           ]
 154         ]
 155       ]
 156     ]
 157   ]
 158 qed.
 159
 160 theorem times_fa_Qtimes: \forall f,g. nat_fact_all_to_Q (times_fa f g) =
 161 Qtimes (nat_fact_all_to_Q f) (nat_fact_all_to_Q g).
 162 intros.
 163 cases f;simplify
 164   [reflexivity
 165   |cases g;reflexivity
 166   |cases g;simplify
 167     [reflexivity
 168     |reflexivity
 169     |rewrite > times_f_ftimes.reflexivity
 170     ]
 171   ]
 172 qed.
 173
 174 theorem times_Qtimes: \forall p,q.
 175 (nat_to_Q (p*q)) = Qtimes (nat_to_Q p) (nat_to_Q q).
 176 intros.unfold nat_to_Q.
 177 rewrite < times_fa_Qtimes.
 178 rewrite < eq_times_times_fa.
 179 reflexivity.
 180 qed.
 181
 182 theorem rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction.
 183 (rtimes (frac f) (frac g) = one \land
 184  rtimes (frac (cons x f)) (frac (cons y g)) = nat_frac_item_to_ratio (x + y))
 185 \lor (\exists h.rtimes (frac f) (frac g) = frac h \land
 186 rtimes (frac (cons x f)) (frac (cons y g)) =
 187 frac (cons (x + y) h)).
 188 intros.
 189 simplify.
 190 elim (rtimes (frac f) (frac g));simplify
 191   [left.split;reflexivity
 192   |right.
 193    apply (ex_intro ? ? f1).
 194    split;reflexivity
 195   ]
 196 qed.
 197
 198 theorem associative_Qtimes:associative ? Qtimes.
 199 unfold.intros.
 200 cases x
 201   [reflexivity
 202    (* non posso scrivere 2,3: ... ?? *)
 203   |cases y
 204     [reflexivity.
 205     |cases z
 206       [reflexivity
 207       |simplify.rewrite > associative_rtimes.
 208        reflexivity.
 209       |simplify.rewrite > associative_rtimes.
 210        reflexivity
 211       ]
 212     |cases z
 213       [reflexivity
 214       |simplify.rewrite > associative_rtimes.
 215        reflexivity.
 216       |simplify.rewrite > associative_rtimes.
 217        reflexivity
 218       ]
 219     ]
 220   |cases y
 221     [reflexivity.
 222     |cases z
 223       [reflexivity
 224       |simplify.rewrite > associative_rtimes.
 225        reflexivity.
 226       |simplify.rewrite > associative_rtimes.
 227        reflexivity
 228       ]
 229     |cases z
 230       [reflexivity
 231       |simplify.rewrite > associative_rtimes.
 232        reflexivity.
 233       |simplify.rewrite > associative_rtimes.
 234        reflexivity
 235       ]
 236     ]
 237   ]
 238 qed.
 239
 240 theorem Qtimes_OQ: \forall q.Qtimes q OQ = OQ.
 241 intro.cases q;reflexivity.
 242 qed.
 243
 244 theorem symmetric_Qtimes: symmetric ? Qtimes.
 245 unfold.intros.
 246 cases x
 247   [simplify in ⊢ (? ? % ?).rewrite > Qtimes_OQ.reflexivity
 248   |elim y
 249     [reflexivity
 250     |simplify.rewrite > symmetric_rtimes.reflexivity
 251     |simplify.rewrite > symmetric_rtimes.reflexivity
 252     ]
 253   |elim y
 254     [reflexivity
 255     |simplify.rewrite > symmetric_rtimes.reflexivity
 256     |simplify.rewrite > symmetric_rtimes.reflexivity
 257     ]
 258   ]
 259 qed.
 260
 261 theorem Qtimes_Qinv: \forall q. q \neq OQ \to Qtimes q (Qinv q) = Qone.
 262 intro.
 263 cases q;intro
 264   [elim H.reflexivity
 265   |simplify.rewrite > rtimes_rinv.reflexivity
 266   |simplify.rewrite > rtimes_rinv.reflexivity
 267   ]
 268 qed.
 269
 270 theorem eq_Qtimes_OQ_to_eq_OQ: \forall p,q.
 271 Qtimes p q = OQ \to p = OQ \lor q = OQ.
 272 intros 2.
 273 cases p
 274   [intro.left.reflexivity
 275   |cases q
 276     [intro.right.reflexivity
 277     |simplify.intro.destruct H
 278     |simplify.intro.destruct H
 279     ]
 280   |cases q
 281     [intro.right.reflexivity
 282     |simplify.intro.destruct H
 283     |simplify.intro.destruct H
 284     ]
 285   ]
 286 qed.
 287
 288 theorem Qinv_Qtimes: \forall p,q.
 289 p \neq OQ \to q \neq OQ \to
 290 Qinv(Qtimes p q) =
 291 Qtimes (Qinv p) (Qinv q).
 292 intros.
 293 rewrite < Qtimes_Qone_q in ⊢ (? ? ? %).
 294 rewrite < (Qtimes_Qinv (Qtimes p q))
 295   [lapply (Qtimes_Qinv ? H).
 296    lapply (Qtimes_Qinv ? H1).
 297    rewrite > symmetric_Qtimes in ⊢ (? ? ? (? % ?)).
 298    rewrite > associative_Qtimes.
 299    rewrite > associative_Qtimes.
 300    rewrite < associative_Qtimes in ⊢ (? ? ? (? ? (? ? %))).
 301    rewrite < symmetric_Qtimes in ⊢ (? ? ? (? ? (? ? (? % ?)))).
 302    rewrite > associative_Qtimes in ⊢ (? ? ? (? ? (? ? %))).
 303    rewrite > Hletin1.
 304    rewrite > Qtimes_q_Qone.
 305    rewrite > Hletin.
 306    rewrite > Qtimes_q_Qone.
 307    reflexivity
 308   |intro.
 309    elim (eq_Qtimes_OQ_to_eq_OQ ? ? H2)
 310     [apply (H H3)|apply (H1 H3)]
 311   ]
 312 qed.
 313
 314 (* a stronger version, taking advantage of inv(O) = O *)
 315 theorem Qinv_Qtimes': \forall p,q.
 316 Qinv(Qtimes p q) =
 317 Qtimes (Qinv p) (Qinv q).
 318 intros.
 319 cases p
 320   [reflexivity
 321   |cases q
 322     [reflexivity
 323     |apply Qinv_Qtimes;intro;destruct H
 324     |apply Qinv_Qtimes;intro;destruct H
 325     ]
 326   |cases q
 327     [reflexivity
 328     |apply Qinv_Qtimes;intro;destruct H
 329     |apply Qinv_Qtimes;intro;destruct H
 330     ]
 331   ]
 332 qed.
 333
 334 theorem Qtimes_frac_frac: \forall p,q,r,s.
 335 Qtimes (frac p q) (frac r s) = (frac (p*r) (q*s)).
 336 intros.
 337 unfold frac.
 338 rewrite > associative_Qtimes.
 339 rewrite < associative_Qtimes in ⊢ (? ? (? ? %) ?).
 340 rewrite > symmetric_Qtimes in ⊢ (? ? (? ? (? % ?)) ?).
 341 rewrite > associative_Qtimes in ⊢ (? ? (? ? %) ?).
 342 rewrite < associative_Qtimes.
 343 rewrite < times_Qtimes.
 344 rewrite < Qinv_Qtimes'.
 345 rewrite < times_Qtimes.
 346 reflexivity.
 347 qed.
 348
 349
 350 (* la prova seguente e' tutta una ripetizione. Sistemare. *)
 351 (*CSC
 352 theorem Qtimes1: \forall f:fraction.
 353 Qtimes (nat_fact_all_to_Q (numerator f))
 354 (Qinv (nat_fact_all_to_Q (numerator (finv f))))
 355 = Qpos (frac f).
 356 simplify.
 357 intro.elim f
 358   [reflexivity
 359   |reflexivity
 360   |elim (or_numerator_nfa_one_nfa_proper f1)
 361     [elim H1.clear H1.
 362      elim H3.clear H3.
 363      cut (finv (nat_fact_to_fraction a) = f1)
 364       [elim z
 365         [simplify.
 366          rewrite > H2.rewrite > H1.simplify.
 367          rewrite > Hcut.reflexivity
 368         |simplify.
 369          rewrite > H2.rewrite > H1.simplify.
 370          rewrite > Hcut.reflexivity
 371         |simplify.
 372          rewrite > H2.rewrite > H1.simplify.
 373          rewrite > Hcut.reflexivity
 374         ]
 375       |generalize in match H.
 376        rewrite > H2.rewrite > H1.simplify.
 377        intro.destruct H3.assumption
 378       ]
 379     |elim H1.clear H1.
 380      elim z
 381       [simplify.
 382        rewrite > H2.rewrite > H2.simplify.
 383        elim (or_numerator_nfa_one_nfa_proper (finv f1))
 384         [elim H1.clear H1.
 385          rewrite > H3.simplify.
 386          cut (nat_fact_to_fraction a = f1)
 387           [rewrite > Hcut.reflexivity
 388           |generalize in match H.
 389            rewrite > H2.
 390            rewrite > H3.
 391            rewrite > Qtimes_q_Qone.
 392            intro.
 393            destruct H1.
 394            assumption
 395           ]
 396         |elim H1.clear H1.
 397          generalize in match H.
 398          rewrite > H2.
 399          rewrite > H3.simplify.
 400          intro.
 401          destruct H1.
 402          rewrite > Hcut.
 403          simplify.reflexivity
 404         ]
 405       |simplify.rewrite > H2.simplify.
 406         elim (or_numerator_nfa_one_nfa_proper (finv f1))
 407         [elim H1.clear H1.
 408          rewrite > H3.simplify.
 409          cut (nat_fact_to_fraction a = f1)
 410           [rewrite > Hcut.reflexivity
 411           |generalize in match H.
 412            rewrite > H2.
 413            rewrite > H3.
 414            rewrite > Qtimes_q_Qone.
 415            intro.
 416            destruct H1.
 417            assumption
 418           ]
 419         |elim H1.clear H1.
 420          generalize in match H.
 421          rewrite > H2.
 422          rewrite > H3.simplify.
 423          intro.
 424          destruct H1.
 425          rewrite > Hcut.
 426          simplify.reflexivity
 427         ]
 428       |simplify.rewrite > H2.simplify.
 429         elim (or_numerator_nfa_one_nfa_proper (finv f1))
 430         [elim H1.clear H1.
 431          rewrite > H3.simplify.
 432          cut (nat_fact_to_fraction a = f1)
 433           [rewrite > Hcut.reflexivity
 434           |generalize in match H.
 435            rewrite > H2.
 436            rewrite > H3.
 437            rewrite > Qtimes_q_Qone.
 438            intro.
 439            destruct H1.
 440            assumption
 441           ]
 442         |elim H1.clear H1.
 443          generalize in match H.
 444          rewrite > H2.
 445          rewrite > H3.simplify.
 446          intro.
 447          destruct H1.
 448          rewrite > Hcut.
 449          simplify.reflexivity
 450         ]
 451       ]
 452     ]
 453   ]
 454 qed.
 455 *)
 456 (*
 457 definition numQ:Q \to Z \def
 458 \lambda q.
 459 match q with
 460 [OQ \Rightarrow OZ
 461 |Qpos r \Rightarrow Z_of_nat (defactorize (numeratorQ (Qpos r)))
 462 |Qneg r \Rightarrow neg_Z_of_nat (defactorize (numeratorQ (Qpos r)))
 463 ].
 464 *)
 465
 466 definition numQ:Q \to nat \def
 467 \lambda q. defactorize (numeratorQ q).
 468
 469 definition denomQ:Q \to nat \def
 470 \lambda q. defactorize (numeratorQ (Qinv q)).
 471
 472 definition Qopp:Q \to Q \def \lambda q.
 473 match q with
 474 [OQ \Rightarrow OQ
 475 |Qpos q \Rightarrow Qneg q
 476 |Qneg q \Rightarrow Qpos q
 477 ].
 478 (*CSC
 479 theorem frac_numQ_denomQ1: \forall r:ratio.
 480 frac (numQ (Qpos r)) (denomQ (Qpos r)) = (Qpos r).
 481 intro.
 482 unfold frac.unfold denomQ.unfold numQ.
 483 unfold nat_to_Q.
 484 rewrite > factorize_defactorize.
 485 rewrite > factorize_defactorize.
 486 elim r
 487   [reflexivity
 488   |elim f
 489     [reflexivity
 490     |reflexivity
 491     |apply Qtimes1.
 492     ]
 493   ]
 494 qed.*)
 495
 496 (*CSC
 497 theorem frac_numQ_denomQ2: \forall r:ratio.
 498 frac (numQ (Qneg r)) (denomQ (Qneg r)) = (Qpos r).
 499 intro.
 500 unfold frac.unfold denomQ.unfold numQ.
 501 unfold nat_to_Q.
 502 rewrite > factorize_defactorize.
 503 rewrite > factorize_defactorize.
 504 elim r
 505   [reflexivity
 506   |elim f
 507     [reflexivity
 508     |reflexivity
 509     |apply Qtimes1.
 510     ]
 511   ]
 512 qed.*)
 513
 514 definition Qabs:Q \to Q \def \lambda q.
 515 match q with
 516 [OQ \Rightarrow OQ
 517 |Qpos q \Rightarrow Qpos q
 518 |Qneg q \Rightarrow Qpos q
 519 ].
 520 (*CSC
 521 theorem frac_numQ_denomQ: \forall q.
 522 frac (numQ q) (denomQ q) = (Qabs q).
 523 intros.
 524 cases q
 525   [reflexivity
 526   |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ1
 527   |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2
 528   ]
 529 qed.*)
 530 (*CSC
 531 definition Qfrac: Z \to nat \to Q \def
 532 \lambda z,n.match z with
 533 [OZ \Rightarrow OQ
 534 |Zpos m \Rightarrow (frac (S m) n)
 535 |Zneg m \Rightarrow Qopp (frac (S m) n)
 536 ].
 537
 538 definition QnumZ \def \lambda q.
 539 match q with
 540 [OQ \Rightarrow OZ
 541 |Qpos r \Rightarrow Z_of_nat (numQ (Qpos r))
 542 |Qneg r \Rightarrow neg_Z_of_nat (numQ (Qpos r))
 543 ].
 544
 545 theorem Qfrac_Z_of_nat: \forall n,m.
 546 Qfrac (Z_of_nat n) m = frac n m.
 547 intros.cases n;reflexivity.
 548 qed.
 549
 550 theorem Qfrac_neg_Z_of_nat: \forall n,m.
 551 Qfrac (neg_Z_of_nat n) m = Qopp (frac n m).
 552 intros.cases n;reflexivity.
 553 qed.
 554
 555 theorem Qfrac_QnumZ_denomQ: \forall q.
 556 Qfrac (QnumZ q) (denomQ q) = q.
 557 intros.
 558 cases q
 559   [reflexivity
 560   |change with
 561     (Qfrac (Z_of_nat (numQ (Qpos r))) (denomQ (Qpos r))=Qpos r).
 562    rewrite > Qfrac_Z_of_nat.
 563    apply frac_numQ_denomQ1.
 564   |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2
 565   ]
 566 qed.
 567 *)