matita/dama/reals.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 set "baseuri" "cic:/matita/reals/".
  16
  17 include "ordered_fields_ch0.ma".
  18
  19 record is_real (F:ordered_field_ch0) : Type
  20 ≝
  21  { r_archimedean: ∀x:F. ∃n:nat. x ≤ (sum_field ? n);
  22    r_complete: is_complete F
  23  }.
  24
  25 record real: Type \def
  26  { r_ordered_field_ch0:> ordered_field_ch0;
  27    r_real_properties: is_real r_ordered_field_ch0
  28  }.
  29
  30 definition lim: ∀R:real.∀f:nat→R.is_cauchy_seq ? f → R.
  31  intros;
  32  elim (r_complete ? (r_real_properties R) ? H);
  33  exact a.
  34 qed.
  35
  36 definition max_seq: ∀R:real.∀x,y:R. nat → R.
  37  intros (R x y);
  38  elim (cos_cotransitive R 0 (inv ? (sum_field ? (S n)) ?) (x-y));
  39   [ apply x
  40   | apply not_eq_sum_field_zero ;
  41     unfold;
  42     auto new
  43   | apply y
  44   | apply lt_zero_to_le_inv_zero
  45   ].
  46 qed.
  47
  48 axiom daemon: False.
  49
  50 theorem cauchy_max_seq: ∀R:real.∀x,y:R. is_cauchy_seq ? (max_seq ? x y).
  51 elim daemon.
  52 (*
  53  intros;
  54  unfold;
  55  intros;
  56  exists; [ exact m | ]; (* apply (ex_intro ? ? m); *)
  57  intros;
  58  unfold max_seq;
  59  elim (of_cotransitive R 0
  60 (inv R (sum_field R (S N))
  61  (not_eq_sum_field_zero R (S N) (le_S_S O N (le_O_n N)))) (x-y)
  62 (lt_zero_to_le_inv_zero R (S N)
  63  (not_eq_sum_field_zero R (S N) (le_S_S O N (le_O_n N)))));
  64   [ simplify;
  65     elim (of_cotransitive R  0
  66 (inv R (1+sum R (plus R) 0 1 m)
  67  (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))) (x-y)
  68 (lt_zero_to_le_inv_zero R (S m)
  69  (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))));
  70     [ simplify;
  71       rewrite > (plus_comm ? x (-x));
  72       rewrite > opp_inverse;
  73       split;
  74        [ apply (le_zero_x_to_le_opp_x_zero R ?);
  75          apply lt_zero_to_le_inv_zero
  76        | apply lt_zero_to_le_inv_zero
  77        ]
  78     | simplify;
  79       split;
  80        [ apply (or_transitive ? ? R ? 0);
  81           [ apply (le_zero_x_to_le_opp_x_zero R ?)
  82           | assumption
  83           ]
  84        | assumption
  85        ]
  86     ]
  87   | simplify;
  88     elim (of_cotransitive R 0
  89 (inv R (1+sum R (plus R) 0 1 m)
  90  (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))) (x-y)
  91 (lt_zero_to_le_inv_zero R (S m)
  92  (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))));
  93      [ simplify;
  94        split;
  95        [ elim daemon
  96        | generalize in match (le_zero_x_to_le_opp_x_zero R ? t1);
  97          intro;
  98          unfold minus in H1;
  99          rewrite > eq_opp_plus_plus_opp_opp in H1;
 100          rewrite > eq_opp_opp_x_x in H1;
 101          rewrite > plus_comm in H1;
 102          apply (or_transitive ? ? R ? 0);
 103           [ assumption
 104           | apply lt_zero_to_le_inv_zero
 105           ]
 106         ]
 107      | simplify;
 108        rewrite > (plus_comm ? y (-y));
 109        rewrite > opp_inverse;
 110        split;
 111        [ elim daemon
 112        | apply lt_zero_to_le_inv_zero
 113        ]
 114      ]
 115   ].
 116   elim daemon.*)
 117 qed.
 118
 119 definition max: ∀R:real.R → R → R.
 120  intros (R x y);
 121  apply (lim R (max_seq R x y));
 122  apply cauchy_max_seq.
 123 qed.
 124
 125 definition abs \def λR:real.λx:R. max R x (-x).
 126
 127 lemma comparison:
 128  ∀R:real.∀f,g:nat→R. is_cauchy_seq ? f → is_cauchy_seq ? g →
 129   (∀n:nat.f n ≤ g n) → lim ? f ? ≤ lim ? g ?.
 130  [ assumption
 131  | assumption
 132  | intros;
 133    elim daemon
 134  ].
 135 qed.
 136
 137 definition to_zero ≝
 138  λR:real.λn.
 139   -(inv R (sum_field R (S n))
 140    (not_eq_sum_field_zero R (S n) (le_S_S O n (le_O_n n)))).
 141
 142 axiom is_cauchy_seq_to_zero: ∀R:real. is_cauchy_seq ? (to_zero R).
 143
 144 lemma technical1: ∀R:real.lim R (to_zero R) (is_cauchy_seq_to_zero R) = 0.
 145  intros;
 146  unfold lim;
 147  elim daemon.
 148 qed.
 149
 150 lemma abs_x_ge_O: ∀R:real.∀x:R. 0 ≤ abs ? x.
 151  intros;
 152  unfold abs;
 153  unfold max;
 154  rewrite < technical1;
 155  apply comparison;
 156  intros;
 157  unfold to_zero;
 158  unfold max_seq;
 159  elim
 160      (cos_cotransitive R 0
 161 (inv R (sum_field R (S n))
 162  (not_eq_sum_field_zero R (S n) (le_S_S O n (le_O_n n)))) (x--x)
 163 (lt_zero_to_le_inv_zero R (S n)
 164  (not_eq_sum_field_zero R (S n) (le_S_S O n (le_O_n n)))));
 165  [ simplify;
 166    (* facile *)
 167    elim daemon
 168  | simplify;
 169    (* facile *)
 170    elim daemon
 171  ].
 172 qed.