matita/contribs/dama/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
  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   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     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     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  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 (* end auto($Revision: 8612 $) proof: TIME=0.01 SIZE=100 DEPTH=100 *)
  76  using (lim_punto_fisso F R1 cont l H)  we proved (punto_fisso F l) (H2)
  77  that is equivalent to (l = (Rdiv l (S (S O)))).
  78  we proved (tends_to alpha l = tends_to alpha O) (H4).
  79  rewrite < H4.
  80  done.
  81 qed.
  82
  83 (******************************************************************************)
  84
  85 (* Dimostrare che la successione alpha2 diverge *)
  86
  87 definition F2 ≝ λ x:R. Rmult x x.
  88
  89 definition alpha2 ≝ successione F2 (S (S O)).
  90
  91 lemma uno: ∀n. alpha2 n ≥ R1.
  92  we need to prove (∀n. alpha2 n ≥ R1).
  93  assume n:nat.
  94  we proceed by induction on n to prove (alpha2 n ≥ R1).
  95  case O.
  96    alias num (instance 0) = "natural number".
  97    we need to prove (alpha2 0 ≥ R1)
  98    or equivalently ((S (S O)) ≥ R1).
  99    done.
 100  case S (m:nat).
 101    by induction hypothesis we know (alpha2 m ≥ R1) (H).
 102    we need to prove (alpha2 (S m) ≥ R1)
 103    or equivalently (Rmult (alpha2 m) (alpha2 m) ≥ R1).letin xxx := (n ≤ n);
 104    we proved (R1 · R1 ≤ alpha2 m · alpha2 m) (H1).
 105    we proved (R1 · R1 = R1) (H2).
 106    rewrite < H2.
 107    done.
 108 qed.
 109
 110 lemma mono1: monotone_not_decreasing alpha2.
 111  we need to prove (monotone_not_decreasing alpha2)
 112  or equivalently (∀n:nat. alpha2 n ≤ alpha2 (S n)).
 113  assume n:nat.
 114  we need to prove (alpha2 n ≤ alpha2 (S n))
 115  or equivalently (alpha2 n ≤ Rmult (alpha2 n) (alpha2 n)).
 116  done.
 117 qed.
 118
 119 (*
 120 lemma due: ∀n. Relev (alpha2 0) n ≥ R0.
 121  we need to prove (∀n. Relev (alpha2 0) n ≥ R0)
 122  or equivalently (∀n. Relev (S (S O)) n ≥ R0).
 123  by _ done.
 124 qed.
 125
 126 lemma tre: ∀n. alpha2 (S n) ≥ Relev (alpha2 0) (S n).
 127  we need to prove (∀n. alpha2 (S n) ≥ Relev (alpha2 0) (S n)).
 128  assume n:nat.
 129  we proceed by induction on n to prove (alpha2 (S n) ≥ Relev (alpha2 0) (S n)).
 130  case 0.
 131   we need to prove (alpha2 1 ≥ Relev (alpha2 0) R1)
 132   or equivalently (Rmult R2 R2 ≥ R2).
 133   by _ done.
 134  case S (m:nat).
 135   by induction hypothesis we know (alpha2 (S m) ≥ Relev (alpha2 0) (S m)) (H).
 136   we need to prove (alpha2 (S (S m)) ≥ Relev (alpha2 0) (S (S m)))
 137   or equivalently
 138   (*..TODO..*)
 139
 140 theorem dim2: tends_to_inf alpha2.
 141 (*..TODO..*)
 142 qed.
 143 *)
 144
 145 (******************************************************************************)
 146
 147 (* Dimostrare che la successione alpha3 converge a 0 *)
 148 (*
 149 definition alpha3 ≝ successione F2 (Rdiv (S 0) (S (S 0))).
 150
 151 lemma quattro: ∀n. alpha3 n ≤ R1.
 152  assume n:nat.
 153  we need to prove (∀n. alpha3 n ≤ R1).
 154  we proceed by induction on n to prove (alpha3 n ≤ R1).
 155  case O.
 156   we need to prove (alpha3 0 ≤ R1).
 157   by _ done.
 158  case S (m:nat).
 159   by induction hypothesis we know (alpha3 m ≤ R1) (H).
 160   we need to prove (alpha3 (S m) ≤ R1)
 161   or equivalently (Rmult (alpha3 m) (alpha3 m) ≤ R1).
 162   by _ done.
 163  qed.
 164
 165 lemma mono3: monotone_not_increasing alpha3.
 166  we need to prove (monotone_not_increasing alpha3)
 167  or equivalently (∀n:nat. alpha (S n) ≤ alpha n).
 168   assume n:nat.
 169   we need to prove (alpha (S n) ≤ alpha n)
 170   or equivalently (Rmult (alpha3 n) (alpha3 n) ≤ alpha3 n).
 171   by _ done.
 172 qed.
 173
 174 lemma bound3: inf_bounded alpha3.
 175  we need to prove (inf_bounded alpha3)
 176  or equivalently (∃m. ∀n:nat. m ≤ alpha3 n).
 177   (* da trovare il modo giusto *)
 178   cut (∀n:nat.R0 ≤ alpha3 n).by (ex_intro ? ? R0 Hcut) done.
 179   (* fatto *)
 180   we need to prove (∀n:nat. R0 ≤ alpha3 n).
 181   assume n:nat.
 182   we proceed by induction on n to prove (R0 ≤ alpha3 n).
 183   case O.
 184     (* manca il comando
 185     the thesis becomes (R0 ≤ alpha O)
 186     or equivalently (R0 ≤ R1).
 187     by _ done. *)
 188     (* approssimiamo con questo *)
 189     we need to prove (R0 ≤ alpha3 O)
 190     or equivalently (R0 ≤ Rdiv (S 0) (S (S 0))).
 191     by _ done.
 192   case S (m:nat).
 193    by induction hypothesis we know (R0 ≤ alpha3 m) (H).
 194    we need to prove (R0 ≤ alpha3 (S m))
 195    or equivalently (R0 ≤ Rmult (alpha3 m) (alpha3 m)).
 196    by _ done.
 197 qed.
 198
 199 theorem dim3: tends_to alpha3 O.
 200 (*..TODO..*)
 201 qed.
 202 *)