X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fordered_fields_ch0.ma;h=d423894d064b77a202ade901fdaca33c765a9c91;hb=8526bd5238a810aab024b45827c6f438ff10df7a;hp=4a7b7a2662a0906dba90eb95b7f07e0e5d5e48fd;hpb=c6b621c1df5abd9a8a1567991379768c435607dd;p=helm.git

diff --git a/helm/software/matita/dama/ordered_fields_ch0.ma b/helm/software/matita/dama/ordered_fields_ch0.ma
index 4a7b7a266..d423894d0 100644
--- a/helm/software/matita/dama/ordered_fields_ch0.ma
+++ b/helm/software/matita/dama/ordered_fields_ch0.ma
@@ -15,72 +15,78 @@
 set "baseuri" "cic:/matita/ordered_fields_ch0/".
 
 include "fields.ma".
-include "ordered_sets.ma".
+include "ordered_groups.ma".
 
 (*CSC: non capisco questi alias! Una volta non servivano*)
 alias id "plus" = "cic:/matita/groups/plus.con".
 alias symbol "plus" = "Abelian group plus".
-record is_ordered_field_ch0 (F:field) (le:F→F→Prop) : Type \def
- { of_mult_compat: ∀a,b. le 0 a → le 0 b → le 0 (a*b);
-   of_plus_compat: ∀a,b,c. le a b → le (a+c) (b+c);
-   of_weak_tricotomy : ∀a,b. a≠b → le a b ∨ le b a;
-   (* 0 characteristics *)
-   (*CSC: qua c'era un ? al posto di F *)
-   of_char0: ∀n. n > O → sum F (plus F) 0 1 n ≠ 0
- }.
- 
-record ordered_field_ch0 : Type \def
+
+record pre_ordered_field_ch0: Type ≝
  { of_field:> field;
-   of_ordered_set:> ordered_set of_field;
-   of_reflexive: reflexive ? (os_le ? of_ordered_set);
-   of_antisimmetric: antisimmetric ? (os_le ? of_ordered_set);
-   of_cotransitive: cotransitive ? (os_le ? of_ordered_set);
-   (*CSC: qui c'era un ? al posto di of_field *)
-   of_ordered_field_properties:> is_ordered_field_ch0 of_field (os_le ? of_ordered_set)
+   of_ordered_abelian_group_: ordered_abelian_group;
+   of_cotransitively_ordered_set_: cotransitively_ordered_set;
+   of_with1_:
+    cos_ordered_set of_cotransitively_ordered_set_ =
+     og_ordered_set of_ordered_abelian_group_;
+   of_with2:
+    og_abelian_group of_ordered_abelian_group_ = r_abelian_group of_field
  }.
 
-(*theorem ordered_set_of_ordered_field_ch0:
- ∀F:ordered_field_ch0.ordered_set F.
- intros;
- apply mk_ordered_set;
-  [ apply (mk_pre_ordered_set ? (of_le F))
-  | apply mk_is_order_relation;
-     [ apply (of_reflexive F)
-     | apply antisimmetric_to_cotransitive_to_transitive;
-       [ apply (of_antisimmetric F)
-       | apply (of_cotransitive F)
-       ]
-     | apply (of_antisimmetric F)
+lemma of_ordered_abelian_group: pre_ordered_field_ch0 → ordered_abelian_group.
+ intro F;
+ apply mk_ordered_abelian_group;
+  [ apply mk_pre_ordered_abelian_group;
+     [ apply (r_abelian_group F)
+     | apply (og_ordered_set (of_ordered_abelian_group_ F))
+     | apply (eq_f ? ? carrier);
+       apply (of_with2 F)
      ]
-  ].
+  |
+    apply
+     (eq_rect' ? ?
+      (λG:abelian_group.λH:og_abelian_group (of_ordered_abelian_group_ F)=G.
+        is_ordered_abelian_group
+         (mk_pre_ordered_abelian_group G (of_ordered_abelian_group_ F)
+          (eq_f abelian_group Type carrier (of_ordered_abelian_group_ F) G
+          H)))
+      ? ? (of_with2 F));
+    simplify;
+    apply (og_ordered_abelian_group_properties (of_ordered_abelian_group_ F))
+  ]
 qed.
 
-coercion cic:/matita/ordered_fields_ch0/ordered_set_of_ordered_field_ch0.con.
-*)
-
-(*interpretation "Ordered field le" 'leq a b =
- (cic:/matita/ordered_fields_ch0/of_le.con _ a b).
- *)
-
-(*CSC: qua c'era uno zero*)
-lemma le_zero_x_to_le_opp_x_zero: ∀F:ordered_field_ch0.∀x:F.(zero F) ≤ x → -x ≤ 0.
-intros;
- generalize in match (of_plus_compat ? ? F ? ? (-x) H); intro;
- rewrite > zero_neutral in H1;
- rewrite > plus_comm in H1;
- rewrite > opp_inverse in H1;
- (*assumption*)apply H1.
+coercion cic:/matita/ordered_fields_ch0/of_ordered_abelian_group.con.
+
+(*CSC: I am not able to prove this since unfold is undone by coercion composition*)
+axiom of_with1:
+ ∀G:pre_ordered_field_ch0.
+  cos_ordered_set (of_cotransitively_ordered_set_ G) =
+   og_ordered_set (of_ordered_abelian_group G).
+
+lemma of_cotransitively_ordered_set : pre_ordered_field_ch0 → cotransitively_ordered_set.
+ intro F;
+ apply mk_cotransitively_ordered_set;
+ [ apply (og_ordered_set F)
+ | apply
+    (eq_rect ? ? (λa:ordered_set.cotransitive (os_carrier a) (os_le a))
+      ? ? (of_with1 F));
+   apply cos_cotransitive
+ ]
 qed.
 
-(*CSC: qua c'era uno zero*)
-lemma le_x_zero_to_le_zero_opp_x: ∀F:ordered_field_ch0.∀x:F. x ≤ 0 → (zero F) ≤ -x.
- intros;
- generalize in match (of_plus_compat ? ? F ? ? (-x) H); intro;
- rewrite > zero_neutral in H1;
- rewrite > plus_comm in H1;
- rewrite > opp_inverse in H1;
- (*assumption.*) apply H1.
-qed.
+coercion cic:/matita/ordered_fields_ch0/of_cotransitively_ordered_set.con.
+
+record is_ordered_field_ch0 (F:pre_ordered_field_ch0) : Type \def
+ { of_mult_compat: ∀a,b:F. 0≤a → 0≤b → 0≤a*b;
+   of_weak_tricotomy : ∀a,b:F. a≠b → a≤b ∨ b≤a;
+   (* 0 characteristics *)
+   of_char0: ∀n. n > O → sum ? (plus F) 0 1 n ≠ 0
+ }.
+ 
+record ordered_field_ch0 : Type \def
+ { of_pre_ordered_field_ch0:> pre_ordered_field_ch0;
+   of_ordered_field_properties:> is_ordered_field_ch0 of_pre_ordered_field_ch0
+ }.
 
 (*
 lemma eq_opp_x_times_opp_one_x: ∀F:ordered_field_ch0.∀x:F.-x = -1*x.
@@ -95,26 +101,26 @@ lemma not_eq_x_zero_to_lt_zero_mult_x_x:
 *)  
 
 axiom lt_zero_to_lt_inv_zero:
- ∀F:ordered_field_ch0.∀x:F.∀p:x≠0. lt ? F 0 x → lt ? F 0 (inv ? x p).
+ ∀F:ordered_field_ch0.∀x:F.∀p:x≠0. lt F 0 x → lt F 0 (inv ? x p).
 
 alias symbol "lt" = "natural 'less than'".
 
 (* The ordering is not necessary. *)
 axiom not_eq_sum_field_zero: ∀F:ordered_field_ch0.∀n. O<n → sum_field F n ≠ 0.
-axiom le_zero_sum_field: ∀F:ordered_field_ch0.∀n. O<n → lt ? F 0 (sum_field F n).
+axiom le_zero_sum_field: ∀F:ordered_field_ch0.∀n. O<n → lt F 0 (sum_field F n).
 
 axiom lt_zero_to_le_inv_zero:
- ∀F:ordered_field_ch0.∀n:nat.∀p:sum_field F n ≠ 0. os_le ? F 0 (inv ? (sum_field ? n) p).
+ ∀F:ordered_field_ch0.∀n:nat.∀p:sum_field F n ≠ 0. 0 ≤ inv ? (sum_field ? n) p.
 
 definition tends_to : ∀F:ordered_field_ch0.∀f:nat→F.∀l:F.Prop.
  apply
   (λF:ordered_field_ch0.λf:nat → F.λl:F.
-    ∀n:nat.∃m:nat.∀j:nat. le m j →
+    ∀n:nat.∃m:nat.∀j:nat.m ≤ j →
      l - (inv F (sum_field ? (S n)) ?) ≤ f j ∧
      f j ≤ l + (inv F (sum_field ? (S n)) ?));
  apply not_eq_sum_field_zero;
  unfold;
- auto new.
+ autobatch.
 qed.
 
 (*
@@ -131,15 +137,15 @@ definition is_cauchy_seq : ∀F:ordered_field_ch0.∀f:nat→F.Prop.
  apply
   (λF:ordered_field_ch0.λf:nat→F.
     ∀m:nat.
-     ∃n:nat.∀N. le n N →
+     ∃n:nat.∀N.n ≤ N →
       -(inv ? (sum_field F (S m)) ?) ≤ f N - f n ∧
       f N - f n ≤ inv ? (sum_field F (S m)) ?);
  apply not_eq_sum_field_zero;
  unfold;
- auto.
+ autobatch.
 qed.
 
 definition is_complete ≝
  λF:ordered_field_ch0.
   ∀f:nat→F. is_cauchy_seq ? f →
-   ex F (λl:F. tends_to ? f l).
\ No newline at end of file
+   ex F (λl:F. tends_to ? f l).