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