helm/software/matita/library/dama/models/increasing_supremum_stabilizes.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 "dama/models/nat_uniform.ma".
  16 include "dama/supremum.ma".
  17 include "nat/le_arith.ma".
  18 include "dama/russell_support.ma".
  19
  20 lemma hint1:
  21  ∀s.sequence (Type_of_ordered_set (segment_ordered_set nat_ordered_set s))
  22    → sequence (hos_carr (os_l (segment_ordered_set nat_ordered_set s))).
  23 intros; assumption;
  24 qed.
  25
  26 coercion hint1 nocomposites.
  27
  28 alias symbol "pi1" = "exT \fst".
  29 alias symbol "N" = "ordered set N".
  30 alias symbol "dependent_pair" = "dependent pair".
  31 lemma increasing_supremum_stabilizes:
  32   ∀sg:‡ℕ.∀a:sequence {[sg]}.
  33    a is_increasing →
  34     ∀X.X is_supremum a → ∃i.∀j.i ≤ j → \fst X = \fst (a j).
  35 intros 4; cases X (x Hx); clear X; letin X ≝ ≪x,Hx≫;
  36 fold normalize X; intros; cases H1;
  37 alias symbol "N" = "Natural numbers".
  38 letin spec ≝ (λi,j:ℕ.(𝕦_ sg ≤ i ∧ x = \fst (a j)) ∨ (i < 𝕦_ sg ∧ x + i ≤ 𝕦_ sg + \fst (a j)));
  39 (* x - aj <= max 0 (u - i) *)
  40 letin m ≝ (hide ? (
  41   let rec aux i ≝
  42     match i with
  43     [ O ⇒ O
  44     | S m ⇒
  45         let pred ≝ aux m in
  46         let apred ≝ a pred in
  47         match cmp_nat x (\fst apred) with
  48         [ cmp_le _ ⇒ pred
  49         | cmp_gt nP ⇒ \fst (H3 apred ?)]]
  50   in aux
  51    :
  52    ∀i:nat.∃j:nat.spec i j));[whd; apply nP;] unfold spec in aux ⊢ %;
  53 [3: unfold X in H2; clear H4 n aux spec H3 H1 H X;
  54     cases (cases_in_segment ??? Hx);
  55     elim 𝕦_ sg in H1 ⊢ %; intros (a Hs H);
  56     [1: left; split; [apply le_n]
  57         generalize in match H;
  58         generalize in match Hx;
  59         rewrite > (?:x = O);
  60         [2: cases Hx; lapply (os_le_to_nat_le ?? H1);
  61             apply (symmetric_eq nat O x ?).apply (le_n_O_to_eq x ?).apply (Hletin).
  62         |1: intros; unfold Type_OF_ordered_set in sg a; whd in a:(? %);
  63             lapply (H2 O) as K; lapply (sl2l_ ?? (a O) ≪x,Hx≫ K) as P;
  64             simplify in P:(???%); lapply (le_transitive ??? P H1) as W;
  65             lapply (os_le_to_nat_le ?? W) as R; apply (le_n_O_to_eq (\fst (a O)) R);]
  66     |2: right; cases Hx; rewrite > (sym_plus x O); split; [apply le_S_S; apply le_O_n];
  67         apply (trans_le ??? (os_le_to_nat_le ?? H3));
  68         apply le_plus_n_r;]
  69 |2: clear H6; cut (x = \fst (a (aux n1))); [2:
  70       cases (le_to_or_lt_eq ?? H5); [2: assumption]
  71       cases (?:False); apply (H2 (aux n1) H6);] clear H5;
  72       generalize in match Hcut; clear Hcut; intro H5;
  73 |1: clear H6]
  74 [2,1:
  75     cases (aux n1) in H5 ⊢ %; intros;
  76     change in match (a ≪w,H5≫) in H6 ⊢ % with (a w);
  77     cases H5; clear H5; cases H7; clear H7;
  78     [1: left; split; [ apply (le_S ?? H5); | assumption]
  79     |3: cases (?:False); rewrite < H8 in H6; apply (not_le_Sn_n ? H6);
  80     |*: cases (cmp_nat 𝕦_ sg (S n1));
  81         [1,3: left; split; [1,3: assumption |2: assumption]
  82             cut (𝕦_ sg = S n1); [2: apply le_to_le_to_eq; assumption ]
  83             clear H7 H5 H4;rewrite > Hcut in H8:(? ? (? % ?)); clear Hcut;
  84             cut (x = S (\fst (a w)));
  85             [2: apply le_to_le_to_eq; [2: assumption]
  86                 change in H8 with (x + n1 ≤ S (n1 + \fst (a w)));
  87                 rewrite > plus_n_Sm in H8; rewrite > sym_plus in H8;
  88                 apply (le_plus_to_le ??? H8);]
  89             cases (H3 (a w) H6);
  90             change with (x = \fst (a w1));
  91             change in H4 with (\fst (a w) < \fst (a w1));
  92             apply le_to_le_to_eq; [ rewrite > Hcut; assumption ]
  93             apply (os_le_to_nat_le (\fst (a w1)) x (H2 w1));
  94         |*: right; split; try assumption;
  95             [1: rewrite > sym_plus in ⊢ (? ? %);
  96                 rewrite < H6; apply le_plus_r; assumption;
  97             |2: cases (H3 (a w) H6);
  98                 change with (x + S n1 ≤ 𝕦_ sg + \fst (a w1));rewrite < plus_n_Sm;
  99                 apply (trans_le ??? (le_S_S ?? H8)); rewrite > plus_n_Sm;
 100                 apply (le_plus ???? (le_n ?) H9);]]]]
 101 clearbody m; unfold spec in m; clear spec;
 102 alias symbol "exists" = "CProp exists".
 103 letin find ≝ (
 104  let rec find i u on u : nat ≝
 105   match u with
 106   [ O ⇒ (m i:nat)
 107   | S w ⇒ match eqb (\fst (a (m i))) x with
 108           [ true ⇒ (m i:nat)
 109           | false ⇒ find (S i) w]]
 110  in find
 111  :
 112   ∀i,bound.∃j.i + bound = 𝕦_ sg → x = \fst (a j));
 113 [1: cases (find (S n) n2); intro; change with (x = \fst (a w));
 114     apply H6; rewrite < H7; simplify; apply plus_n_Sm;
 115 |2: intros; rewrite > (eqb_true_to_eq ?? H5); reflexivity
 116 |3: intros; rewrite > sym_plus in H5; rewrite > H5; clear H5 H4 n n1;
 117     cases (m 𝕦_ sg); cases H4; clear H4; cases H5; clear H5; [assumption]
 118     cases (not_le_Sn_n ? H4)]
 119 clearbody find; cases (find O 𝕦_ sg);
 120 exists [apply w]; intros; change with (x = \fst (a j));
 121 rewrite > (H4 ?); [2: reflexivity]
 122 apply le_to_le_to_eq;
 123 [1: apply os_le_to_nat_le;
 124     apply (trans_increasing a H ? ? (nat_le_to_os_le ?? H5));
 125 |2: apply (trans_le ? x ?);[apply os_le_to_nat_le; apply (H2 j);]
 126     rewrite < (H4 ?); [2: reflexivity] apply le_n;]
 127 qed.
 128
 129 lemma hint2:
 130  ∀s.sequence (Type_of_ordered_set (segment_ordered_set nat_ordered_set s))
 131    → sequence (hos_carr (os_r (segment_ordered_set nat_ordered_set s))).
 132 intros; assumption;
 133 qed.
 134
 135 coercion hint2 nocomposites.
 136
 137 alias symbol "N" = "ordered set N".
 138 axiom increasing_supremum_stabilizes_r:
 139   ∀s:‡ℕ.∀a:sequence {[s]}.a is_decreasing →
 140     ∀x.x is_infimum a → ∃i.∀j.i ≤ j → \fst x = \fst (a j).