From a2fe87da00fb5b9a39e9a1c7d796c61d4c7346af Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Nov 2007 16:44:11 +0000 Subject: [PATCH] ... --- .../matita/dama/constructive_connectives.ma | 9 +++- .../dama/constructive_pointfree/lebesgue.ma | 4 ++ helm/software/matita/dama/excedence.ma | 2 + helm/software/matita/dama/group.ma | 1 - helm/software/matita/dama/lattice.ma | 6 ++- helm/software/matita/dama/metric_space.ma | 1 + helm/software/matita/dama/ordered_group.ma | 16 +++++++ .../software/matita/dama/premetric_lattice.ma | 17 +++++-- helm/software/matita/dama/sequence.ma | 48 ++++++++++++++++++- 9 files changed, 95 insertions(+), 9 deletions(-) diff --git a/helm/software/matita/dama/constructive_connectives.ma b/helm/software/matita/dama/constructive_connectives.ma index 0a840d5a5..8518d7ede 100644 --- a/helm/software/matita/dama/constructive_connectives.ma +++ b/helm/software/matita/dama/constructive_connectives.ma @@ -27,17 +27,24 @@ inductive And (A,B:Type) : Type ≝ interpretation "constructive and" 'and x y = (cic:/matita/constructive_connectives/And.ind#xpointer(1/1) x y). +inductive exT (A:Type) (P:A→Type) : Type ≝ + ex_introT: ∀w:A. P w → exT A P. + inductive ex (A:Type) (P:A→Prop) : Type ≝ ex_intro: ∀w:A. P w → ex A P. +(* notation < "hvbox(Σ ident i opt (: ty) break . p)" right associative with precedence 20 for @{ 'sigma ${default @{\lambda ${ident i} : $ty. $p)} @{\lambda ${ident i} . $p}}}. +*) -interpretation "constructive exists" 'sigma \eta.x = +interpretation "constructive exists" 'exists \eta.x = (cic:/matita/constructive_connectives/ex.ind#xpointer(1/1) _ x). +interpretation "constructive exists (Type)" 'exists \eta.x = + (cic:/matita/constructive_connectives/exT.ind#xpointer(1/1) _ x). alias id "False" = "cic:/matita/logic/connectives/False.ind#xpointer(1/1)". definition Not ≝ λx:Type.x → False. diff --git a/helm/software/matita/dama/constructive_pointfree/lebesgue.ma b/helm/software/matita/dama/constructive_pointfree/lebesgue.ma index 824202a78..766412819 100644 --- a/helm/software/matita/dama/constructive_pointfree/lebesgue.ma +++ b/helm/software/matita/dama/constructive_pointfree/lebesgue.ma @@ -16,9 +16,13 @@ set "baseuri" "cic:/matita/lebesgue/". include "metric_lattice.ma". include "sequence.ma". +include "constructive_connectives.ma". (* Section 3.2 *) +(* 3.21 *) + + (* 3.17 *) diff --git a/helm/software/matita/dama/excedence.ma b/helm/software/matita/dama/excedence.ma index 83dcbf702..34e253b89 100644 --- a/helm/software/matita/dama/excedence.ma +++ b/helm/software/matita/dama/excedence.ma @@ -55,6 +55,8 @@ notation "a break # b" non associative with precedence 50 for @{ 'apart $a $b}. interpretation "axiomatic apartness" 'apart x y = (cic:/matita/excedence/ap_apart.con _ x y). +definition strong_ext ≝ λA:apartness.λop:A→A.∀x,y. op x # op y → x # y. + definition apart ≝ λE:excedence.λa,b:E. a ≰ b ∨ b ≰ a. definition apart_of_excedence: excedence → apartness. diff --git a/helm/software/matita/dama/group.ma b/helm/software/matita/dama/group.ma index 0d682a268..b0c7c2e9b 100644 --- a/helm/software/matita/dama/group.ma +++ b/helm/software/matita/dama/group.ma @@ -20,7 +20,6 @@ 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 ≝ diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/dama/lattice.ma index 398b1af89..20d746a0a 100644 --- a/helm/software/matita/dama/lattice.ma +++ b/helm/software/matita/dama/lattice.ma @@ -20,12 +20,16 @@ record lattice : Type ≝ { l_carr:> apartness; join: l_carr → l_carr → l_carr; meet: l_carr → l_carr → l_carr; + join_refl: ∀x.join x x ≈ x; + meet_refl: ∀x.meet x x ≈ x; 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 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 + absorbmj: ∀f,g:l_carr. meet f (join f g) ≈ f; + strong_extj: ∀x.strong_ext ? (join x); + strong_extm: ∀x.strong_ext ? (meet x) }. interpretation "Lattice meet" 'and a b = diff --git a/helm/software/matita/dama/metric_space.ma b/helm/software/matita/dama/metric_space.ma index d529af83c..6774662a2 100644 --- a/helm/software/matita/dama/metric_space.ma +++ b/helm/software/matita/dama/metric_space.ma @@ -48,3 +48,4 @@ intros (R ms); apply (mk_apartness ? (apart_metric ? ms)); unfold apart_metric; apply (lt0plus_orlt ????? LT0); apply mpositive;] qed. +coercion cic:/matita/metric_space/apart_of_metric_space.con. diff --git a/helm/software/matita/dama/ordered_group.ma b/helm/software/matita/dama/ordered_group.ma index 4f7551ccf..9b37286fc 100644 --- a/helm/software/matita/dama/ordered_group.ma +++ b/helm/software/matita/dama/ordered_group.ma @@ -168,3 +168,19 @@ intros (G x y LEx LEy LT); cases LT (H1 H2); cases (ap_cotransitive ??? y H2); apply (plus_cancr_ap ??? y); apply (ap_rewl ???? (zero_neutral ??)); assumption; qed. + +lemma le0plus_le: + ∀G:ogroup.∀a,b,c:G. 0 ≤ b → a + b ≤ c → a ≤ c. +intros (G a b c L H); apply (le_transitive ????? H); +apply (plus_cancl_le ??? (-a)); +apply (le_rewl ??? 0 (opp_inverse ??)); +apply (le_rewr ??? (-a + a + b) (plus_assoc ????)); +apply (le_rewr ??? (0 + b) (opp_inverse ??)); +apply (le_rewr ??? b (zero_neutral ??)); +assumption; +qed. + + + + + \ No newline at end of file diff --git a/helm/software/matita/dama/premetric_lattice.ma b/helm/software/matita/dama/premetric_lattice.ma index 61c4b826d..42d00fd26 100644 --- a/helm/software/matita/dama/premetric_lattice.ma +++ b/helm/software/matita/dama/premetric_lattice.ma @@ -49,12 +49,21 @@ 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 (join ? pml)|apply (meet ? pml) +|3,4,5,6,7,8,9,10: intros (x y z); whd; intro H; whd in H; cases H (LE AP);] +[apply (prop1b ? pml pml x); |apply (prop1a ? pml pml x); +|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; +try (apply ap_symmetric; assumption); intros 4 (x y z H); change with (0 < (δ y z)); +[ change in H with (0 < δ (x ∨ y) (x ∨ z)); + apply (lt_le_transitive ???? H); + apply (le0plus_le ???? (mpositive ? pml ??) (prop5 ? pml pml x y z)); +| change in H with (0 < δ (x ∧ y) (x ∧ z)); + apply (lt_le_transitive ???? H); + apply (le0plus_le ???? (mpositive ? pml (x∨y) (x∨z))); + apply (le_rewl ??? ? (plus_comm ???)); + apply (prop5 ? pml pml);] qed. coercion cic:/matita/premetric_lattice/lattice_of_pmlattice.con. \ No newline at end of file diff --git a/helm/software/matita/dama/sequence.ma b/helm/software/matita/dama/sequence.ma index 2d304d2af..9edc871e5 100644 --- a/helm/software/matita/dama/sequence.ma +++ b/helm/software/matita/dama/sequence.ma @@ -24,8 +24,50 @@ qed. coercion cic:/matita/sequence/fun_of_sequence.con 1. -definition is_increasing ≝ λO:pordered_set.λa:sequence O.∀n:nat.a n ≤ a (S n). -definition is_decreasing ≝ λO:pordered_set.λa:sequence O.∀n:nat.a (S n) ≤ a n. +definition upper_bound ≝ + λO:pordered_set.λa:sequence O.λu:O.∀n:nat.a n ≤ u. + +definition lower_bound ≝ + λO:pordered_set.λa:sequence O.λu:O.∀n:nat.u ≤ a n. + +definition strong_sup ≝ + λO:pordered_set.λs:sequence O.λx. + upper_bound ? s x ∧ (∀y:O.x ≰ y → ∃n.s n ≰ y). + +definition strong_inf ≝ + λO:pordered_set.λs:sequence O.λx. + lower_bound ? s x ∧ (∀y:O.y ≰ x → ∃n.y ≰ s n). + +definition weak_sup ≝ + λO:pordered_set.λs:sequence O.λx. + upper_bound ? s x ∧ (∀y:O.upper_bound ? s y → x ≤ y). + +definition weak_inf ≝ + λO:pordered_set.λs:sequence O.λx. + lower_bound ? s x ∧ (∀y:O.lower_bound ? s y → y ≤ x). + +lemma strong_sup_is_weak: + ∀O:pordered_set.∀s:sequence O.∀x:O.strong_sup ? s x → weak_sup ? s x. +intros (O s x Ssup); elim Ssup (Ubx M); clear Ssup; split; [assumption] +intros 3 (y Uby E); cases (M ? E) (n En); unfold in Uby; cases (Uby ? En); +qed. + +lemma strong_inf_is_weak: + ∀O:pordered_set.∀s:sequence O.∀x:O.strong_inf ? s x → weak_inf ? s x. +intros (O s x Ssup); elim Ssup (Ubx M); clear Ssup; split; [assumption] +intros 3 (y Uby E); cases (M ? E) (n En); unfold in Uby; cases (Uby ? En); +qed. + + + +definition increasing ≝ + λO:pordered_set.λa:sequence O.∀n:nat.a n ≤ a (S n). + +definition decreasing ≝ + λO:pordered_set.λa:sequence O.∀n:nat.a (S n) ≤ a n. + + +(* definition is_upper_bound ≝ λO:pordered_set.λa:sequence O.λu:O.∀n:nat.a n ≤ u. definition is_lower_bound ≝ λO:pordered_set.λa:sequence O.λu:O.∀n:nat.u ≤ a n. @@ -182,3 +224,5 @@ 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. + +*) \ No newline at end of file -- 2.39.2