]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/sqrt.ma
...
[helm.git] / helm / software / matita / library / nat / sqrt.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 "nat/times.ma".
16 include "nat/compare.ma".
17 include "nat/log.ma".
18
19 definition sqrt \def
20   \lambda n.max n (\lambda x.leb (x*x) n).
21
22 theorem eq_sqrt: \forall n. sqrt (n*n) = n.
23 intros.
24 unfold sqrt.apply max_spec_to_max.
25 unfold max_spec.split
26   [split
27     [cases n
28       [apply le_n
29       |rewrite > times_n_SO in ⊢ (? % ?).
30        apply le_times_r.
31        apply le_S_S.apply le_O_n
32       ]
33     |apply le_to_leb_true.apply le_n
34     ]
35   |intros.
36    apply lt_to_leb_false.
37    apply lt_times;assumption
38   ]
39 qed.
40
41 theorem le_sqrt_to_le_times_l : \forall m,n.n \leq sqrt m \to n*n \leq m.
42 intros;apply (trans_le ? (sqrt m * sqrt m))
43   [apply le_times;assumption
44   |apply leb_true_to_le;apply (f_max_true (λx:nat.leb (x*x) m) m);
45    apply (ex_intro ? ? O);split
46      [apply le_O_n
47      |simplify;reflexivity]]
48 qed.
49  
50 theorem lt_sqrt_to_le_times_l : \forall m,n.n < sqrt m \to n*n < m.
51 intros;apply (trans_le ? (sqrt m * sqrt m))
52   [apply (trans_le ? (S n * S n))
53      [simplify in \vdash (? ? %);apply le_S_S;apply (trans_le ? (n * S n))
54         [apply le_times_r;apply le_S;apply le_n
55         |rewrite > sym_plus;rewrite > plus_n_O in \vdash (? % ?);
56          apply le_plus_r;apply le_O_n]  
57      |apply le_times;assumption]
58   |apply le_sqrt_to_le_times_l;apply le_n]
59 qed.
60
61 theorem le_sqrt_to_le_times_r : \forall m,n.sqrt m < n \to m < n*n.
62 intros;apply not_le_to_lt;intro;
63 apply ((leb_false_to_not_le ? ? 
64            (lt_max_to_false (\lambda x.leb (x*x) m) m n H ?))
65          H1);
66 apply (trans_le ? ? ? ? H1);cases n
67   [apply le_n
68   |rewrite > times_n_SO in \vdash (? % ?);rewrite > sym_times;apply le_times
69      [apply le_S_S;apply le_O_n
70      |apply le_n]]
71 qed.
72   
73 lemma le_sqrt_n_n : \forall n.sqrt n \leq n.
74 intro.unfold sqrt.apply le_max_n.
75 qed.
76
77 lemma leq_sqrt_n : \forall n. sqrt n * sqrt n \leq n.
78 intro;unfold sqrt;apply leb_true_to_le;apply f_max_true;apply (ex_intro ? ? O);
79 split
80   [apply le_O_n
81   |simplify;reflexivity]
82 qed.
83
84 alias num (instance 0) = "natural number".
85
86 lemma lt_sqrt_n : \forall n.1 < n \to sqrt n < n.
87 intros.
88 elim (le_to_or_lt_eq ? ? (le_sqrt_n_n n))
89   [assumption
90   |apply False_ind.
91    apply (le_to_not_lt ? ? (leq_sqrt_n n)).
92    rewrite > H1.
93    rewrite > times_n_SO in ⊢ (? % ?).
94    apply lt_times_r1
95     [apply lt_to_le.assumption
96     |assumption
97     ]
98   ]
99 qed.
100
101 lemma lt_sqrt: \forall n.n < (exp (S (sqrt n)) 2).
102 intro.
103 cases n
104   [apply le_n
105   |cases n1
106     [simplify.apply lt_to_le.apply lt_to_le.apply le_n
107     |apply not_le_to_lt.
108      apply leb_false_to_not_le.
109      rewrite > exp_SSO.
110      apply (lt_max_to_false (\lambda x.(leb (x*x) (S(S n2)))) (S(S n2)))
111       [apply le_n
112       |apply lt_sqrt_n.
113        apply le_S_S.apply lt_O_S.
114       ]
115     ]
116   ]
117 qed.
118
119 lemma le_sqrt_n1: \forall n. n - 2*sqrt n \le exp (sqrt n) 2.
120 intros.
121 apply le_plus_to_minus.
122 apply le_S_S_to_le.
123 cut (S ((sqrt n)\sup 2+2*sqrt n) = (exp (S(sqrt n)) 2))
124   [rewrite > Hcut.apply lt_sqrt
125   |rewrite > exp_SSO.rewrite > exp_SSO.
126    simplify.apply eq_f.
127    rewrite < times_n_Sm.
128    rewrite < plus_n_O.
129    rewrite < assoc_plus in ⊢ (? ? ? %).
130    rewrite > sym_plus.
131    reflexivity
132   ]
133 qed.
134
135 (* falso per n=2, m=7 e n=3, m =15 *)
136 lemma le_sqrt_nl: \forall n,m. 3 < n \to
137 m*(pred m)*n \le exp (sqrt ((exp m 2)*n)) 2.
138 intros.
139 rewrite > minus_n_O in ⊢ (? (? (? ? (? %)) ?) ?).
140 rewrite < eq_minus_S_pred.
141 rewrite > distr_times_minus.
142 rewrite < times_n_SO.
143 rewrite > sym_times.
144 rewrite > distr_times_minus.
145 rewrite > sym_times.
146 apply (trans_le ? (m*m*n -2*sqrt(m*m*n)))
147   [apply monotonic_le_minus_r.
148    apply (le_exp_to_le1 ? ? 2)
149     [apply lt_O_S
150     |rewrite < times_exp.
151      apply (trans_le ? ((exp 2 2)*(m*m*n)))
152       [apply le_times_r.
153        rewrite > exp_SSO.
154        apply leq_sqrt_n
155       |rewrite < exp_SSO.
156        rewrite < times_exp.
157        rewrite < assoc_times.
158        rewrite < sym_times in ⊢ (? (? % ?) ?).
159        rewrite > assoc_times.
160        rewrite > sym_times.
161        apply le_times_l.
162        rewrite > exp_SSO in ⊢ (? ? %).
163        apply le_times_l.
164        assumption
165       ]
166     ]
167   |rewrite <exp_SSO. 
168    apply le_sqrt_n1
169   ]
170 qed.
171        
172 lemma le_sqrt_log_n : \forall n,b. 2 < b \to sqrt n * log b n \leq n.
173 intros.
174 apply (trans_le ? ? ? ? (leq_sqrt_n ?));
175 apply le_times_r;unfold sqrt;
176 apply f_m_to_le_max
177   [apply le_log_n_n;apply lt_to_le;assumption
178   |apply le_to_leb_true;elim (le_to_or_lt_eq ? ? (le_O_n n))
179      [apply (trans_le ? (exp b (log b n)))
180         [elim (log b n)
181            [apply le_O_n
182            |simplify in \vdash (? ? %);
183            elim (le_to_or_lt_eq ? ? (le_O_n n1))
184               [elim (le_to_or_lt_eq ? ? H3)
185                  [apply (trans_le ? (3*(n1*n1)));
186                     [simplify in \vdash (? % ?);rewrite > sym_times in \vdash (? % ?);
187                      simplify in \vdash (? % ?);
188                      simplify;rewrite > sym_plus;
189                      rewrite > plus_n_Sm;rewrite > sym_plus in \vdash (? (? % ?) ?);
190                      rewrite > assoc_plus;apply le_plus_r;
191                      rewrite < plus_n_Sm;
192                      rewrite < plus_n_O;
193                      apply lt_plus;rewrite > times_n_SO in \vdash (? % ?);
194                      apply lt_times_r1;assumption;
195                     |apply le_times
196                        [assumption
197                        |assumption]]
198                  |rewrite < H4;apply le_times
199                     [apply lt_to_le;assumption
200                     |apply lt_to_le;simplify;rewrite < times_n_SO;assumption]]
201              |rewrite < H3;simplify;rewrite < times_n_SO;do 2 apply lt_to_le;assumption]]
202         |simplify;apply le_exp_log;assumption]
203      |rewrite < H1;simplify;apply le_n]]
204 qed.
205
206 (* monotonicity *)
207 theorem monotonic_sqrt: monotonic nat le sqrt.
208 unfold.intros.
209 unfold sqrt in ⊢ (? ? (% ?)).
210 apply f_m_to_le_max
211   [apply (trans_le ? ? ? ? H).
212    apply le_sqrt_n_n
213   |apply le_to_leb_true.
214    apply (trans_le ? ? ? ? H). 
215    apply leq_sqrt_n
216   ]
217 qed.
218    
219