From b098ae0cb12a818332cb3241ccaf76f99c4221a5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 29 Dec 2006 14:08:44 +0000 Subject: [PATCH] First attempt at using/simulating records with manifest types to encode mathematical structures that form a DAG. So far it works quite well, but the generation of the "coerced" projection should be automated. Something to write a paper on. --- matita/dama/integration_algebras.ma | 68 ++-- matita/dama/lattices.ma | 85 ++--- matita/dama/ordered_fields_ch0.ma | 110 +++--- matita/dama/ordered_sets.ma | 529 ++++++++++++++-------------- matita/dama/ordered_sets2.ma | 65 ++-- matita/dama/reals.ma | 4 +- 6 files changed, 432 insertions(+), 429 deletions(-) diff --git a/matita/dama/integration_algebras.ma b/matita/dama/integration_algebras.ma index ca4309380..fdf082df3 100644 --- a/matita/dama/integration_algebras.ma +++ b/matita/dama/integration_algebras.ma @@ -19,40 +19,66 @@ include "lattices.ma". (**************** Riesz Spaces ********************) -record is_riesz_space (K:ordered_field_ch0) (V:vector_space K) - (L:lattice V) -: Prop -\def - { 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 pre_riesz_space (K:ordered_field_ch0) : Type \def + { rs_vector_space:> vector_space K; + rs_lattice_: lattice; + rs_with: os_carrier rs_lattice_ = rs_vector_space + }. + +lemma rs_lattice: ∀K:ordered_field_ch0.pre_riesz_space K → lattice. + intros (K V); + apply mk_lattice; + [ apply (carrier V) + | apply (eq_rect ? ? (λC:Type.C→C→C) ? ? (rs_with ? V)); + apply l_join + | apply (eq_rect ? ? (λC:Type.C→C→C) ? ? (rs_with ? V)); + apply l_meet + | apply + (eq_rect' ? ? + (λa:Type.λH:os_carrier (rs_lattice_ ? V)=a. + is_lattice a + (eq_rect Type (rs_lattice_ K V) (λC:Type.C→C→C) + (l_join (rs_lattice_ K V)) a H) + (eq_rect Type (rs_lattice_ K V) (λC:Type.C→C→C) + (l_meet (rs_lattice_ K V)) a H)) + ? ? (rs_with ? V)); + simplify; + apply l_lattice_properties + ]. +qed. + +coercion cic:/matita/integration_algebras/rs_lattice.con. + +record is_riesz_space (K:ordered_field_ch0) (V:pre_riesz_space K) : Prop ≝ + { rs_compat_le_plus: ∀f,g,h:V. f≤g → f+h≤g+h; + rs_compat_le_times: ∀a:K.∀f:V. zero K≤a → zero V≤f → zero V≤a*f }. record riesz_space (K:ordered_field_ch0) : Type \def - { rs_vector_space:> vector_space K; - rs_lattice:> lattice rs_vector_space; - rs_riesz_space_properties: is_riesz_space ? rs_vector_space rs_lattice + { rs_pre_riesz_space:> pre_riesz_space K; + rs_riesz_space_properties: is_riesz_space ? rs_pre_riesz_space }. 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); + { 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) + ∀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). +definition absolute_value \def λK.λS:riesz_space K.λf.l_join S f (-f). (**************** Normed Riesz spaces ****************************) definition is_riesz_norm ≝ λ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). + ∀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 R V; @@ -78,7 +104,7 @@ record is_l_space (R:real) (V:riesz_space R) (norm:riesz_norm ? V) : Prop ≝ record is_archimedean_riesz_space (K) (S:riesz_space K) : Prop \def { ars_archimedean: ∃u:S.∀n.∀a.∀p:n > O. - os_le ? S + os_le S (absolute_value ? S a) ((inv K (sum_field K n) (not_eq_sum_field_zero K n p))* u) → a = 0 @@ -99,7 +125,7 @@ definition is_weak_unit ≝ 3. Fremlin proves u > 0 implies x /\ u > 0 > 0 for Archimedean spaces only. We pick this definition for now. *) λR:real.λV:archimedean_riesz_space R.λe:V. - ∀v:V. lt ? V 0 v → lt ? V 0 (meet ? V v e). + ∀v:V. lt V 0 v → lt V 0 (l_meet V v e). (* Here we are avoiding a construction (the quotient space to define f=g iff I(|f-g|)=0 *) @@ -112,14 +138,14 @@ record integration_riesz_space (R:real) : Type \def irs_limit1: ∀f:irs_archimedean_riesz_space. tends_to ? - (λn.integral (meet ? irs_archimedean_riesz_space f + (λn.integral (l_meet irs_archimedean_riesz_space f ((sum_field R n)*irs_unit))) (integral f); irs_limit2: ∀f:irs_archimedean_riesz_space. tends_to ? (λn. - integral (meet ? irs_archimedean_riesz_space f + integral (l_meet irs_archimedean_riesz_space f ((inv ? (sum_field R (S n)) (not_eq_sum_field_zero R (S n) (le_S_S O n (le_O_n n))) ) * irs_unit))) 0; @@ -250,10 +276,10 @@ record is_f_algebra (K) (S:archimedean_riesz_space K) (one: S) \def { compat_mult_le: ∀f,g:S. - le ? S 0 f → le ? S 0 g → le ? S 0 (a_mult ? ? ? A f g); + os_le S 0 f → os_le S 0 g → os_le S 0 (a_mult ? ? ? A f g); compat_mult_meet: ∀f,g,h:S. - meet ? S f g = 0 → meet ? S (a_mult ? ? ? A h f) g = 0 + l_meet S f g = 0 → l_meet S (a_mult ? ? ? A h f) g = 0 }. record f_algebra (K:ordered_field_ch0) (R:archimedean_riesz_space K) (one:R) : diff --git a/matita/dama/lattices.ma b/matita/dama/lattices.ma index 0af365d00..8f2aa763d 100644 --- a/matita/dama/lattices.ma +++ b/matita/dama/lattices.ma @@ -16,93 +16,62 @@ set "baseuri" "cic:/matita/lattices/". include "ordered_sets.ma". -record pre_lattice (C:Type) : Type \def - { join_: C → C → C; - meet_: C → C → C +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:C. join f (meet f g) = f; + l_adsorb_m_j: ∀f,g:C. meet f (join f g) = f }. -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_. +record lattice : Type \def + { l_carrier:> Type; + l_join: l_carrier→l_carrier→l_carrier; + l_meet: l_carrier→l_carrier→l_carrier; + l_lattice_properties:> is_lattice ? l_join l_meet + }. interpretation "Lattice meet" 'and a b = - (cic:/matita/lattices/meet.con _ _ a b). + (cic:/matita/lattices/l_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 - }. + (cic:/matita/lattices/l_join.con _ a b). -definition le \def λC:Type.λL:lattice C.λf,g:L. (f ∧ g) = f. +definition le \def λL:lattice.λf,g:L. (f ∧ g) = f. -definition ordered_set_of_lattice: ∀C.lattice C → ordered_set C. - intros; +definition ordered_set_of_lattice: lattice → ordered_set. + intros (L); apply mk_ordered_set; - [ apply mk_pre_ordered_set; - apply (le ? l) + [2: apply (le L) + | skip | 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_j_m ? ? ? L ? x) in ⊢ (? ? (? ? ? %) ?); rewrite > l_adsorb_m_j; [ reflexivity - | apply (l_lattice_properties ? l) + | apply (l_lattice_properties L) ] | intros; unfold transitive; - simplify; unfold le; intros; rewrite < H; - rewrite > (l_associative_m ? ? l); + rewrite > (l_associative_m ? ? ? L); rewrite > H1; reflexivity | unfold antisimmetric; - unfold os_le; - simplify; unfold le; intros; rewrite < H; - rewrite > (l_comm_m ? ? l); + 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. -*) +coercion cic:/matita/lattices/ordered_set_of_lattice.con. \ No newline at end of file diff --git a/matita/dama/ordered_fields_ch0.ma b/matita/dama/ordered_fields_ch0.ma index 4a7b7a266..07f32fade 100644 --- a/matita/dama/ordered_fields_ch0.ma +++ b/matita/dama/ordered_fields_ch0.ma @@ -15,71 +15,83 @@ set "baseuri" "cic:/matita/ordered_fields_ch0/". include "fields.ma". -include "ordered_sets.ma". +include "ordered_sets2.ma". (*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_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 *) - (*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 + +record pre_ordered_field_ch0: Type ≝ { of_field:> field; - 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) + of_cotransitively_ordered_set_: cotransitively_ordered_set; + of_with: os_carrier of_cotransitively_ordered_set_ = carrier of_field }. -(*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) - ] - ]. +(*CSC: the following lemma (that is also a coercion) should be automatically + generated *) +lemma of_cotransitively_ordered_set : pre_ordered_field_ch0 → cotransitively_ordered_set. + intro F; + apply mk_cotransitively_ordered_set; + [ apply mk_ordered_set; + [ apply (carrier F) + | apply + (eq_rect ? ? (λC:Type.C→C→Prop) (os_le (of_cotransitively_ordered_set_ F)) ? (of_with F)) + | apply + (eq_rect' Type (os_carrier (of_cotransitively_ordered_set_ F)) + (λa:Type.λH:os_carrier (of_cotransitively_ordered_set_ F)=a. + is_order_relation a (eq_rect Type (os_carrier (of_cotransitively_ordered_set_ F)) (λC:Type.C→C→Prop) (os_le (of_cotransitively_ordered_set_ F)) a H)) + ? (Type_OF_pre_ordered_field_ch0 F) (of_with F)); + simplify; + apply (os_order_relation_properties (of_cotransitively_ordered_set_ F)) + ] + | simplify; + apply + (eq_rect' ? ? + (λa:Type.λH:os_carrier (of_cotransitively_ordered_set_ F)=a. + cotransitive a + match H in eq + return + λa2:Type.λH1:os_carrier (of_cotransitively_ordered_set_ F)=a2. + a2→a2→Prop + with + [refl_eq ⇒ os_le (of_cotransitively_ordered_set_ F)]) + ? ? (of_with F)); + simplify; + apply cos_cotransitive + ]. qed. -coercion cic:/matita/ordered_fields_ch0/ordered_set_of_ordered_field_ch0.con. -*) +coercion cic:/matita/ordered_fields_ch0/of_cotransitively_ordered_set.con. -(*interpretation "Ordered field le" 'leq a b = - (cic:/matita/ordered_fields_ch0/of_le.con _ a b). - *) +record is_ordered_field_ch0 (F:pre_ordered_field_ch0) : Type \def + { of_mult_compat: ∀a,b:F. 0≤a → 0≤b → 0≤a*b; + of_plus_compat: ∀a,b,c:F. a≤b → a+c≤b+c; + of_weak_tricotomy : ∀a,b:F. a≠b → a≤b ∨ b≤a; + (* 0 characteristics *) + of_char0: ∀n. n > O → sum ? (plus F) 0 1 n ≠ 0 + }. + +record ordered_field_ch0 : Type \def + { of_pre_ordered_field_ch0:> pre_ordered_field_ch0; + of_ordered_field_properties:> is_ordered_field_ch0 of_pre_ordered_field_ch0 + }. -(*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; +lemma le_zero_x_to_le_opp_x_zero: ∀F:ordered_field_ch0.∀x:F.0 ≤ 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*)apply H1. + assumption. qed. -(*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. +lemma le_x_zero_to_le_zero_opp_x: ∀F:ordered_field_ch0.∀x:F. x ≤ 0 → 0 ≤ -x. intros; - generalize in match (of_plus_compat ? ? F ? ? (-x) H); intro; + 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.*) apply H1. + assumption. qed. (* @@ -95,16 +107,16 @@ 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. lt ? F 0 x → lt ? F 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 +record ordered_set: Type ≝ + { os_carrier:> Type; + os_le: os_carrier → os_carrier → Prop; + os_order_relation_properties:> is_order_relation ? os_le }. +interpretation "Ordered Sets le" 'leq a b = + (cic:/matita/ordered_sets/os_le.con _ a b). + theorem antisimmetric_to_cotransitive_to_transitive: ∀C.∀le:relation C. antisimmetric ? le → cotransitive ? le → transitive ? le. @@ -60,139 +52,139 @@ theorem antisimmetric_to_cotransitive_to_transitive: ]. 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_increasing ≝ λO:ordered_set.λa:nat→O.∀n:nat.a n ≤ a (S n). +definition is_decreasing ≝ λO:ordered_set.λ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. +definition is_upper_bound ≝ λO:ordered_set.λa:nat→O.λu:O.∀n:nat.a n ≤ u. +definition is_lower_bound ≝ λO:ordered_set.λ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_sup (O:ordered_set) (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_inf (O:ordered_set) (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 ≝ +record is_bounded_below (O:ordered_set) (a:nat→O) : Type ≝ { ib_lower_bound: O; - ib_lower_bound_is_lower_bound: is_lower_bound ? ? a ib_lower_bound + 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 ≝ +record is_bounded_above (O:ordered_set) (a:nat→O) : Type ≝ { ib_upper_bound: O; - ib_upper_bound_is_upper_bound: is_upper_bound ? ? a ib_upper_bound + 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 is_bounded (O:ordered_set) (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 ≝ +record bounded_below_sequence (O:ordered_set) : Type ≝ { bbs_seq:1> nat→O; - bbs_is_bounded_below:> is_bounded_below ? ? bbs_seq + bbs_is_bounded_below:> is_bounded_below ? bbs_seq }. -record bounded_above_sequence (C:Type) (O:ordered_set C) : Type ≝ +record bounded_above_sequence (O:ordered_set) : Type ≝ { bas_seq:1> nat→O; - bas_is_bounded_above:> is_bounded_above ? ? bas_seq + bas_is_bounded_above:> is_bounded_above ? bas_seq }. -record bounded_sequence (C:Type) (O:ordered_set C) : Type ≝ +record bounded_sequence (O:ordered_set) : Type ≝ { bs_seq:1> nat → O; - bs_is_bounded_below: is_bounded_below ? ? bs_seq; - bs_is_bounded_above: is_bounded_above ? ? bs_seq + 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). + λO:ordered_set.λ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). + λO:ordered_set.λ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). + λO:ordered_set.λ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). + ∀O:ordered_set.∀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). + λO:ordered_set.λ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). + ∀O:ordered_set.∀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); +record is_dedekind_sigma_complete (O:ordered_set) : 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'. + ∀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: ∀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'. + ∀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; +record dedekind_sigma_complete_ordered_set : Type ≝ + { dscos_ordered_set:> ordered_set; dscos_dedekind_sigma_complete_properties:> - is_dedekind_sigma_complete ? dscos_ordered_set + is_dedekind_sigma_complete dscos_ordered_set }. definition inf: - ∀C:Type.∀O:dedekind_sigma_complete_ordered_set C. - bounded_below_sequence ? O → O. + ∀O:dedekind_sigma_complete_ordered_set. + bounded_below_sequence O → O. intros; elim - (dsc_inf ? O (dscos_dedekind_sigma_complete_properties ? O) b); + (dsc_inf O (dscos_dedekind_sigma_complete_properties O) b); [ apply a - | apply (lower_bound ? ? b) + | 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). + ∀O:dedekind_sigma_complete_ordered_set. + ∀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)); + elim (dsc_inf O (dscos_dedekind_sigma_complete_properties O) a +(lower_bound O a) (lower_bound_is_lower_bound 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; + ∀O:dedekind_sigma_complete_ordered_set. + ∀a,a':bounded_below_sequence O. + bbs_seq ? a = bbs_seq ? a' → + inf ? a = inf ? a'. + intros 3; elim a 0; elim a'; simplify in H; @@ -201,43 +193,43 @@ lemma inf_proof_irrelevant: 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)); + rewrite < (dsc_inf_proof_irrelevant O O f (ib_lower_bound ? f i) + (ib_lower_bound ? f i2) (ib_lower_bound_is_lower_bound ? f i) + (ib_lower_bound_is_lower_bound ? f i2)); reflexivity. qed. definition sup: - ∀C:Type.∀O:dedekind_sigma_complete_ordered_set C. - bounded_above_sequence ? O → O. + ∀O:dedekind_sigma_complete_ordered_set. + bounded_above_sequence O → O. intros; elim - (dsc_sup ? O (dscos_dedekind_sigma_complete_properties ? O) b); + (dsc_sup O (dscos_dedekind_sigma_complete_properties O) b); [ apply a - | apply (upper_bound ? ? b) + | 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). + ∀O:dedekind_sigma_complete_ordered_set. + ∀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)); + elim (dsc_sup O (dscos_dedekind_sigma_complete_properties O) a +(upper_bound O a) (upper_bound_is_upper_bound 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; + ∀O:dedekind_sigma_complete_ordered_set. + ∀a,a':bounded_above_sequence O. + bas_seq ? a = bas_seq ? a' → + sup ? a = sup ? a'. + intros 3; elim a 0; elim a'; simplify in H; @@ -246,18 +238,18 @@ lemma sup_proof_irrelevant: 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)); + rewrite < (dsc_sup_proof_irrelevant 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'); + ∀O:dedekind_sigma_complete_ordered_set. + ∀a:bounded_sequence O. inf ? a ≤ sup ? a. + intros (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))*) @@ -265,75 +257,75 @@ theorem inf_le_sup: 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) + ∀O:dedekind_sigma_complete_ordered_set. + ∀a:bounded_below_sequence O.∀m:O. + is_upper_bound ? a m → inf ? a ≤ m. + intros (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)))); + (sup_least_upper_bound ? ? ? + (sup_is_sup ? (mk_bounded_sequence O' a a + (mk_is_bounded_above 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)). + λO:ordered_set.λ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 +record is_order_continuous + (O:dedekind_sigma_complete_ordered_set) (f:O→O) : Prop ≝ - { ioc_is_sequentially_monotone: is_sequentially_monotone ? ? f; + { 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)); + ∀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)) + ∀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)); + ∀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)) + ∀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)); + ∀O:dedekind_sigma_complete_ordered_set. + ∀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) + 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 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)); + 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); + 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; @@ -344,52 +336,52 @@ theorem tail_inf_increasing: qed. definition is_liminf: - ∀C:Type.∀O:dedekind_sigma_complete_ordered_set C. - bounded_below_sequence ? O → O → Prop. + ∀O:dedekind_sigma_complete_ordered_set. + 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)); + (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). + 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. + ∀O:dedekind_sigma_complete_ordered_set. + bounded_sequence O → O. intros; apply - (sup ? ? - (mk_bounded_above_sequence ? ? - (λi.inf ? ? - (mk_bounded_below_sequence ? ? + (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)); + [ 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)); + 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); + (inf O + (mk_bounded_below_sequence O (\lambda j:nat.b (n+j)) + (mk_is_bounded_below O (\lambda j:nat.b (n+j)) (ib_lower_bound O b b) + (\lambda j:nat.ib_lower_bound_is_lower_bound O b b (n+j)))) +\leq ib_upper_bound O b b); + apply (inf_respects_le O); simplify; intro; - apply (ib_upper_bound_is_upper_bound ? ? b b) + apply (ib_upper_bound_is_upper_bound ? b b) ]. qed. -definition reverse_ordered_set: ∀C.ordered_set C → ordered_set C. +definition reverse_ordered_set: ordered_set → ordered_set. intros; apply mk_ordered_set; - [ apply mk_pre_ordered_set; - apply (λx,y:o.y ≤ x) + [2:apply (λx,y:o.y ≤ x) + | skip | apply mk_is_order_relation; [ simplify; intros; @@ -415,8 +407,8 @@ interpretation "Ordered set ge" 'geq a b = (cic:/matita/ordered_sets/reverse_ordered_set.con _ _)) a b). lemma is_lower_bound_reverse_is_upper_bound: - ∀C.∀O:ordered_set C.∀a:nat→O.∀l:O. - is_lower_bound ? O a l → is_upper_bound ? (reverse_ordered_set ? O) a l. + ∀O:ordered_set.∀a:nat→O.∀l:O. + is_lower_bound O a l → is_upper_bound (reverse_ordered_set O) a l. intros; unfold; intro; @@ -427,8 +419,8 @@ lemma is_lower_bound_reverse_is_upper_bound: qed. lemma is_upper_bound_reverse_is_lower_bound: - ∀C.∀O:ordered_set C.∀a:nat→O.∀l:O. - is_upper_bound ? O a l → is_lower_bound ? (reverse_ordered_set ? O) a l. + ∀O:ordered_set.∀a:nat→O.∀l:O. + is_upper_bound O a l → is_lower_bound (reverse_ordered_set O) a l. intros; unfold; intro; @@ -439,8 +431,8 @@ lemma is_upper_bound_reverse_is_lower_bound: qed. lemma reverse_is_lower_bound_is_upper_bound: - ∀C.∀O:ordered_set C.∀a:nat→O.∀l:O. - is_lower_bound ? (reverse_ordered_set ? O) a l → is_upper_bound ? O a l. + ∀O:ordered_set.∀a:nat→O.∀l:O. + is_lower_bound (reverse_ordered_set O) a l → is_upper_bound O a l. intros; unfold in H; unfold reverse_ordered_set in H; @@ -448,8 +440,8 @@ lemma reverse_is_lower_bound_is_upper_bound: qed. lemma reverse_is_upper_bound_is_lower_bound: - ∀C.∀O:ordered_set C.∀a:nat→O.∀l:O. - is_upper_bound ? (reverse_ordered_set ? O) a l → is_lower_bound ? O a l. + ∀O:ordered_set.∀a:nat→O.∀l:O. + is_upper_bound (reverse_ordered_set O) a l → is_lower_bound O a l. intros; unfold in H; unfold reverse_ordered_set in H; @@ -458,73 +450,73 @@ qed. lemma is_inf_to_reverse_is_sup: - ∀C.∀O:ordered_set C.∀a:bounded_below_sequence ? O.∀l:O. - is_inf ? O a l → is_sup ? (reverse_ordered_set ? O) a l. + ∀O:ordered_set.∀a:bounded_below_sequence O.∀l:O. + is_inf O a l → is_sup (reverse_ordered_set O) a l. intros; - apply (mk_is_sup C (reverse_ordered_set ? ?)); + apply (mk_is_sup (reverse_ordered_set O)); [ apply is_lower_bound_reverse_is_upper_bound; apply inf_lower_bound; assumption | intros; - change in v with (Type_OF_ordered_set ? O); + change in v with (os_carrier O); change with (v ≤ l); - apply (inf_greatest_lower_bound ? ? ? ? H); + apply (inf_greatest_lower_bound ? ? ? H); apply reverse_is_upper_bound_is_lower_bound; assumption ]. qed. lemma is_sup_to_reverse_is_inf: - ∀C.∀O:ordered_set C.∀a:bounded_above_sequence ? O.∀l:O. - is_sup ? O a l → is_inf ? (reverse_ordered_set ? O) a l. + ∀O:ordered_set.∀a:bounded_above_sequence O.∀l:O. + is_sup O a l → is_inf (reverse_ordered_set O) a l. intros; - apply (mk_is_inf C (reverse_ordered_set ? ?)); + apply (mk_is_inf (reverse_ordered_set O)); [ apply is_upper_bound_reverse_is_lower_bound; apply sup_upper_bound; assumption | intros; - change in v with (Type_OF_ordered_set ? O); + change in v with (os_carrier O); change with (l ≤ v); - apply (sup_least_upper_bound ? ? ? ? H); + apply (sup_least_upper_bound ? ? ? H); apply reverse_is_lower_bound_is_upper_bound; assumption ]. qed. lemma reverse_is_sup_to_is_inf: - ∀C.∀O:ordered_set C.∀a:bounded_above_sequence ? O.∀l:O. - is_sup ? (reverse_ordered_set ? O) a l → is_inf ? O a l. + ∀O:ordered_set.∀a:bounded_above_sequence O.∀l:O. + is_sup (reverse_ordered_set O) a l → is_inf O a l. intros; apply mk_is_inf; [ apply reverse_is_upper_bound_is_lower_bound; - change in l with (Type_OF_ordered_set ? (reverse_ordered_set ? O)); + change in l with (os_carrier (reverse_ordered_set O)); apply sup_upper_bound; assumption | intros; - change in l with (Type_OF_ordered_set ? (reverse_ordered_set ? O)); - change in v with (Type_OF_ordered_set ? (reverse_ordered_set ? O)); - change with (os_le ? (reverse_ordered_set ? O) l v); - apply (sup_least_upper_bound ? ? ? ? H); - change in v with (Type_OF_ordered_set ? O); + change in l with (os_carrier (reverse_ordered_set O)); + change in v with (os_carrier (reverse_ordered_set O)); + change with (os_le (reverse_ordered_set O) l v); + apply (sup_least_upper_bound ? ? ? H); + change in v with (os_carrier O); apply is_lower_bound_reverse_is_upper_bound; assumption ]. qed. lemma reverse_is_inf_to_is_sup: - ∀C.∀O:ordered_set C.∀a:bounded_above_sequence ? O.∀l:O. - is_inf ? (reverse_ordered_set ? O) a l → is_sup ? O a l. + ∀O:ordered_set.∀a:bounded_above_sequence O.∀l:O. + is_inf (reverse_ordered_set O) a l → is_sup O a l. intros; apply mk_is_sup; [ apply reverse_is_lower_bound_is_upper_bound; - change in l with (Type_OF_ordered_set ? (reverse_ordered_set ? O)); - apply (inf_lower_bound ? ? ? ? H) + change in l with (os_carrier (reverse_ordered_set O)); + apply (inf_lower_bound ? ? ? H) | intros; - change in l with (Type_OF_ordered_set ? (reverse_ordered_set ? O)); - change in v with (Type_OF_ordered_set ? (reverse_ordered_set ? O)); - change with (os_le ? (reverse_ordered_set ? O) v l); - apply (inf_greatest_lower_bound ? ? ? ? H); - change in v with (Type_OF_ordered_set ? O); + change in l with (os_carrier (reverse_ordered_set O)); + change in v with (os_carrier (reverse_ordered_set O)); + change with (os_le (reverse_ordered_set O) v l); + apply (inf_greatest_lower_bound ? ? ? H); + change in v with (os_carrier O); apply is_upper_bound_reverse_is_lower_bound; assumption ]. @@ -532,11 +524,10 @@ qed. definition reverse_dedekind_sigma_complete_ordered_set: - ∀C. - dedekind_sigma_complete_ordered_set C → dedekind_sigma_complete_ordered_set C. + dedekind_sigma_complete_ordered_set → dedekind_sigma_complete_ordered_set. intros; apply mk_dedekind_sigma_complete_ordered_set; - [ apply (reverse_ordered_set ? d) + [ apply (reverse_ordered_set d) | elim daemon (*apply mk_is_dedekind_sigma_complete; [ intros; @@ -568,9 +559,9 @@ definition reverse_dedekind_sigma_complete_ordered_set: qed. definition reverse_bounded_sequence: - ∀C.∀O:dedekind_sigma_complete_ordered_set C. - bounded_sequence ? O → - bounded_sequence ? (reverse_dedekind_sigma_complete_ordered_set ? O). + ∀O:dedekind_sigma_complete_ordered_set. + bounded_sequence O → + bounded_sequence (reverse_dedekind_sigma_complete_ordered_set O). intros; apply mk_bounded_sequence; [ apply bs_seq; @@ -583,10 +574,10 @@ definition reverse_bounded_sequence: qed. definition limsup ≝ - λC:Type.λO:dedekind_sigma_complete_ordered_set C. - λa:bounded_sequence ? O. - liminf ? (reverse_dedekind_sigma_complete_ordered_set ? O) - (reverse_bounded_sequence ? O a). + λO:dedekind_sigma_complete_ordered_set. + λa:bounded_sequence O. + liminf (reverse_dedekind_sigma_complete_ordered_set O) + (reverse_bounded_sequence O a). notation "hvbox(〈a〉)" non associative with precedence 45 @@ -599,12 +590,12 @@ 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))); + ∀O':dedekind_sigma_complete_ordered_set. + ∀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; @@ -614,83 +605,83 @@ theorem eq_f_sup_sup_f: 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'). + ∀O':dedekind_sigma_complete_ordered_set. + ∀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); + 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'. + ∀O':dedekind_sigma_complete_ordered_set. + ∀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 ? ? + 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)); + [ 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))); + 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); + [ 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); + rewrite > (plus_n_O n) in ⊢ (? ? ? (? (? ? ? %))); + apply (H1 (mk_bounded_below_sequence O' (\lambda j:nat.a (n+j)) +(mk_is_bounded_below O' (\lambda j:nat.a (n+j)) (ib_lower_bound O' a a) + (\lambda j:nat.ib_lower_bound_is_lower_bound 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))); +.inf_respects_le O' + (mk_bounded_below_sequence O' (\lambda j:nat.a (plus n j)) + (mk_is_bounded_below O' (\lambda j:nat.a (plus n j)) + (ib_lower_bound O' a a) + (\lambda j:nat.ib_lower_bound_is_lower_bound O' a a (plus n j)))) + (ib_upper_bound O' a a) + (\lambda n1:nat.ib_upper_bound_is_upper_bound O' a a (plus n n1))); intro p2; - apply (eq_f_sup_sup_f' ? ? f H (mk_bounded_above_sequence C O' + apply (eq_f_sup_sup_f' ? f H (mk_bounded_above_sequence 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' + .inf O' + (mk_bounded_below_sequence O' (\lambda j:nat.a (plus i j)) + (mk_is_bounded_below O' (\lambda j:nat.a (plus i j)) + (ib_lower_bound O' a a) + (\lambda n:nat.ib_lower_bound_is_lower_bound O' a a (plus i n))))) +(mk_is_bounded_above 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))); + .inf O' + (mk_bounded_below_sequence O' (\lambda j:nat.a (plus i j)) + (mk_is_bounded_below O' (\lambda j:nat.a (plus i j)) + (ib_lower_bound O' a a) + (\lambda n:nat.ib_lower_bound_is_lower_bound O' a a (plus i n))))) + (ib_upper_bound 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)))))); + (is_increasing ? (\lambda i:nat +.inf O' + (mk_bounded_below_sequence O' (\lambda j:nat.a (plus i j)) + (mk_is_bounded_below O' (\lambda j:nat.a (plus i j)) + (ib_lower_bound O' a a) + (\lambda n:nat.ib_lower_bound_is_lower_bound O' a a (plus i n)))))); apply tail_inf_increasing ]. qed. @@ -698,7 +689,7 @@ qed. -definition lt ≝ λC.λO:ordered_set C.λa,b:O.a ≤ b ∧ a ≠ b. +definition lt ≝ λO:ordered_set.λ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 + (cic:/matita/ordered_sets/lt.con _ _ a b). diff --git a/matita/dama/ordered_sets2.ma b/matita/dama/ordered_sets2.ma index 26e1cdb3f..a8050ec21 100644 --- a/matita/dama/ordered_sets2.ma +++ b/matita/dama/ordered_sets2.ma @@ -17,11 +17,11 @@ 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'. + ∀O':dedekind_sigma_complete_ordered_set. + ∀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). + 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 @@ -29,34 +29,34 @@ theorem le_f_inf_inf_f: ] | intros; clearbody p; - apply (inf_greatest_lower_bound ? ? ? ? (inf_is_inf ? ? ?)); + apply (inf_greatest_lower_bound ? ? ? (inf_is_inf ? ?)); simplify; intro; - letin b := (λi.match i with [ O ⇒ inf ? ? a | S _ ⇒ a n]); + 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); + 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')) + [ 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. + ∀O':dedekind_sigma_complete_ordered_set. + ∀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)); + 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)) + | apply (sup_upper_bound ? ? ? (sup_is_sup ? b)) ]. qed. @@ -64,8 +64,8 @@ interpretation "mk_bounded_sequence" 'hide_everything_but a = (cic:/matita/ordered_sets/bounded_sequence.ind#xpointer(1/1/1) _ _ a _ _). lemma reduce_bas_seq: - ∀C.∀O:ordered_set C.∀a:nat→O.∀p.∀i. - bas_seq ? ? (mk_bounded_above_sequence ? ? a p) i = a i. + ∀O:ordered_set.∀a:nat→O.∀p.∀i. + bas_seq ? (mk_bounded_above_sequence ? a p) i = a i. intros; reflexivity. qed. @@ -78,41 +78,41 @@ qed. qed.*) axiom inf_extensional: - ∀C.∀O:dedekind_sigma_complete_ordered_set C. - ∀a,b:bounded_below_sequence ? O. - (∀i.a i = b i) → inf ? ? a = inf ? O b. + ∀O:dedekind_sigma_complete_ordered_set. + ∀a,b:bounded_below_sequence O. + (∀i.a i = b i) → inf ? a = inf O b. -lemma eq_to_le: ∀C.∀O:ordered_set C.∀x,y:O.x=y → x ≤ y. +lemma eq_to_le: ∀O:ordered_set.∀x,y:O.x=y → x ≤ y. intros; rewrite > H; apply (or_reflexive ? ? O). qed. theorem fatou: - ∀C.∀O':dedekind_sigma_complete_ordered_set C. - ∀f:O'→O'. ∀H:is_order_continuous ? ? f. - ∀a:bounded_sequence ? O'. + ∀O':dedekind_sigma_complete_ordered_set. + ∀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); + 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) + [2: apply (ioc_is_upper_bound_f_sup ? ? H bas) | skip ] - | letin bbs ≝ (bounded_below_sequence_of_bounded_sequence ? ? a); + | letin bbs ≝ (bounded_below_sequence_of_bounded_sequence ? a); apply mk_is_bounded_below; - [2: apply (ioc_is_lower_bound_f_inf ? ? ? H bbs) + [2: apply (ioc_is_lower_bound_f_inf ? ? H bbs) | skip ] | intros; - rewrite > eq_f_liminf_sup_f_inf in ⊢ (? ? ? % ?); + rewrite > eq_f_liminf_sup_f_inf in ⊢ (? ? % ?); [ unfold liminf; apply le_to_le_sup_sup; intro; rewrite > reduce_bas_seq; rewrite > reduce_bas_seq; - apply (or_transitive ? O' O'); + apply (or_transitive ? ? O'); [2: apply le_f_inf_inf_f; assumption | skip @@ -125,3 +125,8 @@ theorem fatou: ] ]. qed. + +record cotransitively_ordered_set: Type := + { cos_ordered_set :> ordered_set; + cos_cotransitive: cotransitive ? (os_le cos_ordered_set) + }. diff --git a/matita/dama/reals.ma b/matita/dama/reals.ma index 9e458e291..c03fdf26b 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 (of_cotransitive R 0 (inv ? (sum_field ? (S n)) ?) (x-y)); + elim (cos_cotransitive R 0 (inv ? (sum_field ? (S n)) ?) (x-y)); [ apply x | apply not_eq_sum_field_zero ; unfold; @@ -157,7 +157,7 @@ lemma abs_x_ge_O: \forall R: real. \forall x:R. (zero R) ≤ abs R x. unfold to_zero; unfold max_seq; elim - (of_cotransitive R 0 + (cos_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) -- 2.39.2