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