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