From ab44166935d77276c04fcce50aa8281292776e29 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 19 Sep 2005 16:25:16 +0000 Subject: [PATCH] * Obsolete debugging comments removed * Debugging comments by Andrea marked with "Andrea:" --- helm/matita/library/higher_order_defs/functions.ma | 1 - helm/matita/library/nat/div_and_mod.ma | 1 - helm/matita/library/nat/gcd.ma | 11 ----------- helm/matita/library/nat/log.ma | 2 +- helm/matita/library/nat/lt_arith.ma | 1 - helm/matita/library/nat/minus.ma | 4 ++-- helm/matita/library/nat/nth_prime.ma | 3 +-- helm/matita/library/nat/plus.ma | 8 +------- helm/matita/library/nat/primes.ma | 2 +- 9 files changed, 6 insertions(+), 27 deletions(-) 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. -- 2.39.2