1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ordered_uniform.ma".
19 alias num (instance 0) = "natural number".
20 definition property_sigma ≝
21 λC:ordered_uniform_space.
23 ∃V:sequence (C square → Prop).
24 (∀i.us_unifbase ? (V i)) ∧
25 ∀a:sequence C.∀x:C.a ↑ x →
26 (∀n.∀i,j.n ≤ i → n ≤ j → V n 〈a i,a j〉) → U 〈a 0,x〉.
29 λm,n.match leb n m with [true ⇒ m | false ⇒ n].
31 lemma le_max: ∀n,m.m ≤ max n m.
32 intros; unfold max; apply leb_elim; simplify; intros; [assumption] apply le_n;
35 lemma max_le_l: ∀n,m,z.max n m ≤ z → n ≤ z.
36 intros 3; unfold max; apply leb_elim; simplify; intros; [assumption]
37 apply lt_to_le; apply (lt_to_le_to_lt ???? H1);
38 apply not_le_to_lt; assumption;
41 lemma sym_max: ∀n,m.max n m = max m n.
42 intros; apply (nat_elim2 ???? n m); simplify; intros;
43 [1: elim n1; [reflexivity] rewrite < H in ⊢ (? ? ? (? %));
44 simplify; rewrite > H; reflexivity;
46 |3: apply leb_elim; apply leb_elim; simplify;
47 [1: intros; apply le_to_le_to_eq; apply le_S_S;assumption;
48 |2,3: intros; reflexivity;
49 |4: intros; unfold max in H;
50 rewrite > (?:leb n1 m1 = false) in H; [2:
51 apply lt_to_leb_false; apply not_le_to_lt; assumption;]
52 rewrite > (?:leb m1 n1 = false) in H; [2:
53 apply lt_to_leb_false; apply not_le_to_lt; assumption;]
54 apply eq_f; assumption;]]
57 lemma max_le_r: ∀n,m,z.max n m ≤ z → m ≤ z.
58 intros; rewrite > sym_max in H; apply (max_le_l ??? H);
62 definition hide ≝ λT:Type.λx:T.x.
64 notation < "\blacksquare" non associative with precedence 50 for @{'hide}.
65 interpretation "hide" 'hide =
66 (cic:/matita/dama/property_sigma/hide.con _ _).
67 interpretation "hide2" 'hide =
68 (cic:/matita/dama/property_sigma/hide.con _ _ _).
70 definition inject ≝ λP.λa:nat.λp:P a. ex_introT ? P ? p.
71 coercion cic:/matita/dama/property_sigma/inject.con 0 1.
72 definition eject ≝ λP.λc: ∃n:nat.P n. match c with [ ex_introT w _ ⇒ w].
73 coercion cic:/matita/dama/property_sigma/eject.con.
77 ∀C:ordered_uniform_space.property_sigma C →
78 ∀a:sequence C.∀l:C.a ↑ l → a is_cauchy → a uniform_converges l.
79 intros 8; cases H1; cases H5; clear H5;
80 cases (H ? H3); cases H5; clear H5;
81 letin m ≝ (hide ? (let rec aux (i:nat) : nat ≝
83 [ O ⇒ match H2 (w i) ? with [ ex_introT k _ ⇒ k ]
84 | S i' ⇒ max (match H2 (w i) ? with [ ex_introT k _ ⇒ k ]) (S (aux i'))
87 ∀z:nat.∃k:nat.∀i,j,l.k ≤ i → k ≤ j → l ≤ z → w l 〈a i, a j〉));
89 |3: intros 3; cases (H2 (w n) (H8 n)); simplify in ⊢ (? (? % ?) ?→?);
90 simplify in ⊢ (?→? (? % ?) ?→?);
91 intros; lapply (H10 i j) as H14;
92 [2: apply (max_le_l ??? H11);|3:apply (max_le_l ??? H12);]
93 cases (le_to_or_lt_eq ?? H13); [2: destruct H15; destruct H5; assumption]
94 generalize in match H11; generalize in match H12;
95 cases (aux n1); simplify in ⊢ (? (? ? %) ?→? (? ? %) ?→?); intros;
96 apply H16; [3: apply le_S_S_to_le; assumption]
97 apply lt_to_le; apply (max_le_r w1); assumption;
98 |4: intros; clear H11; rewrite > H5 in H10;
99 rewrite < (le_n_O_to_eq ? H14); apply H10; assumption;]
100 cut (((m : nat→nat) : sequence nat_ordered_set) is_strictly_increasing) as Hm; [2:
101 intro n; change with (S (m n) ≤ m (S n)); unfold m;
102 whd in ⊢ (? ? %); apply (le_max ? (S (m n)));]
103 cut (((m : nat→nat) : sequence nat_ordered_set) is_increasing) as Hm1; [2:
104 intro n; intro L; change in L with (m (S n) < m n);
105 lapply (Hm n) as L1; change in L1 with (m n < m (S n));
106 lapply (trans_lt ??? L L1) as L3; apply (not_le_Sn_n ? L3);]
108 lapply (selection ?? Hm a l H1) as H10;
109 lapply (H9 ?? H10) as H11; [
110 exists [apply (m 0:nat)] intros;
111 apply (ous_convex ?? H3 ? H11 (H6 (m 0)));
112 simplify; repeat split; [intro X; cases (os_coreflexive ?? X)|2,3:apply H6;]
113 change with (a (m O) ≤ a i);
114 apply (trans_increasing ?? H4); intro; whd in H12;
115 apply (not_le_Sn_n i); apply (transitive_le ??? H12 H5)]
116 clear H10; intros (p q r); change with (w p 〈a (m q),a (m r)〉);
117 generalize in match (refl_eq nat (m p));
118 generalize in match (m p) in ⊢ (? ? ? % → %); intro X; cases X (w1 H15); clear X;
119 intros (H16); simplify in H16:(? ? ? %); destruct H16;
120 apply H15; [3: apply le_n]
121 [1: lapply (trans_increasing ?? Hm1 p q) as T; [apply not_lt_to_le; apply T;]
122 apply (le_to_not_lt p q H5);
123 |2: lapply (trans_increasing ?? Hm1 p r) as T; [apply not_lt_to_le; apply T;]
124 apply (le_to_not_lt p r H10);]