X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fsqrt.ma;h=d523d634dc5ff3fb503fa34f1ca39eaf432fe040;hb=a99fe3ca5a39b4d9754b69863b5f9fb0f91ed286;hp=c5a270128ee9eb580e80344ff363533d469359f2;hpb=31746c2da8a3a669d07fa4c7a1c043d7c958f789;p=helm.git

diff --git a/helm/software/matita/library/nat/sqrt.ma b/helm/software/matita/library/nat/sqrt.ma
index c5a270128..d523d634d 100644
--- a/helm/software/matita/library/nat/sqrt.ma
+++ b/helm/software/matita/library/nat/sqrt.ma
@@ -12,15 +12,32 @@
 (*                                                                        *)
 (**************************************************************************)
 
-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 eq_sqrt: \forall n. sqrt (n*n) = n.
+intros.
+unfold sqrt.apply max_spec_to_max.
+unfold max_spec.split
+  [split
+    [cases n
+      [apply le_n
+      |rewrite > times_n_SO in ⊢ (? % ?).
+       apply le_times_r.
+       apply le_S_S.apply le_O_n
+      ]
+    |apply le_to_leb_true.apply le_n
+    ]
+  |intros.
+   apply lt_to_leb_false.
+   apply lt_times;assumption
+  ]
+qed.
+
 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
@@ -65,6 +82,93 @@ split
 qed.
 
 alias num (instance 0) = "natural number".
+
+lemma lt_sqrt_n : \forall n.1 < n \to sqrt n < n.
+intros.
+elim (le_to_or_lt_eq ? ? (le_sqrt_n_n n))
+  [assumption
+  |apply False_ind.
+   apply (le_to_not_lt ? ? (leq_sqrt_n n)).
+   rewrite > H1.
+   rewrite > times_n_SO in ⊢ (? % ?).
+   apply lt_times_r1
+    [apply lt_to_le.assumption
+    |assumption
+    ]
+  ]
+qed.
+
+lemma lt_sqrt: \forall n.n < (exp (S (sqrt n)) 2).
+intro.
+cases n
+  [apply le_n
+  |cases n1
+    [simplify.apply lt_to_le.apply lt_to_le.apply le_n
+    |apply not_le_to_lt.
+     apply leb_false_to_not_le.
+     rewrite > exp_SSO.
+     apply (lt_max_to_false (\lambda x.(leb (x*x) (S(S n2)))) (S(S n2)))
+      [apply le_n
+      |apply lt_sqrt_n.
+       apply le_S_S.apply lt_O_S.
+      ]
+    ]
+  ]
+qed.
+
+lemma le_sqrt_n1: \forall n. n - 2*sqrt n \le exp (sqrt n) 2.
+intros.
+apply le_plus_to_minus.
+apply le_S_S_to_le.
+cut (S ((sqrt n)\sup 2+2*sqrt n) = (exp (S(sqrt n)) 2))
+  [rewrite > Hcut.apply lt_sqrt
+  |rewrite > exp_SSO.rewrite > exp_SSO.
+   simplify.apply eq_f.
+   rewrite < times_n_Sm.
+   rewrite < plus_n_O.
+   rewrite < assoc_plus in ⊢ (? ? ? %).
+   rewrite > sym_plus.
+   reflexivity
+  ]
+qed.
+
+(* falso per n=2, m=7 e n=3, m =15 *)
+lemma le_sqrt_nl: \forall n,m. 3 < n \to
+m*(pred m)*n \le exp (sqrt ((exp m 2)*n)) 2.
+intros.
+rewrite > minus_n_O in ⊢ (? (? (? ? (? %)) ?) ?).
+rewrite < eq_minus_S_pred.
+rewrite > distr_times_minus.
+rewrite < times_n_SO.
+rewrite > sym_times.
+rewrite > distr_times_minus.
+rewrite > sym_times.
+apply (trans_le ? (m*m*n -2*sqrt(m*m*n)))
+  [apply monotonic_le_minus_r.
+   apply (le_exp_to_le1 ? ? 2)
+    [apply lt_O_S
+    |rewrite < times_exp.
+     apply (trans_le ? ((exp 2 2)*(m*m*n)))
+      [apply le_times_r.
+       rewrite > exp_SSO.
+       apply leq_sqrt_n
+      |rewrite < exp_SSO.
+       rewrite < times_exp.
+       rewrite < assoc_times.
+       rewrite < sym_times in ⊢ (? (? % ?) ?).
+       rewrite > assoc_times.
+       rewrite > sym_times.
+       apply le_times_l.
+       rewrite > exp_SSO in ⊢ (? ? %).
+       apply le_times_l.
+       assumption
+      ]
+    ]
+  |rewrite <exp_SSO. 
+   apply le_sqrt_n1
+  ]
+qed.
+       
 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 ?));
@@ -98,3 +202,18 @@ apply f_m_to_le_max
         |simplify;apply le_exp_log;assumption]
      |rewrite < H1;simplify;apply le_n]]
 qed.
+
+(* monotonicity *)
+theorem monotonic_sqrt: monotonic nat le sqrt.
+unfold.intros.
+unfold sqrt in ⊢ (? ? (% ?)).
+apply f_m_to_le_max
+  [apply (trans_le ? ? ? ? H).
+   apply le_sqrt_n_n
+  |apply le_to_leb_true.
+   apply (trans_le ? ? ? ? H). 
+   apply leq_sqrt_n
+  ]
+qed.
+   
+