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 (to_cotransitive R (of_le R) 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  intros;
  52  unfold;
  53  intros;
  54  exists; [ exact m | ]; (* apply (ex_intro ? ? m); *)
  55  intros;
  56  unfold max_seq;
  57  elim (to_cotransitive R (of_le R) R 0
  58 (inv R (sum_field R (S N))
  59  (not_eq_sum_field_zero R (S N) (le_S_S O N (le_O_n N)))) (x-y)
  60 (lt_zero_to_le_inv_zero R (S N)
  61  (not_eq_sum_field_zero R (S N) (le_S_S O N (le_O_n N)))));
  62   [ simplify;
  63     elim (to_cotransitive R (of_le R) R 0
  64 (inv R (1+sum R (plus R) 0 1 m)
  65  (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))) (x-y)
  66 (lt_zero_to_le_inv_zero R (S m)
  67  (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))));
  68     [ simplify;
  69       rewrite > (plus_comm ? x (-x));
  70       rewrite > opp_inverse;
  71       split;
  72        [ apply (le_zero_x_to_le_opp_x_zero R ?);
  73          apply lt_zero_to_le_inv_zero
  74        | apply lt_zero_to_le_inv_zero
  75        ]
  76     | simplify;
  77       split;
  78        [  apply (to_transitive ? ?
  79        (of_total_order_relation ? ? R) ? 0 ?);
  80          [ apply (le_zero_x_to_le_opp_x_zero R ?)
  81          | assumption
  82          ]
  83        | assumption
  84        ]
  85     ]
  86   | simplify;
  87     elim (to_cotransitive R (of_le R) R 0
  88 (inv R (1+sum R (plus R) 0 1 m)
  89  (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))) (x-y)
  90 (lt_zero_to_le_inv_zero R (S m)
  91  (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))));
  92      [ simplify;
  93        split;
  94        [ elim daemon
  95        | generalize in match (le_zero_x_to_le_opp_x_zero R ? t1);
  96          intro;
  97          unfold minus in H1;
  98          rewrite > eq_opp_plus_plus_opp_opp in H1;
  99          rewrite > eq_opp_opp_x_x in H1;
 100          rewrite > plus_comm in H1;
 101          apply (to_transitive ? ? (of_total_order_relation ? ? R) ? 0 ?);
 102           [ assumption
 103           | apply lt_zero_to_le_inv_zero
 104           ]
 105         ]
 106      | simplify;
 107        rewrite > (plus_comm ? y (-y));
 108        rewrite > opp_inverse;
 109        split;
 110        [ elim daemon
 111        | apply lt_zero_to_le_inv_zero
 112        ]
 113      ]
 114   ].
 115   elim daemon.
 116 qed.
 117
 118 definition max: ∀R:real.R → R → R.
 119  intros (R x y);
 120  apply (lim R (max_seq R x y));
 121  apply cauchy_max_seq.
 122 qed.
 123
 124 definition abs \def λR:real.λx:R. max R x (-x).