helm/software/matita/contribs/dama/dama/models/uniformnat.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 "nat_ordered_set.ma".
  16 include "bishop_set_rewrite.ma".
  17 include "uniform.ma".
  18
  19 definition discrete_uniform_space_of_bishop_set:bishop_set → uniform_space.
  20 intro C; apply (mk_uniform_space C);
  21 [1: intro; apply (∃_:unit.∀n:C square.(fst n ≈ snd n → P n) ∧ (P n → fst n ≈ snd n));
  22 |2: intros 4 (U H x Hx); simplify in Hx;
  23     cases H (_ H1); cases (H1 x); apply H2; apply Hx;
  24 |3: intros; cases H (_ PU); cases H1 (_ PV);
  25     exists[apply (λx.U x ∧ V x)] split;
  26     [1: exists[apply something] intro; cases (PU n); cases (PV n);
  27         split; intros; try split;[apply H2;|apply H4] try assumption;
  28         apply H3; cases H6; assumption;
  29     |2: simplify; intros; assumption;]
  30 |4: intros; cases H (_ PU); exists [apply U] split;
  31     [1: exists [apply something] intro n; cases (PU n);
  32         split; intros; try split;[apply H1;|apply H2] assumption;
  33     |2: intros 2 (x Hx); cases Hx; cases H1; clear H1;
  34         cases (PU 〈(fst x),x1〉); lapply (H4 H2) as H5; simplify in H5;
  35         cases (PU 〈x1,(snd x)〉); lapply (H7 H3) as H8; simplify in H8;
  36         generalize in match H5; generalize in match H8;
  37         generalize in match (PU x); clear H6 H7 H1 H4 H2 H3 H5 H8;
  38         cases x; simplify; intros; cases H1; clear H1; apply H4;
  39         apply (eq_trans ???? H3 H2);]
  40 |5: intros; cases H (_ H1); split; cases x;
  41     [2: cases (H1 〈b,b1〉); intro; apply H2; cases (H1 〈b1,b〉);
  42         lapply (H6 H4) as H7; apply eq_sym; apply H7;
  43     |1: cases (H1 〈b1,b〉); intro; apply H2; cases (H1 〈b,b1〉);
  44         lapply (H6 H4) as H7; apply eq_sym; apply H7;]]
  45 qed.
  46
  47
  48 notation "\naturals" non associative with precedence 99 for @{'nat}.
  49
  50 interpretation "naturals" 'nat = nat.
  51 interpretation "Ordered set N" 'nat = nat_ordered_set.
  52
  53 include "russell_support.ma".
  54
  55 inductive cmp_cases (n,m:nat) : CProp ≝
  56   | cmp_lt : n < m → cmp_cases n m
  57   | cmp_eq : n = m → cmp_cases n m
  58   | cmp_gt : m < n → cmp_cases n m.
  59
  60 lemma cmp_nat: ∀n,m.cmp_cases n m.
  61 intros;
  62 simplify; intros; generalize in match (nat_compare_to_Prop n m);
  63 cases (nat_compare n m); intros;
  64 [constructor 1|constructor 2|constructor 3]
  65 assumption;
  66 qed.
  67
  68 lemma trans_le_lt_lt:
  69   ∀n,m,o:nat.n≤m→m<o→n<o.
  70 intros; apply (trans_le ? (S m)); [apply le_S_S;apply H;|apply H1]
  71 qed.
  72
  73 alias symbol "lt" (instance 2) = "ordered sets less than".
  74 lemma key:
  75  ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing → ∀n,m. a n < a m → n < m.
  76 intros; cases (cmp_nat n m);
  77 [assumption
  78 |generalize in match H1; rewrite < H2; intros;
  79  cases (not_lt_n_n (fst (a n))); apply os_lt_to_nat_lt; apply H3;
  80 |cases (not_lt_n_n (fst (a m)));
  81  apply (trans_le_lt_lt ? (fst (a n)));
  82  [2: apply os_lt_to_nat_lt; apply H1;
  83  |1: apply os_le_to_nat_le; apply (trans_increasing ?? H m n);
  84      apply nat_le_to_os_le; apply le_S_S_to_le; apply le_S; apply H2]]
  85 qed.
  86
  87 lemma le_lt_transitive:
  88  ∀O:ordered_set.∀a,b,c:O.a≤b→b<c→a<c.
  89 intros;
  90 split;
  91 [1: apply (le_transitive ???? H); cases H1; assumption;
  92 |2: cases H1; cases (bs_cotransitive ??? a H3); [2:assumption]
  93     cut (a<b);[2: split; [assumption] apply bs_symmetric; assumption]
  94     cut (a<c);[2: apply (lt_transitive ???? Hcut H1);]
  95     cases Hcut1; assumption]
  96 qed.
  97
  98 alias symbol "pi1" = "exT fst".
  99 lemma nat_dedekind_sigma_complete:
 100   ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing →
 101     ∀x.x is_supremum a → ∃i.∀j.i ≤ j → fst x = fst (a j).
 102 intros 5; cases x (s Hs); clear x; letin X ≝ (〈s,Hs〉);
 103 fold normalize X; intros; cases H1;
 104 letin spec ≝ (λi,j.fst (a j) = s ∨ (i ≤ j ∧ match i with [ O ⇒ fst (a j) = fst (a O) | S m ⇒ fst(a m) < fst (a j)]));
 105 letin m ≝ (
 106   let rec aux i ≝
 107     match i with
 108     [ O ⇒ O
 109     | S m ⇒
 110         let pred ≝ aux m in
 111         let apred ≝ a pred in
 112         match cmp_nat (fst apred) s with
 113         [ cmp_eq _ ⇒ pred
 114         | cmp_gt nP ⇒ match ? in False return λ_.nat with []
 115         | cmp_lt nP ⇒ fst (H3 apred nP)]]
 116   in aux
 117    :
 118    ∀i:nat.∃j:nat.spec i j);unfold spec in aux ⊢ %;
 119 [1: apply (H2 pred nP);
 120 |4: right; split; whd; constructor 1;
 121 |2,3: whd in ⊢ (? ? %);
 122   [1: left; assumption
 123   |2: elim (H3 (a (aux n1)) H5) (res_n);
 124       change with (fst (a res_n) = s ∨ (n1 < res_n ∧ fst (a n1) < fst (a res_n)));
 125       change in H7 with (fst (a (aux n1)) < fst (a res_n));
 126       elim (aux n1) in H7 ⊢ % (pred);
 127       change in H8 with (fst (a pred) < fst (a res_n));
 128       cases H7; clear H7;
 129       [ left; apply le_to_le_to_eq;
 130         [ apply os_le_to_nat_le; apply (H2 res_n);
 131         | rewrite < H9; apply le_S_S_to_le; apply le_S; apply H8;]
 132       | cases H9; clear H9; right; split;
 133         [ lapply (trans_increasing ?? H n1 pred (nat_le_to_os_le ?? H7)) as H11;
 134           clear H6; apply (key ??? H);
 135           apply (le_lt_transitive ?? (a pred)); [assumption]
 136           generalize in match H8; cases (a pred); cases (a res_n);
 137           simplify; intro D; lapply (nat_lt_to_os_lt ?? D) as Q;
 138           cases Q; clear D Q; split; assumption;
 139         | generalize in match H10; generalize in match H7; clear H7 H10;
 140           cases n1; intros;
 141           [ rewrite < H9; assumption
 142           | clear H9; apply (trans_le_lt_lt ??? ? H8);
 143             apply os_le_to_nat_le; lapply (nat_le_to_os_le ?? H7) as H77;
 144             apply(trans_increasing ?? H (S n2) (pred) H77);]]]]]
 145 clearbody m; unfold spec in m; clear spec;
 146 cut (∀i.fst (a (m i)) = s ∨ i ≤ fst (a (m i))) as key2;[
 147 letin find ≝ (
 148  let rec find i u on u : nat ≝
 149   match u with
 150   [ O ⇒ (m i:nat)
 151   | S w ⇒ match eqb (fst (a (m i))) s with
 152           [ true ⇒ (m i:nat)
 153           | false ⇒ find (S i) w]]
 154  in find
 155  :
 156   ∀i,bound.∃j.i + bound = u → s = fst (a j));
 157 [1: cases (find (S n) n2); intro; change with (s = fst (a w));
 158     apply H6; rewrite < H7; simplify; apply plus_n_Sm;
 159 |2: intros; rewrite > (eqb_true_to_eq ?? H5); reflexivity
 160 |3: intros; rewrite > sym_plus in H5; rewrite > H5; clear H5 H4 n n1;
 161     cases (key2 u); [symmetry;assumption]
 162     cases Hs; apply le_to_le_to_eq;[2:change with (fst (a (m u)) ≤ fst X); apply os_le_to_nat_le; apply (H2 (m u));]
 163     apply (trans_le ??? (os_le_to_nat_le ?? H5) H4);
 164 |4: clearbody find; cases (find O u);
 165     exists [apply w]; intros; change with (s = fst (a j));
 166     rewrite > (H4 ?); [2: reflexivity]
 167     apply le_to_le_to_eq; [apply os_le_to_nat_le;
 168       apply (trans_increasing ?? H ? ? (nat_le_to_os_le ?? H5));]
 169     apply (trans_le ? s ?);[apply os_le_to_nat_le; apply (H2 j);]
 170     rewrite < (H4 ?); [2: reflexivity] apply le_n;]]
 171 alias symbol "pi1" (instance 15) = "exT fst".
 172 alias symbol "pi1" (instance 10) = "exT fst".
 173 alias symbol "pi1" (instance 7) = "exT fst".
 174 alias symbol "pi1" (instance 4) = "exT fst".
 175 alias symbol "nat" = "naturals".
 176 cut (∀i.fst (a (fst (m i))) = s
 177         ∨
 178         i ≤ fst (m i)
 179         ∧
 180         match i in nat return λn:ℕ.Prop with
 181         [O⇒ fst (a (fst(m i))) = fst (a O)
 182         |S (w:ℕ)⇒fst (a w) < fst (a (fst(m i)))]) as mitico;[2:
 183  intro; cases (m i); apply H4;]
 184 cut (∀i.fst (a (m i)) = s ∨ fst (a (m i)) < fst (a (m (S i))));[2:
 185   intro;
 186   cases (mitico (S i));
 187     [2: cases (mitico i);
 188           [2: cases H5 (H6 _); cases H4 (_ H7); clear H4 H5;
 189               change in H7 with (fst (a i) < fst (a (fst (m (S i)))));
 190               right;
 191
 192
 193   generalize in match (mitico i); clear mitico;
 194
 195
 196   cases (m i); intros; cases H5; clear H5;
 197   [left; assumption]
 198   cases H6; clear H6; simplify in H7;
 199
 200    change with (fst (a w)=s ∨ a w<a (m (S i)));
 201   cases H4; [left; assumption]
 202   cases H5; clear H4 H5;
 203   cases (m (S i)); change with (fst (a w)=s ∨ a w<a w1);
 204   m i = w
 205   m Si = w1
 206
 207
 208
 209    elim i;
 210   [1: cases (m (S O)); change with (fst (a (m O))=s∨a (m O)<a w);
 211   |2: cases (m (S (S n))); change with (fst (a (m (S n)))=s∨a (m (S n))<a w);
 212
 213       cases H4; clear H4;
 214       [1: right; split;
 215           [change with (le nat_ordered_set (fst (a (m O))) (fst (a w)));
 216            rewrite > H5; apply (H2 (m O));
 217           |
 218       |2: cases H5; clear H5; change in H6 with (fst (a O) < fst (a w));
 219           right; split;  [change with (le nat_ordered_set (fst (a (m O))) (fst (a w)));
 220           apply nat_le_to_os_le; apply le_S_S_to_le; apply le_S;
 221           (* apply H6; *)
 222           |]]
 223
 224
 225
 226       cases (m O); change with (fst (a w) = s ∨ a w < a (m (S O)));
 227       cases H4[left; assumption] cases H5; clear H4 H5;
 228       change in H7 with (fst (a w) = fst (a O));
 229
 230
 231 intro; elim i; [1: right; apply le_O_n;]
 232 generalize in match (refl_eq ? (S n):S n = S n);
 233 generalize in match (S n) in ⊢ (? ? ? % → %); intro R;
 234 cases (m R); intros; change with (fst (a w) = s ∨ R ≤ fst (a w));
 235 rewrite < H6 in H5 ⊢ %; clear H6 R; cases H5; [left; assumption]
 236 cases H6; clear H6 H5; change in H8 with (fst (a n) < fst (a w));
 237 lapply (key l u a H n w);
 238
 239 w = m (S n)
 240
 241
 242
 243 STOP
 244
 245
 246 letin m ≝ (
 247   let rec aux i ≝
 248     match i with
 249     [ O ⇒
 250         let a0 ≝ a O in
 251         match cmp_nat (fst a0) s with
 252         [ cmp_eq _ ⇒ O
 253         | cmp_gt nP ⇒ match ? in False return λ_.nat with []
 254         | cmp_lt nP ⇒ fst (H3 a0 nP)]
 255     | S m ⇒
 256         let pred ≝ aux m in
 257         let apred ≝ a pred in
 258         match cmp_nat (fst apred) s with
 259         [ cmp_eq _ ⇒ pred
 260         | cmp_gt nP ⇒ match ? in False return λ_.nat with []
 261         | cmp_lt nP ⇒
 262
 263                       fst (H3 apred nP)]]
 264   in aux
 265    :
 266    ∀i:nat.∃j:nat.spec i j);unfold spec in aux ⊢ %;
 267 [1: apply (H2 O nP);
 268 |2: apply (H2 pred nP);
 269 |5: left; assumption;
 270 |6: right; cases (H3 (a O) H5); change with (fst (a O) < fst (a w));
 271     apply H7;
 272 |4: right; elim (H3 (a (aux n1)) H5); change with (fst (a (S n1)) < fst (a a1));
 273     rewrite < H4; elim (aux n1) in H7 ⊢ %; elim H7 in H8; clear H7;
 274     simplify in H9;
 275
 276 |3: clear H6; generalize in match H5; cases (aux n1); intros; clear H5;
 277     simplify
 278
 279
 280 STOP
 281
 282
 283 definition nat_uniform_space: uniform_space.
 284 apply (discrete_uniform_space_of_bishop_set ℕ);
 285 qed.
 286
 287 interpretation "Uniform space N" 'nat = nat_uniform_space.
 288
 289 include "ordered_uniform.ma".
 290
 291 definition nat_ordered_uniform_space:ordered_uniform_space.
 292 apply (mk_ordered_uniform_space (mk_ordered_uniform_space_ ℕ ℕ (refl_eq ? ℕ)));
 293 simplify; intros 7; cases H3; cases H4; cases H5; clear H5 H4;
 294 cases H (_); cases (H4 y); apply H5; clear H5 H10; cases (H4 p);
 295 lapply (H10 H1) as H11; clear H10 H5; apply (le_le_eq);
 296 [1: apply (le_transitive ???? H6); apply (Le≪ ? H11); assumption;
 297 |2: apply (le_transitive ????? H7); apply (Le≫ (snd p) H11); assumption;]
 298 qed.
 299
 300 interpretation "Uniform space N" 'nat = nat_ordered_uniform_space.
 301
 302 lemma nat_us_is_oc: ∀l,u:ℕ.order_continuity {[l,u]}.
 303 intros 4; split; intros 3; cases H; cases H3; clear H3 H;
 304 cases (H5 (a i));
 305 cases (H10 (sig_in ?? x1 H2));
 306
 307 exists [1,3:apply x1]
 308 intros; apply H6;