+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "sequences.ma".
-
-(*
-ESERCIZI SULLE SUCCESSIONI
-
-Dimostrare che la successione alpha converge a 0
-*)
-
-definition F ≝ λ x:R.Rdiv x (S (S O)).
-
-definition alpha ≝ successione F R1.
-
-axiom cont: continuo F.
-
-lemma l1: monotone_not_increasing alpha.
- we need to prove (monotone_not_increasing alpha)
- or equivalently (∀n:nat. alpha (S n) ≤ alpha n).
- assume n:nat.
- we need to prove (alpha (S n) ≤ alpha n)
- or equivalently (Rdiv (alpha n) (S (S O)) ≤ alpha n).
- by _ done.
-qed.
-
-lemma l2: inf_bounded alpha.
- we need to prove (inf_bounded alpha)
- or equivalently (∃m. ∀n:nat. m ≤ alpha n).
- (* da trovare il modo giusto *)
- cut (∀n:nat.R0 ≤ alpha n).by (ex_intro ? ? R0 Hcut) done.
- (* fatto *)
- we need to prove (∀n:nat. R0 ≤ alpha n).
- assume n:nat.
- we proceed by induction on n to prove (R0 ≤ alpha n).
- case O.
- (* manca il comando
- the thesis becomes (R0 ≤ alpha O)
- or equivalently (R0 ≤ R1).
- by _ done. *)
- (* approssimiamo con questo *)
- we need to prove (R0 ≤ alpha O)
- or equivalently (R0 ≤ R1).
- by _ done.
- case S (m:nat).
- by induction hypothesis we know (R0 ≤ alpha m) (H).
- we need to prove (R0 ≤ alpha (S m))
- or equivalently (R0 ≤ Rdiv (alpha m) (S (S O))).
- by _ done.
-qed.
-
-axiom xxx':
-∀ F: R → R. ∀b:R. continuo F →
- ∀ l. tends_to (successione F b) l →
- punto_fisso F l.
-
-theorem dimostrazione: tends_to alpha O.
- by _ let l:R such that (tends_to alpha l) (H).
-(* unfold alpha in H.
- change in match alpha in H with (successione F O).
- check(xxx' F cont l H).*)
- by (lim_punto_fisso F R1 cont l H) we proved (punto_fisso F l) (H2)
- that is equivalent to (l = (Rdiv l (S (S O)))).
- by _ we proved (tends_to alpha l = tends_to alpha O) (H4).
- rewrite < H4.
- by _ done.
-qed.
-
-(******************************************************************************)
-
-(* Dimostrare che la successione alpha2 diverge *)
-
-definition F2 ≝ λ x:R. Rmult x x.
-
-definition alpha2 ≝ successione F2 (S (S O)).
-
-lemma uno: ∀n. alpha2 n ≥ R1.
- we need to prove (∀n. alpha2 n ≥ R1).
- assume n:nat.
- we proceed by induction on n to prove (alpha2 n ≥ R1).
- case O.
- alias num (instance 0) = "natural number".
- we need to prove (alpha2 0 ≥ R1)
- or equivalently ((S (S O)) ≥ R1).
- by _ done.
- case S (m:nat).
- by induction hypothesis we know (alpha2 m ≥ R1) (H).
- we need to prove (alpha2 (S m) ≥ R1)
- or equivalently (Rmult (alpha2 m) (alpha2 m) ≥ R1).letin xxx := (n ≤ n);
- by _ we proved (R1 · R1 ≤ alpha2 m · alpha2 m) (H1).
- by _ we proved (R1 · R1 = R1) (H2).
- rewrite < H2.
- by _ done.
-qed.
-
-lemma mono1: monotone_not_decreasing alpha2.
- we need to prove (monotone_not_decreasing alpha2)
- or equivalently (∀n:nat. alpha2 n ≤ alpha2 (S n)).
- assume n:nat.
- we need to prove (alpha2 n ≤ alpha2 (S n))
- or equivalently (alpha2 n ≤ Rmult (alpha2 n) (alpha2 n)).
- by _ done.
-qed.
-
-(*
-lemma due: ∀n. Relev (alpha2 0) n ≥ R0.
- we need to prove (∀n. Relev (alpha2 0) n ≥ R0)
- or equivalently (∀n. Relev (S (S O)) n ≥ R0).
- by _ done.
-qed.
-
-lemma tre: ∀n. alpha2 (S n) ≥ Relev (alpha2 0) (S n).
- we need to prove (∀n. alpha2 (S n) ≥ Relev (alpha2 0) (S n)).
- assume n:nat.
- we proceed by induction on n to prove (alpha2 (S n) ≥ Relev (alpha2 0) (S n)).
- case 0.
- we need to prove (alpha2 1 ≥ Relev (alpha2 0) R1)
- or equivalently (Rmult R2 R2 ≥ R2).
- by _ done.
- case S (m:nat).
- by induction hypothesis we know (alpha2 (S m) ≥ Relev (alpha2 0) (S m)) (H).
- we need to prove (alpha2 (S (S m)) ≥ Relev (alpha2 0) (S (S m)))
- or equivalently
- (*..TODO..*)
-
-theorem dim2: tends_to_inf alpha2.
-(*..TODO..*)
-qed.
-*)
-
-(******************************************************************************)
-
-(* Dimostrare che la successione alpha3 converge a 0 *)
-(*
-definition alpha3 ≝ successione F2 (Rdiv (S 0) (S (S 0))).
-
-lemma quattro: ∀n. alpha3 n ≤ R1.
- assume n:nat.
- we need to prove (∀n. alpha3 n ≤ R1).
- we proceed by induction on n to prove (alpha3 n ≤ R1).
- case O.
- we need to prove (alpha3 0 ≤ R1).
- by _ done.
- case S (m:nat).
- by induction hypothesis we know (alpha3 m ≤ R1) (H).
- we need to prove (alpha3 (S m) ≤ R1)
- or equivalently (Rmult (alpha3 m) (alpha3 m) ≤ R1).
- by _ done.
- qed.
-
-lemma mono3: monotone_not_increasing alpha3.
- we need to prove (monotone_not_increasing alpha3)
- or equivalently (∀n:nat. alpha (S n) ≤ alpha n).
- assume n:nat.
- we need to prove (alpha (S n) ≤ alpha n)
- or equivalently (Rmult (alpha3 n) (alpha3 n) ≤ alpha3 n).
- by _ done.
-qed.
-
-lemma bound3: inf_bounded alpha3.
- we need to prove (inf_bounded alpha3)
- or equivalently (∃m. ∀n:nat. m ≤ alpha3 n).
- (* da trovare il modo giusto *)
- cut (∀n:nat.R0 ≤ alpha3 n).by (ex_intro ? ? R0 Hcut) done.
- (* fatto *)
- we need to prove (∀n:nat. R0 ≤ alpha3 n).
- assume n:nat.
- we proceed by induction on n to prove (R0 ≤ alpha3 n).
- case O.
- (* manca il comando
- the thesis becomes (R0 ≤ alpha O)
- or equivalently (R0 ≤ R1).
- by _ done. *)
- (* approssimiamo con questo *)
- we need to prove (R0 ≤ alpha3 O)
- or equivalently (R0 ≤ Rdiv (S 0) (S (S 0))).
- by _ done.
- case S (m:nat).
- by induction hypothesis we know (R0 ≤ alpha3 m) (H).
- we need to prove (R0 ≤ alpha3 (S m))
- or equivalently (R0 ≤ Rmult (alpha3 m) (alpha3 m)).
- by _ done.
-qed.
-
-theorem dim3: tends_to alpha3 O.
-(*..TODO..*)
-qed.
-*)
\ No newline at end of file
projects / helm.git / blobdiff