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 include "Q/q/qinv.ma".
  16
  17 (*
  18 let rec nat_fact_to_fraction_inv l \def
  19   match l with
  20   [nf_last a \Rightarrow nn a
  21   |nf_cons a p \Rightarrow
  22     cons (neg_Z_of_nat a) (nat_fact_to_fraction_inv p)
  23   ]
  24 .
  25
  26 definition nat_fact_all_to_Q_inv \def
  27 \lambda n.
  28   match n with
  29   [nfa_zero \Rightarrow OQ
  30   |nfa_one \Rightarrow Qpos one
  31   |nfa_proper l \Rightarrow Qpos (frac (nat_fact_to_fraction_inv l))
  32   ]
  33 .
  34
  35 definition nat_to_Q_inv \def
  36 \lambda n. nat_fact_all_to_Q_inv (factorize n).
  37
  38 definition frac:nat \to nat \to Q \def
  39 \lambda p,q. Qtimes (nat_to_Q p) (Qinv (nat_to_Q q)).
  40
  41 theorem Qtimes_frac_frac: \forall p,q,r,s.
  42 Qtimes (frac p q) (frac r s) = (frac (p*r) (q*s)).
  43 intros.
  44 unfold frac.
  45 rewrite > associative_Qtimes.
  46 rewrite < associative_Qtimes in ⊢ (? ? (? ? %) ?).
  47 rewrite > symmetric_Qtimes in ⊢ (? ? (? ? (? % ?)) ?).
  48 rewrite > associative_Qtimes in ⊢ (? ? (? ? %) ?).
  49 rewrite < associative_Qtimes.
  50 rewrite < times_Qtimes.
  51 rewrite < Qinv_Qtimes'.
  52 rewrite < times_Qtimes.
  53 reflexivity.
  54 qed.
  55 *)
  56
  57 (*
  58 definition numQ:Q \to Z \def
  59 \lambda q.
  60 match q with
  61 [OQ \Rightarrow OZ
  62 |Qpos r \Rightarrow Z_of_nat (defactorize (numeratorQ (Qpos r)))
  63 |Qneg r \Rightarrow neg_Z_of_nat (defactorize (numeratorQ (Qpos r)))
  64 ].
  65 *)
  66
  67 definition numQ:Q \to nat \def
  68 \lambda q. defactorize (numeratorQ q).
  69
  70 definition denomQ:Q \to nat \def
  71 \lambda q. defactorize (numeratorQ (Qinv q)).
  72
  73 (*CSC
  74 theorem frac_numQ_denomQ1: \forall r:ratio.
  75 frac (numQ (Qpos r)) (denomQ (Qpos r)) = (Qpos r).
  76 intro.
  77 unfold frac.unfold denomQ.unfold numQ.
  78 unfold nat_to_Q.
  79 rewrite > factorize_defactorize.
  80 rewrite > factorize_defactorize.
  81 elim r
  82   [reflexivity
  83   |elim f
  84     [reflexivity
  85     |reflexivity
  86     |apply Qtimes_numerator_denominator.
  87     ]
  88   ]
  89 qed.*)
  90
  91 (*CSC
  92 theorem frac_numQ_denomQ2: \forall r:ratio.
  93 frac (numQ (Qneg r)) (denomQ (Qneg r)) = (Qpos r).
  94 intro.
  95 unfold frac.unfold denomQ.unfold numQ.
  96 unfold nat_to_Q.
  97 rewrite > factorize_defactorize.
  98 rewrite > factorize_defactorize.
  99 elim r
 100   [reflexivity
 101   |elim f
 102     [reflexivity
 103     |reflexivity
 104     |apply Qtimes_numerator_denominator.
 105     ]
 106   ]
 107 qed.*)
 108
 109 definition Qabs:Q \to Q \def \lambda q.
 110 match q with
 111 [OQ \Rightarrow OQ
 112 |Qpos q \Rightarrow Qpos q
 113 |Qneg q \Rightarrow Qpos q
 114 ].
 115 (*CSC
 116 theorem frac_numQ_denomQ: \forall q.
 117 frac (numQ q) (denomQ q) = (Qabs q).
 118 intros.
 119 cases q
 120   [reflexivity
 121   |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ1
 122   |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2
 123   ]
 124 qed.*)
 125 (*CSC
 126 definition Qfrac: Z \to nat \to Q \def
 127 \lambda z,n.match z with
 128 [OZ \Rightarrow OQ
 129 |Zpos m \Rightarrow (frac (S m) n)
 130 |Zneg m \Rightarrow Qopp (frac (S m) n)
 131 ].
 132
 133 definition QnumZ \def \lambda q.
 134 match q with
 135 [OQ \Rightarrow OZ
 136 |Qpos r \Rightarrow Z_of_nat (numQ (Qpos r))
 137 |Qneg r \Rightarrow neg_Z_of_nat (numQ (Qpos r))
 138 ].
 139
 140 theorem Qfrac_Z_of_nat: \forall n,m.
 141 Qfrac (Z_of_nat n) m = frac n m.
 142 intros.cases n;reflexivity.
 143 qed.
 144
 145 theorem Qfrac_neg_Z_of_nat: \forall n,m.
 146 Qfrac (neg_Z_of_nat n) m = Qopp (frac n m).
 147 intros.cases n;reflexivity.
 148 qed.
 149
 150 theorem Qfrac_QnumZ_denomQ: \forall q.
 151 Qfrac (QnumZ q) (denomQ q) = q.
 152 intros.
 153 cases q
 154   [reflexivity
 155   |change with
 156     (Qfrac (Z_of_nat (numQ (Qpos r))) (denomQ (Qpos r))=Qpos r).
 157    rewrite > Qfrac_Z_of_nat.
 158    apply frac_numQ_denomQ1.
 159   |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2
 160   ]
 161 qed.
 162 *)