helm/software/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 F 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 (* serve l'esistenziale in CProp!
  31 definition lim: ∀R:real.∀f:nat→R.is_cauchy_seq R f → R.
  32  intros;
  33  elim H;
  34 qed.
  35 *)
  36
  37 definition max_seq: ∀R:real.∀x,y:R. nat → R.
  38  intros (R x y);
  39  elim (to_cotransitive R (of_le R) R 0 (inv ? (sum_field R (S n)) ?) (x-y));
  40   [ apply x
  41   | apply not_eq_sum_field_zero ;
  42     unfold;
  43     auto new
  44   | apply y
  45   | apply lt_zero_to_le_inv_zero
  46   ].
  47 qed.
  48
  49 axiom daemon: False.
  50
  51 theorem cauchy_max_seq: ∀R:real.∀x,y. is_cauchy_seq ? (max_seq R x y).
  52  intros;
  53  unfold;
  54  intros;
  55  exists; [ exact m | ]; (* apply (ex_intro ? ? m); *)
  56  intros;
  57  unfold max_seq;
  58  elim (to_cotransitive R (of_le R) R 0
  59 (inv R (sum_field R (S N))
  60  (not_eq_sum_field_zero R (S N) (le_S_S O N (le_O_n N)))) (x-y)
  61 (lt_zero_to_le_inv_zero R (S N)
  62  (not_eq_sum_field_zero R (S N) (le_S_S O N (le_O_n N)))));
  63   [ simplify;
  64     elim (to_cotransitive R (of_le R) R 0
  65 (inv R (1+sum R (plus R) 0 1 m)
  66  (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))) (x-y)
  67 (lt_zero_to_le_inv_zero R (S m)
  68  (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))));
  69     [ simplify;
  70       rewrite > (plus_comm ? x (-x));
  71       rewrite > opp_inverse;
  72       split;
  73        [ elim daemon (* da finire *)
  74        | apply lt_zero_to_le_inv_zero
  75        ]
  76     | simplify;
  77       split;
  78        [ elim daemon (* da finire *)
  79        | assumption
  80        ]
  81     ]
  82   | simplify;
  83     elim (to_cotransitive R (of_le R) R 0
  84 (inv R (1+sum R (plus R) 0 1 m)
  85  (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))) (x-y)
  86 (lt_zero_to_le_inv_zero R (S m)
  87  (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))));
  88      [ simplify;
  89        split;
  90        [ elim daemon (* da finire *)
  91        | generalize in match (le_zero_x_to_le_opp_x_zero R ? t1);
  92          intro;
  93          unfold minus in H1;
  94          rewrite > eq_opp_plus_plus_opp_opp in H1;
  95          rewrite > eq_opp_opp_x_x in H1;
  96          rewrite > plus_comm in H1;
  97          apply (to_transitive ? ? (of_total_order_relation ? ? R) ? 0 ?);
  98           [ assumption
  99           | apply lt_zero_to_le_inv_zero
 100           ]
 101         ]
 102      | simplify;
 103        rewrite > (plus_comm ? y (-y));
 104        rewrite > opp_inverse;
 105        split;
 106        [ elim daemon (* da finire *)
 107        | apply lt_zero_to_le_inv_zero
 108        ]
 109      ]
 110   ].
 111 qed.
 112
 113 definition max: ∀R:real.R → R → R.
 114  intros (R x y);
 115  elim (r_complete ? (r_real_properties R) ? ?);
 116   [|| apply (cauchy_max_seq R x y) ]
 117 qed.
 118