]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/dama/property_sigma.ma
- oCic2NCic and nCic2OCic moved to ng_library
[helm.git] / helm / software / matita / library / dama / property_sigma.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "dama/ordered_uniform.ma".
16 include "dama/russell_support.ma".
17
18 (* Definition 3.5 *)
19 alias num (instance 0) = "natural number".
20 definition property_sigma ≝
21   λC:ordered_uniform_space.
22    ∀U.us_unifbase ? U → 
23      ∃V:sequence (C squareB → Prop).
24        (∀i.us_unifbase ? (V i)) ∧ 
25        ∀a:sequence C.∀x:C.(a ↑ x ∨ a ↓ x) → 
26          (∀n.∀i,j.n ≤ i → n ≤ j → V n 〈a i,a j〉) → U 〈a 0,x〉.
27       
28 definition max ≝
29   λm,n.match leb n m with [true ⇒ m | false ⇒ n].
30   
31 lemma le_max: ∀n,m.m ≤ max n m.
32 intros; unfold max; apply leb_elim; simplify; intros; [assumption] apply le_n;
33 qed.
34
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;
39 qed.
40
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;
45 |2: 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;]]
55 qed.
56
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); 
59 qed.
60   
61 (* Lemma 3.6 *)   
62 lemma sigma_cauchy:
63   ∀C:ordered_uniform_space.property_sigma C →
64     ∀a:sequence C.∀l:C.(a ↑ l ∨ a ↓ l) → a is_cauchy → a uniform_converges l.
65 intros 8; cases (H ? H3) (w H5); cases H5 (H8 H9); clear H5;
66 letin spec ≝ (λz,k:nat.∀i,j,l:nat.k ≤ i → k ≤ j → l ≤ z → w l 〈a i,a j〉);
67 letin m ≝ (hide ? (let rec aux (i:nat) : nat ≝
68   match i with
69   [ O ⇒ match H2 (w i) ? with [ ex_introT k _ ⇒ k ]
70   | S i' ⇒ max (match H2 (w i) ? with [ ex_introT k _ ⇒ k ]) (S (aux i'))
71   ] in aux
72   : ∀z.∃k. spec z k)); unfold spec in aux ⊢ %;
73   [1,2:apply H8;
74   |3: intros 3; cases (H2 (w n) (H8 n)); simplify in ⊢ (? (? % ?) ?→?);
75       simplify in ⊢ (?→? (? % ?) ?→?);
76       intros; lapply (H5 i j) as H14;
77         [2: apply (max_le_l ??? H6);|3:apply (max_le_l ??? H7);]
78       cases (le_to_or_lt_eq ?? H10); [2: destruct H11; destruct H4; assumption]
79       cases (aux n1) in H6 H7 ⊢ %; simplify in ⊢ (? (? ? %) ?→? (? ? %) ?→?); intros;
80       apply H6; [3: apply le_S_S_to_le; assumption]
81       apply lt_to_le; apply (max_le_r w1); assumption;
82   |4: intros; clear H6; rewrite > H4 in H5; 
83       rewrite < (le_n_O_to_eq ? H11); apply H5; assumption;] 
84 cut ((⌊x,(m x:nat)⌋ : sequence nat_ordered_set) is_strictly_increasing) as Hm; [2:
85   intro n; change with (S (m n) ≤ m (S n)); unfold m; 
86   whd in ⊢ (? ? %); apply (le_max ? (S (m n)));]
87 cut ((⌊x,(m x:nat)⌋ : sequence nat_ordered_set) is_increasing) as Hm1; [2:
88   intro n; intro L; change in L with (m (S n) < m n);
89   lapply (Hm n) as L1; change in L1 with (m n < m (S n));
90   lapply (trans_lt ??? L L1) as L3; apply (not_le_Sn_n ? L3);] 
91 clearbody m; unfold spec in m Hm Hm1; clear spec;
92 cut (⌊x,a (m x)⌋ ↑ l ∨ ⌊x,a (m x)⌋ ↓ l) as H10; [2: 
93  cases H1;
94  [ left; apply (selection_uparrow ? Hm a l H4);
95  | right; apply (selection_downarrow ? Hm a l H4);]] 
96 lapply (H9 ?? H10) as H11; [
97   exists [apply (m 0:nat)] intros;
98   cases H1; cases H5; cases H7; cases (us_phi4 ?? H3 〈l,a i〉);
99   apply H15; change with (U 〈a i,l〉);
100     [apply (ous_convex_l C ? H3 ? H11 (H12 (m O)));
101     |apply (ous_convex_r C ? H3 ? H11 (H12 (m O)));]
102   [1:apply (H12 i);
103   |3: apply (le_reflexive l);
104   |4: apply (H12 i);
105   |2:change with (a (m O) ≤ a i);
106      apply (trans_increasing a H6 (\fst (m 0)) i); intro; apply (le_to_not_lt ?? H4 H16);
107   |5:apply (H12 i);
108   |7:apply (ge_reflexive (l : hos_carr (os_r C)));
109   |8:apply (H12 i);
110   |6:change with (a i ≤ a (m O));
111      apply (trans_decreasing a H6 (\fst (m 0)) i); intro; apply (le_to_not_lt ?? H4 H16);]]  
112 clear H10; intros (p q r); change with (w p 〈a (m q),a (m r)〉);
113 generalize in match (refl_eq nat (m p)); 
114 generalize in match (m p) in ⊢ (? ? ? % → %); intro X; cases X (w1 H15); clear X; 
115 intros (H16); simplify in H16:(? ? ? %); destruct H16;
116 apply H15; [3: apply le_n]
117 [1: lapply (trans_increasing ? Hm1 p q) as T; [apply not_lt_to_le; apply T;]
118     apply (le_to_not_lt p q H4);
119 |2: lapply (trans_increasing ? Hm1 p r) as T; [apply not_lt_to_le; apply T;]
120     apply (le_to_not_lt p r H5);]
121 qed.