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