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_ordered_field_ch0 (F:field) (le:F→F→Prop) : Prop \def
  20  { of_mult_compat: ∀a,b. le 0 a → le 0 b → le 0 (a*b);
  21    of_plus_compat: ∀a,b,c. le a b → le (a+c) (b+c);
  22    of_weak_tricotomy : ∀a,b. a≠b → le a b ∨ le b a;
  23    (* 0 characteristics *)
  24    of_char0: ∀n. n > O → sum ? (plus F) 0 1 n ≠ 0
  25  }.
  26
  27 record ordered_field_ch0 : Type \def
  28  { of_field:> field;
  29    of_le: of_field → of_field → Prop;
  30    of_ordered_field_properties:> is_ordered_field_ch0 of_field of_le
  31  }.
  32
  33 interpretation "Ordered field le" 'leq a b =
  34  (cic:/matita/ordered_fields_ch0/of_le.con _ a b).
  35
  36 definition lt \def λF:ordered_field_ch0.λa,b:F.a ≤ b ∧ a ≠ b.
  37
  38 interpretation "Ordered field lt" 'lt a b =
  39  (cic:/matita/ordered_fields_ch0/lt.con _ a b).
  40
  41 lemma le_zero_x_to_le_opp_x_zero: ∀F:ordered_field_ch0.∀x:F. 0 ≤ x → -x ≤ 0.
  42 intros;
  43  generalize in match (of_plus_compat ? ? F ? ? (-x) H); intro;
  44  rewrite > zero_neutral in H1;
  45  rewrite > plus_comm in H1;
  46  rewrite > opp_inverse in H1;
  47  assumption.
  48 qed.
  49
  50 lemma le_x_zero_to_le_zero_opp_x: ∀F:ordered_field_ch0.∀x:F. x ≤ 0 → 0 ≤ -x.
  51  intros;
  52  generalize in match (of_plus_compat ? ? F ? ? (-x) H); intro;
  53  rewrite > zero_neutral in H1;
  54  rewrite > plus_comm in H1;
  55  rewrite > opp_inverse in H1;
  56  assumption.
  57 qed.
  58
  59 (*
  60 lemma eq_opp_x_times_opp_one_x: ∀F:ordered_field_ch0.∀x:F.-x = -1*x.
  61  intros;
  62
  63 lemma not_eq_x_zero_to_lt_zero_mult_x_x:
  64  ∀F:ordered_field_ch0.∀x:F. x ≠ 0 → 0 < x * x.
  65  intros;
  66  elim (of_weak_tricotomy ? ? ? ? ? ? ? ? F ? ? H);
  67   [ generalize in match (le_x_zero_to_le_zero_opp_x F ? H1); intro;
  68     generalize in match (of_mult_compat ? ? ? ? ? ? ? ?  F ? ? H2 H2); intro;
  69 *)
  70
  71 (* The ordering is not necessary. *)
  72 axiom not_eq_sum_field_zero: ∀F:ordered_field_ch0.∀n. O<n → sum_field F n ≠ 0.
  73
  74