helm/software/matita/dama_didactic/ex_seq.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 set "baseuri" "cic:/matita/didactic/ex_seq".
  16
  17 include "sequences.ma".
  18
  19 (*
  20 ESERCIZI SULLE SUCCESSIONI
  21
  22 Dimostrare che la successione alpha converge a 0
  23 *)
  24
  25 definition F ≝ λ x:R.Rdiv x (S (S O)).
  26
  27 definition alpha ≝ successione F R1.
  28
  29 axiom cont: continuo F.
  30
  31 lemma l1: monotone_not_increasing alpha.
  32  we need to prove (monotone_not_increasing alpha)
  33  or equivalently (∀n:nat. alpha (S n) ≤ alpha n).
  34   assume n:nat.
  35   we need to prove (alpha (S n) ≤ alpha n)
  36   or equivalently (Rdiv (alpha n) (S (S O)) ≤ alpha n).
  37   by _ done.
  38 qed.
  39
  40 lemma l2: inf_bounded alpha.
  41  we need to prove (inf_bounded alpha)
  42  or equivalently (∃m. ∀n:nat. m ≤ alpha n).
  43   (* da trovare il modo giusto *)
  44   cut (∀n:nat.R0 ≤ alpha n).by (ex_intro ? ? R0 Hcut) done.
  45   (* fatto *)
  46   we need to prove (∀n:nat. R0 ≤ alpha n).
  47   assume n:nat.
  48   we proceed by induction on n to prove (R0 ≤ alpha n).
  49   case O.
  50     (* manca il comando
  51     the thesis becomes (R0 ≤ alpha O)
  52     or equivalently (R0 ≤ R1).
  53     by _ done. *)
  54     (* approssimiamo con questo *)
  55     we need to prove (R0 ≤ alpha O)
  56     or equivalently (R0 ≤ R1).
  57     by _ done.
  58   case S (m:nat).
  59    by induction hypothesis we know (R0 ≤ alpha m) (H).
  60    we need to prove (R0 ≤ alpha (S m))
  61    or equivalently (R0 ≤ Rdiv (alpha m) (S (S O))).
  62     by _ done.
  63 qed.
  64
  65 axiom xxx':
  66 ∀ F: R → R. ∀b:R. continuo F →
  67  ∀ l. tends_to (successione F b) l →
  68   punto_fisso F l.
  69
  70 theorem dimostrazione: tends_to alpha O.
  71  by _ let l:R such that (tends_to alpha l) (H).
  72 (* unfold alpha in H.
  73  change in match alpha in H with (successione F O).
  74  check(xxx' F cont l H).*)
  75  by (lim_punto_fisso F R1 cont l H)  we proved (punto_fisso F l) (H2)
  76  that is equivalent to (l = (Rdiv l (S (S O)))).
  77  by _ we proved (tends_to alpha l = tends_to alpha O) (H4).
  78  rewrite < H4.
  79  by _ done.
  80 qed.
  81
  82 (******************************************************************************)
  83
  84 (* Dimostrare che la successione alpha2 diverge *)
  85
  86 definition F2 ≝ λ x:R. Rmult x x.
  87
  88 definition alpha2 ≝ successione F2 (S (S O)).
  89
  90 lemma uno: ∀n. alpha2 n ≥ R1.
  91  we need to prove (∀n. alpha2 n ≥ R1).
  92  assume n:nat.
  93  we proceed by induction on n to prove (alpha2 n ≥ R1).
  94  case O.
  95    alias num (instance 0) = "natural number".
  96    we need to prove (alpha2 0 ≥ R1)
  97    or equivalently ((S (S O)) ≥ R1).
  98    by _ done.
  99  case S (m:nat).
 100    by induction hypothesis we know (alpha2 m ≥ R1) (H).
 101    we need to prove (alpha2 (S m) ≥ R1)
 102    or equivalently (Rmult (alpha2 m) (alpha2 m) ≥ R1).letin xxx := (n ≤ n);
 103    by _ we proved (R1 · R1 ≤ alpha2 m · alpha2 m) (H1).
 104    by _ we proved (R1 · R1 = R1) (H2).
 105    rewrite < H2.
 106    by _ done.
 107 qed.
 108
 109 lemma mono1: monotone_not_decreasing alpha2.
 110  we need to prove (monotone_not_decreasing alpha2)
 111  or equivalently (∀n:nat. alpha2 n ≤ alpha2 (S n)).
 112  assume n:nat.
 113  we need to prove (alpha2 n ≤ alpha2 (S n))
 114  or equivalently (alpha2 n ≤ Rmult (alpha2 n) (alpha2 n)).
 115  by _ done.
 116 qed.
 117
 118 (*
 119 lemma due: ∀n. Relev (alpha2 0) n ≥ R0.
 120  we need to prove (∀n. Relev (alpha2 0) n ≥ R0)
 121  or equivalently (∀n. Relev (S (S O)) n ≥ R0).
 122  by _ done.
 123 qed.
 124
 125 lemma tre: ∀n. alpha2 (S n) ≥ Relev (alpha2 0) (S n).
 126  we need to prove (∀n. alpha2 (S n) ≥ Relev (alpha2 0) (S n)).
 127  assume n:nat.
 128  we proceed by induction on n to prove (alpha2 (S n) ≥ Relev (alpha2 0) (S n)).
 129  case 0.
 130   we need to prove (alpha2 1 ≥ Relev (alpha2 0) R1)
 131   or equivalently (Rmult R2 R2 ≥ R2).
 132   by _ done.
 133  case S (m:nat).
 134   by induction hypothesis we know (alpha2 (S m) ≥ Relev (alpha2 0) (S m)) (H).
 135   we need to prove (alpha2 (S (S m)) ≥ Relev (alpha2 0) (S (S m)))
 136   or equivalently
 137   (*..TODO..*)
 138
 139 theorem dim2: tends_to_inf alpha2.
 140 (*..TODO..*)
 141 qed.
 142 *)
 143
 144 (******************************************************************************)
 145
 146 (* Dimostrare che la successione alpha3 converge a 0 *)
 147 (*
 148 definition alpha3 ≝ successione F2 (Rdiv (S 0) (S (S 0))).
 149
 150 lemma quattro: ∀n. alpha3 n ≤ R1.
 151  assume n:nat.
 152  we need to prove (∀n. alpha3 n ≤ R1).
 153  we proceed by induction on n to prove (alpha3 n ≤ R1).
 154  case O.
 155   we need to prove (alpha3 0 ≤ R1).
 156   by _ done.
 157  case S (m:nat).
 158   by induction hypothesis we know (alpha3 m ≤ R1) (H).
 159   we need to prove (alpha3 (S m) ≤ R1)
 160   or equivalently (Rmult (alpha3 m) (alpha3 m) ≤ R1).
 161   by _ done.
 162  qed.
 163
 164 lemma mono3: monotone_not_increasing alpha3.
 165  we need to prove (monotone_not_increasing alpha3)
 166  or equivalently (∀n:nat. alpha (S n) ≤ alpha n).
 167   assume n:nat.
 168   we need to prove (alpha (S n) ≤ alpha n)
 169   or equivalently (Rmult (alpha3 n) (alpha3 n) ≤ alpha3 n).
 170   by _ done.
 171 qed.
 172
 173 lemma bound3: inf_bounded alpha3.
 174  we need to prove (inf_bounded alpha3)
 175  or equivalently (∃m. ∀n:nat. m ≤ alpha3 n).
 176   (* da trovare il modo giusto *)
 177   cut (∀n:nat.R0 ≤ alpha3 n).by (ex_intro ? ? R0 Hcut) done.
 178   (* fatto *)
 179   we need to prove (∀n:nat. R0 ≤ alpha3 n).
 180   assume n:nat.
 181   we proceed by induction on n to prove (R0 ≤ alpha3 n).
 182   case O.
 183     (* manca il comando
 184     the thesis becomes (R0 ≤ alpha O)
 185     or equivalently (R0 ≤ R1).
 186     by _ done. *)
 187     (* approssimiamo con questo *)
 188     we need to prove (R0 ≤ alpha3 O)
 189     or equivalently (R0 ≤ Rdiv (S 0) (S (S 0))).
 190     by _ done.
 191   case S (m:nat).
 192    by induction hypothesis we know (R0 ≤ alpha3 m) (H).
 193    we need to prove (R0 ≤ alpha3 (S m))
 194    or equivalently (R0 ≤ Rmult (alpha3 m) (alpha3 m)).
 195    by _ done.
 196 qed.
 197
 198 theorem dim3: tends_to alpha3 O.
 199 (*..TODO..*)
 200 qed.
 201 *)