]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/library/R/root.ma
advances non lfsx ...
[helm.git] / matitaB / matita / library / R / root.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "Q/q/q.ma".
16 include "R/r.ma". 
17
18 let rec Rexp_nat x n on n ≝
19  match n with
20  [ O ⇒ R1
21  | S p ⇒ x * (Rexp_nat x p) ].
22  
23 axiom daemon : False.
24
25 lemma Rexp_nat_tech : ∀a,b,n.O < n → R0 < b → b < a →
26   Rexp_nat a n - Rexp_nat b n ≤ n*(a - b)*Rexp_nat a (n-1).
27 intros;elim H
28 [simplify;right;autobatch paramodulation
29 |simplify in ⊢ (? ? (? ? %));rewrite < minus_n_O;
30  rewrite > distr_Rtimes_Rplus_l;
31  rewrite > sym_Rtimes;
32  rewrite > distr_Rtimes_Rplus_l;
33  rewrite > sym_Rtimes in ⊢ (? ? (? (? ? %) ?));rewrite < assoc_Rtimes;
34  rewrite > R_OF_nat_S;rewrite > sym_Rtimes in ⊢ (? ? (? ? (? ? %)));
35  rewrite > distr_Rtimes_Rplus_l;rewrite > Rtimes_x_R1;
36  rewrite > sym_Rplus in ⊢ (? ? (? % ?));
37  rewrite > assoc_Rplus;simplify;rewrite > sym_Rtimes;
38  apply Rle_plus_l;
39  do 2 rewrite > distr_Rtimes_Rplus_l;rewrite > Rtimes_x_R1;
40  rewrite < Rplus_x_R0;rewrite > sym_Rplus;
41  apply Rle_plus_r_to_l;rewrite < assoc_Rplus;
42  apply Rle_minus_l_to_r;rewrite > sym_Rplus;rewrite > Rplus_x_R0;
43  apply Rle_minus_l_to_r;rewrite < Ropp_Rtimes_r;
44  rewrite < Ropp_inv;rewrite < sym_Rplus;rewrite < sym_Rtimes;
45  rewrite > Ropp_Rtimes_r;rewrite < distr_Rtimes_Rplus_l;
46  apply (trans_Rle ? (b*n1*(a-b)*Rexp_nat a (n1-1)))
47  [do 2 rewrite > assoc_Rtimes;apply Rle_times_l
48   [rewrite < assoc_Rtimes;assumption|autobatch]
49  |rewrite > assoc_Rtimes in ⊢ (??%);rewrite < distr_Rtimes_Rplus_l;
50   rewrite < distr_Rtimes_Rplus_r;
51   rewrite > sym_Rtimes in ⊢ (? ? (? ? %));rewrite < assoc_Rtimes;
52   rewrite > sym_Rtimes;do 2 rewrite < assoc_Rtimes;
53   rewrite > (?:(Rexp_nat a n1 = Rexp_nat a (n1-1)*a))
54   [do 2 rewrite > assoc_Rtimes;do 2 rewrite > assoc_Rtimes in ⊢ (??%);
55    apply Rle_times_l
56    [apply Rle_times_r
57     [left;assumption
58     |elim daemon] (* trivial *)
59    |elim daemon] (* trivial: auxiliary lemma *)
60   |rewrite > sym_Rtimes;elim H3;simplify
61    [reflexivity
62    |rewrite < minus_n_O;reflexivity]]]]
63 qed.
64
65 (* FIXME: se uso la notazione, la disambiguazione fa un casino... *) 
66 (*lemma roots_lemma : ∀x:R.∀n:nat.R0 ≤ x → 1 ≤ n → ∃y.R0 ≤ y ∧ x = Rexp_nat y n.*)
67
68 lemma roots_lemma : ∀x:R.∀n:nat.R0 ≤ x → 1 ≤ n → ex ? (λy.R0 ≤ y ∧ x = Rexp_nat y n).
69 intros;cases H
70 [alias symbol "lt" = "real numbers less than".
71 letin bound ≝ (λy:R.R0 < y ∧ Rexp_nat y n < x); 
72  elim (R_dedekind bound)
73  [cut (R0 < a)
74   [|
75    (* Hp: ∀y.0<y → y^n<x → y≤a 
76       case 0 < x ≤ 1 : take y = x/2
77       0 < (x/2)^n < x ⇒ 0 < x/2 ≤ a
78       case 1 < x : take y = 1 
79       0 < 1^n = 1 < x ⇒ 0 < 1 ≤ a
80    unfold in H1;elim H1;unfold in H2;lapply (H1 R1)
81    [elim Hletin
82     [autobatch
83     |rewrite < H3;autobatch]
84    |unfold;split
85     [autobatch
86     |rewrite > Rtimes_x_R1;rewrite < Rplus_x_R0 in ⊢ (? % ?);
87      autobatch]] *)
88    elim daemon]
89  apply ex_intro[apply a]
90  split [left;assumption]
91  elim H3;unfold in H4;unfold bound in H4;
92  cases (trichotomy_Rlt x (Rexp_nat a n)) [|assumption]
93  cases H6
94  [letin k ≝ ((Rexp_nat a n - x)*Rinv (n*Rexp_nat a (n-1)));
95   cut (R0 < k) [|elim daemon]
96   cut (k < a) [|elim daemon]
97   cut (ub bound (a-k))
98   [lapply (H5 ? Hcut3);rewrite < Rplus_x_R0 in Hletin:(?%?);
99    rewrite > sym_Rplus in Hletin:(? % ?);lapply (Rle_plus_l_to_r ? ? ? Hletin);
100    rewrite > assoc_Rplus in Hletin1;
101    rewrite > sym_Rplus in Hletin1:(? ? (? ? %));
102    rewrite < assoc_Rplus in Hletin1;
103    lapply (Rle_minus_r_to_l ??? Hletin1);
104    rewrite > sym_Rplus in Hletin2;rewrite > Rplus_x_R0 in Hletin2;
105    rewrite > Rplus_Ropp in Hletin2;cases Hletin2
106    [elim (asym_Rlt ?? Hcut1 H8)
107    |rewrite > H8 in Hcut1;elim (irrefl_Rlt ? Hcut1)]
108   |unfold;intros;elim H8;unfold k;rewrite < Rplus_x_R0;
109    rewrite < sym_Rplus;apply Rle_minus_r_to_l;
110    apply (pos_z_to_le_Rtimes_Rtimes_to_lt ? ? (n*Rexp_nat a (n-1)))
111    [apply pos_times_pos_pos
112     [apply (nat_lt_to_R_lt ?? H1);
113     |elim daemon]
114    |rewrite > Rtimes_x_R0;do 2 rewrite > distr_Rtimes_Rplus_l;
115     rewrite > sym_Rtimes in ⊢ (? ? (? (? ? (? ? (? %))) ?));
116     rewrite > Ropp_Rtimes_r;
117     rewrite < assoc_Rtimes in ⊢ (? ? (? (? ? %) ?));
118     rewrite > Rinv_Rtimes_l
119     [rewrite > sym_Rtimes in ⊢ (? ? (? (? ? %) ?));
120      rewrite > Rtimes_x_R1;rewrite > distr_Ropp_Rplus;
121      rewrite < Ropp_inv;rewrite < assoc_Rplus;
122      rewrite > assoc_Rplus in ⊢ (? ? (? % ?));
123      rewrite > sym_Rplus in ⊢ (? ? (? % ?));
124      rewrite > assoc_Rplus;rewrite > sym_Rplus;
125      apply Rle_minus_l_to_r;rewrite > distr_Ropp_Rplus;
126      rewrite < Ropp_inv;rewrite < sym_Rplus;rewrite > Rplus_x_R0;
127      rewrite < distr_Rtimes_Rplus_l;
128      apply (trans_Rle ? (Rexp_nat a n - Rexp_nat y n)) 
129      [apply Rle_plus_l;left;autobatch
130      | cut (∀x,y.(S x ≤ y) = (x < y));[2: intros; reflexivity]
131        (* applyS Rexp_nat_tech by sym_Rtimes, assoc_Rtimes;*)
132       rewrite > assoc_Rtimes;rewrite > sym_Rtimes in ⊢ (??(??%));
133       rewrite < assoc_Rtimes;apply Rexp_nat_tech
134       [autobatch
135       |assumption
136       |(* by transitivity y^n < x < a^n and injectivity *) elim daemon]]
137     |intro;apply (irrefl_Rlt (n*Rexp_nat a (n-1)));
138      rewrite > H11 in ⊢ (?%?);apply pos_times_pos_pos
139      [apply (nat_lt_to_R_lt ?? H1);
140      |elim daemon]]]]
141 |elim (R_archimedean R1 ((x-Rexp_nat a n)/(n*Rexp_nat (a+1) (n-1)))) 
142  [|autobatch]
143  rewrite > Rtimes_x_R1 in H8;
144  letin h ≝ ((x-Rexp_nat a n)/(n*Rexp_nat (a+1) (n-1)*a1));
145  lapply (H4 (a+h))
146   [rewrite < Rplus_x_R0 in Hletin:(??%);rewrite < sym_Rplus in Hletin:(??%);
147    lapply (Rle_plus_r_to_l ? ? ? Hletin);
148    rewrite > sym_Rplus in Hletin1:(?(?%?)?);rewrite > assoc_Rplus in Hletin1;
149    rewrite > Rplus_Ropp in Hletin1;rewrite > Rplus_x_R0 in Hletin1;
150    unfold h in Hletin1;
151    cut (R0 < (x-Rexp_nat a n)/(n*Rexp_nat (a+1) (n-1)*a1))
152    [cases Hletin1
153     [elim (asym_Rlt ? ? Hcut1 H9)
154     |rewrite > H9 in Hcut1;elim (irrefl_Rlt ? Hcut1)]
155    |apply pos_times_pos_pos
156     [apply Rlt_plus_l_to_r;rewrite > sym_Rplus;rewrite > Rplus_x_R0;
157      assumption
158     |apply lt_R0_Rinv;apply pos_times_pos_pos
159      [apply pos_times_pos_pos
160       [apply (nat_lt_to_R_lt ?? H1);
161       |elim daemon]
162      |apply (trans_Rlt ???? H8);apply pos_times_pos_pos
163       [apply Rlt_plus_l_to_r;rewrite > sym_Rplus;rewrite > Rplus_x_R0;
164        assumption
165       |apply lt_R0_Rinv;apply pos_times_pos_pos
166        [apply (nat_lt_to_R_lt ?? H1);
167        |elim daemon]]]]]
168   |split
169    [(* show that h > R0, also useful in previous parts of the proof *)
170     elim daemon
171    |(* by monotonicity ov Rexp_nat *) elim daemon]]]
172 |apply ex_intro[apply (x/(x+R1))]
173  unfold bound;simplify;split
174  [apply pos_times_pos_pos
175   [assumption
176   |apply lt_R0_Rinv;apply pos_plus_pos_pos
177    [assumption
178    |autobatch]]
179  |apply (trans_Rlt ? (x/(x+R1)))
180   [(* antimonotone exponential with base in [0,1] *) elim daemon
181   |rewrite < Rtimes_x_R1 in ⊢ (??%);
182    apply Rlt_times_l
183    [rewrite < (Rinv_Rtimes_l R1)
184     [rewrite > sym_Rtimes in ⊢ (??%);rewrite > Rtimes_x_R1;
185      apply lt_Rinv
186      [autobatch
187      |rewrite > Rinv_Rtimes_l
188       [apply Rlt_minus_l_to_r;rewrite > Rplus_Ropp;assumption
189       |intro;elim not_eq_R0_R1;symmetry;assumption]]
190     |intro;elim not_eq_R0_R1;symmetry;assumption]
191    |assumption]]]
192 |apply ex_intro[apply (x+R1)]
193  unfold ub;intros;unfold in H3;elim H3;cases (trichotomy_Rlt y (x+R1))
194  [cases H6
195   [left;assumption
196   |elim (asym_Rlt (Rexp_nat y n) x)
197    [assumption
198    |apply (trans_Rlt ? y)
199      [apply (trans_Rlt ???? H7);rewrite > sym_Rplus;
200       apply Rlt_minus_l_to_r;rewrite > Rplus_Ropp;autobatch
201     |(* monotonia; il caso n=1 andra` facilmente gestito a parte *)
202      elim daemon]]]
203  |right;assumption]]
204 |apply ex_intro[apply R0]
205  split
206  [right;reflexivity
207  |rewrite < H2;elim H1;
208   simplify;rewrite > sym_Rtimes;rewrite > Rtimes_x_R0;reflexivity]]
209 qed.
210
211 definition root : ∀n:nat.∀x:R.O < n → R0 ≤ x → R.
212 intros;apply (\fst (choose ?? (roots_lemma x n ??)));assumption;
213 qed.
214
215 notation < "hvbox(maction (\root mstyle scriptlevel 1(term 19 n)
216          \of (term 19 x)) ((\root n \of x)\sub(h,k)))" 
217  with precedence 90 for @{ 'aroot $n $x $h $k}.
218  
219 interpretation "real numbers root" 'aroot n x h k = (root n x h k).
220
221 (* FIXME: qui non c'e` modo di far andare la notazione...*)
222 (*lemma root_sound : ∀n:nat.∀x:R.1 ≤ n → R0 ≤ x → 
223                      R0 ≤ (root n x ??) ∧ x = Rexp_nat (root n x ??) n.*)
224 alias id "PAnd" = "cic:/matita/logic/connectives/And.ind#xpointer(1/1)".
225
226 lemma root_sound : ∀n:nat.∀x:R.1 ≤ n → R0 ≤ x → 
227                      PAnd (R0 ≤ (root n x ??)) (x = Rexp_nat (root n x ??) n).
228 try assumption;
229 intros;unfold root;apply (\snd (choose ?? (roots_lemma x n ??)));
230 qed.
231
232 lemma defactorize_O_nfa_zero : ∀x.defactorize x = 0 → x = nfa_zero.
233 intro;elim x
234 [reflexivity
235 |simplify in H;destruct H
236 |simplify in H;cut (∀m.defactorize_aux n m ≠ O)
237  [elim (Hcut ? H)
238  |intro;intro;autobatch]]
239 qed.   
240
241 lemma lt_O_defactorize_numerator : ∀f.0 < defactorize (numerator f).
242 intro;elim f;simplify
243 [rewrite < plus_n_O;rewrite > plus_n_O in ⊢ (?%?);apply lt_plus;
244  apply lt_O_exp;autobatch
245 |autobatch
246 |generalize in match H;generalize in match (not_eq_numerator_nfa_zero f1);
247  cases (numerator f1);intros
248  [elim H1;reflexivity
249  |simplify;cases z;simplify
250   [1,3:autobatch
251   |rewrite < plus_n_O;rewrite > plus_n_O in ⊢ (?%?);
252    apply lt_plus;autobatch depth=2]
253  |simplify;cases z;simplify;
254   [1,3:autobatch
255   |rewrite < plus_n_O;rewrite > (times_n_O O) in ⊢ (?%?);
256    apply lt_times
257    [rewrite > plus_n_O in ⊢ (?%?); apply lt_plus;autobatch
258    |autobatch]]]]
259 qed.
260
261 lemma lt_O_defactorize_denominator : ∀f.O < defactorize (denominator f).
262 intros;unfold denominator;apply lt_O_defactorize_numerator;
263 qed.
264
265 lemma Rexp_nat_pos : ∀x,n.R0 ≤ x → R0 ≤ Rexp_nat x n.
266 intros;elim n;simplify
267 [left;autobatch
268 |cases H
269  [cases H1
270   [left;autobatch
271   |right;rewrite < H3;rewrite > Rtimes_x_R0;reflexivity]
272  |right;rewrite < H2;rewrite > sym_Rtimes;rewrite > Rtimes_x_R0;reflexivity]]
273 qed.
274
275 definition Rexp_Q : ∀x:R.Q → R0 ≤ x → R.
276 apply (λx,q,p.match q with
277  [ OQ ⇒ R1
278  | Qpos r ⇒ match r with
279   [ one ⇒ x
280   | frac f ⇒ root (defactorize (denominator f)) 
281                     (Rexp_nat x (defactorize (numerator f))) 
282                     (lt_O_defactorize_denominator ?) ? ]
283  | Qneg r ⇒ match r with
284   [ one ⇒ Rinv x
285   | frac f ⇒ Rinv (root (defactorize (denominator f)) 
286                     (Rexp_nat x (defactorize (numerator f)))
287                     (lt_O_defactorize_denominator ?) ?) ]]);
288 autobatch;
289 qed.
290
291 lemma Rexp_nat_plus_Rtimes : 
292   ∀x,p,q.Rexp_nat x (p+q) = Rexp_nat x p * Rexp_nat x q.
293 intros;elim q
294 [simplify;autobatch paramodulation
295 |rewrite < sym_plus;simplify;autobatch paramodulation]
296 qed.
297
298 lemma monotonic_Rexp_nat : ∀x,y,n.O < n → R0 ≤ x → x < y → 
299                                   Rexp_nat x n < Rexp_nat y n.
300 intros;elim H;simplify
301 [do 2 rewrite > Rtimes_x_R1;assumption 
302 |apply (trans_Rlt ? (y*Rexp_nat x n1))
303  [rewrite > sym_Rtimes;rewrite > sym_Rtimes in ⊢ (??%);
304   apply Rlt_times_l
305   [assumption
306   |(* already proved, but for ≤: shit! *)elim daemon]
307  |apply Rlt_times_l
308   [assumption
309   |cases H1
310    [autobatch
311    |rewrite > H5;assumption]]]]
312 qed.
313
314 lemma inj_Rexp_nat_l : ∀x,y,n.O < n → R0 ≤ x → R0 ≤ y →
315                          Rexp_nat x n = Rexp_nat y n → x = y.
316 intros;cases (trichotomy_Rlt x y)
317 [cases H4
318  [lapply (monotonic_Rexp_nat ?? n H H1 H5);
319   elim (Rlt_to_neq ?? Hletin H3)
320  |lapply (monotonic_Rexp_nat ?? n H H2 H5);
321   elim (Rlt_to_neq ?? Hletin);symmetry;assumption]
322 |assumption]
323 qed.
324
325 lemma root_unique : ∀x,y,n.R0 ≤ x → R0 ≤ y → O < n → 
326                       Rexp_nat y n = x → y = root n x ? ?.
327 [1,2:assumption
328 |intros;cases (root_sound n x)
329  [2,3:assumption
330  |rewrite > H5 in H3;lapply (inj_Rexp_nat_l ?????? H3);assumption]]
331 qed.
332
333 lemma Rtimes_Rexp_nat : ∀x,y:R.∀p.Rexp_nat x p*Rexp_nat y p = Rexp_nat (x*y) p.
334 intros;elim p;simplify
335 [autobatch paramodulation
336 |rewrite > assoc_Rtimes;rewrite < assoc_Rtimes in ⊢ (? ? (? ? %) ?);
337  rewrite < sym_Rtimes in ⊢ (? ? (? ? (? % ?)) ?);
338  rewrite < H;do 3 rewrite < assoc_Rtimes;reflexivity]
339 qed.
340
341 lemma times_root : ∀x,y,n,H,H1,H2,H3.
342   root n x H H2 * root n y H H3 = root n (x*y) H H1.
343 intros;lapply (Rtimes_Rexp_nat (root n x H H2) (root n y H H3) n);
344 lapply (sym_eq ??? Hletin);
345 cases (root_sound n x)
346 [2,3:assumption
347 |cases (root_sound n y)
348  [2,3:assumption
349  |rewrite < H5 in Hletin1;rewrite < H7 in Hletin1;
350   lapply (root_unique ?????? Hletin1)
351   [assumption
352   |cases H4
353    [cases H6
354     [left;autobatch
355     |right;autobatch paramodulation]
356    |right;autobatch paramodulation]
357   |*:assumption]]]
358 qed.
359
360 lemma Rexp_nat_Rexp_nat_Rtimes : 
361   ∀x,p,q.Rexp_nat (Rexp_nat x p) q = Rexp_nat x (p*q).
362 intros;elim q
363 [rewrite < times_n_O;simplify;reflexivity
364 |rewrite < times_n_Sm;rewrite > Rexp_nat_plus_Rtimes;simplify;
365  rewrite < H;reflexivity]
366 qed. 
367
368 lemma root_root_times : ∀x,n,m,H,H1,H2.root m (root n x H H1) H2 ? =
369                           root (m*n) x ? H1.
370 [cases (root_sound n x H H1);assumption
371 | change in match O with (O*O); apply lt_times; assumption; 
372   (* autobatch paramodulation; non fa narrowing, non fa deep subsumption... *) 
373 |intros;lapply (Rexp_nat_Rexp_nat_Rtimes (root m (root n x H H1) H2 ?) m n)
374  [cases (root_sound n x H H1);assumption
375  |cases (root_sound m (root n x H H1))
376   [2:assumption
377   |3:cases (root_sound n x H H1);assumption
378   |rewrite < H4 in Hletin:(??%?);lapply (root_sound n x H H1);
379    cases Hletin1;rewrite < H6 in Hletin:(??%?);
380    apply root_unique
381    [apply H3
382    |symmetry;apply Hletin]]]]
383 qed.