From d61b0ec37e7943a058dc9c6381efe49db7eb575f Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 5 Nov 2006 17:04:12 +0000
Subject: [PATCH] Some clean-up here and there in dama (coercions removed,
 implicits added, etc.)

---
 helm/software/matita/dama/fields.ma           |  6 +++---
 .../matita/dama/integration_algebras.ma       | 19 ++++++++-----------
 .../matita/dama/ordered_fields_ch0.ma         | 15 +++++++--------
 helm/software/matita/dama/reals.ma            |  8 ++++----
 helm/software/matita/dama/rings.ma            |  4 ++--
 5 files changed, 24 insertions(+), 28 deletions(-)

diff --git a/helm/software/matita/dama/fields.ma b/helm/software/matita/dama/fields.ma
index 0618f4923..2aac4f446 100644
--- a/helm/software/matita/dama/fields.ma
+++ b/helm/software/matita/dama/fields.ma
@@ -24,7 +24,7 @@ record is_field (R:ring) (inv:∀x:R.x ≠ 0 → R) : Prop
     inv_inverse_: ∀x.∀p: x ≠ 0. mult ? (inv x p) x = 1
  }.
 
-lemma opp_opp: \forall R:ring. \forall x:R. (-(-x))=x.
+lemma opp_opp: ∀R:ring. ∀x:R. --x=x.
 intros; 
 apply (cancellationlaw ? (-x) ? ?); 
 rewrite > (opp_inverse R x); 
@@ -50,10 +50,10 @@ theorem mult_comm: ∀F:field.symmetric ? (mult F).
  apply (mult_comm_ ? ? (field_properties F)).
 qed.
 
-theorem inv_inverse: ∀F:field.∀x.∀p: x ≠ 0. mult ? (inv F x p) x = 1.
+theorem inv_inverse: ∀F:field.∀x:F.∀p: x ≠ 0. (inv ? x p)*x = 1.
  intro;
  apply (inv_inverse_ ? ? (field_properties F)).
 qed.
 
 definition sum_field ≝
- λF:field. sum ? (plus F) (zero F) (one F).
+ λF:field. sum ? (plus F) 0 1.
diff --git a/helm/software/matita/dama/integration_algebras.ma b/helm/software/matita/dama/integration_algebras.ma
index fa43e944a..28185a785 100644
--- a/helm/software/matita/dama/integration_algebras.ma
+++ b/helm/software/matita/dama/integration_algebras.ma
@@ -27,7 +27,7 @@ record is_vector_space (K: field) (G:abelian_group) (emult:K→G→G) : Prop
 record vector_space (K:field): Type \def
 { vs_abelian_group :> abelian_group;
   emult: K → vs_abelian_group → vs_abelian_group;
-  vs_vector_space_properties :> is_vector_space K vs_abelian_group emult
+  vs_vector_space_properties :> is_vector_space ? vs_abelian_group emult
 }.
 
 interpretation "Vector space external product" 'times a b =
@@ -39,8 +39,7 @@ record is_semi_norm (R:real) (V: vector_space R) (semi_norm:V→R) : Prop \def
    sn_triangle_inequality: ∀x,y:V. semi_norm (x + y) ≤ semi_norm x + semi_norm y
  }.
 
-record is_norm (R:real) (V:vector_space R) (norm:V → R)
- : Prop \def
+record is_norm (R:real) (V:vector_space R) (norm:V → R) : Prop \def
  { n_semi_norm:> is_semi_norm ? ? norm;
    n_properness: ∀x:V. norm x = 0 → x = 0
  }.
@@ -91,9 +90,7 @@ record is_archimedean_riesz_space (K) (S:riesz_space K) : Prop
   { ars_archimedean: ∃u.∀n.∀a.∀p:n > O.
      le ? S
       (absolute_value ? S a)
-      (emult ? S
-        (inv ? (sum_field K n) (not_eq_sum_field_zero ? n p))
-        u) →
+      ((inv ? (sum_field K n) (not_eq_sum_field_zero ? n p))* u) →
      a = 0
   }.
 
@@ -106,7 +103,7 @@ record is_integral (K) (R:archimedean_riesz_space K) (I:R→K) : Prop
 \def
  { i_positive: ∀f:R. le ? R 0 f → of_le K 0 (I f);
    i_linear1: ∀f,g:R. I (f + g) = I f + I g;
-   i_linear2: ∀f:R.∀k:K. I (emult ? R k f) = k*(I f)
+   i_linear2: ∀f:R.∀k:K. I (k*f) = k*(I f)
  }.
 
 definition is_weak_unit ≝
@@ -118,12 +115,14 @@ definition is_weak_unit ≝
   ∀x:V. meet x unit = 0 → u = 0.
 *) λR:real.λV:archimedean_riesz_space R.λe:V.True.
 
+(* Here we are avoiding a construction (the quotient space to define
+   f=g iff I(|f-g|)=0 *)
 record integration_riesz_space (R:real) : Type \def
  { irs_archimedean_riesz_space:> archimedean_riesz_space R;
    irs_unit: irs_archimedean_riesz_space;
    irs_weak_unit: is_weak_unit ? ? irs_unit;
    integral: irs_archimedean_riesz_space → R;
-   irs_integral_properties: is_integral R irs_archimedean_riesz_space integral;
+   irs_integral_properties: is_integral ? ? integral;
    irs_limit1:
     ∀f:irs_archimedean_riesz_space.
      tends_to ?
@@ -154,7 +153,7 @@ record is_algebra (K: field) (V:vector_space K) (mult:V→V→V) (one:V) : Prop
 
 record algebra (K: field) (V:vector_space K) (a_one:V) : Type \def
  { a_mult: V → V → V;
-   a_algebra_properties: is_algebra K V a_mult a_one
+   a_algebra_properties: is_algebra ? ? a_mult a_one
  }.
 
 interpretation "Algebra product" 'times a b =
@@ -188,8 +187,6 @@ Type \def
 axiom symmetric_a_mult:
  ∀K,R,one.∀A:f_algebra K R one. symmetric ? (a_mult ? ? ? A).
 
-(* Here we are avoiding a construction (the quotient space to define
-   f=g iff I(|f-g|)=0 *)
 record integration_f_algebra (R:real) : Type \def
  { ifa_integration_riesz_space:> integration_riesz_space R;
    ifa_f_algebra:>
diff --git a/helm/software/matita/dama/ordered_fields_ch0.ma b/helm/software/matita/dama/ordered_fields_ch0.ma
index c7bf906f5..c06ea743e 100644
--- a/helm/software/matita/dama/ordered_fields_ch0.ma
+++ b/helm/software/matita/dama/ordered_fields_ch0.ma
@@ -21,7 +21,8 @@ record is_total_order_relation (C:Type) (le:C→C→Prop) : Type \def
    to_antisimmetry: ∀x,y:C. le x y → le y x → x=y
  }.
 
-theorem to_transitive: ∀C,le. is_total_order_relation C le → transitive ? le.
+theorem to_transitive:
+ ∀C.∀le:C→C→Prop. is_total_order_relation ? le → transitive ? le.
  intros;
  unfold transitive;
  intros;
@@ -44,7 +45,7 @@ record is_ordered_field_ch0 (F:field) (le:F→F→Prop) : Type \def
 record ordered_field_ch0 : Type \def
  { of_field:> field;
    of_le: of_field → of_field → Prop;
-   of_ordered_field_properties:> is_ordered_field_ch0 of_field of_le
+   of_ordered_field_properties:> is_ordered_field_ch0 ? of_le
  }.
 
 interpretation "Ordered field le" 'leq a b =
@@ -93,16 +94,14 @@ axiom not_eq_sum_field_zero: ∀F:ordered_field_ch0.∀n. O<n → sum_field F n
 axiom le_zero_sum_field: ∀F:ordered_field_ch0.∀n. O<n → 0 < sum_field F n.
 
 axiom lt_zero_to_le_inv_zero:
- ∀F:ordered_field_ch0.∀n:nat.∀p:sum_field F n ≠ 0. 0 ≤ inv ? (sum_field F 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.
- alias symbol "leq" = "Ordered field le".
- alias id "le" = "cic:/matita/nat/orders/le.ind#xpointer(1/1)".
  apply
   (λF:ordered_field_ch0.λf:nat → F.λl:F.
-    ∀n:nat.∃m:nat.∀j:nat. le m j →
-     l - (inv F (sum_field F (S n)) ?) ≤ f j ∧
-     f j ≤ l + (inv F (sum_field F (S n)) ?));
+    ∀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.
diff --git a/helm/software/matita/dama/reals.ma b/helm/software/matita/dama/reals.ma
index 97ca4151f..336bfe2e7 100644
--- a/helm/software/matita/dama/reals.ma
+++ b/helm/software/matita/dama/reals.ma
@@ -18,7 +18,7 @@ include "ordered_fields_ch0.ma".
 
 record is_real (F:ordered_field_ch0) : Type
 ≝
- { r_archimedean: ∀x:F. ∃n:nat. x ≤ (sum_field F n);
+ { r_archimedean: ∀x:F. ∃n:nat. x ≤ (sum_field ? n);
    r_complete: is_complete F  
  }.
 
@@ -27,7 +27,7 @@ record real: Type \def
    r_real_properties: is_real r_ordered_field_ch0
  }.
 
-definition lim: ∀R:real.∀f:nat→R.is_cauchy_seq R f → R.
+definition lim: ∀R:real.∀f:nat→R.is_cauchy_seq ? f → R.
  intros;
  elim (r_complete ? (r_real_properties R) ? H);
  exact a.
@@ -35,7 +35,7 @@ qed.
 
 definition max_seq: ∀R:real.∀x,y:R. nat → R.
  intros (R x y);
- elim (to_cotransitive R (of_le R) R 0 (inv ? (sum_field R (S n)) ?) (x-y));
+ elim (to_cotransitive R (of_le R) R 0 (inv ? (sum_field ? (S n)) ?) (x-y));
   [ apply x
   | apply not_eq_sum_field_zero ;
     unfold;
@@ -47,7 +47,7 @@ qed.
 
 axiom daemon: False.
 
-theorem cauchy_max_seq: ∀R:real.∀x,y. is_cauchy_seq ? (max_seq R x y).
+theorem cauchy_max_seq: ∀R:real.∀x,y:R. is_cauchy_seq ? (max_seq ? x y).
  intros;
  unfold;
  intros;
diff --git a/helm/software/matita/dama/rings.ma b/helm/software/matita/dama/rings.ma
index a562a4819..ec460748b 100644
--- a/helm/software/matita/dama/rings.ma
+++ b/helm/software/matita/dama/rings.ma
@@ -90,9 +90,9 @@ lemma eq_mult_x_zero_zero: ∀R:ring.∀x:R.x*0=0.
 intros;
 generalize in match (zero_neutral R 0);
 intro;
-generalize in match (eq_f ? ? (\lambda y.x*y) ? ? H); intro; clear H;
+generalize in match (eq_f ? ? (λy.x*y) ? ? H); intro; clear H;
 rewrite > mult_plus_distr_left in H1;
-generalize in match (eq_f ? ? (\lambda y. (-(x*0)) +y) ? ? H1);intro;
+generalize in match (eq_f ? ? (λy. (-(x*0)) +y) ? ? H1);intro;
 clear H1;
 rewrite < plus_assoc in H;
 rewrite > opp_inverse in H;
-- 
2.39.2