From 9156537d75378d7a254e93b5a2d036d687cd79ee Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 6 Jun 2008 15:56:00 +0000 Subject: [PATCH] lemma 3.6 subverted --- .../matita/contribs/dama/dama/depends | 1 + .../contribs/dama/dama/property_sigma.ma | 105 +++++++++++++++--- .../matita/contribs/dama/dama/supremum.ma | 15 ++- 3 files changed, 102 insertions(+), 19 deletions(-) diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends index c2b2004bb..b56309c6f 100644 --- a/helm/software/matita/contribs/dama/dama/depends +++ b/helm/software/matita/contribs/dama/dama/depends @@ -7,6 +7,7 @@ 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 +property_sigma.ma ordered_uniform.ma ordered_uniform.ma uniform.ma sandwich.ma ordered_uniform.ma logic/equality.ma diff --git a/helm/software/matita/contribs/dama/dama/property_sigma.ma b/helm/software/matita/contribs/dama/dama/property_sigma.ma index 7d35e086f..c67dd1785 100644 --- a/helm/software/matita/contribs/dama/dama/property_sigma.ma +++ b/helm/software/matita/contribs/dama/dama/property_sigma.ma @@ -30,31 +30,102 @@ definition max ≝ lemma le_max: ∀n,m.m ≤ max n m. intros; unfold max; apply leb_elim; simplify; intros; [assumption] apply le_n; -qed. +qed. + +lemma max_le_l: ∀n,m,z.max n m ≤ z → n ≤ z. +intros 3; unfold max; apply leb_elim; simplify; intros; [assumption] +apply lt_to_le; apply (lt_to_le_to_lt ???? H1); +apply not_le_to_lt; assumption; +qed. + +lemma sym_max: ∀n,m.max n m = max m n. +intros; apply (nat_elim2 ???? n m); simplify; intros; +[1: elim n1; [reflexivity] rewrite < H in ⊢ (? ? ? (? %)); + simplify; rewrite > H; reflexivity; +|2: reflexivity +|3: apply leb_elim; apply leb_elim; simplify; + [1: intros; apply le_to_le_to_eq; apply le_S_S;assumption; + |2,3: intros; reflexivity; + |4: intros; unfold max in H; + rewrite > (?:leb n1 m1 = false) in H; [2: + apply lt_to_leb_false; apply not_le_to_lt; assumption;] + rewrite > (?:leb m1 n1 = false) in H; [2: + apply lt_to_leb_false; apply not_le_to_lt; assumption;] + apply eq_f; assumption;]] +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. + definition hide ≝ λT:Type.λx:T.x. notation < "\blacksquare" non associative with precedence 50 for @{'hide}. interpretation "hide" 'hide = (cic:/matita/dama/property_sigma/hide.con _ _). +interpretation "hide2" 'hide = + (cic:/matita/dama/property_sigma/hide.con _ _ _). + +definition inject ≝ λP.λa:nat.λp:P a. ex_introT ? P ? p. +coercion cic:/matita/dama/property_sigma/inject.con 0 1. +definition eject ≝ λP.λc: ∃n:nat.P n. match c with [ ex_introT w _ ⇒ w]. +coercion cic:/matita/dama/property_sigma/eject.con. (* Lemma 3.6 *) lemma sigma_cauchy: - ∀O:ordered_uniform_space.property_sigma O → - ∀a:sequence O.∀l:O.a ↑ l → a is_cauchy → a uniform_converges l. + ∀C:ordered_uniform_space.property_sigma C → + ∀a:sequence C.∀l:C.a ↑ l → a is_cauchy → a uniform_converges l. intros 8; cases H1; cases H5; clear H5; cases (H ? H3); cases H5; clear H5; -letin m ≝ (? : sequence nat_ordered_set); [ - apply (hide (nat→nat)); intro i; elim i (i' Rec); - [1: apply (hide nat);cases (H2 ? (H8 0)) (k _); apply k; - |2: apply (max (hide nat ?) (S Rec)); cases (H2 ? (H8 (S i'))) (k Hk);apply k]] -cut (m 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)));] -lapply (selection ?? Hm a l H1) as H10; -lapply (H9 ?? H10) as H11; -[1: exists [apply (m 0)] intros; - apply (ous_convex ?? H3 ? H11 (H6 (m 0))); - simplify; repeat split; - - - \ No newline at end of file +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〉)); + [1,2:apply H8; + |3: intros 3; cases (H2 (w n) (H8 n)); simplify in ⊢ (? (? % ?) ?→?); + simplify in ⊢ (?→? (? % ?) ?→?); + intros; lapply (H10 i j) as H14; + [2: apply (max_le_l ??? H11);|3:apply (max_le_l ??? H12);] + cases (le_to_or_lt_eq ?? H13); [2: destruct H15; destruct H5; assumption] + generalize in match H11; generalize in match H12; + cases (aux n1); simplify in ⊢ (? (? ? %) ?→? (? ? %) ?→?); intros; + apply H16; [3: apply le_S_S_to_le; assumption] + apply lt_to_le; apply (max_le_r w1); assumption; + |4: intros; clear H11; rewrite > H5 in H10; + rewrite < (le_n_O_to_eq ? H14); apply H10; assumption;] +cut (((m : nat→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: + 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; +lapply (selection ?? Hm a l H1) as H10; +lapply (H9 ?? H10) as H11; [ + exists [apply (m 0:nat)] intros; + apply (ous_convex ?? H3 ? H11 (H6 (m 0))); + simplify; repeat split; [intro X; cases (os_coreflexive ?? X)|2,3:apply H6;] + change with (a (m O) ≤ a i); + apply (trans_increasing ?? H4); intro; whd in H12; + apply (not_le_Sn_n i); apply (transitive_le ??? H12 H5)] +clear H10; intros (p q r); change with (w p 〈a (m q),a (m r)〉); +generalize in match (refl_eq nat (m q)); +generalize in match (m q) in ⊢ (? ? ? % → %); intro X; cases X; clear X; +intros; simplify in H12:(? ? ? %); simplify in ⊢ (? ? (? ? ? % ?)); +generalize in match (refl_eq nat (m r)); +generalize in match (m r) in ⊢ (? ? ? % → %); intro X; cases X; clear X; +intros; simplify in H14:(? ? ? %); simplify in ⊢ (? ? (? ? ? ? %)); +generalize in match (refl_eq nat (m p)); +generalize in match (m p) in ⊢ (? ? ? % → %); intro X; cases X; clear X; +intros; simplify in H16:(? ? ? %); +apply H15; [3: apply le_n] destruct H16; destruct H14; destruct H12; clear H11 H13 H15; +[1: lapply (trans_increasing ?? Hm1 p q) as T; [apply not_lt_to_le; apply T;] + apply (le_to_not_lt p q H5); +|2: lapply (trans_increasing ?? Hm1 p r) as T; [apply not_lt_to_le; apply T;] + apply (le_to_not_lt p r H10);] +qed. \ No newline at end of file diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma index b2411f652..a4df77806 100644 --- a/helm/software/matita/contribs/dama/dama/supremum.ma +++ b/helm/software/matita/contribs/dama/dama/supremum.ma @@ -122,6 +122,17 @@ include "nat_ordered_set.ma". alias symbol "nleq" = "Ordered set excess". alias symbol "leq" = "Ordered set less or equal than". lemma trans_increasing: + ∀C:ordered_set.∀a:sequence C.a is_increasing → ∀n,m:nat_ordered_set. n ≤ m → a n ≤ a m. +intros 5 (C a Hs n m); elim m; [ + rewrite > (le_n_O_to_eq n (not_lt_to_le O n H)); + intro X; cases (os_coreflexive ?? X);] +cases (le_to_or_lt_eq ?? (not_lt_to_le (S n1) n H1)); clear H1; +[2: rewrite > H2; intro; cases (os_coreflexive ?? H1); +|1: apply (le_transitive ???? (H ?) (Hs ?)); + intro; whd in H1; apply (not_le_Sn_n n); apply (transitive_le ??? H2 H1);] +qed. + +lemma trans_increasing_exc: ∀C:ordered_set.∀a:sequence C.a is_increasing → ∀n,m:nat_ordered_set. m ≰ n → a n ≤ a m. intros 5 (C a Hs n m); elim m; [cases (not_le_Sn_O n H);] intro; apply H; @@ -153,12 +164,12 @@ lemma selection: ∀C:ordered_set.∀m:sequence nat_ordered_set.m is_strictly_increasing → ∀a:sequence C.∀u.a ↑ u → (λx.a (m x)) ↑ u. intros (C m Hm a u Ha); cases Ha (Ia Su); cases Su (Uu Hu); repeat split; -[1: intro n; simplify; apply trans_increasing; [assumption] apply (Hm n); +[1: intro n; simplify; apply trans_increasing_exc; [assumption] apply (Hm n); |2: intro n; simplify; apply Uu; |3: intros (y Hy); simplify; cases (Hu ? Hy); cases (strictly_increasing_reaches C ? Hm w); exists [apply w1]; cases (os_cotransitive ??? (a (m w1)) H); [2:assumption] - cases (trans_increasing C ? Ia ?? H1); assumption;] + cases (trans_increasing_exc C ? Ia ?? H1); assumption;] qed. (* Definition 2.7 *) -- 2.39.2