helm/software/matita/library/R/r.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 "logic/equality.ma".
  16 include "logic/coimplication.ma".
  17 include "logic/cprop_connectives.ma".
  18 include "datatypes/constructors.ma".
  19 include "nat/orders.ma".
  20 include "Z/z.ma".
  21
  22 axiom choose : ∀A:Type.∀P:A → Prop.(∃x.P x) → exP ? P.
  23 alias symbol "plus" = "Disjoint union".
  24 axiom decide : ∀A,B.A ∨ B → A + B.
  25
  26 axiom R : Type.
  27
  28 axiom R0 : R.
  29 axiom R1 : R.
  30
  31 axiom Rplus : R → R → R.
  32 axiom Rtimes : R → R → R.
  33 axiom Ropp : R → R.
  34 axiom Rinv : R → R.
  35 axiom Rlt : R → R → Prop.
  36 definition Rle : R → R → Prop ≝ λx,y:R.Rlt x y ∨ x = y.
  37
  38 interpretation "real numbers" 'R = R.
  39
  40 interpretation "real numbers plus" 'plus x y = (Rplus x y).
  41 interpretation "real numbers times" 'times x y = (Rtimes x y).
  42 interpretation "real numbers opposite" 'uminus x = (Ropp x).
  43 interpretation "real numbers reciprocal" 'invert x = (Rinv x).
  44 interpretation "real numbers less than" 'lt x y = (Rlt x y).
  45 interpretation "real numbers less eq" 'leq x y = (Rle x y).
  46
  47 axiom not_eq_R0_R1 : ¬ R0 = R1.
  48
  49 (* commutative ring with unity *)
  50
  51 axiom sym_Rplus : ∀x,y:R. x + y = y + x.
  52 axiom assoc_Rplus : ∀x,y,z:R.(x+y)+z = x+(y+z).
  53 axiom Rplus_x_R0 : ∀x.x + R0 = x.
  54 axiom Rplus_Ropp : ∀x.x + (-x) = R0.
  55
  56 axiom sym_Rtimes : ∀x,y:R. x * y = y * x.
  57 axiom assoc_Rtimes : ∀x,y,z:R.(x*y)*z = x*(y*z).
  58 axiom Rtimes_x_R1 : ∀x.x * R1 = x.
  59 axiom distr_Rtimes_Rplus_l : ∀x,y,z:R.x*(y+z) = x*y + x*z.
  60
  61 (*pump 200.*)
  62 pump 40.
  63
  64 lemma distr_Rtimes_Rplus_r : ∀x,y,z:R.(x+y)*z = x*z + y*z.
  65 intros; autobatch;
  66 qed.
  67
  68 (* commutative field *)
  69
  70 axiom Rinv_Rtimes_l : ∀x. ¬ x = R0 → x * (Rinv x) = R1.
  71
  72 (* ordered commutative field *)
  73
  74 axiom irrefl_Rlt : ∀x:R.¬ x < x.
  75 axiom asym_Rlt : ∀x,y:R. x < y → ¬ y < x.
  76 axiom trans_Rlt : ∀x,y,z:R.x < y → y < z → x < z.
  77 axiom trichotomy_Rlt : ∀x,y.x < y ∨ y < x ∨ x = y.
  78
  79 lemma trans_Rle : ∀x,y,z:R.x ≤ y → y ≤ z → x ≤ z.
  80 intros;cases H
  81 [cases H1; unfold; autobatch;
  82 |autobatch;]
  83 (*
  84  [left;autobatch
  85  |rewrite < H3;assumption]
  86 |rewrite > H2;assumption]*)
  87 qed.
  88
  89 axiom Rlt_plus_l : ∀z,x,y:R.x < y → z + x < z + y.
  90 axiom Rlt_times_l : ∀z,x,y:R.x < y → R0 < z → z*x < z*y.
  91
  92 (* FIXME: these should be lemmata *)
  93 axiom Rle_plus_l : ∀z,x,y:R.x ≤ y → z + x ≤ z + y.
  94 axiom Rle_times_l : ∀z,x,y:R.x ≤ y → R0 < z → z*x ≤ z*y.
  95
  96 lemma Rle_plus_r : ∀z,x,y:R.x ≤ y → x + z ≤ y + z.
  97 intros; autobatch.
  98 qed.
  99
 100 lemma Rle_times_r : ∀z,x,y:R.x ≤ y → R0 < z → x*z ≤ y*z.
 101 intros;
 102 (* rewrite > sym_Rtimes;rewrite > sym_Rtimes in ⊢ (??%); *)
 103 autobatch;
 104 qed.
 105
 106 (* Dedekind-completeness *)
 107
 108 definition ub ≝ λS: R → Prop.λx:R.∀y.S y → y ≤ x.
 109 definition lub ≝ λS: R → Prop.λx:R.ub S x ∧ ∀y. ub S y → x ≤ y.
 110
 111 axiom R_dedekind : ∀S:R → Prop.(∃x.S x) → (∃x.ub S x) → ∃x.lub S x.
 112
 113 (* coercions *)
 114
 115 definition R_of_nat : nat → R ≝
 116  λn.match n with
 117  [ O ⇒ R0
 118  | S p ⇒ let rec aux m ≝
 119    match m with
 120    [ O ⇒ R1
 121    | S q ⇒ (aux q) + R1] in aux p].
 122
 123 definition R_of_Z ≝
 124 λz.match z with
 125 [ pos n ⇒ R_of_nat (S n)
 126 | neg n ⇒ Ropp (R_of_nat (S n))
 127 | OZ ⇒ R0 ].
 128
 129 (* FIXME!!! coercion clash! *)
 130 coercion R_of_Z.
 131
 132 (*coercion R_of_nat.*)
 133
 134 (* archimedean property *)
 135
 136 axiom R_archimedean : ∀x,y:R.R0 < x → ∃n:nat.y < n*x.
 137
 138 (*definition Rminus : R → R → R ≝
 139  λx,y.x + (-y).*)
 140
 141 interpretation "real numbers minus" 'minus x y = (Rplus x (Ropp y)).
 142 interpretation "real numbers divide" 'divide x y = (Rtimes x (Rinv y)).
 143
 144 (* basic properties *)
 145
 146 (* equality *)
 147
 148 (*
 149 lemma Rplus_eq_l : ∀x,y,z.x = y → z + x= z + y.
 150 intros;autobatch;
 151 qed.
 152
 153 lemma Rplus_eq_r Rtimes_eq_l Rtimes_eq_r analogamente *)
 154
 155 lemma eq_Rplus_l_to_r : ∀a,b,c:R.a+b=c → a = c-b.
 156 intros;lapply (eq_f ? ? (λx:R.x-b) ? ? H);
 157 rewrite > assoc_Rplus in Hletin;rewrite > Rplus_Ropp in Hletin;
 158 rewrite > Rplus_x_R0 in Hletin;assumption;
 159 qed.
 160
 161 lemma eq_Rplus_r_to_l : ∀a,b,c:R.a=b+c → a-c = b.
 162 intros;symmetry;apply eq_Rplus_l_to_r;symmetry;assumption;
 163 qed.
 164
 165 lemma eq_Rminus_l_to_r : ∀a,b,c:R.a-b=c → a = c+b.
 166 intros;lapply (eq_f ? ? (λx:R.x+b) ? ? H);
 167 rewrite > assoc_Rplus in Hletin;rewrite > sym_Rplus in Hletin:(??(??%)?);
 168 rewrite > Rplus_Ropp in Hletin;rewrite > Rplus_x_R0 in Hletin;assumption;
 169 qed.
 170
 171 lemma eq_Rminus_r_to_l : ∀a,b,c:R.a=b-c → a+c = b.
 172 intros;symmetry;apply eq_Rminus_l_to_r;autobatch paramodulation;
 173 qed.
 174
 175 lemma eq_Rtimes_l_to_r : ∀a,b,c:R.b ≠ R0 → a*b=c → a = c/b.
 176 intros;lapply (eq_f ? ? (λx:R.x/b) ? ? H1);
 177 rewrite > assoc_Rtimes in Hletin;rewrite > Rinv_Rtimes_l in Hletin
 178 [rewrite > Rtimes_x_R1 in Hletin;assumption
 179 |assumption]
 180 qed.
 181
 182 lemma eq_Rtimes_r_to_l : ∀a,b,c:R.c ≠ R0 → a=b*c → a/c = b.
 183 intros;symmetry;apply eq_Rtimes_l_to_r
 184 [assumption
 185 |symmetry;assumption]
 186 qed.
 187
 188 lemma eq_Rdiv_l_to_r : ∀a,b,c:R.b ≠ R0 → a/b=c → a = c*b.
 189 intros;lapply (eq_f ? ? (λx:R.x*b) ? ? H1);
 190 rewrite > assoc_Rtimes in Hletin;rewrite > sym_Rtimes in Hletin:(??(??%)?);
 191 rewrite > Rinv_Rtimes_l in Hletin
 192 [rewrite > Rtimes_x_R1 in Hletin;assumption
 193 |assumption]
 194 qed.
 195
 196 lemma eq_Rdiv_r_to_l : ∀a,b,c:R.c ≠ R0 → a=b/c → a*c = b.
 197 intros;symmetry;apply eq_Rdiv_l_to_r
 198 [assumption
 199 |symmetry;assumption]
 200 qed.
 201
 202 (* lemma unique_Ropp : ∀x,y.x + y = R0 → y = -x.
 203 intros;autobatch paramodulation;
 204 qed. *)
 205
 206 lemma Rtimes_x_R0 : ∀x.x * R0 = R0.
 207 (*intro; autobatch paramodulation.*)
 208 intros;
 209 rewrite < Rplus_x_R0 in ⊢ (? ? % ?);
 210 rewrite < (Rplus_Ropp (x*R0)) in ⊢ (? ? (? ? %) %);
 211 rewrite < assoc_Rplus;
 212 apply eq_f2;autobatch paramodulation;
 213
 214 qed.
 215
 216 lemma eq_Rtimes_Ropp_R1_Ropp : ∀x.x*(-R1) = -x.
 217 intro. (*autobatch paramodulation.*)
 218
 219 rewrite < Rplus_x_R0 in ⊢ (? ? % ?);
 220 rewrite < Rplus_x_R0 in ⊢ (? ? ? %);
 221 rewrite < (Rplus_Ropp x) in ⊢ (? ? % ?);
 222 rewrite < assoc_Rplus;
 223 rewrite < sym_Rplus in ⊢ (? ? % ?);
 224 rewrite < sym_Rplus in ⊢ (? ? (? ? %) ?);
 225 apply eq_f2 [reflexivity]
 226 rewrite < Rtimes_x_R1 in ⊢ (? ? (? % ?) ?);
 227 rewrite < distr_Rtimes_Rplus_l;autobatch paramodulation;
 228
 229 qed.
 230
 231 lemma Ropp_inv : ∀x.x = Ropp (Ropp x).
 232 intro;autobatch;
 233 qed.
 234
 235 lemma Rinv_inv : ∀x.x ≠ R0 → x = Rinv (Rinv x).
 236 intros;rewrite < Rtimes_x_R1 in ⊢ (???%);rewrite > sym_Rtimes;
 237 apply eq_Rtimes_l_to_r
 238 [intro;lapply (eq_f ? ? (λy:R.x*y) ? ? H1);
 239  rewrite > Rinv_Rtimes_l in Hletin
 240  [rewrite > Rtimes_x_R0 in Hletin;apply not_eq_R0_R1;symmetry;assumption
 241  |assumption]
 242 |apply Rinv_Rtimes_l;assumption]
 243 qed.
 244
 245 lemma Ropp_R0 : R0 = - R0. demodulate all. (*
 246 rewrite < eq_Rtimes_Ropp_R1_Ropp;autobatch paramodulation; *)
 247 qed.
 248
 249 lemma distr_Ropp_Rplus : ∀x,y:R.-(x + y) = -x -y.
 250 intros; demodulate all; (*rewrite < eq_Rtimes_Ropp_R1_Ropp;
 251 rewrite > sym_Rtimes;rewrite > distr_Rtimes_Rplus_l;
 252 autobatch paramodulation;*)
 253 qed.
 254
 255 lemma Ropp_Rtimes_l : ∀x,y:R.-(x*y) = -x*y.
 256 intros; demodulate all; (*rewrite < eq_Rtimes_Ropp_R1_Ropp;
 257 rewrite > sym_Rtimes;rewrite < assoc_Rtimes;autobatch paramodulation;*)
 258 qed.
 259
 260 lemma Ropp_Rtimes_r : ∀x,y:R.-(x*y) = x*-y.
 261 intros; demodulate all; (*rewrite > sym_Rtimes;rewrite > sym_Rtimes in ⊢ (???%);
 262 autobatch;*)
 263 qed.
 264
 265 (* less than *)
 266
 267 lemma Rlt_to_Rlt_Ropp_Ropp : ∀x,y.x < y → -y < -x.
 268 intros;rewrite < Rplus_x_R0 in ⊢ (??%);
 269 rewrite < (Rplus_Ropp y);rewrite < Rplus_x_R0 in ⊢ (?%?);
 270 rewrite < assoc_Rplus;rewrite < sym_Rplus in ⊢ (??%);
 271 apply Rlt_plus_l;
 272 rewrite < (Rplus_Ropp x);rewrite < sym_Rplus in ⊢ (?%?);autobatch;
 273 qed.
 274
 275 lemma lt_R0_R1 : R0 < R1.
 276 elim (trichotomy_Rlt R0 R1) [|elim (not_eq_R0_R1 H)]
 277 elim H [assumption]
 278 rewrite > Ropp_inv in ⊢ (??%);rewrite < eq_Rtimes_Ropp_R1_Ropp;
 279 rewrite < (Rtimes_x_R0 (-R1));
 280 apply Rlt_times_l;rewrite < (Rtimes_x_R0 (-R1));
 281 rewrite > sym_Rtimes;rewrite > eq_Rtimes_Ropp_R1_Ropp;autobatch;
 282 qed.
 283
 284 lemma pos_z_to_lt_Rtimes_Rtimes_to_lt : ∀x,y,z.R0 < z → z*x < z*y → x < y.
 285 intros;elim (trichotomy_Rlt x y)
 286 [elim H2 [assumption]
 287  elim (asym_Rlt (z*y) (z*x));autobatch
 288 |rewrite > H2 in H1;elim (irrefl_Rlt ? H1)]
 289 qed.
 290
 291 lemma pos_z_to_le_Rtimes_Rtimes_to_lt : ∀x,y,z.R0 < z → z*x ≤ z*y → x ≤ y.
 292 intros;cases H1
 293 [left;autobatch
 294 |right; rewrite < Rtimes_x_R1;rewrite < Rtimes_x_R1 in ⊢ (???%);
 295  rewrite < sym_Rtimes;rewrite < sym_Rtimes in ⊢ (???%);
 296  rewrite < (Rinv_Rtimes_l z)
 297  [demodulate all; (*rewrite < sym_Rtimes in ⊢ (??(?%?)?);rewrite < sym_Rtimes in ⊢ (???(?%?));
 298   autobatch paramodulation*)
 299  |intro;rewrite > H3 in H;apply (irrefl_Rlt R0);assumption]]
 300 qed.
 301
 302 lemma neg_z_to_lt_Rtimes_Rtimes_to_lt : ∀x,y,z.z < R0 → z*x < z*y → y < x.
 303 intros;rewrite > Ropp_inv in ⊢ (?%?);
 304 rewrite > Ropp_inv in ⊢ (??%);
 305 apply Rlt_to_Rlt_Ropp_Ropp;apply (pos_z_to_lt_Rtimes_Rtimes_to_lt ?? (-z))
 306 [rewrite > Ropp_R0;autobatch
 307 |applyS H1; (*
 308  rewrite < (eq_Rtimes_Ropp_R1_Ropp) in ⊢ (?(??%)?);
 309  rewrite < (eq_Rtimes_Ropp_R1_Ropp) in ⊢ (??(??%));
 310  do 2 rewrite < assoc_Rtimes;
 311  rewrite > eq_Rtimes_Ropp_R1_Ropp;
 312  rewrite > eq_Rtimes_Ropp_R1_Ropp in ⊢ (??%);
 313  rewrite > sym_Rtimes;rewrite > sym_Rtimes in ⊢ (??%);
 314  rewrite < (eq_Rtimes_Ropp_R1_Ropp) in ⊢ (?%?);
 315  rewrite < (eq_Rtimes_Ropp_R1_Ropp) in ⊢ (??%);
 316  do 2 rewrite > assoc_Rtimes;
 317  rewrite > eq_Rtimes_Ropp_R1_Ropp;
 318  rewrite < Ropp_inv;
 319  rewrite > sym_Rtimes;rewrite > sym_Rtimes in ⊢ (??%);
 320  assumption*)]
 321 qed.
 322
 323 lemma lt_R0_Rinv : ∀x.R0 < x → R0 < Rinv x.
 324 intros;apply (pos_z_to_lt_Rtimes_Rtimes_to_lt ?? x H);rewrite > Rinv_Rtimes_l;
 325 [rewrite > Rtimes_x_R0;autobatch
 326 |intro;apply (irrefl_Rlt x);rewrite < H1 in H;assumption]
 327 qed.
 328
 329 lemma pos_times_pos_pos : ∀x,y.R0 < x → R0 < y → R0 < x*y.
 330 intros;rewrite < (Rtimes_x_R0 x);autobatch;
 331 qed.
 332
 333 lemma pos_plus_pos_pos : ∀x,y.R0 < x → R0 < y → R0 < x+y.
 334 intros;rewrite < (Rplus_Ropp x);apply Rlt_plus_l;
 335 apply (trans_Rlt ???? H1);rewrite > Ropp_R0;
 336 apply Rlt_to_Rlt_Ropp_Ropp;assumption;
 337 qed.
 338
 339 lemma Rlt_to_neq : ∀x,y:R.x < y → x ≠ y.
 340 intros;intro;rewrite > H1 in H;apply (irrefl_Rlt ? H);
 341 qed.
 342
 343 lemma lt_Rinv : ∀x,y.R0 < x → x < y → Rinv y < Rinv x.
 344 intros;
 345 lapply (Rlt_times_l (Rinv x * Rinv y) ? ? H1)
 346 [ lapply (Rinv_Rtimes_l x);[2: intro; destruct H2; autobatch;]
 347   lapply (Rinv_Rtimes_l y);[2: intro; destruct H2; autobatch;]
 348   cut ((x \sup -1/y*x<x \sup -1/y*y) = (y^-1 < x ^-1));[2:autobatch
 349 (* end auto($Revision: 9716 $) proof: TIME=2.24 SIZE=100 DEPTH=100 *) ;]
 350   rewrite < Hcut; assumption;
 351  (*
 352  rewrite > sym_Rtimes in Hletin;rewrite < assoc_Rtimes in Hletin;
 353  rewrite > assoc_Rtimes in Hletin:(??%);
 354  rewrite > sym_Rtimes in Hletin:(??(??%));
 355  rewrite > Rinv_Rtimes_l in Hletin
 356  [rewrite > Rinv_Rtimes_l in Hletin
 357   [applyS Hletin;(*rewrite > Rtimes_x_R1 in Hletin;rewrite > sym_Rtimes in Hletin;
 358    rewrite > Rtimes_x_R1 in Hletin;assumption*)
 359   |intro;rewrite > H2 in H1;apply (asym_Rlt ? ? H H1)]
 360  |intro;rewrite > H2 in H;apply (irrefl_Rlt ? H)]*)
 361 |apply pos_times_pos_pos;apply lt_R0_Rinv;autobatch]
 362 qed.
 363
 364 lemma Rlt_plus_l_to_r : ∀a,b,c.a + b < c → a < c - b.
 365 intros;
 366 autobatch by H, (Rlt_plus_l (-b) (a+b) c);
 367 (*
 368 rewrite < Rplus_x_R0;rewrite < (Rplus_Ropp b);
 369 rewrite < assoc_Rplus;
 370 rewrite < sym_Rplus;rewrite < sym_Rplus in ⊢ (??%);
 371 apply (Rlt_plus_l (-b) (a+b) c);assumption;
 372 *)
 373 qed.
 374
 375 lemma Rlt_plus_r_to_l : ∀a,b,c.a < b + c → a - c < b.
 376 intros;
 377 rewrite > Ropp_inv;rewrite > Ropp_inv in ⊢ (??%);
 378 apply Rlt_to_Rlt_Ropp_Ropp;rewrite > distr_Ropp_Rplus;
 379 apply Rlt_plus_l_to_r;rewrite < distr_Ropp_Rplus;apply Rlt_to_Rlt_Ropp_Ropp;
 380 assumption;
 381 qed.
 382
 383 lemma Rlt_minus_l_to_r : ∀a,b,c.a - b < c → a < c + b.
 384 intros;rewrite > (Ropp_inv b);apply Rlt_plus_l_to_r;assumption;
 385 qed.
 386
 387 lemma Rlt_minus_r_to_l : ∀a,b,c.a < b - c → a + c < b.
 388 intros;rewrite > (Ropp_inv c);apply Rlt_plus_r_to_l;assumption;
 389 qed.
 390
 391 lemma Rlt_div_r_to_l : ∀a,b,c.R0 < c → a < b/c → a*c < b.
 392 intros;rewrite < sym_Rtimes;
 393 rewrite < Rtimes_x_R1 in ⊢ (??%);rewrite < sym_Rtimes in ⊢ (??%);
 394 rewrite < (Rinv_Rtimes_l c)
 395 [rewrite > assoc_Rtimes;apply Rlt_times_l
 396  [rewrite > sym_Rtimes;assumption
 397  |autobatch]
 398 |intro;elim (Rlt_to_neq ?? H);symmetry;assumption]
 399 qed.
 400
 401 lemma Rlt_times_l_to_r : ∀a,b,c.R0 < b → a*b < c → a < c/b.
 402 intros;rewrite < sym_Rtimes;
 403 rewrite < Rtimes_x_R1;rewrite < sym_Rtimes;
 404 rewrite < (Rinv_Rtimes_l b)
 405 [rewrite < sym_Rtimes in ⊢ (? (? % ?) ?);
 406  rewrite > assoc_Rtimes;apply Rlt_times_l
 407  [rewrite > sym_Rtimes;assumption
 408  |autobatch]
 409 |intro;elim (Rlt_to_neq ?? H);symmetry;assumption]
 410 qed.
 411
 412 lemma Rle_plus_l_to_r : ∀a,b,c.a + b ≤ c → a ≤ c - b.
 413 intros;cases H
 414 [left;autobatch
 415 |right;autobatch]
 416 qed.
 417
 418 lemma Rle_plus_r_to_l : ∀a,b,c.a ≤ b + c → a - c ≤ b.
 419 intros;cases H
 420 [left;autobatch
 421 |right;autobatch]
 422 qed.
 423
 424 lemma Rle_minus_l_to_r : ∀a,b,c.a - b ≤ c → a ≤ c + b.
 425 intros;cases H
 426 [left;autobatch
 427 |right;autobatch]
 428 qed.
 429
 430 lemma Rle_minus_r_to_l : ∀a,b,c.a ≤ b - c → a + c ≤ b.
 431 intros;cases H
 432 [left;autobatch
 433 |right;autobatch]
 434 qed.
 435
 436 lemma R_OF_nat_S : ∀n.R_OF_nat (S n) = R_OF_nat n + R1.
 437 intros;elim n;simplify
 438 [autobatch paramodulation
 439 |reflexivity]
 440 qed.
 441
 442 lemma nat_lt_to_R_lt : ∀m,n:nat.m < n → R_OF_nat m < R_OF_nat n.
 443 intros;elim H
 444 [cases m;simplify
 445  [autobatch
 446  |rewrite < Rplus_x_R0 in ⊢ (?%?);apply Rlt_plus_l;autobatch]
 447 |apply (trans_Rlt ??? H2);cases n1;simplify
 448  [autobatch
 449  |rewrite < Rplus_x_R0 in ⊢ (?%?);apply Rlt_plus_l;autobatch]]
 450 qed.