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 set "baseuri" "cic:/matita/Q/frac".
  16
  17 include "nat/factorization.ma".
  18 include "Q/q.ma".
  19
  20
  21 definition numeratorQ \def
  22 \lambda q.match q with
  23   [OQ \Rightarrow nfa_zero
  24   |Qpos r \Rightarrow
  25     match r with
  26     [one \Rightarrow nfa_one
  27     |frac x \Rightarrow numerator x
  28     ]
  29   |Qneg r \Rightarrow
  30     match r with
  31     [one \Rightarrow nfa_one
  32     |frac x \Rightarrow numerator x
  33     ]
  34   ]
  35 .
  36
  37 definition nat_fact_all_to_Q \def
  38 \lambda n.
  39   match n with
  40   [nfa_zero \Rightarrow OQ
  41   |nfa_one \Rightarrow Qpos one
  42   |nfa_proper l \Rightarrow Qpos (frac (nat_fact_to_fraction l))
  43   ]
  44 .
  45
  46 theorem numeratorQ_nat_fact_all_to_Q: \forall g.
  47 numeratorQ (nat_fact_all_to_Q g) = g.
  48 intro.cases g
  49   [reflexivity
  50   |reflexivity
  51   |apply numerator_nat_fact_to_fraction
  52   ]
  53 qed.
  54
  55 definition nat_to_Q \def
  56 \lambda n. nat_fact_all_to_Q (factorize n).
  57
  58 let rec nat_fact_to_fraction_inv l \def
  59   match l with
  60   [nf_last a \Rightarrow nn a
  61   |nf_cons a p \Rightarrow
  62     cons (neg_Z_of_nat a) (nat_fact_to_fraction_inv p)
  63   ]
  64 .
  65
  66
  67 (*
  68 definition nat_fact_all_to_Q_inv \def
  69 \lambda n.
  70   match n with
  71   [nfa_zero \Rightarrow OQ
  72   |nfa_one \Rightarrow Qpos one
  73   |nfa_proper l \Rightarrow Qpos (frac (nat_fact_to_fraction_inv l))
  74   ]
  75 .
  76
  77 definition nat_to_Q_inv \def
  78 \lambda n. nat_fact_all_to_Q_inv (factorize n).
  79 *)
  80
  81 definition Qinv \def
  82 \lambda q.match q with
  83 [OQ \Rightarrow OQ
  84 |Qpos r \Rightarrow Qpos (rinv r)
  85 |Qneg r \Rightarrow Qneg (rinv r)
  86 ].
  87
  88 definition frac:nat \to nat \to Q \def
  89 \lambda p,q. Qtimes (nat_to_Q p) (Qinv (nat_to_Q q)).
  90
  91 theorem rtimes_oner: \forall r.rtimes r one = r.
  92 intro.cases r;reflexivity.
  93 qed.
  94
  95 theorem rtimes_onel: \forall r.rtimes one r = r.
  96 intro.cases r;reflexivity.
  97 qed.
  98
  99 definition Qone \def Qpos one.
 100
 101 theorem Qtimes_Qoner: \forall q.Qtimes q Qone = q.
 102 intro.cases q
 103   [reflexivity
 104   |cases r
 105     [reflexivity
 106     |reflexivity
 107     ]
 108   |cases r
 109     [reflexivity
 110     |reflexivity
 111     ]
 112   ]
 113 qed.
 114
 115 theorem Qtimes_Qonel: \forall q.Qtimes Qone q = q.
 116 intros.cases q
 117   [reflexivity
 118   |cases r
 119     [reflexivity
 120     |reflexivity
 121     ]
 122   |cases r
 123     [reflexivity
 124     |reflexivity
 125     ]
 126   ]
 127 qed.
 128
 129 let rec times_f h g \def
 130   match h with
 131   [nf_last a \Rightarrow
 132     match g with
 133     [nf_last b \Rightarrow nf_last (S (a+b))
 134     |nf_cons b g1 \Rightarrow nf_cons (S (a+b)) g1
 135     ]
 136   |nf_cons a h1 \Rightarrow
 137     match g with
 138     [nf_last b \Rightarrow nf_cons (S (a+b)) h1
 139     |nf_cons b g1 \Rightarrow nf_cons (a+b) (times_f h1 g1)
 140     ]
 141   ]
 142 .
 143
 144 definition times_fa \def
 145 \lambda f,g.
 146 match f with
 147 [nfa_zero \Rightarrow nfa_zero
 148 |nfa_one \Rightarrow g
 149 |nfa_proper f1 \Rightarrow match g with
 150   [nfa_zero \Rightarrow nfa_zero
 151   |nfa_one \Rightarrow nfa_proper f1
 152   |nfa_proper g1 \Rightarrow nfa_proper (times_f f1 g1)
 153   ]
 154 ]
 155 .
 156
 157 theorem eq_times_f_times1:\forall g,h,m. defactorize_aux (times_f g h) m
 158 =defactorize_aux g m*defactorize_aux h m.
 159 intro.elim g
 160   [elim h;simplify;autobatch
 161   |elim h
 162     [simplify;autobatch
 163     |simplify.rewrite > (H n3 (S m)).autobatch
 164     ]
 165   ]
 166 qed.
 167
 168 theorem eq_times_fa_times: \forall f,g.
 169 defactorize (times_fa f g) = defactorize f*defactorize g.
 170 intros.
 171 elim f
 172   [reflexivity
 173   |simplify.apply plus_n_O
 174   |elim g;simplify
 175     [apply times_n_O
 176     |apply times_n_SO
 177     |apply eq_times_f_times1
 178     ]
 179   ]
 180 qed.
 181
 182 theorem eq_times_times_fa: \forall n,m.
 183 factorize (n*m) = times_fa (factorize n) (factorize m).
 184 intros.
 185 rewrite <(factorize_defactorize (times_fa (factorize n) (factorize m))).
 186 rewrite > eq_times_fa_times.
 187 rewrite > defactorize_factorize.
 188 rewrite > defactorize_factorize.
 189 reflexivity.
 190 qed.
 191
 192
 193 theorem eq_plus_Zplus: \forall n,m:nat. Z_of_nat (n+m) =
 194 Z_of_nat n + Z_of_nat m.
 195 intro.cases n;intro
 196   [reflexivity
 197   |cases m
 198     [simplify.rewrite < plus_n_O.reflexivity
 199     |simplify.reflexivity.
 200     ]
 201   ]
 202 qed.
 203
 204 definition unfrac \def \lambda f.
 205 match f with
 206   [one \Rightarrow pp O
 207   |frac f \Rightarrow f
 208   ]
 209 .
 210
 211 lemma injective_frac: injective fraction ratio frac.
 212 unfold.intros.
 213 change with ((unfrac (frac x)) = (unfrac (frac y))).
 214 rewrite < H.reflexivity.
 215 qed.
 216
 217 theorem times_f_ftimes: \forall n,m.
 218 frac (nat_fact_to_fraction (times_f n m))
 219 = ftimes (nat_fact_to_fraction n) (nat_fact_to_fraction m).
 220 intro.
 221 elim n
 222   [elim m
 223     [simplify.
 224      rewrite < plus_n_Sm.reflexivity
 225     |elim n2
 226       [simplify.rewrite < plus_n_O.reflexivity
 227       |simplify.reflexivity.
 228       ]
 229     ]
 230   |elim m
 231     [elim n1
 232       [simplify.reflexivity
 233       |simplify.rewrite < plus_n_Sm.reflexivity
 234       ]
 235     |simplify.
 236      cut (\exist h.ftimes (nat_fact_to_fraction n2) (nat_fact_to_fraction n4) = frac h)
 237       [elim Hcut.
 238        rewrite > H2.
 239        simplify.apply eq_f.
 240        apply eq_f2
 241         [apply eq_plus_Zplus
 242         |apply injective_frac.
 243          rewrite < H2.
 244          apply H
 245         ]
 246       |generalize in match n4.
 247        elim n2
 248         [cases n6;simplify;autobatch
 249         |cases n7;simplify
 250           [autobatch
 251           |elim (H2 n9).
 252            rewrite > H3.
 253            simplify.
 254            autobatch
 255           ]
 256         ]
 257       ]
 258     ]
 259   ]
 260 qed.
 261
 262 theorem times_fa_Qtimes: \forall f,g. nat_fact_all_to_Q (times_fa f g) =
 263 Qtimes (nat_fact_all_to_Q f) (nat_fact_all_to_Q g).
 264 intros.
 265 cases f;simplify
 266   [reflexivity
 267   |cases g;reflexivity
 268   |cases g;simplify
 269     [reflexivity
 270     |reflexivity
 271     |rewrite > times_f_ftimes.reflexivity
 272     ]
 273   ]
 274 qed.
 275
 276 theorem times_Qtimes: \forall p,q.
 277 (nat_to_Q (p*q)) = Qtimes (nat_to_Q p) (nat_to_Q q).
 278 intros.unfold nat_to_Q.
 279 rewrite < times_fa_Qtimes.
 280 rewrite < eq_times_times_fa.
 281 reflexivity.
 282 qed.
 283
 284 theorem rtimes_Zplus: \forall x,y.
 285 rtimes (Z_to_ratio x) (Z_to_ratio y) =
 286 Z_to_ratio (x + y).
 287 intro.
 288 elim x
 289   [reflexivity
 290   |elim y;reflexivity
 291   |elim y;reflexivity
 292   ]
 293 qed.
 294
 295 theorem rtimes_Zplus1: \forall x,y,f.
 296 rtimes (Z_to_ratio x) (frac (cons y f)) =
 297 frac (cons ((x + y)) f).
 298 intro.
 299 elim x
 300   [reflexivity
 301   |elim y;reflexivity
 302   |elim y;reflexivity
 303   ]
 304 qed.
 305
 306 theorem rtimes_Zplus2: \forall x,y,f.
 307 rtimes (frac (cons y f)) (Z_to_ratio x) =
 308 frac (cons ((y + x)) f).
 309 intros.
 310 elim x
 311   [elim y;reflexivity
 312   |elim y;reflexivity
 313   |elim y;reflexivity
 314   ]
 315 qed.
 316
 317 theorem or_one_frac: \forall f,g.
 318 rtimes (frac f) (frac g) = one \lor
 319 \exists h.rtimes (frac f) (frac g) = frac h.
 320 intros.
 321 elim (rtimes (frac f) (frac g))
 322   [left.reflexivity
 323   |right.apply (ex_intro ? ? f1).reflexivity
 324   ]
 325 qed.
 326
 327 theorem one_to_rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction.
 328 rtimes (frac f) (frac g) = one \to
 329 rtimes (frac (cons x f)) (frac (cons y g)) = Z_to_ratio (x + y).
 330 intros.simplify.simplify in H.rewrite > H.simplify.
 331 reflexivity.
 332 qed.
 333
 334 theorem frac_to_rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction.
 335 \forall h.rtimes (frac f) (frac g) = frac h \to
 336 rtimes (frac (cons x f)) (frac (cons y g)) = frac (cons (x + y) h).
 337 intros.simplify.simplify in H.rewrite > H.simplify.
 338 reflexivity.
 339 qed.
 340
 341 theorem rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction.
 342 (rtimes (frac f) (frac g) = one \land
 343  rtimes (frac (cons x f)) (frac (cons y g)) = Z_to_ratio (x + y))
 344 \lor (\exists h.rtimes (frac f) (frac g) = frac h \land
 345 rtimes (frac (cons x f)) (frac (cons y g)) =
 346 frac (cons (x + y) h)).
 347 intros.
 348 simplify.
 349 elim (rtimes (frac f) (frac g));simplify
 350   [left.split;reflexivity
 351   |right.
 352    apply (ex_intro ? ? f1).
 353    split;reflexivity
 354   ]
 355 qed.
 356
 357 theorem Z_to_ratio_frac_frac: \forall z,f1,f2.
 358 rtimes (rtimes (Z_to_ratio z) (frac f1)) (frac f2)
 359 =rtimes (Z_to_ratio z) (rtimes (frac f1) (frac f2)).
 360 intros 2.elim f1
 361   [elim f2
 362     [ change with
 363      (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (pos n))) (Z_to_ratio (pos n1))
 364       =rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (pos n)) (Z_to_ratio (pos n1)))).
 365      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
 366      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
 367      rewrite > assoc_Zplus.reflexivity
 368     |change with
 369      (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (pos n))) (Z_to_ratio (neg n1))
 370       =rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (pos n)) (Z_to_ratio (neg n1)))).
 371      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
 372      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
 373      rewrite > assoc_Zplus.reflexivity
 374     |change with
 375       (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (pos n))) (frac (cons z1 f))
 376        = rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (pos n)) (frac (cons z1 f)))).
 377      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus1.
 378      rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus1.
 379      rewrite > assoc_Zplus.reflexivity
 380     ]
 381   |elim f2
 382     [change with
 383      (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (neg n))) (Z_to_ratio (pos n1))
 384       =rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (neg n)) (Z_to_ratio (pos n1)))).
 385      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
 386      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
 387      rewrite > assoc_Zplus.reflexivity
 388     |change with
 389      (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (neg n))) (Z_to_ratio (neg n1))
 390       =rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (neg n)) (Z_to_ratio (neg n1)))).
 391      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
 392      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
 393      rewrite > assoc_Zplus.reflexivity
 394     |change with
 395       (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (neg n))) (frac (cons z1 f))
 396        = rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (neg n)) (frac (cons z1 f)))).
 397      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus1.
 398      rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus1.
 399      rewrite > assoc_Zplus.reflexivity
 400     ]
 401   |elim f2
 402     [change with
 403      (rtimes (rtimes (Z_to_ratio z) (frac (cons z1 f))) (Z_to_ratio (pos n))
 404       =rtimes (Z_to_ratio z) (rtimes (frac (cons z1 f)) (Z_to_ratio (pos n)))).
 405      rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus2.
 406      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
 407      rewrite > assoc_Zplus.reflexivity
 408     |change with
 409      (rtimes (rtimes (Z_to_ratio z) (frac (cons z1 f))) (Z_to_ratio (neg n))
 410       =rtimes (Z_to_ratio z) (rtimes (frac (cons z1 f)) (Z_to_ratio (neg n)))).
 411      rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus2.
 412      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
 413      rewrite > assoc_Zplus.reflexivity
 414     |elim (or_one_frac f f3)
 415       [rewrite > rtimes_Zplus1.
 416        rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
 417        rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
 418        rewrite > rtimes_Zplus.
 419        rewrite > assoc_Zplus.reflexivity
 420       |elim H2.clear H2.
 421        rewrite > rtimes_Zplus1.
 422        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H3).
 423        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H3).
 424        rewrite > rtimes_Zplus1.
 425        rewrite > assoc_Zplus.reflexivity
 426       ]
 427     ]
 428   ]
 429 qed.
 430
 431 theorem cons_frac_frac: \forall f1,z,f,f2.
 432 rtimes (rtimes (frac (cons z f)) (frac f1)) (frac f2)
 433 =rtimes (frac (cons z f)) (rtimes (frac f1) (frac f2)).
 434 intro.elim f1
 435   [elim f2
 436     [change with
 437      (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (pos n))) (Z_to_ratio (pos n1))
 438       =rtimes (frac (cons z f)) (rtimes (Z_to_ratio (pos n)) (Z_to_ratio (pos n1)))).
 439      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
 440      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
 441      rewrite > assoc_Zplus.reflexivity
 442     |change with
 443      (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (pos n))) (Z_to_ratio (neg n1))
 444       =rtimes (frac (cons z f)) (rtimes (Z_to_ratio (pos n)) (Z_to_ratio (neg n1)))).
 445      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
 446      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
 447      rewrite > assoc_Zplus.reflexivity
 448     |change with
 449       (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (pos n))) (frac (cons z1 f3))
 450        = rtimes (frac (cons z f)) (rtimes (Z_to_ratio (pos n)) (frac (cons z1 f3)))).
 451      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
 452      elim (or_one_frac f f3)
 453       [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
 454        rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
 455        rewrite > assoc_Zplus.reflexivity
 456       |elim H1.clear H1.
 457        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
 458        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
 459        rewrite > assoc_Zplus.reflexivity
 460       ]
 461     ]
 462   |elim f2
 463     [change with
 464      (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (neg n))) (Z_to_ratio (pos n1))
 465       =rtimes (frac (cons z f)) (rtimes (Z_to_ratio (neg n)) (Z_to_ratio (pos n1)))).
 466      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
 467      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
 468      rewrite > assoc_Zplus.reflexivity
 469     |change with
 470      (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (neg n))) (Z_to_ratio (neg n1))
 471       =rtimes (frac (cons z f)) (rtimes (Z_to_ratio (neg n)) (Z_to_ratio (neg n1)))).
 472      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
 473      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
 474      rewrite > assoc_Zplus.reflexivity
 475     |change with
 476       (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (neg n))) (frac (cons z1 f3))
 477        = rtimes (frac (cons z f)) (rtimes (Z_to_ratio (neg n)) (frac (cons z1 f3)))).
 478      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
 479      elim (or_one_frac f f3)
 480       [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
 481        rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
 482        rewrite > assoc_Zplus.reflexivity
 483       |elim H1.clear H1.
 484        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
 485        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
 486        rewrite > assoc_Zplus.reflexivity
 487       ]
 488     ]
 489   |elim f3
 490     [change with
 491      (rtimes (rtimes (frac (cons z1 f2)) (frac (cons z f))) (Z_to_ratio (pos n))
 492       =rtimes (frac (cons z1 f2)) (rtimes (frac (cons z f)) (Z_to_ratio (pos n)))).
 493      rewrite > rtimes_Zplus2.
 494      elim (or_one_frac f2 f)
 495       [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
 496        rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
 497        rewrite > rtimes_Zplus.
 498        rewrite > assoc_Zplus.reflexivity
 499       |elim H1.clear H1.
 500        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
 501        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
 502        rewrite > rtimes_Zplus2.
 503        rewrite > assoc_Zplus.reflexivity
 504       ]
 505     |change with
 506      (rtimes (rtimes (frac (cons z1 f2)) (frac (cons z f))) (Z_to_ratio (neg n))
 507       =rtimes (frac (cons z1 f2)) (rtimes (frac (cons z f)) (Z_to_ratio (neg n)))).
 508      rewrite > rtimes_Zplus2.
 509      elim (or_one_frac f2 f)
 510       [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
 511        rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
 512        rewrite > rtimes_Zplus.
 513        rewrite > assoc_Zplus.reflexivity
 514       |elim H1.clear H1.
 515        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
 516        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
 517        rewrite > rtimes_Zplus2.
 518        rewrite > assoc_Zplus.reflexivity
 519       ]
 520     |elim (or_one_frac f2 f)
 521       [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
 522        rewrite > rtimes_Zplus1.
 523        elim (or_one_frac f f4)
 524         [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H3).
 525          rewrite > rtimes_Zplus2.
 526          cut (f4 = f2)
 527           [rewrite > Hcut.
 528            rewrite > assoc_Zplus.reflexivity
 529           |apply injective_frac.
 530            rewrite < rtimes_onel.
 531            rewrite < H2.
 532            (* problema inaspettato: mi serve l'unicita' dell'inversa,
 533               che richiede (?) l'associativita. Per fortuna basta
 534               l'ipotesi induttiva. *)
 535            cases f2
 536             [change with
 537              (rtimes (rtimes (Z_to_ratio (pos n)) (frac f)) (frac f4)=Z_to_ratio (pos n)).
 538              rewrite > Z_to_ratio_frac_frac.
 539              rewrite > H3.
 540              rewrite > rtimes_oner.
 541              reflexivity
 542             |change with
 543              (rtimes (rtimes (Z_to_ratio (neg n)) (frac f)) (frac f4)=Z_to_ratio (neg n)).
 544              rewrite > Z_to_ratio_frac_frac.
 545              rewrite > H3.
 546              rewrite > rtimes_oner.
 547              reflexivity
 548             |rewrite > H.
 549              rewrite > H3.
 550              rewrite > rtimes_oner.
 551              reflexivity
 552             ]
 553           ]
 554         |elim H3.clear H3.
 555          rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H4).
 556          cut (rtimes (frac f2) (frac a) = frac f4)
 557           [rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? f4 Hcut).
 558            rewrite > assoc_Zplus.reflexivity
 559           |rewrite < H4.
 560            generalize in match H2.
 561            cases f2;intro
 562             [change with
 563              (rtimes (Z_to_ratio (pos n)) (rtimes (frac f)(frac f4)) =frac f4).
 564              rewrite < Z_to_ratio_frac_frac.
 565              rewrite > H3.
 566              rewrite > rtimes_onel.
 567              reflexivity
 568             |change with
 569              (rtimes (Z_to_ratio (neg n)) (rtimes (frac f)(frac f4)) =frac f4).
 570              rewrite < Z_to_ratio_frac_frac.
 571              rewrite > H3.
 572              rewrite > rtimes_onel.
 573              reflexivity
 574             |rewrite < H.
 575              rewrite > H3.
 576              rewrite > rtimes_onel.
 577              reflexivity
 578             ]
 579           ]
 580         ]
 581       |elim H2.clear H2.
 582        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H3).
 583        elim (or_one_frac f f4)
 584         [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
 585          rewrite > rtimes_Zplus2.
 586          cut (rtimes (frac a) (frac f4) = frac f2)
 587           [rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? f2 Hcut).
 588            rewrite > assoc_Zplus.reflexivity
 589           |rewrite < H3.
 590            generalize in match H2.
 591            cases f2;intro
 592             [change with
 593              (rtimes (rtimes (Z_to_ratio (pos n)) (frac f)) (frac f4)=Z_to_ratio (pos n)).
 594              rewrite > Z_to_ratio_frac_frac.
 595              rewrite > H4.
 596              rewrite > rtimes_oner.
 597              reflexivity
 598             |change with
 599              (rtimes (rtimes (Z_to_ratio (neg n)) (frac f)) (frac f4)=Z_to_ratio (neg n)).
 600              rewrite > Z_to_ratio_frac_frac.
 601              rewrite > H4.
 602              rewrite > rtimes_oner.
 603              reflexivity
 604             |rewrite > H.
 605              rewrite > H4.
 606              rewrite > rtimes_oner.
 607              reflexivity
 608             ]
 609           ]
 610         |elim H2.clear H2.
 611          rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a1 H4).
 612          elim (or_one_frac a f4)
 613           [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
 614            cut (rtimes (frac f2) (frac a1) = one)
 615             [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? Hcut).
 616              rewrite > assoc_Zplus.reflexivity
 617             |rewrite < H4.
 618              generalize in match H3.
 619              cases f2;intro
 620               [change with
 621                (rtimes (Z_to_ratio (pos n)) (rtimes (frac f)(frac f4)) = one).
 622                rewrite < Z_to_ratio_frac_frac.
 623                rewrite > H5.
 624                assumption
 625               |change with
 626                (rtimes (Z_to_ratio (neg n)) (rtimes (frac f)(frac f4)) = one).
 627                rewrite < Z_to_ratio_frac_frac.
 628                rewrite > H5.
 629                assumption
 630               |rewrite < H.
 631                rewrite > H5.
 632                assumption
 633               ]
 634             ]
 635           |elim H2.clear H2.
 636            rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a2 H5).
 637            cut (rtimes (frac f2) (frac a1) = frac a2)
 638             [rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a2 Hcut).
 639              rewrite > assoc_Zplus.reflexivity
 640             |rewrite < H4.
 641              generalize in match H3.
 642              cases f2;intro
 643               [change with
 644                (rtimes (Z_to_ratio (pos n)) (rtimes (frac f)(frac f4)) = frac a2).
 645                rewrite < Z_to_ratio_frac_frac.
 646                rewrite > H2.
 647                assumption
 648               |change with
 649                (rtimes (Z_to_ratio (neg n)) (rtimes (frac f)(frac f4)) = frac a2).
 650                rewrite < Z_to_ratio_frac_frac.
 651                rewrite > H2.
 652                assumption
 653               |rewrite < H.
 654                rewrite > H2.
 655                assumption
 656               ]
 657             ]
 658           ]
 659         ]
 660       ]
 661     ]
 662   ]
 663 qed.
 664
 665 theorem frac_frac_fracaux: \forall f,f1,f2.
 666 rtimes (rtimes (frac f) (frac f1)) (frac f2)
 667 =rtimes (frac f) (rtimes (frac f1) (frac f2)).
 668 intros.
 669 cases f
 670   [change with
 671    (rtimes (rtimes (Z_to_ratio (pos n)) (frac f1)) (frac f2)
 672     =rtimes (Z_to_ratio (pos n)) (rtimes (frac f1) (frac f2))).
 673    apply Z_to_ratio_frac_frac
 674   |change with
 675    (rtimes (rtimes (Z_to_ratio (neg n)) (frac f1)) (frac f2)
 676     =rtimes (Z_to_ratio (neg n)) (rtimes (frac f1) (frac f2))).
 677    apply Z_to_ratio_frac_frac
 678   |apply cons_frac_frac
 679   ]
 680 qed.
 681
 682 theorem associative_rtimes:associative ? rtimes.
 683 unfold.intros.
 684 cases x
 685   [reflexivity
 686   |cases y
 687     [reflexivity.
 688     |cases z
 689       [rewrite > rtimes_oner.rewrite > rtimes_oner.reflexivity
 690       |apply frac_frac_fracaux
 691       ]
 692     ]
 693   ]
 694 qed.
 695
 696 theorem associative_Qtimes:associative ? Qtimes.
 697 unfold.intros.
 698 cases x
 699   [reflexivity
 700    (* non posso scrivere 2,3: ... ?? *)
 701   |cases y
 702     [reflexivity.
 703     |cases z
 704       [reflexivity
 705       |simplify.rewrite > associative_rtimes.
 706        reflexivity.
 707       |simplify.rewrite > associative_rtimes.
 708        reflexivity
 709       ]
 710     |cases z
 711       [reflexivity
 712       |simplify.rewrite > associative_rtimes.
 713        reflexivity.
 714       |simplify.rewrite > associative_rtimes.
 715        reflexivity
 716       ]
 717     ]
 718   |cases y
 719     [reflexivity.
 720     |cases z
 721       [reflexivity
 722       |simplify.rewrite > associative_rtimes.
 723        reflexivity.
 724       |simplify.rewrite > associative_rtimes.
 725        reflexivity
 726       ]
 727     |cases z
 728       [reflexivity
 729       |simplify.rewrite > associative_rtimes.
 730        reflexivity.
 731       |simplify.rewrite > associative_rtimes.
 732        reflexivity
 733       ]
 734     ]
 735   ]
 736 qed.
 737
 738 theorem Qtimes_OQ: \forall q.Qtimes q OQ = OQ.
 739 intro.cases q;reflexivity.
 740 qed.
 741
 742 theorem symmetric_Qtimes: symmetric ? Qtimes.
 743 unfold.intros.
 744 cases x
 745   [simplify in ⊢ (? ? % ?).rewrite > Qtimes_OQ.reflexivity
 746   |elim y
 747     [reflexivity
 748     |simplify.alias id "symmetric_rtimes" = "cic:/matita/Q/times/symmetric_rtimes.con".
 749 rewrite > symmetric_rtimes.reflexivity
 750     |simplify.rewrite > symmetric_rtimes.reflexivity
 751     ]
 752   |elim y
 753     [reflexivity
 754     |simplify.rewrite > symmetric_rtimes.reflexivity
 755     |simplify.rewrite > symmetric_rtimes.reflexivity
 756     ]
 757   ]
 758 qed.
 759
 760 theorem Qtimes_Qinv: \forall q. q \neq OQ \to Qtimes q (Qinv q) = Qone.
 761 intro.
 762 cases q;intro
 763   [elim H.reflexivity
 764   |simplify.alias id "rtimes_rinv" = "cic:/matita/Q/times/rtimes_rinv.con".
 765 rewrite > rtimes_rinv.reflexivity
 766   |simplify.rewrite > rtimes_rinv.reflexivity
 767   ]
 768 qed.
 769
 770 theorem eq_Qtimes_OQ_to_eq_OQ: \forall p,q.
 771 Qtimes p q = OQ \to p = OQ \lor q = OQ.
 772 intros 2.
 773 cases p
 774   [intro.left.reflexivity
 775   |cases q
 776     [intro.right.reflexivity
 777     |simplify.intro.destruct H
 778     |simplify.intro.destruct H
 779     ]
 780   |cases q
 781     [intro.right.reflexivity
 782     |simplify.intro.destruct H
 783     |simplify.intro.destruct H
 784     ]
 785   ]
 786 qed.
 787
 788 theorem Qinv_Qtimes: \forall p,q.
 789 p \neq OQ \to q \neq OQ \to
 790 Qinv(Qtimes p q) =
 791 Qtimes (Qinv p) (Qinv q).
 792 intros.
 793 rewrite < Qtimes_Qonel in ⊢ (? ? ? %).
 794 rewrite < (Qtimes_Qinv (Qtimes p q))
 795   [lapply (Qtimes_Qinv ? H).
 796    lapply (Qtimes_Qinv ? H1).
 797    rewrite > symmetric_Qtimes in ⊢ (? ? ? (? % ?)).
 798    rewrite > associative_Qtimes.
 799    rewrite > associative_Qtimes.
 800    rewrite < associative_Qtimes in ⊢ (? ? ? (? ? (? ? %))).
 801    rewrite < symmetric_Qtimes in ⊢ (? ? ? (? ? (? ? (? % ?)))).
 802    rewrite > associative_Qtimes in ⊢ (? ? ? (? ? (? ? %))).
 803    rewrite > Hletin1.
 804    rewrite > Qtimes_Qoner.
 805    rewrite > Hletin.
 806    rewrite > Qtimes_Qoner.
 807    reflexivity
 808   |intro.
 809    elim (eq_Qtimes_OQ_to_eq_OQ ? ? H2)
 810     [apply (H H3)|apply (H1 H3)]
 811   ]
 812 qed.
 813
 814 (* a stronger version, taking advantage of inv(O) = O *)
 815 theorem Qinv_Qtimes': \forall p,q.
 816 Qinv(Qtimes p q) =
 817 Qtimes (Qinv p) (Qinv q).
 818 intros.
 819 cases p
 820   [reflexivity
 821   |cases q
 822     [reflexivity
 823     |apply Qinv_Qtimes;intro;destruct H
 824     |apply Qinv_Qtimes;intro;destruct H
 825     ]
 826   |cases q
 827     [reflexivity
 828     |apply Qinv_Qtimes;intro;destruct H
 829     |apply Qinv_Qtimes;intro;destruct H
 830     ]
 831   ]
 832 qed.
 833
 834 theorem Qtimes_frac_frac: \forall p,q,r,s.
 835 Qtimes (frac p q) (frac r s) = (frac (p*r) (q*s)).
 836 intros.
 837 unfold frac.
 838 rewrite > associative_Qtimes.
 839 rewrite < associative_Qtimes in ⊢ (? ? (? ? %) ?).
 840 rewrite > symmetric_Qtimes in ⊢ (? ? (? ? (? % ?)) ?).
 841 rewrite > associative_Qtimes in ⊢ (? ? (? ? %) ?).
 842 rewrite < associative_Qtimes.
 843 rewrite < times_Qtimes.
 844 rewrite < Qinv_Qtimes'.
 845 rewrite < times_Qtimes.
 846 reflexivity.
 847 qed.
 848
 849
 850 (* la prova seguente e' tutta una ripetizione. Sistemare. *)
 851 (*CSC
 852 theorem Qtimes1: \forall f:fraction.
 853 Qtimes (nat_fact_all_to_Q (numerator f))
 854 (Qinv (nat_fact_all_to_Q (numerator (finv f))))
 855 = Qpos (frac f).
 856 simplify.
 857 intro.elim f
 858   [reflexivity
 859   |reflexivity
 860   |elim (or_numerator_nfa_one_nfa_proper f1)
 861     [elim H1.clear H1.
 862      elim H3.clear H3.
 863      cut (finv (nat_fact_to_fraction a) = f1)
 864       [elim z
 865         [simplify.
 866          rewrite > H2.rewrite > H1.simplify.
 867          rewrite > Hcut.reflexivity
 868         |simplify.
 869          rewrite > H2.rewrite > H1.simplify.
 870          rewrite > Hcut.reflexivity
 871         |simplify.
 872          rewrite > H2.rewrite > H1.simplify.
 873          rewrite > Hcut.reflexivity
 874         ]
 875       |generalize in match H.
 876        rewrite > H2.rewrite > H1.simplify.
 877        intro.destruct H3.assumption
 878       ]
 879     |elim H1.clear H1.
 880      elim z
 881       [simplify.
 882        rewrite > H2.rewrite > H2.simplify.
 883        elim (or_numerator_nfa_one_nfa_proper (finv f1))
 884         [elim H1.clear H1.
 885          rewrite > H3.simplify.
 886          cut (nat_fact_to_fraction a = f1)
 887           [rewrite > Hcut.reflexivity
 888           |generalize in match H.
 889            rewrite > H2.
 890            rewrite > H3.
 891            rewrite > Qtimes_Qoner.
 892            intro.
 893            destruct H1.
 894            assumption
 895           ]
 896         |elim H1.clear H1.
 897          generalize in match H.
 898          rewrite > H2.
 899          rewrite > H3.simplify.
 900          intro.
 901          destruct H1.
 902          rewrite > Hcut.
 903          simplify.reflexivity
 904         ]
 905       |simplify.rewrite > H2.simplify.
 906         elim (or_numerator_nfa_one_nfa_proper (finv f1))
 907         [elim H1.clear H1.
 908          rewrite > H3.simplify.
 909          cut (nat_fact_to_fraction a = f1)
 910           [rewrite > Hcut.reflexivity
 911           |generalize in match H.
 912            rewrite > H2.
 913            rewrite > H3.
 914            rewrite > Qtimes_Qoner.
 915            intro.
 916            destruct H1.
 917            assumption
 918           ]
 919         |elim H1.clear H1.
 920          generalize in match H.
 921          rewrite > H2.
 922          rewrite > H3.simplify.
 923          intro.
 924          destruct H1.
 925          rewrite > Hcut.
 926          simplify.reflexivity
 927         ]
 928       |simplify.rewrite > H2.simplify.
 929         elim (or_numerator_nfa_one_nfa_proper (finv f1))
 930         [elim H1.clear H1.
 931          rewrite > H3.simplify.
 932          cut (nat_fact_to_fraction a = f1)
 933           [rewrite > Hcut.reflexivity
 934           |generalize in match H.
 935            rewrite > H2.
 936            rewrite > H3.
 937            rewrite > Qtimes_Qoner.
 938            intro.
 939            destruct H1.
 940            assumption
 941           ]
 942         |elim H1.clear H1.
 943          generalize in match H.
 944          rewrite > H2.
 945          rewrite > H3.simplify.
 946          intro.
 947          destruct H1.
 948          rewrite > Hcut.
 949          simplify.reflexivity
 950         ]
 951       ]
 952     ]
 953   ]
 954 qed.
 955 *)
 956 (*
 957 definition numQ:Q \to Z \def
 958 \lambda q.
 959 match q with
 960 [OQ \Rightarrow OZ
 961 |Qpos r \Rightarrow Z_of_nat (defactorize (numeratorQ (Qpos r)))
 962 |Qneg r \Rightarrow neg_Z_of_nat (defactorize (numeratorQ (Qpos r)))
 963 ].
 964 *)
 965
 966 definition numQ:Q \to nat \def
 967 \lambda q. defactorize (numeratorQ q).
 968
 969 definition denomQ:Q \to nat \def
 970 \lambda q. defactorize (numeratorQ (Qinv q)).
 971
 972 definition Qopp:Q \to Q \def \lambda q.
 973 match q with
 974 [OQ \Rightarrow OQ
 975 |Qpos q \Rightarrow Qneg q
 976 |Qneg q \Rightarrow Qpos q
 977 ].
 978 (*CSC
 979 theorem frac_numQ_denomQ1: \forall r:ratio.
 980 frac (numQ (Qpos r)) (denomQ (Qpos r)) = (Qpos r).
 981 intro.
 982 unfold frac.unfold denomQ.unfold numQ.
 983 unfold nat_to_Q.
 984 rewrite > factorize_defactorize.
 985 rewrite > factorize_defactorize.
 986 elim r
 987   [reflexivity
 988   |elim f
 989     [reflexivity
 990     |reflexivity
 991     |apply Qtimes1.
 992     ]
 993   ]
 994 qed.*)
 995
 996 (*CSC
 997 theorem frac_numQ_denomQ2: \forall r:ratio.
 998 frac (numQ (Qneg r)) (denomQ (Qneg r)) = (Qpos r).
 999 intro.
1000 unfold frac.unfold denomQ.unfold numQ.
1001 unfold nat_to_Q.
1002 rewrite > factorize_defactorize.
1003 rewrite > factorize_defactorize.
1004 elim r
1005   [reflexivity
1006   |elim f
1007     [reflexivity
1008     |reflexivity
1009     |apply Qtimes1.
1010     ]
1011   ]
1012 qed.*)
1013
1014 definition Qabs:Q \to Q \def \lambda q.
1015 match q with
1016 [OQ \Rightarrow OQ
1017 |Qpos q \Rightarrow Qpos q
1018 |Qneg q \Rightarrow Qpos q
1019 ].
1020 (*CSC
1021 theorem frac_numQ_denomQ: \forall q.
1022 frac (numQ q) (denomQ q) = (Qabs q).
1023 intros.
1024 cases q
1025   [reflexivity
1026   |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ1
1027   |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2
1028   ]
1029 qed.*)
1030 (*CSC
1031 definition Qfrac: Z \to nat \to Q \def
1032 \lambda z,n.match z with
1033 [OZ \Rightarrow OQ
1034 |Zpos m \Rightarrow (frac (S m) n)
1035 |Zneg m \Rightarrow Qopp (frac (S m) n)
1036 ].
1037
1038 definition QnumZ \def \lambda q.
1039 match q with
1040 [OQ \Rightarrow OZ
1041 |Qpos r \Rightarrow Z_of_nat (numQ (Qpos r))
1042 |Qneg r \Rightarrow neg_Z_of_nat (numQ (Qpos r))
1043 ].
1044
1045 theorem Qfrac_Z_of_nat: \forall n,m.
1046 Qfrac (Z_of_nat n) m = frac n m.
1047 intros.cases n;reflexivity.
1048 qed.
1049
1050 theorem Qfrac_neg_Z_of_nat: \forall n,m.
1051 Qfrac (neg_Z_of_nat n) m = Qopp (frac n m).
1052 intros.cases n;reflexivity.
1053 qed.
1054
1055 theorem Qfrac_QnumZ_denomQ: \forall q.
1056 Qfrac (QnumZ q) (denomQ q) = q.
1057 intros.
1058 cases q
1059   [reflexivity
1060   |change with
1061     (Qfrac (Z_of_nat (numQ (Qpos r))) (denomQ (Qpos r))=Qpos r).
1062    rewrite > Qfrac_Z_of_nat.
1063    apply frac_numQ_denomQ1.
1064   |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2
1065   ]
1066 qed.
1067 *)