From: Enrico Tassi Date: Tue, 27 Nov 2007 11:56:08 +0000 (+0000) Subject: major reorganization (read cleanup) X-Git-Tag: make_still_working~5766 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a42d4bd78f10ac8fc725c50c193503a3f29b848f;p=helm.git major reorganization (read cleanup) --- diff --git a/helm/software/matita/dama/attic/fields.ma b/helm/software/matita/dama/attic/fields.ma new file mode 100644 index 000000000..194a39110 --- /dev/null +++ b/helm/software/matita/dama/attic/fields.ma @@ -0,0 +1,60 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fields/". + +include "attic/rings.ma". + +record is_field (R:ring) (inv:∀x:R.x ≠ 0 → R) : Prop +≝ + { (* multiplicative abelian properties *) + mult_comm_: symmetric ? (mult R); + (* multiplicative group properties *) + inv_inverse_: ∀x.∀p: x ≠ 0. inv x p * x = 1 + }. + +lemma opp_opp: ∀R:ring. ∀x:R. --x=x. +intros; +apply (cancellationlaw ? (-x) ? ?); +rewrite > (opp_inverse R x); +rewrite > plus_comm; +rewrite > opp_inverse; +reflexivity. +qed. + +let rec sum (C:Type) (plus:C→C→C) (zero,one:C) (n:nat) on n ≝ + match n with + [ O ⇒ zero + | (S m) ⇒ plus one (sum C plus zero one m) + ]. + +record field : Type \def + { f_ring:> ring; + inv: ∀x:f_ring. x ≠ 0 → f_ring; + field_properties: is_field f_ring inv + }. + +theorem mult_comm: ∀F:field.symmetric ? (mult F). + intro; + apply (mult_comm_ ? ? (field_properties F)). +qed. + +theorem inv_inverse: ∀F:field.∀x:F.∀p: x ≠ 0. (inv ? x p)*x = 1. + intro; + apply (inv_inverse_ ? ? (field_properties F)). +qed. + +(*CSC: qua funzionava anche mettendo ? al posto della prima F*) +definition sum_field ≝ + λF:field. sum F (plus F) 0 1. diff --git a/helm/software/matita/dama/attic/integration_algebras.ma b/helm/software/matita/dama/attic/integration_algebras.ma new file mode 100644 index 000000000..50bf063a4 --- /dev/null +++ b/helm/software/matita/dama/attic/integration_algebras.ma @@ -0,0 +1,368 @@ +(**************************************************************************) +(* ___ *) +(* ||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/integration_algebras/". + +include "attic/vector_spaces.ma". +include "lattice.ma". + +(**************** Riesz Spaces ********************) + +record pre_riesz_space (K:ordered_field_ch0) : Type \def + { rs_vector_space:> vector_space K; + rs_lattice_: lattice; + rs_ordered_abelian_group_: ordered_abelian_group; + rs_with1: + og_abelian_group rs_ordered_abelian_group_ = vs_abelian_group ? rs_vector_space; + rs_with2: + og_ordered_set rs_ordered_abelian_group_ = ordered_set_of_lattice rs_lattice_ + }. + +lemma rs_lattice: ∀K.pre_riesz_space K → lattice. + intros (K V); + cut (os_carrier (rs_lattice_ ? V) = V); + [ apply mk_lattice; + [ apply (carrier V) + | apply (eq_rect ? ? (λC:Type.C→C→C) ? ? Hcut); + apply l_join + | apply (eq_rect ? ? (λC:Type.C→C→C) ? ? Hcut); + 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)) + ? ? Hcut); + simplify; + apply l_lattice_properties + ] + | transitivity (os_carrier (rs_ordered_abelian_group_ ? V)); + [ apply (eq_f ? ? os_carrier); + symmetry; + apply rs_with2 + | apply (eq_f ? ? carrier); + apply rs_with1 + ] + ]. +qed. + +coercion cic:/matita/integration_algebras/rs_lattice.con. + +lemma rs_ordered_abelian_group: ∀K.pre_riesz_space K → ordered_abelian_group. + intros (K V); + apply mk_ordered_abelian_group; + [ apply mk_pre_ordered_abelian_group; + [ apply (vs_abelian_group ? (rs_vector_space ? V)) + | apply (ordered_set_of_lattice (rs_lattice ? V)) + | reflexivity + ] + | simplify; + generalize in match + (og_ordered_abelian_group_properties (rs_ordered_abelian_group_ ? V)); + intro P; + unfold in P; + elim daemon(* + apply + (eq_rect ? ? + (λO:ordered_set. + ∀f,g,h. + os_le O f g → + os_le O + (plus (abelian_group_OF_pre_riesz_space K V) f h) + (plus (abelian_group_OF_pre_riesz_space K V) g h)) + ? ? (rs_with2 ? V)); + apply + (eq_rect ? ? + (λG:abelian_group. + ∀f,g,h. + os_le (ordered_set_OF_pre_riesz_space K V) f g → + os_le (ordered_set_OF_pre_riesz_space K V) + (plus (abelian_group_OF_pre_riesz_space K V) f h) + (plus (abelian_group_OF_pre_riesz_space K V) g h)) + ? ? (rs_with1 ? V)); + simplify; + apply og_ordered_abelian_group_properties*) + ] +qed. + +coercion cic:/matita/integration_algebras/rs_ordered_abelian_group.con. + +record is_riesz_space (K:ordered_field_ch0) (V:pre_riesz_space K) : Prop ≝ + { rs_compat_le_times: ∀a:K.∀f:V. 0≤a → 0≤f → 0≤a*f + }. + +record riesz_space (K:ordered_field_ch0) : Type \def + { 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. 0≤u → 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 ≝ λK.λS:riesz_space K.λf:S.f ∨ -f. + +(**************** Normed Riesz spaces ****************************) + +definition is_riesz_norm ≝ + λR:real.λV:riesz_space R.λnorm:norm R V. + ∀f,g:V. absolute_value ? V f ≤ absolute_value ? V g → + 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; + 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 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:S.∀n.∀a.∀p:n > O. + absolute_value ? S a ≤ + (inv K (sum_field K n) (not_eq_sum_field_zero K n p))* u → + a = 0 + }. + +record archimedean_riesz_space (K:ordered_field_ch0) : Type \def + { ars_riesz_space:> riesz_space K; + ars_archimedean_property: is_archimedean_riesz_space ? ars_riesz_space + }. + +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 + defining it on Riesz spaces) + 2. Fremlin proves |x|/\u=0 \to u=0. How do we remove the absolute value? + λR:real.λV:archimedean_riesz_space R.λunit: V. + ∀x:V. meet x unit = 0 → u = 0. + 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. 0 archimedean_riesz_space R; + irs_unit: irs_archimedean_riesz_space; + irs_weak_unit: is_weak_unit ? ? irs_unit; + integral: irs_archimedean_riesz_space → R; + irs_positive_linear: is_positive_linear ? ? integral; + irs_limit1: + ∀f:irs_archimedean_riesz_space. + tends_to ? + (λn.integral (f ∧ ((sum_field R n)*irs_unit))) + (integral f); + irs_limit2: + ∀f:irs_archimedean_riesz_space. + tends_to ? + (λn. + integral (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; + irs_quotient_space1: + ∀f,g:irs_archimedean_riesz_space. + integral (absolute_value ? irs_archimedean_riesz_space (f - g)) = 0 → f=g + }. + +definition induced_norm_fun ≝ + λR:real.λV:integration_riesz_space R.λf:V. + integral ? V (absolute_value ? ? f). + +lemma induced_norm_is_norm: + ∀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 positive; + [ apply (irs_positive_linear ? V) + | (* difficile *) + elim daemon + ] + | intros; + unfold induced_norm_fun; + (* facile *) + elim daemon + | intros; + unfold induced_norm_fun; + (* difficile *) + elim daemon + ] + | intros; + unfold induced_norm_fun in H; + apply irs_quotient_space1; + unfold minus; + rewrite < plus_comm; + rewrite < eq_zero_opp_zero; + rewrite > zero_neutral; + assumption + ].*) +qed. + +definition induced_norm ≝ + λR:real.λV:integration_riesz_space R. + mk_norm ? ? (induced_norm_fun ? V) (induced_norm_is_norm ? V). + +lemma is_riesz_norm_induced_norm: + ∀R:real.∀V:integration_riesz_space R. + is_riesz_norm ? ? (induced_norm ? V). + intros; + unfold is_riesz_norm; + intros; + unfold induced_norm; + simplify; + unfold induced_norm_fun; + (* difficile *) + elim daemon. +qed. + +definition induced_riesz_norm ≝ + λR:real.λV:integration_riesz_space R. + mk_riesz_norm ? ? (induced_norm ? V) (is_riesz_norm_induced_norm ? V). + +definition distance_induced_by_integral ≝ + λR:real.λV:integration_riesz_space R. + induced_distance ? ? (induced_norm R V). + +definition is_complete_integration_riesz_space ≝ + λR:real.λV:integration_riesz_space R. + is_complete ? ? (distance_induced_by_integral ? V). + +record complete_integration_riesz_space (R:real) : Type ≝ + { cirz_integration_riesz_space:> integration_riesz_space R; + cirz_complete_integration_riesz_space_property: + is_complete_integration_riesz_space ? cirz_integration_riesz_space + }. + +(* now we prove that any complete integration riesz space is an L-space *) + +(*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; + constructor 1; + [ apply cirz_complete_integration_riesz_space_property + | intros; + unfold induced_riesz_norm; + simplify; + unfold induced_norm; + simplify; + unfold induced_norm_fun; + (* difficile *) + elim daemon + ]. +qed.*) + +(**************************** f-ALGEBRAS ********************************) + +record is_algebra (K: field) (V:vector_space K) (mult:V→V→V) (one:V) : Prop +≝ + { (* ring properties *) + a_ring: is_ring V mult one; + (* algebra properties *) + a_associative_left: ∀a,f,g. a * (mult f g) = mult (a * f) g; + a_associative_right: ∀a,f,g. a * (mult f g) = mult f (a * g) + }. + +record algebra (K: field) : Type \def + { a_vector_space:> vector_space K; + a_one: a_vector_space; + a_mult: a_vector_space → a_vector_space → a_vector_space; + a_algebra_properties: is_algebra ? ? a_mult a_one + }. + +interpretation "Algebra product" 'times a b = + (cic:/matita/integration_algebras/a_mult.con _ a b). + +definition ring_of_algebra ≝ + λK.λA:algebra K. + mk_ring A (a_mult ? A) (a_one ? A) + (a_ring ? ? ? ? (a_algebra_properties ? A)). + +coercion cic:/matita/integration_algebras/ring_of_algebra.con. + +record pre_f_algebra (K:ordered_field_ch0) : Type ≝ + { fa_archimedean_riesz_space:> archimedean_riesz_space K; + fa_algebra_: algebra K; + fa_with: a_vector_space ? fa_algebra_ = rs_vector_space ? fa_archimedean_riesz_space + }. + +lemma fa_algebra: ∀K:ordered_field_ch0.pre_f_algebra K → algebra K. + intros (K A); + apply mk_algebra; + [ apply (rs_vector_space ? A) + | elim daemon + | elim daemon + | elim daemon + ] + qed. + +coercion cic:/matita/integration_algebras/fa_algebra.con. + +record is_f_algebra (K) (A:pre_f_algebra K) : Prop ≝ +{ compat_mult_le: ∀f,g:A.0 ≤ f → 0 ≤ g → 0 ≤ f*g; + compat_mult_meet: + ∀f,g,h:A.(f ∧ g) = 0 → ((h*f) ∧ g) = 0 +}. + +record f_algebra (K:ordered_field_ch0) : Type ≝ +{ fa_pre_f_algebra:> pre_f_algebra K; + fa_f_algebra_properties: is_f_algebra ? fa_pre_f_algebra +}. + +(* to be proved; see footnote 2 in the paper by Spitters *) +axiom symmetric_a_mult: + ∀K.∀A:f_algebra K. symmetric ? (a_mult ? A). + +record integration_f_algebra (R:real) : Type \def + { ifa_integration_riesz_space:> integration_riesz_space R; + ifa_f_algebra_: f_algebra R; + ifa_with: + fa_archimedean_riesz_space ? ifa_f_algebra_ = + irs_archimedean_riesz_space ? ifa_integration_riesz_space + }. + +axiom ifa_f_algebra: ∀R:real.integration_f_algebra R → f_algebra R. + +coercion cic:/matita/integration_algebras/ifa_f_algebra.con. diff --git a/helm/software/matita/dama/attic/ordered_fields_ch0.ma b/helm/software/matita/dama/attic/ordered_fields_ch0.ma new file mode 100644 index 000000000..b312c31ab --- /dev/null +++ b/helm/software/matita/dama/attic/ordered_fields_ch0.ma @@ -0,0 +1,151 @@ +(**************************************************************************) +(* ___ *) +(* ||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_fields_ch0/". + +include "attic/fields.ma". +include "ordered_group.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 pre_ordered_field_ch0: Type ≝ + { of_field:> field; + of_ordered_abelian_group_: ordered_abelian_group; + of_cotransitively_ordered_set_: cotransitively_ordered_set; + of_with1_: + cos_ordered_set of_cotransitively_ordered_set_ = + og_ordered_set of_ordered_abelian_group_; + of_with2: + og_abelian_group of_ordered_abelian_group_ = r_abelian_group of_field + }. + +lemma of_ordered_abelian_group: pre_ordered_field_ch0 → ordered_abelian_group. + intro F; + apply mk_ordered_abelian_group; + [ apply mk_pre_ordered_abelian_group; + [ apply (r_abelian_group F) + | apply (og_ordered_set (of_ordered_abelian_group_ F)) + | apply (eq_f ? ? carrier); + apply (of_with2 F) + ] + | + apply + (eq_rect' ? ? + (λG:abelian_group.λH:og_abelian_group (of_ordered_abelian_group_ F)=G. + is_ordered_abelian_group + (mk_pre_ordered_abelian_group G (of_ordered_abelian_group_ F) + (eq_f abelian_group Type carrier (of_ordered_abelian_group_ F) G + H))) + ? ? (of_with2 F)); + simplify; + apply (og_ordered_abelian_group_properties (of_ordered_abelian_group_ F)) + ] +qed. + +coercion cic:/matita/ordered_fields_ch0/of_ordered_abelian_group.con. + +(*CSC: I am not able to prove this since unfold is undone by coercion composition*) +axiom of_with1: + ∀G:pre_ordered_field_ch0. + cos_ordered_set (of_cotransitively_ordered_set_ G) = + og_ordered_set (of_ordered_abelian_group G). + +lemma of_cotransitively_ordered_set : pre_ordered_field_ch0 → cotransitively_ordered_set. + intro F; + apply mk_cotransitively_ordered_set; + [ apply (og_ordered_set F) + | apply + (eq_rect ? ? (λa:ordered_set.cotransitive (os_carrier a) (os_le a)) + ? ? (of_with1 F)); + apply cos_cotransitive + ] +qed. + +coercion cic:/matita/ordered_fields_ch0/of_cotransitively_ordered_set.con. + +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_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 + }. + +(* +lemma eq_opp_x_times_opp_one_x: ∀F:ordered_field_ch0.∀x:F.-x = -1*x. + intros; + +lemma not_eq_x_zero_to_lt_zero_mult_x_x: + ∀F:ordered_field_ch0.∀x:F. x ≠ 0 → 0 < x * x. + intros; + elim (of_weak_tricotomy ? ? ? ? ? ? ? ? F ? ? H); + [ generalize in match (le_x_zero_to_le_zero_opp_x F ? H1); intro; + 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. 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 ordered_field_ch0; + r_real_properties: is_real r_ordered_field_ch0 + }. + +definition lim: ∀R:real.∀f:nat→R.is_cauchy_seq ? f → R. + intros; + elim (r_complete ? (r_real_properties R) ? H); + exact a. +qed. + +definition max_seq: ∀R:real.∀x,y:R. nat → R. + intros (R x y); + elim (cos_cotransitive R 0 (inv ? (sum_field ? (S n)) ?) (x-y)); + [ apply x + | apply not_eq_sum_field_zero ; + unfold; + autobatch + | apply y + | apply lt_zero_to_le_inv_zero + ]. +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 (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 (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) + (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; + split; + [ apply (le_zero_x_to_le_opp_x_zero R ?); + apply lt_zero_to_le_inv_zero + | apply lt_zero_to_le_inv_zero + ] + | simplify; + split; + [ apply (or_transitive ? ? R ? 0); + [ apply (le_zero_x_to_le_opp_x_zero R ?) + | assumption + ] + | assumption + ] + ] + | simplify; + 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) + (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m))))); + [ simplify; + split; + [ elim daemon + | generalize in match (le_zero_x_to_le_opp_x_zero R ? t1); + intro; + unfold minus in H1; + rewrite > eq_opp_plus_plus_opp_opp in H1; + rewrite > eq_opp_opp_x_x in H1; + rewrite > plus_comm in H1; + apply (or_transitive ? ? R ? 0); + [ assumption + | apply lt_zero_to_le_inv_zero + ] + ] + | simplify; + rewrite > (plus_comm ? y (-y)); + rewrite > opp_inverse; + split; + [ elim daemon + | apply lt_zero_to_le_inv_zero + ] + ] + ]. + elim daemon.*) +qed. + +definition max: ∀R:real.R → R → R. + intros (R x y); + apply (lim R (max_seq R x y)); + apply cauchy_max_seq. +qed. + +definition abs \def λR:real.λx:R. max R x (-x). + +lemma comparison: + ∀R:real.∀f,g:nat→R. is_cauchy_seq ? f → is_cauchy_seq ? g → + (∀n:nat.f n ≤ g n) → lim ? f ? ≤ lim ? g ?. + [ assumption + | assumption + | intros; + elim daemon + ]. +qed. + +definition to_zero ≝ + λR:real.λn. + -(inv R (sum_field R (S n)) + (not_eq_sum_field_zero R (S n) (le_S_S O n (le_O_n n)))). + +axiom is_cauchy_seq_to_zero: ∀R:real. is_cauchy_seq ? (to_zero R). + +lemma technical1: ∀R:real.lim R (to_zero R) (is_cauchy_seq_to_zero R) = 0. + intros; + unfold lim; + elim daemon. +qed. + +lemma abs_x_ge_O: ∀R:real.∀x:R. 0 ≤ abs ? x. + intros; + unfold abs; + unfold max; + rewrite < technical1; + apply comparison; + intros; + unfold to_zero; + unfold max_seq; + elim + (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) + (not_eq_sum_field_zero R (S n) (le_S_S O n (le_O_n n))))); + [ simplify; + (* facile *) + elim daemon + | simplify; + (* facile *) + elim daemon + ]. +qed. diff --git a/helm/software/matita/dama/attic/rings.ma b/helm/software/matita/dama/attic/rings.ma new file mode 100644 index 000000000..2ea188847 --- /dev/null +++ b/helm/software/matita/dama/attic/rings.ma @@ -0,0 +1,103 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rings/". + +include "group.ma". + +record is_ring (G:abelian_group) (mult:G→G→G) (one:G) : Prop +≝ + { (* multiplicative monoid properties *) + mult_assoc_: associative ? mult; + one_neutral_left_: left_neutral ? mult one; + one_neutral_right_: right_neutral ? mult one; + (* ring properties *) + mult_plus_distr_left_: distributive_left ? mult (plus G); + mult_plus_distr_right_: distributive_right ? mult (plus G); + not_eq_zero_one_: (0 ≠ one) + }. + +record ring : Type \def + { r_abelian_group:> abelian_group; + mult: r_abelian_group → r_abelian_group → r_abelian_group; + one: r_abelian_group; + r_ring_properties: is_ring r_abelian_group mult one + }. + +theorem mult_assoc: ∀R:ring.associative ? (mult R). + intros; + apply (mult_assoc_ ? ? ? (r_ring_properties R)). +qed. + +theorem one_neutral_left: ∀R:ring.left_neutral ? (mult R) (one R). + intros; + apply (one_neutral_left_ ? ? ? (r_ring_properties R)). +qed. + +theorem one_neutral_right: ∀R:ring.right_neutral ? (mult R) (one R). + intros; + apply (one_neutral_right_ ? ? ? (r_ring_properties R)). +qed. + +theorem mult_plus_distr_left: ∀R:ring.distributive_left ? (mult R) (plus R). + intros; + apply (mult_plus_distr_left_ ? ? ? (r_ring_properties R)). +qed. + +theorem mult_plus_distr_right: ∀R:ring.distributive_right ? (mult R) (plus R). + intros; + apply (mult_plus_distr_right_ ? ? ? (r_ring_properties R)). +qed. + +theorem not_eq_zero_one: ∀R:ring.0 ≠ one R. + intros; + apply (not_eq_zero_one_ ? ? ? (r_ring_properties R)). +qed. + +interpretation "Ring mult" 'times a b = + (cic:/matita/rings/mult.con _ a b). + +notation "1" with precedence 89 +for @{ 'one }. + +interpretation "Ring one" 'one = + (cic:/matita/rings/one.con _). + +lemma eq_mult_zero_x_zero: ∀R:ring.∀x:R.0*x=0. + intros; + generalize in match (zero_neutral R 0); intro; + generalize in match (eq_f ? ? (λy.y*x) ? ? H); intro; clear H; + rewrite > mult_plus_distr_right in H1; + generalize in match (eq_f ? ? (λy.-(0*x)+y) ? ? H1); intro; clear H1; + rewrite < plus_assoc in H; + rewrite > opp_inverse in H; + rewrite > zero_neutral in H; + assumption. +qed. + +lemma eq_mult_x_zero_zero: ∀R:ring.∀x:R.x*0=0. +intros; +generalize in match (zero_neutral R 0); +intro; +generalize in match (eq_f ? ? (λy.x*y) ? ? H); intro; clear H; +(*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; +rewrite > opp_inverse in H; +rewrite > zero_neutral in H; +assumption. +qed. + diff --git a/helm/software/matita/dama/attic/vector_spaces.ma b/helm/software/matita/dama/attic/vector_spaces.ma new file mode 100644 index 000000000..1e29bee24 --- /dev/null +++ b/helm/software/matita/dama/attic/vector_spaces.ma @@ -0,0 +1,151 @@ +(**************************************************************************) +(* ___ *) +(* ||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/vector_spaces/". + +include "attic/reals.ma". + +record is_vector_space (K: field) (G:abelian_group) (emult:K→G→G) : Prop +≝ + { vs_nilpotent: ∀v. emult 0 v = 0; + vs_neutral: ∀v. emult 1 v = v; + vs_distributive: ∀a,b,v. emult (a + b) v = (emult a v) + (emult b v); + vs_associative: ∀a,b,v. emult (a * b) v = emult a (emult b v) + }. + +record vector_space (K:field): Type \def +{ vs_abelian_group :> abelian_group; + emult: K → vs_abelian_group → vs_abelian_group; + vs_vector_space_properties :> is_vector_space ? vs_abelian_group emult +}. + +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. 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 + }. + +theorem eq_semi_norm_zero_zero: + ∀R:real.∀V:vector_space R.∀semi_norm:V→R. + is_semi_norm ? ? semi_norm → + semi_norm 0 = 0. + intros; + (* facile *) + elim daemon. +qed. + +record is_norm (R:real) (V:vector_space R) (norm:V → R) : Prop ≝ + { n_semi_norm:> is_semi_norm ? ? norm; + n_properness: ∀x:V. norm x = 0 → x = 0 + }. + +record norm (R:real) (V:vector_space R) : Type ≝ + { n_function:1> V→R; + n_norm_properties: is_norm ? ? n_function + }. + +record is_semi_distance (R:real) (C:Type) (semi_d: C→C→R) : Prop ≝ + { 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 + }. + +record is_distance (R:real) (C:Type) (d:C→C→R) : Prop ≝ + { d_semi_distance:> is_semi_distance ? ? d; + d_properness: ∀x,y:C. d x y = 0 → x=y + }. + +record distance (R:real) (V:vector_space R) : Type ≝ + { d_function:2> V→V→R; + d_distance_properties: is_distance ? ? d_function + }. + +definition induced_distance_fun ≝ + λR:real.λV:vector_space R.λnorm:norm ? V. + λf,g:V.norm (f - g). + +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; + [ unfold induced_distance_fun; + intros; + apply sn_positive; + apply n_semi_norm; + apply (n_norm_properties ? ? norm) + | unfold induced_distance_fun; + intros; + unfold minus; + rewrite < plus_comm; + rewrite > opp_inverse; + apply eq_semi_norm_zero_zero; + apply n_semi_norm; + apply (n_norm_properties ? ? norm) + | unfold induced_distance_fun; + intros; + (* ??? *) + elim daemon + ] + | unfold induced_distance_fun; + intros; + generalize in match (n_properness ? ? norm ? ? H); + [ intro; + (* facile *) + elim daemon + | apply (n_norm_properties ? ? norm) + ] + ].*) +qed. + +definition induced_distance ≝ + λR:real.λV:vector_space R.λnorm:norm ? V. + mk_distance ? ? (induced_distance_fun ? ? norm) + (induced_distance_is_distance ? ? norm). + +definition tends_to : + ∀R:real.∀V:vector_space R.∀d:distance ? V.∀f:nat→V.∀l:V.Prop. +apply + (λR:real.λV:vector_space R.λd:distance ? V.λf:nat→V.λl:V. + ∀n:nat.∃m:nat.∀j:nat. m ≤ j → + d (f j) l ≤ inv R (sum_field ? (S n)) ?); + apply not_eq_sum_field_zero; + unfold; + autobatch. +qed. + +definition is_cauchy_seq : ∀R:real.\forall V:vector_space R. +\forall d:distance ? V.∀f:nat→V.Prop. + apply + (λR:real.λV: vector_space R. \lambda d:distance ? V. + \lambda f:nat→V. + ∀m:nat. + ∃n:nat.∀N. n ≤ N → + -(inv R (sum_field ? (S m)) ?) ≤ d (f N) (f n) ∧ + d (f N) (f n)≤ inv R (sum_field R (S m)) ?); + apply not_eq_sum_field_zero; + unfold; + autobatch. +qed. + +definition is_complete ≝ + λR:real.λV:vector_space R. + λd:distance ? V. + ∀f:nat→V. is_cauchy_seq ? ? d f→ + ex V (λl:V. tends_to ? ? d f l). diff --git a/helm/software/matita/dama/fields.ma b/helm/software/matita/dama/fields.ma deleted file mode 100644 index 5ab17edae..000000000 --- a/helm/software/matita/dama/fields.ma +++ /dev/null @@ -1,60 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/fields/". - -include "rings.ma". - -record is_field (R:ring) (inv:∀x:R.x ≠ 0 → R) : Prop -≝ - { (* multiplicative abelian properties *) - mult_comm_: symmetric ? (mult R); - (* multiplicative group properties *) - inv_inverse_: ∀x.∀p: x ≠ 0. inv x p * x = 1 - }. - -lemma opp_opp: ∀R:ring. ∀x:R. --x=x. -intros; -apply (cancellationlaw ? (-x) ? ?); -rewrite > (opp_inverse R x); -rewrite > plus_comm; -rewrite > opp_inverse; -reflexivity. -qed. - -let rec sum (C:Type) (plus:C→C→C) (zero,one:C) (n:nat) on n ≝ - match n with - [ O ⇒ zero - | (S m) ⇒ plus one (sum C plus zero one m) - ]. - -record field : Type \def - { f_ring:> ring; - inv: ∀x:f_ring. x ≠ 0 → f_ring; - field_properties: is_field f_ring inv - }. - -theorem mult_comm: ∀F:field.symmetric ? (mult F). - intro; - apply (mult_comm_ ? ? (field_properties F)). -qed. - -theorem inv_inverse: ∀F:field.∀x:F.∀p: x ≠ 0. (inv ? x p)*x = 1. - intro; - apply (inv_inverse_ ? ? (field_properties F)). -qed. - -(*CSC: qua funzionava anche mettendo ? al posto della prima F*) -definition sum_field ≝ - λF:field. sum F (plus F) 0 1. diff --git a/helm/software/matita/dama/group.ma b/helm/software/matita/dama/group.ma new file mode 100644 index 000000000..0d682a268 --- /dev/null +++ b/helm/software/matita/dama/group.ma @@ -0,0 +1,229 @@ +(**************************************************************************) +(* ___ *) +(* ||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/group/". + +include "excedence.ma". + +definition left_neutral ≝ λC:apartness.λop.λe:C. ∀x:C. op e x ≈ x. +definition right_neutral ≝ λC:apartness.λop. λe:C. ∀x:C. op x e ≈ x. +definition left_inverse ≝ λC:apartness.λop.λe:C.λinv:C→C. ∀x:C. op (inv x) x ≈ e. +definition right_inverse ≝ λC:apartness.λop.λe:C.λ inv: C→ C. ∀x:C. op x (inv x) ≈ e. +definition strong_ext ≝ λA:apartness.λop:A→A.∀x,y. op x # op y → x # y. +(* ALLOW DEFINITION WITH SOME METAS *) + +definition distributive_left ≝ + λA:apartness.λf:A→A→A.λg:A→A→A. + ∀x,y,z. f x (g y z) ≈ g (f x y) (f x z). + +definition distributive_right ≝ + λA:apartness.λf:A→A→A.λg:A→A→A. + ∀x,y,z. f (g x y) z ≈ g (f x z) (f y z). + +record abelian_group : Type ≝ + { carr:> apartness; + plus: carr → carr → carr; + zero: carr; + opp: carr → carr; + plus_assoc_: associative ? plus (eq carr); + plus_comm_: commutative ? plus (eq carr); + zero_neutral_: left_neutral ? plus zero; + opp_inverse_: left_inverse ? plus zero opp; + plus_strong_ext: ∀z.strong_ext ? (plus z) +}. + +notation "0" with precedence 89 for @{ 'zero }. + +interpretation "Abelian group zero" 'zero = + (cic:/matita/group/zero.con _). + +interpretation "Abelian group plus" 'plus a b = + (cic:/matita/group/plus.con _ a b). + +interpretation "Abelian group opp" 'uminus a = + (cic:/matita/group/opp.con _ a). + +definition minus ≝ + λG:abelian_group.λa,b:G. a + -b. + +interpretation "Abelian group minus" 'minus a b = + (cic:/matita/group/minus.con _ a b). + +lemma plus_assoc: ∀G:abelian_group.∀x,y,z:G.x+(y+z)≈x+y+z ≝ plus_assoc_. +lemma plus_comm: ∀G:abelian_group.∀x,y:G.x+y≈y+x ≝ plus_comm_. +lemma zero_neutral: ∀G:abelian_group.∀x:G.0+x≈x ≝ zero_neutral_. +lemma opp_inverse: ∀G:abelian_group.∀x:G.-x+x≈0 ≝ opp_inverse_. + +definition ext ≝ λA:apartness.λop:A→A. ∀x,y. x ≈ y → op x ≈ op y. + +lemma strong_ext_to_ext: ∀A:apartness.∀op:A→A. strong_ext ? op → ext ? op. +intros 6 (A op SEop x y Exy); intro Axy; apply Exy; apply SEop; assumption; +qed. + +lemma feq_plusl: ∀G:abelian_group.∀x,y,z:G. y ≈ z → x+y ≈ x+z. +intros (G x y z Eyz); apply (strong_ext_to_ext ?? (plus_strong_ext ? x)); +assumption; +qed. + +coercion cic:/matita/group/feq_plusl.con nocomposites. + +lemma plus_strong_extr: ∀G:abelian_group.∀z:G.strong_ext ? (λx.x + z). +intros 5 (G z x y A); simplify in A; +lapply (plus_comm ? z x) as E1; lapply (plus_comm ? z y) as E2; +lapply (ap_rewl ???? E1 A) as A1; lapply (ap_rewr ???? E2 A1) as A2; +apply (plus_strong_ext ???? A2); +qed. + +lemma feq_plusr: ∀G:abelian_group.∀x,y,z:G. y ≈ z → y+x ≈ z+x. +intros (G x y z Eyz); apply (strong_ext_to_ext ?? (plus_strong_extr ? x)); +assumption; +qed. + +coercion cic:/matita/group/feq_plusr.con nocomposites. + +(* generation of coercions to make *_rew[lr] easier *) +lemma feq_plusr_sym_: ∀G:abelian_group.∀x,y,z:G.z ≈ y → y+x ≈ z+x. +compose feq_plusr with eq_sym (H); apply H; assumption; +qed. +coercion cic:/matita/group/feq_plusr_sym_.con nocomposites. +lemma feq_plusl_sym_: ∀G:abelian_group.∀x,y,z:G.z ≈ y → x+y ≈ x+z. +compose feq_plusl with eq_sym (H); apply H; assumption; +qed. +coercion cic:/matita/group/feq_plusl_sym_.con nocomposites. + +lemma fap_plusl: ∀G:abelian_group.∀x,y,z:G. y # z → x+y # x+z. +intros (G x y z Ayz); apply (plus_strong_ext ? (-x)); +apply (ap_rewl ??? ((-x + x) + y)); +[1: apply plus_assoc; +|2: apply (ap_rewr ??? ((-x +x) +z)); + [1: apply plus_assoc; + |2: apply (ap_rewl ??? (0 + y)); + [1: apply (feq_plusr ???? (opp_inverse ??)); + |2: apply (ap_rewl ???? (zero_neutral ? y)); + apply (ap_rewr ??? (0 + z) (opp_inverse ??)); + apply (ap_rewr ???? (zero_neutral ??)); assumption;]]] +qed. + +lemma fap_plusr: ∀G:abelian_group.∀x,y,z:G. y # z → y+x # z+x. +intros (G x y z Ayz); apply (plus_strong_extr ? (-x)); +apply (ap_rewl ??? (y + (x + -x))); +[1: apply (eq_sym ??? (plus_assoc ????)); +|2: apply (ap_rewr ??? (z + (x + -x))); + [1: apply (eq_sym ??? (plus_assoc ????)); + |2: apply (ap_rewl ??? (y + (-x+x)) (plus_comm ? x (-x))); + apply (ap_rewl ??? (y + 0) (opp_inverse ??)); + apply (ap_rewl ??? (0 + y) (plus_comm ???)); + apply (ap_rewl ??? y (zero_neutral ??)); + apply (ap_rewr ??? (z + (-x+x)) (plus_comm ? x (-x))); + apply (ap_rewr ??? (z + 0) (opp_inverse ??)); + apply (ap_rewr ??? (0 + z) (plus_comm ???)); + apply (ap_rewr ??? z (zero_neutral ??)); + assumption]] +qed. + +lemma plus_cancl: ∀G:abelian_group.∀y,z,x:G. x+y ≈ x+z → y ≈ z. +intros 6 (G y z x E Ayz); apply E; apply fap_plusl; assumption; +qed. + +lemma plus_cancr: ∀G:abelian_group.∀y,z,x:G. y+x ≈ z+x → y ≈ z. +intros 6 (G y z x E Ayz); apply E; apply fap_plusr; assumption; +qed. + +theorem eq_opp_plus_plus_opp_opp: + ∀G:abelian_group.∀x,y:G. -(x+y) ≈ -x + -y. +intros (G x y); apply (plus_cancr ??? (x+y)); +apply (eq_trans ?? 0 ? (opp_inverse ??)); +apply (eq_trans ?? (-x + -y + x + y)); [2: apply (eq_sym ??? (plus_assoc ????))] +apply (eq_trans ?? (-y + -x + x + y)); [2: repeat apply feq_plusr; apply plus_comm] +apply (eq_trans ?? (-y + (-x + x) + y)); [2: apply feq_plusr; apply plus_assoc;] +apply (eq_trans ?? (-y + 0 + y)); + [2: apply feq_plusr; apply feq_plusl; apply eq_sym; apply opp_inverse] +apply (eq_trans ?? (-y + y)); + [2: apply feq_plusr; apply eq_sym; + apply (eq_trans ?? (0+-y)); [apply plus_comm|apply zero_neutral]] +apply eq_sym; apply opp_inverse. +qed. + +theorem eq_opp_opp_x_x: ∀G:abelian_group.∀x:G.--x ≈ x. +intros (G x); apply (plus_cancl ??? (-x)); +apply (eq_trans ?? (--x + -x)); [apply plus_comm] +apply (eq_trans ?? 0); [apply opp_inverse] +apply eq_sym; apply opp_inverse; +qed. + +theorem eq_zero_opp_zero: ∀G:abelian_group.0 ≈ -0. [assumption] +intro G; apply (plus_cancr ??? 0); +apply (eq_trans ?? 0); [apply zero_neutral;] +apply eq_sym; apply opp_inverse; +qed. + +lemma feq_oppr: ∀G:abelian_group.∀x,y,z:G. y ≈ z → x ≈ -y → x ≈ -z. +intros (G x y z H1 H2); apply (plus_cancr ??? z); +apply (eq_trans ?? 0 ?? (opp_inverse ?z)); +apply (eq_trans ?? (-y + z) ? H2); +apply (eq_trans ?? (-y + y) ? H1); +apply (eq_trans ?? 0 ? (opp_inverse ??)); +apply eq_reflexive; +qed. + +lemma feq_oppl: ∀G:abelian_group.∀x,y,z:G. y ≈ z → -y ≈ x → -z ≈ x. +intros (G x y z H1 H2); apply eq_sym; apply (feq_oppr ??y); +[2:apply eq_sym] assumption; +qed. + +lemma feq_opp: ∀G:abelian_group.∀x,y:G. x ≈ y → -x ≈ -y. +intros (G x y H); apply (feq_oppl ??y ? H); apply eq_reflexive; +qed. + +coercion cic:/matita/group/feq_opp.con nocomposites. + +lemma eq_opp_sym: ∀G:abelian_group.∀x,y:G. y ≈ x → -x ≈ -y. +compose feq_opp with eq_sym (H); apply H; assumption; +qed. + +coercion cic:/matita/group/eq_opp_sym.con nocomposites. + +lemma eq_opp_plusr: ∀G:abelian_group.∀x,y,z:G. x ≈ y → -(x + z) ≈ -(y + z). +compose feq_plusr with feq_opp(H); apply H; assumption; +qed. + +coercion cic:/matita/group/eq_opp_plusr.con nocomposites. + +lemma eq_opp_plusl: ∀G:abelian_group.∀x,y,z:G. x ≈ y → -(z + x) ≈ -(z + y). +compose feq_plusl with feq_opp(H); apply H; assumption; +qed. + +coercion cic:/matita/group/eq_opp_plusl.con nocomposites. + +lemma plus_cancr_ap: ∀G:abelian_group.∀x,y,z:G. x+z # y+z → x # y. +intros (G x y z H); lapply (fap_plusr ? (-z) ?? H) as H1; clear H; +lapply (ap_rewl ? (x + (z + -z)) ?? (plus_assoc ? x z (-z)) H1) as H2; clear H1; +lapply (ap_rewl ? (x + (-z + z)) ?? (plus_comm ?z (-z)) H2) as H1; clear H2; +lapply (ap_rewl ? (x + 0) ?? (opp_inverse ?z) H1) as H2; clear H1; +lapply (ap_rewl ? (0+x) ?? (plus_comm ?x 0) H2) as H1; clear H2; +lapply (ap_rewl ? x ?? (zero_neutral ?x) H1) as H2; clear H1; +lapply (ap_rewr ? (y + (z + -z)) ?? (plus_assoc ? y z (-z)) H2) as H3; +lapply (ap_rewr ? (y + (-z + z)) ?? (plus_comm ?z (-z)) H3) as H4; +lapply (ap_rewr ? (y + 0) ?? (opp_inverse ?z) H4) as H5; +lapply (ap_rewr ? (0+y) ?? (plus_comm ?y 0) H5) as H6; +lapply (ap_rewr ? y ?? (zero_neutral ?y) H6); +assumption; +qed. + +lemma pluc_cancl_ap: ∀G:abelian_group.∀x,y,z:G. z+x # z+y → x # y. +intros (G x y z H); apply (plus_cancr_ap ??? z); +apply (ap_rewl ???? (plus_comm ???)); +apply (ap_rewr ???? (plus_comm ???)); +assumption; +qed. diff --git a/helm/software/matita/dama/groups.ma b/helm/software/matita/dama/groups.ma deleted file mode 100644 index c00740ee9..000000000 --- a/helm/software/matita/dama/groups.ma +++ /dev/null @@ -1,229 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/groups/". - -include "excedence.ma". - -definition left_neutral ≝ λC:apartness.λop.λe:C. ∀x:C. op e x ≈ x. -definition right_neutral ≝ λC:apartness.λop. λe:C. ∀x:C. op x e ≈ x. -definition left_inverse ≝ λC:apartness.λop.λe:C.λinv:C→C. ∀x:C. op (inv x) x ≈ e. -definition right_inverse ≝ λC:apartness.λop.λe:C.λ inv: C→ C. ∀x:C. op x (inv x) ≈ e. -definition strong_ext ≝ λA:apartness.λop:A→A.∀x,y. op x # op y → x # y. -(* ALLOW DEFINITION WITH SOME METAS *) - -definition distributive_left ≝ - λA:apartness.λf:A→A→A.λg:A→A→A. - ∀x,y,z. f x (g y z) ≈ g (f x y) (f x z). - -definition distributive_right ≝ - λA:apartness.λf:A→A→A.λg:A→A→A. - ∀x,y,z. f (g x y) z ≈ g (f x z) (f y z). - -record abelian_group : Type ≝ - { carr:> apartness; - plus: carr → carr → carr; - zero: carr; - opp: carr → carr; - plus_assoc_: associative ? plus (eq carr); - plus_comm_: commutative ? plus (eq carr); - zero_neutral_: left_neutral ? plus zero; - opp_inverse_: left_inverse ? plus zero opp; - plus_strong_ext: ∀z.strong_ext ? (plus z) -}. - -notation "0" with precedence 89 for @{ 'zero }. - -interpretation "Abelian group zero" 'zero = - (cic:/matita/groups/zero.con _). - -interpretation "Abelian group plus" 'plus a b = - (cic:/matita/groups/plus.con _ a b). - -interpretation "Abelian group opp" 'uminus a = - (cic:/matita/groups/opp.con _ a). - -definition minus ≝ - λG:abelian_group.λa,b:G. a + -b. - -interpretation "Abelian group minus" 'minus a b = - (cic:/matita/groups/minus.con _ a b). - -lemma plus_assoc: ∀G:abelian_group.∀x,y,z:G.x+(y+z)≈x+y+z ≝ plus_assoc_. -lemma plus_comm: ∀G:abelian_group.∀x,y:G.x+y≈y+x ≝ plus_comm_. -lemma zero_neutral: ∀G:abelian_group.∀x:G.0+x≈x ≝ zero_neutral_. -lemma opp_inverse: ∀G:abelian_group.∀x:G.-x+x≈0 ≝ opp_inverse_. - -definition ext ≝ λA:apartness.λop:A→A. ∀x,y. x ≈ y → op x ≈ op y. - -lemma strong_ext_to_ext: ∀A:apartness.∀op:A→A. strong_ext ? op → ext ? op. -intros 6 (A op SEop x y Exy); intro Axy; apply Exy; apply SEop; assumption; -qed. - -lemma feq_plusl: ∀G:abelian_group.∀x,y,z:G. y ≈ z → x+y ≈ x+z. -intros (G x y z Eyz); apply (strong_ext_to_ext ?? (plus_strong_ext ? x)); -assumption; -qed. - -coercion cic:/matita/groups/feq_plusl.con nocomposites. - -lemma plus_strong_extr: ∀G:abelian_group.∀z:G.strong_ext ? (λx.x + z). -intros 5 (G z x y A); simplify in A; -lapply (plus_comm ? z x) as E1; lapply (plus_comm ? z y) as E2; -lapply (ap_rewl ???? E1 A) as A1; lapply (ap_rewr ???? E2 A1) as A2; -apply (plus_strong_ext ???? A2); -qed. - -lemma feq_plusr: ∀G:abelian_group.∀x,y,z:G. y ≈ z → y+x ≈ z+x. -intros (G x y z Eyz); apply (strong_ext_to_ext ?? (plus_strong_extr ? x)); -assumption; -qed. - -coercion cic:/matita/groups/feq_plusr.con nocomposites. - -(* generation of coercions to make *_rew[lr] easier *) -lemma feq_plusr_sym_: ∀G:abelian_group.∀x,y,z:G.z ≈ y → y+x ≈ z+x. -compose feq_plusr with eq_sym (H); apply H; assumption; -qed. -coercion cic:/matita/groups/feq_plusr_sym_.con nocomposites. -lemma feq_plusl_sym_: ∀G:abelian_group.∀x,y,z:G.z ≈ y → x+y ≈ x+z. -compose feq_plusl with eq_sym (H); apply H; assumption; -qed. -coercion cic:/matita/groups/feq_plusl_sym_.con nocomposites. - -lemma fap_plusl: ∀G:abelian_group.∀x,y,z:G. y # z → x+y # x+z. -intros (G x y z Ayz); apply (plus_strong_ext ? (-x)); -apply (ap_rewl ??? ((-x + x) + y)); -[1: apply plus_assoc; -|2: apply (ap_rewr ??? ((-x +x) +z)); - [1: apply plus_assoc; - |2: apply (ap_rewl ??? (0 + y)); - [1: apply (feq_plusr ???? (opp_inverse ??)); - |2: apply (ap_rewl ???? (zero_neutral ? y)); - apply (ap_rewr ??? (0 + z) (opp_inverse ??)); - apply (ap_rewr ???? (zero_neutral ??)); assumption;]]] -qed. - -lemma fap_plusr: ∀G:abelian_group.∀x,y,z:G. y # z → y+x # z+x. -intros (G x y z Ayz); apply (plus_strong_extr ? (-x)); -apply (ap_rewl ??? (y + (x + -x))); -[1: apply (eq_sym ??? (plus_assoc ????)); -|2: apply (ap_rewr ??? (z + (x + -x))); - [1: apply (eq_sym ??? (plus_assoc ????)); - |2: apply (ap_rewl ??? (y + (-x+x)) (plus_comm ? x (-x))); - apply (ap_rewl ??? (y + 0) (opp_inverse ??)); - apply (ap_rewl ??? (0 + y) (plus_comm ???)); - apply (ap_rewl ??? y (zero_neutral ??)); - apply (ap_rewr ??? (z + (-x+x)) (plus_comm ? x (-x))); - apply (ap_rewr ??? (z + 0) (opp_inverse ??)); - apply (ap_rewr ??? (0 + z) (plus_comm ???)); - apply (ap_rewr ??? z (zero_neutral ??)); - assumption]] -qed. - -lemma plus_cancl: ∀G:abelian_group.∀y,z,x:G. x+y ≈ x+z → y ≈ z. -intros 6 (G y z x E Ayz); apply E; apply fap_plusl; assumption; -qed. - -lemma plus_cancr: ∀G:abelian_group.∀y,z,x:G. y+x ≈ z+x → y ≈ z. -intros 6 (G y z x E Ayz); apply E; apply fap_plusr; assumption; -qed. - -theorem eq_opp_plus_plus_opp_opp: - ∀G:abelian_group.∀x,y:G. -(x+y) ≈ -x + -y. -intros (G x y); apply (plus_cancr ??? (x+y)); -apply (eq_trans ?? 0 ? (opp_inverse ??)); -apply (eq_trans ?? (-x + -y + x + y)); [2: apply (eq_sym ??? (plus_assoc ????))] -apply (eq_trans ?? (-y + -x + x + y)); [2: repeat apply feq_plusr; apply plus_comm] -apply (eq_trans ?? (-y + (-x + x) + y)); [2: apply feq_plusr; apply plus_assoc;] -apply (eq_trans ?? (-y + 0 + y)); - [2: apply feq_plusr; apply feq_plusl; apply eq_sym; apply opp_inverse] -apply (eq_trans ?? (-y + y)); - [2: apply feq_plusr; apply eq_sym; - apply (eq_trans ?? (0+-y)); [apply plus_comm|apply zero_neutral]] -apply eq_sym; apply opp_inverse. -qed. - -theorem eq_opp_opp_x_x: ∀G:abelian_group.∀x:G.--x ≈ x. -intros (G x); apply (plus_cancl ??? (-x)); -apply (eq_trans ?? (--x + -x)); [apply plus_comm] -apply (eq_trans ?? 0); [apply opp_inverse] -apply eq_sym; apply opp_inverse; -qed. - -theorem eq_zero_opp_zero: ∀G:abelian_group.0 ≈ -0. [assumption] -intro G; apply (plus_cancr ??? 0); -apply (eq_trans ?? 0); [apply zero_neutral;] -apply eq_sym; apply opp_inverse; -qed. - -lemma feq_oppr: ∀G:abelian_group.∀x,y,z:G. y ≈ z → x ≈ -y → x ≈ -z. -intros (G x y z H1 H2); apply (plus_cancr ??? z); -apply (eq_trans ?? 0 ?? (opp_inverse ?z)); -apply (eq_trans ?? (-y + z) ? H2); -apply (eq_trans ?? (-y + y) ? H1); -apply (eq_trans ?? 0 ? (opp_inverse ??)); -apply eq_reflexive; -qed. - -lemma feq_oppl: ∀G:abelian_group.∀x,y,z:G. y ≈ z → -y ≈ x → -z ≈ x. -intros (G x y z H1 H2); apply eq_sym; apply (feq_oppr ??y); -[2:apply eq_sym] assumption; -qed. - -lemma feq_opp: ∀G:abelian_group.∀x,y:G. x ≈ y → -x ≈ -y. -intros (G x y H); apply (feq_oppl ??y ? H); apply eq_reflexive; -qed. - -coercion cic:/matita/groups/feq_opp.con nocomposites. - -lemma eq_opp_sym: ∀G:abelian_group.∀x,y:G. y ≈ x → -x ≈ -y. -compose feq_opp with eq_sym (H); apply H; assumption; -qed. - -coercion cic:/matita/groups/eq_opp_sym.con nocomposites. - -lemma eq_opp_plusr: ∀G:abelian_group.∀x,y,z:G. x ≈ y → -(x + z) ≈ -(y + z). -compose feq_plusr with feq_opp(H); apply H; assumption; -qed. - -coercion cic:/matita/groups/eq_opp_plusr.con nocomposites. - -lemma eq_opp_plusl: ∀G:abelian_group.∀x,y,z:G. x ≈ y → -(z + x) ≈ -(z + y). -compose feq_plusl with feq_opp(H); apply H; assumption; -qed. - -coercion cic:/matita/groups/eq_opp_plusl.con nocomposites. - -lemma plus_cancr_ap: ∀G:abelian_group.∀x,y,z:G. x+z # y+z → x # y. -intros (G x y z H); lapply (fap_plusr ? (-z) ?? H) as H1; clear H; -lapply (ap_rewl ? (x + (z + -z)) ?? (plus_assoc ? x z (-z)) H1) as H2; clear H1; -lapply (ap_rewl ? (x + (-z + z)) ?? (plus_comm ?z (-z)) H2) as H1; clear H2; -lapply (ap_rewl ? (x + 0) ?? (opp_inverse ?z) H1) as H2; clear H1; -lapply (ap_rewl ? (0+x) ?? (plus_comm ?x 0) H2) as H1; clear H2; -lapply (ap_rewl ? x ?? (zero_neutral ?x) H1) as H2; clear H1; -lapply (ap_rewr ? (y + (z + -z)) ?? (plus_assoc ? y z (-z)) H2) as H3; -lapply (ap_rewr ? (y + (-z + z)) ?? (plus_comm ?z (-z)) H3) as H4; -lapply (ap_rewr ? (y + 0) ?? (opp_inverse ?z) H4) as H5; -lapply (ap_rewr ? (0+y) ?? (plus_comm ?y 0) H5) as H6; -lapply (ap_rewr ? y ?? (zero_neutral ?y) H6); -assumption; -qed. - -lemma pluc_cancl_ap: ∀G:abelian_group.∀x,y,z:G. z+x # z+y → x # y. -intros (G x y z H); apply (plus_cancr_ap ??? z); -apply (ap_rewl ???? (plus_comm ???)); -apply (ap_rewr ???? (plus_comm ???)); -assumption; -qed. diff --git a/helm/software/matita/dama/integration_algebras.ma b/helm/software/matita/dama/integration_algebras.ma deleted file mode 100644 index c37a1f0b1..000000000 --- a/helm/software/matita/dama/integration_algebras.ma +++ /dev/null @@ -1,368 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/integration_algebras/". - -include "vector_spaces.ma". -include "lattice.ma". - -(**************** Riesz Spaces ********************) - -record pre_riesz_space (K:ordered_field_ch0) : Type \def - { rs_vector_space:> vector_space K; - rs_lattice_: lattice; - rs_ordered_abelian_group_: ordered_abelian_group; - rs_with1: - og_abelian_group rs_ordered_abelian_group_ = vs_abelian_group ? rs_vector_space; - rs_with2: - og_ordered_set rs_ordered_abelian_group_ = ordered_set_of_lattice rs_lattice_ - }. - -lemma rs_lattice: ∀K.pre_riesz_space K → lattice. - intros (K V); - cut (os_carrier (rs_lattice_ ? V) = V); - [ apply mk_lattice; - [ apply (carrier V) - | apply (eq_rect ? ? (λC:Type.C→C→C) ? ? Hcut); - apply l_join - | apply (eq_rect ? ? (λC:Type.C→C→C) ? ? Hcut); - 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)) - ? ? Hcut); - simplify; - apply l_lattice_properties - ] - | transitivity (os_carrier (rs_ordered_abelian_group_ ? V)); - [ apply (eq_f ? ? os_carrier); - symmetry; - apply rs_with2 - | apply (eq_f ? ? carrier); - apply rs_with1 - ] - ]. -qed. - -coercion cic:/matita/integration_algebras/rs_lattice.con. - -lemma rs_ordered_abelian_group: ∀K.pre_riesz_space K → ordered_abelian_group. - intros (K V); - apply mk_ordered_abelian_group; - [ apply mk_pre_ordered_abelian_group; - [ apply (vs_abelian_group ? (rs_vector_space ? V)) - | apply (ordered_set_of_lattice (rs_lattice ? V)) - | reflexivity - ] - | simplify; - generalize in match - (og_ordered_abelian_group_properties (rs_ordered_abelian_group_ ? V)); - intro P; - unfold in P; - elim daemon(* - apply - (eq_rect ? ? - (λO:ordered_set. - ∀f,g,h. - os_le O f g → - os_le O - (plus (abelian_group_OF_pre_riesz_space K V) f h) - (plus (abelian_group_OF_pre_riesz_space K V) g h)) - ? ? (rs_with2 ? V)); - apply - (eq_rect ? ? - (λG:abelian_group. - ∀f,g,h. - os_le (ordered_set_OF_pre_riesz_space K V) f g → - os_le (ordered_set_OF_pre_riesz_space K V) - (plus (abelian_group_OF_pre_riesz_space K V) f h) - (plus (abelian_group_OF_pre_riesz_space K V) g h)) - ? ? (rs_with1 ? V)); - simplify; - apply og_ordered_abelian_group_properties*) - ] -qed. - -coercion cic:/matita/integration_algebras/rs_ordered_abelian_group.con. - -record is_riesz_space (K:ordered_field_ch0) (V:pre_riesz_space K) : Prop ≝ - { rs_compat_le_times: ∀a:K.∀f:V. 0≤a → 0≤f → 0≤a*f - }. - -record riesz_space (K:ordered_field_ch0) : Type \def - { 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. 0≤u → 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 ≝ λK.λS:riesz_space K.λf:S.f ∨ -f. - -(**************** Normed Riesz spaces ****************************) - -definition is_riesz_norm ≝ - λR:real.λV:riesz_space R.λnorm:norm R V. - ∀f,g:V. absolute_value ? V f ≤ absolute_value ? V g → - 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; - 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 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:S.∀n.∀a.∀p:n > O. - absolute_value ? S a ≤ - (inv K (sum_field K n) (not_eq_sum_field_zero K n p))* u → - a = 0 - }. - -record archimedean_riesz_space (K:ordered_field_ch0) : Type \def - { ars_riesz_space:> riesz_space K; - ars_archimedean_property: is_archimedean_riesz_space ? ars_riesz_space - }. - -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 - defining it on Riesz spaces) - 2. Fremlin proves |x|/\u=0 \to u=0. How do we remove the absolute value? - λR:real.λV:archimedean_riesz_space R.λunit: V. - ∀x:V. meet x unit = 0 → u = 0. - 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. 0 archimedean_riesz_space R; - irs_unit: irs_archimedean_riesz_space; - irs_weak_unit: is_weak_unit ? ? irs_unit; - integral: irs_archimedean_riesz_space → R; - irs_positive_linear: is_positive_linear ? ? integral; - irs_limit1: - ∀f:irs_archimedean_riesz_space. - tends_to ? - (λn.integral (f ∧ ((sum_field R n)*irs_unit))) - (integral f); - irs_limit2: - ∀f:irs_archimedean_riesz_space. - tends_to ? - (λn. - integral (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; - irs_quotient_space1: - ∀f,g:irs_archimedean_riesz_space. - integral (absolute_value ? irs_archimedean_riesz_space (f - g)) = 0 → f=g - }. - -definition induced_norm_fun ≝ - λR:real.λV:integration_riesz_space R.λf:V. - integral ? V (absolute_value ? ? f). - -lemma induced_norm_is_norm: - ∀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 positive; - [ apply (irs_positive_linear ? V) - | (* difficile *) - elim daemon - ] - | intros; - unfold induced_norm_fun; - (* facile *) - elim daemon - | intros; - unfold induced_norm_fun; - (* difficile *) - elim daemon - ] - | intros; - unfold induced_norm_fun in H; - apply irs_quotient_space1; - unfold minus; - rewrite < plus_comm; - rewrite < eq_zero_opp_zero; - rewrite > zero_neutral; - assumption - ].*) -qed. - -definition induced_norm ≝ - λR:real.λV:integration_riesz_space R. - mk_norm ? ? (induced_norm_fun ? V) (induced_norm_is_norm ? V). - -lemma is_riesz_norm_induced_norm: - ∀R:real.∀V:integration_riesz_space R. - is_riesz_norm ? ? (induced_norm ? V). - intros; - unfold is_riesz_norm; - intros; - unfold induced_norm; - simplify; - unfold induced_norm_fun; - (* difficile *) - elim daemon. -qed. - -definition induced_riesz_norm ≝ - λR:real.λV:integration_riesz_space R. - mk_riesz_norm ? ? (induced_norm ? V) (is_riesz_norm_induced_norm ? V). - -definition distance_induced_by_integral ≝ - λR:real.λV:integration_riesz_space R. - induced_distance ? ? (induced_norm R V). - -definition is_complete_integration_riesz_space ≝ - λR:real.λV:integration_riesz_space R. - is_complete ? ? (distance_induced_by_integral ? V). - -record complete_integration_riesz_space (R:real) : Type ≝ - { cirz_integration_riesz_space:> integration_riesz_space R; - cirz_complete_integration_riesz_space_property: - is_complete_integration_riesz_space ? cirz_integration_riesz_space - }. - -(* now we prove that any complete integration riesz space is an L-space *) - -(*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; - constructor 1; - [ apply cirz_complete_integration_riesz_space_property - | intros; - unfold induced_riesz_norm; - simplify; - unfold induced_norm; - simplify; - unfold induced_norm_fun; - (* difficile *) - elim daemon - ]. -qed.*) - -(**************************** f-ALGEBRAS ********************************) - -record is_algebra (K: field) (V:vector_space K) (mult:V→V→V) (one:V) : Prop -≝ - { (* ring properties *) - a_ring: is_ring V mult one; - (* algebra properties *) - a_associative_left: ∀a,f,g. a * (mult f g) = mult (a * f) g; - a_associative_right: ∀a,f,g. a * (mult f g) = mult f (a * g) - }. - -record algebra (K: field) : Type \def - { a_vector_space:> vector_space K; - a_one: a_vector_space; - a_mult: a_vector_space → a_vector_space → a_vector_space; - a_algebra_properties: is_algebra ? ? a_mult a_one - }. - -interpretation "Algebra product" 'times a b = - (cic:/matita/integration_algebras/a_mult.con _ a b). - -definition ring_of_algebra ≝ - λK.λA:algebra K. - mk_ring A (a_mult ? A) (a_one ? A) - (a_ring ? ? ? ? (a_algebra_properties ? A)). - -coercion cic:/matita/integration_algebras/ring_of_algebra.con. - -record pre_f_algebra (K:ordered_field_ch0) : Type ≝ - { fa_archimedean_riesz_space:> archimedean_riesz_space K; - fa_algebra_: algebra K; - fa_with: a_vector_space ? fa_algebra_ = rs_vector_space ? fa_archimedean_riesz_space - }. - -lemma fa_algebra: ∀K:ordered_field_ch0.pre_f_algebra K → algebra K. - intros (K A); - apply mk_algebra; - [ apply (rs_vector_space ? A) - | elim daemon - | elim daemon - | elim daemon - ] - qed. - -coercion cic:/matita/integration_algebras/fa_algebra.con. - -record is_f_algebra (K) (A:pre_f_algebra K) : Prop ≝ -{ compat_mult_le: ∀f,g:A.0 ≤ f → 0 ≤ g → 0 ≤ f*g; - compat_mult_meet: - ∀f,g,h:A.(f ∧ g) = 0 → ((h*f) ∧ g) = 0 -}. - -record f_algebra (K:ordered_field_ch0) : Type ≝ -{ fa_pre_f_algebra:> pre_f_algebra K; - fa_f_algebra_properties: is_f_algebra ? fa_pre_f_algebra -}. - -(* to be proved; see footnote 2 in the paper by Spitters *) -axiom symmetric_a_mult: - ∀K.∀A:f_algebra K. symmetric ? (a_mult ? A). - -record integration_f_algebra (R:real) : Type \def - { ifa_integration_riesz_space:> integration_riesz_space R; - ifa_f_algebra_: f_algebra R; - ifa_with: - fa_archimedean_riesz_space ? ifa_f_algebra_ = - irs_archimedean_riesz_space ? ifa_integration_riesz_space - }. - -axiom ifa_f_algebra: ∀R:real.integration_f_algebra R → f_algebra R. - -coercion cic:/matita/integration_algebras/ifa_f_algebra.con. diff --git a/helm/software/matita/dama/metric_space.ma b/helm/software/matita/dama/metric_space.ma index 35e0e0066..d529af83c 100644 --- a/helm/software/matita/dama/metric_space.ma +++ b/helm/software/matita/dama/metric_space.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/metric_space/". -include "ordered_groups.ma". +include "ordered_group.ma". record metric_space (R : ogroup) : Type ≝ { ms_carr :> Type; diff --git a/helm/software/matita/dama/ordered_fields_ch0.ma b/helm/software/matita/dama/ordered_fields_ch0.ma deleted file mode 100644 index d423894d0..000000000 --- a/helm/software/matita/dama/ordered_fields_ch0.ma +++ /dev/null @@ -1,151 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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_fields_ch0/". - -include "fields.ma". -include "ordered_groups.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 pre_ordered_field_ch0: Type ≝ - { of_field:> field; - of_ordered_abelian_group_: ordered_abelian_group; - of_cotransitively_ordered_set_: cotransitively_ordered_set; - of_with1_: - cos_ordered_set of_cotransitively_ordered_set_ = - og_ordered_set of_ordered_abelian_group_; - of_with2: - og_abelian_group of_ordered_abelian_group_ = r_abelian_group of_field - }. - -lemma of_ordered_abelian_group: pre_ordered_field_ch0 → ordered_abelian_group. - intro F; - apply mk_ordered_abelian_group; - [ apply mk_pre_ordered_abelian_group; - [ apply (r_abelian_group F) - | apply (og_ordered_set (of_ordered_abelian_group_ F)) - | apply (eq_f ? ? carrier); - apply (of_with2 F) - ] - | - apply - (eq_rect' ? ? - (λG:abelian_group.λH:og_abelian_group (of_ordered_abelian_group_ F)=G. - is_ordered_abelian_group - (mk_pre_ordered_abelian_group G (of_ordered_abelian_group_ F) - (eq_f abelian_group Type carrier (of_ordered_abelian_group_ F) G - H))) - ? ? (of_with2 F)); - simplify; - apply (og_ordered_abelian_group_properties (of_ordered_abelian_group_ F)) - ] -qed. - -coercion cic:/matita/ordered_fields_ch0/of_ordered_abelian_group.con. - -(*CSC: I am not able to prove this since unfold is undone by coercion composition*) -axiom of_with1: - ∀G:pre_ordered_field_ch0. - cos_ordered_set (of_cotransitively_ordered_set_ G) = - og_ordered_set (of_ordered_abelian_group G). - -lemma of_cotransitively_ordered_set : pre_ordered_field_ch0 → cotransitively_ordered_set. - intro F; - apply mk_cotransitively_ordered_set; - [ apply (og_ordered_set F) - | apply - (eq_rect ? ? (λa:ordered_set.cotransitive (os_carrier a) (os_le a)) - ? ? (of_with1 F)); - apply cos_cotransitive - ] -qed. - -coercion cic:/matita/ordered_fields_ch0/of_cotransitively_ordered_set.con. - -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_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 - }. - -(* -lemma eq_opp_x_times_opp_one_x: ∀F:ordered_field_ch0.∀x:F.-x = -1*x. - intros; - -lemma not_eq_x_zero_to_lt_zero_mult_x_x: - ∀F:ordered_field_ch0.∀x:F. x ≠ 0 → 0 < x * x. - intros; - elim (of_weak_tricotomy ? ? ? ? ? ? ? ? F ? ? H); - [ generalize in match (le_x_zero_to_le_zero_opp_x F ? H1); intro; - 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. 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 tordered_set; + og_with: carr og_abelian_group_ = og_tordered_set +}. + +lemma og_abelian_group: pre_ogroup → abelian_group. +intro G; apply (mk_abelian_group G); [1,2,3: rewrite < (og_with G)] +[apply (plus (og_abelian_group_ G));|apply zero;|apply opp] +unfold apartness_OF_pre_ogroup; cases (og_with G); simplify; +[apply plus_assoc|apply plus_comm|apply zero_neutral|apply opp_inverse|apply plus_strong_ext] +qed. + +coercion cic:/matita/ordered_gorup/og_abelian_group.con. + +record ogroup : Type ≝ { + og_carr:> pre_ogroup; + exc_canc_plusr: ∀f,g,h:og_carr. f+h ≰ g+h → f ≰ g +}. + +notation > "'Ex'≪" non associative with precedence 50 for + @{'excedencerewritel}. + +interpretation "exc_rewl" 'excedencerewritel = + (cic:/matita/excedence/exc_rewl.con _ _ _). + +notation > "'Ex'≫" non associative with precedence 50 for + @{'excedencerewriter}. + +interpretation "exc_rewr" 'excedencerewriter = + (cic:/matita/excedence/exc_rewr.con _ _ _). + +lemma fexc_plusr: + ∀G:ogroup.∀x,y,z:G. x ≰ y → x+z ≰ y + z. +intros 5 (G x y z L); apply (exc_canc_plusr ??? (-z)); +apply (Ex≪ (x + (z + -z)) (plus_assoc ????)); +apply (Ex≪ (x + (-z + z)) (plus_comm ??z)); +apply (Ex≪ (x+0) (opp_inverse ??)); +apply (Ex≪ (0+x) (plus_comm ???)); +apply (Ex≪ x (zero_neutral ??)); +apply (Ex≫ (y + (z + -z)) (plus_assoc ????)); +apply (Ex≫ (y + (-z + z)) (plus_comm ??z)); +apply (Ex≫ (y+0) (opp_inverse ??)); +apply (Ex≫ (0+y) (plus_comm ???)); +apply (Ex≫ y (zero_neutral ??) L); +qed. + +coercion cic:/matita/ordered_gorup/fexc_plusr.con nocomposites. + +lemma exc_canc_plusl: ∀G:ogroup.∀f,g,h:G. h+f ≰ h+g → f ≰ g. +intros 5 (G x y z L); apply (exc_canc_plusr ??? z); +apply (exc_rewl ??? (z+x) (plus_comm ???)); +apply (exc_rewr ??? (z+y) (plus_comm ???) L); +qed. + +lemma fexc_plusl: + ∀G:ogroup.∀x,y,z:G. x ≰ y → z+x ≰ z+y. +intros 5 (G x y z L); apply (exc_canc_plusl ??? (-z)); +apply (exc_rewl ???? (plus_assoc ??z x)); +apply (exc_rewr ???? (plus_assoc ??z y)); +apply (exc_rewl ??? (0+x) (opp_inverse ??)); +apply (exc_rewr ??? (0+y) (opp_inverse ??)); +apply (exc_rewl ???? (zero_neutral ??)); +apply (exc_rewr ???? (zero_neutral ??) L); +qed. + +coercion cic:/matita/ordered_gorup/fexc_plusl.con nocomposites. + +lemma plus_cancr_le: + ∀G:ogroup.∀x,y,z:G.x+z ≤ y + z → x ≤ y. +intros 5 (G x y z L); +apply (le_rewl ??? (0+x) (zero_neutral ??)); +apply (le_rewl ??? (x+0) (plus_comm ???)); +apply (le_rewl ??? (x+(-z+z)) (opp_inverse ??)); +apply (le_rewl ??? (x+(z+ -z)) (plus_comm ??z)); +apply (le_rewl ??? (x+z+ -z) (plus_assoc ????)); +apply (le_rewr ??? (0+y) (zero_neutral ??)); +apply (le_rewr ??? (y+0) (plus_comm ???)); +apply (le_rewr ??? (y+(-z+z)) (opp_inverse ??)); +apply (le_rewr ??? (y+(z+ -z)) (plus_comm ??z)); +apply (le_rewr ??? (y+z+ -z) (plus_assoc ????)); +intro H; apply L; clear L; apply (exc_canc_plusr ??? (-z) H); +qed. + +lemma fle_plusl: ∀G:ogroup. ∀f,g,h:G. f≤g → h+f≤h+g. +intros (G f g h); +apply (plus_cancr_le ??? (-h)); +apply (le_rewl ??? (f+h+ -h) (plus_comm ? f h)); +apply (le_rewl ??? (f+(h+ -h)) (plus_assoc ????)); +apply (le_rewl ??? (f+(-h+h)) (plus_comm ? h (-h))); +apply (le_rewl ??? (f+0) (opp_inverse ??)); +apply (le_rewl ??? (0+f) (plus_comm ???)); +apply (le_rewl ??? (f) (zero_neutral ??)); +apply (le_rewr ??? (g+h+ -h) (plus_comm ? h ?)); +apply (le_rewr ??? (g+(h+ -h)) (plus_assoc ????)); +apply (le_rewr ??? (g+(-h+h)) (plus_comm ??h)); +apply (le_rewr ??? (g+0) (opp_inverse ??)); +apply (le_rewr ??? (0+g) (plus_comm ???)); +apply (le_rewr ??? (g) (zero_neutral ??) H); +qed. + +lemma plus_cancl_le: + ∀G:ogroup.∀x,y,z:G.z+x ≤ z+y → x ≤ y. +intros 5 (G x y z L); +apply (le_rewl ??? (0+x) (zero_neutral ??)); +apply (le_rewl ??? ((-z+z)+x) (opp_inverse ??)); +apply (le_rewl ??? (-z+(z+x)) (plus_assoc ????)); +apply (le_rewr ??? (0+y) (zero_neutral ??)); +apply (le_rewr ??? ((-z+z)+y) (opp_inverse ??)); +apply (le_rewr ??? (-z+(z+y)) (plus_assoc ????)); +apply (fle_plusl ??? (-z) L); +qed. + +lemma exc_opp_x_zero_to_exc_zero_x: + ∀G:ogroup.∀x:G.-x ≰ 0 → 0 ≰ x. +intros (G x H); apply (exc_canc_plusr ??? (-x)); +apply (exc_rewr ???? (plus_comm ???)); +apply (exc_rewr ???? (opp_inverse ??)); +apply (exc_rewl ???? (zero_neutral ??) H); +qed. + +lemma le_zero_x_to_le_opp_x_zero: + ∀G:ogroup.∀x:G.0 ≤ x → -x ≤ 0. +intros (G x Px); apply (plus_cancr_le ??? x); +apply (le_rewl ??? 0 (opp_inverse ??)); +apply (le_rewr ??? x (zero_neutral ??) Px); +qed. + +lemma exc_zero_opp_x_to_exc_x_zero: + ∀G:ogroup.∀x:G. 0 ≰ -x → x ≰ 0. +intros (G x H); apply (exc_canc_plusl ??? (-x)); +apply (exc_rewr ???? (plus_comm ???)); +apply (exc_rewl ???? (opp_inverse ??)); +apply (exc_rewr ???? (zero_neutral ??) H); +qed. + +lemma le_x_zero_to_le_zero_opp_x: + ∀G:ogroup.∀x:G. x ≤ 0 → 0 ≤ -x. +intros (G x Lx0); apply (plus_cancr_le ??? x); +apply (le_rewr ??? 0 (opp_inverse ??)); +apply (le_rewl ??? x (zero_neutral ??)); +assumption; +qed. + +lemma lt0plus_orlt: + ∀G:ogroup. ∀x,y:G. 0 ≤ x → 0 ≤ y → 0 < x + y → 0 < x ∨ 0 < y. +intros (G x y LEx LEy LT); cases LT (H1 H2); cases (ap_cotransitive ??? y H2); +[right; split; assumption|left;split;[assumption]] +apply (plus_cancr_ap ??? y); apply (ap_rewl ???? (zero_neutral ??)); +assumption; +qed. diff --git a/helm/software/matita/dama/ordered_groups.ma b/helm/software/matita/dama/ordered_groups.ma deleted file mode 100644 index 74188d8a0..000000000 --- a/helm/software/matita/dama/ordered_groups.ma +++ /dev/null @@ -1,170 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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_groups/". - -include "ordered_set.ma". -include "groups.ma". - -record pre_ogroup : Type ≝ { - og_abelian_group_: abelian_group; - og_tordered_set:> tordered_set; - og_with: carr og_abelian_group_ = og_tordered_set -}. - -lemma og_abelian_group: pre_ogroup → abelian_group. -intro G; apply (mk_abelian_group G); [1,2,3: rewrite < (og_with G)] -[apply (plus (og_abelian_group_ G));|apply zero;|apply opp] -unfold apartness_OF_pre_ogroup; cases (og_with G); simplify; -[apply plus_assoc|apply plus_comm|apply zero_neutral|apply opp_inverse|apply plus_strong_ext] -qed. - -coercion cic:/matita/ordered_groups/og_abelian_group.con. - -record ogroup : Type ≝ { - og_carr:> pre_ogroup; - exc_canc_plusr: ∀f,g,h:og_carr. f+h ≰ g+h → f ≰ g -}. - -notation > "'Ex'≪" non associative with precedence 50 for - @{'excedencerewritel}. - -interpretation "exc_rewl" 'excedencerewritel = - (cic:/matita/excedence/exc_rewl.con _ _ _). - -notation > "'Ex'≫" non associative with precedence 50 for - @{'excedencerewriter}. - -interpretation "exc_rewr" 'excedencerewriter = - (cic:/matita/excedence/exc_rewr.con _ _ _). - -lemma fexc_plusr: - ∀G:ogroup.∀x,y,z:G. x ≰ y → x+z ≰ y + z. -intros 5 (G x y z L); apply (exc_canc_plusr ??? (-z)); -apply (Ex≪ (x + (z + -z)) (plus_assoc ????)); -apply (Ex≪ (x + (-z + z)) (plus_comm ??z)); -apply (Ex≪ (x+0) (opp_inverse ??)); -apply (Ex≪ (0+x) (plus_comm ???)); -apply (Ex≪ x (zero_neutral ??)); -apply (Ex≫ (y + (z + -z)) (plus_assoc ????)); -apply (Ex≫ (y + (-z + z)) (plus_comm ??z)); -apply (Ex≫ (y+0) (opp_inverse ??)); -apply (Ex≫ (0+y) (plus_comm ???)); -apply (Ex≫ y (zero_neutral ??) L); -qed. - -coercion cic:/matita/ordered_groups/fexc_plusr.con nocomposites. - -lemma exc_canc_plusl: ∀G:ogroup.∀f,g,h:G. h+f ≰ h+g → f ≰ g. -intros 5 (G x y z L); apply (exc_canc_plusr ??? z); -apply (exc_rewl ??? (z+x) (plus_comm ???)); -apply (exc_rewr ??? (z+y) (plus_comm ???) L); -qed. - -lemma fexc_plusl: - ∀G:ogroup.∀x,y,z:G. x ≰ y → z+x ≰ z+y. -intros 5 (G x y z L); apply (exc_canc_plusl ??? (-z)); -apply (exc_rewl ???? (plus_assoc ??z x)); -apply (exc_rewr ???? (plus_assoc ??z y)); -apply (exc_rewl ??? (0+x) (opp_inverse ??)); -apply (exc_rewr ??? (0+y) (opp_inverse ??)); -apply (exc_rewl ???? (zero_neutral ??)); -apply (exc_rewr ???? (zero_neutral ??) L); -qed. - -coercion cic:/matita/ordered_groups/fexc_plusl.con nocomposites. - -lemma plus_cancr_le: - ∀G:ogroup.∀x,y,z:G.x+z ≤ y + z → x ≤ y. -intros 5 (G x y z L); -apply (le_rewl ??? (0+x) (zero_neutral ??)); -apply (le_rewl ??? (x+0) (plus_comm ???)); -apply (le_rewl ??? (x+(-z+z)) (opp_inverse ??)); -apply (le_rewl ??? (x+(z+ -z)) (plus_comm ??z)); -apply (le_rewl ??? (x+z+ -z) (plus_assoc ????)); -apply (le_rewr ??? (0+y) (zero_neutral ??)); -apply (le_rewr ??? (y+0) (plus_comm ???)); -apply (le_rewr ??? (y+(-z+z)) (opp_inverse ??)); -apply (le_rewr ??? (y+(z+ -z)) (plus_comm ??z)); -apply (le_rewr ??? (y+z+ -z) (plus_assoc ????)); -intro H; apply L; clear L; apply (exc_canc_plusr ??? (-z) H); -qed. - -lemma fle_plusl: ∀G:ogroup. ∀f,g,h:G. f≤g → h+f≤h+g. -intros (G f g h); -apply (plus_cancr_le ??? (-h)); -apply (le_rewl ??? (f+h+ -h) (plus_comm ? f h)); -apply (le_rewl ??? (f+(h+ -h)) (plus_assoc ????)); -apply (le_rewl ??? (f+(-h+h)) (plus_comm ? h (-h))); -apply (le_rewl ??? (f+0) (opp_inverse ??)); -apply (le_rewl ??? (0+f) (plus_comm ???)); -apply (le_rewl ??? (f) (zero_neutral ??)); -apply (le_rewr ??? (g+h+ -h) (plus_comm ? h ?)); -apply (le_rewr ??? (g+(h+ -h)) (plus_assoc ????)); -apply (le_rewr ??? (g+(-h+h)) (plus_comm ??h)); -apply (le_rewr ??? (g+0) (opp_inverse ??)); -apply (le_rewr ??? (0+g) (plus_comm ???)); -apply (le_rewr ??? (g) (zero_neutral ??) H); -qed. - -lemma plus_cancl_le: - ∀G:ogroup.∀x,y,z:G.z+x ≤ z+y → x ≤ y. -intros 5 (G x y z L); -apply (le_rewl ??? (0+x) (zero_neutral ??)); -apply (le_rewl ??? ((-z+z)+x) (opp_inverse ??)); -apply (le_rewl ??? (-z+(z+x)) (plus_assoc ????)); -apply (le_rewr ??? (0+y) (zero_neutral ??)); -apply (le_rewr ??? ((-z+z)+y) (opp_inverse ??)); -apply (le_rewr ??? (-z+(z+y)) (plus_assoc ????)); -apply (fle_plusl ??? (-z) L); -qed. - -lemma exc_opp_x_zero_to_exc_zero_x: - ∀G:ogroup.∀x:G.-x ≰ 0 → 0 ≰ x. -intros (G x H); apply (exc_canc_plusr ??? (-x)); -apply (exc_rewr ???? (plus_comm ???)); -apply (exc_rewr ???? (opp_inverse ??)); -apply (exc_rewl ???? (zero_neutral ??) H); -qed. - -lemma le_zero_x_to_le_opp_x_zero: - ∀G:ogroup.∀x:G.0 ≤ x → -x ≤ 0. -intros (G x Px); apply (plus_cancr_le ??? x); -apply (le_rewl ??? 0 (opp_inverse ??)); -apply (le_rewr ??? x (zero_neutral ??) Px); -qed. - -lemma exc_zero_opp_x_to_exc_x_zero: - ∀G:ogroup.∀x:G. 0 ≰ -x → x ≰ 0. -intros (G x H); apply (exc_canc_plusl ??? (-x)); -apply (exc_rewr ???? (plus_comm ???)); -apply (exc_rewl ???? (opp_inverse ??)); -apply (exc_rewr ???? (zero_neutral ??) H); -qed. - -lemma le_x_zero_to_le_zero_opp_x: - ∀G:ogroup.∀x:G. x ≤ 0 → 0 ≤ -x. -intros (G x Lx0); apply (plus_cancr_le ??? x); -apply (le_rewr ??? 0 (opp_inverse ??)); -apply (le_rewl ??? x (zero_neutral ??)); -assumption; -qed. - -lemma lt0plus_orlt: - ∀G:ogroup. ∀x,y:G. 0 ≤ x → 0 ≤ y → 0 < x + y → 0 < x ∨ 0 < y. -intros (G x y LEx LEy LT); cases LT (H1 H2); cases (ap_cotransitive ??? y H2); -[right; split; assumption|left;split;[assumption]] -apply (plus_cancr_ap ??? y); apply (ap_rewl ???? (zero_neutral ??)); -assumption; -qed. diff --git a/helm/software/matita/dama/preweighted_lattice.ma b/helm/software/matita/dama/preweighted_lattice.ma index 9a46fb319..39105c0fd 100644 --- a/helm/software/matita/dama/preweighted_lattice.ma +++ b/helm/software/matita/dama/preweighted_lattice.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/preweighted_lattice/". -include "ordered_groups.ma". +include "ordered_group.ma". record wlattice (R : ogroup) : Type ≝ { wl_carr:> Type; diff --git a/helm/software/matita/dama/reals.ma b/helm/software/matita/dama/reals.ma deleted file mode 100644 index d57e6cfba..000000000 --- a/helm/software/matita/dama/reals.ma +++ /dev/null @@ -1,172 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/reals/". - -include "ordered_fields_ch0.ma". - -record is_real (F:ordered_field_ch0) : Type -≝ - { r_archimedean: ∀x:F. ∃n:nat. x ≤ (sum_field ? 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 - }. - -definition lim: ∀R:real.∀f:nat→R.is_cauchy_seq ? f → R. - intros; - elim (r_complete ? (r_real_properties R) ? H); - exact a. -qed. - -definition max_seq: ∀R:real.∀x,y:R. nat → R. - intros (R x y); - elim (cos_cotransitive R 0 (inv ? (sum_field ? (S n)) ?) (x-y)); - [ apply x - | apply not_eq_sum_field_zero ; - unfold; - autobatch - | apply y - | apply lt_zero_to_le_inv_zero - ]. -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 (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 (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) - (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; - split; - [ apply (le_zero_x_to_le_opp_x_zero R ?); - apply lt_zero_to_le_inv_zero - | apply lt_zero_to_le_inv_zero - ] - | simplify; - split; - [ apply (or_transitive ? ? R ? 0); - [ apply (le_zero_x_to_le_opp_x_zero R ?) - | assumption - ] - | assumption - ] - ] - | simplify; - 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) - (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m))))); - [ simplify; - split; - [ elim daemon - | generalize in match (le_zero_x_to_le_opp_x_zero R ? t1); - intro; - unfold minus in H1; - rewrite > eq_opp_plus_plus_opp_opp in H1; - rewrite > eq_opp_opp_x_x in H1; - rewrite > plus_comm in H1; - apply (or_transitive ? ? R ? 0); - [ assumption - | apply lt_zero_to_le_inv_zero - ] - ] - | simplify; - rewrite > (plus_comm ? y (-y)); - rewrite > opp_inverse; - split; - [ elim daemon - | apply lt_zero_to_le_inv_zero - ] - ] - ]. - elim daemon.*) -qed. - -definition max: ∀R:real.R → R → R. - intros (R x y); - apply (lim R (max_seq R x y)); - apply cauchy_max_seq. -qed. - -definition abs \def λR:real.λx:R. max R x (-x). - -lemma comparison: - ∀R:real.∀f,g:nat→R. is_cauchy_seq ? f → is_cauchy_seq ? g → - (∀n:nat.f n ≤ g n) → lim ? f ? ≤ lim ? g ?. - [ assumption - | assumption - | intros; - elim daemon - ]. -qed. - -definition to_zero ≝ - λR:real.λn. - -(inv R (sum_field R (S n)) - (not_eq_sum_field_zero R (S n) (le_S_S O n (le_O_n n)))). - -axiom is_cauchy_seq_to_zero: ∀R:real. is_cauchy_seq ? (to_zero R). - -lemma technical1: ∀R:real.lim R (to_zero R) (is_cauchy_seq_to_zero R) = 0. - intros; - unfold lim; - elim daemon. -qed. - -lemma abs_x_ge_O: ∀R:real.∀x:R. 0 ≤ abs ? x. - intros; - unfold abs; - unfold max; - rewrite < technical1; - apply comparison; - intros; - unfold to_zero; - unfold max_seq; - elim - (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) - (not_eq_sum_field_zero R (S n) (le_S_S O n (le_O_n n))))); - [ simplify; - (* facile *) - elim daemon - | simplify; - (* facile *) - elim daemon - ]. -qed. \ No newline at end of file diff --git a/helm/software/matita/dama/rings.ma b/helm/software/matita/dama/rings.ma deleted file mode 100644 index 3ed2fab25..000000000 --- a/helm/software/matita/dama/rings.ma +++ /dev/null @@ -1,103 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/rings/". - -include "groups.ma". - -record is_ring (G:abelian_group) (mult:G→G→G) (one:G) : Prop -≝ - { (* multiplicative monoid properties *) - mult_assoc_: associative ? mult; - one_neutral_left_: left_neutral ? mult one; - one_neutral_right_: right_neutral ? mult one; - (* ring properties *) - mult_plus_distr_left_: distributive_left ? mult (plus G); - mult_plus_distr_right_: distributive_right ? mult (plus G); - not_eq_zero_one_: (0 ≠ one) - }. - -record ring : Type \def - { r_abelian_group:> abelian_group; - mult: r_abelian_group → r_abelian_group → r_abelian_group; - one: r_abelian_group; - r_ring_properties: is_ring r_abelian_group mult one - }. - -theorem mult_assoc: ∀R:ring.associative ? (mult R). - intros; - apply (mult_assoc_ ? ? ? (r_ring_properties R)). -qed. - -theorem one_neutral_left: ∀R:ring.left_neutral ? (mult R) (one R). - intros; - apply (one_neutral_left_ ? ? ? (r_ring_properties R)). -qed. - -theorem one_neutral_right: ∀R:ring.right_neutral ? (mult R) (one R). - intros; - apply (one_neutral_right_ ? ? ? (r_ring_properties R)). -qed. - -theorem mult_plus_distr_left: ∀R:ring.distributive_left ? (mult R) (plus R). - intros; - apply (mult_plus_distr_left_ ? ? ? (r_ring_properties R)). -qed. - -theorem mult_plus_distr_right: ∀R:ring.distributive_right ? (mult R) (plus R). - intros; - apply (mult_plus_distr_right_ ? ? ? (r_ring_properties R)). -qed. - -theorem not_eq_zero_one: ∀R:ring.0 ≠ one R. - intros; - apply (not_eq_zero_one_ ? ? ? (r_ring_properties R)). -qed. - -interpretation "Ring mult" 'times a b = - (cic:/matita/rings/mult.con _ a b). - -notation "1" with precedence 89 -for @{ 'one }. - -interpretation "Ring one" 'one = - (cic:/matita/rings/one.con _). - -lemma eq_mult_zero_x_zero: ∀R:ring.∀x:R.0*x=0. - intros; - generalize in match (zero_neutral R 0); intro; - generalize in match (eq_f ? ? (λy.y*x) ? ? H); intro; clear H; - rewrite > mult_plus_distr_right in H1; - generalize in match (eq_f ? ? (λy.-(0*x)+y) ? ? H1); intro; clear H1; - rewrite < plus_assoc in H; - rewrite > opp_inverse in H; - rewrite > zero_neutral in H; - assumption. -qed. - -lemma eq_mult_x_zero_zero: ∀R:ring.∀x:R.x*0=0. -intros; -generalize in match (zero_neutral R 0); -intro; -generalize in match (eq_f ? ? (λy.x*y) ? ? H); intro; clear H; -(*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; -rewrite > opp_inverse in H; -rewrite > zero_neutral in H; -assumption. -qed. - diff --git a/helm/software/matita/dama/vector_spaces.ma b/helm/software/matita/dama/vector_spaces.ma deleted file mode 100644 index 6aaebd12b..000000000 --- a/helm/software/matita/dama/vector_spaces.ma +++ /dev/null @@ -1,151 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/vector_spaces/". - -include "reals.ma". - -record is_vector_space (K: field) (G:abelian_group) (emult:K→G→G) : Prop -≝ - { vs_nilpotent: ∀v. emult 0 v = 0; - vs_neutral: ∀v. emult 1 v = v; - vs_distributive: ∀a,b,v. emult (a + b) v = (emult a v) + (emult b v); - vs_associative: ∀a,b,v. emult (a * b) v = emult a (emult b v) - }. - -record vector_space (K:field): Type \def -{ vs_abelian_group :> abelian_group; - emult: K → vs_abelian_group → vs_abelian_group; - vs_vector_space_properties :> is_vector_space ? vs_abelian_group emult -}. - -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. 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 - }. - -theorem eq_semi_norm_zero_zero: - ∀R:real.∀V:vector_space R.∀semi_norm:V→R. - is_semi_norm ? ? semi_norm → - semi_norm 0 = 0. - intros; - (* facile *) - elim daemon. -qed. - -record is_norm (R:real) (V:vector_space R) (norm:V → R) : Prop ≝ - { n_semi_norm:> is_semi_norm ? ? norm; - n_properness: ∀x:V. norm x = 0 → x = 0 - }. - -record norm (R:real) (V:vector_space R) : Type ≝ - { n_function:1> V→R; - n_norm_properties: is_norm ? ? n_function - }. - -record is_semi_distance (R:real) (C:Type) (semi_d: C→C→R) : Prop ≝ - { 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 - }. - -record is_distance (R:real) (C:Type) (d:C→C→R) : Prop ≝ - { d_semi_distance:> is_semi_distance ? ? d; - d_properness: ∀x,y:C. d x y = 0 → x=y - }. - -record distance (R:real) (V:vector_space R) : Type ≝ - { d_function:2> V→V→R; - d_distance_properties: is_distance ? ? d_function - }. - -definition induced_distance_fun ≝ - λR:real.λV:vector_space R.λnorm:norm ? V. - λf,g:V.norm (f - g). - -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; - [ unfold induced_distance_fun; - intros; - apply sn_positive; - apply n_semi_norm; - apply (n_norm_properties ? ? norm) - | unfold induced_distance_fun; - intros; - unfold minus; - rewrite < plus_comm; - rewrite > opp_inverse; - apply eq_semi_norm_zero_zero; - apply n_semi_norm; - apply (n_norm_properties ? ? norm) - | unfold induced_distance_fun; - intros; - (* ??? *) - elim daemon - ] - | unfold induced_distance_fun; - intros; - generalize in match (n_properness ? ? norm ? ? H); - [ intro; - (* facile *) - elim daemon - | apply (n_norm_properties ? ? norm) - ] - ].*) -qed. - -definition induced_distance ≝ - λR:real.λV:vector_space R.λnorm:norm ? V. - mk_distance ? ? (induced_distance_fun ? ? norm) - (induced_distance_is_distance ? ? norm). - -definition tends_to : - ∀R:real.∀V:vector_space R.∀d:distance ? V.∀f:nat→V.∀l:V.Prop. -apply - (λR:real.λV:vector_space R.λd:distance ? V.λf:nat→V.λl:V. - ∀n:nat.∃m:nat.∀j:nat. m ≤ j → - d (f j) l ≤ inv R (sum_field ? (S n)) ?); - apply not_eq_sum_field_zero; - unfold; - autobatch. -qed. - -definition is_cauchy_seq : ∀R:real.\forall V:vector_space R. -\forall d:distance ? V.∀f:nat→V.Prop. - apply - (λR:real.λV: vector_space R. \lambda d:distance ? V. - \lambda f:nat→V. - ∀m:nat. - ∃n:nat.∀N. n ≤ N → - -(inv R (sum_field ? (S m)) ?) ≤ d (f N) (f n) ∧ - d (f N) (f n)≤ inv R (sum_field R (S m)) ?); - apply not_eq_sum_field_zero; - unfold; - autobatch. -qed. - -definition is_complete ≝ - λR:real.λV:vector_space R. - λd:distance ? V. - ∀f:nat→V. is_cauchy_seq ? ? d f→ - ex V (λl:V. tends_to ? ? d f l).