From cb2419357a3f80388f71eb2730bff154bd4ef000 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Jun 2008 15:53:27 +0000 Subject: [PATCH 1/1] some notation added with a bit PITA --- .../matita/contribs/dama/dama/bishop_set.ma | 21 +++++- .../contribs/dama/dama/cprop_connectives.ma | 26 ++++++- .../matita/contribs/dama/dama/depends | 14 ++-- .../matita/contribs/dama/dama/lebesgue.ma | 42 ++++------- .../contribs/dama/dama/models/uniformnat.ma | 11 ++- .../matita/contribs/dama/dama/ordered_set.ma | 26 +++++++ .../contribs/dama/dama/ordered_uniform.ma | 75 ++++++++++++------- .../dama/dama/property_exhaustivity.ma | 30 ++++---- .../contribs/dama/dama/property_sigma.ma | 15 ++-- .../matita/contribs/dama/dama/sequence.ma | 4 + .../matita/contribs/dama/dama/supremum.ma | 48 +----------- .../matita/contribs/dama/dama/uniform.ma | 50 +++++-------- 12 files changed, 193 insertions(+), 169 deletions(-) diff --git a/helm/software/matita/contribs/dama/dama/bishop_set.ma b/helm/software/matita/contribs/dama/dama/bishop_set.ma index 78176d776..9fee3d9fd 100644 --- a/helm/software/matita/contribs/dama/dama/bishop_set.ma +++ b/helm/software/matita/contribs/dama/dama/bishop_set.ma @@ -26,7 +26,7 @@ record bishop_set: Type ≝ { notation "hvbox(a break # b)" non associative with precedence 45 for @{ 'apart $a $b}. -interpretation "bishop_setapartness" 'apart x y = (bs_apart _ x y). +interpretation "bishop set apartness" 'apart x y = (bs_apart _ x y). definition bishop_set_of_ordered_set: ordered_set → bishop_set. intros (E); apply (mk_bishop_set E (λa,b:E. a ≰ b ∨ b ≰ a)); @@ -94,3 +94,22 @@ theorem lt_to_excess: ∀E:ordered_set.∀a,b:E. (a < b) → (b ≰ a). intros (E a b Lab); cases Lab (LEab Aab); cases Aab (H H);[cases (LEab H)] assumption; qed. + +definition bs_subset ≝ λO:bishop_set.λP,Q:O→Prop.∀x:O.P x → Q x. + +interpretation "bishop set subset" 'subset a b = (bs_subset _ a b). + +definition square_bishop_set : bishop_set → bishop_set. +intro S; apply (mk_bishop_set (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. + +notation "s 2 \atop \neq" non associative with precedence 90 + for @{ 'square_bs $s }. +interpretation "bishop set square" 'square x = (square_bishop_set x). +interpretation "bishop set square" 'square_bs x = (square_bishop_set x). \ No newline at end of file diff --git a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma index b42eaf61b..9e0e4b5fb 100644 --- a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma +++ b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma @@ -39,13 +39,29 @@ notation < "a ∧ b ∧ c ∧ d" left associative with precedence 35 for @{'and4 interpretation "constructive quaternary and" 'and4 x y z t = (Conj4 x y z t). +coinductive product (A,B:Type) : Type ≝ pair : ∀a:A.∀b:B.product A B. + +notation "a \times b" left associative with precedence 70 for @{'product $a $b}. +interpretation "prod" 'product a b = (product a b). + +definition first : ∀A.∀P.A × P → A ≝ λA,P,s.match s with [pair x _ ⇒ x]. +definition second : ∀A.∀P.A × P → P ≝ λA,P,s.match s with [pair _ y ⇒ y]. + +interpretation "pair pi1" 'pi1 = (first _ _). +interpretation "pair pi2" 'pi2 = (second _ _). +interpretation "pair pi1" 'pi1a x = (first _ _ x). +interpretation "pair pi2" 'pi2a x = (second _ _ x). +interpretation "pair pi1" 'pi1b x y = (first _ _ x y). +interpretation "pair pi2" 'pi2b x y = (second _ _ x y). + +notation "hvbox(\langle a, break b\rangle)" left associative with precedence 70 for @{ 'pair $a $b}. +interpretation "pair" 'pair a b = (pair _ _ a b). + inductive exT (A:Type) (P:A→CProp) : CProp ≝ ex_introT: ∀w:A. P w → exT A P. interpretation "CProp exists" 'exists \eta.x = (exT _ x). - -inductive exT23 (A:Type) (P:A→CProp) (Q:A→CProp) (R:A→A→CProp) : CProp ≝ - ex_introT23: ∀w,p:A. P w → Q p → R w p → exT23 A P Q R. +interpretation "dependent pair" 'pair a b = (ex_introT _ _ a b). notation < "'fst' \nbsp x" non associative with precedence 90 for @{'pi1a $x}. notation < "'snd' \nbsp x" non associative with precedence 90 for @{'pi2a $x}. @@ -65,6 +81,9 @@ interpretation "exT snd" 'pi2 = (pi2exT _ _). interpretation "exT snd" 'pi2a x = (pi2exT _ _ x). interpretation "exT snd" 'pi2b x y = (pi2exT _ _ x y). +inductive exT23 (A:Type) (P:A→CProp) (Q:A→CProp) (R:A→A→CProp) : CProp ≝ + ex_introT23: ∀w,p:A. P w → Q p → R w p → exT23 A P Q R. + definition pi1exT23 ≝ λA,P,Q,R.λx:exT23 A P Q R.match x with [ex_introT23 x _ _ _ _ ⇒ x]. definition pi2exT23 ≝ @@ -93,4 +112,3 @@ definition antisymmetric ≝ λA:Type.λR:A→A→CProp.λeq:A→A→Prop.∀x:A definition reflexive ≝ λA:Type.λR:A→A→CProp.∀x:A.R x x. definition transitive ≝ λA:Type.λR:A→A→CProp.∀x,y,z:A.R x y → R y z → R x z. - diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends index d00e75e49..99165ee70 100644 --- a/helm/software/matita/contribs/dama/dama/depends +++ b/helm/software/matita/contribs/dama/dama/depends @@ -1,17 +1,17 @@ -sandwich.ma ordered_uniform.ma property_sigma.ma ordered_uniform.ma russell_support.ma -uniform.ma supremum.ma bishop_set.ma ordered_set.ma -sequence.ma nat/nat.ma ordered_uniform.ma uniform.ma -supremum.ma bishop_set.ma cprop_connectives.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma ordered_set.ma sequence.ma -property_exhaustivity.ma ordered_uniform.ma property_sigma.ma bishop_set_rewrite.ma bishop_set.ma -cprop_connectives.ma logic/equality.ma -nat_ordered_set.ma ordered_set.ma bishop_set.ma cprop_connectives.ma nat/compare.ma +sequence.ma nat/nat.ma +nat_ordered_set.ma bishop_set.ma nat/compare.ma lebesgue.ma property_exhaustivity.ma sandwich.ma +property_exhaustivity.ma ordered_uniform.ma property_sigma.ma +cprop_connectives.ma logic/equality.ma ordered_set.ma cprop_connectives.ma +sandwich.ma ordered_uniform.ma russell_support.ma cprop_connectives.ma nat/nat.ma +uniform.ma supremum.ma +supremum.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma sequence.ma models/uniformnat.ma bishop_set_rewrite.ma nat_ordered_set.ma ordered_uniform.ma russell_support.ma uniform.ma datatypes/constructors.ma logic/equality.ma diff --git a/helm/software/matita/contribs/dama/dama/lebesgue.ma b/helm/software/matita/contribs/dama/dama/lebesgue.ma index dcf59e2aa..af0a11453 100644 --- a/helm/software/matita/contribs/dama/dama/lebesgue.ma +++ b/helm/software/matita/contribs/dama/dama/lebesgue.ma @@ -20,7 +20,7 @@ lemma order_converges_bigger_lowsegment: ∀C:ordered_set. ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u]. ∀x:C.∀p:a order_converges x. - ∀j.l ≤ (fst p) j. + ∀j.l ≤ (pi1exT23 ???? p) j. intros; cases p (xi yi Ux Dy Hxy); clear p; simplify; cases Ux (Ixi Sxi); clear Ux; cases Dy (Dyi Iyi); clear Dy; cases (Hxy j) (Ia Sa); clear Hxy; cases Ia (Da SSa); cases Sa (Inca SIa); clear Ia Sa; @@ -32,7 +32,7 @@ lemma order_converges_smaller_upsegment: ∀C:ordered_set. ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u]. ∀x:C.∀p:a order_converges x. - ∀j.(snd p) j ≤ u. + ∀j.(pi2exT23 ???? p) j ≤ u. intros; cases p; clear p; simplify; cases H1; clear H1; cases H2; clear H2; cases (H3 j); clear H3; cases H2; cases H7; clear H2 H7; intro H2; cases (H10 ? H2); @@ -46,12 +46,8 @@ theorem lebesgue_oc: ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u]. ∀x:C.a order_converges x → x ∈ [l,u] ∧ - ∀h:x ∈ [l,u]. (* manca il pullback? *) - uniform_converge - (uniform_space_OF_ordered_uniform_space - (segment_ordered_uniform_space C l u)) - (λn.sig_in C (λx.x∈[l,u]) (a n) (H n)) - (sig_in ?? x h). + ∀h:x ∈ [l,u]. + uniform_converge {[l,u]} (⌊n,〈a n,H n〉⌋) 〈x,h〉. intros; generalize in match (order_converges_bigger_lowsegment ???? H1 ? H2); generalize in match (order_converges_smaller_upsegment ???? H1 ? H2); @@ -69,17 +65,16 @@ split; [1: apply (le_transitive ???? (H8 0)); cases (Hyi 0); assumption |2: apply (le_transitive ????? (H4 0)); cases (Hxi 0); assumption] |2: intros 3 (h); - letin X ≝ (sig_in ?? x h); - letin Xi ≝ (λn.sig_in ?? (xi n) (Hxi n)); - letin Yi ≝ (λn.sig_in ?? (yi n) (Hyi n)); - letin Ai ≝ (λn:nat.sig_in ?? (a n) (H1 n)); - apply (sandwich {[l,u]} X Xi Yi Ai); try assumption; + letin Xi ≝ (⌊n,〈xi n,Hxi n〉⌋); + letin Yi ≝ (⌊n,〈yi n,Hyi n〉⌋); + letin Ai ≝ (⌊n,〈a n,H1 n〉⌋); + apply (sandwich {[l,u]} 〈?,h〉 Xi Yi Ai); try assumption; [1: intro j; cases (Hxy j); cases H3; cases H4; split; [apply (H5 0);|apply (H7 0)] - |2: cases (H l u Xi X) (Ux Uy); apply Ux; cases Hx; split; [apply H3;] + |2: cases (H l u Xi 〈?,h〉) (Ux Uy); apply Ux; cases Hx; split; [apply H3;] cases H4; split; [apply H5] intros (y Hy);cases (H6 (fst y));[2:apply Hy]; exists [apply w] apply H7; - |3: cases (H l u Yi X) (Ux Uy); apply Uy; cases Hy; split; [apply H3;] + |3: cases (H l u Yi 〈?,h〉) (Ux Uy); apply Uy; cases Hy; split; [apply H3;] cases H4; split; [apply H5] intros (y Hy);cases (H6 (fst y));[2:apply Hy]; exists [apply w] apply H7;]] qed. @@ -92,12 +87,8 @@ theorem lebesgue_se: ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u]. ∀x:C.a order_converges x → x ∈ [l,u] ∧ - ∀h:x ∈ [l,u]. (* manca il pullback? *) - uniform_converge - (uniform_space_OF_ordered_uniform_space - (segment_ordered_uniform_space C l u)) - (λn.sig_in C (λx.x∈[l,u]) (a n) (H n)) - (sig_in ?? x h). + ∀h:x ∈ [l,u]. + uniform_converge {[l,u]} (⌊n,〈a n,H n〉⌋) 〈x,h〉. intros (C S); generalize in match (order_converges_bigger_lowsegment ???? H1 ? H2); generalize in match (order_converges_smaller_upsegment ???? H1 ? H2); @@ -117,11 +108,10 @@ split; |2: intros 3; lapply (uparrow_upperlocated ? xi x Hx)as Ux; lapply (downarrow_lowerlocated ? yi x Hy)as Uy; - letin X ≝ (sig_in ?? x h); - letin Xi ≝ (λn.sig_in ?? (xi n) (Hxi n)); - letin Yi ≝ (λn.sig_in ?? (yi n) (Hyi n)); - letin Ai ≝ (λn:nat.sig_in ?? (a n) (H1 n)); - apply (sandwich {[l,u]} X Xi Yi Ai); try assumption; + letin Xi ≝ (⌊n,〈xi n,Hxi n〉⌋); + letin Yi ≝ (⌊n,〈yi n,Hyi n〉⌋); + letin Ai ≝ (⌊n,〈a n,H1 n〉⌋); + apply (sandwich {[l,u]} 〈x,h〉 Xi Yi Ai); try assumption; [1: intro j; cases (Hxy j); cases H3; cases H4; split; [apply (H5 0);|apply (H7 0)] |2: cases (restrict_uniform_convergence_uparrow ? S ?? (H l u) Xi x Hx); diff --git a/helm/software/matita/contribs/dama/dama/models/uniformnat.ma b/helm/software/matita/contribs/dama/dama/models/uniformnat.ma index 8c0acd9a2..824d6c293 100644 --- a/helm/software/matita/contribs/dama/dama/models/uniformnat.ma +++ b/helm/software/matita/contribs/dama/dama/models/uniformnat.ma @@ -19,14 +19,14 @@ include "uniform.ma". definition discrete_uniform_space_of_bishop_set:bishop_set → uniform_space. intro C; apply (mk_uniform_space C); [1: intro; apply (∃_:unit.∀n:C square.(fst n ≈ snd n → P n) ∧ (P n → fst n ≈ snd n)); -|2: intros 4 (U H x Hx); unfold in Hx; +|2: intros 4 (U H x Hx); simplify in Hx; cases H (_ H1); cases (H1 x); apply H2; apply Hx; |3: intros; cases H (_ PU); cases H1 (_ PV); exists[apply (λx.U x ∧ V x)] split; [1: exists[apply something] intro; cases (PU n); cases (PV n); split; intros; try split;[apply H2;|apply H4] try assumption; apply H3; cases H6; assumption; - |2: simplify; unfold mk_set; intros; assumption;] + |2: simplify; intros; assumption;] |4: intros; cases H (_ PU); exists [apply U] split; [1: exists [apply something] intro n; cases (PU n); split; intros; try split;[apply H1;|apply H2] assumption; @@ -95,13 +95,12 @@ split; cases Hcut1; assumption] qed. -alias symbol "pi1" = "sigma pi1". +alias symbol "pi1" = "exT fst". lemma nat_dedekind_sigma_complete: ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing → ∀x.x is_supremum a → ∃i.∀j.i ≤ j → fst x = fst (a j). -intros 5; cases x (s Hs); clear x; letin X ≝ (sig_in ℕ (λx:ℕ.x∈[l,u]) s Hs); +intros 5; cases x (s Hs); clear x; letin X ≝ (〈s,Hs〉); fold normalize X; intros; cases H1; -alias symbol "pi1" = "sigma pi1". letin spec ≝ (λi,j.fst (a j) = s ∨ (i ≤ j ∧ match i with [ O ⇒ fst (a j) = fst (a O) | S m ⇒ fst(a m) < fst (a j)])); letin m ≝ ( let rec aux i ≝ @@ -144,7 +143,7 @@ letin m ≝ ( apply os_le_to_nat_le; lapply (nat_le_to_os_le ?? H7) as H77; apply(trans_increasing ?? H (S n2) (pred) H77);]]]]] clearbody m; unfold spec in m; clear spec; -cut (∀i.fst a (m i) = s ∨ i ≤ fst (a (m i))) as key2;[ +cut (∀i.fst (a (m i)) = s ∨ i ≤ fst (a (m i))) as key2;[ letin find ≝ ( let rec find i u on u : nat ≝ match u with diff --git a/helm/software/matita/contribs/dama/dama/ordered_set.ma b/helm/software/matita/contribs/dama/dama/ordered_set.ma index c161fee45..a820eff54 100644 --- a/helm/software/matita/contribs/dama/dama/ordered_set.ma +++ b/helm/software/matita/contribs/dama/dama/ordered_set.ma @@ -48,3 +48,29 @@ cases (os_cotransitive ??? a1 Eab) (H H); [cases (Laa1 H)] cases (os_cotransitive ??? b1 H) (H1 H1); [assumption] cases (Lb1b H1); qed. + +lemma square_ordered_set: ordered_set → ordered_set. +intro O; +apply (mk_ordered_set (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. + +notation "s 2 \atop \nleq" non associative with precedence 90 + for @{ 'square_os $s }. +notation > "s 'square'" non associative with precedence 90 + for @{ 'square $s }. +interpretation "ordered set square" 'square s = (square_ordered_set s). +interpretation "ordered set square" 'square_os s = (square_ordered_set s). + +definition os_subset ≝ λO:ordered_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 "ordered set subset" 'subset a b = (os_subset _ a b). + diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma index c9b5e7da6..8aacb5b59 100644 --- a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma +++ b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma @@ -37,58 +37,80 @@ record ordered_uniform_space : Type ≝ { ous_convex: ∀U.us_unifbase ous_stuff U → convex ous_stuff U }. -lemma segment_square_of_O_square: +definition invert_os_relation ≝ + λC:ordered_set.λU:C square → Prop. + λx:C square. U 〈snd x,fst x〉. + +interpretation "relation invertion" 'invert a = (invert_os_relation _ a). +interpretation "relation invertion" 'invert_symbol = (invert_os_relation _). +interpretation "relation invertion" 'invert_appl a x = (invert_os_relation _ a x). + +lemma segment_square_of_ordered_set_square: ∀O:ordered_set.∀u,v:O.∀x:O square. fst x ∈ [u,v] → snd x ∈ [u,v] → {[u,v]} square. intros; split; exists; [1: apply (fst x) |3: apply (snd x)] assumption; qed. -coercion cic:/matita/dama/ordered_uniform/segment_square_of_O_square.con 0 2. +coercion cic:/matita/dama/ordered_uniform/segment_square_of_ordered_set_square.con 0 2. -alias symbol "pi1" (instance 4) = "sigma pi1". -alias symbol "pi1" (instance 2) = "sigma pi1". -lemma O_square_of_segment_square : +alias symbol "pi1" (instance 4) = "exT fst". +alias symbol "pi1" (instance 2) = "exT fst". +lemma ordered_set_square_of_segment_square : ∀O:ordered_set.∀u,v:O.{[u,v]} square → O square ≝ - λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈fst(fst b),fst(snd b)〉. + λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈fst(fst b),fst(snd b)〉. -coercion cic:/matita/dama/ordered_uniform/O_square_of_segment_square.con. +coercion cic:/matita/dama/ordered_uniform/ordered_set_square_of_segment_square.con. lemma restriction_agreement : ∀O:ordered_uniform_space.∀l,r:O.∀P:{[l,r]} square → Prop.∀OP:O square → Prop.Prop. -apply(λO:ordered_uniform_space.λl,r:O.λP:{[l,r]} square → Prop.λOP:O square → Prop. - ∀b:O square.∀H1,H2. - (P b → OP b) ∧ (OP b → P b)); +apply(λO:ordered_uniform_space.λl,r:O. + λP:{[l,r]} square → Prop.λOP:O square → Prop. + ∀b:O square.∀H1,H2.(P b → OP b) ∧ (OP b → P b)); [5,7: apply H1|6,8:apply H2]skip; qed. lemma unrestrict: ∀O:ordered_uniform_space.∀l,r:O.∀U,u.∀x:{[l,r]} square. restriction_agreement ? l r U u → U x → u x. -intros 7; cases x (b b1); cases b; cases b1; -cases (H 〈x1,x2〉 H1 H2) (L _); intros; apply L; assumption; +intros 7; cases x (b b1); cases b (w1 H1); cases b1 (w2 H2); clear b b1 x; +cases (H 〈w1,w2〉 H1 H2) (L _); intro Uw; apply L; apply Uw; qed. lemma restrict: ∀O:ordered_uniform_space.∀l,r:O.∀U,u.∀x:{[l,r]} square. restriction_agreement ? l r U u → u x → U x. -intros 6; cases x (b b1); cases b; cases b1; intros (X); -cases (X 〈x1,x2〉 H H1) (_ R); apply R; assumption; +intros 6; cases x (b b1); cases b (w1 H1); cases b1 (w2 H2); clear b1 b x; +intros (Ra uw); cases (Ra 〈w1,w2〉 H1 H2) (_ R); apply R; apply uw; qed. lemma invert_restriction_agreement: - ∀O:ordered_uniform_space.∀l,r:O.∀U:{[l,r]} square → Prop.∀u. + ∀O:ordered_uniform_space.∀l,r:O. + ∀U:{[l,r]} square → Prop.∀u:O square → Prop. restriction_agreement ? l r U u → restriction_agreement ? l r (inv U) (inv u). intros 9; split; intro; -[1: apply (unrestrict ????? (segment_square_of_O_square ??? 〈snd b,fst b〉 H2 H1) H H3); -|2: apply (restrict ????? (segment_square_of_O_square ??? 〈snd b,fst b〉 H2 H1) H H3);] +[1: apply (unrestrict ????? (segment_square_of_ordered_set_square ??? 〈snd b,fst b〉 H2 H1) H H3); +|2: apply (restrict ????? (segment_square_of_ordered_set_square ??? 〈snd b,fst b〉 H2 H1) H H3);] qed. +alias symbol "square" (instance 8) = "bishop set square". lemma bs_of_ss: ∀O:ordered_set.∀u,v:O.{[u,v]} square → (bishop_set_of_ordered_set O) square ≝ - λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈fst(fst b),fst(snd b)〉. + λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈fst(fst b),fst(snd b)〉. -notation < "x \sub \neq" non associative with precedence 91 for @{'bsss $x}. +notation < "x \sub \neq" left associative with precedence 91 for @{'bsss $x}. interpretation "bs_of_ss" 'bsss x = (bs_of_ss _ _ _ x). +alias symbol "square" (instance 7) = "ordered set square". +alias symbol "pair" (instance 4) = "dependent pair". +alias symbol "pair" (instance 2) = "dependent pair". +lemma ss_of_bs: + ∀O:ordered_set.∀u,v:O. + ∀b:O square.fst b ∈ [u,v] → snd b ∈ [u,v] → {[u,v]} square ≝ + λO:ordered_set.λu,v:O. + λb:(O:bishop_set) square.λH1,H2.〈〈fst b,H1〉,〈snd b,H2〉〉. + +notation < "x \sub \nleq" left associative with precedence 91 for @{'ssbs $x}. +interpretation "ss_of_bs" 'ssbs x = (ss_of_bs _ _ _ x _ _). + lemma segment_ordered_uniform_space: ∀O:ordered_uniform_space.∀u,v:O.ordered_uniform_space. intros (O l r); apply mk_ordered_uniform_space; @@ -97,7 +119,7 @@ intros (O l r); apply mk_ordered_uniform_space; letin f ≝ (λP:{[l,r]} square → Prop. ∃OP:O square → Prop. (us_unifbase O OP) ∧ restriction_agreement ??? P OP); apply (mk_uniform_space (bishop_set_of_ordered_set {[l,r]}) f); - [1: intros (U H); intro x; unfold mk_set; simplify; + [1: intros (U H); intro x; simplify; cases H (w Hw); cases Hw (Gw Hwp); clear H Hw; intro Hm; lapply (us_phi1 ?? Gw x Hm) as IH; apply (restrict ?????? Hwp IH); @@ -107,22 +129,23 @@ intros (O l r); apply mk_ordered_uniform_space; exists; [apply (λb:{[l,r]} square.w b)] split; [1: unfold f; simplify; clearbody f; exists; [apply w]; split; [assumption] intro b; simplify; - unfold segment_square_of_O_square; (* ??? *) + unfold segment_square_of_ordered_set_square; cases b; intros; split; intros; assumption; - |2: intros 2 (x Hx); unfold mk_set; cases (Hw ? Hx); split; + |2: intros 2 (x Hx); cases (Hw ? Hx); split; [apply (restrict ?????? HuU H)|apply (restrict ?????? HvV H1);]] |3: intros (U Hu); cases Hu (u HU); cases HU (Gu HuU); clear Hu HU; cases (us_phi3 ?? Gu) (w HW); cases HW (Gw Hwu); clear HW; exists; [apply (λx:{[l,r]} square.w x)] split; [1: exists;[apply w];split;[assumption] intros; simplify; intro; - unfold segment_square_of_O_square; (* ??? *) + unfold segment_square_of_ordered_set_square; cases b; intros; split; intro; assumption; |2: intros 2 (x Hx); apply (restrict ?????? HuU); apply Hwu; cases Hx (m Hm); exists[apply (fst m)] apply Hm;] |4: intros (U HU x); cases HU (u Hu); cases Hu (Gu HuU); clear HU Hu; cases (us_phi4 ?? Gu x) (Hul Hur); split; intros; - [1: apply (restrict ?????? (invert_restriction_agreement ????? HuU)); + [1: lapply (invert_restriction_agreement ????? HuU) as Ra; + apply (restrict ????? x Ra); apply Hul; apply (unrestrict ?????? HuU H); |2: apply (restrict ?????? HuU); apply Hur; apply (unrestrict ?????? (invert_restriction_agreement ????? HuU) H);]] @@ -138,12 +161,12 @@ interpretation "Ordered uniform space segment" 'segment_set a b = (segment_ordered_uniform_space _ a b). (* Lemma 3.2 *) -alias symbol "pi1" = "sigma pi1". +alias symbol "pi1" = "exT fst". lemma restric_uniform_convergence: ∀O:ordered_uniform_space.∀l,u:O. ∀x:{[l,u]}. ∀a:sequence {[l,u]}. - (λn.fst (a n)) uniform_converges (fst x) → + ⌊n,fst (a n)⌋ uniform_converges (fst x) → a uniform_converges x. intros 8; cases H1; cases H2; clear H2 H1; cases (H ? H3) (m Hm); exists [apply m]; intros; diff --git a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma index 44be29543..58de86885 100644 --- a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma +++ b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma @@ -23,18 +23,18 @@ definition exhaustive ≝ (b is_decreasing → b is_lower_located → b is_cauchy). lemma segment_upperbound: - ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.u is_upper_bound (λn.fst (a n)). + ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.u is_upper_bound ⌊n,fst (a n)⌋. intros 5; change with (fst (a n) ≤ u); cases (a n); cases H; assumption; qed. lemma segment_lowerbound: - ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.l is_lower_bound (λn.fst (a n)). + ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.l is_lower_bound ⌊n,fst (a n)⌋. intros 5; change with (l ≤ fst (a n)); cases (a n); cases H; assumption; qed. lemma segment_preserves_uparrow: ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.∀x,h. - (λn.fst (a n)) ↑ x → a ↑ (sig_in ?? x h). + ⌊n,fst (a n)⌋ ↑ x → a ↑ 〈x,h〉. intros; cases H (Ha Hx); split [apply Ha] cases Hx; split; [apply H1] intros; cases (H2 (fst y)); [2: apply H3;] exists [apply w] assumption; @@ -42,7 +42,7 @@ qed. lemma segment_preserves_downarrow: ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.∀x,h. - (λn.fst (a n)) ↓ x → a ↓ (sig_in ?? x h). + ⌊n,fst (a n)⌋ ↓ x → a ↓ 〈x,h〉. intros; cases H (Ha Hx); split [apply Ha] cases Hx; split; [apply H1] intros; cases (H2 (fst y));[2:apply H3]; exists [apply w] assumption; @@ -51,7 +51,7 @@ qed. (* Fact 2.18 *) lemma segment_cauchy: ∀C:ordered_uniform_space.∀l,u:C.∀a:sequence {[l,u]}. - a is_cauchy → (λn:nat.fst (a n)) is_cauchy. + a is_cauchy → ⌊n,fst (a n)⌋ is_cauchy. intros 7; alias symbol "pi1" (instance 3) = "pair pi1". alias symbol "pi2" = "pair pi2". @@ -65,18 +65,18 @@ qed. lemma restrict_uniform_convergence_uparrow: ∀C:ordered_uniform_space.property_sigma C → ∀l,u:C.exhaustive {[l,u]} → - ∀a:sequence {[l,u]}.∀x:C. (λn.fst (a n)) ↑ x → - x∈[l,u] ∧ ∀h:x ∈ [l,u].a uniform_converges (sig_in ?? x h). + ∀a:sequence {[l,u]}.∀x:C. ⌊n,fst (a n)⌋ ↑ x → + x∈[l,u] ∧ ∀h:x ∈ [l,u].a uniform_converges 〈x,h〉. intros; cases H2 (Ha Hx); clear H2; cases Hx; split; [1: split; [1: apply (supremum_is_upper_bound C ?? Hx u); apply (segment_upperbound ? l); - |2: apply (le_transitive ?? (fst (a 0))); [2: apply H2;] + |2: apply (le_transitive ? ??? ? (H2 O)); apply (segment_lowerbound ?l u);] |2: intros; - lapply (uparrow_upperlocated ? a (sig_in ?? x h)) as Ha1; + lapply (uparrow_upperlocated ? a 〈x,h〉) as Ha1; [2: apply segment_preserves_uparrow;split; assumption;] - lapply (segment_preserves_supremum ?l u a (sig_in ??? h)) as Ha2; + lapply (segment_preserves_supremum ? l u a 〈?,h〉) as Ha2; [2:split; assumption]; cases Ha2; clear Ha2; cases (H1 a a); lapply (H6 H4 Ha1) as HaC; lapply (segment_cauchy ? l u ? HaC) as Ha; @@ -87,18 +87,18 @@ qed. lemma restrict_uniform_convergence_downarrow: ∀C:ordered_uniform_space.property_sigma C → ∀l,u:C.exhaustive {[l,u]} → - ∀a:sequence {[l,u]}.∀x:C. (λn.fst (a n)) ↓ x → - x∈[l,u] ∧ ∀h:x ∈ [l,u].a uniform_converges (sig_in ?? x h). + ∀a:sequence {[l,u]}.∀x:C. ⌊n,fst (a n)⌋ ↓ x → + x∈[l,u] ∧ ∀h:x ∈ [l,u].a uniform_converges 〈x,h〉. intros; cases H2 (Ha Hx); clear H2; cases Hx; split; [1: split; [2: apply (infimum_is_lower_bound C ?? Hx l); apply (segment_lowerbound ? l u); - |1: apply (le_transitive ?? (fst (a 0))); [apply H2;] + |1: apply (le_transitive ???? (H2 O)); apply (segment_upperbound ? l u);] |2: intros; - lapply (downarrow_lowerlocated ? a (sig_in ?? x h)) as Ha1; + lapply (downarrow_lowerlocated ? a 〈x,h〉) as Ha1; [2: apply segment_preserves_downarrow;split; assumption;] - lapply (segment_preserves_infimum ?l u a (sig_in ??? h)) as Ha2; + lapply (segment_preserves_infimum ?l u a 〈?,h〉) as Ha2; [2:split; assumption]; cases Ha2; clear Ha2; cases (H1 a a); lapply (H7 H4 Ha1) as HaC; lapply (segment_cauchy ? l u ? HaC) as Ha; diff --git a/helm/software/matita/contribs/dama/dama/property_sigma.ma b/helm/software/matita/contribs/dama/dama/property_sigma.ma index ece02e9ba..ba90bb0ab 100644 --- a/helm/software/matita/contribs/dama/dama/property_sigma.ma +++ b/helm/software/matita/contribs/dama/dama/property_sigma.ma @@ -57,19 +57,20 @@ qed. lemma max_le_r: ∀n,m,z.max n m ≤ z → m ≤ z. intros; rewrite > sym_max in H; apply (max_le_l ??? H); qed. - + (* Lemma 3.6 *) lemma sigma_cauchy: ∀C:ordered_uniform_space.property_sigma C → ∀a:sequence C.∀l:C.(a ↑ l ∨ a ↓ l) → a is_cauchy → a uniform_converges l. intros 8; cases (H ? H3) (w H5); cases H5 (H8 H9); clear H5; +alias symbol "pair" = "pair". +letin spec ≝ (λz,k:nat.∀i,j,l:nat.k ≤ i → k ≤ j → l ≤ z → w l 〈a i,a j〉); letin m ≝ (hide ? (let rec aux (i:nat) : nat ≝ match i with [ O ⇒ match H2 (w i) ? with [ ex_introT k _ ⇒ k ] | S i' ⇒ max (match H2 (w i) ? with [ ex_introT k _ ⇒ k ]) (S (aux i')) ] in aux - : - ∀z:nat.∃k:nat.∀i,j,l.k ≤ i → k ≤ j → l ≤ z → w l 〈a i, a j〉)); + : ∀z.∃k. spec z k)); unfold spec in aux ⊢ %; [1,2:apply H8; |3: intros 3; cases (H2 (w n) (H8 n)); simplify in ⊢ (? (? % ?) ?→?); simplify in ⊢ (?→? (? % ?) ?→?); @@ -82,15 +83,15 @@ letin m ≝ (hide ? (let rec aux (i:nat) : nat ≝ apply lt_to_le; apply (max_le_r w1); assumption; |4: intros; clear H6; rewrite > H4 in H5; rewrite < (le_n_O_to_eq ? H11); apply H5; assumption;] -cut (((m : nat→nat) : sequence nat_ordered_set) is_strictly_increasing) as Hm; [2: +cut ((⌊x,(m x:nat)⌋ : sequence nat_ordered_set) is_strictly_increasing) as Hm; [2: intro n; change with (S (m n) ≤ m (S n)); unfold m; whd in ⊢ (? ? %); apply (le_max ? (S (m n)));] -cut (((m : nat→nat) : sequence nat_ordered_set) is_increasing) as Hm1; [2: +cut ((⌊x,(m x:nat)⌋ : sequence nat_ordered_set) is_increasing) as Hm1; [2: intro n; intro L; change in L with (m (S n) < m n); lapply (Hm n) as L1; change in L1 with (m n < m (S n)); lapply (trans_lt ??? L L1) as L3; apply (not_le_Sn_n ? L3);] -clearbody m; -cut ((λx:nat.a (m x))↑ l ∨ (λx:nat.a (m x)) ↓ l) as H10; [2: +clearbody m; unfold spec in m Hm Hm1; clear spec; +cut (⌊x,a (m x)⌋ ↑ l ∨ ⌊x,a (m x)⌋ ↓ l) as H10; [2: cases H1; [ left; apply (selection_uparrow ?? Hm a l H4); | right; apply (selection_downarrow ?? Hm a l H4);]] diff --git a/helm/software/matita/contribs/dama/dama/sequence.ma b/helm/software/matita/contribs/dama/dama/sequence.ma index 482e8aed7..c64315481 100644 --- a/helm/software/matita/contribs/dama/dama/sequence.ma +++ b/helm/software/matita/contribs/dama/dama/sequence.ma @@ -26,6 +26,10 @@ notation < "hvbox((\lfloor p \rfloor) \sub ident i)" left associative with precedence 70 for @{ 'sequence (\lambda ${ident i} : $t . $p)}. +notation > "hvbox((\lfloor p \rfloor) \sub ident i)" + left associative with precedence 70 +for @{ 'sequence (\lambda ${ident i} . $p)}. + notation > "hvbox(\lfloor ident i, p \rfloor)" left associative with precedence 70 for @{ 'sequence (\lambda ${ident i} . $p)}. diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma index ea5c55050..468c1d506 100644 --- a/helm/software/matita/contribs/dama/dama/supremum.ma +++ b/helm/software/matita/contribs/dama/dama/supremum.ma @@ -237,16 +237,6 @@ notation "hvbox(x \in break [a,b])" non associative with precedence 45 for @{'segment_in $a $b $x}. interpretation "Ordered set sergment in" 'segment_in a b x= (segment _ a b x). -(* -coinductive sigma (A:Type) (P:A→Prop) : Type ≝ sig_in : ∀x.P x → sigma A P. - -definition pi1sig : ∀A.∀P.sigma A P → A ≝ λA,P,s.match s with [sig_in x _ ⇒ x]. - -interpretation "sigma pi1" 'pi1a x = (pi1sig _ _ x). - -interpretation "Type exists" 'exists \eta.x = (sigma _ 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])); @@ -284,41 +274,11 @@ intros; split; cases H; clear H; 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 = (first _ _). -interpretation "pair pi2" 'pi2 = (second _ _). -interpretation "pair pi1" 'pi1a x = (first _ _ x). -interpretation "pair pi2" 'pi2a x = (second _ _ x). -interpretation "pair pi1" 'pi1b x y = (first _ _ x y). -interpretation "pair pi2" 'pi2b x y = (second _ _ x y). - -notation "hvbox(\langle a, break b\rangle)" left associative with precedence 70 for @{ 'pair $a $b}. -interpretation "pair" 'pair a b = (prod _ _ a b). -interpretation "prod" 'product a b = (pair a b). - -lemma square_ordered_set: ordered_set → ordered_set. -intro O; -apply (mk_ordered_set (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. - -notation < "s 2 \atop \nleq" non associative with precedence 90 - for @{ 'square $s }. -notation > "s 'square'" non associative with precedence 90 - for @{ 'square $s }. -interpretation "ordered set square" 'square s = (square_ordered_set s). - +alias symbol "square" = "ordered set square". +alias symbol "pi2" = "pair pi2". +alias symbol "pi1" = "pair pi1". definition square_segment ≝ - λO:ordered_set.λa,b:O.λx:square_ordered_set O. + λO:ordered_set.λa,b:O.λx:O square. And4 (fst x ≤ b) (a ≤ fst x) (snd x ≤ b) (a ≤ snd x). definition convex ≝ diff --git a/helm/software/matita/contribs/dama/dama/uniform.ma b/helm/software/matita/contribs/dama/dama/uniform.ma index b8b77572b..faba6d83a 100644 --- a/helm/software/matita/contribs/dama/dama/uniform.ma +++ b/helm/software/matita/contribs/dama/dama/uniform.ma @@ -14,55 +14,39 @@ 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 = (subset _ a b). - -notation < "s 2 \atop \neq" non associative with precedence 90 - for @{ 'square2 $s }. -notation > "s 'square'" non associative with precedence 90 - for @{ 'square $s }. -interpretation "bishop set square" 'square x = (square_bishop_set x). -interpretation "bishop set square" 'square2 x = (square_bishop_set x). +(* Definition 2.13 *) +alias symbol "square" = "bishop set square". +alias symbol "pair" = "pair". alias symbol "exists" = "exists". alias symbol "and" = "logical and". -definition compose_relations ≝ +definition compose_bs_relations ≝ λC:bishop_set.λU,V:C square → Prop. λx:C square.∃y:C. U 〈fst x,y〉 ∧ V 〈y,snd x〉. -notation "a \circ b" left associative with precedence 70 - for @{'compose $a $b}. -interpretation "relations composition" 'compose a b = (compose_relations _ a b). +definition compose_os_relations ≝ + λC:ordered_set.λU,V:C square → Prop. + λx:C square.∃y:C. U 〈fst x,y〉 ∧ V 〈y,snd x〉. + +interpretation "bishop set relations composition" 'compose a b = (compose_bs_relations _ a b). +interpretation "ordered set relations composition" 'compose a b = (compose_os_relations _ a b). -definition invert_relation ≝ +definition invert_bs_relation ≝ λC:bishop_set.λU:C square → Prop. λx:C square. U 〈snd x,fst x〉. notation < "s \sup (-1)" left associative with precedence 70 for @{ 'invert $s }. notation < "s \sup (-1) x" left associative with precedence 70 - for @{ 'invert2 $s $x}. + for @{ 'invert_appl $s $x}. notation > "'inv'" right associative with precedence 70 - for @{ 'invert0 }. -interpretation "relation invertion" 'invert a = (invert_relation _ a). -interpretation "relation invertion" 'invert0 = (invert_relation _). -interpretation "relation invertion" 'invert2 a x = (invert_relation _ a x). + for @{ 'invert_symbol }. +interpretation "relation invertion" 'invert a = (invert_bs_relation _ a). +interpretation "relation invertion" 'invert_symbol = (invert_bs_relation _). +interpretation "relation invertion" 'invert_appl a x = (invert_bs_relation _ a x). alias symbol "exists" = "CProp exists". +alias symbol "compose" = "bishop set relations composition". alias symbol "and" (instance 21) = "constructive and". alias symbol "and" (instance 16) = "constructive and". alias symbol "and" (instance 9) = "constructive and". -- 2.39.2