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.
  49   apply H.
  50   apply H1.
  51   elim g.
  52     apply H2.
  53     apply H3.
  54     apply H4.apply H5.
  55 qed.
  56
  57 (* boolean equality *)
  58 let rec eqfb f g \def
  59 match f with
  60 [ (pp n) \Rightarrow
  61   match g with
  62   [ (pp m) \Rightarrow eqb n m
  63   | (nn m) \Rightarrow false
  64   | (cons y g1) \Rightarrow false]
  65 | (nn n) \Rightarrow
  66   match g with
  67   [ (pp m) \Rightarrow false
  68   | (nn m) \Rightarrow eqb n m
  69   | (cons y g1) \Rightarrow false]
  70 | (cons x f1) \Rightarrow
  71   match g with
  72   [ (pp m) \Rightarrow false
  73   | (nn m) \Rightarrow false
  74   | (cons y g1) \Rightarrow andb (eqZb x y) (eqfb f1 g1)]].
  75
  76 (* discrimination *)
  77 definition aux \def
  78   \lambda f. match f with
  79     [ (pp n) \Rightarrow n
  80     | (nn n) \Rightarrow n
  81     | (cons x f) \Rightarrow O].
  82
  83 definition fhd \def
  84 \lambda f. match f with
  85     [ (pp n) \Rightarrow (pos n)
  86     | (nn n) \Rightarrow (neg n)
  87     | (cons x f) \Rightarrow x].
  88
  89 definition ftl \def
  90 \lambda f. match f with
  91     [ (pp n) \Rightarrow (pp n)
  92     | (nn n) \Rightarrow (nn n)
  93     | (cons x f) \Rightarrow f].
  94
  95 theorem injective_pp : injective nat fraction pp.
  96 simplify.intros.
  97 change with (aux (pp x)) = (aux (pp y)).
  98 apply eq_f.assumption.
  99 qed.
 100
 101 theorem injective_nn : injective nat fraction nn.
 102 simplify.intros.
 103 change with (aux (nn x)) = (aux (nn y)).
 104 apply eq_f.assumption.
 105 qed.
 106
 107 theorem eq_cons_to_eq1: \forall f,g:fraction.\forall x,y:Z.
 108 (cons x f) = (cons y g) \to x = y.
 109 intros.
 110 change with (fhd (cons x f)) = (fhd (cons y g)).
 111 apply eq_f.assumption.
 112 qed.
 113
 114 theorem eq_cons_to_eq2: \forall x,y:Z.\forall f,g:fraction.
 115 (cons x f) = (cons y g) \to f = g.
 116 intros.
 117 change with (ftl (cons x f)) = (ftl (cons y g)).
 118 apply eq_f.assumption.
 119 qed.
 120
 121 theorem not_eq_pp_nn: \forall n,m:nat. \lnot (pp n) = (nn m).
 122 intros.simplify. intro.
 123 change with match (pp n) with
 124 [ (pp n) \Rightarrow False
 125 | (nn n) \Rightarrow True
 126 | (cons x f) \Rightarrow True].
 127 rewrite > H.
 128 simplify.exact I.
 129 qed.
 130
 131 theorem not_eq_pp_cons:
 132 \forall n:nat.\forall x:Z. \forall f:fraction.
 133 \lnot (pp n) = (cons x f).
 134 intros.simplify. intro.
 135 change with match (pp n) with
 136 [ (pp n) \Rightarrow False
 137 | (nn n) \Rightarrow True
 138 | (cons x f) \Rightarrow True].
 139 rewrite > H.
 140 simplify.exact I.
 141 qed.
 142
 143 theorem not_eq_nn_cons:
 144 \forall n:nat.\forall x:Z. \forall f:fraction.
 145 \lnot (nn n) = (cons x f).
 146 intros.simplify. intro.
 147 change with match (nn n) with
 148 [ (pp n) \Rightarrow True
 149 | (nn n) \Rightarrow False
 150 | (cons x f) \Rightarrow True].
 151 rewrite > H.
 152 simplify.exact I.
 153 qed.
 154
 155 theorem decidable_eq_fraction: \forall f,g:fraction.
 156 decidable (f = g).
 157 intros.simplify.
 158 apply fraction_elim2 (\lambda f,g. Or (f=g) (f=g \to False)).
 159   intros.elim g1.
 160     elim ((decidable_eq_nat n n1) : Or (n=n1) (n=n1 \to False)).
 161       left.apply eq_f. assumption.
 162       right.intro.apply H.apply injective_pp.assumption.
 163     right.apply not_eq_pp_nn.
 164     right.apply not_eq_pp_cons.
 165   intros. elim g1.
 166       right.intro.apply not_eq_pp_nn n1 n ?.apply sym_eq. assumption.
 167       elim ((decidable_eq_nat n n1) : Or (n=n1) (n=n1 \to False)).
 168         left. apply eq_f. assumption.
 169         right.intro.apply H.apply injective_nn.assumption.
 170       right.apply not_eq_nn_cons.
 171   intros.right.intro.apply not_eq_pp_cons m x f1 ?.apply sym_eq.assumption.
 172   intros.right.intro.apply not_eq_nn_cons m x f1 ?.apply sym_eq.assumption.
 173   intros.elim H.
 174     elim ((decidable_eq_Z x y) : Or (x=y) (x=y \to False)).
 175       left.apply eq_f2.assumption.
 176       assumption.
 177     right.intro.apply H2.apply eq_cons_to_eq1 f1 g1.assumption.
 178     right.intro.apply H1.apply eq_cons_to_eq2 x y f1 g1.assumption.
 179 qed.
 180
 181 theorem eqfb_to_Prop: \forall f,g:fraction.
 182 match (eqfb f g) with
 183 [true \Rightarrow f=g
 184 |false \Rightarrow \lnot f=g].
 185 intros.apply fraction_elim2
 186 (\lambda f,g.match (eqfb f g) with
 187 [true \Rightarrow f=g
 188 |false \Rightarrow \lnot f=g]).
 189   intros.elim g1.
 190     simplify.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_nn.
 194     simplify.apply not_eq_pp_cons.
 195   intros.elim g1.
 196     simplify.intro.apply not_eq_pp_nn n1 n ?.apply sym_eq. assumption.
 197     simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption.
 198     intro.simplify.intro.apply H.apply injective_nn.assumption.
 199   simplify.apply not_eq_nn_cons.
 200   intros.simplify.intro.apply not_eq_pp_cons m x f1 ?.apply sym_eq. assumption.
 201   intros.simplify.intro.apply not_eq_nn_cons m x f1 ?.apply sym_eq. assumption.
 202   intros.
 203    change in match (eqfb (cons x f1) (cons y g1))
 204    with (andb (eqZb x y) (eqfb f1 g1)).
 205     apply eqZb_elim.
 206       intro.generalize in match H.elim (eqfb f1 g1).
 207         simplify.apply eq_f2.assumption.
 208         apply H2.
 209       simplify.intro.apply H2.apply eq_cons_to_eq2 x y.assumption.
 210       intro.simplify.intro.apply H1.apply eq_cons_to_eq1 f1 g1.assumption.
 211 qed.
 212
 213 let rec finv f \def
 214   match f with
 215   [ (pp n) \Rightarrow (nn n)
 216   | (nn n) \Rightarrow (pp n)
 217   | (cons x g) \Rightarrow (cons (Zopp x) (finv g))].
 218
 219 definition Z_to_ratio :Z \to ratio \def
 220 \lambda x:Z. match x with
 221 [ OZ \Rightarrow one
 222 | (pos n) \Rightarrow frac (pp n)
 223 | (neg n) \Rightarrow frac (nn n)].
 224
 225 let rec ftimes f g \def
 226   match f with
 227   [ (pp n) \Rightarrow
 228     match g with
 229     [(pp m) \Rightarrow Z_to_ratio (Zplus (pos n) (pos m))
 230     | (nn m) \Rightarrow Z_to_ratio (Zplus (pos n) (neg m))
 231     | (cons y g1) \Rightarrow frac (cons (Zplus (pos n) y) g1)]
 232   | (nn n) \Rightarrow
 233     match g with
 234     [(pp m) \Rightarrow Z_to_ratio (Zplus (neg n) (pos m))
 235     | (nn m) \Rightarrow Z_to_ratio (Zplus (neg n) (neg m))
 236     | (cons y g1) \Rightarrow frac (cons (Zplus (neg n) y) g1)]
 237   | (cons x f1) \Rightarrow
 238     match g with
 239     [ (pp m) \Rightarrow frac (cons (Zplus x (pos m)) f1)
 240     | (nn m) \Rightarrow frac (cons (Zplus x (neg m)) f1)
 241     | (cons y g1) \Rightarrow
 242       match ftimes f1 g1 with
 243         [ one \Rightarrow Z_to_ratio (Zplus x y)
 244         | (frac h) \Rightarrow frac (cons (Zplus x y) h)]]].
 245
 246 theorem symmetric2_ftimes: symmetric2 fraction ratio ftimes.
 247 simplify. intros.apply fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f).
 248   intros.elim g.
 249     change with Z_to_ratio (Zplus (pos n) (pos n1)) = Z_to_ratio (Zplus (pos n1) (pos n)).
 250      apply eq_f.apply sym_Zplus.
 251     change with Z_to_ratio (Zplus (pos n) (neg n1)) = Z_to_ratio (Zplus (neg n1) (pos n)).
 252      apply eq_f.apply sym_Zplus.
 253     change with frac (cons (Zplus (pos n) z) f) = frac (cons (Zplus z (pos n)) f).
 254      rewrite < sym_Zplus.reflexivity.
 255   intros.elim g.
 256     change with Z_to_ratio (Zplus (neg n) (pos n1)) = Z_to_ratio (Zplus (pos n1) (neg n)).
 257      apply eq_f.apply sym_Zplus.
 258     change with Z_to_ratio (Zplus (neg n) (neg n1)) = Z_to_ratio (Zplus (neg n1) (neg n)).
 259      apply eq_f.apply sym_Zplus.
 260     change with frac (cons (Zplus (neg n) z) f) = frac (cons (Zplus z (neg n)) f).
 261      rewrite < sym_Zplus.reflexivity.
 262   intros.change with frac (cons (Zplus x1 (pos m)) f) = frac (cons (Zplus (pos m) x1) f).
 263    rewrite < sym_Zplus.reflexivity.
 264   intros.change with frac (cons (Zplus x1 (neg m)) f) = frac (cons (Zplus (neg m) x1) f).
 265    rewrite < sym_Zplus.reflexivity.
 266   intros.
 267    change with
 268    match ftimes f g with
 269    [ one \Rightarrow Z_to_ratio (Zplus x1 y1)
 270    | (frac h) \Rightarrow frac (cons (Zplus x1 y1) h)] =
 271    match ftimes g f with
 272    [ one \Rightarrow Z_to_ratio (Zplus y1 x1)
 273    | (frac h) \Rightarrow frac (cons (Zplus y1 x1) h)].
 274     rewrite < H.rewrite < sym_Zplus.reflexivity.
 275 qed.
 276
 277 theorem ftimes_finv : \forall f:fraction. ftimes f (finv f) = one.
 278 intro.elim f.
 279   change with Z_to_ratio (Zplus (pos n) (Zopp (pos n))) = one.
 280    rewrite > Zplus_Zopp.reflexivity.
 281   change with Z_to_ratio (Zplus (neg n) (Zopp (neg n))) = one.
 282    rewrite > Zplus_Zopp.reflexivity.
 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 (Zplus z (Zopp z))
 287   | (frac h) \Rightarrow frac (cons (Zplus z (Zopp 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.