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
  19 record is_total_order_relation (C:Type) (le:C→C→Prop) : Type \def
  20  { to_cotransitive: ∀x,y,z:C. le x y → le x z ∨ le z y;
  21    to_antisimmetry: ∀x,y:C. le x y → le y x → x=y
  22  }.
  23
  24 theorem to_transitive: ∀C,le. is_total_order_relation C le → transitive ? le.
  25  intros;
  26  unfold transitive;
  27  intros;
  28  elim (to_cotransitive ? ? i ? ? z H);
  29   [ assumption
  30   | rewrite < (to_antisimmetry ? ? i ? ? H1 t);
  31     assumption
  32   ].
  33 qed.
  34
  35 record is_ordered_field_ch0 (F:field) (le:F→F→Prop) : Type \def
  36  { of_total_order_relation:> is_total_order_relation ? le;
  37    of_mult_compat: ∀a,b. le 0 a → le 0 b → le 0 (a*b);
  38    of_plus_compat: ∀a,b,c. le a b → le (a+c) (b+c);
  39    of_weak_tricotomy : ∀a,b. a≠b → le a b ∨ le b a;
  40    (* 0 characteristics *)
  41    of_char0: ∀n. n > O → sum ? (plus F) 0 1 n ≠ 0
  42  }.
  43
  44 record ordered_field_ch0 : Type \def
  45  { of_field:> field;
  46    of_le: of_field → of_field → Prop;
  47    of_ordered_field_properties:> is_ordered_field_ch0 of_field of_le
  48  }.
  49
  50 interpretation "Ordered field le" 'leq a b =
  51  (cic:/matita/ordered_fields_ch0/of_le.con _ a b).
  52
  53 definition lt \def λF:ordered_field_ch0.λa,b:F.a ≤ b ∧ a ≠ b.
  54
  55 interpretation "Ordered field lt" 'lt a b =
  56  (cic:/matita/ordered_fields_ch0/lt.con _ a b).
  57
  58 lemma le_zero_x_to_le_opp_x_zero: ∀F:ordered_field_ch0.∀x:F. 0 ≤ x → -x ≤ 0.
  59 intros;
  60  generalize in match (of_plus_compat ? ? F ? ? (-x) H); intro;
  61  rewrite > zero_neutral in H1;
  62  rewrite > plus_comm in H1;
  63  rewrite > opp_inverse in H1;
  64  assumption.
  65 qed.
  66
  67 lemma le_x_zero_to_le_zero_opp_x: ∀F:ordered_field_ch0.∀x:F. x ≤ 0 → 0 ≤ -x.
  68  intros;
  69  generalize in match (of_plus_compat ? ? F ? ? (-x) H); intro;
  70  rewrite > zero_neutral in H1;
  71  rewrite > plus_comm in H1;
  72  rewrite > opp_inverse in H1;
  73  assumption.
  74 qed.
  75
  76 (*
  77 lemma eq_opp_x_times_opp_one_x: ∀F:ordered_field_ch0.∀x:F.-x = -1*x.
  78  intros;
  79
  80 lemma not_eq_x_zero_to_lt_zero_mult_x_x:
  81  ∀F:ordered_field_ch0.∀x:F. x ≠ 0 → 0 < x * x.
  82  intros;
  83  elim (of_weak_tricotomy ? ? ? ? ? ? ? ? F ? ? H);
  84   [ generalize in match (le_x_zero_to_le_zero_opp_x F ? H1); intro;
  85     generalize in match (of_mult_compat ? ? ? ? ? ? ? ?  F ? ? H2 H2); intro;
  86 *)
  87
  88 axiom lt_zero_to_lt_inv_zero:
  89  ∀F:ordered_field_ch0.∀x:F.∀p:x≠0. 0 < x → 0 < inv ? x p.
  90
  91 (* The ordering is not necessary. *)
  92 axiom not_eq_sum_field_zero: ∀F:ordered_field_ch0.∀n. O<n → sum_field F n ≠ 0.
  93 axiom le_zero_sum_field: ∀F:ordered_field_ch0.∀n. O<n → 0 < sum_field F n.
  94
  95 axiom lt_zero_to_le_inv_zero:
  96  ∀F:ordered_field_ch0.∀n:nat.∀p:sum_field F n ≠ 0. 0 ≤ inv ? (sum_field F n) p.
  97
  98 definition tends_to : ∀F:ordered_field_ch0.∀f:nat→F.∀l:F.Prop.
  99  alias symbol "leq" = "Ordered field le".
 100  alias id "le" = "cic:/matita/nat/orders/le.ind#xpointer(1/1)".
 101  apply
 102   (λF:ordered_field_ch0.λf:nat → F.λl:F.
 103     ∀n:nat.∃m:nat.∀j:nat. le m j →
 104      l - (inv F (sum_field F (S n)) ?) ≤ f j ∧
 105      f j ≤ l + (inv F (sum_field F (S n)) ?));
 106  apply not_eq_sum_field_zero;
 107  unfold;
 108  auto new.
 109 qed.
 110
 111 (*
 112 definition is_cauchy_seq ≝
 113  λF:ordered_field_ch0.λf:nat→F.
 114   ∀eps:F. 0 < eps →
 115    ∃n:nat.∀M. n ≤ M →
 116     -eps ≤ f M - f n ∧ f M - f n ≤ eps.
 117 *)
 118
 119
 120
 121 definition is_cauchy_seq : ∀F:ordered_field_ch0.∀f:nat→F.Prop.
 122  apply
 123   (λF:ordered_field_ch0.λf:nat→F.
 124     ∀m:nat.
 125      ∃n:nat.∀N. n ≤ N →
 126       -(inv ? (sum_field F (S m)) ?) ≤ f N - f n ∧
 127       f N - f n ≤ inv ? (sum_field F (S m)) ?);
 128  apply not_eq_sum_field_zero;
 129  unfold;
 130  auto.
 131 qed.
 132
 133 definition is_complete ≝
 134  λF:ordered_field_ch0.
 135   ∀f:nat→F. is_cauchy_seq ? f →
 136    ex F (λl:F. tends_to ? f l).