matita/contribs/library_auto/auto/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/library_autobatch/Q/q".
  16
  17 include "auto/Z/compare.ma".
  18 include "auto/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.
  48 elim f
  49 [ apply H
  50 | apply H1
  51 | elim g
  52   [ apply H2
  53   | apply H3
  54   | autobatch
  55     (*apply H4.
  56     apply H5*)
  57   ]
  58 ]
  59 qed.
  60
  61 (* boolean equality *)
  62 let rec eqfb f g \def
  63 match f with
  64 [ (pp n) \Rightarrow
  65   match g with
  66   [ (pp m) \Rightarrow eqb n m
  67   | (nn m) \Rightarrow false
  68   | (cons y g1) \Rightarrow false]
  69 | (nn n) \Rightarrow
  70   match g with
  71   [ (pp m) \Rightarrow false
  72   | (nn m) \Rightarrow eqb n m
  73   | (cons y g1) \Rightarrow false]
  74 | (cons x f1) \Rightarrow
  75   match g with
  76   [ (pp m) \Rightarrow false
  77   | (nn m) \Rightarrow false
  78   | (cons y g1) \Rightarrow andb (eqZb x y) (eqfb f1 g1)]].
  79
  80 (* discrimination *)
  81 definition aux \def
  82   \lambda f. match f with
  83     [ (pp n) \Rightarrow n
  84     | (nn n) \Rightarrow n
  85     | (cons x f) \Rightarrow O].
  86
  87 definition fhd \def
  88 \lambda f. match f with
  89     [ (pp n) \Rightarrow (pos n)
  90     | (nn n) \Rightarrow (neg n)
  91     | (cons x f) \Rightarrow x].
  92
  93 definition ftl \def
  94 \lambda f. match f with
  95     [ (pp n) \Rightarrow (pp n)
  96     | (nn n) \Rightarrow (nn n)
  97     | (cons x f) \Rightarrow f].
  98
  99 theorem injective_pp : injective nat fraction pp.
 100 unfold injective.
 101 intros.
 102 change with ((aux(pp x)) = (aux (pp y))).
 103 autobatch.
 104 (*apply eq_f.
 105 assumption.*)
 106 qed.
 107
 108 theorem injective_nn : injective nat fraction nn.
 109 unfold injective.
 110 intros.
 111 change with ((aux (nn x)) = (aux (nn y))).
 112 autobatch.
 113 (*apply eq_f.
 114 assumption.*)
 115 qed.
 116
 117 theorem eq_cons_to_eq1: \forall f,g:fraction.\forall x,y:Z.
 118 (cons x f) = (cons y g) \to x = y.
 119 intros.
 120 change with ((fhd (cons x f)) = (fhd (cons y g))).
 121 autobatch.
 122 (*apply eq_f.assumption.*)
 123 qed.
 124
 125 theorem eq_cons_to_eq2: \forall x,y:Z.\forall f,g:fraction.
 126 (cons x f) = (cons y g) \to f = g.
 127 intros.
 128 change with ((ftl (cons x f)) = (ftl (cons y g))).
 129 autobatch.
 130 (*apply eq_f.assumption.*)
 131 qed.
 132
 133 theorem not_eq_pp_nn: \forall n,m:nat. pp n \neq nn m.
 134 intros.
 135 unfold Not.
 136 intro.
 137 change with match (pp n) with
 138 [ (pp n) \Rightarrow False
 139 | (nn n) \Rightarrow True
 140 | (cons x f) \Rightarrow True].
 141 rewrite > H.
 142 simplify.
 143 exact I.
 144 qed.
 145
 146 theorem not_eq_pp_cons:
 147 \forall n:nat.\forall x:Z. \forall f:fraction.
 148 pp n \neq cons x f.
 149 intros.
 150 unfold Not.
 151 intro.
 152 change with match (pp n) with
 153 [ (pp n) \Rightarrow False
 154 | (nn n) \Rightarrow True
 155 | (cons x f) \Rightarrow True].
 156 rewrite > H.
 157 simplify.
 158 exact I.
 159 qed.
 160
 161 theorem not_eq_nn_cons:
 162 \forall n:nat.\forall x:Z. \forall f:fraction.
 163 nn n \neq cons x f.
 164 intros.
 165 unfold Not.
 166 intro.
 167 change with match (nn n) with
 168 [ (pp n) \Rightarrow True
 169 | (nn n) \Rightarrow False
 170 | (cons x f) \Rightarrow True].
 171 rewrite > H.
 172 simplify.
 173 exact I.
 174 qed.
 175
 176 theorem decidable_eq_fraction: \forall f,g:fraction.
 177 decidable (f = g).
 178 intros.
 179 unfold decidable.
 180 apply (fraction_elim2 (\lambda f,g. f=g \lor (f=g \to False)))
 181 [ intros.
 182   elim g1
 183   [ elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False))
 184     [ autobatch
 185       (*left.
 186       apply eq_f.
 187       assumption*)
 188     | right.
 189       intro.
 190       autobatch
 191       (*apply H.
 192       apply injective_pp.
 193       assumption*)
 194     ]
 195   | autobatch
 196     (*right.
 197     apply not_eq_pp_nn*)
 198   | autobatch
 199     (*right.
 200     apply not_eq_pp_cons*)
 201   ]
 202 | intros.
 203   elim g1
 204   [ right.
 205     intro.
 206     apply (not_eq_pp_nn n1 n).
 207     autobatch
 208     (*apply sym_eq.
 209     assumption*)
 210   | elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False))
 211     [ autobatch
 212       (*left.
 213       apply eq_f.
 214       assumption*)
 215     | right.
 216       intro.
 217       autobatch
 218       (*apply H.
 219       apply injective_nn.
 220       assumption*)
 221     ]
 222   | autobatch
 223     (*right.
 224     apply not_eq_nn_cons*)
 225   ]
 226 | intros.
 227   right.
 228   intro.
 229   apply (not_eq_pp_cons m x f1).
 230   autobatch
 231   (*apply sym_eq.
 232   assumption*)
 233 | intros.
 234   right.
 235   intro.
 236   apply (not_eq_nn_cons m x f1).
 237   autobatch
 238   (*apply sym_eq.
 239   assumption*)
 240 | intros.
 241   elim H
 242   [ elim ((decidable_eq_Z x y) : x=y \lor (x=y \to False))
 243     [ autobatch
 244       (*left.
 245       apply eq_f2;
 246         assumption*)
 247     | right.
 248       intro.
 249       autobatch
 250       (*apply H2.
 251       apply (eq_cons_to_eq1 f1 g1).
 252       assumption*)
 253     ]
 254   | right.
 255     intro.
 256     autobatch
 257     (*apply H1.
 258     apply (eq_cons_to_eq2 x y f1 g1).
 259     assumption*)
 260   ]
 261 ]
 262 qed.
 263
 264 theorem eqfb_to_Prop: \forall f,g:fraction.
 265 match (eqfb f g) with
 266 [true \Rightarrow f=g
 267 |false \Rightarrow f \neq g].
 268 intros.
 269 apply (fraction_elim2
 270 (\lambda f,g.match (eqfb f g) with
 271 [true \Rightarrow f=g
 272 |false \Rightarrow f \neq g]))
 273 [ intros.
 274   elim g1
 275   [ simplify.
 276     apply eqb_elim
 277     [ intro.
 278       simplify.
 279       autobatch
 280       (*apply eq_f.
 281       assumption*)
 282     | intro.
 283       simplify.
 284       unfold Not.
 285       intro.
 286       autobatch
 287       (*apply H.
 288       apply injective_pp.
 289       assumption*)
 290     ]
 291   | simplify.
 292     apply not_eq_pp_nn
 293   | simplify.
 294     apply not_eq_pp_cons
 295   ]
 296 | intros.
 297   elim g1
 298   [ simplify.
 299     unfold Not.
 300     intro.
 301     apply (not_eq_pp_nn n1 n).
 302     autobatch
 303     (*apply sym_eq.
 304     assumption*)
 305   | simplify.
 306     apply eqb_elim
 307     [ intro.
 308       simplify.
 309       autobatch
 310       (*apply eq_f.
 311       assumption*)
 312     | intro.
 313       simplify.
 314       unfold Not.
 315       intro.
 316       autobatch
 317       (*apply H.
 318       apply injective_nn.
 319       assumption*)
 320     ]
 321   | simplify.
 322     apply not_eq_nn_cons
 323   ]
 324 | intros.
 325   simplify.
 326   unfold Not.
 327   intro.
 328   apply (not_eq_pp_cons m x f1).
 329   autobatch
 330   (*apply sym_eq.
 331   assumption*)
 332 | intros.
 333   simplify.
 334   unfold Not.
 335   intro.
 336   apply (not_eq_nn_cons m x f1).
 337   autobatch
 338   (*apply sym_eq.
 339   assumption*)
 340 | intros.
 341   simplify.
 342   apply eqZb_elim
 343   [ intro.
 344     generalize in match H.
 345     elim (eqfb f1 g1)
 346     [ simplify.
 347       apply eq_f2
 348       [ assumption
 349       | (*qui autobatch non chiude il goal*)
 350         apply H2
 351       ]
 352     | simplify.
 353       unfold Not.
 354       intro.
 355       apply H2.
 356       autobatch
 357       (*apply (eq_cons_to_eq2 x y).
 358       assumption*)
 359     ]
 360   | intro.
 361     simplify.
 362     unfold Not.
 363     intro.
 364     autobatch
 365     (*apply H1.
 366     apply (eq_cons_to_eq1 f1 g1).
 367     assumption*)
 368   ]
 369 ]
 370 qed.
 371
 372 let rec finv f \def
 373   match f with
 374   [ (pp n) \Rightarrow (nn n)
 375   | (nn n) \Rightarrow (pp n)
 376   | (cons x g) \Rightarrow (cons (Zopp x) (finv g))].
 377
 378 definition Z_to_ratio :Z \to ratio \def
 379 \lambda x:Z. match x with
 380 [ OZ \Rightarrow one
 381 | (pos n) \Rightarrow frac (pp n)
 382 | (neg n) \Rightarrow frac (nn n)].
 383
 384 let rec ftimes f g \def
 385   match f with
 386   [ (pp n) \Rightarrow
 387     match g with
 388     [(pp m) \Rightarrow Z_to_ratio (pos n + pos m)
 389     | (nn m) \Rightarrow Z_to_ratio (pos n + neg m)
 390     | (cons y g1) \Rightarrow frac (cons (pos n + y) g1)]
 391   | (nn n) \Rightarrow
 392     match g with
 393     [(pp m) \Rightarrow Z_to_ratio (neg n + pos m)
 394     | (nn m) \Rightarrow Z_to_ratio (neg n + neg m)
 395     | (cons y g1) \Rightarrow frac (cons (neg n + y) g1)]
 396   | (cons x f1) \Rightarrow
 397     match g with
 398     [ (pp m) \Rightarrow frac (cons (x + pos m) f1)
 399     | (nn m) \Rightarrow frac (cons (x + neg m) f1)
 400     | (cons y g1) \Rightarrow
 401       match ftimes f1 g1 with
 402         [ one \Rightarrow Z_to_ratio (x + y)
 403         | (frac h) \Rightarrow frac (cons (x + y) h)]]].
 404
 405 theorem symmetric2_ftimes: symmetric2 fraction ratio ftimes.
 406 unfold symmetric2.
 407 intros.
 408 apply (fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f))
 409 [ intros.
 410   elim g
 411   [ change with (Z_to_ratio (pos n + pos n1) = Z_to_ratio (pos n1 + pos n)).
 412     autobatch
 413     (*apply eq_f.
 414     apply sym_Zplus*)
 415   | change with (Z_to_ratio (pos n + neg n1) = Z_to_ratio (neg n1 + pos n)).
 416     autobatch
 417     (*apply eq_f.
 418     apply sym_Zplus*)
 419   | change with (frac (cons (pos n + z) f) = frac (cons (z + pos n) f)).
 420     autobatch
 421     (*rewrite < sym_Zplus.
 422     reflexivity*)
 423   ]
 424 | intros.
 425   elim g
 426   [ change with (Z_to_ratio (neg n + pos n1) = Z_to_ratio (pos n1 + neg n)).
 427     autobatch
 428     (*apply eq_f.
 429     apply sym_Zplus*)
 430   | change with (Z_to_ratio (neg n + neg n1) = Z_to_ratio (neg n1 + neg n)).
 431     autobatch
 432     (*apply eq_f.
 433     apply sym_Zplus*)
 434   | change with (frac (cons (neg n + z) f) = frac (cons (z + neg n) f)).
 435     autobatch
 436     (*rewrite < sym_Zplus.
 437     reflexivity*)
 438   ]
 439 | intros.
 440   change with (frac (cons (x1 + pos m) f) = frac (cons (pos m + x1) f)).
 441   autobatch
 442   (*rewrite < sym_Zplus.
 443   reflexivity*)
 444 | intros.
 445   change with (frac (cons (x1 + neg m) f) = frac (cons (neg m + x1) f)).
 446   autobatch
 447   (*rewrite < sym_Zplus.
 448   reflexivity*)
 449 | intros.
 450    (*CSC: simplify does something nasty here because of a redex in Zplus *)
 451    change with
 452    (match ftimes f g with
 453    [ one \Rightarrow Z_to_ratio (x1 + y1)
 454    | (frac h) \Rightarrow frac (cons (x1 + y1) h)] =
 455    match ftimes g f with
 456    [ one \Rightarrow Z_to_ratio (y1 + x1)
 457    | (frac h) \Rightarrow frac (cons (y1 + x1) h)]).
 458    rewrite < H.
 459    rewrite < sym_Zplus.
 460    reflexivity
 461 ]
 462 qed.
 463
 464 theorem ftimes_finv : \forall f:fraction. ftimes f (finv f) = one.
 465 intro.
 466 elim f
 467 [ change with (Z_to_ratio (pos n + - (pos n)) = one).
 468   autobatch
 469   (*rewrite > Zplus_Zopp.
 470   reflexivity*)
 471 | change with (Z_to_ratio (neg n + - (neg n)) = one).
 472   autobatch
 473   (*rewrite > Zplus_Zopp.
 474   reflexivity*)
 475 |
 476   (*CSC: simplify does something nasty here because of a redex in Zplus *)
 477   (* again: we would need something to help finding the right change *)
 478   change with
 479   (match ftimes f1 (finv f1) with
 480   [ one \Rightarrow Z_to_ratio (z + - z)
 481   | (frac h) \Rightarrow frac (cons (z + - z) h)] = one).
 482   rewrite > H.
 483   rewrite > Zplus_Zopp.
 484   reflexivity
 485 ]
 486 qed.
 487
 488 definition rtimes : ratio \to ratio \to ratio \def
 489 \lambda r,s:ratio.
 490   match r with
 491   [one \Rightarrow s
 492   | (frac f) \Rightarrow
 493       match s with
 494       [one \Rightarrow frac f
 495       | (frac g) \Rightarrow ftimes f g]].
 496
 497 theorem symmetric_rtimes : symmetric ratio rtimes.
 498 change with (\forall r,s:ratio. rtimes r s = rtimes s r).
 499 intros.
 500 elim r
 501 [ elim s;reflexivity
 502 | elim s
 503   [ reflexivity
 504   | simplify.
 505     apply symmetric2_ftimes
 506   ]
 507 ]
 508 qed.
 509
 510 definition rinv : ratio \to ratio \def
 511 \lambda r:ratio.
 512   match r with
 513   [one \Rightarrow one
 514   | (frac f) \Rightarrow frac (finv f)].
 515
 516 theorem rtimes_rinv: \forall r:ratio. rtimes r (rinv r) = one.
 517 intro.
 518 elim r
 519 [ reflexivity
 520 | simplify.
 521   apply ftimes_finv
 522 ]
 523 qed.