From 9791cd146bc0b8df953aee7bb8a3df60553b530c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Nov 2007 11:36:52 +0000 Subject: [PATCH] bir georganization, most of the structures done --- .../dama/classical_pointfree/ordered_sets.ma | 2 +- .../matita/dama/constructive_connectives.ma | 2 +- .../constructive_higher_order_relations.ma | 13 +++ .../dama/constructive_pointfree/lebesgue.ma | 93 +------------------ helm/software/matita/dama/excedence.ma | 19 ++++ helm/software/matita/dama/groups.ma | 22 +++++ helm/software/matita/dama/lattice.ma | 21 ++--- helm/software/matita/dama/metric_lattice.ma | 18 ++-- .../dama/{metric_set.ma => metric_space.ma} | 28 +++++- helm/software/matita/dama/ordered_groups.ma | 10 +- helm/software/matita/dama/ordered_set.ma | 45 +++++++++ .../software/matita/dama/premetric_lattice.ma | 60 ++++++++++++ .../dama/{ordered_sets.ma => sequence.ma} | 46 +-------- 13 files changed, 219 insertions(+), 160 deletions(-) rename helm/software/matita/dama/{metric_set.ma => metric_space.ma} (57%) create mode 100644 helm/software/matita/dama/ordered_set.ma create mode 100644 helm/software/matita/dama/premetric_lattice.ma rename helm/software/matita/dama/{ordered_sets.ma => sequence.ma} (81%) diff --git a/helm/software/matita/dama/classical_pointfree/ordered_sets.ma b/helm/software/matita/dama/classical_pointfree/ordered_sets.ma index 18658cf7a..604da01d6 100644 --- a/helm/software/matita/dama/classical_pointfree/ordered_sets.ma +++ b/helm/software/matita/dama/classical_pointfree/ordered_sets.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/classical_pointwise/ordered_sets/". -include "ordered_sets.ma". +include "ordered_set.ma". 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); diff --git a/helm/software/matita/dama/constructive_connectives.ma b/helm/software/matita/dama/constructive_connectives.ma index 2cf0d8d58..0a840d5a5 100644 --- a/helm/software/matita/dama/constructive_connectives.ma +++ b/helm/software/matita/dama/constructive_connectives.ma @@ -43,4 +43,4 @@ alias id "False" = "cic:/matita/logic/connectives/False.ind#xpointer(1/1)". definition Not ≝ λx:Type.x → False. interpretation "constructive not" 'not x = - (cic:/matita/constructive_connectives/Not.con x). \ No newline at end of file + (cic:/matita/constructive_connectives/Not.con x). diff --git a/helm/software/matita/dama/constructive_higher_order_relations.ma b/helm/software/matita/dama/constructive_higher_order_relations.ma index cf58e2640..789c7c9c5 100644 --- a/helm/software/matita/dama/constructive_higher_order_relations.ma +++ b/helm/software/matita/dama/constructive_higher_order_relations.ma @@ -35,3 +35,16 @@ definition associative ≝ definition commutative ≝ λC:Type.λop:C→C→C.λeq:C→C→Type.∀x,y. eq (op x y) (op y x). + +alias id "antisymmetric" = "cic:/matita/higher_order_defs/relations/antisymmetric.con". +theorem antisimmetric_to_cotransitive_to_transitive: + ∀C:Type.∀le:C→C→Prop. antisymmetric ? le → cotransitive ? le → transitive ? le. +intros (T f Af cT); unfold transitive; intros (x y z fxy fyz); +lapply (cT ??z fxy) as H; cases H; [assumption] cases (Af ? ? fyz H1); +qed. + +lemma Or_symmetric: symmetric ? Or. +unfold; intros (x y H); cases H; [right|left] assumption; +qed. + + \ No newline at end of file diff --git a/helm/software/matita/dama/constructive_pointfree/lebesgue.ma b/helm/software/matita/dama/constructive_pointfree/lebesgue.ma index 0dac6fc99..1eb6e4aac 100644 --- a/helm/software/matita/dama/constructive_pointfree/lebesgue.ma +++ b/helm/software/matita/dama/constructive_pointfree/lebesgue.ma @@ -14,95 +14,8 @@ set "baseuri" "cic:/matita/lebesgue/". -include "reals.ma". -include "lattice.ma". +include "metric_lattice.ma". +include "sequence.ma". -axiom ltT : ∀R:real.∀a,b:R.Type. - - -alias symbol "or" = "constructive or". -definition rapart ≝ λR:real.λa,b:R.a < b ∨ b < a. +(* Section 3.2 *) -notation "a # b" non associative with precedence 50 for - @{ 'apart $a $b}. -notation "a \approx b" non associative with precedence 50 for - @{ 'napart $a $b}. -interpretation "real apartness" 'apart a b = - (cic:/matita/lebesgue/rapart.con _ a b). -interpretation "real non apartness" 'napart a b = - (cic:/matita/constructive_connectives/Not.con - (cic:/matita/lebesgue/rapart.con _ a b)). - -record is_semi_metric (R : real) (T : Type) (d : T → T → R): Prop ≝ { - sm_positive: ∀a,b:T. d a b ≤ 0; - sm_reflexive: ∀a. d a a ≈ 0; - sm_symmetric: ∀a,b. d a b ≈ d b a; - sm_tri_ineq: ∀a,b,c:T. d a b ≤ d a c + d c b -}. - -record semimetric_set (R : real) : Type ≝ { - ms_carr :> Type; - ms_semimetric: ms_carr → ms_carr → R; - ms_properties:> is_semi_metric R ms_carr ms_semimetric -}. - -notation < "\nbsp \delta a \nbsp b" non associative with precedence 80 for @{ 'delta2 $a $b}. -interpretation "semimetric" 'delta2 a b = (cic:/matita/lebesgue/ms_semimetric.con _ _ a b). -notation "\delta" non associative with precedence 80 for @{ 'delta }. -interpretation "semimetric" 'delta = (cic:/matita/lebesgue/ms_semimetric.con _ _). - -record pre_semimetric_lattice (R : real) : Type ≝ { - ml_lattice :> lattice; - ml_semimetric_set_ : semimetric_set R; - with_ml_lattice_eq_ml_semimetric_set_: ms_carr ? ml_semimetric_set_ = ml_lattice -}. - -lemma ml_semimetric_set : ∀R.∀ms:pre_semimetric_lattice R. semimetric_set R. -intros (R ml); constructor 1; [apply (ml : Type);] -cases ml (l ms with_); clear ml; simplify; -[1: rewrite < with_; apply (ms_semimetric ? ms); -|2: cases with_; simplify; apply (ms_properties ? ms);] -qed. - -coercion cic:/matita/lebesgue/ml_semimetric_set.con. - -record is_semimetric_lattice (R : real) (ml : pre_semimetric_lattice R) : Prop ≝ { - prop1a: ∀a : ml.δ (a ∧ a) a ≈ 0; - prop1b: ∀a : ml.δ (a ∨ a) a ≈ 0; - prop2a: ∀a,b: ml. δ (a ∨ b) (b ∨ a) ≈ 0; - prop2b: ∀a,b: ml. δ (a ∧ b) (b ∧ a) ≈ 0; - prop3a: ∀a,b,c: ml. δ (a ∨ (b ∨ c)) ((a ∨ b) ∨ c) ≈ 0; - prop3b: ∀a,b,c: ml. δ (a ∧ (b ∧ c)) ((a ∧ b) ∧ c) ≈ 0; - prop4a: ∀a,b: ml. δ (a ∨ (a ∧ b)) a ≈ 0; - prop4b: ∀a,b: ml. δ (a ∧ (a ∨ b)) a ≈ 0; - prop5: ∀a,b,c: ml. δ (a ∨ b) (a ∨ c) + δ (a ∧ b) (a ∧ c) ≤ δ b c -}. - -record semimetric_lattice (R : real) : Type ≝ { - ml_pre_semimetric_lattice:> pre_semimetric_lattice R; - ml_semimetric_lattice_properties: is_semimetric_lattice R ml_pre_semimetric_lattice -}. - -definition apart:= - λR: real. λml: semimetric_lattice R. λa,b: ml. - (* 0 < δ a b *) ltT ? 0 (δ a b). - (* < scazzato, ma CSC dice che poi si cambia dopo *) - -interpretation "semimetric lattice apartness" 'apart a b = - (cic:/matita/lebesgue/apart.con _ _ a b). -interpretation "semimetric lattice non apartness" 'napart a b = - (cic:/matita/constructive_connectives/Not.con - (cic:/matita/lebesgue/apart.con _ _ a b)). - - -lemma triangular_inequality : ∀R: real. ∀ms: semimetric_set R.∀a,b,c:ms. - δ a b ≤ δ a c + δ c b. -intros (R ms a b c); exact (sm_tri_ineq R ms (ms_semimetric R ms) ms a b c); -qed. - -lemma foo : ∀R: real. ∀ml: semimetric_lattice R.∀a,b,a1,b1: ml. - a ≈ a1 → b ≈ b1 → (δ a b ≈ δ a1 b1). -intros; -lapply (triangular_inequality ? ? a b a1) as H1; -lapply (triangular_inequality ? ? a1 b b1) as H2; -lapply (og_ordered_abelian_group_properties R ? ? (δ a a1) H2) as H3; diff --git a/helm/software/matita/dama/excedence.ma b/helm/software/matita/dama/excedence.ma index c2a5ffd4f..83dcbf702 100644 --- a/helm/software/matita/dama/excedence.ma +++ b/helm/software/matita/dama/excedence.ma @@ -97,6 +97,7 @@ qed. lemma eq_trans:∀E:apartness.∀x,y,z:E.x ≈ y → y ≈ z → x ≈ z ≝ eq_trans_. (* BUG: vedere se ricapita *) +alias id "antisymmetric" = "cic:/matita/constructive_higher_order_relations/antisymmetric.con". lemma le_antisymmetric: ∀E.antisymmetric ? (le E) (eq ?). intros 5 (E x y Lxy Lyx); intro H; cases H; [apply Lxy;|apply Lyx] assumption; @@ -160,3 +161,21 @@ lemma exc_rewr: ∀A:excedence.∀x,z,y:A. x ≈ y → z ≰ y → z ≰ x. intros (A x z y Exy Azy); elim (exc_cotransitive ???x Azy); [assumption] elim (Exy); left; assumption; qed. + +lemma lt_rewr: ∀A:excedence.∀x,z,y:A. x ≈ y → z < y → z < x. +intros (A x y z E H); split; elim H; +[apply (le_rewr ???? (eq_sym ??? E));|apply (ap_rewr ???? E)] assumption; +qed. + +lemma lt_rewl: ∀A:excedence.∀x,z,y:A. x ≈ y → y < z → x < z. +intros (A x y z E H); split; elim H; +[apply (le_rewl ???? (eq_sym ??? E));| apply (ap_rewl ???? E);] assumption; +qed. + +lemma lt_le_transitive: ∀A:excedence.∀x,y,z:A.x < y → y ≤ z → x < z. +intros (A x y z LT LE); cases LT (LEx APx); split; [apply (le_transitive ???? LEx LE)] +whd in LE LEx APx; cases APx (EXx EXx); [cases (LEx EXx)] +cases (exc_cotransitive ??? z EXx) (EXz EXz); [cases (LE EXz)] +right; assumption; +qed. + diff --git a/helm/software/matita/dama/groups.ma b/helm/software/matita/dama/groups.ma index f2b4bd01c..c00740ee9 100644 --- a/helm/software/matita/dama/groups.ma +++ b/helm/software/matita/dama/groups.ma @@ -205,3 +205,25 @@ 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/lattice.ma b/helm/software/matita/dama/lattice.ma index a1cea05b0..398b1af89 100644 --- a/helm/software/matita/dama/lattice.ma +++ b/helm/software/matita/dama/lattice.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/lattices/". +set "baseuri" "cic:/matita/lattice/". include "excedence.ma". @@ -22,15 +22,20 @@ record lattice : Type ≝ { meet: l_carr → l_carr → l_carr; join_comm: ∀x,y:l_carr. join x y ≈ join y x; meet_comm: ∀x,y:l_carr. meet x y ≈ meet y x; - join_assoc: ∀x,y,z:l_carr. join x (join y z) ≈ join (join y x) z; - meet_assoc: ∀x,y,z:l_carr. meet x (meet y z) ≈ meet (meet y x) z; + join_assoc: ∀x,y,z:l_carr. join x (join y z) ≈ join (join x y) z; + meet_assoc: ∀x,y,z:l_carr. meet x (meet y z) ≈ meet (meet x y) z; absorbjm: ∀f,g:l_carr. join f (meet f g) ≈ f; absorbmj: ∀f,g:l_carr. meet f (join f g) ≈ f }. +interpretation "Lattice meet" 'and a b = + (cic:/matita/lattice/meet.con _ a b). + +interpretation "Lattice join" 'or a b = + (cic:/matita/lattice/join.con _ a b). (* -include "ordered_sets.ma". +include "ordered_set.ma". record lattice (C:Type) (join,meet:C→C→C) : Prop \def { (* abelian semigroup properties *) @@ -50,12 +55,6 @@ record lattice : Type \def l_lattice_properties:> is_lattice ? l_join l_meet }. -interpretation "Lattice meet" 'and a b = - (cic:/matita/lattices/l_meet.con _ a b). - -interpretation "Lattice join" 'or a b = - (cic:/matita/lattices/l_join.con _ a b). - definition le \def λL:lattice.λf,g:L. (f ∧ g) = f. definition ordered_set_of_lattice: lattice → ordered_set. @@ -91,4 +90,4 @@ definition ordered_set_of_lattice: lattice → ordered_set. qed. coercion cic:/matita/lattices/ordered_set_of_lattice.con. -*) \ No newline at end of file +*) diff --git a/helm/software/matita/dama/metric_lattice.ma b/helm/software/matita/dama/metric_lattice.ma index 62a84090c..c8a9c895f 100644 --- a/helm/software/matita/dama/metric_lattice.ma +++ b/helm/software/matita/dama/metric_lattice.ma @@ -14,21 +14,21 @@ set "baseuri" "cic:/matita/metric_lattice/". -include "metric_set.ma". +include "metric_space.ma". include "lattice.ma". record mlattice (R : ogroup) : Type ≝ { - ml_mset_: metric_set R; + ml_mspace_: metric_space R; ml_lattice:> lattice; - ml_with_: ms_carr ? ml_mset_ = ap_carr (l_carr ml_lattice) + ml_with_: ms_carr ? ml_mspace_ = ap_carr (l_carr ml_lattice) }. -lemma ml_mset: ∀R.mlattice R → metric_set R. -intros (R ml); apply (mk_metric_set R ml); unfold Type_OF_mlattice; +lemma ml_mspace: ∀R.mlattice R → metric_space R. +intros (R ml); apply (mk_metric_space R ml); unfold Type_OF_mlattice; cases (ml_with_ ? ml); simplify; -[apply (metric ? (ml_mset_ ? ml));|apply (mpositive ? (ml_mset_ ? ml)); -|apply (mreflexive ? (ml_mset_ ? ml));|apply (msymmetric ? (ml_mset_ ? ml)); -|apply (mtineq ? (ml_mset_ ? ml))] +[apply (metric ? (ml_mspace_ ? ml));|apply (mpositive ? (ml_mspace_ ? ml)); +|apply (mreflexive ? (ml_mspace_ ? ml));|apply (msymmetric ? (ml_mspace_ ? ml)); +|apply (mtineq ? (ml_mspace_ ? ml))] qed. -coercion cic:/matita/metric_lattice/ml_mset.con. +coercion cic:/matita/metric_lattice/ml_mspace.con. diff --git a/helm/software/matita/dama/metric_set.ma b/helm/software/matita/dama/metric_space.ma similarity index 57% rename from helm/software/matita/dama/metric_set.ma rename to helm/software/matita/dama/metric_space.ma index 74cb7d51c..35e0e0066 100644 --- a/helm/software/matita/dama/metric_set.ma +++ b/helm/software/matita/dama/metric_space.ma @@ -12,14 +12,14 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/metric_set/". +set "baseuri" "cic:/matita/metric_space/". include "ordered_groups.ma". -record metric_set (R : ogroup) : Type ≝ { +record metric_space (R : ogroup) : Type ≝ { ms_carr :> Type; metric: ms_carr → ms_carr → R; - mpositive: ∀a,b:ms_carr. metric a b ≤ 0; + mpositive: ∀a,b:ms_carr. 0 ≤ metric a b; mreflexive: ∀a. metric a a ≈ 0; msymmetric: ∀a,b. metric a b ≈ metric b a; mtineq: ∀a,b,c:ms_carr. metric a b ≤ metric a c + metric c b @@ -27,6 +27,24 @@ record metric_set (R : ogroup) : Type ≝ { }. notation < "\nbsp \delta a \nbsp b" non associative with precedence 80 for @{ 'delta2 $a $b}. -interpretation "metric" 'delta2 a b = (cic:/matita/metric_set/metric.con _ _ a b). +interpretation "metric" 'delta2 a b = (cic:/matita/metric_space/metric.con _ _ a b). notation "\delta" non associative with precedence 80 for @{ 'delta }. -interpretation "metric" 'delta = (cic:/matita/metric_set/metric.con _ _). +interpretation "metric" 'delta = (cic:/matita/metric_space/metric.con _ _). + +definition apart_metric:= + λR.λms:metric_space R.λa,b:ms.0 < δ a b. + +lemma apart_of_metric_space: ∀R:ogroup.metric_space R → apartness. +intros (R ms); apply (mk_apartness ? (apart_metric ? ms)); unfold apart_metric; unfold; +[1: intros 2 (x H); cases H (H1 H2); + lapply (ap_rewr ???? (eq_sym ??? (mreflexive ??x)) H2); + apply (ap_coreflexive R 0); assumption; +|2: intros (x y H); cases H; split; + [1: apply (le_rewr ???? (msymmetric ????)); assumption + |2: apply (ap_rewr ???? (msymmetric ????)); assumption] +|3: simplify; intros (x y z H); cases H (LExy Axy); + lapply (mtineq ?? x y z) as H1; whd in Axy; cases Axy (H2 H2); [cases (LExy H2)] + clear LExy; lapply (lt_le_transitive ???? H H1) as LT0; + apply (lt0plus_orlt ????? LT0); apply mpositive;] +qed. + diff --git a/helm/software/matita/dama/ordered_groups.ma b/helm/software/matita/dama/ordered_groups.ma index 0d13eda04..74188d8a0 100644 --- a/helm/software/matita/dama/ordered_groups.ma +++ b/helm/software/matita/dama/ordered_groups.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/ordered_groups/". -include "ordered_sets.ma". +include "ordered_set.ma". include "groups.ma". record pre_ogroup : Type ≝ { @@ -160,3 +160,11 @@ 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_set.ma b/helm/software/matita/dama/ordered_set.ma new file mode 100644 index 000000000..709126c14 --- /dev/null +++ b/helm/software/matita/dama/ordered_set.ma @@ -0,0 +1,45 @@ +(**************************************************************************) +(* ___ *) +(* ||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_set/". + +include "excedence.ma". + +record is_porder_relation (C:Type) (le:C→C→Prop) (eq:C→C→Prop) : Type ≝ { + por_reflexive: reflexive ? le; + por_transitive: transitive ? le; + por_antisimmetric: antisymmetric ? le eq +}. + +record pordered_set: Type ≝ { + pos_carr:> excedence; + pos_order_relation_properties:> is_porder_relation ? (le pos_carr) (eq pos_carr) +}. + +lemma pordered_set_of_excedence: excedence → pordered_set. +intros (E); apply (mk_pordered_set E); apply (mk_is_porder_relation); +[apply le_reflexive|apply le_transitive|apply le_antisymmetric] +qed. + +alias id "transitive" = "cic:/matita/higher_order_defs/relations/transitive.con". +alias id "cotransitive" = "cic:/matita/higher_order_defs/relations/cotransitive.con". +alias id "antisymmetric" = "cic:/matita/higher_order_defs/relations/antisymmetric.con". + +definition total_order_property : ∀E:excedence. Type ≝ + λE:excedence. ∀a,b:E. a ≰ b → b < a. + +record tordered_set : Type ≝ { + tos_poset:> pordered_set; + tos_totality: total_order_property tos_poset +}. diff --git a/helm/software/matita/dama/premetric_lattice.ma b/helm/software/matita/dama/premetric_lattice.ma new file mode 100644 index 000000000..61c4b826d --- /dev/null +++ b/helm/software/matita/dama/premetric_lattice.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/premetric_lattice/". + +include "metric_space.ma". + +record premetric_lattice_ (R : ogroup) : Type ≝ { + pml_carr:> metric_space R; + meet: pml_carr → pml_carr → pml_carr; + join: pml_carr → pml_carr → pml_carr +}. + +interpretation "valued lattice meet" 'and a b = + (cic:/matita/premetric_lattice/meet.con _ _ a b). + +interpretation "valued lattice join" 'or a b = + (cic:/matita/premetric_lattice/join.con _ _ a b). + +record premetric_lattice_props (R : ogroup) (ml : premetric_lattice_ R) : Prop ≝ { + prop1a: ∀a : ml.δ (a ∧ a) a ≈ 0; + prop1b: ∀a : ml.δ (a ∨ a) a ≈ 0; + prop2a: ∀a,b: ml. δ (a ∨ b) (b ∨ a) ≈ 0; + prop2b: ∀a,b: ml. δ (a ∧ b) (b ∧ a) ≈ 0; + prop3a: ∀a,b,c: ml. δ (a ∨ (b ∨ c)) ((a ∨ b) ∨ c) ≈ 0; + prop3b: ∀a,b,c: ml. δ (a ∧ (b ∧ c)) ((a ∧ b) ∧ c) ≈ 0; + prop4a: ∀a,b: ml. δ (a ∨ (a ∧ b)) a ≈ 0; + prop4b: ∀a,b: ml. δ (a ∧ (a ∨ b)) a ≈ 0; + prop5: ∀a,b,c: ml. δ (a ∨ b) (a ∨ c) + δ (a ∧ b) (a ∧ c) ≤ δ b c +}. + +record pmlattice (R : ogroup) : Type ≝ { + carr :> premetric_lattice_ R; + ispremetriclattice:> premetric_lattice_props R carr +}. + +include "lattice.ma". + +lemma lattice_of_pmlattice: ∀R: ogroup. pmlattice R → lattice. +intros (R pml); apply (mk_lattice (apart_of_metric_space ? pml)); +[apply (join ? pml)|apply (meet ? pml)] +intros (x y z); whd; intro H; whd in H; cases H (LE AP); +[apply (prop2a ? pml pml x y); |apply (prop2b ? pml pml x y); +|apply (prop3a ? pml pml x y z);|apply (prop3b ? pml pml x y z); +|apply (prop4a ? pml pml x y); |apply (prop4b ? pml pml x y);] +apply ap_symmetric; assumption; +qed. + +coercion cic:/matita/premetric_lattice/lattice_of_pmlattice.con. \ No newline at end of file diff --git a/helm/software/matita/dama/ordered_sets.ma b/helm/software/matita/dama/sequence.ma similarity index 81% rename from helm/software/matita/dama/ordered_sets.ma rename to helm/software/matita/dama/sequence.ma index 946d89573..8d3ba44df 100644 --- a/helm/software/matita/dama/ordered_sets.ma +++ b/helm/software/matita/dama/sequence.ma @@ -12,35 +12,9 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/ordered_sets/". +set "baseuri" "cic:/matita/sequence/". -include "excedence.ma". - -record is_porder_relation (C:Type) (le:C→C→Prop) (eq:C→C→Prop) : Type ≝ { - por_reflexive: reflexive ? le; - por_transitive: transitive ? le; - por_antisimmetric: antisymmetric ? le eq -}. - -record pordered_set: Type ≝ { - pos_carr:> excedence; - pos_order_relation_properties:> is_porder_relation ? (le pos_carr) (eq pos_carr) -}. - -lemma pordered_set_of_excedence: excedence → pordered_set. -intros (E); apply (mk_pordered_set E); apply (mk_is_porder_relation); -[apply le_reflexive|apply le_transitive|apply le_antisymmetric] -qed. - -alias id "transitive" = "cic:/matita/higher_order_defs/relations/transitive.con". -alias id "cotransitive" = "cic:/matita/higher_order_defs/relations/cotransitive.con". -alias id "antisymmetric" = "cic:/matita/higher_order_defs/relations/antisymmetric.con". - -theorem antisimmetric_to_cotransitive_to_transitive: - ∀C:Type.∀le:C→C→Prop. antisymmetric ? le → cotransitive ? le → transitive ? le. -intros (T f Af cT); unfold transitive; intros (x y z fxy fyz); -lapply (cT ? ? fxy z) as H; cases H; [assumption] cases (Af ? ? fyz H1); -qed. +include "ordered_set.ma". definition is_increasing ≝ λO:pordered_set.λa:nat→O.∀n:nat.a n ≤ a (S n). definition is_decreasing ≝ λO:pordered_set.λa:nat→O.∀n:nat.a (S n) ≤ a n. @@ -93,13 +67,13 @@ definition bounded_below_sequence_of_bounded_sequence ≝ λO:pordered_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. +coercion cic:/matita/sequence/bounded_below_sequence_of_bounded_sequence.con. definition bounded_above_sequence_of_bounded_sequence ≝ λO:pordered_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. +coercion cic:/matita/sequence/bounded_above_sequence_of_bounded_sequence.con. definition lower_bound ≝ λO:pordered_set.λb:bounded_below_sequence O. @@ -121,10 +95,6 @@ lemma upper_bound_is_upper_bound: intros; unfold upper_bound; apply ib_upper_bound_is_upper_bound. qed. -lemma Or_symmetric: symmetric ? Or. -unfold; intros (x y H); cases H; [right|left] assumption; -qed. - definition reverse_excedence: excedence → excedence. intros (E); apply (mk_excedence E); [apply (λx,y.exc_relation E y x)] cases E (T f cRf cTf); simplify; @@ -204,11 +174,3 @@ intros (O a l H); apply mk_is_sup; |2: intros (v H1); apply (inf_greatest_lower_bound (reverse_pordered_set O) a l H v); apply is_upper_bound_reverse_is_lower_bound; assumption;] qed. - -definition total_order_property : ∀E:excedence. Type ≝ - λE:excedence. ∀a,b:E. a ≰ b → b < a. - -record tordered_set : Type ≝ { - tos_poset:> pordered_set; - tos_totality: total_order_property tos_poset -}. -- 2.39.2