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 let rec finv f \def
  18   match f with
  19   [ (pp n) \Rightarrow (nn n)
  20   | (nn n) \Rightarrow (pp n)
  21   | (cons x g) \Rightarrow (cons (Zopp x) (finv g))].
  22
  23 theorem finv_finv: ∀f. finv (finv f) = f.
  24  intro;
  25  elim f;
  26   [1,2: reflexivity
  27   | simplify;
  28     rewrite > H;
  29     rewrite > Zopp_Zopp;
  30     reflexivity
  31   ]
  32 qed.
  33
  34 definition rinv : ratio \to ratio \def
  35 \lambda r:ratio.
  36   match r with
  37   [one \Rightarrow one
  38   | (frac f) \Rightarrow frac (finv f)].
  39
  40 theorem rinv_rinv: ∀r. rinv (rinv r) = r.
  41  intro;
  42  elim r;
  43   [ reflexivity
  44   | simplify;
  45     rewrite > finv_finv;
  46     reflexivity]
  47 qed.
  48
  49 definition Qinv : Q → Q ≝
  50  λp.
  51   match p with
  52    [ OQ ⇒ OQ  (* arbitrary value *)
  53    | Qpos r ⇒ Qpos (rinv r)
  54    | Qneg r ⇒ Qneg (rinv r)
  55    ].
  56
  57 theorem Qinv_Qinv: ∀q. Qinv (Qinv q) = q.
  58  intro;
  59  elim q;
  60   [ reflexivity
  61   |*:simplify;
  62     rewrite > rinv_rinv;
  63     reflexivity]
  64 qed.
  65
  66 theorem denominator_integral_factor_finv:
  67  ∀f. enumerator_integral_fraction f = denominator_integral_fraction (finv f).
  68  intro;
  69  elim f;
  70   [1,2: reflexivity
  71   |simplify;
  72    rewrite > H;
  73    elim z; simplify; reflexivity]
  74 qed.
  75
  76 definition is_positive ≝
  77  λq.
  78   match q with
  79    [ Qpos _ ⇒ True
  80    | _ ⇒ False
  81    ].
  82
  83 definition is_negative ≝
  84  λq.
  85   match q with
  86    [ Qneg _ ⇒ True
  87    | _ ⇒ False
  88    ].
  89
  90 theorem is_positive_denominator_Qinv:
  91  ∀q. is_positive q → enumerator q = denominator (Qinv q).
  92  intro;
  93  elim q;
  94   [1,3: elim H;
  95   | simplify; clear H;
  96     elim r; simplify;
  97      [ reflexivity
  98      | rewrite > denominator_integral_factor_finv;
  99        reflexivity]]
 100 qed.
 101
 102 theorem is_negative_denominator_Qinv:
 103  ∀q. is_negative q → enumerator q = -(denominator (Qinv q)).
 104  intro;
 105  elim q;
 106   [1,2: elim H;
 107   | simplify; clear H;
 108     elim r; simplify;
 109      [ reflexivity
 110      | rewrite > denominator_integral_factor_finv;
 111        unfold Zopp;
 112        elim (denominator_integral_fraction (finv f));
 113        simplify;
 114         [ reflexivity
 115         | generalize in match (lt_O_defactorize_aux (nat_fact_of_integral_fraction a) O);
 116           elim (defactorize_aux (nat_fact_of_integral_fraction a) O);
 117           simplify;
 118            [ elim (Not_lt_n_n ? H)
 119            | reflexivity]]]]
 120 qed.
 121
 122 theorem is_positive_enumerator_Qinv:
 123   ∀q. is_positive q → enumerator (Qinv q) = denominator q.
 124  intros;
 125  lapply (is_positive_denominator_Qinv (Qinv q));
 126   [ rewrite > Qinv_Qinv in Hletin;
 127     assumption
 128   | generalize in match H; elim q; assumption]
 129 qed.
 130
 131 theorem is_negative_enumerator_Qinv:
 132   ∀q. is_negative q → enumerator (Qinv q) = -(denominator q).
 133  intros;
 134  lapply (is_negative_denominator_Qinv (Qinv q));
 135   [ rewrite > Qinv_Qinv in Hletin;
 136     assumption
 137   | generalize in match H; elim q; assumption]
 138 qed.