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