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