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