From bb7af347df386afcd3ea2adea8e7e982e3a5a253 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 29 Oct 2008 13:09:42 +0000 Subject: [PATCH] models ported --- .../matita/contribs/dama/dama/lebesgue.ma | 63 +++++-------------- .../models/nat_dedekind_sigma_complete.ma | 41 ++++++------ .../contribs/dama/dama/models/nat_lebesgue.ma | 8 +-- .../dama/dama/models/nat_order_continuous.ma | 12 ++-- .../dama/dama/models/nat_ordered_uniform.ma | 14 +++-- .../dama/dama/property_exhaustivity.ma | 10 ++- .../matita/contribs/dama/dama/supremum.ma | 20 ++++-- 7 files changed, 75 insertions(+), 93 deletions(-) diff --git a/helm/software/matita/contribs/dama/dama/lebesgue.ma b/helm/software/matita/contribs/dama/dama/lebesgue.ma index 1536476b0..251352d1f 100644 --- a/helm/software/matita/contribs/dama/dama/lebesgue.ma +++ b/helm/software/matita/contribs/dama/dama/lebesgue.ma @@ -23,63 +23,28 @@ lemma order_converges_bigger_lowsegment: ∀C:ordered_set. ∀a:sequence (os_l C).∀s:segment C.∀H:∀i:nat.a i ∈ s. ∀x:C.∀p:order_converge C a x. - ∀j. seg_l (os_l C) s (λl.le (os_l C) l (pi1exT23 ???? p j)). + ∀j. 𝕝_s ≤ (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; -cases (wloss_prop (os_l C))(W W);rewrite (?:s = O); [2: cases Hs; lapply (os_le_to_nat_le ?? H1); apply (symmetric_eq nat O s ?).apply (le_n_O_to_eq s ?).apply (Hletin). - |1: intros; lapply (os_le_to_nat_le (\fst (a O)) O (H2 O)); - lapply (le_n_O_to_eq ? Hletin); assumption;] + |1: intros; unfold Type_of_ordered_set in sg; + lapply (H2 O) as K; lapply (sl2l ?? (a O) ≪s,Hs≫ K) as P; + simplify in P:(???%); lapply (le_transitive ??? P H1) as W; + lapply (os_le_to_nat_le ?? W) as R; apply (le_n_O_to_eq (\fst (a O)) R);] |2: right; cases Hs; rewrite > (sym_plus s O); split; [apply le_S_S; apply le_O_n]; - apply (trans_le ??? (os_le_to_nat_le ?? H1)); + apply (trans_le ??? (os_le_to_nat_le ?? H3)); apply le_plus_n_r;] |2: clear H6; cut (s = \fst (a (aux n1))); [2: cases (le_to_or_lt_eq ?? H5); [2: assumption] @@ -72,9 +76,9 @@ letin m ≝ (hide ? ( cases H5; clear H5; cases H7; clear H7; [1: left; split; [ apply (le_S ?? H5); | assumption] |3: cases (?:False); rewrite < H8 in H6; apply (not_le_Sn_n ? H6); - |*: cases (cmp_nat u (S n1)); + |*: cases (cmp_nat 𝕦_sg (S n1)); [1,3: left; split; [1,3: assumption |2: assumption] - cut (u = S n1); [2: apply le_to_le_to_eq; assumption ] + cut (𝕦_sg = S n1); [2: apply le_to_le_to_eq; assumption ] clear H7 H5 H4;rewrite > Hcut in H8:(? ? (? % ?)); clear Hcut; cut (s = S (\fst (a w))); [2: apply le_to_le_to_eq; [2: assumption] @@ -90,7 +94,7 @@ letin m ≝ (hide ? ( [1: rewrite > sym_plus in ⊢ (? ? %); rewrite < H6; apply le_plus_r; assumption; |2: cases (H3 (a w) H6); - change with (s + S n1 ≤ u + \fst (a w1));rewrite < plus_n_Sm; + change with (s + S n1 ≤ 𝕦_sg + \fst (a w1));rewrite < plus_n_Sm; apply (trans_le ??? (le_S_S ?? H8)); rewrite > plus_n_Sm; apply (le_plus ???? (le_n ?) H9);]]]] clearbody m; unfold spec in m; clear spec; @@ -103,14 +107,14 @@ letin find ≝ ( | false ⇒ find (S i) w]] in find : - ∀i,bound.∃j.i + bound = u → s = \fst (a j)); + ∀i,bound.∃j.i + bound = 𝕦_sg → s = \fst (a j)); [1: cases (find (S n) n2); intro; change with (s = \fst (a w)); apply H6; rewrite < H7; simplify; apply plus_n_Sm; |2: intros; rewrite > (eqb_true_to_eq ?? H5); reflexivity |3: intros; rewrite > sym_plus in H5; rewrite > H5; clear H5 H4 n n1; - cases (m u); cases H4; clear H4; cases H5; clear H5; [assumption] + cases (m 𝕦_sg); cases H4; clear H4; cases H5; clear H5; [assumption] cases (not_le_Sn_n ? H4)] -clearbody find; cases (find O u); +clearbody find; cases (find O 𝕦_sg); exists [apply w]; intros; change with (s = \fst (a j)); rewrite > (H4 ?); [2: reflexivity] apply le_to_le_to_eq; @@ -121,8 +125,8 @@ apply le_to_le_to_eq; qed. lemma hint2: - ∀l,u.sequence (Type_of_ordered_set (segment_ordered_set nat_ordered_set l u)) - → sequence (hos_carr (os_r (segment_ordered_set nat_ordered_set l u))). + ∀s.sequence (Type_of_ordered_set (segment_ordered_set nat_ordered_set s)) + → sequence (hos_carr (os_r (segment_ordered_set nat_ordered_set s))). intros; assumption; qed. @@ -130,6 +134,5 @@ coercion hint2 nocomposites. alias symbol "N" = "ordered set N". axiom nat_dedekind_sigma_complete_r: - ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_decreasing → + ∀s:‡ℕ.∀a:sequence {[s]}.a is_decreasing → ∀x.x is_infimum a → ∃i.∀j.i ≤ j → \fst x = \fst (a j). - diff --git a/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.ma b/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.ma index dd1f52b72..fd1d8dbcb 100644 --- a/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.ma +++ b/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.ma @@ -16,11 +16,11 @@ include "lebesgue.ma". include "models/nat_order_continuous.ma". theorem nat_lebesgue_oc: - ∀a:sequence ℕ.∀l,u:ℕ.∀H:∀i:nat.a i ∈ [l,u]. + ∀a:sequence ℕ.∀s:‡ℕ.∀H:∀i:nat.a i ∈ s. ∀x:ℕ.a order_converges x → - x ∈ [l,u] ∧ - ∀h:x ∈ [l,u]. - uniform_converge {[l,u]} ⌊n,≪a n,H n≫⌋ ≪x,h≫. + x ∈ s ∧ + ∀h:x ∈ s. + uniform_converge {[s]} ⌊n,≪a n,H n≫⌋ ≪x,h≫. intros; apply lebesgue_oc; [apply nat_us_is_oc] assumption; qed. diff --git a/helm/software/matita/contribs/dama/dama/models/nat_order_continuous.ma b/helm/software/matita/contribs/dama/dama/models/nat_order_continuous.ma index 7949ba2d2..0b4c92e3e 100644 --- a/helm/software/matita/contribs/dama/dama/models/nat_order_continuous.ma +++ b/helm/software/matita/contribs/dama/dama/models/nat_order_continuous.ma @@ -15,20 +15,20 @@ include "models/nat_dedekind_sigma_complete.ma". include "models/nat_ordered_uniform.ma". -lemma nat_us_is_oc: ∀l,u:ℕ.order_continuity (segment_ordered_uniform_space ℕ l u). -intros 4; split; intros 3; cases H1; cases H2; clear H2 H1; cases H; clear H; -[1: cases (nat_dedekind_sigma_complete l u a H1 ? H2); +lemma nat_us_is_oc: ∀s:‡ℕ.order_continuity (segment_ordered_uniform_space ℕ s). +intros 3; split; intros 3; cases H1; cases H2; clear H2 H1; cases H; clear H; +[1: cases (nat_dedekind_sigma_complete s a H1 ? H2); exists [apply w1]; intros; - apply (restrict nat_ordered_uniform_space l u ??? H4); + apply (restrict nat_ordered_uniform_space s ??? H4); generalize in match (H ? H5); cases x; intro; generalize in match (refl_eq ? (a i):a i = a i); generalize in match (a i) in ⊢ (?? % ? → %); intro X; cases X; clear X; intro; rewrite < H9 in H7; simplify; rewrite < H7; simplify; apply (us_phi1 nat_uniform_space ? H3); simplify; apply (eq_reflexive (us_carr nat_uniform_space)); -|2: cases (nat_dedekind_sigma_complete_r l u a H1 ? H2); +|2: cases (nat_dedekind_sigma_complete_r s a H1 ? H2); exists [apply w1]; intros; - apply (restrict nat_ordered_uniform_space l u ??? H4); + apply (restrict nat_ordered_uniform_space s ??? H4); generalize in match (H ? H5); cases x; intro; generalize in match (refl_eq ? (a i):a i = a i); diff --git a/helm/software/matita/contribs/dama/dama/models/nat_ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/models/nat_ordered_uniform.ma index 82eedb35a..becbab2fb 100644 --- a/helm/software/matita/contribs/dama/dama/models/nat_ordered_uniform.ma +++ b/helm/software/matita/contribs/dama/dama/models/nat_ordered_uniform.ma @@ -18,11 +18,15 @@ include "ordered_uniform.ma". definition nat_ordered_uniform_space:ordered_uniform_space. apply (mk_ordered_uniform_space (mk_ordered_uniform_space_ ℕ ℕ (refl_eq ? ℕ))); -simplify; intros 7; cases H3; -cases H (_); cases (H8 y); apply H9; cases (H8 p); -lapply (H12 H1) as H13; apply (le_le_eq); -[1: apply (le_transitive ??? H4); apply (Le≪ ? H13); assumption; -|2: apply (le_transitive ???? H5); apply (Le≫ ? (eq_sym ??? H13)); assumption;] +simplify; intros 10; cases H (_); cases (H7 y); apply H8; cases (H7 s); +lapply (H11 H1) as H13; apply (le_le_eq); +[2: apply (le_transitive ??? H5); apply (Le≪ ? H13); assumption; +|1: assumption; +|3: change with (le (os_r ℕ) (\snd y) (\fst y)); + apply (ge_transitive ??? H5);apply (ge_transitive ???? H4); + change with (le (os_l ℕ) (\fst s) (\snd s)); + apply (Le≫ ? H13); apply le_reflexive; +|4: assumption;] qed. interpretation "Ordered uniform space N" 'N = nat_ordered_uniform_space. diff --git a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma index 9788d4d35..7145b4288 100644 --- a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma +++ b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma @@ -68,8 +68,6 @@ definition exhaustive ≝ (a is_increasing → a is_upper_located → a is_cauchy) ∧ (b is_decreasing → b is_lower_located → b is_cauchy). -STOP - lemma h_uparrow_to_in_segment: ∀C:half_ordered_set. ∀s:segment C. @@ -80,13 +78,13 @@ lemma h_uparrow_to_in_segment: intros (C H a H1 x H2); unfold in H2; cases H2; clear H2;unfold in H3 H4; cases H4; clear H4; unfold in H2; cases (wloss_prop C) (W W); apply prove_in_segment; unfold; [ apply (hle_transitive ??? x ? (H2 O)); lapply (H1 O) as K; unfold in K; rewrite "𝕦_term 90 s" non associative with precedence 45 for @{'upp $s}. -notation "𝕦 \sub term 90 s" non associative with precedence 45 for @{'upp $s}. -notation > "𝕝_term 90 s" non associative with precedence 45 for @{'low $s}. -notation "𝕝 \sub term 90 s" non associative with precedence 45 for @{'low $s}. +notation > "𝕦_term 90 s" non associative with precedence 90 for @{'upp $s}. +notation "𝕦 \sub term 90 s" non associative with precedence 90 for @{'upp $s}. +notation > "𝕝_term 90 s" non associative with precedence 90 for @{'low $s}. +notation "𝕝 \sub term 90 s" non associative with precedence 90 for @{'low $s}. definition seg_u ≝ λO:half_ordered_set.λs:segment O. @@ -340,6 +340,18 @@ whd in ⊢ (? (% ? ?) ?? ? ? ? → ?); simplify in ⊢ (% → ?); cases (wloss_prop O) (E E); do 2 rewrite < E; intros; assumption; qed. +lemma l2sl: + ∀C,s.∀x,y:half_segment_ordered_set C s. \fst x ≤≤ \fst y → x ≤≤ y. +intros; intro; apply H; apply sx2x; apply H1; +qed. + + +lemma sl2l: + ∀C,s.∀x,y:half_segment_ordered_set C s. x ≤≤ y → \fst x ≤≤ \fst y. +intros; intro; apply H; apply x2sx; apply H1; +qed. + + lemma h_segment_preserves_supremum: ∀O:half_ordered_set.∀s:segment O. ∀a:sequence (half_segment_ordered_set ? s). -- 2.39.2