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