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 "datatypes/constructors.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); unfold 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; unfold mk_set; 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 lemma nat_dedekind_sigma_complete:
  55   ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing →
  56     ∀x.x is_supremum a → ∃i.∀j.i ≤ j → x ≈ a j.
  57 intros 5; cases x; clear x; intros;
  58 cases H2;
  59 letin m ≝ (
  60   let rec aux i ≝
  61     match i with
  62     [ O ⇒ match eqb (fst (a O)) x1 with
  63             [ true ⇒ O
  64             | false ⇒ match H4 (a O) ? with
  65                       [ ex_introT n _ ⇒ n]]
  66     | S m ⇒ let pred ≝ aux m in
  67             match eqb (fst (a pred)) x1 with
  68             [ true ⇒ pred
  69             | false ⇒ match H4 (a pred) ? with
  70                       [ ex_introT n _ ⇒ n]]]
  71    in aux
  72    :
  73    ∀i:nat.∃j.a j = x1 ∨ a i < a j);
  74
  75 cases (∀n.a n = x1 ∨ x1 ≰ a n);
  76
  77  elim x1 in H1 ⊢ % 0;
  78 [1: intro H2; letin X ≝ (sig_in ℕ (λx:ℕ.x∈[l,u]) O H2); intros;
  79     fold unfold X X in H1 ⊢ %;
  80     exists [apply O] cases H1; intros; apply le_le_eq;[2: apply H3;]
  81     intro; alias symbol "pi1" = "sigma pi1".
  82     change in H6 with (fst (a j) < O);
  83     apply (not_le_Sn_O (fst (a j))); apply H6;
  84 |2: intros 3; letin S_X ≝ (sig_in ℕ (λx:ℕ.x∈[l,u]) (S n) H2); intros;
  85     fold unfold S_X S_X in H3 ⊢ %;
  86     generalize in match (leb_to_Prop l n); elim (leb l n); simplify in H4;
  87     [1: cut (n ≤ u); [2: cases H2; normalize in H5 ⊢ %;
  88           apply le_S_S_to_le; lapply (not_lt_to_le ?? H5) as XX;
  89           apply le_S; apply XX;]
  90         cases H1; [2:split; apply nat_le_to_os_le; assumption|3:simplify;
  91
  92     elim (or_lt_le (S n) l);
  93       [ cases (?:l = S n ∨ l < S n);[
  94           unfold lt; cases H2; normalize in H5;
  95         apply (Right (eq nat n (S n)) (lt n (S n)) ?).apply (not_le_to_lt (S n) n ?).apply (not_le_Sn_n n).]
  96         [ destruct H4;
  97
  98
  99   ∀x.∃i.x ≰ a i ∨ x ≤ a i.
 100 intros; elim x;
 101
 102
 103 definition nat_uniform_space: uniform_space.
 104 apply (discrete_uniform_space_of_bishop_set ℕ);
 105 qed.
 106
 107 interpretation "Uniform space N" 'nat = nat_uniform_space.
 108
 109 include "ordered_uniform.ma".
 110
 111 definition nat_ordered_uniform_space:ordered_uniform_space.
 112 apply (mk_ordered_uniform_space (mk_ordered_uniform_space_ ℕ ℕ (refl_eq ? ℕ)));
 113 simplify; intros 7; cases H3; cases H4; cases H5; clear H5 H4;
 114 cases H (_); cases (H4 y); apply H5; clear H5 H10; cases (H4 p);
 115 lapply (H10 H1) as H11; clear H10 H5; apply (le_le_eq);
 116 [1: apply (le_transitive ???? H6); apply (Le≪ ? H11); assumption;
 117 |2: apply (le_transitive ????? H7); apply (Le≫ (snd p) H11); assumption;]
 118 qed.
 119
 120 interpretation "Uniform space N" 'nat = nat_ordered_uniform_space.
 121
 122 lemma nat_us_is_oc: ∀l,u:ℕ.order_continuity {[l,u]}.
 123 intros 4; split; intros 3; cases H; cases H3; clear H3 H;
 124 cases (H5 (a i));
 125 cases (H10 (sig_in ?? x1 H2));
 126
 127 exists [1,3:apply x1]
 128 intros; apply H6;