Up to max (up to a bug).

diff --git a/helm/software/matita/dama/constructive_connectives.ma b/helm/software/matita/dama/constructive_connectives.ma
index 259357934da012a99aba8adafac2febba1152462..461f90e6dd66ef507029de1e0494ecb0859097c0 100644 (file)
--- a/helm/software/matita/dama/constructive_connectives.ma
+++ b/helm/software/matita/dama/constructive_connectives.ma
@@ -18,6 +18,17 @@ inductive or (A,B:Type) : Type \def
    Left : A → or A B
  | Right : B → or A B.
 
-interpretation "classical or" 'or x y =
+interpretation "constructive or" 'or x y =
   (cic:/matita/constructive_connectives/or.ind#xpointer(1/1) x y).
 
+inductive ex (A:Type) (P:A→Prop) : Type \def
+  ex_intro: ∀w:A. P w → ex A P.
+
+notation < "hvbox(Σ ident i opt (: ty) break . p)"
+  right associative with precedence 20
+for @{ 'exists ${default
+  @{\lambda ${ident i} : $ty. $p)}
+  @{\lambda ${ident i} . $p}}}.
+
+interpretation "constructive exists" 'sigma \eta.x =
+  (cic:/matita/constructive_connectives/ex.ind#xpointer(1/1) _ x).
\ No newline at end of file

diff --git a/helm/software/matita/dama/groups.ma b/helm/software/matita/dama/groups.ma
index 6d832c208272231be0be1276410fddf5e67c4c88..1b39c1518348e7431de23d10ee1d2e6fc3dcf86f 100644 (file)
--- a/helm/software/matita/dama/groups.ma
+++ b/helm/software/matita/dama/groups.ma
@@ -103,3 +103,27 @@ rewrite > zero_neutral in H1;
 assumption.
 qed.
 
+theorem eq_opp_plus_plus_opp_opp: ∀G:abelian_group.∀x,y:G. -(x+y) = -x + -y.
+ intros;
+ apply (cancellationlaw ? (x+y));
+ rewrite < plus_comm;
+ rewrite > opp_inverse;
+ rewrite > plus_assoc;
+ rewrite > plus_comm in ⊢ (? ? ? (? ? ? (? ? ? %)));
+ rewrite < plus_assoc in ⊢ (? ? ? (? ? ? %));
+ rewrite > plus_comm;
+ rewrite > plus_comm in ⊢ (? ? ? (? ? (? ? % ?) ?));
+ rewrite > opp_inverse;
+ rewrite > zero_neutral;
+ rewrite > opp_inverse;
+ reflexivity.
+qed.
+
+theorem eq_opp_opp_x_x: ∀G:abelian_group.∀x:G.--x=x.
+ intros;
+ apply (cancellationlaw ? (-x));
+ rewrite > opp_inverse;
+ rewrite > plus_comm;
+ rewrite > opp_inverse;
+ reflexivity.
+qed.
\ No newline at end of file

diff --git a/helm/software/matita/dama/ordered_fields_ch0.ma b/helm/software/matita/dama/ordered_fields_ch0.ma
index f796ebb1ddcc3aef64b8b906b98d7e4ce35689f6..c7bf906f54afc3bd0f39670f024e6fcf5a0edbf4 100644 (file)
--- a/helm/software/matita/dama/ordered_fields_ch0.ma
+++ b/helm/software/matita/dama/ordered_fields_ch0.ma
@@ -21,6 +21,17 @@ 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.
+ intros;
+ unfold transitive;
+ intros;
+ elim (to_cotransitive ? ? i ? ? z H);
+  [ assumption
+  | rewrite < (to_antisimmetry ? ? i ? ? H1 t);
+    assumption
+  ].
+qed.
+
 record is_ordered_field_ch0 (F:field) (le:F→F→Prop) : Type \def
  { of_total_order_relation:> is_total_order_relation ? le;
    of_mult_compat: ∀a,b. le 0 a → le 0 b → le 0 (a*b);
@@ -105,6 +116,8 @@ definition is_cauchy_seq ≝
     -eps ≤ f M - f n ∧ f M - f n ≤ eps.
 *)
 
+
+
 definition is_cauchy_seq : ∀F:ordered_field_ch0.∀f:nat→F.Prop.
  apply
   (λF:ordered_field_ch0.λf:nat→F.
@@ -120,4 +133,4 @@ qed.
 definition is_complete ≝
  λF:ordered_field_ch0.
   ∀f:nat→F. is_cauchy_seq ? f →
-   ∃l:F. tends_to ? f l.
\ No newline at end of file
+   ex F (λl:F. tends_to ? f l).
\ No newline at end of file

diff --git a/helm/software/matita/dama/reals.ma b/helm/software/matita/dama/reals.ma
index 5566ece4327f802144990b519ca05544ea7deb18..f587435a3b38ff4f406fc125dd492c22b61e8513 100644 (file)
--- a/helm/software/matita/dama/reals.ma
+++ b/helm/software/matita/dama/reals.ma
@@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/reals/".
 
 include "ordered_fields_ch0.ma".
 
-record is_real (F:ordered_field_ch0) : Prop
+record is_real (F:ordered_field_ch0) : Type
 ≝
  { r_archimedean: ∀x:F. ∃n:nat. x ≤ (sum_field F n);
    r_complete: is_complete F  
@@ -46,48 +46,73 @@ definition max_seq: ∀R:real.∀x,y:R. nat → R.
   ].
 qed.
 
+axiom daemon: False.
+
 theorem cauchy_max_seq: ∀R:real.∀x,y. is_cauchy_seq ? (max_seq R x y).
  intros;
  unfold;
  intros;
- apply (ex_intro ? ? m);
+ exists; [ exact m | ]; (* apply (ex_intro ? ? m); *)
  intros;
- split;
-  [ 
-  | unfold max_seq;
-    elim (to_cotransitive R (of_le R) R 0
+ unfold max_seq;
+ elim (to_cotransitive R (of_le R) R 0
 (inv R (sum_field R (S N))
  (not_eq_sum_field_zero R (S N) (le_S_S O N (le_O_n N)))) (x-y)
 (lt_zero_to_le_inv_zero R (S N)
  (not_eq_sum_field_zero R (S N) (le_S_S O N (le_O_n N)))));
-     [ simplify;
-       elim (to_cotransitive R (of_le R) R 0
+  [ simplify;
+    elim (to_cotransitive R (of_le R) R 0
 (inv R (1+sum R (plus R) 0 1 m)
  (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))) (x-y)
 (lt_zero_to_le_inv_zero R (S m)
  (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))));
-       [ simplify;
-         rewrite > (plus_comm ? x (-x));
-         rewrite > opp_inverse;
-         apply lt_zero_to_le_inv_zero
-       | simplify;
-         assumption
+    [ simplify;
+      rewrite > (plus_comm ? x (-x));
+      rewrite > opp_inverse;
+      split;
+       [ elim daemon (* da finire *)
+       | apply lt_zero_to_le_inv_zero
+       ]
+    | simplify;
+      split;
+       [ elim daemon (* da finire *)
+       | assumption
        ]
-     | elim (to_cotransitive R (of_le R) R 0
+    ]
+  | simplify;
+    elim (to_cotransitive R (of_le R) R 0
 (inv R (1+sum R (plus R) 0 1 m)
  (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))) (x-y)
 (lt_zero_to_le_inv_zero R (S m)
  (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))));
-        [ simplify;
-          generalize in match (le_zero_x_to_le_opp_x_zero R ? t1);
-          intro;
-          (* finire *)
-        |simplify;
-         rewrite > (plus_comm ? y (-y));
-         rewrite > opp_inverse;
-         apply lt_zero_to_le_inv_zero
+     [ simplify;
+       split;
+       [ elim daemon (* da finire *)
+       | generalize in match (le_zero_x_to_le_opp_x_zero R ? t1);
+         intro;
+         unfold minus in H1;
+         rewrite > eq_opp_plus_plus_opp_opp in H1;
+         rewrite > eq_opp_opp_x_x in H1;
+         rewrite > plus_comm in H1;
+         apply (to_transitive ? ? (of_total_order_relation ? ? R) ? 0 ?);
+          [ assumption
+          | apply lt_zero_to_le_inv_zero
+          ]
         ]
+     | simplify;
+       rewrite > (plus_comm ? y (-y));
+       rewrite > opp_inverse;
+       split;
+       [ elim daemon (* da finire *)
+       | apply lt_zero_to_le_inv_zero
+       ]
      ]
   ].
+qed.
+
+definition max: ∀R:real.R → R → R.
+ intros (R x y);
+ elim (r_complete ? (r_real_properties R) ? ?);
+  [|| apply (cauchy_max_seq R x y) ]
+qed.
  
- 
\ No newline at end of file