helm/software/matita/contribs/dama/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 "ordered_uniform.ma".
  16
  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 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〉.
  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 definition hide ≝ λT:Type.λx:T.x.
  36
  37 notation < "\blacksquare" non associative with precedence 50 for @{'hide}.
  38 interpretation "hide" 'hide =
  39  (cic:/matita/dama/property_sigma/hide.con _ _).
  40
  41 (* Lemma 3.6 *)
  42 lemma sigma_cauchy:
  43   ∀O:ordered_uniform_space.property_sigma O →
  44     ∀a:sequence O.∀l:O.a ↑ l → a is_cauchy → a uniform_converges l.
  45 intros 8; cases H1; cases H5; clear H5;
  46 cases (H ? H3); cases H5; clear H5;
  47 letin m ≝ (? : sequence nat_ordered_set); [
  48   apply (hide (nat→nat)); intro i; elim i (i' Rec);
  49     [1: apply (hide nat);cases (H2 ? (H8 0)) (k _); apply k;
  50     |2: apply (max (hide nat ?) (S Rec)); cases (H2 ? (H8 (S i'))) (k Hk);apply k]]
  51 cut (m is_strictly_increasing) as Hm; [2:
  52   intro n; change with (S (m n) ≤ m (S n)); unfold m; whd in ⊢ (? ? %); apply (le_max ? (S (m n)));]
  53 lapply (selection ?? Hm a l H1) as H10;
  54 lapply (H9 ?? H10) as H11;
  55 [1: exists [apply (m 0)] intros;
  56     apply (ous_convex ?? H3 ? H11 (H6 (m 0)));
  57     simplify; repeat split;
  58
  59
  60