helm/software/matita/library/Q/inv.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 "Q/q.ma".
  16
  17 theorem denominator_integral_factor_finv:
  18  ∀f. enumerator_integral_fraction f = denominator_integral_fraction (finv f).
  19  intro;
  20  elim f;
  21   [1,2: reflexivity
  22   |simplify;
  23    rewrite > H;
  24    elim z; simplify; reflexivity]
  25 qed.
  26
  27 definition is_positive ≝
  28  λq.
  29   match q with
  30    [ Qpos _ ⇒ True
  31    | _ ⇒ False
  32    ].
  33
  34 definition is_negative ≝
  35  λq.
  36   match q with
  37    [ Qneg _ ⇒ True
  38    | _ ⇒ False
  39    ].
  40
  41 theorem is_positive_denominator_Qinv:
  42  ∀q. is_positive q → enumerator q = denominator (Qinv q).
  43  intro;
  44  elim q;
  45   [1,3: elim H;
  46   | simplify; clear H;
  47     elim r; simplify;
  48      [ reflexivity
  49      | rewrite > denominator_integral_factor_finv;
  50        reflexivity]]
  51 qed.
  52
  53 theorem is_negative_denominator_Qinv:
  54  ∀q. is_negative q → enumerator q = -(denominator (Qinv q)).
  55  intro;
  56  elim q;
  57   [1,2: elim H;
  58   | simplify; clear H;
  59     elim r; simplify;
  60      [ reflexivity
  61      | rewrite > denominator_integral_factor_finv;
  62        unfold Zopp;
  63        elim (denominator_integral_fraction (finv f));
  64        simplify;
  65         [ reflexivity
  66         | generalize in match (lt_O_defactorize_aux (nat_fact_of_integral_fraction a) O);
  67           elim (defactorize_aux (nat_fact_of_integral_fraction a) O);
  68           simplify;
  69            [ elim (Not_lt_n_n ? H)
  70            | reflexivity]]]]
  71 qed.
  72
  73 theorem is_positive_enumerator_Qinv:
  74   ∀q. is_positive q → enumerator (Qinv q) = denominator q.
  75  intros;
  76  lapply (is_positive_denominator_Qinv (Qinv q));
  77   [ rewrite > Qinv_Qinv in Hletin;
  78     assumption
  79   | elim q in H ⊢ %; assumption]
  80 qed.
  81
  82 theorem is_negative_enumerator_Qinv:
  83   ∀q. is_negative q → enumerator (Qinv q) = -(denominator q).
  84  intros;
  85  lapply (is_negative_denominator_Qinv (Qinv q));
  86   [ rewrite > Qinv_Qinv in Hletin;
  87     assumption
  88   | elim q in H ⊢ %; assumption]
  89 qed.