helm/software/matita/library/R/Rexp.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 "R/root.ma".
  16 include "nat/orders.ma".
  17 include "Z/times.ma".
  18
  19 definition Rexp_Z ≝
  20 λx:R.λy:Z.match y with
  21 [ pos z ⇒ Rexp_nat x (S z)
  22 | neg z ⇒ Rinv (Rexp_nat x (S z))
  23 | OZ ⇒ R1 ].
  24
  25 lemma eq_Rexp_nat_Rexp_Z : ∀x.∀n:nat.Rexp_nat x n = Rexp_Z x n.
  26 intros;cases n;simplify;reflexivity;
  27 qed.
  28
  29 definition expcut : ∀x,y,z:R.Prop ≝
  30   λx,y,z:R.∃p:Z.∃q:nat.∃H1,H2.
  31     z = root q (Rexp_Z x p) H1 H2 ∧ p ≤ (y*q).
  32
  33 axiom Zopp_to_Ropp : ∀z. R_of_Z (Zopp z) = Ropp (R_of_Z z).
  34 axiom distr_Rinv_Rtimes : ∀x,y.x ≠ R0 → y ≠ R0 → Rinv (x*y) = Rinv x * Rinv y.
  35 axiom Rinv_Rexp_nat : ∀n,z. z ≠ R0 → Rinv (Rexp_nat z n) = Rexp_nat (Rinv z) n.
  36
  37 lemma Rexp_nat_R0 : ∀x,n.Rexp_nat x n = R0 → x = R0.
  38 intros 2;elim n
  39 [simplify in H;elim not_eq_R0_R1;symmetry;assumption
  40 |simplify in H1;
  41  cases (trichotomy_Rlt x R0)
  42  [apply H;simplify in H1;cases H2;lapply (Rlt_to_neq ? ? H3);
  43   rewrite < (Rtimes_x_R0 (Rinv x));
  44   rewrite > sym_Rtimes in ⊢ (???%);apply eq_Rtimes_l_to_r
  45   [assumption
  46   |2,4:rewrite > sym_Rtimes;assumption
  47   |intro;apply Hletin;symmetry;assumption]
  48  |assumption]]
  49 qed.
  50
  51 lemma Rexp_Z_Rexp_Z_Rtimes :
  52  ∀x,y,z.x ≠ R0 → Rexp_Z (Rexp_Z x y) z = Rexp_Z x (y*z).
  53 intros;cases y
  54 [simplify;cases z
  55  [reflexivity
  56  |simplify;rewrite > sym_Rtimes;rewrite > Rtimes_x_R1;
  57   elim n
  58   [reflexivity
  59   |simplify;rewrite > sym_Rtimes;rewrite > Rtimes_x_R1;assumption]
  60  |simplify;rewrite > sym_Rtimes;rewrite > Rtimes_x_R1;
  61   elim n;simplify
  62   [rewrite < Rtimes_x_R1;rewrite < sym_Rtimes;
  63    apply Rinv_Rtimes_l;intro;autobatch
  64   |rewrite > sym_Rtimes;rewrite > Rtimes_x_R1;assumption]]
  65 |cases z
  66  [reflexivity
  67  |simplify;change in ⊢ (? ? (? ? (? % ?)) ?) with (Rexp_nat x (S n));
  68   rewrite > Rexp_nat_Rexp_nat_Rtimes;
  69   rewrite > assoc_Rtimes;rewrite < Rexp_nat_plus_Rtimes;do 2 apply eq_f;
  70   rewrite > sym_times in ⊢ (???%); simplify;
  71   do 2 rewrite < assoc_plus;rewrite < sym_plus in ⊢ (? ? (? % ?) ?);
  72   rewrite < sym_times;reflexivity
  73  |simplify;apply eq_f;change in ⊢ (? ? (? ? (? % ?)) ?) with (Rexp_nat x (S n));
  74   rewrite > Rexp_nat_Rexp_nat_Rtimes;
  75   rewrite > assoc_Rtimes;rewrite < Rexp_nat_plus_Rtimes;
  76   do 2 apply eq_f;rewrite > sym_times in ⊢ (???%); simplify;
  77   do 2 rewrite < assoc_plus;rewrite < sym_plus in ⊢ (? ? (? % ?) ?);
  78   rewrite < sym_times;reflexivity]
  79 |cases z
  80  [reflexivity
  81  |simplify;change in ⊢ (? ? (? (? %) (? (? %) ?)) ?) with (Rexp_nat x (S n));
  82   rewrite < Rinv_Rexp_nat
  83   [rewrite < distr_Rinv_Rtimes
  84    [apply eq_f;rewrite > Rexp_nat_Rexp_nat_Rtimes;
  85     rewrite < Rexp_nat_plus_Rtimes;
  86     change in ⊢ (? ? ? %) with (Rexp_nat x (S (n1+n*S n1)));
  87     apply eq_f;autobatch paramodulation
  88    |intro;apply H;apply (Rexp_nat_R0 ?? H1)
  89    |intro;apply H;lapply (Rexp_nat_R0 ?? H1);apply (Rexp_nat_R0 ?? Hletin)]
  90   |intro;apply H;apply (Rexp_nat_R0 ?? H1)]
  91  |simplify;rewrite < Rinv_Rexp_nat
  92   [rewrite < distr_Rinv_Rtimes
  93    [rewrite < Rinv_inv
  94     [change in ⊢ (? ? (? ? (? % ?)) ?) with (Rexp_nat x (S n));
  95      rewrite > Rexp_nat_Rexp_nat_Rtimes;
  96      rewrite > assoc_Rtimes;rewrite < Rexp_nat_plus_Rtimes;
  97      apply eq_f;apply eq_f;rewrite > sym_times in ⊢ (???%); simplify;
  98      do 2 rewrite < assoc_plus;rewrite < sym_plus in ⊢ (? ? (? % ?) ?);
  99      rewrite < sym_times;reflexivity
 100     |intro;apply H;
 101      change in H1:(??%?) with (Rexp_nat (x*Rexp_nat x n) (S n1));
 102      lapply (Rexp_nat_R0 ?? H1);
 103      change in Hletin:(??%?) with (Rexp_nat x (S n));
 104      apply (Rexp_nat_R0 ?? Hletin)]
 105    |intro;apply H;change in H1:(??%?) with (Rexp_nat x (S n));
 106     apply (Rexp_nat_R0 ?? H1)
 107    |intro;apply H;
 108     lapply (Rexp_nat_R0 ?? H1);
 109     change in Hletin:(??%?) with (Rexp_nat x (S n));
 110     apply (Rexp_nat_R0 ?? Hletin)]
 111   |intro;apply H;change in H1:(??%?) with (Rexp_nat x (S n));
 112    apply (Rexp_nat_R0 ?? H1)]]]
 113 qed.
 114
 115 lemma pos_Rexp_nat : ∀x,n.R0 < x → R0 < Rexp_nat x n.
 116 intros;elim n;simplify
 117 [autobatch
 118 |rewrite < (Rtimes_x_R0 x);apply Rlt_times_l;assumption]
 119 qed.
 120
 121 lemma Rexp_nat_R0_Sn : ∀n.Rexp_nat R0 (S n) = R0.
 122 intro;simplify;rewrite > sym_Rtimes;rewrite > Rtimes_x_R0;reflexivity;
 123 qed.
 124
 125 lemma lt_to_lt_Rexp_nat : ∀x,y,n.R0 ≤ x → R0 ≤ y → O < n → x < y →
 126   Rexp_nat x n < Rexp_nat y n.
 127 intros;cases H
 128 [cases H1
 129  [elim H2;simplify
 130   [do 2 rewrite > Rtimes_x_R1;assumption
 131   |apply (trans_Rlt ? (y*Rexp_nat x n1))
 132    [rewrite > sym_Rtimes;rewrite > sym_Rtimes in ⊢ (??%);
 133     apply Rlt_times_l
 134     [assumption
 135     |apply pos_Rexp_nat;assumption]
 136    |apply Rlt_times_l;autobatch]]
 137  |rewrite < H5 in H3;elim (irrefl_Rlt R0);apply (trans_Rlt ? x);assumption]
 138 |cases H1
 139  [rewrite < H4;cases H2;rewrite > Rexp_nat_R0_Sn
 140   [simplify;rewrite > Rtimes_x_R1;assumption
 141   |apply pos_Rexp_nat;assumption]
 142  |elim (irrefl_Rlt x);rewrite < H4 in ⊢ (??%);rewrite > H5;assumption]]
 143 qed.
 144
 145 lemma le_to_le_Rexp_nat : ∀x,y,n.R0 ≤ x → R0 ≤ y → x ≤ y →
 146   Rexp_nat x n ≤ Rexp_nat y n.
 147 intros;elim n
 148 [right;reflexivity
 149 |cases H
 150  [cases H1
 151   [cases H2
 152    [left;apply lt_to_lt_Rexp_nat;autobatch
 153    |rewrite > H6;right;reflexivity]
 154   |rewrite < H5 in H2;elim (irrefl_Rlt R0);cases H2
 155    [apply (trans_Rlt ? x);assumption
 156    |rewrite < H6 in ⊢ (??%);assumption]]
 157  |rewrite < H4;rewrite > Rexp_nat_R0_Sn;cases H1
 158   [left;apply pos_Rexp_nat;assumption
 159   |rewrite < H5;rewrite > Rexp_nat_R0_Sn;right;reflexivity]]]
 160 qed.
 161
 162 lemma inj_Rexp_nat : ∀x,y,n.R0 ≤ x → R0 ≤ y → O < n →
 163   Rexp_nat x n = Rexp_nat y n → x = y.
 164 intros;cases (trichotomy_Rlt x y)
 165 [cases H4
 166  [lapply (lt_to_lt_Rexp_nat ??? H H1 H2 H5);rewrite > H3 in Hletin;
 167   elim (irrefl_Rlt ? Hletin)
 168  |lapply (lt_to_lt_Rexp_nat ??? H1 H H2 H5);rewrite > H3 in Hletin;
 169   elim (irrefl_Rlt ? Hletin)]
 170 |assumption]
 171 qed.
 172
 173 axiom eq_Rinv_Ropp_Ropp_Rinv : ∀x. x ≠ R0 → Rinv (Ropp x) = Ropp (Rinv x).
 174 lemma Rlt_times_r : ∀x,y,z:R.x < y → R0 < z → x*z < y*z.
 175 intros;rewrite < sym_Rtimes;rewrite < sym_Rtimes in ⊢ (??%);
 176 autobatch;
 177 qed.
 178
 179 lemma Rexp_nat_R1 : ∀x.Rexp_nat x 1 = x.
 180 intros;simplify;rewrite > Rtimes_x_R1;reflexivity;
 181 qed.
 182
 183 alias symbol "lt" = "real numbers less than".
 184 lemma Rexp_lemma : ∀x,y:R. R1 < x → ∃z.lub (expcut x y) z.
 185 intros;apply R_dedekind
 186 [unfold expcut;cases (trichotomy_Rlt y R0)
 187  [cases H1
 188   [cases (R_archimedean R1 (Ropp y))
 189    [apply ex_intro[apply (Rexp_Z x (Zopp x1))]
 190     apply ex_intro[apply (Zopp x1)]
 191     apply ex_intro[apply 1]
 192     apply ex_intro[apply le_n]
 193     apply ex_intro
 194     [left;cases x1;simplify
 195      [autobatch
 196      |apply lt_R0_Rinv;change in ⊢(??%) with (Rexp_nat x (S n));
 197       apply pos_Rexp_nat;autobatch]
 198     |split
 199      [cases (root_sound 1 (Rexp_Z x (-x1)))
 200       [rewrite > Rexp_nat_R1 in H5;apply H5
 201       |*:skip]
 202      |simplify;left;rewrite > Rtimes_x_R1;rewrite > Ropp_inv in ⊢ (??%);
 203       lapply (Rlt_to_Rlt_Ropp_Ropp ?? H3);rewrite > Rtimes_x_R1 in Hletin;
 204       rewrite > Zopp_to_Ropp;apply Hletin]]
 205    |autobatch]
 206   |cases (R_archimedean y R1)
 207    [cut (O < x1) [|elim daemon]
 208     cut (R0 ≤ x) [|left;apply (trans_Rlt ???? H);autobatch]
 209     apply ex_intro[apply (root x1 x Hcut Hcut1);assumption]
 210     apply ex_intro[apply (Z_of_nat 1)]
 211     apply ex_intro[apply x1]
 212     apply ex_intro[assumption]
 213     apply ex_intro
 214     [simplify;rewrite > Rtimes_x_R1;assumption
 215     |simplify in ⊢ (? (? ? ? (? ? % ? ?)) ?);
 216      split
 217      [symmetry;cases (root_sound x1 (x*R1) Hcut)
 218       [apply root_unique
 219        [apply H4
 220        |rewrite > Rtimes_x_R1 in H5:(??%?);
 221         symmetry;assumption]
 222       |skip]
 223      |simplify;rewrite > sym_Rtimes;left;assumption]]
 224    |assumption]]
 225  |rewrite > H1;
 226   apply ex_intro
 227   [apply (root 1 (Rexp_Z x OZ))
 228    [autobatch
 229    |simplify;left;autobatch]
 230   |apply ex_intro[apply OZ]
 231    apply ex_intro[apply 1]
 232    apply ex_intro[autobatch]
 233    apply ex_intro[simplify;left;autobatch]
 234    split
 235    [reflexivity
 236    |simplify;rewrite > Rtimes_x_R1;right;reflexivity]]]
 237 |cases (R_archimedean R1 y)
 238  [apply ex_intro[apply (Rexp_Z x x1)]
 239   unfold;intros;unfold in H2;
 240   cases H2;cases H3;cases H4;cases H5;cases H6;
 241   clear H2 H3 H4 H5 H6;
 242   rewrite > Rtimes_x_R1 in H1;
 243   cut (x2 < x1*x3)
 244   [apply (trans_Rle ? (root x3 (Rexp_Z x (x1*x3)) ??))
 245    [assumption
 246    |apply (trans_Rle ??? x5);(*monotonia potenza*)elim daemon
 247    |rewrite > H7;left;
 248     (* monotonia della root *)
 249     elim daemon
 250    |right;elim (root_sound x3 (Rexp_Z (Rexp_Z x x1) x3))
 251     [rewrite < Rexp_Z_Rexp_Z_Rtimes
 252      [apply (inj_Rexp_nat ?? x3)
 253       [apply H2
 254       |left;rewrite < eq_Rexp_nat_Rexp_Z;apply pos_Rexp_nat;
 255        autobatch
 256       |assumption
 257       |symmetry;rewrite > eq_Rexp_nat_Rexp_Z;apply H3]
 258      |intro;rewrite > H4 in H;apply (asym_Rlt ?? H);apply lt_R0_R1]
 259     |*:skip]]
 260   |(*apply Rlt_div_l_to_r manca *) elim daemon]
 261  |autobatch]]
 262 qed.
 263
 264 definition Rexp : ∀x,y:R.R0 < x → R.
 265 intros;cases (decide ? ? (trichotomy_Rlt x R1))
 266 [cases (decide ? ? H1)
 267  [apply (\fst (choose ?? (Rexp_lemma (Rinv x) r ?)));
 268   rewrite < Rtimes_x_R1 in ⊢(??%);rewrite < sym_Rtimes;
 269   apply Rlt_times_l_to_r
 270   [assumption
 271   |rewrite < sym_Rtimes;rewrite > Rtimes_x_R1;assumption]
 272  |apply (\fst (choose ?? (Rexp_lemma x r H2)))]
 273 |apply R1]
 274 qed.
 275
 276 (* testing "decide" axiom
 277 lemma aaa : ∀x,y:R.R1 < x → lub (expcut x y) (Rexp x y ?).
 278 [autobatch
 279 |intros;unfold Rexp;
 280  cases (decide (x<R1∨R1<x) (x=R1) (trichotomy_Rlt x R1))
 281  [simplify;cases (decide (x<R1) (R1<x) H1)
 282   [elim (asym_Rlt ?? H H2)
 283   |simplify;
 284    apply (\snd (choose ℝ (lub (expcut x y)) (Rexp_lemma x y H2)))]
 285   |simplify;rewrite > H1 in H;elim (irrefl_Rlt ? H)]]
 286 qed.*)
 287
 288 interpretation "real numbers exponent" 'exp a b = (Rexp a b _).