1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (* $Id: IVT.v,v 1.5 2004/04/23 10:01:04 lcf Exp $ *)
21 include "reals/CPoly_Contin.ma".
24 Section Nested_Intervals
27 (*#* * Intermediate Value Theorem
31 %\begin{convention}% Let [a,b:nat->IR] be sequences such that:
34 - [forall (i:nat), (a i) [<] (b i)];
35 - for every positive real number [eps], there is an [i] such that [(b i) [<] (a i) [+]eps].
40 alias id "a" = "cic:/CoRN/reals/IVT/Nested_Intervals/a.var".
42 alias id "b" = "cic:/CoRN/reals/IVT/Nested_Intervals/b.var".
44 alias id "a_mon" = "cic:/CoRN/reals/IVT/Nested_Intervals/a_mon.var".
46 alias id "b_mon" = "cic:/CoRN/reals/IVT/Nested_Intervals/b_mon.var".
48 alias id "a_b" = "cic:/CoRN/reals/IVT/Nested_Intervals/a_b.var".
50 alias id "b_a" = "cic:/CoRN/reals/IVT/Nested_Intervals/b_a.var".
52 inline procedural "cic:/CoRN/reals/IVT/a_mon'.con".
54 inline procedural "cic:/CoRN/reals/IVT/b_mon'.con".
56 inline procedural "cic:/CoRN/reals/IVT/a_b'.con".
58 inline procedural "cic:/CoRN/reals/IVT/intervals_cauchy.con".
62 inline procedural "cic:/CoRN/reals/IVT/Nested_Intervals/a'.con" "Nested_Intervals__".
66 inline procedural "cic:/CoRN/reals/IVT/Cnested_intervals_limit.con".
68 (*#* %\begin{convention}% Let [f] be a continuous real function.
72 alias id "f" = "cic:/CoRN/reals/IVT/Nested_Intervals/f.var".
74 alias id "f_contin" = "cic:/CoRN/reals/IVT/Nested_Intervals/f_contin.var".
76 inline procedural "cic:/CoRN/reals/IVT/f_contin_pos.con".
78 inline procedural "cic:/CoRN/reals/IVT/f_contin_neg.con".
80 (*#* Assume also that [forall i, f (a i) [<=] Zero [<=] f (b i)]. *)
82 alias id "f_a" = "cic:/CoRN/reals/IVT/Nested_Intervals/f_a.var".
84 alias id "f_b" = "cic:/CoRN/reals/IVT/Nested_Intervals/f_b.var".
86 inline procedural "cic:/CoRN/reals/IVT/Cnested_intervals_zero.con".
96 (*#* ** Bissections *)
98 alias id "f" = "cic:/CoRN/reals/IVT/Bisection/f.var".
100 alias id "f_apzero_interval" = "cic:/CoRN/reals/IVT/Bisection/f_apzero_interval.var".
102 alias id "a" = "cic:/CoRN/reals/IVT/Bisection/a.var".
104 alias id "b" = "cic:/CoRN/reals/IVT/Bisection/b.var".
106 alias id "a_b" = "cic:/CoRN/reals/IVT/Bisection/a_b.var".
108 alias id "f_a" = "cic:/CoRN/reals/IVT/Bisection/f_a.var".
110 alias id "f_b" = "cic:/CoRN/reals/IVT/Bisection/f_b.var".
113 %\begin{convention}% Let [Small] denote [Two[/]ThreeNZ], [lft] be [(Two[*]a[+]b) [/]ThreeNZ] and [rht] be [(a[+]Two[*]b) [/]ThreeNZ].
119 inline procedural "cic:/CoRN/reals/IVT/Bisection/Small.con" "Bisection__".
121 inline procedural "cic:/CoRN/reals/IVT/Bisection/lft.con" "Bisection__".
123 inline procedural "cic:/CoRN/reals/IVT/Bisection/rht.con" "Bisection__".
127 inline procedural "cic:/CoRN/reals/IVT/a_lft.con".
129 inline procedural "cic:/CoRN/reals/IVT/rht_b.con".
131 inline procedural "cic:/CoRN/reals/IVT/lft_rht.con".
133 inline procedural "cic:/CoRN/reals/IVT/smaller_lft.con".
135 inline procedural "cic:/CoRN/reals/IVT/smaller_rht.con".
138 Hint Resolve smaller_lft smaller_rht: algebra.
141 inline procedural "cic:/CoRN/reals/IVT/Cbisect'.con".
148 Section Bisect_Interval
151 alias id "f" = "cic:/CoRN/reals/IVT/Bisect_Interval/f.var".
153 alias id "C_f_apzero_interval" = "cic:/CoRN/reals/IVT/Bisect_Interval/C_f_apzero_interval.var".
157 inline procedural "cic:/CoRN/reals/IVT/Bisect_Interval/Small.con" "Bisect_Interval__".
161 inline procedural "cic:/CoRN/reals/IVT/bisect_interval.ind".
163 inline procedural "cic:/CoRN/reals/IVT/Cbisect_exists.con".
165 inline procedural "cic:/CoRN/reals/IVT/bisect.con".
167 inline procedural "cic:/CoRN/reals/IVT/bisect_prop.con".
177 (*#* ** IVT for operations
178 Same conventions as before.
181 alias id "f" = "cic:/CoRN/reals/IVT/IVT_Op/f.var".
183 alias id "f_contin" = "cic:/CoRN/reals/IVT/IVT_Op/f_contin.var".
185 alias id "f_apzero_interval" = "cic:/CoRN/reals/IVT/IVT_Op/f_apzero_interval.var".
187 alias id "a" = "cic:/CoRN/reals/IVT/IVT_Op/a.var".
189 alias id "b" = "cic:/CoRN/reals/IVT/IVT_Op/b.var".
191 alias id "a_b" = "cic:/CoRN/reals/IVT/IVT_Op/a_b.var".
193 alias id "f_a" = "cic:/CoRN/reals/IVT/IVT_Op/f_a.var".
195 alias id "f_b" = "cic:/CoRN/reals/IVT/IVT_Op/f_b.var".
199 inline procedural "cic:/CoRN/reals/IVT/IVT_Op/Small.con" "IVT_Op__".
203 inline procedural "cic:/CoRN/reals/IVT/interval_sequence.con".
205 inline procedural "cic:/CoRN/reals/IVT/IVT_Op/a_.con" "IVT_Op__".
207 inline procedural "cic:/CoRN/reals/IVT/IVT_Op/b_.con" "IVT_Op__".
209 inline procedural "cic:/CoRN/reals/IVT/intervals_smaller.con".
211 inline procedural "cic:/CoRN/reals/IVT/intervals_small''.con".
213 inline procedural "cic:/CoRN/reals/IVT/intervals_small'.con".
215 inline procedural "cic:/CoRN/reals/IVT/intervals_small.con".
217 inline procedural "cic:/CoRN/reals/IVT/Civt_op.con".
227 (*#* ** IVT for polynomials *)
229 inline procedural "cic:/CoRN/reals/IVT/Civt_poly.con".