helm/software/matita/library/Q/q.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 "Z/compare.ma".
  16 include "Z/plus.ma".
  17 include "nat/factorization.ma".
  18
  19 (* a fraction is a list of Z-coefficients for primes, in natural
  20 order. The last coefficient must eventually be different from 0 *)
  21
  22 inductive fraction : Set \def
  23   pp : nat \to fraction
  24 | nn: nat \to fraction
  25 | cons : Z \to fraction \to fraction.
  26
  27 let rec fraction_of_nat_fact n ≝
  28  match n with
  29   [ nf_last m ⇒ pp m
  30   | nf_cons m l ⇒ cons (Z_of_nat (S m)) (fraction_of_nat_fact l)
  31   ].
  32
  33 (* a fraction is integral if every coefficient is not negative *)
  34 let rec nat_fact_of_integral_fraction n ≝
  35  match n with
  36   [ pp n ⇒ nf_last n
  37   | nn _ ⇒ nf_last O (* dummy value *)
  38   | cons z l ⇒
  39      match z with
  40       [ OZ ⇒ nf_cons O (nat_fact_of_integral_fraction l)
  41       | pos n ⇒ nf_cons n (nat_fact_of_integral_fraction l)
  42       | neg n ⇒ nf_last O (* dummy value *)
  43       ]
  44   ].
  45
  46 theorem nat_fact_of_integral_fraction_fraction_of_nat_fact:
  47  ∀n. nat_fact_of_integral_fraction (fraction_of_nat_fact n) = n.
  48  intro;
  49  elim n;
  50   [ reflexivity;
  51   | simplify;
  52     rewrite > H;
  53     reflexivity
  54   ]
  55 qed.
  56
  57 inductive ratio : Set \def
  58       one :  ratio
  59     | frac : fraction \to ratio.
  60
  61 (* a rational number is either O or a ratio with a sign *)
  62 inductive Q : Set \def
  63     OQ : Q
  64   | Qpos : ratio  \to Q
  65   | Qneg : ratio  \to Q.
  66
  67 definition Q_of_nat ≝
  68  λn.
  69   match factorize n with
  70    [ nfa_zero ⇒ OQ
  71    | nfa_one ⇒ Qpos one
  72    | nfa_proper l ⇒ Qpos (frac (fraction_of_nat_fact l))
  73    ].
  74
  75 let rec enumerator_integral_fraction l ≝
  76  match l with
  77   [ pp n ⇒ Some ? l
  78   | nn _ ⇒ None ?
  79   | cons z r ⇒
  80      match enumerator_integral_fraction r with
  81       [ None ⇒
  82          match z with
  83           [ pos n ⇒ Some ? (pp n)
  84           | _ ⇒ None ?
  85           ]
  86       | Some r' ⇒
  87          Some ?
  88           match z with
  89            [ neg _ ⇒ cons OZ r'
  90            | _ ⇒ cons z r'
  91            ]
  92        ]
  93   ].
  94
  95 let rec denominator_integral_fraction l ≝
  96  match l with
  97   [ pp _ ⇒ None ?
  98   | nn n ⇒ Some ? (pp n)
  99   | cons z r ⇒
 100      match denominator_integral_fraction r with
 101       [ None ⇒
 102          match z with
 103           [ neg n ⇒ Some ? (pp n)
 104           | _ ⇒ None ?
 105           ]
 106       | Some r' ⇒
 107          Some ?
 108           match z with
 109            [ pos _ ⇒ cons OZ r'
 110            | neg m ⇒ cons (pos m) r'
 111            | OZ ⇒ cons OZ r'
 112            ]
 113        ]
 114   ].
 115
 116 definition enumerator_of_fraction ≝
 117  λq.
 118   match q with
 119    [ one ⇒ S O
 120    | frac f ⇒
 121       match enumerator_integral_fraction f with
 122        [ None ⇒ S O
 123        | Some l ⇒ defactorize_aux (nat_fact_of_integral_fraction l) O
 124        ]
 125    ].
 126
 127 definition denominator_of_fraction ≝
 128  λq.
 129   match q with
 130    [ one ⇒ S O
 131    | frac f ⇒
 132       match denominator_integral_fraction f with
 133        [ None ⇒ S O
 134        | Some l ⇒ defactorize_aux (nat_fact_of_integral_fraction l) O
 135        ]
 136    ].
 137
 138 definition enumerator ≝
 139  λq.
 140   match q with
 141    [ OQ ⇒ OZ
 142    | Qpos r ⇒ pos (pred (enumerator_of_fraction r))
 143    | Qneg r ⇒ neg(pred (enumerator_of_fraction r))
 144    ].
 145
 146 definition denominator ≝
 147  λq.
 148   match q with
 149    [ OQ ⇒ S O
 150    | Qpos r ⇒ denominator_of_fraction r
 151    | Qneg r ⇒ denominator_of_fraction r
 152    ].
 153
 154 (* double elimination principles *)
 155 theorem fraction_elim2:
 156 \forall R:fraction \to fraction \to Prop.
 157 (\forall n:nat.\forall g:fraction.R (pp n) g) \to
 158 (\forall n:nat.\forall g:fraction.R (nn n) g) \to
 159 (\forall x:Z.\forall f:fraction.\forall m:nat.R (cons x f) (pp m)) \to
 160 (\forall x:Z.\forall f:fraction.\forall m:nat.R (cons x f) (nn m)) \to
 161 (\forall x,y:Z.\forall f,g:fraction.R f g \to R (cons x f) (cons y g)) \to
 162 \forall f,g:fraction. R f g.
 163 intros 7.elim f.
 164   apply H.
 165   apply H1.
 166   elim g.
 167     apply H2.
 168     apply H3.
 169     apply H4.apply H5.
 170 qed.
 171
 172 (* boolean equality *)
 173 let rec eqfb f g \def
 174 match f with
 175 [ (pp n) \Rightarrow
 176   match g with
 177   [ (pp m) \Rightarrow eqb n m
 178   | (nn m) \Rightarrow false
 179   | (cons y g1) \Rightarrow false]
 180 | (nn n) \Rightarrow
 181   match g with
 182   [ (pp m) \Rightarrow false
 183   | (nn m) \Rightarrow eqb n m
 184   | (cons y g1) \Rightarrow false]
 185 | (cons x f1) \Rightarrow
 186   match g with
 187   [ (pp m) \Rightarrow false
 188   | (nn m) \Rightarrow false
 189   | (cons y g1) \Rightarrow andb (eqZb x y) (eqfb f1 g1)]].
 190
 191 (* discrimination *)
 192 definition aux \def
 193   \lambda f. match f with
 194     [ (pp n) \Rightarrow n
 195     | (nn n) \Rightarrow n
 196     | (cons x f) \Rightarrow O].
 197
 198 definition fhd \def
 199 \lambda f. match f with
 200     [ (pp n) \Rightarrow (pos n)
 201     | (nn n) \Rightarrow (neg n)
 202     | (cons x f) \Rightarrow x].
 203
 204 definition ftl \def
 205 \lambda f. match f with
 206     [ (pp n) \Rightarrow (pp n)
 207     | (nn n) \Rightarrow (nn n)
 208     | (cons x f) \Rightarrow f].
 209
 210 theorem injective_pp : injective nat fraction pp.
 211 unfold injective.intros.
 212 change with ((aux (pp x)) = (aux (pp y))).
 213 apply eq_f.assumption.
 214 qed.
 215
 216 theorem injective_nn : injective nat fraction nn.
 217 unfold injective.intros.
 218 change with ((aux (nn x)) = (aux (nn y))).
 219 apply eq_f.assumption.
 220 qed.
 221
 222 theorem eq_cons_to_eq1: \forall f,g:fraction.\forall x,y:Z.
 223 (cons x f) = (cons y g) \to x = y.
 224 intros.
 225 change with ((fhd (cons x f)) = (fhd (cons y g))).
 226 apply eq_f.assumption.
 227 qed.
 228
 229 theorem eq_cons_to_eq2: \forall x,y:Z.\forall f,g:fraction.
 230 (cons x f) = (cons y g) \to f = g.
 231 intros.
 232 change with ((ftl (cons x f)) = (ftl (cons y g))).
 233 apply eq_f.assumption.
 234 qed.
 235
 236 theorem not_eq_pp_nn: \forall n,m:nat. pp n \neq nn m.
 237 intros.unfold Not. intro.
 238 change with match (pp n) with
 239 [ (pp n) \Rightarrow False
 240 | (nn n) \Rightarrow True
 241 | (cons x f) \Rightarrow True].
 242 rewrite > H.
 243 simplify.exact I.
 244 qed.
 245
 246 theorem not_eq_pp_cons:
 247 \forall n:nat.\forall x:Z. \forall f:fraction.
 248 pp n \neq cons x f.
 249 intros.unfold Not. intro.
 250 change with match (pp n) with
 251 [ (pp n) \Rightarrow False
 252 | (nn n) \Rightarrow True
 253 | (cons x f) \Rightarrow True].
 254 rewrite > H.
 255 simplify.exact I.
 256 qed.
 257
 258 theorem not_eq_nn_cons:
 259 \forall n:nat.\forall x:Z. \forall f:fraction.
 260 nn n \neq cons x f.
 261 intros.unfold Not. intro.
 262 change with match (nn n) with
 263 [ (pp n) \Rightarrow True
 264 | (nn n) \Rightarrow False
 265 | (cons x f) \Rightarrow True].
 266 rewrite > H.
 267 simplify.exact I.
 268 qed.
 269
 270 theorem decidable_eq_fraction: \forall f,g:fraction.
 271 decidable (f = g).
 272 intros.unfold decidable.
 273 apply (fraction_elim2 (\lambda f,g. f=g \lor (f=g \to False))).
 274   intros.elim g1.
 275     elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)).
 276       left.apply eq_f. assumption.
 277       right.intro.apply H.apply injective_pp.assumption.
 278     right.apply not_eq_pp_nn.
 279     right.apply not_eq_pp_cons.
 280   intros. elim g1.
 281       right.intro.apply (not_eq_pp_nn n1 n).apply sym_eq. assumption.
 282       elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)).
 283         left. apply eq_f. assumption.
 284         right.intro.apply H.apply injective_nn.assumption.
 285       right.apply not_eq_nn_cons.
 286   intros.right.intro.apply (not_eq_pp_cons m x f1).apply sym_eq.assumption.
 287   intros.right.intro.apply (not_eq_nn_cons m x f1).apply sym_eq.assumption.
 288   intros.elim H.
 289     elim ((decidable_eq_Z x y) : x=y \lor (x=y \to False)).
 290       left.apply eq_f2.assumption.
 291       assumption.
 292     right.intro.apply H2.apply (eq_cons_to_eq1 f1 g1).assumption.
 293     right.intro.apply H1.apply (eq_cons_to_eq2 x y f1 g1).assumption.
 294 qed.
 295
 296 theorem eqfb_to_Prop: \forall f,g:fraction.
 297 match (eqfb f g) with
 298 [true \Rightarrow f=g
 299 |false \Rightarrow f \neq g].
 300 intros.apply (fraction_elim2
 301 (\lambda f,g.match (eqfb f g) with
 302 [true \Rightarrow f=g
 303 |false \Rightarrow f \neq g])).
 304   intros.elim g1.
 305     simplify.apply eqb_elim.
 306       intro.simplify.apply eq_f.assumption.
 307       intro.simplify.unfold Not.intro.apply H.apply injective_pp.assumption.
 308     simplify.apply not_eq_pp_nn.
 309     simplify.apply not_eq_pp_cons.
 310   intros.elim g1.
 311     simplify.unfold Not.intro.apply (not_eq_pp_nn n1 n).apply sym_eq. assumption.
 312     simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption.
 313     intro.simplify.unfold Not.intro.apply H.apply injective_nn.assumption.
 314   simplify.apply not_eq_nn_cons.
 315   intros.simplify.unfold Not.intro.apply (not_eq_pp_cons m x f1).apply sym_eq. assumption.
 316   intros.simplify.unfold Not.intro.apply (not_eq_nn_cons m x f1).apply sym_eq. assumption.
 317   intros.
 318    simplify.
 319    apply eqZb_elim.
 320       intro.generalize in match H.elim (eqfb f1 g1).
 321         simplify.apply eq_f2.assumption.
 322         apply H2.
 323       simplify.unfold Not.intro.apply H2.apply (eq_cons_to_eq2 x y).assumption.
 324       intro.simplify.unfold Not.intro.apply H1.apply (eq_cons_to_eq1 f1 g1).assumption.
 325 qed.