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 (*
  56 definition numQ:Q \to Z \def
  57 \lambda q.
  58 match q with
  59 [OQ \Rightarrow OZ
  60 |Qpos r \Rightarrow Z_of_nat (defactorize (numeratorQ (Qpos r)))
  61 |Qneg r \Rightarrow neg_Z_of_nat (defactorize (numeratorQ (Qpos r)))
  62 ].
  63 *)
  64
  65 definition numQ:Q \to nat \def
  66 \lambda q. defactorize (numeratorQ q).
  67
  68 definition denomQ:Q \to nat \def
  69 \lambda q. defactorize (numeratorQ (Qinv q)).
  70
  71 (*CSC
  72 theorem frac_numQ_denomQ1: \forall r:ratio.
  73 frac (numQ (Qpos r)) (denomQ (Qpos r)) = (Qpos r).
  74 intro.
  75 unfold frac.unfold denomQ.unfold numQ.
  76 unfold nat_to_Q.
  77 rewrite > factorize_defactorize.
  78 rewrite > factorize_defactorize.
  79 elim r
  80   [reflexivity
  81   |elim f
  82     [reflexivity
  83     |reflexivity
  84     |apply Qtimes_numerator_denominator.
  85     ]
  86   ]
  87 qed.*)
  88
  89 (*CSC
  90 theorem frac_numQ_denomQ2: \forall r:ratio.
  91 frac (numQ (Qneg r)) (denomQ (Qneg r)) = (Qpos r).
  92 intro.
  93 unfold frac.unfold denomQ.unfold numQ.
  94 unfold nat_to_Q.
  95 rewrite > factorize_defactorize.
  96 rewrite > factorize_defactorize.
  97 elim r
  98   [reflexivity
  99   |elim f
 100     [reflexivity
 101     |reflexivity
 102     |apply Qtimes_numerator_denominator.
 103     ]
 104   ]
 105 qed.*)
 106
 107 definition Qabs:Q \to Q \def \lambda q.
 108 match q with
 109 [OQ \Rightarrow OQ
 110 |Qpos q \Rightarrow Qpos q
 111 |Qneg q \Rightarrow Qpos q
 112 ].
 113 (*CSC
 114 theorem frac_numQ_denomQ: \forall q.
 115 frac (numQ q) (denomQ q) = (Qabs q).
 116 intros.
 117 cases q
 118   [reflexivity
 119   |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ1
 120   |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2
 121   ]
 122 qed.*)
 123 (*CSC
 124 definition Qfrac: Z \to nat \to Q \def
 125 \lambda z,n.match z with
 126 [OZ \Rightarrow OQ
 127 |Zpos m \Rightarrow (frac (S m) n)
 128 |Zneg m \Rightarrow Qopp (frac (S m) n)
 129 ].
 130
 131 definition QnumZ \def \lambda q.
 132 match q with
 133 [OQ \Rightarrow OZ
 134 |Qpos r \Rightarrow Z_of_nat (numQ (Qpos r))
 135 |Qneg r \Rightarrow neg_Z_of_nat (numQ (Qpos r))
 136 ].
 137
 138 theorem Qfrac_Z_of_nat: \forall n,m.
 139 Qfrac (Z_of_nat n) m = frac n m.
 140 intros.cases n;reflexivity.
 141 qed.
 142
 143 theorem Qfrac_neg_Z_of_nat: \forall n,m.
 144 Qfrac (neg_Z_of_nat n) m = Qopp (frac n m).
 145 intros.cases n;reflexivity.
 146 qed.
 147
 148 theorem Qfrac_QnumZ_denomQ: \forall q.
 149 Qfrac (QnumZ q) (denomQ q) = q.
 150 intros.
 151 cases q
 152   [reflexivity
 153   |change with
 154     (Qfrac (Z_of_nat (numQ (Qpos r))) (denomQ (Qpos r))=Qpos r).
 155    rewrite > Qfrac_Z_of_nat.
 156    apply frac_numQ_denomQ1.
 157   |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2
 158   ]
 159 qed.
 160 *)