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