From 1509e99ac3aba0e725ac7ced7db20d5d23ea276a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 3 Jun 2008 15:56:51 +0000 Subject: [PATCH] some work on uniformity --- .../matita/contribs/dama/dama/depends | 4 +- .../contribs/dama/dama/ordered_uniform.ma | 62 +++++++++ .../matita/contribs/dama/dama/uniform.ma | 128 ++++++++++++++++++ 3 files changed, 193 insertions(+), 1 deletion(-) create mode 100644 helm/software/matita/contribs/dama/dama/ordered_uniform.ma create mode 100644 helm/software/matita/contribs/dama/dama/uniform.ma diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends index 5e4ec73cb..ea9ec7bff 100644 --- a/helm/software/matita/contribs/dama/dama/depends +++ b/helm/software/matita/contribs/dama/dama/depends @@ -4,8 +4,10 @@ ordered_set.ma cprop_connectives.ma cprop_connectives.ma logic/equality.ma bishop_set_rewrite.ma bishop_set.ma sequence.ma nat/nat.ma -supremum.ma bishop_set.ma cprop_connectives.ma nat_ordered_set.ma ordered_set.ma sequence.ma +uniform.ma supremum.ma +supremum.ma bishop_set.ma cprop_connectives.ma nat/plus.ma nat_ordered_set.ma ordered_set.ma sequence.ma nat_ordered_set.ma cprop_connectives.ma nat/compare.ma ordered_set.ma logic/equality.ma nat/compare.ma nat/nat.ma +nat/plus.ma diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma new file mode 100644 index 000000000..974405214 --- /dev/null +++ b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma @@ -0,0 +1,62 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "uniform.ma". + +record ordered_uniform_space_ : Type ≝ { + ous_os:> ordered_set; + ous_us_: uniform_space; + with_ : us_carr ous_us_ = bishop_set_of_ordered_set ous_os +}. + +lemma ous_unifspace: ordered_uniform_space_ → uniform_space. +intro X; apply (mk_uniform_space (bishop_set_of_ordered_set X)); +unfold bishop_set_OF_ordered_uniform_space_; +[1: rewrite < (with_ X); simplify; apply (us_unifbase (ous_us_ X)); +|2: cases (with_ X); simplify; apply (us_phi1 (ous_us_ X)); +|3: cases (with_ X); simplify; apply (us_phi2 (ous_us_ X)); +|4: cases (with_ X); simplify; apply (us_phi3 (ous_us_ X)); +|5: cases (with_ X); simplify; apply (us_phi4 (ous_us_ X))] +qed. + +coercion cic:/matita/dama/ordered_uniform/ous_unifspace.con. + +record ordered_uniform_space : Type ≝ { + ous_stuff :> ordered_uniform_space_; + ous_prop1: ∀U.us_unifbase ous_stuff U → convex ous_stuff U +}. + + +lemma segment_ordered_uniform_space: + ∀O:ordered_uniform_space.∀u,v:O.ordered_uniform_space. +intros (O u v); apply mk_ordered_uniform_space; +[1: apply mk_ordered_uniform_space_; + [1: apply (mk_ordered_set (sigma ? (λx.x ∈ [u,v]))); + [1: intros (x y); apply (fst x ≰ fst y); + |2: intros 1; cases x; simplify; apply os_coreflexive; + |3: intros 3; cases x; cases y; cases z; simplify; apply os_cotransitive] + |2: apply (mk_uniform_space (bishop_set_of_ordered_set (mk_ordered_set (sigma ? (λx.x ∈ [u,v])) ???))); + |3: apply refl_eq; +qed. + + +(* Lemma 3.2 *) +lemma foo: + ∀O:ordered_uniform_space.∀l,u:O. + ∀x:(segment_ordered_uniform_space O l u). + ∀a:sequence (segment_ordered_uniform_space O l u). + (* (λn.fst (a n)) uniform_converges (fst x) → *) + a uniform_converges x. + + \ No newline at end of file diff --git a/helm/software/matita/contribs/dama/dama/uniform.ma b/helm/software/matita/contribs/dama/dama/uniform.ma new file mode 100644 index 000000000..2b5ed2cb8 --- /dev/null +++ b/helm/software/matita/contribs/dama/dama/uniform.ma @@ -0,0 +1,128 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "supremum.ma". + +(* Definition 2.13 *) +definition square_bishop_set : bishop_set → bishop_set. +intro S; apply (mk_bishop_set (pair S S)); +[1: intros (x y); apply ((fst x # fst y) ∨ (snd x # snd y)); +|2: intro x; simplify; intro; cases H (X X); clear H; apply (bs_coreflexive ?? X); +|3: intros 2 (x y); simplify; intro H; cases H (X X); clear H; [left|right] apply (bs_symmetric ??? X); +|4: intros 3 (x y z); simplify; intro H; cases H (X X); clear H; + [1: cases (bs_cotransitive ??? (fst z) X); [left;left|right;left]assumption; + |2: cases (bs_cotransitive ??? (snd z) X); [left;right|right;right]assumption;]] +qed. + +definition subset ≝ λO:bishop_set.λP,Q:O→Prop.∀x:O.P x → Q x. + +notation "a \subseteq u" left associative with precedence 70 + for @{ 'subset $a $u }. +interpretation "Bishop subset" 'subset a b = + (cic:/matita/dama/uniform/subset.con _ a b). + +notation "{ ident x : t | p }" non associative with precedence 50 + for @{ 'explicitset (\lambda ${ident x} : $t . $p) }. +definition mk_set ≝ λT:bishop_set.λx:T→Prop.x. +interpretation "explicit set" 'explicitset t = + (cic:/matita/dama/uniform/mk_set.con _ t). + +notation < "s \sup 2" non associative with precedence 90 + for @{ 'square $s }. +notation > "s 'square'" non associative with precedence 90 + for @{ 'square $s }. +interpretation "bishop suqare set" 'square x = + (cic:/matita/dama/uniform/square_bishop_set.con x). + +alias symbol "exists" = "exists". +alias symbol "and" = "logical and". +definition compose_relations ≝ + λC:bishop_set.λU,V:C square → Prop. + λx:C square.∃y:C. U (prod ?? (fst x) y) ∧ V (prod ?? y (snd x)). + +notation "a \circ b" left associative with precedence 60 + for @{'compose $a $b}. +interpretation "relations composition" 'compose a b = + (cic:/matita/dama/uniform/compose_relations.con _ a b). + +definition invert_relation ≝ + λC:bishop_set.λU:C square → Prop. + λx:C square. U (prod ?? (snd x) (fst x)). + +notation < "s \sup (-1)" non associative with precedence 90 + for @{ 'invert $s }. +notation > "'inv' s" non associative with precedence 90 + for @{ 'invert $s }. +interpretation "relation invertion" 'invert a = + (cic:/matita/dama/uniform/invert_relation.con _ a). + +record uniform_space : Type ≝ { + us_carr:> bishop_set; + us_unifbase: (us_carr square → Prop) → CProp; + us_phi1: ∀U:us_carr square → Prop. us_unifbase U → + {x:us_carr square|fst x ≈ snd x} ⊆ U; + us_phi2: ∀U,V:us_carr square → Prop. us_unifbase U → us_unifbase V → + ∃W:us_carr square → Prop.us_unifbase W ∧ (W ⊆ {x:?|U x ∧ V x}); + us_phi3: ∀U:us_carr square → Prop. us_unifbase U → + ∃W:us_carr square → Prop.us_unifbase W ∧ (W ∘ W) ⊆ U; + us_phi4: ∀U:us_carr square → Prop. us_unifbase U → U = inv U (* I should use double inclusion ... *) +}. + +(* Definition 2.14 *) +alias symbol "leq" = "natural 'less or equal to'". +definition cauchy ≝ + λC:uniform_space.λa:sequence C.∀U.us_unifbase C U → + ∃n. ∀i,j. n ≤ i → n ≤ j → U (prod ?? (a i) (a j)). + +notation < "a \nbsp 'is_cauchy'" non associative with precedence 50 + for @{'cauchy $a}. +notation > "a 'is_cauchy'" non associative with precedence 50 + for @{'cauchy $a}. +interpretation "Cauchy sequence" 'cauchy s = + (cic:/matita/dama/uniform/cauchy.con _ s). + +(* Definition 2.15 *) +definition uniform_converge ≝ + λC:uniform_space.λa:sequence C.λu:C. + ∀U.us_unifbase C U → ∃n. ∀i. n ≤ i → U (prod ?? u (a i)). + +notation < "a \nbsp (\u \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 50 + for @{'uniform_converge $a $x}. +notation > "a 'uniform_converges' x" non associative with precedence 50 + for @{'uniform_converge $a $x}. +interpretation "Uniform convergence" 'uniform_converge s u = + (cic:/matita/dama/uniform/uniform_converge.con _ s u). + +(* Lemma 2.16 *) +lemma uniform_converge_is_cauchy : + ∀C:uniform_space.∀a:sequence C.∀x:C. + a uniform_converges x → a is_cauchy. +intros (C a x Ha); intros 2 (u Hu); +cases (us_phi3 ?? Hu) (v Hv0); cases Hv0 (Hv H); clear Hv0; +cases (Ha ? Hv) (n Hn); exists [apply n]; intros; +apply H; unfold; exists [apply x]; split [2: apply (Hn ? H2)] +rewrite > (us_phi4 ?? Hv); simplify; apply (Hn ? H1); +qed. + +(* Definition 2.17 *) +definition mk_big_set ≝ + λP:CProp.λF:P→CProp.F. +interpretation "explicit big set" 'explicitset t = + (cic:/matita/dama/uniform/mk_big_set.con _ t). + +definition restrict_uniformity ≝ + λC:uniform_space.λX:C→Prop. + {U:C square → Prop| (U ⊆ {x:C square|X (fst x) ∧ X(snd x)}) ∧ us_unifbase C U}. + + -- 2.39.2