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 definition frac:nat \to nat \to Q \def
  37 \lambda p,q. Qtimes (nat_to_Q p) (Qinv (nat_to_Q q)).
  38
  39 theorem Qtimes_frac_frac: \forall p,q,r,s.
  40 Qtimes (frac p q) (frac r s) = (frac (p*r) (q*s)).
  41 intros.
  42 unfold frac.
  43 rewrite > associative_Qtimes.
  44 rewrite < associative_Qtimes in ⊢ (? ? (? ? %) ?).
  45 rewrite > symmetric_Qtimes in ⊢ (? ? (? ? (? % ?)) ?).
  46 rewrite > associative_Qtimes in ⊢ (? ? (? ? %) ?).
  47 rewrite < associative_Qtimes.
  48 rewrite < times_Qtimes.
  49 rewrite < Qinv_Qtimes'.
  50 rewrite < times_Qtimes.
  51 reflexivity.
  52 qed.
  53 *)
  54
  55 (* la prova seguente e' tutta una ripetizione. Sistemare. *)
  56 (*CSC
  57 theorem Qtimes1: \forall f:fraction.
  58 Qtimes (nat_fact_all_to_Q (numerator f))
  59 (Qinv (nat_fact_all_to_Q (numerator (finv f))))
  60 = Qpos (frac f).
  61 simplify.
  62 intro.elim f
  63   [reflexivity
  64   |reflexivity
  65   |elim (or_numerator_nfa_one_nfa_proper f1)
  66     [elim H1.clear H1.
  67      elim H3.clear H3.
  68      cut (finv (nat_fact_to_fraction a) = f1)
  69       [elim z
  70         [simplify.
  71          rewrite > H2.rewrite > H1.simplify.
  72          rewrite > Hcut.reflexivity
  73         |simplify.
  74          rewrite > H2.rewrite > H1.simplify.
  75          rewrite > Hcut.reflexivity
  76         |simplify.
  77          rewrite > H2.rewrite > H1.simplify.
  78          rewrite > Hcut.reflexivity
  79         ]
  80       |generalize in match H.
  81        rewrite > H2.rewrite > H1.simplify.
  82        intro.destruct H3.assumption
  83       ]
  84     |elim H1.clear H1.
  85      elim z
  86       [simplify.
  87        rewrite > H2.rewrite > H2.simplify.
  88        elim (or_numerator_nfa_one_nfa_proper (finv f1))
  89         [elim H1.clear H1.
  90          rewrite > H3.simplify.
  91          cut (nat_fact_to_fraction a = f1)
  92           [rewrite > Hcut.reflexivity
  93           |generalize in match H.
  94            rewrite > H2.
  95            rewrite > H3.
  96            rewrite > Qtimes_q_Qone.
  97            intro.
  98            destruct H1.
  99            assumption
 100           ]
 101         |elim H1.clear H1.
 102          generalize in match H.
 103          rewrite > H2.
 104          rewrite > H3.simplify.
 105          intro.
 106          destruct H1.
 107          rewrite > Hcut.
 108          simplify.reflexivity
 109         ]
 110       |simplify.rewrite > H2.simplify.
 111         elim (or_numerator_nfa_one_nfa_proper (finv f1))
 112         [elim H1.clear H1.
 113          rewrite > H3.simplify.
 114          cut (nat_fact_to_fraction a = f1)
 115           [rewrite > Hcut.reflexivity
 116           |generalize in match H.
 117            rewrite > H2.
 118            rewrite > H3.
 119            rewrite > Qtimes_q_Qone.
 120            intro.
 121            destruct H1.
 122            assumption
 123           ]
 124         |elim H1.clear H1.
 125          generalize in match H.
 126          rewrite > H2.
 127          rewrite > H3.simplify.
 128          intro.
 129          destruct H1.
 130          rewrite > Hcut.
 131          simplify.reflexivity
 132         ]
 133       |simplify.rewrite > H2.simplify.
 134         elim (or_numerator_nfa_one_nfa_proper (finv f1))
 135         [elim H1.clear H1.
 136          rewrite > H3.simplify.
 137          cut (nat_fact_to_fraction a = f1)
 138           [rewrite > Hcut.reflexivity
 139           |generalize in match H.
 140            rewrite > H2.
 141            rewrite > H3.
 142            rewrite > Qtimes_q_Qone.
 143            intro.
 144            destruct H1.
 145            assumption
 146           ]
 147         |elim H1.clear H1.
 148          generalize in match H.
 149          rewrite > H2.
 150          rewrite > H3.simplify.
 151          intro.
 152          destruct H1.
 153          rewrite > Hcut.
 154          simplify.reflexivity
 155         ]
 156       ]
 157     ]
 158   ]
 159 qed.
 160 *)
 161 (*
 162 definition numQ:Q \to Z \def
 163 \lambda q.
 164 match q with
 165 [OQ \Rightarrow OZ
 166 |Qpos r \Rightarrow Z_of_nat (defactorize (numeratorQ (Qpos r)))
 167 |Qneg r \Rightarrow neg_Z_of_nat (defactorize (numeratorQ (Qpos r)))
 168 ].
 169 *)
 170
 171 definition numQ:Q \to nat \def
 172 \lambda q. defactorize (numeratorQ q).
 173
 174 definition denomQ:Q \to nat \def
 175 \lambda q. defactorize (numeratorQ (Qinv q)).
 176
 177 (*CSC
 178 theorem frac_numQ_denomQ1: \forall r:ratio.
 179 frac (numQ (Qpos r)) (denomQ (Qpos r)) = (Qpos r).
 180 intro.
 181 unfold frac.unfold denomQ.unfold numQ.
 182 unfold nat_to_Q.
 183 rewrite > factorize_defactorize.
 184 rewrite > factorize_defactorize.
 185 elim r
 186   [reflexivity
 187   |elim f
 188     [reflexivity
 189     |reflexivity
 190     |apply Qtimes1.
 191     ]
 192   ]
 193 qed.*)
 194
 195 (*CSC
 196 theorem frac_numQ_denomQ2: \forall r:ratio.
 197 frac (numQ (Qneg r)) (denomQ (Qneg r)) = (Qpos r).
 198 intro.
 199 unfold frac.unfold denomQ.unfold numQ.
 200 unfold nat_to_Q.
 201 rewrite > factorize_defactorize.
 202 rewrite > factorize_defactorize.
 203 elim r
 204   [reflexivity
 205   |elim f
 206     [reflexivity
 207     |reflexivity
 208     |apply Qtimes1.
 209     ]
 210   ]
 211 qed.*)
 212
 213 definition Qabs:Q \to Q \def \lambda q.
 214 match q with
 215 [OQ \Rightarrow OQ
 216 |Qpos q \Rightarrow Qpos q
 217 |Qneg q \Rightarrow Qpos q
 218 ].
 219 (*CSC
 220 theorem frac_numQ_denomQ: \forall q.
 221 frac (numQ q) (denomQ q) = (Qabs q).
 222 intros.
 223 cases q
 224   [reflexivity
 225   |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ1
 226   |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2
 227   ]
 228 qed.*)
 229 (*CSC
 230 definition Qfrac: Z \to nat \to Q \def
 231 \lambda z,n.match z with
 232 [OZ \Rightarrow OQ
 233 |Zpos m \Rightarrow (frac (S m) n)
 234 |Zneg m \Rightarrow Qopp (frac (S m) n)
 235 ].
 236
 237 definition QnumZ \def \lambda q.
 238 match q with
 239 [OQ \Rightarrow OZ
 240 |Qpos r \Rightarrow Z_of_nat (numQ (Qpos r))
 241 |Qneg r \Rightarrow neg_Z_of_nat (numQ (Qpos r))
 242 ].
 243
 244 theorem Qfrac_Z_of_nat: \forall n,m.
 245 Qfrac (Z_of_nat n) m = frac n m.
 246 intros.cases n;reflexivity.
 247 qed.
 248
 249 theorem Qfrac_neg_Z_of_nat: \forall n,m.
 250 Qfrac (neg_Z_of_nat n) m = Qopp (frac n m).
 251 intros.cases n;reflexivity.
 252 qed.
 253
 254 theorem Qfrac_QnumZ_denomQ: \forall q.
 255 Qfrac (QnumZ q) (denomQ q) = q.
 256 intros.
 257 cases q
 258   [reflexivity
 259   |change with
 260     (Qfrac (Z_of_nat (numQ (Qpos r))) (denomQ (Qpos r))=Qpos r).
 261    rewrite > Qfrac_Z_of_nat.
 262    apply frac_numQ_denomQ1.
 263   |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2
 264   ]
 265 qed.
 266 *)