From: Enrico Tassi Date: Thu, 5 Jun 2008 15:28:56 +0000 (+0000) Subject: sandwich is back X-Git-Tag: make_still_working~5084 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cb4d4678ada706caaf8c54f2d6780c228645f911;p=helm.git sandwich is back --- diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends index ea9ec7bff..c2b2004bb 100644 --- a/helm/software/matita/contribs/dama/dama/depends +++ b/helm/software/matita/contribs/dama/dama/depends @@ -7,6 +7,8 @@ sequence.ma nat/nat.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 +ordered_uniform.ma uniform.ma +sandwich.ma ordered_uniform.ma logic/equality.ma nat/compare.ma nat/nat.ma diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma index 974405214..34b33d0ac 100644 --- a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma +++ b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma @@ -34,29 +34,119 @@ 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 -}. + ous_convex: ∀U.us_unifbase ous_stuff U → convex ous_stuff U +}. + +lemma segment_square_of_O_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. +alias symbol "pi1" (instance 4) = "sigma pi1". +alias symbol "pi1" (instance 2) = "sigma pi1". +lemma O_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)〉. + +coercion cic:/matita/dama/ordered_uniform/O_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)); +[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; +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; +qed. + +lemma invert_restriction_agreement: + ∀O:ordered_uniform_space.∀l,r:O.∀U:{[l,r]} square → Prop.∀u. + 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);] +qed. + +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)〉. + +notation < "x \sub \neq" non associative with precedence 91 for @{'bsss $x}. +interpretation "bs_of_ss" 'bsss x = + (cic:/matita/dama/ordered_uniform/bs_of_ss.con _ _ _ x). 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; +intros (O l r); apply mk_ordered_uniform_space; +[1: apply (mk_ordered_uniform_space_ {[l,r]}); + [1: alias symbol "and" = "constructive and". + 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; + 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); + |2: intros (U V HU HV); cases HU (u Hu); cases HV (v Hv); clear HU HV; + cases Hu (Gu HuU); cases Hv (Gv HvV); clear Hu Hv; + cases (us_phi2 ??? Gu Gv) (w HW); cases HW (Gw Hw); clear HW; + 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; (* ??? *) + cases b; intros; split; intros; assumption; + |2: intros 2 (x Hx); unfold mk_set; 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; (* ??? *) + 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)); + apply Hul; apply (unrestrict ?????? HuU H); + |2: apply (restrict ?????? HuU); apply Hur; + apply (unrestrict ?????? (invert_restriction_agreement ????? HuU) H);]] + |2: simplify; reflexivity;] +|2: simplify; unfold convex; intros; + cases H (u HU); cases HU (Gu HuU); clear HU H; + lapply (ous_convex ?? Gu (bs_of_ss ? l r p) ? H2 (bs_of_ss ? l r y) H3) as Cu; + [1: apply (unrestrict ?????? HuU); apply H1; + |2: apply (restrict ?????? HuU Cu);]] qed. +interpretation "Ordered uniform space segment" 'segment_set a b = + (cic:/matita/dama/ordered_uniform/segment_ordered_uniform_space.con _ a b). (* Lemma 3.2 *) +alias symbol "pi1" = "sigma pi1". 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) → *) + ∀x:{[l,u]}. + ∀a:sequence {[l,u]}. + (λn.fst (a n)) uniform_converges (fst x) → a uniform_converges x. - - \ No newline at end of file +intros 8; cases H1; cases H2; clear H2 H1; +cases (H ? H3) (m Hm); exists [apply m]; intros; +apply (restrict ? l u ??? H4); apply (Hm ? H1); +qed. + diff --git a/helm/software/matita/contribs/dama/dama/sandwich.ma b/helm/software/matita/contribs/dama/dama/sandwich.ma new file mode 100644 index 000000000..df66b8b8c --- /dev/null +++ b/helm/software/matita/contribs/dama/dama/sandwich.ma @@ -0,0 +1,49 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ordered_uniform.ma". + +lemma le_w_plus: ∀n,m,o.n+m≤o → m ≤ o. +intro; elim n; simplify; [assumption] +lapply (le_S ?? H1); apply H; apply le_S_S_to_le; assumption; +qed. + +alias symbol "leq" = "Ordered set less or equal than". +alias symbol "and" = "logical and". +theorem sandwich: + ∀O:ordered_uniform_space.∀l:O.∀a,b,x:sequence O. + (∀i:nat.a i ≤ x i ∧ x i ≤ b i) → + a uniform_converges l → + b uniform_converges l → + x uniform_converges l. +intros 10; +cases (us_phi3 ? ? H3) (V GV); cases GV (Gv HV); clear GV; +cases (us_phi3 ? ? Gv) (W GW); cases GW (Gw HW); clear GW; +cases (H1 ? Gw) (ma Hma); cases (H2 ? Gw) (mb Hmb); clear H1 H2; +exists [apply (ma + mb)] intros; apply (HV 〈l,(x i)〉); +unfold; simplify; exists [apply (a i)] split; +[2: apply (ous_convex ?? Gv 〈a i,b i〉); cases (H i) (Lax Lxb); clear H; + [1: apply HW; exists [apply l]simplify; split; + [1: cases (us_phi4 ?? Gw 〈(a i),l〉); apply H2; clear H2 H; + apply (Hma i); rewrite > sym_plus in H1; apply (le_w_plus mb); assumption; + |2: apply Hmb; apply (le_w_plus ma); assumption] + |2: simplify; apply (le_transitive ???? Lax Lxb); + |3: simplify; repeat split; try assumption; + [1: apply (le_transitive ???? Lax Lxb); + |2: (* prove le_reflexive *) intro X; cases (os_coreflexive ?? X)]] +|1: apply HW; exists[apply l] simplify; split; + [1: apply (us_phi1 ?? Gw); unfold; apply eq_reflexive; + |2: apply Hma; rewrite > sym_plus in H1; apply (le_w_plus mb); assumption;]] +qed. + diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma index 0c6d545b8..b2411f652 100644 --- a/helm/software/matita/contribs/dama/dama/supremum.ma +++ b/helm/software/matita/contribs/dama/dama/supremum.ma @@ -187,7 +187,7 @@ notation "[a,b]" non associative with precedence 50 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 +notation "hvbox(x \in break [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). @@ -196,13 +196,13 @@ coinductive sigma (A:Type) (P:A→Prop) : Type ≝ sig_in : ∀x.P x → sigma A 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' \nbsp x" non associative with precedence 50 for @{'pi1 $x}. +notation < "'snd' \nbsp 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). @@ -214,15 +214,14 @@ intros (O u v); apply (mk_ordered_set (∃x.x ∈ [u,v])); |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 +notation "hvbox({[a, break 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). + ∀O:ordered_set.∀l,u:O.∀a:sequence {[l,u]}.∀x:{[l,u]}. (λn.fst (a n)) is_increasing ∧ (fst x) is_supremum (λn.fst (a n)) → a ↑ x. intros; split; cases H; clear H; @@ -241,9 +240,17 @@ interpretation "pair pi1" 'pi1 x = (cic:/matita/dama/supremum/first.con _ _ x). interpretation "pair pi2" 'pi2 x = (cic:/matita/dama/supremum/second.con _ _ x). + +notation "hvbox(\langle a, break b\rangle)" non associative with precedence 91 for @{ 'pair $a $b}. +interpretation "pair" 'pair a b = + (cic:/matita/dama/supremum/pair.ind#xpointer(1/1/1) _ _ a b). + +notation "a \times b" left associative with precedence 60 for @{'prod $a $b}. +interpretation "prod" 'prod a b = + (cic:/matita/dama/supremum/pair.ind#xpointer(1/1) a b). lemma square_ordered_set: ordered_set → ordered_set. -intro O; apply (mk_ordered_set (pair O O)); +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); @@ -252,6 +259,13 @@ intro O; apply (mk_ordered_set (pair O O)); [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 = + (cic:/matita/dama/supremum/square_ordered_set.con s). definition square_segment ≝ λO:ordered_set.λa,b:O.λx:square_ordered_set O. @@ -260,7 +274,7 @@ definition square_segment ≝ (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. + λO:ordered_set.λU:O square → Prop. ∀p.U p → fst p ≤ snd p → ∀y. square_segment ? (fst p) (snd p) y → U y. (* Definition 2.11 *) diff --git a/helm/software/matita/contribs/dama/dama/uniform.ma b/helm/software/matita/contribs/dama/dama/uniform.ma index 2b5ed2cb8..d5d714726 100644 --- a/helm/software/matita/contribs/dama/dama/uniform.ma +++ b/helm/software/matita/contribs/dama/dama/uniform.ma @@ -32,41 +32,55 @@ notation "a \subseteq u" left associative with precedence 70 interpretation "Bishop subset" 'subset a b = (cic:/matita/dama/uniform/subset.con _ a b). -notation "{ ident x : t | p }" non associative with precedence 50 +notation "hvbox({ ident x : t | break 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 2 \atop \neq" non associative with precedence 90 + for @{ 'square2 $s }. notation > "s 'square'" non associative with precedence 90 for @{ 'square $s }. -interpretation "bishop suqare set" 'square x = +interpretation "bishop set square" 'square x = + (cic:/matita/dama/uniform/square_bishop_set.con x). +interpretation "bishop set square" 'square2 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)). + λx:C square.∃y:C. U 〈fst x,y〉 ∧ V 〈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). +notation "hvbox(x \in break a \circ break b)" non associative with precedence 50 + for @{'compose2 $a $b $x}. +interpretation "relations composition" 'compose2 a b x = + (cic:/matita/dama/uniform/compose_relations.con _ a b x). definition invert_relation ≝ λC:bishop_set.λU:C square → Prop. - λx:C square. U (prod ?? (snd x) (fst x)). + λx:C square. U 〈snd x,fst x〉. notation < "s \sup (-1)" non associative with precedence 90 for @{ 'invert $s }. +notation < "s \sup (-1) x" non associative with precedence 90 + for @{ 'invert2 $s $x}. notation > "'inv' s" non associative with precedence 90 for @{ 'invert $s }. interpretation "relation invertion" 'invert a = (cic:/matita/dama/uniform/invert_relation.con _ a). +interpretation "relation invertion" 'invert2 a x = + (cic:/matita/dama/uniform/invert_relation.con _ a x). +alias symbol "exists" = "CProp exists". +alias symbol "and" (instance 18) = "constructive and". +alias symbol "and" (instance 10) = "constructive and". record uniform_space : Type ≝ { us_carr:> bishop_set; us_unifbase: (us_carr square → Prop) → CProp; @@ -76,14 +90,14 @@ record uniform_space : Type ≝ { ∃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 ... *) + us_phi4: ∀U:us_carr square → Prop. us_unifbase U → ∀x.(U x → (inv U) x) ∧ ((inv U) x → U x) }. (* 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)). + ∃n. ∀i,j. n ≤ i → n ≤ j → U 〈a i,a j〉. notation < "a \nbsp 'is_cauchy'" non associative with precedence 50 for @{'cauchy $a}. @@ -95,7 +109,7 @@ interpretation "Cauchy sequence" 'cauchy 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)). + ∀U.us_unifbase C U → ∃n. ∀i. n ≤ i → U 〈u,a i〉. notation < "a \nbsp (\u \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 50 for @{'uniform_converge $a $x}. @@ -112,7 +126,8 @@ 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); +cases (us_phi4 ?? Hv 〈a i,x〉) (P1 P2); apply P2; +apply (Hn ? H1); qed. (* Definition 2.17 *)