From 6d27950e804ea499909ae0fabceea99f35d118e9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 20 Oct 2008 10:18:10 +0000 Subject: [PATCH] after a PITA, lebergue is dualized! --- .../matita/contribs/dama/dama/lebesgue.ma | 18 +-- .../contribs/dama/dama/models/q_bars.ma | 129 +++--------------- .../contribs/dama/dama/models/q_copy.ma | 47 ++++++- .../contribs/dama/dama/models/q_rebase.ma | 8 +- .../contribs/dama/dama/ordered_uniform.ma | 80 ++++++----- .../dama/dama/property_exhaustivity.ma | 63 ++++++--- .../contribs/dama/dama/property_sigma.ma | 25 ++-- .../matita/contribs/dama/dama/sandwich.ma | 6 +- 8 files changed, 185 insertions(+), 191 deletions(-) diff --git a/helm/software/matita/contribs/dama/dama/lebesgue.ma b/helm/software/matita/contribs/dama/dama/lebesgue.ma index 5740db8de..2e6b0a1e4 100644 --- a/helm/software/matita/contribs/dama/dama/lebesgue.ma +++ b/helm/software/matita/contribs/dama/dama/lebesgue.ma @@ -24,7 +24,7 @@ lemma order_converges_bigger_lowsegment: 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; -intro H2; cases (SSa ? H2) (w Hw); simplify in Hw; +intro H2; cases (SSa l H2) (w Hw); simplify in Hw; cases (H (w+j)) (Hal Hau); apply (Hau Hw); qed. @@ -54,16 +54,16 @@ generalize in match (order_converges_smaller_upsegment ???? H1 ? H2); cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ (% → % → ?); intros; cut (∀i.xi i ∈ [l,u]) as Hxi; [2: intros; split; [2:apply H3] cases (Hxy i) (H5 _); cases H5 (H7 _); - apply (le_transitive ???? (H7 0)); simplify; + apply (ge_transitive u ??? (H7 0)); simplify; cases (H1 i); assumption;] clear H3; cut (∀i.yi i ∈ [l,u]) as Hyi; [2: intros; split; [apply H2] cases (Hxy i) (_ H5); cases H5 (H7 _); - apply (le_transitive ????? (H7 0)); simplify; + apply (le_transitive l ? (yi i) ? (H7 0)); simplify; cases (H1 i); assumption;] clear H2; split; [1: cases Hx; cases H3; cases Hy; cases H7; split; - [1: apply (le_transitive ???? (H8 0)); cases (Hyi 0); assumption - |2: apply (le_transitive ????? (H4 0)); cases (Hxi 0); assumption] + [1: apply (ge_transitive u ?? ? (H8 0)); cases (Hyi 0); assumption + |2: apply (le_transitive l ? x ? (H4 0)); cases (Hxi 0); assumption] |2: intros 3 (h); letin Xi ≝ (⌊n,≪xi n, Hxi n≫⌋); letin Yi ≝ (⌊n,≪yi n, Hyi n≫⌋); @@ -95,11 +95,11 @@ generalize in match (order_converges_smaller_upsegment ???? H1 ? H2); cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ (% → % → ?); intros; cut (∀i.xi i ∈ [l,u]) as Hxi; [2: intros; split; [2:apply H3] cases (Hxy i) (H5 _); cases H5 (H7 _); - apply (le_transitive ???? (H7 0)); simplify; + apply (ge_transitive u ?? ? (H7 0)); simplify; cases (H1 i); assumption;] clear H3; cut (∀i.yi i ∈ [l,u]) as Hyi; [2: intros; split; [apply H2] cases (Hxy i) (_ H5); cases H5 (H7 _); - apply (le_transitive ????? (H7 0)); simplify; + apply (le_transitive l ? (yi i) ? (H7 0)); simplify; cases (H1 i); assumption;] clear H2; letin Xi ≝ (⌊n,≪xi n, Hxi n≫⌋); letin Yi ≝ (⌊n,≪yi n, Hyi n≫⌋); @@ -107,8 +107,8 @@ cases (restrict_uniform_convergence_uparrow ? S ?? (H l u) Xi x Hx); cases (restrict_uniform_convergence_downarrow ? S ?? (H l u) Yi x Hy); split; [1: assumption] intros 3; -lapply (uparrow_upperlocated ? xi x Hx)as Ux; -lapply (downarrow_lowerlocated ? yi x Hy)as Uy; +lapply (uparrow_upperlocated xi x Hx)as Ux; +lapply (downarrow_lowerlocated yi x Hy)as Uy; letin Ai ≝ (⌊n,≪a n, H1 n≫⌋); apply (sandwich {[l,u]} ≪?, h≫ Xi Yi Ai); [4: assumption;|2:apply H3;|3:apply H5] intro j; cases (Hxy j); cases H7; cases H8; split; [apply (H9 0);|apply (H11 0)] diff --git a/helm/software/matita/contribs/dama/dama/models/q_bars.ma b/helm/software/matita/contribs/dama/dama/models/q_bars.ma index 79cc540a8..1d2107b7c 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_bars.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_bars.ma @@ -87,6 +87,15 @@ coinductive value_spec (f : list bar) (i : ℚ) : ℚ × ℚ → CProp ≝ nth_height f j = q → nth_base f j < i → j < \len f → (∀n.n H6; - rewrite < H1; simplify; rewrite > nth_len; unfold P; + rewrite < H1; simplify; rewrite > nth_len; unfold match_pred; cases (q_cmp (Qpos i) (\fst x)); simplify; intros (X Hs); [2: destruct X] clear X; cases (sorted_pivot q2_lt ??? ▭ Hs); @@ -129,7 +136,7 @@ apply (value_of ?? (pred (find ? P f ▭))); repeat rewrite < plus_n_Sm; rewrite < plus_n_O; simplify; rewrite > sym_plus; rewrite < minus_plus_m_m; reflexivity;] rewrite > len_append; rewrite > H1; simplify; rewrite < plus_n_SO; - apply le_S_S; clear H1 H6 H7 Hs H8 H9 Hn x l2 l1 H4 H3 H2 H P; + apply le_S_S; clear H1 H6 H7 Hs H8 H9 Hn x l2 l1 H4 H3 H2 H; elim (\len f) in i1 n H5; [cases (not_le_Sn_O ? H);] simplify; cases n2; [ repeat rewrite < minus_n_O; apply le_S_S_to_le; assumption] cases n1 in H1; [intros; rewrite > eq_minus_n_m_O; apply le_O_n] @@ -140,18 +147,18 @@ apply (value_of ?? (pred (find ? P f ▭))); |2: cases (not_le_Sn_n i1); rewrite > H in ⊢ (??%); apply (trans_le ??? ? H4); cases i1 in H3; intros; apply le_S_S; [ apply le_O_n; | assumption]] -|3: cases (cases_find bar P f ▭); [ +|3: unfold match_domain; cases (cases_find bar (match_pred i) f ▭); [ cases i1 in H; intros; simplify; [assumption] apply lt_S_to_lt; assumption;] rewrite > H; cases (\len f) in len_bases_gt_O_f; intros; [cases (not_le_Sn_O ? H3)] simplify; apply le_n; -|4: intros; cases (cases_find bar P f ▭) in H; simplify; intros; +|4: intros; unfold match_domain in H; cases (cases_find bar (match_pred i) f ▭) in H; simplify; intros; [1: lapply (H3 n); [2: cases i1 in H4; intros [assumption] apply le_S; assumption;] - unfold P in Hletin; cases (q_cmp (Qpos i) (\fst (\nth f ▭ n))) in Hletin; + unfold match_pred in Hletin; cases (q_cmp (Qpos i) (\fst (\nth f ▭ n))) in Hletin; simplify; intros; [destruct H6] assumption; |2: destruct H; cases f in len_bases_gt_O_f H2 H3; clear H1; simplify; intros; [cases (not_le_Sn_O ? H)] lapply (H1 n); [2: apply le_S; assumption] - unfold P in Hletin; cases (q_cmp (Qpos i) (\fst (\nth (b::l) ▭ n))) in Hletin; + unfold match_pred in Hletin; cases (q_cmp (Qpos i) (\fst (\nth (b::l) ▭ n))) in Hletin; simplify; intros; [destruct H4] assumption;]] qed. @@ -167,107 +174,13 @@ intros; cases (value_lemma (bars q) ?? r); | apply bars_begin_lt_Qpos;] qed. -alias symbol "lt" (instance 5) = "natural 'less than'". -alias symbol "lt" (instance 4) = "Q less than". -lemma value_simpl: - ∀f:list bar.sorted q2_lt f → O < (length bar f) → - ∀i:ratio.nth_base f O < Qpos i → ℚ × ℚ. -intros; cases (value_lemma f H H1 i H2); assumption; -qed. - lemma cases_value : ∀f,i. value_spec (bars f) (Qpos i) (value f i). intros; unfold value; cases (value_lemma (bars f) (bars_sorted f) (len_bases_gt_O f) i (bars_begin_lt_Qpos f i)); assumption; qed. -lemma cases_value_simpl : - ∀f,H1,H2,i,Hi.value_spec f (Qpos i) (value_simpl f H1 H2 i Hi). -intros; unfold value_simpl; cases (value_lemma f H1 H2 i Hi); -assumption; -qed. - definition same_values ≝ λl1,l2:q_f.∀input. value l1 input = value l2 input. -definition same_values_simpl ≝ - λl1,l2:list bar.∀H1,H2,H3,H4,input,Hi1,Hi2. - value_simpl l1 H1 H2 input Hi1 = value_simpl l2 H3 H4 input Hi2. - -lemma value_head : - ∀x,y,l,H1,H2,i,H3. - Qpos i ≤ \fst x → value_simpl (y::x::l) H1 H2 i H3 = \snd y. -intros; cases (cases_value_simpl ? H1 H2 i H3); -cases j in H4 H5 H6 H7 H8 (j); simplify; intros; -[1: symmetry; assumption; -|2: cases (?:False); cases j in H4 H5 H6 H7 H8; intros; - [1: lapply (q_le_lt_trans ??? H H5) as K;cases (q_lt_corefl ? K); - |2: lapply (H7 1); [2: do 2 apply le_S_S; apply le_O_n;] - simplify in Hletin; - lapply (q_le_lt_trans ??? H Hletin) as K;cases (q_lt_corefl ? K);]] -qed. - -lemma same_values_simpl_to_same_values: - ∀b1,b2,Hs1,Hs2,Hb1,Hb2,He1,He2,input. - same_values_simpl b1 b2 → - value (mk_q_f b1 Hs1 Hb1 He1) input = - value (mk_q_f b2 Hs2 Hb2 He2) input. -intros; -lapply (len_bases_gt_O (mk_q_f b1 Hs1 Hb1 He1)); -lapply (len_bases_gt_O (mk_q_f b2 Hs2 Hb2 He2)); -lapply (H ???? input) as K; try assumption; -[2: rewrite > Hb1; apply q_pos_OQ; -|3: rewrite > Hb2; apply q_pos_OQ; -|1: apply K;] -qed. - -include "russell_support.ma". - -lemma value_tail : - ∀x,y,l,H1,H2,i,H3. - \fst x < Qpos i → - value_simpl (y::x::l) H1 H2 i H3 = - value_simpl (x::l) ?? i ?. -[1: apply hide; apply (sorted_tail q2_lt); [apply y| assumption] -|2: apply hide; simplify; apply le_S_S; apply le_O_n; -|3: apply hide; assumption;] -intros;cases (cases_value_simpl ? H1 H2 i H3); -generalize in ⊢ (? ? ? (? ? % ? ? ?)); intro; -generalize in ⊢ (? ? ? (? ? ? % ? ?)); intro; -generalize in ⊢ (? ? ? (? ? ? ? ? %)); intro; -cases (cases_value_simpl (x::l) H9 H10 i H11); -cut (j = S j1) as E; [ destruct E; destruct H12; reflexivity;] -clear H12 H4; cases j in H8 H5 H6 H7; -[1: intros;cases (?:False); lapply (H7 1 (le_n ?)); [2: simplify; do 2 apply le_S_S; apply le_O_n] - simplify in Hletin; apply (q_lt_corefl (\fst x)); - apply (q_lt_le_trans ??? H Hletin); -|2: simplify; intros; clear q q1 j H11 H10 H1 H2; simplify in H3 H14; apply eq_f; - cases (cmp_nat n j1); [cases (cmp_nat j1 n);[apply le_to_le_to_eq; assumption]] - [1: clear H1; cases (?:False); - lapply (H7 (S j1)); [2: cases j1 in H2; intros[cases (not_le_Sn_O ? H1)] apply le_S_S; assumption] - [2: apply le_S_S; assumption;] simplify in Hletin; - apply (q_lt_corefl ? (q_le_lt_trans ??? Hletin H13)); - |2: cases (?:False); - lapply (H16 n); [2: assumption|3:simplify; apply le_S_S_to_le; assumption] - apply (q_lt_corefl ? (q_le_lt_trans ??? Hletin H4));]] -qed. - -lemma value_unit: - ∀x,i,h1,h2,h3.value_simpl [x] h1 h2 i h3 = \snd x. -intros; cases (cases_value_simpl [x] h1 h2 i h3); cases j in H H2; simplify; -intros; [2: cases (?:False); apply (not_le_Sn_O n); apply le_S_S_to_le; apply H2] -symmetry; assumption; -qed. - -lemma same_value_tail: - ∀b,b1,h1,h3,xs,r1,input,H12,H13,Hi1,H14,H15,Hi2. - same_values_simpl (〈b1,h1〉::xs) (〈b1,h3〉::r1) → - value_simpl (b::〈b1,h1〉::xs) H12 H13 input Hi1 - =value_simpl (b::〈b1,h3〉::r1) H14 H15 input Hi2. -intros; cases (q_cmp (Qpos input) b1); -[1: rewrite > (value_head 〈b1,h1〉 b xs); [2:assumption] - rewrite > (value_head 〈b1,h3〉 b r1); [2:assumption] reflexivity; -|2: rewrite > (value_tail 〈b1,h1〉 b xs);[2: assumption] - rewrite > (value_tail 〈b1,h3〉 b r1);[2: assumption] apply H;] -qed. definition same_bases ≝ λl1,l2:list bar. ∀i.\fst (\nth l1 ▭ i) = \fst (\nth l2 ▭ i). diff --git a/helm/software/matita/contribs/dama/dama/models/q_copy.ma b/helm/software/matita/contribs/dama/dama/models/q_copy.ma index 00788cd16..de7384077 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_copy.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_copy.ma @@ -93,13 +93,50 @@ lapply (sorted_tail q2_lt ?? H) as K; clear H; cases l in H1 K; simplify; intros [apply (sorted_one q2_lt);|apply (sorted_cons q2_lt);[2: assumption] apply H] qed. +lemma value_head : ∀a,l,i.Qpos i ≤ \fst a → value_simple (a::l) i = \snd a. +intros; unfold value_simple; unfold match_domain; cases (cases_find bar (match_pred i) (a::l) ▭); +[1: cases i1 in H2 H3 H4; intros; [reflexivity] lapply (H4 O) as K; [2: apply le_S_S; apply le_O_n;] + simplify in K; unfold match_pred in K; cases (q_cmp (Qpos i) (\fst a)) in K; + simplify; intros; [destruct H6] lapply (q_le_lt_trans ??? H H5) as K; cases (q_lt_corefl ? K); +|2: cases (?:False); lapply (H3 0); [2: simplify; apply le_S_S; apply le_O_n;] + unfold match_pred in Hletin; simplify in Hletin; cases (q_cmp (Qpos i) (\fst a)) in Hletin; + simplify; intros; [destruct H5] lapply (q_le_lt_trans ??? H H4); apply (q_lt_corefl ? Hletin);] +qed. + +lemma value_unit : ∀x,i. value_simple [x] i = \snd x. +intros; unfold value_simple; unfold match_domain; +cases (cases_find bar (match_pred i) [x] ▭); +[1: cases i1 in H; intros; [reflexivity] simplify in H; + cases (not_le_Sn_O ? (le_S_S_to_le ?? H)); +|2: simplify in H; destruct H; reflexivity;] +qed. +lemma value_tail : + ∀a,b,l,i.\fst a < Qpos i → \fst b ≤ Qpos i → value_simple (a::b::l) i = value_simple (b::l) i. +intros; unfold value_simple; unfold match_domain; +cases (cases_find bar (match_pred i) (a::b::l) ▭); +[1: cases i1 in H3 H2 H4 H5; intros 1; simplify in ⊢ (? ? (? ? %) ?→?); unfold in ⊢ (? ? % ?→?); intros; + [1: cases (?:False); cases (q_cmp (Qpos i) (\fst a)) in H3; simplify; intros;[2: destruct H6] + apply (q_lt_corefl ? (q_lt_le_trans ??? H H3)); + |2: + +normalize in ⊢ (? ? % ?→?); simplify; +[1: rewrite > (value_head); + lemma value_copy : - ∀l,h1,h2,i,h3. - value_simpl (copy l) h1 h2 i h3 = 〈OQ,OQ〉. -intros; elim l in h1 h2 h3; [cases (not_le_Sn_O ? H1);] -cases l1 in H H1 H2 H3; -[1: intros; simplify in ⊢ (? ? (? % ? ? ? ?) ?); + ∀l,i.rewrite > (value_u + value_simple (copy l) i = 〈OQ,OQ〉. +intros; elim l; +[1: reflexivity; +|2: cases l1 in H; intros; simplify in ⊢ (? ? (? % ?) ?); + [1: rewrite > (value_unit); reflexivity; + |2: cases (q_cmp (\fst b) (Qpos i)); + + change with (\fst ▭ = \lamsimplify in ⊢ (? ? (? % ?) ?); unfold value_simple; unfold match_domain; + cases (cases_find bar (match_pred i) [〈\fst x,〈OQ,OQ〉〉] ▭); + [1: simplify in H1:(??%%); + + unfold match_pred; rewrite > (value_unit 〈\fst a,〈OQ,OQ〉〉); reflexivity; |2: intros; simplify in H2 H3 H4 ⊢ (? ? (? % ? ? ? ?) ?); cases (q_cmp (Qpos i) (\fst b)); diff --git a/helm/software/matita/contribs/dama/dama/models/q_rebase.ma b/helm/software/matita/contribs/dama/dama/models/q_rebase.ma index c521e6bbd..f8243d6d1 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_rebase.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_rebase.ma @@ -14,7 +14,7 @@ include "russell_support.ma". include "models/q_copy.ma". - +(* definition rebase_spec ≝ λl1,l2:q_f.λp:q_f × q_f. And3 @@ -88,9 +88,13 @@ intros 6; cases H; simplify; intros; clear H; whd; rewrite < H6; apply (inversion_sorted2 ??? H5); | apply (sorted_one q2_lt);] qed. +*) + + definition rebase_spec_aux ≝ - λl1,l2:list bar.λp:(list bar) × (list bar). + λl1,l2 + :list bar.λp:(list bar) × (list bar). sorted q2_lt l1 → (\snd (\last ▭ l1) = 〈OQ,OQ〉) → sorted q2_lt l2 → (\snd (\last ▭ l2) = 〈OQ,OQ〉) → rebase_spec_aux_p l1 l2 p. diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma index e724dc2e6..8cca24c90 100644 --- a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma +++ b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma @@ -36,20 +36,7 @@ record ordered_uniform_space : Type ≝ { ous_stuff :> ordered_uniform_space_; ous_convex: ∀U.us_unifbase ous_stuff U → convex ous_stuff U }. -(* -definition Type_of_ordered_uniform_space : ordered_uniform_space → Type. -intro; compose ordered_set_OF_ordered_uniform_space with os_l. -apply (hos_carr (f o)); -qed. - -definition Type_of_ordered_uniform_space_dual : ordered_uniform_space → Type. -intro; compose ordered_set_OF_ordered_uniform_space with os_r. -apply (hos_carr (f o)); -qed. -coercion Type_of_ordered_uniform_space_dual. -coercion Type_of_ordered_uniform_space. -*) definition half_ordered_set_OF_ordered_uniform_space : ordered_uniform_space → half_ordered_set. intro; compose ordered_set_OF_ordered_uniform_space with os_l. apply (f o); qed. @@ -114,24 +101,6 @@ lemma bs2_of_bss2: coercion bs2_of_bss2 nocomposites. -(* -notation < "x \sub \neq" with precedence 91 for @{'bsss $x}. -interpretation "bs_of_ss" 'bsss x = (bs_of_ss _ _ _ x). -*) - -(* -lemma ss_of_bs: - ∀O:ordered_set.∀u,v:O. - ∀b:O squareO.\fst b ∈ [u,v] → \snd b ∈ [u,v] → {[u,v]} squareO ≝ - λO:ordered_set.λu,v:O. - λb:O squareB.λH1,H2.〈≪\fst b,H1≫,≪\snd b,H2≫〉. -*) - -(* -notation < "x \sub \nleq" 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; @@ -185,16 +154,57 @@ interpretation "Ordered uniform space segment" 'segment_set a b = alias symbol "pi1" = "exT \fst". lemma restric_uniform_convergence: ∀O:ordered_uniform_space.∀l,u:O. - ∀x:(segment_ordered_uniform_space O l u). - ∀a:sequence (segment_ordered_uniform_space O l u). - uniform_converge (segment_ordered_uniform_space O l u) - (mk_seq O (λn:nat.\fst (a n))) (\fst x) → True. + ∀x:{[l,u]}. + ∀a:sequence {[l,u]}. + (⌊n, \fst (a n)⌋ : sequence O) 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; apply (restrict ? l u ??? H4); apply (Hm ? H1); qed. +definition hint_sequence: + ∀C:ordered_set. + sequence (hos_carr (os_l C)) → sequence (Type_of_ordered_set C). +intros;assumption; +qed. + +definition hint_sequence1: + ∀C:ordered_set. + sequence (hos_carr (os_r C)) → sequence (Type_of_ordered_set_dual C). +intros;assumption; +qed. + +definition hint_sequence2: + ∀C:ordered_set. + sequence (Type_of_ordered_set C) → sequence (hos_carr (os_l C)). +intros;assumption; +qed. + +definition hint_sequence3: + ∀C:ordered_set. + sequence (Type_of_ordered_set_dual C) → sequence (hos_carr (os_r C)). +intros;assumption; +qed. + +coercion hint_sequence nocomposites. +coercion hint_sequence1 nocomposites. +coercion hint_sequence2 nocomposites. +coercion hint_sequence3 nocomposites. + definition order_continuity ≝ λC:ordered_uniform_space.∀a:sequence C.∀x:C. (a ↑ x → a uniform_converges x) ∧ (a ↓ x → a uniform_converges x). + +lemma hint_boh1: ∀O. Type_OF_ordered_uniform_space O → hos_carr (os_l O). +intros; assumption; +qed. + +coercion hint_boh1 nocomposites. + +lemma hint_boh2: ∀O:ordered_uniform_space. hos_carr (os_l O) → Type_OF_ordered_uniform_space O. +intros; assumption; +qed. + +coercion hint_boh2 nocomposites. + diff --git a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma index f7250f9e2..96170fa26 100644 --- a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma +++ b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma @@ -55,13 +55,13 @@ lemma segment_cauchy: intros 7; alias symbol "pi1" (instance 3) = "pair pi1". alias symbol "pi2" = "pair pi2". -apply (H (λx:{[l,u]} square.U 〈\fst (\fst x),\fst (\snd x)〉)); +apply (H (λx:{[l,u]} 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 *) +(* Lemma 3.8 NON DUALIZZATO *) lemma restrict_uniform_convergence_uparrow: ∀C:ordered_uniform_space.property_sigma C → ∀l,u:C.exhaustive {[l,u]} → @@ -69,39 +69,66 @@ lemma restrict_uniform_convergence_uparrow: 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); + [1: apply (supremum_is_upper_bound ? x Hx u); apply (segment_upperbound ? l); - |2: apply (le_transitive ? ??? ? (H2 O)); - apply (segment_lowerbound ?l u);] + |2: apply (le_transitive l ? x ? (H2 O)); + apply (segment_lowerbound ? l u a 0);] |2: intros; - lapply (uparrow_upperlocated ? a ≪x,h≫) as Ha1; - [2: apply segment_preserves_uparrow;split; assumption;] - lapply (segment_preserves_supremum ? l u a ≪?,h≫) as Ha2; + lapply (uparrow_upperlocated a ≪x,h≫) as Ha1; + [2: apply (segment_preserves_uparrow C l u);split; assumption;] + 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; lapply (sigma_cauchy ? H ? x ? Ha); [left; split; assumption] apply restric_uniform_convergence; assumption;] qed. - -lemma restrict_uniform_convergence_downarrow: + +lemma hint_mah1: + ∀C. Type_OF_ordered_uniform_space1 C → hos_carr (os_r C). + intros; assumption; qed. + +coercion hint_mah1 nocomposites. + +lemma hint_mah2: + ∀C. sequence (hos_carr (os_l C)) → sequence (hos_carr (os_r C)). + intros; assumption; qed. + +coercion hint_mah2 nocomposites. + +lemma hint_mah3: + ∀C. Type_OF_ordered_uniform_space C → hos_carr (os_r C). + intros; assumption; qed. + +coercion hint_mah3 nocomposites. + +lemma hint_mah4: + ∀C. sequence (hos_carr (os_r C)) → sequence (hos_carr (os_l C)). + intros; assumption; qed. + +coercion hint_mah4 nocomposites. + +axiom 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 → + ∀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); + [2: apply (infimum_is_lower_bound ? x Hx l); apply (segment_lowerbound ? l u); - |1: apply (le_transitive ???? (H2 O)); - apply (segment_upperbound ? l u);] + |1: lapply (ge_transitive ? ? x ? (H2 O)); [apply u||assumption] + apply (segment_upperbound ? l u a 0);] |2: intros; - lapply (downarrow_lowerlocated ? a ≪x,h≫) as Ha1; - [2: apply segment_preserves_downarrow;split; assumption;] - lapply (segment_preserves_infimum ?l u a ≪?,h≫) as Ha2; + lapply (downarrow_lowerlocated a ≪x,h≫) as Ha1; + [2: apply (segment_preserves_downarrow ? l u);split; assumption;] + lapply (segment_preserves_infimum l u); + [2: apply 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; lapply (sigma_cauchy ? H ? x ? Ha); [right; split; assumption] apply restric_uniform_convergence; assumption;] -qed. \ No newline at end of file +qed. +*) \ No newline at end of file diff --git a/helm/software/matita/contribs/dama/dama/property_sigma.ma b/helm/software/matita/contribs/dama/dama/property_sigma.ma index 241882bdd..9d9485f9c 100644 --- a/helm/software/matita/contribs/dama/dama/property_sigma.ma +++ b/helm/software/matita/contribs/dama/dama/property_sigma.ma @@ -20,7 +20,7 @@ alias num (instance 0) = "natural number". definition property_sigma ≝ λC:ordered_uniform_space. ∀U.us_unifbase ? U → - ∃V:sequence (C square → Prop). + ∃V:sequence (C squareB → Prop). (∀i.us_unifbase ? (V i)) ∧ ∀a:sequence C.∀x:C.(a ↑ x ∨ a ↓ x) → (∀n.∀i,j.n ≤ i → n ≤ j → V n 〈a i,a j〉) → U 〈a 0,x〉. @@ -57,7 +57,7 @@ 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 → @@ -91,26 +91,29 @@ cut ((⌊x,(m x:nat)⌋ : sequence nat_ordered_set) is_increasing) as Hm1; [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);]] + [ left; apply (selection_uparrow ? Hm a l H4); + | right; apply (selection_downarrow ? Hm a l H4);]] lapply (H9 ?? H10) as H11; [ exists [apply (m 0:nat)] intros; cases H1; [cases H5; cases H7; apply (ous_convex ?? H3 ? H11 (H12 (m O))); |cases H5; cases H7; cases (us_phi4 ?? H3 〈(a (m O)),l〉); lapply (H14 H11) as H11'; apply (ous_convex ?? H3 〈l,(a (m O))〉 H11' (H12 (m O)));] - simplify; repeat split; [1,6:intro X; cases (os_coreflexive ?? X)|*: try apply H12;] - [1:change with (a (m O) ≤ a i); - apply (trans_increasing ?? H6); intro; apply (le_to_not_lt ?? H4 H14); - |2:change with (a i ≤ a (m O)); - apply (trans_decreasing ?? H6); intro; apply (le_to_not_lt ?? H4 H16);]] + simplify; repeat split; + [1,6: apply (le_reflexive l); + |2,5: apply (H12 (\fst (m 0))); + |3,8: apply (H12 i); + |4:change with (a (m O) ≤ a i); + apply (trans_increasing a H6 (\fst (m 0)) i); intro; apply (le_to_not_lt ?? H4 H14); + |7:change with (a i ≤ a (m O)); + apply (trans_decreasing ? H6 (\fst (m 0)) i); intro; apply (le_to_not_lt ?? H4 H16);]] clear H10; intros (p q r); change with (w p 〈a (m q),a (m r)〉); generalize in match (refl_eq nat (m p)); generalize in match (m p) in ⊢ (? ? ? % → %); intro X; cases X (w1 H15); clear X; intros (H16); simplify in H16:(? ? ? %); destruct H16; apply H15; [3: apply le_n] -[1: lapply (trans_increasing ?? Hm1 p q) as T; [apply not_lt_to_le; apply T;] +[1: lapply (trans_increasing ? Hm1 p q) as T; [apply not_lt_to_le; apply T;] apply (le_to_not_lt p q H4); -|2: lapply (trans_increasing ?? Hm1 p r) as T; [apply not_lt_to_le; apply T;] +|2: lapply (trans_increasing ? Hm1 p r) as T; [apply not_lt_to_le; apply T;] apply (le_to_not_lt p r H5);] qed. diff --git a/helm/software/matita/contribs/dama/dama/sandwich.ma b/helm/software/matita/contribs/dama/dama/sandwich.ma index abccb351b..e55b6d3b3 100644 --- a/helm/software/matita/contribs/dama/dama/sandwich.ma +++ b/helm/software/matita/contribs/dama/dama/sandwich.ma @@ -38,10 +38,10 @@ unfold; simplify; exists [apply (a i)] 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); + |2: simplify; apply (le_transitive (a i) ?? Lax Lxb); |3: simplify; repeat split; try assumption; - [1: apply (le_transitive ???? Lax Lxb); - |2: intro X; cases (os_coreflexive ?? X)]] + [1: apply (le_transitive ?? (b i) Lax Lxb); + |2: intro X; cases (exc_coreflexive (a i) 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;]] -- 2.39.2