From: Enrico Zoli Date: Tue, 31 Oct 2006 18:23:36 +0000 (+0000) Subject: We begin to play the real game: we have defined real numbers and X-Git-Tag: 0.4.95@7852~827 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=348acb421355c345a9af0754c1c16508a43eeea5;p=helm.git We begin to play the real game: we have defined real numbers and constructive connectives (only the disjunction for now) and we are trying to define the max between two real numbers as the limit of a particular cauchy sequence. Cool. --- diff --git a/matita/dama/constructive_connectives.ma b/matita/dama/constructive_connectives.ma new file mode 100644 index 000000000..259357934 --- /dev/null +++ b/matita/dama/constructive_connectives.ma @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||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). + diff --git a/matita/dama/groups.ma b/matita/dama/groups.ma index 8353ea676..6d832c208 100644 --- a/matita/dama/groups.ma +++ b/matita/dama/groups.ma @@ -17,6 +17,7 @@ set "baseuri" "cic:/matita/groups/". 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. diff --git a/matita/dama/integration_algebras.ma b/matita/dama/integration_algebras.ma index b2fb189e9..2a2aae51d 100644 --- a/matita/dama/integration_algebras.ma +++ b/matita/dama/integration_algebras.ma @@ -137,20 +137,6 @@ record f_algebra (K:ordered_field_ch0) : Type \def (* 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); diff --git a/matita/dama/ordered_fields_ch0.ma b/matita/dama/ordered_fields_ch0.ma index d95108eb3..f796ebb1d 100644 --- a/matita/dama/ordered_fields_ch0.ma +++ b/matita/dama/ordered_fields_ch0.ma @@ -16,8 +16,14 @@ set "baseuri" "cic:/matita/ordered_fields_ch0/". 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 *) @@ -68,7 +74,50 @@ lemma not_eq_x_zero_to_lt_zero_mult_x_x: 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 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