X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fproperty_exhaustivity.ma;h=0e0f013e988ec9758afba613b1a8d6493928e80c;hb=c33fae30b4ce40198b8e1889ea1c1b58697cd567;hp=cf3a5b0574cfe099fd04f79cb29f62ef087cb416;hpb=5070f476ff80ee53fe444d284f9e7587a37022f4;p=helm.git diff --git a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma index cf3a5b057..0e0f013e9 100644 --- a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma +++ b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma @@ -15,92 +15,194 @@ include "ordered_uniform.ma". include "property_sigma.ma". -(* Definition 3.7 *) -definition exhaustive â - λC:ordered_uniform_space. - âa,b:sequence C. - (a is_increasing â a is_upper_located â a is_cauchy) ⧠- (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)). -intros 5; change with (fst (a n) ⤠u); cases (a n); cases H; assumption; +lemma h_segment_upperbound: + âC:half_ordered_set. + âs:segment C. + âa:sequence (half_segment_ordered_set C s). + (seg_u C s) (upper_bound ? ân,\fst (a n)â). +intros; cases (wloss_prop C); unfold; rewrite < H; simplify; intro n; +cases (a n); simplify; unfold in H1; rewrite < H in H1; cases H1; +simplify in H2 H3; rewrite < H in H2 H3; assumption; qed. -lemma segment_lowerbound: - â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. +notation "'segment_upperbound'" non associative with precedence 90 for @{'segment_upperbound}. +notation "'segment_lowerbound'" non associative with precedence 90 for @{'segment_lowerbound}. -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). -intros; cases H (Ha Hx); split [apply Ha] cases Hx; -split; [apply H1] intros; -cases (H2 (fst y) H3); exists [apply w] assumption; -qed. +interpretation "segment_upperbound" 'segment_upperbound = (h_segment_upperbound (os_l _)). +interpretation "segment_lowerbound" 'segment_lowerbound = (h_segment_upperbound (os_r _)). -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). -intros; cases H (Ha Hx); split [apply Ha] cases Hx; -split; [apply H1] intros; -cases (H2 (fst y) H3); exists [apply w] assumption; +lemma h_segment_preserves_uparrow: + âC:half_ordered_set.âs:segment C.âa:sequence (half_segment_ordered_set C s). + âx,h. uparrow C ân,\fst (a n)â x â uparrow (half_segment_ordered_set C s) a âªx,hâ«. +intros; cases H (Ha Hx); split; +[ intro n; intro H; apply (Ha n); apply (sx2x ???? H); +| cases Hx; split; + [ intro n; intro H; apply (H1 n);apply (sx2x ???? H); + | intros; cases (H2 (\fst y)); [2: apply (sx2x ???? H3);] + exists [apply w] apply (x2sx ?? (a w) y H4);]] qed. - + +notation "'segment_preserves_uparrow'" non associative with precedence 90 for @{'segment_preserves_uparrow}. +notation "'segment_preserves_downarrow'" non associative with precedence 90 for @{'segment_preserves_downarrow}. + +interpretation "segment_preserves_uparrow" 'segment_preserves_uparrow = (h_segment_preserves_uparrow (os_l _)). +interpretation "segment_preserves_downarrow" 'segment_preserves_downarrow = (h_segment_preserves_uparrow (os_r _)). + (* 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. -intros 7; + âC:ordered_uniform_space.âs:â¡C.âa:sequence {[s]}. + a is_cauchy â ân,\fst (a n)â is_cauchy. +intros 6; alias symbol "pi1" (instance 3) = "pair pi1". -apply (H (λx:{[l,u]} square.U â©fst (fst x),fst (snd x)âª)); +alias symbol "pi2" = "pair pi2". +apply (H (λx:{[s]} squareB.U â©\fst (\fst x),\fst (\snd x)âª)); (unfold segment_ordered_uniform_space; simplify); exists [apply U] split; [assumption;] intro; cases b; intros; simplify; split; intros; assumption; qed. -(* Lemma 3.8 *) +(* Definition 3.7 *) +definition exhaustive â + λC:ordered_uniform_space. + âa,b:sequence C. + (a is_increasing â a is_upper_located â a is_cauchy) ⧠+ (b is_decreasing â b is_lower_located â b is_cauchy). + +lemma prove_in_segment: + âO:ordered_set.âs:segment (os_l O).âx:O. + ð_s (λl.l ⤠x) â ð¦_s (λu.x ⤠u) â x â s. +intros; unfold; cases (wloss_prop (os_l O)); rewrite < H2; +split; assumption; +qed. + +lemma under_wloss_upperbound: + âC:half_ordered_set.âs:segment C.âa:sequence C. + seg_u C s (upper_bound C a) â + âi.seg_u C s (λu.a i â¤â¤ u). +intros; unfold in H; unfold; +cases (wloss_prop C); rewrite