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