From: Claudio Sacerdoti Coen Date: Fri, 15 Dec 2006 10:39:07 +0000 (+0000) Subject: Huge DAMA update: X-Git-Tag: 0.4.95@7852~728 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dd3157d36216486d914a97cfff7a9cd34f009ffe;p=helm.git Huge DAMA update: 1. up to Fatou lemma (almost there) 2. requires the new unification procedure for coercions to enable multiple coercion paths between two nodes 3. it stresses CicUniv.mere_ugraphs. To compile the new DAMA file quickly you have to disable that function :-( --- diff --git a/matita/dama/constructive_connectives.ma b/matita/dama/constructive_connectives.ma index 461f90e6d..a0fb66ded 100644 --- a/matita/dama/constructive_connectives.ma +++ b/matita/dama/constructive_connectives.ma @@ -26,9 +26,9 @@ inductive ex (A:Type) (P:A→Prop) : Type \def notation < "hvbox(Σ ident i opt (: ty) break . p)" right associative with precedence 20 -for @{ 'exists ${default +for @{ 'sigma ${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 + (cic:/matita/constructive_connectives/ex.ind#xpointer(1/1) _ x). diff --git a/matita/dama/fields.ma b/matita/dama/fields.ma index 2aac4f446..305c49764 100644 --- a/matita/dama/fields.ma +++ b/matita/dama/fields.ma @@ -55,5 +55,6 @@ theorem inv_inverse: ∀F:field.∀x:F.∀p: x ≠ 0. (inv ? x p)*x = 1. apply (inv_inverse_ ? ? (field_properties F)). qed. +(*CSC: qua funzionava anche mettendo ? al posto della prima F*) definition sum_field ≝ - λF:field. sum ? (plus F) 0 1. + λF:field. sum F (plus F) 0 1. diff --git a/matita/dama/integration_algebras.ma b/matita/dama/integration_algebras.ma index 46bebc0e9..ca4309380 100644 --- a/matita/dama/integration_algebras.ma +++ b/matita/dama/integration_algebras.ma @@ -15,43 +15,16 @@ set "baseuri" "cic:/matita/integration_algebras/". include "vector_spaces.ma". +include "lattices.ma". -record is_lattice (C:Type) (join,meet:C→C→C) : Prop \def - { (* abelian semigroup properties *) - l_comm_j: symmetric ? join; - l_associative_j: associative ? join; - l_comm_m: symmetric ? meet; - l_associative_m: associative ? meet; - (* other properties *) - l_adsorb_j_m: ∀f,g. join f (meet f g) = f; - l_adsorb_m_j: ∀f,g. meet f (join f g) = f - }. - -record lattice (C:Type) : Type \def - { join: C → C → C; - meet: C → C → C; - l_lattice_properties: is_lattice ? join meet - }. - -definition le \def λC:Type.λL:lattice C.λf,g. meet ? L f g = f. - -interpretation "Lattice le" 'leq a b = - (cic:/matita/integration_algebras/le.con _ _ a b). - -definition lt \def λC:Type.λL:lattice C.λf,g. le ? L f g ∧ f ≠ g. - -interpretation "Lattice lt" 'lt a b = - (cic:/matita/integration_algebras/lt.con _ _ a b). - -definition carrier_of_lattice ≝ - λC:Type.λL:lattice C.C. +(**************** Riesz Spaces ********************) record is_riesz_space (K:ordered_field_ch0) (V:vector_space K) - (L:lattice (Type_OF_vector_space ? V)) + (L:lattice V) : Prop \def - { rs_compat_le_plus: ∀f,g,h. le ? L f g → le ? L (f+h) (g+h); - rs_compat_le_times: ∀a:K.∀f. of_le ? 0 a → le ? L 0 f → le ? L 0 (a*f) + { rs_compat_le_plus: ∀f,g,h:V. os_le ? L f g → os_le ? L (f+h) (g+h); + rs_compat_le_times: ∀a:K.∀f:V. zero K≤a → os_le ? L (zero V) f → os_le ? L (zero V) (a*f) }. record riesz_space (K:ordered_field_ch0) : Type \def @@ -60,41 +33,54 @@ record riesz_space (K:ordered_field_ch0) : Type \def rs_riesz_space_properties: is_riesz_space ? rs_vector_space rs_lattice }. +record is_positive_linear (K) (V:riesz_space K) (T:V→K) : Prop ≝ + { positive: ∀u:V. os_le ? V 0 u → os_le ? K 0 (T u); + linear1: ∀u,v:V. T (u+v) = T u + T v; + linear2: ∀u:V.∀k:K. T (k*u) = k*(T u) + }. + +record sequentially_order_continuous (K) (V:riesz_space K) (T:V→K) : Prop ≝ + { soc_incr: + ∀a:nat→V.∀l:V.is_increasing ? ? a → is_sup ? V a l → + is_increasing ? K (λn.T (a n)) ∧ tends_to ? (λn.T (a n)) (T l) + }. + definition absolute_value \def λK.λS:riesz_space K.λf.join ? S f (-f). -(*CSC: qui la notazione non fa capire!!! *) +(**************** Normed Riesz spaces ****************************) + definition is_riesz_norm ≝ - λR:real.λV:riesz_space R.λnorm:norm ? V. - ∀f,g:V. le ? V (absolute_value ? V f) (absolute_value ? V g) → - of_le R (norm f) (norm g). + λR:real.λV:riesz_space R.λnorm:norm R V. + ∀f,g:V. os_le ? V (absolute_value ? V f) (absolute_value ? V g) → + os_le ? R (n_function R V norm f) (n_function R V norm g). record riesz_norm (R:real) (V:riesz_space R) : Type ≝ - { rn_norm:> norm ? V; + { rn_norm:> norm R V; rn_riesz_norm_property: is_riesz_norm ? ? rn_norm }. (*CSC: non fa la chiusura delle coercion verso funclass *) definition rn_function ≝ λR:real.λV:riesz_space R.λnorm:riesz_norm ? V. - n_function ? ? (rn_norm ? ? norm). + n_function R V (rn_norm ? ? norm). coercion cic:/matita/integration_algebras/rn_function.con 1. (************************** L-SPACES *************************************) - +(* record is_l_space (R:real) (V:riesz_space R) (norm:riesz_norm ? V) : Prop ≝ { ls_banach: is_complete ? V (induced_distance ? ? norm); ls_linear: ∀f,g:V. le ? V 0 f → le ? V 0 g → norm (f+g) = norm f + norm g }. - +*) (******************** ARCHIMEDEAN RIESZ SPACES ***************************) record is_archimedean_riesz_space (K) (S:riesz_space K) : Prop \def - { ars_archimedean: ∃u.∀n.∀a.∀p:n > O. - le ? S + { ars_archimedean: ∃u:S.∀n.∀a.∀p:n > O. + os_le ? S (absolute_value ? S a) - ((inv ? (sum_field K n) (not_eq_sum_field_zero ? n p))* u) → + ((inv K (sum_field K n) (not_eq_sum_field_zero K n p))* u) → a = 0 }. @@ -103,13 +89,6 @@ record archimedean_riesz_space (K:ordered_field_ch0) : Type \def ars_archimedean_property: is_archimedean_riesz_space ? ars_riesz_space }. -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 (k*f) = k*(I f) - }. - definition is_weak_unit ≝ (* This definition is by Spitters. He cites Fremlin 353P, but: 1. that theorem holds only in f-algebras (as in Spitters, but we are @@ -129,7 +108,7 @@ record integration_riesz_space (R:real) : Type \def 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 ? ? integral; + irs_positive_linear: is_positive_linear ? ? integral; irs_limit1: ∀f:irs_archimedean_riesz_space. tends_to ? @@ -151,17 +130,18 @@ record integration_riesz_space (R:real) : Type \def definition induced_norm_fun ≝ λR:real.λV:integration_riesz_space R.λf:V. - integral ? ? (absolute_value ? ? f). + integral ? V (absolute_value ? ? f). lemma induced_norm_is_norm: - ∀R:real.∀V:integration_riesz_space R.is_norm ? V (induced_norm_fun ? V). + ∀R:real.∀V:integration_riesz_space R.is_norm R V (induced_norm_fun ? V). + elim daemon.(* intros; apply mk_is_norm; [ apply mk_is_semi_norm; [ unfold induced_norm_fun; intros; - apply i_positive; - [ apply (irs_integral_properties ? V) + apply positive; + [ apply (irs_positive_linear ? V) | (* difficile *) elim daemon ] @@ -182,7 +162,7 @@ lemma induced_norm_is_norm: rewrite < eq_zero_opp_zero; rewrite > zero_neutral; assumption - ]. + ].*) qed. definition induced_norm ≝ @@ -222,7 +202,7 @@ record complete_integration_riesz_space (R:real) : Type ≝ (* now we prove that any complete integration riesz space is an L-space *) -theorem is_l_space_l_space_induced_by_integral: +(*theorem is_l_space_l_space_induced_by_integral: ∀R:real.∀V:complete_integration_riesz_space R. is_l_space ? ? (induced_riesz_norm ? V). intros; @@ -237,7 +217,7 @@ theorem is_l_space_l_space_induced_by_integral: (* difficile *) elim daemon ]. -qed. +qed.*) (**************************** f-ALGEBRAS ********************************) diff --git a/matita/dama/lattices.ma b/matita/dama/lattices.ma new file mode 100644 index 000000000..0af365d00 --- /dev/null +++ b/matita/dama/lattices.ma @@ -0,0 +1,108 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lattices/". + +include "ordered_sets.ma". + +record pre_lattice (C:Type) : Type \def + { join_: C → C → C; + meet_: C → C → C + }. + +definition carrier_of_lattice ≝ λC:Type.λL:pre_lattice C.C. + +coercion cic:/matita/lattices/carrier_of_lattice.con. + +definition join : ∀C.∀L:pre_lattice C.L→L→L ≝ join_. +definition meet : ∀C.∀L:pre_lattice C.L→L→L ≝ meet_. + +interpretation "Lattice meet" 'and a b = + (cic:/matita/lattices/meet.con _ _ a b). + +interpretation "Lattice join" 'or a b = + (cic:/matita/lattices/join.con _ _ a b). + +record is_lattice (C:Type) (L:pre_lattice C) : Prop \def + { (* abelian semigroup properties *) + l_comm_j: symmetric ? (join ? L); + l_associative_j: associative ? (join ? L); + l_comm_m: symmetric ? (meet ? L); + l_associative_m: associative ? (meet ? L); + (* other properties *) + l_adsorb_j_m: ∀f,g:L. (f ∨ f ∧ g) = f; + l_adsorb_m_j: ∀f,g:L. (f ∧ (f ∨ g)) = f + }. + +record lattice (C:Type) : Type \def + { l_pre_lattice:> pre_lattice C; + l_lattice_properties:> is_lattice ? l_pre_lattice + }. + +definition le \def λC:Type.λL:lattice C.λf,g:L. (f ∧ g) = f. + +definition ordered_set_of_lattice: ∀C.lattice C → ordered_set C. + intros; + apply mk_ordered_set; + [ apply mk_pre_ordered_set; + apply (le ? l) + | apply mk_is_order_relation; + [ unfold reflexive; + intros; + unfold; + simplify; + unfold le; + change in x with (carrier_of_lattice ? l); + rewrite < (l_adsorb_j_m ? ? l ? x) in ⊢ (? ? (? ? ? ? %) ?); + rewrite > l_adsorb_m_j; + [ reflexivity + | apply (l_lattice_properties ? l) + ] + | intros; + unfold transitive; + simplify; + unfold le; + intros; + rewrite < H; + rewrite > (l_associative_m ? ? l); + rewrite > H1; + reflexivity + | unfold antisimmetric; + unfold os_le; + simplify; + unfold le; + intros; + rewrite < H; + rewrite > (l_comm_m ? ? l); + assumption + ] + ] +qed. + +coercion cic:/matita/lattices/ordered_set_of_lattice.con. + +(* +interpretation "Lattice le" 'leq a b = + (cic:/matita/integration_algebras/le.con _ _ a b). + +definition lt \def λC:Type.λL:lattice C.λf,g. le ? L f g ∧ f ≠ g. + +interpretation "Lattice lt" 'lt a b = + (cic:/matita/integration_algebras/lt.con _ _ a b). +*) + +(* The next coercion introduces a cycle in the coercion graph with + unexpected bad results +coercion cic:/matita/integration_algebras/carrier_of_lattice.con. +*) diff --git a/matita/dama/ordered_fields_ch0.ma b/matita/dama/ordered_fields_ch0.ma index c06ea743e..4a7b7a266 100644 --- a/matita/dama/ordered_fields_ch0.ma +++ b/matita/dama/ordered_fields_ch0.ma @@ -15,63 +15,71 @@ set "baseuri" "cic:/matita/ordered_fields_ch0/". include "fields.ma". +include "ordered_sets.ma". -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 - }. - -theorem to_transitive: - ∀C.∀le:C→C→Prop. is_total_order_relation ? le → transitive ? le. - intros; - unfold transitive; - intros; - elim (to_cotransitive ? ? i ? ? z H); - [ assumption - | rewrite < (to_antisimmetry ? ? i ? ? H1 t); - assumption - ]. -qed. - +(*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_total_order_relation:> is_total_order_relation ? le; - of_mult_compat: ∀a,b. le 0 a → le 0 b → le 0 (a*b); + { 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 *) - of_char0: ∀n. n > O → sum ? (plus F) 0 1 n ≠ 0 + (*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 { of_field:> field; - of_le: of_field → of_field → Prop; - of_ordered_field_properties:> is_ordered_field_ch0 ? of_le + 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) }. -interpretation "Ordered field le" 'leq a b = - (cic:/matita/ordered_fields_ch0/of_le.con _ a b). - -definition lt \def λF:ordered_field_ch0.λa,b:F.a ≤ b ∧ a ≠ b. +(*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) + ] + ]. +qed. -interpretation "Ordered field lt" 'lt a b = - (cic:/matita/ordered_fields_ch0/lt.con _ a b). +coercion cic:/matita/ordered_fields_ch0/ordered_set_of_ordered_field_ch0.con. +*) -lemma le_zero_x_to_le_opp_x_zero: ∀F:ordered_field_ch0.∀x:F. 0 ≤ x → -x ≤ 0. +(*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. + (*assumption*)apply H1. qed. -lemma le_x_zero_to_le_zero_opp_x: ∀F:ordered_field_ch0.∀x:F. x ≤ 0 → 0 ≤ -x. +(*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. + (*assumption.*) apply H1. qed. (* @@ -87,19 +95,21 @@ 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. 0 < x → 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 pre_ordered_set C; + os_order_relation_properties:> is_order_relation ? os_pre_ordered_set + }. + +theorem antisimmetric_to_cotransitive_to_transitive: + ∀C.∀le:relation C. antisimmetric ? le → cotransitive ? le → + transitive ? le. + intros; + unfold transitive; + intros; + elim (c ? ? z H1); + [ assumption + | rewrite < (H ? ? H2 t); + assumption + ]. +qed. + +definition is_increasing ≝ λC.λO:ordered_set C.λa:nat→O.∀n:nat.a n ≤ a (S n). +definition is_decreasing ≝ λC.λO:ordered_set C.λa:nat→O.∀n:nat.a (S n) ≤ a n. + +definition is_upper_bound ≝ λC.λO:ordered_set C.λa:nat→O.λu:O.∀n:nat.a n ≤ u. +definition is_lower_bound ≝ λC.λO:ordered_set C.λa:nat→O.λu:O.∀n:nat.u ≤ a n. + +record is_sup (C:Type) (O:ordered_set C) (a:nat→O) (u:O) : Prop ≝ + { sup_upper_bound: is_upper_bound ? O a u; + sup_least_upper_bound: ∀v:O. is_upper_bound ? O a v → u≤v + }. + +record is_inf (C:Type) (O:ordered_set C) (a:nat→O) (u:O) : Prop ≝ + { inf_lower_bound: is_lower_bound ? O a u; + inf_greatest_lower_bound: ∀v:O. is_lower_bound ? O a v → v≤u + }. + +record is_bounded_below (C:Type) (O:ordered_set C) (a:nat→O) : Type ≝ + { ib_lower_bound: O; + ib_lower_bound_is_lower_bound: is_lower_bound ? ? a ib_lower_bound + }. + +record is_bounded_above (C:Type) (O:ordered_set C) (a:nat→O) : Type ≝ + { ib_upper_bound: O; + ib_upper_bound_is_upper_bound: is_upper_bound ? ? a ib_upper_bound + }. + +record is_bounded (C:Type) (O:ordered_set C) (a:nat→O) : Type ≝ + { ib_bounded_below:> is_bounded_below ? ? a; + ib_bounded_above:> is_bounded_above ? ? a + }. + +record bounded_below_sequence (C:Type) (O:ordered_set C) : Type ≝ + { bbs_seq:1> nat→O; + bbs_is_bounded_below:> is_bounded_below ? ? bbs_seq + }. + +record bounded_above_sequence (C:Type) (O:ordered_set C) : Type ≝ + { bas_seq:1> nat→O; + bas_is_bounded_above:> is_bounded_above ? ? bas_seq + }. + +record bounded_sequence (C:Type) (O:ordered_set C) : Type ≝ + { bs_seq:1> nat → O; + bs_is_bounded_below: is_bounded_below ? ? bs_seq; + bs_is_bounded_above: is_bounded_above ? ? bs_seq + }. + +definition bounded_below_sequence_of_bounded_sequence ≝ + λC.λO:ordered_set C.λb:bounded_sequence ? O. + mk_bounded_below_sequence ? ? b (bs_is_bounded_below ? ? b). + +coercion cic:/matita/ordered_sets/bounded_below_sequence_of_bounded_sequence.con. + +definition bounded_above_sequence_of_bounded_sequence ≝ + λC.λO:ordered_set C.λb:bounded_sequence ? O. + mk_bounded_above_sequence ? ? b (bs_is_bounded_above ? ? b). + +coercion cic:/matita/ordered_sets/bounded_above_sequence_of_bounded_sequence.con. + +definition lower_bound ≝ + λC.λO:ordered_set C.λb:bounded_below_sequence ? O. + ib_lower_bound ? ? b (bbs_is_bounded_below ? ? b). + +lemma lower_bound_is_lower_bound: + ∀C.∀O:ordered_set C.∀b:bounded_below_sequence ? O. + is_lower_bound ? ? b (lower_bound ? ? b). + intros; + unfold lower_bound; + apply ib_lower_bound_is_lower_bound. +qed. + +definition upper_bound ≝ + λC.λO:ordered_set C.λb:bounded_above_sequence ? O. + ib_upper_bound ? ? b (bas_is_bounded_above ? ? b). + +lemma upper_bound_is_upper_bound: + ∀C.∀O:ordered_set C.∀b:bounded_above_sequence ? O. + is_upper_bound ? ? b (upper_bound ? ? b). + intros; + unfold upper_bound; + apply ib_upper_bound_is_upper_bound. +qed. + +record is_dedekind_sigma_complete (C:Type) (O:ordered_set C) : Type ≝ + { dsc_inf: ∀a:nat→O.∀m:O. is_lower_bound ? ? a m → ex ? (λs:O.is_inf ? O a s); + dsc_inf_proof_irrelevant: + ∀a:nat→O.∀m,m':O.∀p:is_lower_bound ? ? a m.∀p':is_lower_bound ? ? a m'. + (match dsc_inf a m p with [ ex_intro s _ ⇒ s ]) = + (match dsc_inf a m' p' with [ ex_intro s' _ ⇒ s' ]); + dsc_sup: ∀a:nat→O.∀m:O. is_upper_bound ? ? a m → ex ? (λs:O.is_sup ? O a s); + dsc_sup_proof_irrelevant: + ∀a:nat→O.∀m,m':O.∀p:is_upper_bound ? ? a m.∀p':is_upper_bound ? ? a m'. + (match dsc_sup a m p with [ ex_intro s _ ⇒ s ]) = + (match dsc_sup a m' p' with [ ex_intro s' _ ⇒ s' ]) + }. + +record dedekind_sigma_complete_ordered_set (C:Type) : Type ≝ + { dscos_ordered_set:> ordered_set C; + dscos_dedekind_sigma_complete_properties:> + is_dedekind_sigma_complete ? dscos_ordered_set + }. + +definition inf: + ∀C:Type.∀O:dedekind_sigma_complete_ordered_set C. + bounded_below_sequence ? O → O. + intros; + elim + (dsc_inf ? O (dscos_dedekind_sigma_complete_properties ? O) b); + [ apply a + | apply (lower_bound ? ? b) + | apply lower_bound_is_lower_bound + ] +qed. + +lemma inf_is_inf: + ∀C:Type.∀O:dedekind_sigma_complete_ordered_set C. + ∀a:bounded_below_sequence ? O. + is_inf ? ? a (inf ? ? a). + intros; + unfold inf; + simplify; + elim (dsc_inf C O (dscos_dedekind_sigma_complete_properties C O) a +(lower_bound C O a) (lower_bound_is_lower_bound C O a)); + simplify; + assumption. +qed. + +lemma inf_proof_irrelevant: + ∀C:Type.∀O:dedekind_sigma_complete_ordered_set C. + ∀a,a':bounded_below_sequence ? O. + bbs_seq ? ? a = bbs_seq ? ? a' → + inf ? ? a = inf ? ? a'. + intros 4; + elim a 0; + elim a'; + simplify in H; + generalize in match i1; + clear i1; + rewrite > H; + intro; + simplify; + rewrite < (dsc_inf_proof_irrelevant C O O f (ib_lower_bound ? ? f i2) + (ib_lower_bound ? ? f i) (ib_lower_bound_is_lower_bound ? ? f i2) + (ib_lower_bound_is_lower_bound ? ? f i)); + reflexivity. +qed. + +definition sup: + ∀C:Type.∀O:dedekind_sigma_complete_ordered_set C. + bounded_above_sequence ? O → O. + intros; + elim + (dsc_sup ? O (dscos_dedekind_sigma_complete_properties ? O) b); + [ apply a + | apply (upper_bound ? ? b) + | apply upper_bound_is_upper_bound + ]. +qed. + +lemma sup_is_sup: + ∀C:Type.∀O:dedekind_sigma_complete_ordered_set C. + ∀a:bounded_above_sequence ? O. + is_sup ? ? a (sup ? ? a). + intros; + unfold sup; + simplify; + elim (dsc_sup C O (dscos_dedekind_sigma_complete_properties C O) a +(upper_bound C O a) (upper_bound_is_upper_bound C O a)); + simplify; + assumption. +qed. + +lemma sup_proof_irrelevant: + ∀C:Type.∀O:dedekind_sigma_complete_ordered_set C. + ∀a,a':bounded_above_sequence ? O. + bas_seq ? ? a = bas_seq ? ? a' → + sup ? ? a = sup ? ? a'. + intros 4; + elim a 0; + elim a'; + simplify in H; + generalize in match i1; + clear i1; + rewrite > H; + intro; + simplify; + rewrite < (dsc_sup_proof_irrelevant C O O f (ib_upper_bound ? ? f i2) + (ib_upper_bound ? ? f i) (ib_upper_bound_is_upper_bound ? ? f i2) + (ib_upper_bound_is_upper_bound ? ? f i)); + reflexivity. +qed. + +axiom daemon: False. + +theorem inf_le_sup: + ∀C:Type.∀O:dedekind_sigma_complete_ordered_set C. + ∀a:bounded_sequence ? O. inf ? ? a ≤ sup ? ? a. + intros (C O'); + apply (or_transitive ? ? O' ? (a O)); + [ elim daemon (*apply (inf_lower_bound ? ? ? ? (inf_is_inf ? ? a))*) + | elim daemon (*apply (sup_upper_bound ? ? ? ? (sup_is_sup ? ? a))*) + ]. +qed. + +lemma inf_respects_le: + ∀C:Type.∀O:dedekind_sigma_complete_ordered_set C. + ∀a:bounded_below_sequence ? O.∀m:O. + is_upper_bound ? ? a m → inf ? ? a ≤ m. + intros (C O'); + apply (or_transitive ? ? O' ? (sup ? ? (mk_bounded_sequence ? ? a ? ?))); + [ apply (bbs_is_bounded_below ? ? a) + | apply (mk_is_bounded_above ? ? ? m H) + | apply inf_le_sup + | apply + (sup_least_upper_bound ? ? ? ? + (sup_is_sup ? ? (mk_bounded_sequence C O' a a + (mk_is_bounded_above C O' a m H)))); + assumption + ]. +qed. + +definition is_sequentially_monotone ≝ + λC.λO:ordered_set C.λf:O→O. + ∀a:nat→O.∀p:is_increasing ? ? a. + is_increasing ? ? (λi.f (a i)). + +record is_order_continuous (C) + (O:dedekind_sigma_complete_ordered_set C) (f:O→O) : Prop +≝ + { ioc_is_sequentially_monotone: is_sequentially_monotone ? ? f; + ioc_is_upper_bound_f_sup: + ∀a:bounded_above_sequence ? O. + is_upper_bound ? ? (λi.f (a i)) (f (sup ? ? a)); + ioc_respects_sup: + ∀a:bounded_above_sequence ? O. + is_increasing ? ? a → + f (sup ? ? a) = + sup ? ? (mk_bounded_above_sequence ? ? (λi.f (a i)) + (mk_is_bounded_above ? ? ? (f (sup ? ? a)) + (ioc_is_upper_bound_f_sup a))); + ioc_is_lower_bound_f_inf: + ∀a:bounded_below_sequence ? O. + is_lower_bound ? ? (λi.f (a i)) (f (inf ? ? a)); + ioc_respects_inf: + ∀a:bounded_below_sequence ? O. + is_decreasing ? ? a → + f (inf ? ? a) = + inf ? ? (mk_bounded_below_sequence ? ? (λi.f (a i)) + (mk_is_bounded_below ? ? ? (f (inf ? ? a)) + (ioc_is_lower_bound_f_inf a))) + }. + +theorem tail_inf_increasing: + ∀C.∀O:dedekind_sigma_complete_ordered_set C. + ∀a:bounded_below_sequence ? O. + let y ≝ λi.mk_bounded_below_sequence ? ? (λj.a (i+j)) ? in + let x ≝ λi.inf ? ? (y i) in + is_increasing ? ? x. + [ apply (mk_is_bounded_below ? ? ? (ib_lower_bound ? ? a a)); + simplify; + intro; + apply (ib_lower_bound_is_lower_bound ? ? a a) + | intros; + unfold is_increasing; + intro; + unfold x in ⊢ (? ? ? ? %); + apply (inf_greatest_lower_bound ? ? ? ? (inf_is_inf ? ? (y (S n)))); + change with (is_lower_bound ? ? (y (S n)) (inf ? ? (y n))); + unfold is_lower_bound; + intro; + generalize in match (inf_lower_bound ? ? ? ? (inf_is_inf ? ? (y n)) (S n1)); + (*CSC: coercion per FunClass inserita a mano*) + suppose (inf ? ? (y n) ≤ bbs_seq ? ? (y n) (S n1)) (H); + cut (bbs_seq ? ? (y n) (S n1) = bbs_seq ? ? (y (S n)) n1); + [ rewrite < Hcut; + assumption + | unfold y; + simplify; + auto paramodulation library + ] + ]. +qed. + +definition is_liminf: + ∀C:Type.∀O:dedekind_sigma_complete_ordered_set C. + bounded_below_sequence ? O → O → Prop. + intros; + apply + (is_sup ? ? (λi.inf ? ? (mk_bounded_below_sequence ? ? (λj.b (i+j)) ?)) t); + apply (mk_is_bounded_below ? ? ? (ib_lower_bound ? ? b b)); + simplify; + intros; + apply (ib_lower_bound_is_lower_bound ? ? b b). +qed. + +definition liminf: + ∀C:Type.∀O:dedekind_sigma_complete_ordered_set C. + bounded_sequence ? O → O. + intros; + apply + (sup ? ? + (mk_bounded_above_sequence ? ? + (λi.inf ? ? + (mk_bounded_below_sequence ? ? + (λj.b (i+j)) ?)) ?)); + [ apply (mk_is_bounded_below ? ? ? (ib_lower_bound ? ? b b)); + simplify; + intros; + apply (ib_lower_bound_is_lower_bound ? ? b b) + | apply (mk_is_bounded_above ? ? ? (ib_upper_bound ? ? b b)); + unfold is_upper_bound; + intro; + change with + (inf C O + (mk_bounded_below_sequence C O (\lambda j:nat.b (n+j)) + (mk_is_bounded_below C O (\lambda j:nat.b (n+j)) (ib_lower_bound C O b b) + (\lambda j:nat.ib_lower_bound_is_lower_bound C O b b (n+j)))) +\leq ib_upper_bound C O b b); + apply (inf_respects_le ? O); + simplify; + intro; + apply (ib_upper_bound_is_upper_bound ? ? b b) + ]. +qed. + +notation "hvbox(〈a〉)" + non associative with precedence 45 +for @{ 'hide_everything_but $a }. + +interpretation "mk_bounded_above_sequence" 'hide_everything_but a += (cic:/matita/ordered_sets/bounded_above_sequence.ind#xpointer(1/1/1) _ _ a _). + +interpretation "mk_bounded_below_sequence" 'hide_everything_but a += (cic:/matita/ordered_sets/bounded_below_sequence.ind#xpointer(1/1/1) _ _ a _). + +theorem eq_f_sup_sup_f: + ∀C.∀O':dedekind_sigma_complete_ordered_set C. + ∀f:O'→O'. ∀H:is_order_continuous ? ? f. + ∀a:bounded_above_sequence ? O'. + ∀p:is_increasing ? ? a. + f (sup ? ? a) = sup ? ? (mk_bounded_above_sequence ? ? (λi.f (a i)) ?). + [ apply (mk_is_bounded_above ? ? ? (f (sup ? ? a))); + apply ioc_is_upper_bound_f_sup; + assumption + | intros; + apply ioc_respects_sup; + assumption + ]. +qed. + +theorem eq_f_sup_sup_f': + ∀C.∀O':dedekind_sigma_complete_ordered_set C. + ∀f:O'→O'. ∀H:is_order_continuous ? ? f. + ∀a:bounded_above_sequence ? O'. + ∀p:is_increasing ? ? a. + ∀p':is_bounded_above ? ? (λi.f (a i)). + f (sup ? ? a) = sup ? ? (mk_bounded_above_sequence ? ? (λi.f (a i)) p'). + intros; + rewrite > (eq_f_sup_sup_f ? ? f H a H1); + apply sup_proof_irrelevant; + reflexivity. +qed. + +theorem eq_f_liminf_sup_f_inf: + ∀C.∀O':dedekind_sigma_complete_ordered_set C. + ∀f:O'→O'. ∀H:is_order_continuous ? ? f. + ∀a:bounded_sequence ? O'. + let p1 := ? in + f (liminf ? ? a) = + sup ? ? + (mk_bounded_above_sequence ? ? + (λi.f (inf ? ? + (mk_bounded_below_sequence ? ? + (λj.a (i+j)) + ?))) + p1). + [ apply (mk_is_bounded_below ? ? ? (ib_lower_bound ? ? a a)); + simplify; + intro; + apply (ib_lower_bound_is_lower_bound ? ? a a) + | apply (mk_is_bounded_above ? ? ? (f (sup ? ? a))); + unfold is_upper_bound; + intro; + apply (or_transitive ? ? O' ? (f (a n))); + [ generalize in match (ioc_is_lower_bound_f_inf ? ? ? H); + intro H1; + simplify in H1; + rewrite > (plus_n_O n) in ⊢ (? ? ? ? (? (? ? ? ? %))); + apply (H1 (mk_bounded_below_sequence C O' (\lambda j:nat.a (n+j)) +(mk_is_bounded_below C O' (\lambda j:nat.a (n+j)) (ib_lower_bound C O' a a) + (\lambda j:nat.ib_lower_bound_is_lower_bound C O' a a (n+j)))) O); + | elim daemon (*apply (ioc_is_upper_bound_f_sup ? ? ? H)*) + ] + | intros; + unfold liminf; + clearbody p1; + generalize in match (\lambda n:nat +.inf_respects_le C O' + (mk_bounded_below_sequence C O' (\lambda j:nat.a (plus n j)) + (mk_is_bounded_below C O' (\lambda j:nat.a (plus n j)) + (ib_lower_bound C O' a a) + (\lambda j:nat.ib_lower_bound_is_lower_bound C O' a a (plus n j)))) + (ib_upper_bound C O' a a) + (\lambda n1:nat.ib_upper_bound_is_upper_bound C O' a a (plus n n1))); + intro p2; + apply (eq_f_sup_sup_f' ? ? f H (mk_bounded_above_sequence C O' +(\lambda i:nat + .inf C O' + (mk_bounded_below_sequence C O' (\lambda j:nat.a (plus i j)) + (mk_is_bounded_below C O' (\lambda j:nat.a (plus i j)) + (ib_lower_bound C O' a a) + (\lambda n:nat.ib_lower_bound_is_lower_bound C O' a a (plus i n))))) +(mk_is_bounded_above C O' + (\lambda i:nat + .inf C O' + (mk_bounded_below_sequence C O' (\lambda j:nat.a (plus i j)) + (mk_is_bounded_below C O' (\lambda j:nat.a (plus i j)) + (ib_lower_bound C O' a a) + (\lambda n:nat.ib_lower_bound_is_lower_bound C O' a a (plus i n))))) + (ib_upper_bound C O' a a) p2))); + unfold bas_seq; + change with + (is_increasing ? ? (\lambda i:nat +.inf C O' + (mk_bounded_below_sequence C O' (\lambda j:nat.a (plus i j)) + (mk_is_bounded_below C O' (\lambda j:nat.a (plus i j)) + (ib_lower_bound C O' a a) + (\lambda n:nat.ib_lower_bound_is_lower_bound C O' a a (plus i n)))))); + apply tail_inf_increasing + ]. +qed. + + + + +definition lt ≝ λC.λO:ordered_set C.λa,b:O.a ≤ b ∧ a ≠ b. + +interpretation "Ordered set lt" 'lt a b = + (cic:/matita/ordered_sets/lt.con _ _ a b). \ No newline at end of file diff --git a/matita/dama/ordered_sets2.ma b/matita/dama/ordered_sets2.ma new file mode 100644 index 000000000..b597d372c --- /dev/null +++ b/matita/dama/ordered_sets2.ma @@ -0,0 +1,92 @@ +(**************************************************************************) +(* ___ *) +(* ||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/ordered_sets2". + +include "ordered_sets.ma". + +theorem le_f_inf_inf_f: + ∀C.∀O':dedekind_sigma_complete_ordered_set C. + ∀f:O'→O'. ∀H:is_order_continuous ? ? f. + ∀a:bounded_below_sequence ? O'. + let p := ? in + f (inf ? ? a) ≤ inf ? ? (mk_bounded_below_sequence ? ? (λi. f (a i)) p). + [ apply mk_is_bounded_below; + [2: apply ioc_is_lower_bound_f_inf; + assumption + | skip + ] + | intros; + clearbody p; + apply (inf_greatest_lower_bound ? ? ? ? (inf_is_inf ? ? ?)); + simplify; + intro; + letin b := (λi.match i with [ O ⇒ inf ? ? a | S _ ⇒ a n]); + change with (f (b O) ≤ f (b (S O))); + apply (ioc_is_sequentially_monotone ? ? ? H); + simplify; + clear b; + intro; + elim n1; simplify; + [ apply (inf_lower_bound ? ? ? ? (inf_is_inf ? ? ?)); + | apply (or_reflexive ? O' (dscos_ordered_set ? O')) + ] + ]. +qed. + +theorem le_to_le_sup_sup: + ∀C.∀O':dedekind_sigma_complete_ordered_set C. + ∀a,b:bounded_above_sequence ? O'. + (∀i.a i ≤ b i) → sup ? ? a ≤ sup ? ? b. + intros; + apply (sup_least_upper_bound ? ? ? ? (sup_is_sup ? ? a)); + unfold; + intro; + apply (or_transitive ? ? O'); + [2: apply H + | skip + | apply (sup_upper_bound ? ? ? ? (sup_is_sup ? ? b)) + ]. +qed. + +interpretation "mk_bounded_sequence" 'hide_everything_but a += (cic:/matita/ordered_sets/bounded_sequence.ind#xpointer(1/1/1) _ _ a _ _). + +theorem fatou: + ∀C.∀O':dedekind_sigma_complete_ordered_set C. + ∀f:O'→O'. ∀H:is_order_continuous ? ? f. + ∀a:bounded_sequence ? O'. + let pb := ? in + let pa := ? in + f (liminf ? ? a) ≤ liminf ? ? (mk_bounded_sequence ? ? (λi. f (a i)) pb pa). + [ letin bas ≝ (bounded_above_sequence_of_bounded_sequence ? ? a); + apply mk_is_bounded_above; + [2: apply (ioc_is_upper_bound_f_sup ? ? ? H bas) + | skip + ] + | letin bbs ≝ (bounded_below_sequence_of_bounded_sequence ? ? a); + apply mk_is_bounded_below; + [2: apply (ioc_is_lower_bound_f_inf ? ? ? H bbs) + | skip + ] + | intros; + rewrite > eq_f_liminf_sup_f_inf; + [ unfold liminf; + apply le_to_le_sup_sup; + elim daemon (*(* f inf < inf f *) + apply le_f_inf_inf_f*) + | assumption + ] + ]. +qed. diff --git a/matita/dama/reals.ma b/matita/dama/reals.ma index 63f487899..9e458e291 100644 --- a/matita/dama/reals.ma +++ b/matita/dama/reals.ma @@ -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 ? (S n)) ?) (x-y)); + elim (of_cotransitive R 0 (inv ? (sum_field ? (S n)) ?) (x-y)); [ apply x | apply not_eq_sum_field_zero ; unfold; @@ -48,19 +48,21 @@ qed. axiom daemon: False. theorem cauchy_max_seq: ∀R:real.∀x,y:R. is_cauchy_seq ? (max_seq ? x y). +elim daemon. +(* intros; unfold; intros; exists; [ exact m | ]; (* apply (ex_intro ? ? m); *) intros; unfold max_seq; - elim (to_cotransitive R (of_le R) R 0 + elim (of_cotransitive 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 + elim (of_cotransitive 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) @@ -75,16 +77,15 @@ theorem cauchy_max_seq: ∀R:real.∀x,y:R. is_cauchy_seq ? (max_seq ? x y). ] | simplify; split; - [ apply (to_transitive ? ? - (of_total_order_relation ? ? R) ? 0 ?); - [ apply (le_zero_x_to_le_opp_x_zero R ?) - | assumption - ] + [ apply (or_transitive ? ? R ? 0); + [ apply (le_zero_x_to_le_opp_x_zero R ?) + | assumption + ] | assumption ] ] | simplify; - elim (to_cotransitive R (of_le R) R 0 + elim (of_cotransitive 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) @@ -98,7 +99,7 @@ theorem cauchy_max_seq: ∀R:real.∀x,y:R. is_cauchy_seq ? (max_seq ? x y). 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 ?); + apply (or_transitive ? ? R ? 0); [ assumption | apply lt_zero_to_le_inv_zero ] @@ -112,7 +113,7 @@ theorem cauchy_max_seq: ∀R:real.∀x,y:R. is_cauchy_seq ? (max_seq ? x y). ] ] ]. - elim daemon. + elim daemon.*) qed. definition max: ∀R:real.R → R → R. @@ -146,7 +147,7 @@ lemma technical1: ∀R:real.lim R (to_zero R) (is_cauchy_seq_to_zero R) = 0. elim daemon. qed. -lemma abs_x_ge_O: \forall R: real. \forall x:R. 0 ≤ abs R x. +lemma abs_x_ge_O: \forall R: real. \forall x:R. (zero R) ≤ abs R x. intros; unfold abs; unfold max; @@ -156,7 +157,7 @@ lemma abs_x_ge_O: \forall R: real. \forall x:R. 0 ≤ abs R x. unfold to_zero; unfold max_seq; elim - (to_cotransitive R (of_le R) R 0 + (of_cotransitive 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--x) (lt_zero_to_le_inv_zero R (S n) diff --git a/matita/dama/rings.ma b/matita/dama/rings.ma index ec460748b..3ed2fab25 100644 --- a/matita/dama/rings.ma +++ b/matita/dama/rings.ma @@ -91,7 +91,8 @@ intros; generalize in match (zero_neutral R 0); intro; generalize in match (eq_f ? ? (λy.x*y) ? ? H); intro; clear H; -rewrite > mult_plus_distr_left in H1; +(*CSC: qua funzionava prima della patch all'unificazione!*) +rewrite > (mult_plus_distr_left R) in H1; generalize in match (eq_f ? ? (λy. (-(x*0)) +y) ? ? H1);intro; clear H1; rewrite < plus_assoc in H; diff --git a/matita/dama/vector_spaces.ma b/matita/dama/vector_spaces.ma index c20b3ca8b..3165be2e6 100644 --- a/matita/dama/vector_spaces.ma +++ b/matita/dama/vector_spaces.ma @@ -34,7 +34,7 @@ interpretation "Vector space external product" 'times a b = (cic:/matita/vector_spaces/emult.con _ _ a b). record is_semi_norm (R:real) (V: vector_space R) (semi_norm:V→R) : Prop \def - { sn_positive: ∀x:V. 0 ≤ semi_norm x; + { sn_positive: ∀x:V. zero R ≤ semi_norm x; sn_omogeneous: ∀a:R.∀x:V. semi_norm (a*x) = (abs ? a) * semi_norm x; sn_triangle_inequality: ∀x,y:V. semi_norm (x + y) ≤ semi_norm x + semi_norm y }. @@ -59,7 +59,7 @@ record norm (R:real) (V:vector_space R) : Type ≝ }. record is_semi_distance (R:real) (C:Type) (semi_d: C→C→R) : Prop ≝ - { sd_positive: ∀x,y:C. 0 ≤ semi_d x y; + { sd_positive: ∀x,y:C. zero R ≤ semi_d x y; sd_properness: ∀x:C. semi_d x x = 0; sd_triangle_inequality: ∀x,y,z:C. semi_d x z ≤ semi_d x y + semi_d z y }. @@ -81,6 +81,7 @@ definition induced_distance_fun ≝ theorem induced_distance_is_distance: ∀R:real.∀V:vector_space R.∀norm:norm ? V. is_distance ? ? (induced_distance_fun ? ? norm). +elim daemon.(* intros; apply mk_is_distance; [ apply mk_is_semi_distance; @@ -110,7 +111,7 @@ theorem induced_distance_is_distance: elim daemon | apply (n_norm_properties ? ? norm) ] - ]. + ].*) qed. definition induced_distance ≝ @@ -120,8 +121,6 @@ definition induced_distance ≝ definition tends_to : ∀R:real.∀V:vector_space R.∀d:distance ? V.∀f:nat→V.∀l:V.Prop. - alias symbol "leq" = "Ordered field le". - alias id "le" = "cic:/matita/nat/orders/le.ind#xpointer(1/1)". apply (λR:real.λV:vector_space R.λd:distance ? V.λf:nat→V.λl:V. ∀n:nat.∃m:nat.∀j:nat. le m j →