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);
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).
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
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;
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;
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.
+
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.
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/lattices/".
+set "baseuri" "cic:/matita/lattice/".
include "excedence.ma".
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 *)
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.
qed.
coercion cic:/matita/lattices/ordered_set_of_lattice.con.
-*)
\ No newline at end of file
+*)
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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/metric_set/".
-
-include "ordered_groups.ma".
-
-record metric_set (R : ogroup) : Type ≝ {
- ms_carr :> Type;
- metric: ms_carr → ms_carr → R;
- mpositive: ∀a,b:ms_carr. metric a b ≤ 0;
- 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
- (* manca qualcosa per essere una metrica e non una semimetrica *)
-}.
-
-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).
-notation "\delta" non associative with precedence 80 for @{ 'delta }.
-interpretation "metric" 'delta = (cic:/matita/metric_set/metric.con _ _).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/metric_space/".
+
+include "ordered_groups.ma".
+
+record metric_space (R : ogroup) : Type ≝ {
+ ms_carr :> Type;
+ metric: ms_carr → ms_carr → R;
+ 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
+ (* manca qualcosa per essere una metrica e non una semimetrica *)
+}.
+
+notation < "\nbsp \delta a \nbsp b" non associative with precedence 80 for @{ 'delta2 $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_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.
+
set "baseuri" "cic:/matita/ordered_groups/".
-include "ordered_sets.ma".
+include "ordered_set.ma".
include "groups.ma".
record pre_ogroup : Type ≝ {
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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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
+}.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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_sets/".
-
-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.
-
-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.
-
-definition is_upper_bound ≝ λO:pordered_set.λa:nat→O.λu:O.∀n:nat.a n ≤ u.
-definition is_lower_bound ≝ λO:pordered_set.λa:nat→O.λu:O.∀n:nat.u ≤ a n.
-
-record is_sup (O:pordered_set) (a:nat→O) (u:O) : Prop ≝
- { sup_upper_bound: is_upper_bound O a u;
- sup_least_upper_bound: ∀v:O. is_upper_bound O a v → u≤v
- }.
-
-record is_inf (O:pordered_set) (a:nat→O) (u:O) : Prop ≝
- { inf_lower_bound: is_lower_bound O a u;
- inf_greatest_lower_bound: ∀v:O. is_lower_bound O a v → v≤u
- }.
-
-record is_bounded_below (O:pordered_set) (a:nat→O) : Type ≝
- { ib_lower_bound: O;
- ib_lower_bound_is_lower_bound: is_lower_bound ? a ib_lower_bound
- }.
-
-record is_bounded_above (O:pordered_set) (a:nat→O) : Type ≝
- { ib_upper_bound: O;
- ib_upper_bound_is_upper_bound: is_upper_bound ? a ib_upper_bound
- }.
-
-record is_bounded (O:pordered_set) (a:nat→O) : Type ≝
- { ib_bounded_below:> is_bounded_below ? a;
- ib_bounded_above:> is_bounded_above ? a
- }.
-
-record bounded_below_sequence (O:pordered_set) : Type ≝
- { bbs_seq:1> nat→O;
- bbs_is_bounded_below:> is_bounded_below ? bbs_seq
- }.
-
-record bounded_above_sequence (O:pordered_set) : Type ≝
- { bas_seq:1> nat→O;
- bas_is_bounded_above:> is_bounded_above ? bas_seq
- }.
-
-record bounded_sequence (O:pordered_set) : Type ≝
- { bs_seq:1> nat → O;
- bs_is_bounded_below: is_bounded_below ? bs_seq;
- bs_is_bounded_above: is_bounded_above ? bs_seq
- }.
-
-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.
-
-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.
-
-definition lower_bound ≝
- λO:pordered_set.λb:bounded_below_sequence O.
- ib_lower_bound ? b (bbs_is_bounded_below ? b).
-
-lemma lower_bound_is_lower_bound:
- ∀O:pordered_set.∀b:bounded_below_sequence O.
- is_lower_bound ? b (lower_bound ? b).
-intros; unfold lower_bound; apply ib_lower_bound_is_lower_bound.
-qed.
-
-definition upper_bound ≝
- λO:pordered_set.λb:bounded_above_sequence O.
- ib_upper_bound ? b (bas_is_bounded_above ? b).
-
-lemma upper_bound_is_upper_bound:
- ∀O:pordered_set.∀b:bounded_above_sequence O.
- is_upper_bound ? b (upper_bound ? b).
-intros; unfold upper_bound; apply ib_upper_bound_is_upper_bound.
-qed.
-
-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;
-[1: unfold Not; intros (x H); apply (cRf x); assumption
-|2: intros (x y z); apply Or_symmetric; apply cTf; assumption;]
-qed.
-
-definition reverse_pordered_set: pordered_set → pordered_set.
-intros (p); apply (mk_pordered_set (reverse_excedence p));
-generalize in match (reverse_excedence p); intros (E);
-apply mk_is_porder_relation;
-[apply le_reflexive|apply le_transitive|apply le_antisymmetric]
-qed.
-
-lemma is_lower_bound_reverse_is_upper_bound:
- ∀O:pordered_set.∀a:nat→O.∀l:O.
- is_lower_bound O a l → is_upper_bound (reverse_pordered_set O) a l.
-intros (O a l H); unfold; intros (n); unfold reverse_pordered_set;
-unfold reverse_excedence; simplify; fold unfold le (le ? l (a n)); apply H;
-qed.
-
-lemma is_upper_bound_reverse_is_lower_bound:
- ∀O:pordered_set.∀a:nat→O.∀l:O.
- is_upper_bound O a l → is_lower_bound (reverse_pordered_set O) a l.
-intros (O a l H); unfold; intros (n); unfold reverse_pordered_set;
-unfold reverse_excedence; simplify; fold unfold le (le ? (a n) l); apply H;
-qed.
-
-lemma reverse_is_lower_bound_is_upper_bound:
- ∀O:pordered_set.∀a:nat→O.∀l:O.
- is_lower_bound (reverse_pordered_set O) a l → is_upper_bound O a l.
-intros (O a l H); unfold; intros (n); unfold reverse_pordered_set in H;
-unfold reverse_excedence in H; simplify in H; apply H;
-qed.
-
-lemma reverse_is_upper_bound_is_lower_bound:
- ∀O:pordered_set.∀a:nat→O.∀l:O.
- is_upper_bound (reverse_pordered_set O) a l → is_lower_bound O a l.
-intros (O a l H); unfold; intros (n); unfold reverse_pordered_set in H;
-unfold reverse_excedence in H; simplify in H; apply H;
-qed.
-
-lemma is_inf_to_reverse_is_sup:
- ∀O:pordered_set.∀a:bounded_below_sequence O.∀l:O.
- is_inf O a l → is_sup (reverse_pordered_set O) a l.
-intros (O a l H); apply (mk_is_sup (reverse_pordered_set O));
-[1: apply is_lower_bound_reverse_is_upper_bound; apply inf_lower_bound; assumption
-|2: unfold reverse_pordered_set; simplify; unfold reverse_excedence; simplify;
- intros (m H1); apply (inf_greatest_lower_bound ? ? ? H); apply H1;]
-qed.
-
-lemma is_sup_to_reverse_is_inf:
- ∀O:pordered_set.∀a:bounded_above_sequence O.∀l:O.
- is_sup O a l → is_inf (reverse_pordered_set O) a l.
-intros (O a l H); apply (mk_is_inf (reverse_pordered_set O));
-[1: apply is_upper_bound_reverse_is_lower_bound; apply sup_upper_bound; assumption
-|2: unfold reverse_pordered_set; simplify; unfold reverse_excedence; simplify;
- intros (m H1); apply (sup_least_upper_bound ? ? ? H); apply H1;]
-qed.
-
-lemma reverse_is_sup_to_is_inf:
- ∀O:pordered_set.∀a:bounded_above_sequence O.∀l:O.
- is_sup (reverse_pordered_set O) a l → is_inf O a l.
-intros (O a l H); apply mk_is_inf;
-[1: apply reverse_is_upper_bound_is_lower_bound;
- apply (sup_upper_bound (reverse_pordered_set O)); assumption
-|2: intros (v H1); apply (sup_least_upper_bound (reverse_pordered_set O) a l H v);
- apply is_lower_bound_reverse_is_upper_bound; assumption;]
-qed.
-
-lemma reverse_is_inf_to_is_sup:
- ∀O:pordered_set.∀a:bounded_above_sequence O.∀l:O.
- is_inf (reverse_pordered_set O) a l → is_sup O a l.
-intros (O a l H); apply mk_is_sup;
-[1: apply reverse_is_lower_bound_is_upper_bound;
- apply (inf_lower_bound (reverse_pordered_set O)); assumption
-|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
-}.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/sequence/".
+
+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.
+
+definition is_upper_bound ≝ λO:pordered_set.λa:nat→O.λu:O.∀n:nat.a n ≤ u.
+definition is_lower_bound ≝ λO:pordered_set.λa:nat→O.λu:O.∀n:nat.u ≤ a n.
+
+record is_sup (O:pordered_set) (a:nat→O) (u:O) : Prop ≝
+ { sup_upper_bound: is_upper_bound O a u;
+ sup_least_upper_bound: ∀v:O. is_upper_bound O a v → u≤v
+ }.
+
+record is_inf (O:pordered_set) (a:nat→O) (u:O) : Prop ≝
+ { inf_lower_bound: is_lower_bound O a u;
+ inf_greatest_lower_bound: ∀v:O. is_lower_bound O a v → v≤u
+ }.
+
+record is_bounded_below (O:pordered_set) (a:nat→O) : Type ≝
+ { ib_lower_bound: O;
+ ib_lower_bound_is_lower_bound: is_lower_bound ? a ib_lower_bound
+ }.
+
+record is_bounded_above (O:pordered_set) (a:nat→O) : Type ≝
+ { ib_upper_bound: O;
+ ib_upper_bound_is_upper_bound: is_upper_bound ? a ib_upper_bound
+ }.
+
+record is_bounded (O:pordered_set) (a:nat→O) : Type ≝
+ { ib_bounded_below:> is_bounded_below ? a;
+ ib_bounded_above:> is_bounded_above ? a
+ }.
+
+record bounded_below_sequence (O:pordered_set) : Type ≝
+ { bbs_seq:1> nat→O;
+ bbs_is_bounded_below:> is_bounded_below ? bbs_seq
+ }.
+
+record bounded_above_sequence (O:pordered_set) : Type ≝
+ { bas_seq:1> nat→O;
+ bas_is_bounded_above:> is_bounded_above ? bas_seq
+ }.
+
+record bounded_sequence (O:pordered_set) : Type ≝
+ { bs_seq:1> nat → O;
+ bs_is_bounded_below: is_bounded_below ? bs_seq;
+ bs_is_bounded_above: is_bounded_above ? bs_seq
+ }.
+
+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/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/sequence/bounded_above_sequence_of_bounded_sequence.con.
+
+definition lower_bound ≝
+ λO:pordered_set.λb:bounded_below_sequence O.
+ ib_lower_bound ? b (bbs_is_bounded_below ? b).
+
+lemma lower_bound_is_lower_bound:
+ ∀O:pordered_set.∀b:bounded_below_sequence O.
+ is_lower_bound ? b (lower_bound ? b).
+intros; unfold lower_bound; apply ib_lower_bound_is_lower_bound.
+qed.
+
+definition upper_bound ≝
+ λO:pordered_set.λb:bounded_above_sequence O.
+ ib_upper_bound ? b (bas_is_bounded_above ? b).
+
+lemma upper_bound_is_upper_bound:
+ ∀O:pordered_set.∀b:bounded_above_sequence O.
+ is_upper_bound ? b (upper_bound ? b).
+intros; unfold upper_bound; apply ib_upper_bound_is_upper_bound.
+qed.
+
+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;
+[1: unfold Not; intros (x H); apply (cRf x); assumption
+|2: intros (x y z); apply Or_symmetric; apply cTf; assumption;]
+qed.
+
+definition reverse_pordered_set: pordered_set → pordered_set.
+intros (p); apply (mk_pordered_set (reverse_excedence p));
+generalize in match (reverse_excedence p); intros (E);
+apply mk_is_porder_relation;
+[apply le_reflexive|apply le_transitive|apply le_antisymmetric]
+qed.
+
+lemma is_lower_bound_reverse_is_upper_bound:
+ ∀O:pordered_set.∀a:nat→O.∀l:O.
+ is_lower_bound O a l → is_upper_bound (reverse_pordered_set O) a l.
+intros (O a l H); unfold; intros (n); unfold reverse_pordered_set;
+unfold reverse_excedence; simplify; fold unfold le (le ? l (a n)); apply H;
+qed.
+
+lemma is_upper_bound_reverse_is_lower_bound:
+ ∀O:pordered_set.∀a:nat→O.∀l:O.
+ is_upper_bound O a l → is_lower_bound (reverse_pordered_set O) a l.
+intros (O a l H); unfold; intros (n); unfold reverse_pordered_set;
+unfold reverse_excedence; simplify; fold unfold le (le ? (a n) l); apply H;
+qed.
+
+lemma reverse_is_lower_bound_is_upper_bound:
+ ∀O:pordered_set.∀a:nat→O.∀l:O.
+ is_lower_bound (reverse_pordered_set O) a l → is_upper_bound O a l.
+intros (O a l H); unfold; intros (n); unfold reverse_pordered_set in H;
+unfold reverse_excedence in H; simplify in H; apply H;
+qed.
+
+lemma reverse_is_upper_bound_is_lower_bound:
+ ∀O:pordered_set.∀a:nat→O.∀l:O.
+ is_upper_bound (reverse_pordered_set O) a l → is_lower_bound O a l.
+intros (O a l H); unfold; intros (n); unfold reverse_pordered_set in H;
+unfold reverse_excedence in H; simplify in H; apply H;
+qed.
+
+lemma is_inf_to_reverse_is_sup:
+ ∀O:pordered_set.∀a:bounded_below_sequence O.∀l:O.
+ is_inf O a l → is_sup (reverse_pordered_set O) a l.
+intros (O a l H); apply (mk_is_sup (reverse_pordered_set O));
+[1: apply is_lower_bound_reverse_is_upper_bound; apply inf_lower_bound; assumption
+|2: unfold reverse_pordered_set; simplify; unfold reverse_excedence; simplify;
+ intros (m H1); apply (inf_greatest_lower_bound ? ? ? H); apply H1;]
+qed.
+
+lemma is_sup_to_reverse_is_inf:
+ ∀O:pordered_set.∀a:bounded_above_sequence O.∀l:O.
+ is_sup O a l → is_inf (reverse_pordered_set O) a l.
+intros (O a l H); apply (mk_is_inf (reverse_pordered_set O));
+[1: apply is_upper_bound_reverse_is_lower_bound; apply sup_upper_bound; assumption
+|2: unfold reverse_pordered_set; simplify; unfold reverse_excedence; simplify;
+ intros (m H1); apply (sup_least_upper_bound ? ? ? H); apply H1;]
+qed.
+
+lemma reverse_is_sup_to_is_inf:
+ ∀O:pordered_set.∀a:bounded_above_sequence O.∀l:O.
+ is_sup (reverse_pordered_set O) a l → is_inf O a l.
+intros (O a l H); apply mk_is_inf;
+[1: apply reverse_is_upper_bound_is_lower_bound;
+ apply (sup_upper_bound (reverse_pordered_set O)); assumption
+|2: intros (v H1); apply (sup_least_upper_bound (reverse_pordered_set O) a l H v);
+ apply is_lower_bound_reverse_is_upper_bound; assumption;]
+qed.
+
+lemma reverse_is_inf_to_is_sup:
+ ∀O:pordered_set.∀a:bounded_above_sequence O.∀l:O.
+ is_inf (reverse_pordered_set O) a l → is_sup O a l.
+intros (O a l H); apply mk_is_sup;
+[1: apply reverse_is_lower_bound_is_upper_bound;
+ apply (inf_lower_bound (reverse_pordered_set O)); assumption
+|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.
projects / helm.git / commitdiff