]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/Q/frac.ma
9ce49360496d4e3b02d641effccacbc9e6833deb
[helm.git] / helm / software / matita / library / Q / frac.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 (*
16 let rec nat_fact_to_fraction_inv l \def
17   match l with
18   [nf_last a \Rightarrow nn a
19   |nf_cons a p \Rightarrow 
20     cons (neg_Z_of_nat a) (nat_fact_to_fraction_inv p)
21   ]
22 .
23
24 definition nat_fact_all_to_Q_inv \def
25 \lambda n.
26   match n with
27   [nfa_zero \Rightarrow OQ
28   |nfa_one \Rightarrow Qpos one
29   |nfa_proper l \Rightarrow Qpos (frac (nat_fact_to_fraction_inv l))
30   ]
31 .
32
33 definition nat_to_Q_inv \def
34 \lambda n. nat_fact_all_to_Q_inv (factorize n).
35
36 definition frac:nat \to nat \to Q \def
37 \lambda p,q. Qtimes (nat_to_Q p) (Qinv (nat_to_Q q)).
38
39 theorem Qtimes_frac_frac: \forall p,q,r,s.
40 Qtimes (frac p q) (frac r s) = (frac (p*r) (q*s)).
41 intros.
42 unfold frac.
43 rewrite > associative_Qtimes.
44 rewrite < associative_Qtimes in ⊢ (? ? (? ? %) ?).
45 rewrite > symmetric_Qtimes in ⊢ (? ? (? ? (? % ?)) ?).
46 rewrite > associative_Qtimes in ⊢ (? ? (? ? %) ?).
47 rewrite < associative_Qtimes.
48 rewrite < times_Qtimes.
49 rewrite < Qinv_Qtimes'.
50 rewrite < times_Qtimes.
51 reflexivity.
52 qed.
53 *)
54
55 (*     
56 definition numQ:Q \to Z \def
57 \lambda q. 
58 match q with
59 [OQ \Rightarrow OZ
60 |Qpos r \Rightarrow Z_of_nat (defactorize (numeratorQ (Qpos r)))
61 |Qneg r \Rightarrow neg_Z_of_nat (defactorize (numeratorQ (Qpos r)))
62 ].
63 *)
64
65 alias id "numeratorQ" = "cic:/matita/Q/q/q/numeratorQ.con".
66 alias id "nat" = "cic:/matita/nat/nat/nat.ind#xpointer(1/1)".
67 alias id "defactorize" = "cic:/matita/nat/factorization/defactorize.con".
68 alias id "Q" = "cic:/matita/Q/q/q/Q.ind#xpointer(1/1)".
69 definition numQ:Q \to nat \def
70 \lambda q. defactorize (numeratorQ q).
71
72 alias id "Qinv" = "cic:/matita/Q/q/qinv/Qinv.con".
73 definition denomQ:Q \to nat \def
74 \lambda q. defactorize (numeratorQ (Qinv q)).
75
76 (*CSC
77 theorem frac_numQ_denomQ1: \forall r:ratio. 
78 frac (numQ (Qpos r)) (denomQ (Qpos r)) = (Qpos r).
79 intro.
80 unfold frac.unfold denomQ.unfold numQ.
81 unfold nat_to_Q.
82 rewrite > factorize_defactorize.
83 rewrite > factorize_defactorize.
84 elim r
85   [reflexivity
86   |elim f
87     [reflexivity
88     |reflexivity
89     |apply Qtimes_numerator_denominator.
90     ]
91   ]
92 qed.*)
93
94 (*CSC
95 theorem frac_numQ_denomQ2: \forall r:ratio. 
96 frac (numQ (Qneg r)) (denomQ (Qneg r)) = (Qpos r).
97 intro.
98 unfold frac.unfold denomQ.unfold numQ.
99 unfold nat_to_Q.
100 rewrite > factorize_defactorize.
101 rewrite > factorize_defactorize.
102 elim r
103   [reflexivity
104   |elim f
105     [reflexivity
106     |reflexivity
107     |apply Qtimes_numerator_denominator.
108     ]
109   ]
110 qed.*)
111
112 alias id "Qpos" = "cic:/matita/Q/q/q/Q.ind#xpointer(1/1/2)".
113 alias id "OQ" = "cic:/matita/Q/q/q/Q.ind#xpointer(1/1/1)".
114 definition Qabs:Q \to Q \def \lambda q.
115 match q with
116 [OQ \Rightarrow OQ
117 |Qpos q \Rightarrow Qpos q
118 |Qneg q \Rightarrow Qpos q
119 ].
120 (*CSC
121 theorem frac_numQ_denomQ: \forall q. 
122 frac (numQ q) (denomQ q) = (Qabs q).
123 intros.
124 cases q
125   [reflexivity
126   |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ1
127   |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2
128   ]
129 qed.*)
130 (*CSC
131 definition Qfrac: Z \to nat \to Q \def
132 \lambda z,n.match z with
133 [OZ \Rightarrow OQ
134 |Zpos m \Rightarrow (frac (S m) n)
135 |Zneg m \Rightarrow Qopp (frac (S m) n)
136 ].
137
138 definition QnumZ \def \lambda q.
139 match q with
140 [OQ \Rightarrow OZ
141 |Qpos r \Rightarrow Z_of_nat (numQ (Qpos r))
142 |Qneg r \Rightarrow neg_Z_of_nat (numQ (Qpos r))
143 ].
144
145 theorem Qfrac_Z_of_nat: \forall n,m.
146 Qfrac (Z_of_nat n) m = frac n m.
147 intros.cases n;reflexivity.
148 qed.
149
150 theorem Qfrac_neg_Z_of_nat: \forall n,m.
151 Qfrac (neg_Z_of_nat n) m = Qopp (frac n m).
152 intros.cases n;reflexivity.
153 qed.
154
155 theorem Qfrac_QnumZ_denomQ: \forall q. 
156 Qfrac (QnumZ q) (denomQ q) = q.
157 intros.
158 cases q
159   [reflexivity
160   |change with
161     (Qfrac (Z_of_nat (numQ (Qpos r))) (denomQ (Qpos r))=Qpos r).
162    rewrite > Qfrac_Z_of_nat.
163    apply frac_numQ_denomQ1.
164   |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2
165   ]
166 qed.
167 *)