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 ∨ 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 definition hide ≝ λT:Type.λx:T.x.
  62
  63 notation < "\blacksquare" non associative with precedence 50 for @{'hide}.
  64 interpretation "hide" 'hide = (hide _ _).
  65 interpretation "hide2" 'hide = (hide _ _ _).
  66
  67 definition inject ≝ λP.λa:nat.λp:P a. ex_introT ? P ? p.
  68 coercion cic:/matita/dama/property_sigma/inject.con 0 1.
  69 definition eject ≝ λP.λc: ∃n:nat.P n. match c with [ ex_introT w _ ⇒ w].
  70 coercion cic:/matita/dama/property_sigma/eject.con.
  71
  72 (* Lemma 3.6 *)
  73 lemma sigma_cauchy:
  74   ∀C:ordered_uniform_space.property_sigma C →
  75     ∀a:sequence C.∀l:C.(a ↑ l ∨ a ↓ l) → a is_cauchy → a uniform_converges l.
  76 intros 8; cases (H ? H3) (w H5); cases H5 (H8 H9); clear H5;
  77 letin m ≝ (hide ? (let rec aux (i:nat) : nat ≝
  78   match i with
  79   [ O ⇒ match H2 (w i) ? with [ ex_introT k _ ⇒ k ]
  80   | S i' ⇒ max (match H2 (w i) ? with [ ex_introT k _ ⇒ k ]) (S (aux i'))
  81   ] in aux
  82   :
  83   ∀z:nat.∃k:nat.∀i,j,l.k ≤ i → k ≤ j → l ≤ z → w l 〈a i, a j〉));
  84   [1,2:apply H8;
  85   |3: intros 3; cases (H2 (w n) (H8 n)); simplify in ⊢ (? (? % ?) ?→?);
  86       simplify in ⊢ (?→? (? % ?) ?→?);
  87       intros; lapply (H5 i j) as H14;
  88         [2: apply (max_le_l ??? H6);|3:apply (max_le_l ??? H7);]
  89       cases (le_to_or_lt_eq ?? H10); [2: destruct H11; destruct H4; assumption]
  90       generalize in match H6; generalize in match H7;
  91       cases (aux n1); simplify in ⊢ (? (? ? %) ?→? (? ? %) ?→?); intros;
  92       apply H12; [3: apply le_S_S_to_le; assumption]
  93       apply lt_to_le; apply (max_le_r w1); assumption;
  94   |4: intros; clear H6; rewrite > H4 in H5;
  95       rewrite < (le_n_O_to_eq ? H11); apply H5; assumption;]
  96 cut (((m : nat→nat) : sequence nat_ordered_set) is_strictly_increasing) as Hm; [2:
  97   intro n; change with (S (m n) ≤ m (S n)); unfold m;
  98   whd in ⊢ (? ? %); apply (le_max ? (S (m n)));]
  99 cut (((m : nat→nat) : sequence nat_ordered_set) is_increasing) as Hm1; [2:
 100   intro n; intro L; change in L with (m (S n) < m n);
 101   lapply (Hm n) as L1; change in L1 with (m n < m (S n));
 102   lapply (trans_lt ??? L L1) as L3; apply (not_le_Sn_n ? L3);]
 103 clearbody m;
 104 cut ((λx:nat.a (m x))↑ l ∨ (λx:nat.a (m x)) ↓ l) as H10; [2:
 105  cases H1;
 106  [ left; apply (selection_uparrow ?? Hm a l H4);
 107  | right; apply (selection_downarrow ?? Hm a l H4);]]
 108 lapply (H9 ?? H10) as H11; [
 109   exists [apply (m 0:nat)] intros;
 110   cases H1;
 111     [cases H5; cases H7; apply (ous_convex ?? H3 ? H11 (H12 (m O)));
 112     |cases H5; cases H7; cases (us_phi4 ?? H3 〈(a (m O)),l〉);
 113      lapply (H14 H11) as H11'; apply (ous_convex ?? H3 〈l,(a (m O))〉 H11' (H12 (m O)));]
 114   simplify; repeat split; [1,6:intro X; cases (os_coreflexive ?? X)|*: try apply H12;]
 115   [1:change with (a (m O) ≤ a i);
 116      apply (trans_increasing ?? H6); intro; apply (le_to_not_lt ?? H4 H14);
 117   |2:change with (a i ≤ a (m O));
 118      apply (trans_decreasing ?? H6); intro; apply (le_to_not_lt ?? H4 H16);]]
 119 clear H10; intros (p q r); change with (w p 〈a (m q),a (m r)〉);
 120 generalize in match (refl_eq nat (m p));
 121 generalize in match (m p) in ⊢ (? ? ? % → %); intro X; cases X (w1 H15); clear X;
 122 intros (H16); simplify in H16:(? ? ? %); destruct H16;
 123 apply H15; [3: apply le_n]
 124 [1: lapply (trans_increasing ?? Hm1 p q) as T; [apply not_lt_to_le; apply T;]
 125     apply (le_to_not_lt p q H4);
 126 |2: lapply (trans_increasing ?? Hm1 p r) as T; [apply not_lt_to_le; apply T;]
 127     apply (le_to_not_lt p r H5);]
 128 qed.