helm/software/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_groups.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_ordered_abelian_group_: ordered_abelian_group;
  27    of_cotransitively_ordered_set_: cotransitively_ordered_set;
  28    of_with1_:
  29     cos_ordered_set of_cotransitively_ordered_set_ =
  30      og_ordered_set of_ordered_abelian_group_;
  31    of_with2:
  32     og_abelian_group of_ordered_abelian_group_ = r_abelian_group of_field
  33  }.
  34
  35 lemma of_ordered_abelian_group: pre_ordered_field_ch0 → ordered_abelian_group.
  36  intro F;
  37  apply mk_ordered_abelian_group;
  38   [ apply mk_pre_ordered_abelian_group;
  39      [ apply (r_abelian_group F)
  40      | apply (og_ordered_set (of_ordered_abelian_group_ F))
  41      | apply (eq_f ? ? carrier);
  42        apply (of_with2 F)
  43      ]
  44   |
  45     apply
  46      (eq_rect' ? ?
  47       (λG:abelian_group.λH:og_abelian_group (of_ordered_abelian_group_ F)=G.
  48         is_ordered_abelian_group
  49          (mk_pre_ordered_abelian_group G (of_ordered_abelian_group_ F)
  50           (eq_f abelian_group Type carrier (of_ordered_abelian_group_ F) G
  51           H)))
  52       ? ? (of_with2 F));
  53     simplify;
  54     apply (og_ordered_abelian_group_properties (of_ordered_abelian_group_ F))
  55   ]
  56 qed.
  57
  58 coercion cic:/matita/ordered_fields_ch0/of_ordered_abelian_group.con.
  59
  60 (*CSC: I am not able to prove this since unfold is undone by coercion composition*)
  61 axiom of_with1:
  62  ∀G:pre_ordered_field_ch0.
  63   cos_ordered_set (of_cotransitively_ordered_set_ G) =
  64    og_ordered_set (of_ordered_abelian_group G).
  65
  66 lemma of_cotransitively_ordered_set : pre_ordered_field_ch0 → cotransitively_ordered_set.
  67  intro F;
  68  apply mk_cotransitively_ordered_set;
  69  [ apply (og_ordered_set F)
  70  | apply
  71     (eq_rect ? ? (λa:ordered_set.cotransitive (os_carrier a) (os_le a))
  72       ? ? (of_with1 F));
  73    apply cos_cotransitive
  74  ]
  75 qed.
  76
  77 coercion cic:/matita/ordered_fields_ch0/of_cotransitively_ordered_set.con.
  78
  79 record is_ordered_field_ch0 (F:pre_ordered_field_ch0) : Type \def
  80  { of_mult_compat: ∀a,b:F. 0≤a → 0≤b → 0≤a*b;
  81    of_weak_tricotomy : ∀a,b:F. a≠b → a≤b ∨ b≤a;
  82    (* 0 characteristics *)
  83    of_char0: ∀n. n > O → sum ? (plus F) 0 1 n ≠ 0
  84  }.
  85
  86 record ordered_field_ch0 : Type \def
  87  { of_pre_ordered_field_ch0:> pre_ordered_field_ch0;
  88    of_ordered_field_properties:> is_ordered_field_ch0 of_pre_ordered_field_ch0
  89  }.
  90
  91 (*
  92 lemma eq_opp_x_times_opp_one_x: ∀F:ordered_field_ch0.∀x:F.-x = -1*x.
  93  intros;
  94
  95 lemma not_eq_x_zero_to_lt_zero_mult_x_x:
  96  ∀F:ordered_field_ch0.∀x:F. x ≠ 0 → 0 < x * x.
  97  intros;
  98  elim (of_weak_tricotomy ? ? ? ? ? ? ? ? F ? ? H);
  99   [ generalize in match (le_x_zero_to_le_zero_opp_x F ? H1); intro;
 100     generalize in match (of_mult_compat ? ? ? ? ? ? ? ?  F ? ? H2 H2); intro;
 101 *)
 102
 103 axiom lt_zero_to_lt_inv_zero:
 104  ∀F:ordered_field_ch0.∀x:F.∀p:x≠0. lt F 0 x → lt F 0 (inv ? x p).
 105
 106 alias symbol "lt" = "natural 'less than'".
 107
 108 (* The ordering is not necessary. *)
 109 axiom not_eq_sum_field_zero: ∀F:ordered_field_ch0.∀n. O<n → sum_field F n ≠ 0.
 110 axiom le_zero_sum_field: ∀F:ordered_field_ch0.∀n. O<n → lt F 0 (sum_field F n).
 111
 112 axiom lt_zero_to_le_inv_zero:
 113  ∀F:ordered_field_ch0.∀n:nat.∀p:sum_field F n ≠ 0. 0 ≤ inv ? (sum_field ? n) p.
 114
 115 definition tends_to : ∀F:ordered_field_ch0.∀f:nat→F.∀l:F.Prop.
 116  apply
 117   (λF:ordered_field_ch0.λf:nat → F.λl:F.
 118     ∀n:nat.∃m:nat.∀j:nat.m ≤ j →
 119      l - (inv F (sum_field ? (S n)) ?) ≤ f j ∧
 120      f j ≤ l + (inv F (sum_field ? (S n)) ?));
 121  apply not_eq_sum_field_zero;
 122  unfold;
 123  autobatch.
 124 qed.
 125
 126 (*
 127 definition is_cauchy_seq ≝
 128  λF:ordered_field_ch0.λf:nat→F.
 129   ∀eps:F. 0 < eps →
 130    ∃n:nat.∀M. n ≤ M →
 131     -eps ≤ f M - f n ∧ f M - f n ≤ eps.
 132 *)
 133
 134
 135
 136 definition is_cauchy_seq : ∀F:ordered_field_ch0.∀f:nat→F.Prop.
 137  apply
 138   (λF:ordered_field_ch0.λf:nat→F.
 139     ∀m:nat.
 140      ∃n:nat.∀N.n ≤ N →
 141       -(inv ? (sum_field F (S m)) ?) ≤ f N - f n ∧
 142       f N - f n ≤ inv ? (sum_field F (S m)) ?);
 143  apply not_eq_sum_field_zero;
 144  unfold;
 145  autobatch.
 146 qed.
 147
 148 definition is_complete ≝
 149  λF:ordered_field_ch0.
 150   ∀f:nat→F. is_cauchy_seq ? f →
 151    ex F (λl:F. tends_to ? f l).