]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/Q/inv.ma
9cc2fc3b43ea9c7c06fd001338221d0c38d37759
[helm.git] / 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 *)