From 695cc9c1ead293e380709ebcd98818e019b8e49e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 3 Jun 2008 12:09:21 +0000 Subject: [PATCH] end of section 2.2 --- .../matita/contribs/dama/dama/depends | 9 +- .../matita/contribs/dama/dama/supremum.ma | 161 +++++++++++++++++- 2 files changed, 162 insertions(+), 8 deletions(-) diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends index 5a19b2a54..5e4ec73cb 100644 --- a/helm/software/matita/contribs/dama/dama/depends +++ b/helm/software/matita/contribs/dama/dama/depends @@ -1,12 +1,11 @@ -.unnamed.ma bishop_set.ma ordered_set.ma +extra.ma bishop_set_rewrite.ma +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 -bishop_set_rewrite.ma bishop_set.ma -cprop_connectives.ma logic/equality.ma nat_ordered_set.ma cprop_connectives.ma nat/compare.ma ordered_set.ma -ordered_set.ma cprop_connectives.ma -extra.ma bishop_set_rewrite.ma logic/equality.ma nat/compare.ma nat/nat.ma diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma index 65d43ac18..0c6d545b8 100644 --- a/helm/software/matita/contribs/dama/dama/supremum.ma +++ b/helm/software/matita/contribs/dama/dama/supremum.ma @@ -17,32 +17,54 @@ include "ordered_set.ma". (* Definition 2.4 *) definition upper_bound ≝ λO:ordered_set.λa:sequence O.λu:O.∀n:nat.a n ≤ u. +definition lower_bound ≝ λO:ordered_set.λa:sequence O.λu:O.∀n:nat.u ≤ a n. definition supremum ≝ λO:ordered_set.λs:sequence O.λx.upper_bound ? s x ∧ (∀y:O.x ≰ y → ∃n.s n ≰ y). +definition infimum ≝ + λO:ordered_set.λs:sequence O.λx.lower_bound ? s x ∧ (∀y:O.y ≰ x → ∃n.y ≰ s n). definition increasing ≝ λO:ordered_set.λa:sequence O.∀n:nat.a n ≤ a (S n). +definition decreasing ≝ λO:ordered_set.λa:sequence O.∀n:nat.a (S n) ≤ a n. notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 50 for @{'upper_bound $s $x}. -notation < "s \nbsp 'is_increasing'" non associative with precedence 50 +notation < "x \nbsp 'is_lower_bound' \nbsp s" non associative with precedence 50 + for @{'lower_bound $s $x}. +notation < "s \nbsp 'is_increasing'" non associative with precedence 50 for @{'increasing $s}. -notation < "x \nbsp 'is_supremum' \nbsp s" non associative with precedence 50 +notation < "s \nbsp 'is_decreasing'" non associative with precedence 50 + for @{'decreasing $s}. +notation < "x \nbsp 'is_supremum' \nbsp s" non associative with precedence 50 for @{'supremum $s $x}. +notation < "x \nbsp 'is_infimum' \nbsp s" non associative with precedence 50 + for @{'infimum $s $x}. notation > "x 'is_upper_bound' s" non associative with precedence 50 for @{'upper_bound $s $x}. +notation > "x 'is_lower_bound' s" non associative with precedence 50 + for @{'lower_bound $s $x}. notation > "s 'is_increasing'" non associative with precedence 50 for @{'increasing $s}. +notation > "s 'is_decreasing'" non associative with precedence 50 + for @{'decreasing $s}. notation > "x 'is_supremum' s" non associative with precedence 50 for @{'supremum $s $x}. +notation > "x 'is_infimum' s" non associative with precedence 50 + for @{'infimum $s $x}. interpretation "Ordered set upper bound" 'upper_bound s x = (cic:/matita/dama/supremum/upper_bound.con _ s x). +interpretation "Ordered set lower bound" 'lower_bound s x = + (cic:/matita/dama/supremum/lower_bound.con _ s x). interpretation "Ordered set increasing" 'increasing s = (cic:/matita/dama/supremum/increasing.con _ s). +interpretation "Ordered set decreasing" 'decreasing s = + (cic:/matita/dama/supremum/decreasing.con _ s). interpretation "Ordered set strong sup" 'supremum s x = (cic:/matita/dama/supremum/supremum.con _ s x). +interpretation "Ordered set strong inf" 'infimum s x = + (cic:/matita/dama/supremum/infimum.con _ s x). include "bishop_set.ma". @@ -66,20 +88,35 @@ qed. (* Lemma 2.6 *) definition strictly_increasing ≝ λC:ordered_set.λa:sequence C.∀n:nat.a (S n) ≰ a n. +definition strictly_decreasing ≝ + λC:ordered_set.λa:sequence C.∀n:nat.a n ≰ a (S n). + notation < "s \nbsp 'is_strictly_increasing'" non associative with precedence 50 for @{'strictly_increasing $s}. notation > "s 'is_strictly_increasing'" non associative with precedence 50 for @{'strictly_increasing $s}. -interpretation "Ordered set increasing" 'strictly_increasing s = +interpretation "Ordered set strict increasing" 'strictly_increasing s = (cic:/matita/dama/supremum/strictly_increasing.con _ s). +notation < "s \nbsp 'is_strictly_decreasing'" non associative with precedence 50 + for @{'strictly_decreasing $s}. +notation > "s 'is_strictly_decreasing'" non associative with precedence 50 + for @{'strictly_decreasing $s}. +interpretation "Ordered set strict decreasing" 'strictly_decreasing s = + (cic:/matita/dama/supremum/strictly_decreasing.con _ s). notation "a \uparrow u" non associative with precedence 50 for @{'sup_inc $a $u}. interpretation "Ordered set supremum of increasing" 'sup_inc s u = (cic:/matita/dama/cprop_connectives/And.ind#xpointer(1/1) (cic:/matita/dama/supremum/increasing.con _ s) (cic:/matita/dama/supremum/supremum.con _ s u)). +notation "a \downarrow u" non associative with precedence 50 for @{'inf_dec $a $u}. +interpretation "Ordered set supremum of increasing" 'inf_dec s u = + (cic:/matita/dama/cprop_connectives/And.ind#xpointer(1/1) + (cic:/matita/dama/supremum/decreasing.con _ s) + (cic:/matita/dama/supremum/infimum.con _ s u)). +include "nat/plus.ma". include "nat_ordered_set.ma". alias symbol "nleq" = "Ordered set excess". @@ -124,3 +161,121 @@ intros (C m Hm a u Ha); cases Ha (Ia Su); cases Su (Uu Hu); repeat split; cases (trans_increasing C ? Ia ?? H1); assumption;] qed. +(* Definition 2.7 *) +alias symbol "exists" = "CProp exists". +alias symbol "and" = "constructive and". +definition order_converge ≝ + λO:ordered_set.λa:sequence O.λx:O. + ∃l:sequence O.∃u:sequence O. + l is_increasing ∧ u is_decreasing ∧ l ↑ x ∧ u ↓ x ∧ + ∀i:nat. (l i) is_infimum (λw.a (w+i)) ∧ (u i) is_supremum (λw.a (w+i)). + +notation < "a \nbsp (\circ \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 50 + for @{'order_converge $a $x}. +notation > "a 'order_converges' x" non associative with precedence 50 + for @{'order_converge $a $x}. +interpretation "Order convergence" 'order_converge s u = + (cic:/matita/dama/supremum/order_converge.con _ s u). + +(* Definition 2.8 *) + +definition segment ≝ λO:ordered_set.λa,b:O.λx:O. + (cic:/matita/logic/connectives/And.ind#xpointer(1/1) (x ≤ b) (a ≤ x)). + +notation "[a,b]" non associative with precedence 50 + for @{'segment $a $b}. +interpretation "Ordered set sergment" 'segment a b = + (cic:/matita/dama/supremum/segment.con _ a b). + +notation "x \in [a,b]" non associative with precedence 50 + for @{'segment2 $a $b $x}. +interpretation "Ordered set sergment in" 'segment2 a b x= + (cic:/matita/dama/supremum/segment.con _ a b x). + +coinductive sigma (A:Type) (P:A→Prop) : Type ≝ sig_in : ∀x.P x → sigma A P. + +definition pi1 : ∀A.∀P.sigma A P → A ≝ λA,P,s.match s with [sig_in x _ ⇒ x]. + +notation < "\pi \sub 1 x" non associative with precedence 50 for @{'pi1 $x}. +notation < "\pi \sub 2 x" non associative with precedence 50 for @{'pi2 $x}. +notation > "'fst' x" non associative with precedence 50 for @{'pi1 $x}. +notation > "'snd' x" non associative with precedence 50 for @{'pi2 $x}. +interpretation "sigma pi1" 'pi1 x = + (cic:/matita/dama/supremum/pi1.con _ _ x). + +interpretation "Type exists" 'exists \eta.x = + (cic:/matita/dama/supremum/sigma.ind#xpointer(1/1) _ x). + +lemma segment_ordered_set: + ∀O:ordered_set.∀u,v:O.ordered_set. +intros (O u v); apply (mk_ordered_set (∃x.x ∈ [u,v])); +[1: intros (x y); apply (fst x ≰ fst y); +|2: intro x; cases x; simplify; apply os_coreflexive; +|3: intros 3 (x y z); cases x; cases y ; cases z; simplify; apply os_cotransitive] +qed. + +notation < "{\x|\x \in [a,b]}" non associative with precedence 90 + for @{'segment_set $a $b}. +interpretation "Ordered set segment" 'segment_set a b = + (cic:/matita/dama/supremum/segment_ordered_set.con _ a b). + +(* Lemma 2.9 *) +lemma segment_preserves_supremum: + ∀O:ordered_set.∀l,u:O.∀a:sequence (segment_ordered_set ? l u). + ∀x:(segment_ordered_set ? l u). + (λn.fst (a n)) is_increasing ∧ + (fst x) is_supremum (λn.fst (a n)) → a ↑ x. +intros; split; cases H; clear H; +[1: apply H1; +|2: cases H2; split; clear H2; + [1: apply H; + |2: clear H; intro y0; apply (H3 (fst y0));]] +qed. + +(* Definition 2.10 *) +coinductive pair (A,B:Type) : Type ≝ prod : ∀a:A.∀b:B.pair A B. +definition first : ∀A.∀P.pair A P → A ≝ λA,P,s.match s with [prod x _ ⇒ x]. +definition second : ∀A.∀P.pair A P → P ≝ λA,P,s.match s with [prod _ y ⇒ y]. + +interpretation "pair pi1" 'pi1 x = + (cic:/matita/dama/supremum/first.con _ _ x). +interpretation "pair pi2" 'pi2 x = + (cic:/matita/dama/supremum/second.con _ _ x). + +lemma square_ordered_set: ordered_set → ordered_set. +intro O; apply (mk_ordered_set (pair O O)); +[1: intros (x y); apply (fst x ≰ fst y ∨ snd x ≰ snd y); +|2: intro x0; cases x0 (x y); clear x0; simplify; intro H; + cases H (X X); apply (os_coreflexive ?? X); +|3: intros 3 (x0 y0 z0); cases x0 (x1 x2); cases y0 (y1 y2) ; cases z0 (z1 z2); + clear x0 y0 z0; simplify; intro H; cases H (H1 H1); clear H; + [1: cases (os_cotransitive ??? z1 H1); [left; left|right;left]assumption; + |2: cases (os_cotransitive ??? z2 H1); [left;right|right;right]assumption]] +qed. + +definition square_segment ≝ + λO:ordered_set.λa,b:O.λx:square_ordered_set O. + (cic:/matita/logic/connectives/And.ind#xpointer(1/1) + (cic:/matita/logic/connectives/And.ind#xpointer(1/1) (fst x ≤ b) (a ≤ fst x)) + (cic:/matita/logic/connectives/And.ind#xpointer(1/1) (snd x ≤ b) (a ≤ snd x))). + +definition convex ≝ + λO:ordered_set.λU:square_ordered_set O → Prop. + ∀p.U p → fst p ≤ snd p → ∀y. square_segment ? (fst p) (snd p) y → U y. + +(* Definition 2.11 *) +definition upper_located ≝ + λO:ordered_set.λa:sequence O.∀x,y:O. y ≰ x → + (∃i:nat.a i ≰ x) ∨ (∃b:O.y≰b ∧ ∀i:nat.a i ≤ b). + +(* Lemma 2.12 *) +lemma uparrow_located: + ∀C:ordered_set.∀a:sequence C.∀u:C.a ↑ u → upper_located ? a. +intros (C a u H); cases H (H2 H3); clear H; intros 3 (x y Hxy); +cases H3 (H4 H5); clear H3; cases (os_cotransitive ??? u Hxy) (W W); +[2: cases (H5 ? W) (w Hw); left; exists [apply w] assumption; +|1: right; exists [apply u]; split; [apply W|apply H4]] +qed. + + + \ No newline at end of file -- 2.39.2