From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 19 Sep 2005 16:25:16 +0000 (+0000)
Subject: * Obsolete debugging comments removed
X-Git-Tag: LAST_BEFORE_NEW~90
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ab44166935d77276c04fcce50aa8281292776e29;p=helm.git

* Obsolete debugging comments removed
* Debugging comments by Andrea marked with "Andrea:"
---

diff --git a/helm/matita/library/higher_order_defs/functions.ma b/helm/matita/library/higher_order_defs/functions.ma
index d2a577a49..321ae46b7 100644
--- a/helm/matita/library/higher_order_defs/functions.ma
+++ b/helm/matita/library/higher_order_defs/functions.ma
@@ -20,7 +20,6 @@ definition injective: \forall A,B:Type.\forall f:A \to B.Prop
 \def \lambda A,B.\lambda f.
   \forall x,y:A.f x = f y \to x=y.
 
-(* we have still to attach exists *)
 definition surjective: \forall A,B:Type.\forall f:A \to B.Prop
 \def \lambda A,B.\lambda f.
   \forall z:B. \exists x:A.z=f x.
diff --git a/helm/matita/library/nat/div_and_mod.ma b/helm/matita/library/nat/div_and_mod.ma
index ad74a324d..73344c7c4 100644
--- a/helm/matita/library/nat/div_and_mod.ma
+++ b/helm/matita/library/nat/div_and_mod.ma
@@ -133,7 +133,6 @@ rewrite < sym_plus.
 apply le_plus_n.
 rewrite < sym_times.
 rewrite > distr_times_minus.
-(* ATTENZIONE ALL' ORDINAMENTO DEI GOALS *)
 rewrite > plus_minus.
 rewrite > sym_times.
 rewrite < H5.
diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma
index b7ef49121..be1d79b1d 100644
--- a/helm/matita/library/nat/gcd.ma
+++ b/helm/matita/library/nat/gcd.ma
@@ -482,17 +482,6 @@ apply gcd_O_to_eq_O.apply sym_eq.assumption.
 apply le_to_or_lt_eq.apply le_O_n.
 qed.
 
-(* esempio di sfarfallalmento !!! *)
-(*
-theorem bad: \forall n,p,q:nat.prime n \to divides n (p*q) \to
-divides n p \lor divides n q.
-intros.
-cut divides n p \lor \not (divides n p).
-elim Hcut.left.assumption.
-right.
-cut \exists a,b. a*n - b*p = (S O) \lor b*p - a*n = (S O).
-elim Hcut1.elim H3.*)
-
 theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to divides n (p*q) \to
 divides n p \lor divides n q.
 intros.
diff --git a/helm/matita/library/nat/log.ma b/helm/matita/library/nat/log.ma
index 3babb5c75..51d0108d9 100644
--- a/helm/matita/library/nat/log.ma
+++ b/helm/matita/library/nat/log.ma
@@ -175,7 +175,7 @@ apply lt_div_n_m_n.assumption.assumption.assumption.
 intros.
 change with (\lnot (mod n1 m = O)).
 rewrite > H4.
-(* META NOT FOUND !!!  
+(* Andrea: META NOT FOUND !!!  
 rewrite > sym_eq. *)
 simplify.intro.
 apply not_eq_O_S m1.
diff --git a/helm/matita/library/nat/lt_arith.ma b/helm/matita/library/nat/lt_arith.ma
index dd4fdcbf9..f8df1c6be 100644
--- a/helm/matita/library/nat/lt_arith.ma
+++ b/helm/matita/library/nat/lt_arith.ma
@@ -116,7 +116,6 @@ qed.
 theorem lt_times_to_lt_l: 
 \forall n,p,q:nat. lt (times p (S n)) (times q (S n)) \to lt p q.
 intros.
-(* convertibility problem here *)
 cut Or (lt p q) (Not (lt p q)).
 elim Hcut.
 assumption.
diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma
index 079e902ad..7240b7d09 100644
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -118,8 +118,8 @@ intros 2.
 apply nat_elim2 (\lambda n,m.n \leq m \to n-m = O).
 intros.simplify.reflexivity.
 intros.apply False_ind.
-(* ancora problemi con il not *)
-apply not_le_Sn_O n1 H.
+apply not_le_Sn_O.
+goal 13.apply H.
 intros.
 simplify.apply H.apply le_S_S_to_le. apply H1.
 qed.
diff --git a/helm/matita/library/nat/nth_prime.ma b/helm/matita/library/nat/nth_prime.ma
index 8035d49dd..200ccba5a 100644
--- a/helm/matita/library/nat/nth_prime.ma
+++ b/helm/matita/library/nat/nth_prime.ma
@@ -62,7 +62,7 @@ apply ex_intro nat ? (smallest_factor (S (fact (S n1)))).
 split.split.
 apply smallest_factor_fact.
 apply le_smallest_factor_n.
-(* ancora hint non lo trova *)
+(* Andrea: ancora hint non lo trova *)
 apply prime_smallest_factor_n.
 change with (S(S O)) \le S (fact (S n1)).
 apply le_S.apply le_SSO_fact.
@@ -98,7 +98,6 @@ apply nat_case n.
 change with prime (S(S O)).
 apply primeb_to_Prop (S(S O)).
 intro.
-(* ammirare la resa del letin !! *)
 change with
 let previous_prime \def (nth_prime m) in
 let upper_bound \def S (fact previous_prime) in
diff --git a/helm/matita/library/nat/plus.ma b/helm/matita/library/nat/plus.ma
index 1c145dd61..79640b136 100644
--- a/helm/matita/library/nat/plus.ma
+++ b/helm/matita/library/nat/plus.ma
@@ -36,11 +36,6 @@ simplify.reflexivity.
 simplify.apply eq_f.assumption.
 qed.
 
-(* some problem here: confusion between relations/symmetric 
-and functions/symmetric; functions symmetric is not in 
-functions.moo why?
-theorem symmetric_plus: symmetric nat plus. *)
-
 theorem sym_plus: \forall n,m:nat. n+m = m+n.
 intros.elim n.
 simplify.apply plus_n_O.
@@ -67,8 +62,7 @@ theorem inj_plus_r: \forall p,n,m:nat. p+n = p+m \to n=m
 
 theorem injective_plus_l: \forall m:nat.injective nat nat (\lambda n.n+m).
 intro.simplify.intros.
-(* qui vorrei applicare injective_plus_r *)
-apply inj_plus_r m.
+apply injective_plus_r m.
 rewrite < sym_plus.
 rewrite < sym_plus y.
 assumption.
diff --git a/helm/matita/library/nat/primes.ma b/helm/matita/library/nat/primes.ma
index 644cae978..dc5f627e4 100644
--- a/helm/matita/library/nat/primes.ma
+++ b/helm/matita/library/nat/primes.ma
@@ -59,7 +59,7 @@ apply witness n m (div m n).
 rewrite > plus_n_O (n*div m n).
 rewrite < H1.
 rewrite < sym_times.
-(* perche' hint non lo trova ?*)
+(* Andrea: perche' hint non lo trova ?*)
 apply div_mod.
 assumption.
 qed.