--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/constructive_connectives/".
+
+inductive or (A,B:Type) : Type \def
+ Left : A → or A B
+ | Right : B → or A B.
+
+interpretation "classical or" 'or x y =
+ (cic:/matita/constructive_connectives/or.ind#xpointer(1/1) x y).
+
include "higher_order_defs/functions.ma".
include "nat/nat.ma".
include "nat/orders.ma".
+include "constructive_connectives.ma".
definition left_neutral \def λC,op.λe:C. ∀x:C. op e x = x.
(* to be proved; see footnote 2 in the paper by Spitters *)
axiom symmetric_a_mult: ∀K.∀A:f_algebra K. symmetric ? (a_mult ? ? A).
-
-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)) ?));
- apply not_eq_sum_field_zero;
- unfold;
- auto new.
-qed.
-
record is_integral (K) (A:f_algebra K) (I:Type_OF_f_algebra ? A→K) : Prop
\def
{ i_positive: ∀f:Type_OF_f_algebra ? A. le ? (lattice_OF_f_algebra ? A) 0 f → of_le K 0 (I f);
include "fields.ma".
-record is_ordered_field_ch0 (F:field) (le:F→F→Prop) : Prop \def
- { of_mult_compat: ∀a,b. le 0 a → le 0 b → le 0 (a*b);
+record is_total_order_relation (C:Type) (le:C→C→Prop) : Type \def
+ { to_cotransitive: ∀x,y,z:C. le x y → le x z ∨ le z y;
+ to_antisimmetry: ∀x,y:C. le x y → le y x → x=y
+ }.
+
+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);
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 *)
generalize in match (of_mult_compat ? ? ? ? ? ? ? ? F ? ? H2 H2); intro;
*)
+axiom lt_zero_to_lt_inv_zero:
+ ∀F:ordered_field_ch0.∀x:F.∀p:x≠0. 0 < x → 0 < inv ? x p.
+
(* 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 → 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.
+
+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)) ?));
+ apply not_eq_sum_field_zero;
+ unfold;
+ auto new.
+qed.
+
+(*
+definition is_cauchy_seq ≝
+ λF:ordered_field_ch0.λf:nat→F.
+ ∀eps:F. 0 < eps →
+ ∃n:nat.∀M. n ≤ M →
+ -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.
+ ∀m:nat.
+ ∃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.
+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
include "ordered_fields_ch0.ma".
+record is_real (F:ordered_field_ch0) : Prop
+≝
+ { r_archimedean: ∀x:F. ∃n:nat. x ≤ (sum_field F n);
+ r_complete: is_complete F
+ }.
+record real: Type \def
+ { r_ordered_field_ch0:> ordered_field_ch0;
+ r_real_properties: is_real r_ordered_field_ch0
+ }.
+
+(* serve l'esistenziale in CProp!
+definition lim: ∀R:real.∀f:nat→R.is_cauchy_seq R f → R.
+ intros;
+ elim H;
+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));
+ [ apply x
+ | apply not_eq_sum_field_zero ;
+ unfold;
+ auto new
+ | apply y
+ | apply lt_zero_to_le_inv_zero
+ ].
+qed.
+
+theorem cauchy_max_seq: ∀R:real.∀x,y. is_cauchy_seq ? (max_seq R x y).
+ intros;
+ unfold;
+ intros;
+ apply (ex_intro ? ? m);
+ intros;
+ split;
+ [
+ | 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
+(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
+ ]
+ | 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
+ ]
+ ]
+ ].
+
+
\ No newline at end of file
projects / helm.git / commitdiff