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;
 132        [ unfold lt; change in H1 with (O < n);
 133          autobatch; (*applyS H1;*)
 134        | assumption;
 135        | elim daemon; ]]
 136       (*
 137       rewrite > assoc_Rtimes;rewrite > sym_Rtimes in ⊢ (??(??%));
 138       rewrite < assoc_Rtimes;apply Rexp_nat_tech
 139       [autobatch
 140       |assumption
 141       |(* by transitivity y^n < x < a^n and injectivity *) elim daemon]]*)
 142     |intro;apply (irrefl_Rlt (n*Rexp_nat a (n-1)));
 143      rewrite > H11 in ⊢ (?%?);apply pos_times_pos_pos
 144      [apply (nat_lt_to_R_lt ?? H1);
 145      |elim daemon]]]]
 146 |elim (R_archimedean R1 ((x-Rexp_nat a n)/(n*Rexp_nat (a+1) (n-1))))
 147  [|autobatch]
 148  rewrite > Rtimes_x_R1 in H8;
 149  letin h ≝ ((x-Rexp_nat a n)/(n*Rexp_nat (a+1) (n-1)*a1));
 150  lapply (H4 (a+h))
 151   [rewrite < Rplus_x_R0 in Hletin:(??%);rewrite < sym_Rplus in Hletin:(??%);
 152    lapply (Rle_plus_r_to_l ? ? ? Hletin);
 153    rewrite > sym_Rplus in Hletin1:(?(?%?)?);rewrite > assoc_Rplus in Hletin1;
 154    rewrite > Rplus_Ropp in Hletin1;rewrite > Rplus_x_R0 in Hletin1;
 155    unfold h in Hletin1;
 156    cut (R0 < (x-Rexp_nat a n)/(n*Rexp_nat (a+1) (n-1)*a1))
 157    [cases Hletin1
 158     [elim (asym_Rlt ? ? Hcut1 H9)
 159     |rewrite > H9 in Hcut1;elim (irrefl_Rlt ? Hcut1)]
 160    |apply pos_times_pos_pos
 161     [apply Rlt_plus_l_to_r;rewrite > sym_Rplus;rewrite > Rplus_x_R0;
 162      assumption
 163     |apply lt_R0_Rinv;apply pos_times_pos_pos
 164      [apply pos_times_pos_pos
 165       [apply (nat_lt_to_R_lt ?? H1);
 166       |elim daemon]
 167      |apply (trans_Rlt ???? H8);apply pos_times_pos_pos
 168       [apply Rlt_plus_l_to_r;rewrite > sym_Rplus;rewrite > Rplus_x_R0;
 169        assumption
 170       |apply lt_R0_Rinv;apply pos_times_pos_pos
 171        [apply (nat_lt_to_R_lt ?? H1);
 172        |elim daemon]]]]]
 173   |split
 174    [(* show that h > R0, also useful in previous parts of the proof *)
 175     elim daemon
 176    |(* by monotonicity ov Rexp_nat *) elim daemon]]]
 177 |apply ex_intro[apply (x/(x+R1))]
 178  unfold bound;simplify;split
 179  [apply pos_times_pos_pos
 180   [assumption
 181   |apply lt_R0_Rinv;apply pos_plus_pos_pos
 182    [assumption
 183    |autobatch]]
 184  |apply (trans_Rlt ? (x/(x+R1)))
 185   [(* antimonotone exponential with base in [0,1] *) elim daemon
 186   |rewrite < Rtimes_x_R1 in ⊢ (??%);
 187    apply Rlt_times_l
 188    [rewrite < (Rinv_Rtimes_l R1)
 189     [rewrite > sym_Rtimes in ⊢ (??%);rewrite > Rtimes_x_R1;
 190      apply lt_Rinv
 191      [autobatch
 192      |rewrite > Rinv_Rtimes_l
 193       [apply Rlt_minus_l_to_r;rewrite > Rplus_Ropp;assumption
 194       |intro;elim not_eq_R0_R1;symmetry;assumption]]
 195     |intro;elim not_eq_R0_R1;symmetry;assumption]
 196    |assumption]]]
 197 |apply ex_intro[apply (x+R1)]
 198  unfold ub;intros;unfold in H3;elim H3;cases (trichotomy_Rlt y (x+R1))
 199  [cases H6
 200   [left;assumption
 201   |elim (asym_Rlt (Rexp_nat y n) x)
 202    [assumption
 203    |apply (trans_Rlt ? y)
 204      [apply (trans_Rlt ???? H7);rewrite > sym_Rplus;
 205       apply Rlt_minus_l_to_r;rewrite > Rplus_Ropp;autobatch
 206     |(* monotonia; il caso n=1 andra` facilmente gestito a parte *)
 207      elim daemon]]]
 208  |right;assumption]]
 209 |apply ex_intro[apply R0]
 210  split
 211  [right;reflexivity
 212  |rewrite < H2;elim H1;
 213   simplify;rewrite > sym_Rtimes;rewrite > Rtimes_x_R0;reflexivity]]
 214 qed.
 215
 216 definition root : ∀n:nat.∀x:R.O < n → R0 ≤ x → R.
 217 intros;apply (\fst (choose ?? (roots_lemma x n ??)));assumption;
 218 qed.
 219
 220 notation < "hvbox(maction (\root mstyle scriptlevel 1(term 19 n)
 221          \of (term 19 x)) ((\root n \of x)\sub(h,k)))"
 222  with precedence 90 for @{ 'aroot $n $x $h $k}.
 223
 224 interpretation "real numbers root" 'aroot n x h k = (root n x h k).
 225
 226 (* FIXME: qui non c'e` modo di far andare la notazione...*)
 227 (*lemma root_sound : ∀n:nat.∀x:R.1 ≤ n → R0 ≤ x →
 228                      R0 ≤ (root n x ??) ∧ x = Rexp_nat (root n x ??) n.*)
 229 alias id "PAnd" = "cic:/matita/logic/connectives/And.ind#xpointer(1/1)".
 230
 231 lemma root_sound : ∀n:nat.∀x:R.1 ≤ n → R0 ≤ x →
 232                      PAnd (R0 ≤ (root n x ??)) (x = Rexp_nat (root n x ??) n).
 233 try assumption;
 234 intros;unfold root;apply (\snd (choose ?? (roots_lemma x n ??)));
 235 qed.
 236
 237 lemma defactorize_O_nfa_zero : ∀x.defactorize x = 0 → x = nfa_zero.
 238 intro;elim x
 239 [reflexivity
 240 |simplify in H;destruct H
 241 |simplify in H;cut (∀m.defactorize_aux n m ≠ O)
 242  [elim (Hcut ? H)
 243  |intro;intro;autobatch]]
 244 qed.
 245
 246 lemma lt_O_defactorize_numerator : ∀f.0 < defactorize (numerator f).
 247 intro;elim f;simplify
 248 [rewrite < plus_n_O;rewrite > plus_n_O in ⊢ (?%?);apply lt_plus;
 249  apply lt_O_exp;autobatch
 250 |autobatch
 251 |generalize in match H;generalize in match (not_eq_numerator_nfa_zero f1);
 252  cases (numerator f1);intros
 253  [elim H1;reflexivity
 254  |simplify;cases z;simplify
 255   [1,3:autobatch
 256   |rewrite < plus_n_O;rewrite > plus_n_O in ⊢ (?%?);
 257    apply lt_plus;autobatch]
 258  |simplify;cases z;simplify;
 259   [1,3:autobatch
 260   |rewrite < plus_n_O;rewrite > (times_n_O O) in ⊢ (?%?);
 261    apply lt_times
 262    [rewrite > plus_n_O in ⊢ (?%?); apply lt_plus;autobatch
 263    |autobatch]]]]
 264 qed.
 265
 266 lemma lt_O_defactorize_denominator : ∀f.O < defactorize (denominator f).
 267 intros;unfold denominator;apply lt_O_defactorize_numerator;
 268 qed.
 269
 270 lemma Rexp_nat_pos : ∀x,n.R0 ≤ x → R0 ≤ Rexp_nat x n.
 271 intros;elim n;simplify
 272 [left;autobatch
 273 |cases H
 274  [cases H1
 275   [left;autobatch
 276   |right;rewrite < H3;rewrite > Rtimes_x_R0;reflexivity]
 277  |right;rewrite < H2;rewrite > sym_Rtimes;rewrite > Rtimes_x_R0;reflexivity]]
 278 qed.
 279
 280 definition Rexp_Q : ∀x:R.Q → R0 ≤ x → R.
 281 apply (λx,q,p.match q with
 282  [ OQ ⇒ R1
 283  | Qpos r ⇒ match r with
 284   [ one ⇒ x
 285   | frac f ⇒ root (defactorize (denominator f))
 286                     (Rexp_nat x (defactorize (numerator f)))
 287                     (lt_O_defactorize_denominator ?) ? ]
 288  | Qneg r ⇒ match r with
 289   [ one ⇒ Rinv x
 290   | frac f ⇒ Rinv (root (defactorize (denominator f))
 291                     (Rexp_nat x (defactorize (numerator f)))
 292                     (lt_O_defactorize_denominator ?) ?) ]]);
 293 autobatch;
 294 qed.
 295
 296 lemma Rexp_nat_plus_Rtimes :
 297   ∀x,p,q.Rexp_nat x (p+q) = Rexp_nat x p * Rexp_nat x q.
 298 intros;elim q
 299 [simplify;autobatch paramodulation
 300 |rewrite < sym_plus;simplify;autobatch paramodulation]
 301 qed.
 302
 303 lemma monotonic_Rexp_nat : ∀x,y,n.O < n → R0 ≤ x → x < y →
 304                                   Rexp_nat x n < Rexp_nat y n.
 305 intros;elim H;simplify
 306 [do 2 rewrite > Rtimes_x_R1;assumption
 307 |apply (trans_Rlt ? (y*Rexp_nat x n1))
 308  [rewrite > sym_Rtimes;rewrite > sym_Rtimes in ⊢ (??%);
 309   apply Rlt_times_l
 310   [assumption
 311   |(* already proved, but for ≤: shit! *)elim daemon]
 312  |apply Rlt_times_l
 313   [assumption
 314   |cases H1
 315    [autobatch
 316    |rewrite > H5;assumption]]]]
 317 qed.
 318
 319 lemma inj_Rexp_nat_l : ∀x,y,n.O < n → R0 ≤ x → R0 ≤ y →
 320                          Rexp_nat x n = Rexp_nat y n → x = y.
 321 intros;cases (trichotomy_Rlt x y)
 322 [cases H4
 323  [lapply (monotonic_Rexp_nat ?? n H H1 H5);
 324   elim (Rlt_to_neq ?? Hletin H3)
 325  |lapply (monotonic_Rexp_nat ?? n H H2 H5);
 326   elim (Rlt_to_neq ?? Hletin);symmetry;assumption]
 327 |assumption]
 328 qed.
 329
 330 lemma root_unique : ∀x,y,n.R0 ≤ x → R0 ≤ y → O < n →
 331                       Rexp_nat y n = x → y = root n x ? ?.
 332 [1,2:assumption
 333 |intros;cases (root_sound n x)
 334  [2,3:assumption
 335  |rewrite > H5 in H3;lapply (inj_Rexp_nat_l ?????? H3);assumption]]
 336 qed.
 337
 338 lemma Rtimes_Rexp_nat : ∀x,y:R.∀p.Rexp_nat x p*Rexp_nat y p = Rexp_nat (x*y) p.
 339 intros;elim p;simplify
 340 [autobatch paramodulation
 341 |rewrite > assoc_Rtimes;rewrite < assoc_Rtimes in ⊢ (? ? (? ? %) ?);
 342  rewrite < sym_Rtimes in ⊢ (? ? (? ? (? % ?)) ?);
 343  rewrite < H;do 3 rewrite < assoc_Rtimes;reflexivity]
 344 qed.
 345
 346 lemma times_root : ∀x,y,n,H,H1,H2,H3.
 347   root n x H H2 * root n y H H3 = root n (x*y) H H1.
 348 intros;lapply (Rtimes_Rexp_nat (root n x H H2) (root n y H H3) n);
 349 lapply (sym_eq ??? Hletin);
 350 cases (root_sound n x)
 351 [2,3:assumption
 352 |cases (root_sound n y)
 353  [2,3:assumption
 354  |rewrite < H5 in Hletin1;rewrite < H7 in Hletin1;
 355   lapply (root_unique ?????? Hletin1)
 356   [assumption
 357   |cases H4
 358    [cases H6
 359     [left;autobatch
 360     |right;autobatch paramodulation]
 361    |right;autobatch paramodulation]
 362   |*:assumption]]]
 363 qed.
 364
 365 lemma Rexp_nat_Rexp_nat_Rtimes :
 366   ∀x,p,q.Rexp_nat (Rexp_nat x p) q = Rexp_nat x (p*q).
 367 intros;elim q
 368 [rewrite < times_n_O;simplify;reflexivity
 369 |rewrite < times_n_Sm;rewrite > Rexp_nat_plus_Rtimes;simplify;
 370  rewrite < H;reflexivity]
 371 qed.
 372
 373 lemma root_root_times : ∀x,n,m,H,H1,H2.root m (root n x H H1) H2 ? =
 374                           root (m*n) x ? H1.
 375 [cases (root_sound n x H H1);assumption
 376 | change in match O with (O*O); apply lt_times; assumption;
 377   (* autobatch paramodulation; non fa narrowing, non fa deep subsumption... *)
 378 |intros;lapply (Rexp_nat_Rexp_nat_Rtimes (root m (root n x H H1) H2 ?) m n)
 379  [cases (root_sound n x H H1);assumption
 380  |cases (root_sound m (root n x H H1))
 381   [2:assumption
 382   |3:cases (root_sound n x H H1);assumption
 383   |rewrite < H4 in Hletin:(??%?);lapply (root_sound n x H H1);
 384    cases Hletin1;rewrite < H6 in Hletin:(??%?);
 385    apply root_unique
 386    [apply H3
 387    |symmetry;apply Hletin]]]]
 388 qed.