matita/dama/ordered_fields_ch0.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/ordered_fields_ch0/".
  16
  17 include "fields.ma".
  18 include "ordered_sets2.ma".
  19
  20 (*CSC: non capisco questi alias! Una volta non servivano*)
  21 alias id "plus" = "cic:/matita/groups/plus.con".
  22 alias symbol "plus" = "Abelian group plus".
  23
  24 record pre_ordered_field_ch0: Type ≝
  25  { of_field:> field;
  26    of_cotransitively_ordered_set_: cotransitively_ordered_set;
  27    of_with: os_carrier of_cotransitively_ordered_set_ = carrier of_field
  28  }.
  29
  30 (*CSC: the following lemma (that is also a coercion) should be automatically
  31   generated *)
  32 lemma of_cotransitively_ordered_set : pre_ordered_field_ch0 → cotransitively_ordered_set.
  33  intro F;
  34  apply mk_cotransitively_ordered_set;
  35  [ apply mk_ordered_set;
  36    [ apply (carrier F)
  37    | apply
  38       (eq_rect ? ? (λC:Type.C→C→Prop) (os_le (of_cotransitively_ordered_set_ F)) ? (of_with F))
  39    | apply
  40       (eq_rect' Type (os_carrier (of_cotransitively_ordered_set_ F))
  41         (λa:Type.λH:os_carrier (of_cotransitively_ordered_set_ F)=a.
  42           is_order_relation a (eq_rect Type (os_carrier (of_cotransitively_ordered_set_ F)) (λC:Type.C→C→Prop) (os_le (of_cotransitively_ordered_set_ F)) a H))
  43         ? (Type_OF_pre_ordered_field_ch0 F) (of_with F));
  44      simplify;
  45      apply (os_order_relation_properties (of_cotransitively_ordered_set_ F))
  46    ]
  47  | simplify;
  48    apply
  49     (eq_rect' ? ?
  50       (λa:Type.λH:os_carrier (of_cotransitively_ordered_set_ F)=a.
  51         cotransitive a
  52          match H in eq
  53           return
  54            λa2:Type.λH1:os_carrier (of_cotransitively_ordered_set_ F)=a2.
  55             a2→a2→Prop
  56          with
  57           [refl_eq ⇒ os_le (of_cotransitively_ordered_set_ F)])
  58       ? ? (of_with F));
  59    simplify;
  60    apply cos_cotransitive
  61  ].
  62 qed.
  63
  64 coercion cic:/matita/ordered_fields_ch0/of_cotransitively_ordered_set.con.
  65
  66 record is_ordered_field_ch0 (F:pre_ordered_field_ch0) : Type \def
  67  { of_mult_compat: ∀a,b:F. 0≤a → 0≤b → 0≤a*b;
  68    of_plus_compat: ∀a,b,c:F. a≤b → a+c≤b+c;
  69    of_weak_tricotomy : ∀a,b:F. a≠b → a≤b ∨ b≤a;
  70    (* 0 characteristics *)
  71    of_char0: ∀n. n > O → sum ? (plus F) 0 1 n ≠ 0
  72  }.
  73
  74 record ordered_field_ch0 : Type \def
  75  { of_pre_ordered_field_ch0:> pre_ordered_field_ch0;
  76    of_ordered_field_properties:> is_ordered_field_ch0 of_pre_ordered_field_ch0
  77  }.
  78
  79 lemma le_zero_x_to_le_opp_x_zero: ∀F:ordered_field_ch0.∀x:F.0 ≤ x → -x ≤ 0.
  80  intros;
  81  generalize in match (of_plus_compat ? F ? ? (-x) H); intro;
  82  rewrite > zero_neutral in H1;
  83  rewrite > plus_comm in H1;
  84  rewrite > opp_inverse in H1;
  85  assumption.
  86 qed.
  87
  88 lemma le_x_zero_to_le_zero_opp_x: ∀F:ordered_field_ch0.∀x:F. x ≤ 0 → 0 ≤ -x.
  89  intros;
  90  generalize in match (of_plus_compat ? F ? ? (-x) H); intro;
  91  rewrite > zero_neutral in H1;
  92  rewrite > plus_comm in H1;
  93  rewrite > opp_inverse in H1;
  94  assumption.
  95 qed.
  96
  97 (*
  98 lemma eq_opp_x_times_opp_one_x: ∀F:ordered_field_ch0.∀x:F.-x = -1*x.
  99  intros;
 100
 101 lemma not_eq_x_zero_to_lt_zero_mult_x_x:
 102  ∀F:ordered_field_ch0.∀x:F. x ≠ 0 → 0 < x * x.
 103  intros;
 104  elim (of_weak_tricotomy ? ? ? ? ? ? ? ? F ? ? H);
 105   [ generalize in match (le_x_zero_to_le_zero_opp_x F ? H1); intro;
 106     generalize in match (of_mult_compat ? ? ? ? ? ? ? ?  F ? ? H2 H2); intro;
 107 *)
 108
 109 axiom lt_zero_to_lt_inv_zero:
 110  ∀F:ordered_field_ch0.∀x:F.∀p:x≠0. lt F 0 x → lt F 0 (inv ? x p).
 111
 112 alias symbol "lt" = "natural 'less than'".
 113
 114 (* The ordering is not necessary. *)
 115 axiom not_eq_sum_field_zero: ∀F:ordered_field_ch0.∀n. O<n → sum_field F n ≠ 0.
 116 axiom le_zero_sum_field: ∀F:ordered_field_ch0.∀n. O<n → lt F 0 (sum_field F n).
 117
 118 axiom lt_zero_to_le_inv_zero:
 119  ∀F:ordered_field_ch0.∀n:nat.∀p:sum_field F n ≠ 0. 0 ≤ inv ? (sum_field ? n) p.
 120
 121 definition tends_to : ∀F:ordered_field_ch0.∀f:nat→F.∀l:F.Prop.
 122  apply
 123   (λF:ordered_field_ch0.λf:nat → F.λl:F.
 124     ∀n:nat.∃m:nat.∀j:nat.m ≤ j →
 125      l - (inv F (sum_field ? (S n)) ?) ≤ f j ∧
 126      f j ≤ l + (inv F (sum_field ? (S n)) ?));
 127  apply not_eq_sum_field_zero;
 128  unfold;
 129  auto new.
 130 qed.
 131
 132 (*
 133 definition is_cauchy_seq ≝
 134  λF:ordered_field_ch0.λf:nat→F.
 135   ∀eps:F. 0 < eps →
 136    ∃n:nat.∀M. n ≤ M →
 137     -eps ≤ f M - f n ∧ f M - f n ≤ eps.
 138 *)
 139
 140
 141
 142 definition is_cauchy_seq : ∀F:ordered_field_ch0.∀f:nat→F.Prop.
 143  apply
 144   (λF:ordered_field_ch0.λf:nat→F.
 145     ∀m:nat.
 146      ∃n:nat.∀N.n ≤ N →
 147       -(inv ? (sum_field F (S m)) ?) ≤ f N - f n ∧
 148       f N - f n ≤ inv ? (sum_field F (S m)) ?);
 149  apply not_eq_sum_field_zero;
 150  unfold;
 151  auto.
 152 qed.
 153
 154 definition is_complete ≝
 155  λF:ordered_field_ch0.
 156   ∀f:nat→F. is_cauchy_seq ? f →
 157    ex F (λl:F. tends_to ? f l).