Square root added.

diff --git a/helm/software/matita/library/nat/sqrt.ma b/helm/software/matita/library/nat/sqrt.ma
new file mode 100644 (file)
index 0000000..c5a2701
--- /dev/null
+++ b/helm/software/matita/library/nat/sqrt.ma
@@ -0,0 +1,100 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/nat/sqrt/".
+
+include "nat/times.ma".
+include "nat/compare.ma".
+include "nat/log.ma".
+
+definition sqrt \def
+  \lambda n.max n (\lambda x.leb (x*x) n).
+  
+theorem le_sqrt_to_le_times_l : \forall m,n.n \leq sqrt m \to n*n \leq m.
+intros;apply (trans_le ? (sqrt m * sqrt m))
+  [apply le_times;assumption
+  |apply leb_true_to_le;apply (f_max_true (λx:nat.leb (x*x) m) m);
+   apply (ex_intro ? ? O);split
+     [apply le_O_n
+     |simplify;reflexivity]]
+qed.
+ 
+theorem lt_sqrt_to_le_times_l : \forall m,n.n < sqrt m \to n*n < m.
+intros;apply (trans_le ? (sqrt m * sqrt m))
+  [apply (trans_le ? (S n * S n))
+     [simplify in \vdash (? ? %);apply le_S_S;apply (trans_le ? (n * S n))
+        [apply le_times_r;apply le_S;apply le_n
+        |rewrite > sym_plus;rewrite > plus_n_O in \vdash (? % ?);
+         apply le_plus_r;apply le_O_n]  
+     |apply le_times;assumption]
+  |apply le_sqrt_to_le_times_l;apply le_n]
+qed.
+
+theorem le_sqrt_to_le_times_r : \forall m,n.sqrt m < n \to m < n*n.
+intros;apply not_le_to_lt;intro;
+apply ((leb_false_to_not_le ? ? 
+           (lt_max_to_false (\lambda x.leb (x*x) m) m n H ?))
+         H1);
+apply (trans_le ? ? ? ? H1);cases n
+  [apply le_n
+  |rewrite > times_n_SO in \vdash (? % ?);rewrite > sym_times;apply le_times
+     [apply le_S_S;apply le_O_n
+     |apply le_n]]
+qed.
+  
+lemma le_sqrt_n_n : \forall n.sqrt n \leq n.
+intro.unfold sqrt.apply le_max_n.
+qed.
+
+lemma leq_sqrt_n : \forall n. sqrt n * sqrt n \leq n.
+intro;unfold sqrt;apply leb_true_to_le;apply f_max_true;apply (ex_intro ? ? O);
+split
+  [apply le_O_n
+  |simplify;reflexivity]
+qed.
+
+alias num (instance 0) = "natural number".
+lemma le_sqrt_log_n : \forall n,b. 2 < b \to sqrt n * log b n \leq n.
+intros.
+apply (trans_le ? ? ? ? (leq_sqrt_n ?));
+apply le_times_r;unfold sqrt;
+apply f_m_to_le_max
+  [apply le_log_n_n;apply lt_to_le;assumption
+  |apply le_to_leb_true;elim (le_to_or_lt_eq ? ? (le_O_n n))
+     [apply (trans_le ? (exp b (log b n)))
+        [elim (log b n)
+           [apply le_O_n
+           |simplify in \vdash (? ? %);
+           elim (le_to_or_lt_eq ? ? (le_O_n n1))
+              [elim (le_to_or_lt_eq ? ? H3)
+                 [apply (trans_le ? (3*(n1*n1)));
+                    [simplify in \vdash (? % ?);rewrite > sym_times in \vdash (? % ?);
+                     simplify in \vdash (? % ?);
+                     simplify;rewrite > sym_plus;
+                     rewrite > plus_n_Sm;rewrite > sym_plus in \vdash (? (? % ?) ?);
+                     rewrite > assoc_plus;apply le_plus_r;
+                     rewrite < plus_n_Sm;
+                     rewrite < plus_n_O;
+                     apply lt_plus;rewrite > times_n_SO in \vdash (? % ?);
+                     apply lt_times_r1;assumption;
+                    |apply le_times
+                       [assumption
+                       |assumption]]
+                 |rewrite < H4;apply le_times
+                    [apply lt_to_le;assumption
+                    |apply lt_to_le;simplify;rewrite < times_n_SO;assumption]]
+             |rewrite < H3;simplify;rewrite < times_n_SO;do 2 apply lt_to_le;assumption]]
+        |simplify;apply le_exp_log;assumption]
+     |rewrite < H1;simplify;apply le_n]]
+qed.