1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
19 [ (pp n) \Rightarrow (nn n)
20 | (nn n) \Rightarrow (pp n)
21 | (cons x g) \Rightarrow (cons (Zopp x) (finv g))].
23 theorem finv_finv: ∀f. finv (finv f) = f.
34 definition rinv : ratio \to ratio \def
38 | (frac f) \Rightarrow frac (finv f)].
40 theorem rinv_rinv: ∀r. rinv (rinv r) = r.
49 definition Qinv : Q → Q ≝
52 [ OQ ⇒ OQ (* arbitrary value *)
53 | Qpos r ⇒ Qpos (rinv r)
54 | Qneg r ⇒ Qneg (rinv r)
57 theorem Qinv_Qinv: ∀q. Qinv (Qinv q) = q.
66 theorem denominator_integral_factor_finv:
67 ∀f. enumerator_integral_fraction f = denominator_integral_fraction (finv f).
73 elim z; simplify; reflexivity]
76 definition is_positive ≝
83 definition is_negative ≝
90 theorem is_positive_denominator_Qinv:
91 ∀q. is_positive q → enumerator q = denominator (Qinv q).
98 | rewrite > denominator_integral_factor_finv;
102 theorem is_negative_denominator_Qinv:
103 ∀q. is_negative q → enumerator q = -(denominator (Qinv q)).
110 | rewrite > denominator_integral_factor_finv;
112 elim (denominator_integral_fraction (finv f));
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);
118 [ elim (Not_lt_n_n ? H)
122 theorem is_positive_enumerator_Qinv:
123 ∀q. is_positive q → enumerator (Qinv q) = denominator q.
125 lapply (is_positive_denominator_Qinv (Qinv q));
126 [ rewrite > Qinv_Qinv in Hletin;
128 | generalize in match H; elim q; assumption]
131 theorem is_negative_enumerator_Qinv:
132 ∀q. is_negative q → enumerator (Qinv q) = -(denominator q).
134 lapply (is_negative_denominator_Qinv (Qinv q));
135 [ rewrite > Qinv_Qinv in Hletin;
137 | generalize in match H; elim q; assumption]