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 (**************************************************************************)
15 include "Q/q/qinv.ma".
16 include "Q/ratio/rtimes.ma".
18 definition Qtimes : Q \to Q \to Q \def
25 |Qpos q1 \Rightarrow Qpos (rtimes p1 q1)
26 |Qneg q1 \Rightarrow Qneg (rtimes p1 q1)
31 |Qpos q1 \Rightarrow Qneg (rtimes p1 q1)
32 |Qneg q1 \Rightarrow Qpos (rtimes p1 q1)
36 interpretation "rational times" 'times x y = (Qtimes x y).
38 theorem Qtimes_q_OQ: ∀q. q * OQ = OQ.
44 theorem symmetric_Qtimes: symmetric ? Qtimes.
47 [ rewrite > Qtimes_q_OQ; reflexivity
50 try rewrite > sym_rtimes;
55 theorem Qtimes_q_Qone: ∀q.q * Qone = q.
58 |2,3: cases r; reflexivity
62 theorem Qtimes_Qone_q: ∀q.Qone * q = q.
65 |2,3: cases r; reflexivity
69 theorem Qtimes_Qinv: ∀q. q ≠ OQ → q * (Qinv q) = Qpos one.
74 rewrite > rtimes_rinv;
79 theorem times_fa_Qtimes: \forall f,g. nat_fact_all_to_Q (times_fa f g) =
80 Qtimes (nat_fact_all_to_Q f) (nat_fact_all_to_Q g).
88 |rewrite > times_f_ftimes.reflexivity]]
91 theorem times_Qtimes: \forall p,q.
92 (nat_to_Q (p*q)) = Qtimes (nat_to_Q p) (nat_to_Q q).
93 intros.unfold nat_to_Q.
94 rewrite < times_fa_Qtimes.
95 rewrite < eq_times_times_fa.
99 theorem associative_Qtimes:associative ? Qtimes.
103 (* non posso scrivere 2,3: ... ?? *)
108 |simplify.rewrite > associative_rtimes.
110 |simplify.rewrite > associative_rtimes.
115 |simplify.rewrite > associative_rtimes.
117 |simplify.rewrite > associative_rtimes.
125 |simplify.rewrite > associative_rtimes.
127 |simplify.rewrite > associative_rtimes.
132 |simplify.rewrite > associative_rtimes.
134 |simplify.rewrite > associative_rtimes.
138 theorem eq_Qtimes_OQ_to_eq_OQ: \forall p,q.
139 Qtimes p q = OQ \to p = OQ \lor q = OQ.
142 [intro.left.reflexivity
144 [intro.right.reflexivity
145 |simplify.intro.destruct H
146 |simplify.intro.destruct H
149 [intro.right.reflexivity
150 |simplify.intro.destruct H
151 |simplify.intro.destruct H]]
154 theorem Qinv_Qtimes: \forall p,q.
155 p \neq OQ \to q \neq OQ \to Qinv(Qtimes p q) = Qtimes (Qinv p) (Qinv q).
157 rewrite < Qtimes_Qone_q in ⊢ (? ? ? %).
158 rewrite < (Qtimes_Qinv (Qtimes p q))
159 [lapply (Qtimes_Qinv ? H).
160 lapply (Qtimes_Qinv ? H1).
161 rewrite > symmetric_Qtimes in ⊢ (? ? ? (? % ?)).
162 rewrite > associative_Qtimes.
163 rewrite > associative_Qtimes.
164 rewrite < associative_Qtimes in ⊢ (? ? ? (? ? (? ? %))).
165 rewrite < symmetric_Qtimes in ⊢ (? ? ? (? ? (? ? (? % ?)))).
166 rewrite > associative_Qtimes in ⊢ (? ? ? (? ? (? ? %))).
168 rewrite > Qtimes_q_Qone.
170 rewrite > Qtimes_q_Qone.
173 elim (eq_Qtimes_OQ_to_eq_OQ ? ? H2)
174 [apply (H H3)|apply (H1 H3)]]
177 (* a stronger version, taking advantage of inv(O) = O *)
178 theorem Qinv_Qtimes': \forall p,q. Qinv(Qtimes p q) = Qtimes (Qinv p) (Qinv q).
184 |apply Qinv_Qtimes;intro;destruct H
185 |apply Qinv_Qtimes;intro;destruct H
189 |apply Qinv_Qtimes;intro;destruct H
190 |apply Qinv_Qtimes;intro;destruct H]]
193 theorem Qtimes_numerator_denominator: ∀f:fraction.
194 Qtimes (nat_fact_all_to_Q (numerator f)) (Qinv (nat_fact_all_to_Q (denominator f)))
200 |elim (or_numerator_nfa_one_nfa_proper f1)
203 cut (finv (nat_fact_to_fraction a) = f1)
206 rewrite > H2;rewrite > H1;simplify;
207 rewrite > Hcut;reflexivity
208 |generalize in match H.
209 rewrite > H2.rewrite > H1.simplify.
210 intro.destruct H3.reflexivity
215 rewrite > H2;simplify;
216 elim (or_numerator_nfa_one_nfa_proper (finv f1))
217 [1,3,5:elim H1;clear H1;
218 rewrite > H3;simplify;
219 cut (nat_fact_to_fraction a = f1)
220 [1,3,5:rewrite > Hcut;reflexivity
221 |*:generalize in match H;
224 rewrite > Qtimes_q_Qone;
231 generalize in match H;
233 rewrite > H3;simplify;