helm/software/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.