From 30b7e65d641fe7243c4f36ed448f56360a1c5e1c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 22 Sep 2005 17:30:11 +0000 Subject: [PATCH] More notation here and there: \sup, \divides, \ndivides, ! --- helm/matita/core_notation.moo | 10 +- helm/matita/library/logic/connectives.ma | 2 +- helm/matita/library/nat/compare.ma | 2 +- helm/matita/library/nat/factorial.ma | 16 +-- helm/matita/library/nat/factorization.ma | 46 ++++----- helm/matita/library/nat/gcd.ma | 88 ++++++++-------- helm/matita/library/nat/log.ma | 2 +- helm/matita/library/nat/minus.ma | 2 +- helm/matita/library/nat/nth_prime.ma | 30 +++--- helm/matita/library/nat/primes.ma | 122 ++++++++++++----------- 10 files changed, 163 insertions(+), 157 deletions(-) diff --git a/helm/matita/core_notation.moo b/helm/matita/core_notation.moo index 9af57e4fe..86de49f0d 100644 --- a/helm/matita/core_notation.moo +++ b/helm/matita/core_notation.moo @@ -46,6 +46,14 @@ notation "hvbox(a break \ngtr b)" non associative with precedence 45 for @{ 'ngtr $a $b }. +notation "hvbox(a break \divides b)" + non associative with precedence 45 +for @{ 'divides $a $b }. + +notation "hvbox(a break \ndivides b)" + non associative with precedence 45 +for @{ 'ndivides $a $b }. + notation "hvbox(a break + b)" left associative with precedence 50 for @{ 'plus $a $b }. @@ -75,7 +83,7 @@ notation "- a" for @{ 'uminus $a }. notation "a !" - left associative with precedence 65 + non associative with precedence 80 for @{ 'fact $a }. notation "(a \sup b)" diff --git a/helm/matita/library/logic/connectives.ma b/helm/matita/library/logic/connectives.ma index 15b1cfe10..a8cba2b4a 100644 --- a/helm/matita/library/logic/connectives.ma +++ b/helm/matita/library/logic/connectives.ma @@ -57,7 +57,7 @@ inductive Or (A,B:Prop) : Prop \def interpretation "logical or" 'or x y = (cic:/matita/logic/connectives/Or.ind#xpointer(1/1) x y). -definition decidable : Prop \to Prop \def \lambda A:Prop. A \lor \not A. +definition decidable : Prop \to Prop \def \lambda A:Prop. A \lor \lnot A. inductive ex (A:Type) (P:A \to Prop) : Prop \def ex_intro: \forall x:A. P x \to ex A P. diff --git a/helm/matita/library/nat/compare.ma b/helm/matita/library/nat/compare.ma index 22c8b25a7..e20d824df 100644 --- a/helm/matita/library/nat/compare.ma +++ b/helm/matita/library/nat/compare.ma @@ -89,7 +89,7 @@ simplify.intros.apply H.apply le_S_S_to_le.assumption. qed. theorem leb_elim: \forall n,m:nat. \forall P:bool \to Prop. -(n \leq m \to (P true)) \to (\not (n \leq m) \to (P false)) \to +(n \leq m \to (P true)) \to (\lnot (n \leq m) \to (P false)) \to P (leb n m). intros. cut diff --git a/helm/matita/library/nat/factorial.ma b/helm/matita/library/nat/factorial.ma index 159559f09..d792574e3 100644 --- a/helm/matita/library/nat/factorial.ma +++ b/helm/matita/library/nat/factorial.ma @@ -23,33 +23,33 @@ let rec fact n \def interpretation "factorial" 'fact n = (cic:/matita/nat/factorial/fact.con n). -theorem le_SO_fact : \forall n. (S O) \le n !. +theorem le_SO_fact : \forall n. (S O) \le n!. intro.elim n.simplify.apply le_n. -change with (S O) \le (S n1)*n1 !. +change with (S O) \le (S n1)*n1!. apply trans_le ? ((S n1)*(S O)).simplify. apply le_S_S.apply le_O_n. apply le_times_r.assumption. qed. -theorem le_SSO_fact : \forall n. (S O) < n \to (S(S O)) \le n !. +theorem le_SSO_fact : \forall n. (S O) < n \to (S(S O)) \le n!. intro.apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S O) H. -intros.change with (S (S O)) \le (S m)*m !. +intros.change with (S (S O)) \le (S m)*m!. apply trans_le ? ((S(S O))*(S O)).apply le_n. apply le_times.exact H.apply le_SO_fact. qed. -theorem le_n_fact_n: \forall n. n \le n !. +theorem le_n_fact_n: \forall n. n \le n!. intro. elim n.apply le_O_n. -change with S n1 \le (S n1)*n1 !. +change with S n1 \le (S n1)*n1!. apply trans_le ? ((S n1)*(S O)). rewrite < times_n_SO.apply le_n. apply le_times.apply le_n. apply le_SO_fact. qed. -theorem lt_n_fact_n: \forall n. (S(S O)) < n \to n < n !. +theorem lt_n_fact_n: \forall n. (S(S O)) < n \to n < n!. intro.apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S(S O)) H. -intros.change with (S m) < (S m)*m !. +intros.change with (S m) < (S m)*m!. apply lt_to_le_to_lt ? ((S m)*(S (S O))). rewrite < sym_times. simplify. diff --git a/helm/matita/library/nat/factorization.ma b/helm/matita/library/nat/factorization.ma index 43b942a5b..1b946be52 100644 --- a/helm/matita/library/nat/factorization.ma +++ b/helm/matita/library/nat/factorization.ma @@ -25,7 +25,7 @@ definition max_prime_factor \def \lambda n:nat. (* max_prime_factor is indeed a factor *) theorem divides_max_prime_factor_n: \forall n:nat. (S O) < n \to -divides (nth_prime (max_prime_factor n)) n. +nth_prime (max_prime_factor n) \divides n. intros.apply divides_b_true_to_divides. apply lt_O_nth_prime_n. apply f_max_true (\lambda p:nat.eqb (mod n (nth_prime p)) O) n. @@ -48,7 +48,7 @@ apply prime_to_nth_prime. apply prime_smallest_factor_n.assumption. qed. -theorem divides_to_max_prime_factor : \forall n,m. (S O) < n \to O < m \to divides n m \to +theorem divides_to_max_prime_factor : \forall n,m. (S O) < n \to O < m \to n \divides m \to max_prime_factor n \le max_prime_factor m. intros.change with (max n (\lambda p:nat.eqb (mod n (nth_prime p)) O)) \le @@ -60,7 +60,7 @@ change with divides_b (nth_prime (max_prime_factor n)) m = true. apply divides_to_divides_b_true. cut prime (nth_prime (max_prime_factor n)). apply lt_O_nth_prime_n.apply prime_nth_prime. -cut divides (nth_prime (max_prime_factor n)) n. +cut nth_prime (max_prime_factor n) \divides n. apply transitive_divides ? n. apply divides_max_prime_factor_n. assumption.assumption. @@ -81,13 +81,13 @@ rewrite > H1. cut max_prime_factor r \lt max_prime_factor n \lor max_prime_factor r = max_prime_factor n. elim Hcut.assumption. -absurd (divides (nth_prime (max_prime_factor n)) r). +absurd nth_prime (max_prime_factor n) \divides r. rewrite < H4. apply divides_max_prime_factor_n. assumption. -change with (divides (nth_prime (max_prime_factor n)) r) \to False. +change with nth_prime (max_prime_factor n) \divides r \to False. intro. -cut \not (mod r (nth_prime (max_prime_factor n))) = O. +cut \lnot (mod r (nth_prime (max_prime_factor n))) = O. apply Hcut1.apply divides_to_mod_O. apply lt_O_nth_prime_n.assumption. apply plog_aux_to_not_mod_O n n ? q r. @@ -266,12 +266,12 @@ assumption. apply sym_eq. apply S_pred. cut O < q \lor O = q. elim Hcut2.assumption. -absurd divides (nth_prime p) (S (S m1)). +absurd nth_prime p \divides S (S m1). apply divides_max_prime_factor_n (S (S m1)). simplify.apply le_S_S.apply le_S_S. apply le_O_n. cut (S(S m1)) = r. rewrite > Hcut3 in \vdash (? (? ? %)). -change with divides (nth_prime p) r \to False. +change with nth_prime p \divides r \to False. intro. apply plog_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r. apply lt_SO_nth_prime_n. @@ -332,13 +332,13 @@ match f with | (nf_cons n g) \Rightarrow max_p_exponent g]. theorem divides_max_p_defactorize: \forall f:nat_fact.\forall i:nat. -divides (nth_prime ((max_p f)+i)) (defactorize_aux f i). +nth_prime ((max_p f)+i) \divides defactorize_aux f i. intro. elim f.simplify.apply witness ? ? ((nth_prime i) \sup n). reflexivity. change with -divides (nth_prime (S(max_p n1)+i)) -((nth_prime i) \sup n *(defactorize_aux n1 (S i))). +nth_prime (S(max_p n1)+i) \divides +(nth_prime i) \sup n *(defactorize_aux n1 (S i)). elim H (S i). rewrite > H1. rewrite < sym_times. @@ -350,11 +350,11 @@ qed. theorem divides_exp_to_divides: \forall p,n,m:nat. prime p \to -divides p (n \sup m) \to divides p n. +p \divides n \sup m \to p \divides n. intros 3.elim m.simplify in H1. apply transitive_divides p (S O).assumption. apply divides_SO_n. -cut divides p n \lor divides p (n \sup n1). +cut p \divides n \lor p \divides n \sup n1. elim Hcut.assumption. apply H.assumption.assumption. apply divides_times_to_divides.assumption. @@ -363,7 +363,7 @@ qed. theorem divides_exp_to_eq: \forall p,q,m:nat. prime p \to prime q \to -divides p (q \sup m) \to p = q. +p \divides q \sup m \to p = q. intros. simplify in H1. elim H1.apply H4. @@ -373,10 +373,10 @@ simplify in H.elim H.assumption. qed. theorem not_divides_defactorize_aux: \forall f:nat_fact. \forall i,j:nat. -i < j \to \not divides (nth_prime i) (defactorize_aux f j). +i < j \to nth_prime i \ndivides defactorize_aux f j. intro.elim f. change with -divides (nth_prime i) ((nth_prime j) \sup (S n)) \to False. +nth_prime i \divides (nth_prime j) \sup (S n) \to False. intro.absurd (nth_prime i) = (nth_prime j). apply divides_exp_to_eq ? ? (S n). apply prime_nth_prime.apply prime_nth_prime. @@ -386,10 +386,10 @@ intro.cut i = j. apply not_le_Sn_n i.rewrite > Hcut in \vdash (? ? %).assumption. apply injective_nth_prime ? ? H2. change with -divides (nth_prime i) ((nth_prime j) \sup n *(defactorize_aux n1 (S j))) \to False. +nth_prime i \divides (nth_prime j) \sup n *(defactorize_aux n1 (S j)) \to False. intro. -cut divides (nth_prime i) ((nth_prime j) \sup n) -\lor divides (nth_prime i) (defactorize_aux n1 (S j)). +cut nth_prime i \divides (nth_prime j) \sup n +\lor nth_prime i \divides defactorize_aux n1 (S j). elim Hcut. absurd (nth_prime i) = (nth_prime j). apply divides_exp_to_eq ? ? n. @@ -420,11 +420,11 @@ assumption. absurd defactorize_aux (nf_last n) i = defactorize_aux (nf_cons n1 n2) i. rewrite > H2.reflexivity. -absurd divides (nth_prime (S(max_p n2)+i)) (defactorize_aux (nf_cons n1 n2) i). +absurd nth_prime (S(max_p n2)+i) \divides defactorize_aux (nf_cons n1 n2) i. apply divides_max_p_defactorize. rewrite < H2. change with -(divides (nth_prime (S(max_p n2)+i)) ((nth_prime i) \sup (S n))) \to False. +(nth_prime (S(max_p n2)+i) \divides (nth_prime i) \sup (S n)) \to False. intro. absurd nth_prime (S (max_p n2) + i) = nth_prime i. apply divides_exp_to_eq ? ? (S n). @@ -441,11 +441,11 @@ elim g. absurd defactorize_aux (nf_last n2) i = defactorize_aux (nf_cons n n1) i. apply sym_eq. assumption. -absurd divides (nth_prime (S(max_p n1)+i)) (defactorize_aux (nf_cons n n1) i). +absurd nth_prime (S(max_p n1)+i) \divides defactorize_aux (nf_cons n n1) i. apply divides_max_p_defactorize. rewrite > H2. change with -(divides (nth_prime (S(max_p n1)+i)) ((nth_prime i) \sup (S n2))) \to False. +(nth_prime (S(max_p n1)+i) \divides (nth_prime i) \sup (S n2)) \to False. intro. absurd nth_prime (S (max_p n1) + i) = nth_prime i. apply divides_exp_to_eq ? ? (S n2). diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma index be1d79b1d..8475fc06a 100644 --- a/helm/matita/library/nat/gcd.ma +++ b/helm/matita/library/nat/gcd.ma @@ -36,8 +36,8 @@ definition gcd : nat \to nat \to nat \def [ O \Rightarrow n | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]. -theorem divides_mod: \forall p,m,n:nat. O < n \to divides p m \to divides p n \to -divides p (mod m n). +theorem divides_mod: \forall p,m,n:nat. O < n \to p \divides m \to p \divides n \to +p \divides mod m n. intros.elim H1.elim H2. apply witness ? ? (n2 - n1*(div m n)). rewrite > distr_times_minus. @@ -56,7 +56,7 @@ apply div_mod.assumption. qed. theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to -divides p (mod m n) \to divides p n \to divides p m. +p \divides mod m n \to p \divides n \to p \divides m. intros.elim H1.elim H2. apply witness p m ((n1*(div m n))+n2). rewrite > distr_times_plus. @@ -67,29 +67,27 @@ apply div_mod.assumption. qed. theorem divides_gcd_aux_mn: \forall p,m,n. O < n \to n \le m \to n \le p \to -divides (gcd_aux p m n) m \land divides (gcd_aux p m n) n. +gcd_aux p m n \divides m \land gcd_aux p m n \divides n. intro.elim p. absurd O < n.assumption.apply le_to_not_lt.assumption. -cut (divides n1 m) \lor \not (divides n1 m). +cut (n1 \divides m) \lor (n1 \ndivides m). change with -(divides (match divides_b n1 m with [ true \Rightarrow n1 -| false \Rightarrow gcd_aux n n1 (mod m n1)]) m) \land -(divides +| false \Rightarrow gcd_aux n n1 (mod m n1)]) \divides m \land (match divides_b n1 m with [ true \Rightarrow n1 -| false \Rightarrow gcd_aux n n1 (mod m n1)]) n1). +| false \Rightarrow gcd_aux n n1 (mod m n1)]) \divides n1. elim Hcut.rewrite > divides_to_divides_b_true. simplify. split.assumption.apply witness n1 n1 (S O).apply times_n_SO. assumption.assumption. rewrite > not_divides_to_divides_b_false. change with -(divides (gcd_aux n n1 (mod m n1)) m) \land -(divides (gcd_aux n n1 (mod m n1)) n1). -cut (divides (gcd_aux n n1 (mod m n1)) n1) \land -(divides (gcd_aux n n1 (mod m n1)) (mod m n1)). +gcd_aux n n1 (mod m n1) \divides m \land +gcd_aux n n1 (mod m n1) \divides n1. +cut gcd_aux n n1 (mod m n1) \divides n1 \land +gcd_aux n n1 (mod m n1) \divides mod m n1. elim Hcut1. split.apply divides_mod_to_divides ? ? n1. assumption.assumption.assumption.assumption. @@ -110,11 +108,10 @@ apply decidable_divides n1 m.assumption. qed. theorem divides_gcd_nm: \forall n,m. -divides (gcd n m) m \land divides (gcd n m) n. +gcd n m \divides m \land gcd n m \divides n. intros. change with -divides -(match leb n m with +match leb n m with [ true \Rightarrow match n with [ O \Rightarrow m @@ -122,10 +119,9 @@ divides | false \Rightarrow match m with [ O \Rightarrow n - | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]) m + | (S p) \Rightarrow gcd_aux (S p) n (S p) ]] \divides m \land - divides -(match leb n m with +match leb n m with [ true \Rightarrow match n with [ O \Rightarrow m @@ -133,16 +129,16 @@ divides | false \Rightarrow match m with [ O \Rightarrow n - | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]) n. + | (S p) \Rightarrow gcd_aux (S p) n (S p) ]] \divides n. apply leb_elim n m. apply nat_case1 n. simplify.intros.split. apply witness m m (S O).apply times_n_SO. apply witness m O O.apply times_n_O. intros.change with -divides (gcd_aux (S m1) m (S m1)) m +gcd_aux (S m1) m (S m1) \divides m \land -divides (gcd_aux (S m1) m (S m1)) (S m1). +gcd_aux (S m1) m (S m1) \divides (S m1). apply divides_gcd_aux_mn. simplify.apply le_S_S.apply le_O_n. assumption.apply le_n. @@ -152,12 +148,12 @@ simplify.intros.split. apply witness n O O.apply times_n_O. apply witness n n (S O).apply times_n_SO. intros.change with -divides (gcd_aux (S m1) n (S m1)) (S m1) +gcd_aux (S m1) n (S m1) \divides (S m1) \land -divides (gcd_aux (S m1) n (S m1)) n. -cut divides (gcd_aux (S m1) n (S m1)) n +gcd_aux (S m1) n (S m1) \divides n. +cut gcd_aux (S m1) n (S m1) \divides n \land -divides (gcd_aux (S m1) n (S m1)) (S m1). +gcd_aux (S m1) n (S m1) \divides S m1. elim Hcut.split.assumption.assumption. apply divides_gcd_aux_mn. simplify.apply le_S_S.apply le_O_n. @@ -166,38 +162,36 @@ rewrite > H1.apply trans_le ? (S n). apply le_n_Sn.assumption.apply le_n. qed. -theorem divides_gcd_n: \forall n,m. -divides (gcd n m) n. +theorem divides_gcd_n: \forall n,m. gcd n m \divides n. intros. exact proj2 ? ? (divides_gcd_nm n m). qed. -theorem divides_gcd_m: \forall n,m. -divides (gcd n m) m. +theorem divides_gcd_m: \forall n,m. gcd n m \divides m. intros. exact proj1 ? ? (divides_gcd_nm n m). qed. theorem divides_gcd_aux: \forall p,m,n,d. O < n \to n \le m \to n \le p \to -divides d m \to divides d n \to divides d (gcd_aux p m n). +d \divides m \to d \divides n \to d \divides gcd_aux p m n. intro.elim p. absurd O < n.assumption.apply le_to_not_lt.assumption. change with -divides d +d \divides (match divides_b n1 m with [ true \Rightarrow n1 | false \Rightarrow gcd_aux n n1 (mod m n1)]). -cut divides n1 m \lor \not (divides n1 m). +cut n1 \divides m \lor n1 \ndivides m. elim Hcut. rewrite > divides_to_divides_b_true. simplify.assumption. assumption.assumption. rewrite > not_divides_to_divides_b_false. -change with divides d (gcd_aux n n1 (mod m n1)). +change with d \divides gcd_aux n n1 (mod m n1). apply H. cut O \lt mod m n1 \lor O = mod m n1. elim Hcut1.assumption. -absurd divides n1 m.apply mod_O_to_divides. +absurd n1 \divides m.apply mod_O_to_divides. assumption.apply sym_eq.assumption.assumption. apply le_to_or_lt_eq.apply le_O_n. apply lt_to_le. @@ -213,10 +207,10 @@ apply decidable_divides n1 m.assumption. qed. theorem divides_d_gcd: \forall m,n,d. -divides d m \to divides d n \to divides d (gcd n m). +d \divides m \to d \divides n \to d \divides gcd n m. intros. change with -divides d ( +d \divides match leb n m with [ true \Rightarrow match n with @@ -225,17 +219,17 @@ match leb n m with | false \Rightarrow match m with [ O \Rightarrow n - | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]). + | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]. apply leb_elim n m. apply nat_case1 n.simplify.intros.assumption. intros. -change with divides d (gcd_aux (S m1) m (S m1)). +change with d \divides gcd_aux (S m1) m (S m1). apply divides_gcd_aux. simplify.apply le_S_S.apply le_O_n.assumption.apply le_n.assumption. rewrite < H2.assumption. apply nat_case1 m.simplify.intros.assumption. intros. -change with divides d (gcd_aux (S m1) n (S m1)). +change with d \divides gcd_aux (S m1) n (S m1). apply divides_gcd_aux. simplify.apply le_S_S.apply le_O_n. apply lt_to_le.apply not_le_to_lt.assumption.apply le_n.assumption. @@ -248,7 +242,7 @@ intro. elim p. absurd O < n.assumption.apply le_to_not_lt.assumption. cut O < m. -cut (divides n1 m) \lor \not (divides n1 m). +cut n1 \divides m \lor n1 \ndivides m. change with \exists a,b. a*n1 - b*m = match divides_b n1 m with @@ -319,7 +313,7 @@ assumption. apply H n1 (mod m n1). cut O \lt mod m n1 \lor O = mod m n1. elim Hcut2.assumption. -absurd divides n1 m.apply mod_O_to_divides. +absurd n1 \divides m.apply mod_O_to_divides. assumption. symmetry.assumption.assumption. apply le_to_or_lt_eq.apply le_O_n. @@ -413,7 +407,7 @@ qed. theorem gcd_O_to_eq_O:\forall m,n:nat. (gcd m n) = O \to m = O \land n = O. -intros.cut divides O n \land divides O m. +intros.cut O \divides n \land O \divides m. elim Hcut.elim H2.split. assumption.elim H1.assumption. rewrite < H. @@ -462,7 +456,7 @@ apply gcd_O_to_eq_O.apply sym_eq.assumption. apply le_to_or_lt_eq.apply le_O_n. qed. -theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to \not (divides n m) \to +theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to n \ndivides m \to gcd n m = (S O). intros.simplify in H.change with gcd n m = (S O). elim H. @@ -482,10 +476,10 @@ apply gcd_O_to_eq_O.apply sym_eq.assumption. apply le_to_or_lt_eq.apply le_O_n. qed. -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. +theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to n \divides p*q \to +n \divides p \lor n \divides q. intros. -cut divides n p \lor \not (divides n p). +cut n \divides p \lor n \ndivides p. elim Hcut. left.assumption. right. diff --git a/helm/matita/library/nat/log.ma b/helm/matita/library/nat/log.ma index e7fd12f15..ca9eac304 100644 --- a/helm/matita/library/nat/log.ma +++ b/helm/matita/library/nat/log.ma @@ -89,7 +89,7 @@ apply plog_aux_to_Prop. assumption. qed. (* questo va spostato in primes1.ma *) -theorem plog_exp: \forall n,m,i. O < m \to \not (mod n m = O) \to +theorem plog_exp: \forall n,m,i. O < m \to \lnot (mod n m = O) \to \forall p. i \le p \to plog_aux p (m \sup i * n) m = pair nat nat i n. intros 5. elim i. diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma index 7240b7d09..cbf92049c 100644 --- a/helm/matita/library/nat/minus.ma +++ b/helm/matita/library/nat/minus.ma @@ -235,7 +235,7 @@ theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p). intros. -cut m+p \le n \or \not m+p \le n. +cut m+p \le n \or \lnot m+p \le n. elim Hcut. symmetry.apply plus_to_minus.assumption. rewrite > assoc_plus.rewrite > sym_plus p.rewrite < plus_minus_m_m. diff --git a/helm/matita/library/nat/nth_prime.ma b/helm/matita/library/nat/nth_prime.ma index f165705ac..1f3a57d7f 100644 --- a/helm/matita/library/nat/nth_prime.ma +++ b/helm/matita/library/nat/nth_prime.ma @@ -39,11 +39,11 @@ normalize.reflexivity. qed. *) theorem smallest_factor_fact: \forall n:nat. -n < smallest_factor (S (n !)). +n < smallest_factor (S n!). intros. apply not_le_to_lt. -change with smallest_factor (S (n !)) \le n \to False.intro. -apply not_divides_S_fact n (smallest_factor(S (n !))). +change with smallest_factor (S n!) \le n \to False.intro. +apply not_divides_S_fact n (smallest_factor(S n!)). apply lt_SO_smallest_factor. simplify.apply le_S_S.apply le_SO_fact. assumption. @@ -52,19 +52,19 @@ simplify.apply le_S_S.apply le_O_n. qed. theorem ex_prime: \forall n. (S O) \le n \to \exists m. -n < m \land m \le (S (n !)) \land (prime m). +n < m \land m \le S n! \land (prime m). intros. elim H. apply ex_intro nat ? (S(S O)). split.split.apply le_n (S(S O)). apply le_n (S(S O)).apply primeb_to_Prop (S(S O)). -apply ex_intro nat ? (smallest_factor (S ((S n1) !))). +apply ex_intro nat ? (smallest_factor (S (S n1)!)). split.split. apply smallest_factor_fact. apply le_smallest_factor_n. (* Andrea: ancora hint non lo trova *) apply prime_smallest_factor_n. -change with (S(S O)) \le S ((S n1) !). +change with (S(S O)) \le S (S n1)!. apply le_S.apply le_SSO_fact. simplify.apply le_S_S.assumption. qed. @@ -74,7 +74,7 @@ match n with [ O \Rightarrow (S(S O)) | (S p) \Rightarrow let previous_prime \def (nth_prime p) in - let upper_bound \def S (previous_prime !) in + let upper_bound \def S previous_prime! in min_aux (upper_bound - (S previous_prime)) upper_bound primeb]. (* it works, but nth_prime 4 takes already a few minutes - @@ -100,13 +100,13 @@ apply primeb_to_Prop (S(S O)). intro. change with let previous_prime \def (nth_prime m) in -let upper_bound \def S (previous_prime !) in +let upper_bound \def S previous_prime! in prime (min_aux (upper_bound - (S previous_prime)) upper_bound primeb). apply primeb_true_to_prime. apply f_min_aux_true. -apply ex_intro nat ? (smallest_factor (S ((nth_prime m) !))). +apply ex_intro nat ? (smallest_factor (S (nth_prime m)!)). split.split. -cut S ((nth_prime m) !)-(S ((nth_prime m) !) - (S (nth_prime m))) = (S (nth_prime m)). +cut S (nth_prime m)!-(S (nth_prime m)! - (S (nth_prime m))) = (S (nth_prime m)). rewrite > Hcut.exact smallest_factor_fact (nth_prime m). (* maybe we could factorize this proof *) apply plus_to_minus. @@ -117,7 +117,7 @@ apply le_n_fact_n. apply le_smallest_factor_n. apply prime_to_primeb_true. apply prime_smallest_factor_n. -change with (S(S O)) \le S ((nth_prime m) !). +change with (S(S O)) \le S (nth_prime m)!. apply le_S_S.apply le_SO_fact. qed. @@ -127,7 +127,7 @@ change with \forall n:nat. (nth_prime n) < (nth_prime (S n)). intros. change with let previous_prime \def (nth_prime n) in -let upper_bound \def S (previous_prime !) in +let upper_bound \def S previous_prime! in (S previous_prime) \le min_aux (upper_bound - (S previous_prime)) upper_bound primeb. intros. cut upper_bound - (upper_bound -(S previous_prime)) = (S previous_prime). @@ -168,13 +168,13 @@ exact lt_nth_prime_n_nth_prime_Sn.assumption. qed. theorem lt_nth_prime_to_not_prime: \forall n,m. nth_prime n < m \to m < nth_prime (S n) -\to \not (prime m). +\to \lnot (prime m). intros. apply primeb_false_to_not_prime. letin previous_prime \def nth_prime n. -letin upper_bound \def S (previous_prime !). +letin upper_bound \def S previous_prime!. apply lt_min_aux_to_false primeb upper_bound (upper_bound - (S previous_prime)) m. -cut S ((nth_prime n) !)-(S ((nth_prime n) !) - (S (nth_prime n))) = (S (nth_prime n)). +cut S (nth_prime n)!-(S (nth_prime n)! - (S (nth_prime n))) = (S (nth_prime n)). rewrite > Hcut.assumption. apply plus_to_minus. apply le_minus_m. diff --git a/helm/matita/library/nat/primes.ma b/helm/matita/library/nat/primes.ma index 505d3de49..515388917 100644 --- a/helm/matita/library/nat/primes.ma +++ b/helm/matita/library/nat/primes.ma @@ -22,6 +22,10 @@ include "nat/factorial.ma". inductive divides (n,m:nat) : Prop \def witness : \forall p:nat.m = times n p \to divides n m. +interpretation "divides" 'divides n m = (cic:/matita/nat/primes/divides.ind#xpointer(1/1) n m). +interpretation "not divides" 'ndivides n m = + (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/primes/divides.ind#xpointer(1/1) n m)). + theorem reflexive_divides : reflexive nat divides. simplify. intros. @@ -29,7 +33,7 @@ exact witness x x (S O) (times_n_SO x). qed. theorem divides_to_div_mod_spec : -\forall n,m. O < n \to divides n m \to div_mod_spec m n (div m n) O. +\forall n,m. O < n \to n \divides m \to div_mod_spec m n (div m n) O. intros.elim H1.rewrite > H2. constructor 1.assumption. apply lt_O_n_elim n H.intros. @@ -38,7 +42,7 @@ rewrite > div_times.apply sym_times. qed. theorem div_mod_spec_to_div : -\forall n,m,p. div_mod_spec m n p O \to divides n m. +\forall n,m,p. div_mod_spec m n p O \to n \divides m. intros.elim H. apply witness n m p. rewrite < sym_times. @@ -46,14 +50,14 @@ rewrite > plus_n_O (p*n).assumption. qed. theorem divides_to_mod_O: -\forall n,m. O < n \to divides n m \to (mod m n) = O. +\forall n,m. O < n \to n \divides m \to (mod m n) = O. intros.apply div_mod_spec_to_eq2 m n (div m n) (mod m n) (div m n) O. apply div_mod_spec_div_mod.assumption. apply divides_to_div_mod_spec.assumption.assumption. qed. theorem mod_O_to_divides: -\forall n,m. O< n \to (mod m n) = O \to divides n m. +\forall n,m. O< n \to (mod m n) = O \to n \divides m. intros. apply witness n m (div m n). rewrite > plus_n_O (n*div m n). @@ -64,16 +68,16 @@ apply div_mod. assumption. qed. -theorem divides_n_O: \forall n:nat. divides n O. +theorem divides_n_O: \forall n:nat. n \divides O. intro. apply witness n O O.apply times_n_O. qed. -theorem divides_SO_n: \forall n:nat. divides (S O) n. +theorem divides_SO_n: \forall n:nat. (S O) \divides n. intro. apply witness (S O) n n. simplify.apply plus_n_O. qed. theorem divides_plus: \forall n,p,q:nat. -divides n p \to divides n q \to divides n (p+q). +n \divides p \to n \divides q \to n \divides p+q. intros. elim H.elim H1. apply witness n (p+q) (n2+n1). rewrite > H2.rewrite > H3.apply sym_eq.apply distr_times_plus. @@ -87,7 +91,7 @@ rewrite > H2.rewrite > H3.apply sym_eq.apply distr_times_minus. qed. theorem divides_times: \forall n,m,p,q:nat. -divides n p \to divides m q \to divides (n*m) (p*q). +n \divides p \to m \divides q \to n*m \divides p*q. intros. elim H.elim H1. apply witness (n*m) (p*q) (n2*n1). rewrite > H2.rewrite > H3. @@ -102,7 +106,7 @@ apply sym_eq. apply assoc_times. qed. theorem transitive_divides: \forall n,m,p. -divides n m \to divides m p \to divides n p. +n \divides m \to m \divides p \to n \divides p. intros. elim H.elim H1. apply witness n p (n2*n1). rewrite > H3.rewrite > H2. @@ -110,7 +114,7 @@ apply assoc_times. qed. (* divides le *) -theorem divides_to_le : \forall n,m. O < m \to divides n m \to n \le m. +theorem divides_to_le : \forall n,m. O < m \to n \divides m \to n \le m. intros. elim H1.rewrite > H2.cut O < n2. apply lt_O_n_elim n2 Hcut.intro.rewrite < sym_times. simplify.rewrite < sym_plus. @@ -123,7 +127,7 @@ apply not_le_Sn_n O. apply le_O_n. qed. -theorem divides_to_lt_O : \forall n,m. O < m \to divides n m \to O < n. +theorem divides_to_lt_O : \forall n,m. O < m \to n \divides m \to O < n. intros.elim H1. elim le_to_or_lt_eq O n (le_O_n n). assumption. @@ -139,13 +143,13 @@ definition divides_b : nat \to nat \to bool \def theorem divides_b_to_Prop : \forall n,m:nat. O < n \to match divides_b n m with -[ true \Rightarrow divides n m -| false \Rightarrow \lnot (divides n m)]. +[ true \Rightarrow n \divides m +| false \Rightarrow n \ndivides m]. intros. change with match eqb (mod m n) O with -[ true \Rightarrow divides n m -| false \Rightarrow \lnot (divides n m)]. +[ true \Rightarrow n \divides m +| false \Rightarrow n \ndivides m]. apply eqb_elim. intro.simplify.apply mod_O_to_divides.assumption.assumption. intro.simplify.intro.apply H1.apply divides_to_mod_O.assumption.assumption. @@ -153,65 +157,65 @@ qed. theorem divides_b_true_to_divides : \forall n,m:nat. O < n \to -(divides_b n m = true ) \to divides n m. +(divides_b n m = true ) \to n \divides m. intros. change with match true with -[ true \Rightarrow divides n m -| false \Rightarrow \lnot (divides n m)]. +[ true \Rightarrow n \divides m +| false \Rightarrow n \ndivides m]. rewrite < H1.apply divides_b_to_Prop. assumption. qed. theorem divides_b_false_to_not_divides : \forall n,m:nat. O < n \to -(divides_b n m = false ) \to \lnot (divides n m). +(divides_b n m = false ) \to n \ndivides m. intros. change with match false with -[ true \Rightarrow divides n m -| false \Rightarrow \lnot (divides n m)]. +[ true \Rightarrow n \divides m +| false \Rightarrow n \ndivides m]. rewrite < H1.apply divides_b_to_Prop. assumption. qed. theorem decidable_divides: \forall n,m:nat.O < n \to -decidable (divides n m). -intros.change with (divides n m) \lor \not (divides n m). +decidable (n \divides m). +intros.change with (n \divides m) \lor n \ndivides m. cut match divides_b n m with -[ true \Rightarrow divides n m -| false \Rightarrow \not (divides n m)] \to (divides n m) \lor \not (divides n m). +[ true \Rightarrow n \divides m +| false \Rightarrow n \ndivides m] \to n \divides m \lor n \ndivides m. apply Hcut.apply divides_b_to_Prop.assumption. elim (divides_b n m).left.apply H1.right.apply H1. qed. theorem divides_to_divides_b_true : \forall n,m:nat. O < n \to -divides n m \to divides_b n m = true. +n \divides m \to divides_b n m = true. intros. cut match (divides_b n m) with -[ true \Rightarrow (divides n m) -| false \Rightarrow \not (divides n m)] \to ((divides_b n m) = true). +[ true \Rightarrow n \divides m +| false \Rightarrow n \ndivides m] \to ((divides_b n m) = true). apply Hcut.apply divides_b_to_Prop.assumption. elim divides_b n m.reflexivity. -absurd (divides n m).assumption.assumption. +absurd (n \divides m).assumption.assumption. qed. theorem not_divides_to_divides_b_false: \forall n,m:nat. O < n \to -\not(divides n m) \to (divides_b n m) = false. +\lnot(n \divides m) \to (divides_b n m) = false. intros. cut match (divides_b n m) with -[ true \Rightarrow (divides n m) -| false \Rightarrow \not (divides n m)] \to ((divides_b n m) = false). +[ true \Rightarrow n \divides m +| false \Rightarrow n \ndivides m] \to ((divides_b n m) = false). apply Hcut.apply divides_b_to_Prop.assumption. elim divides_b n m. -absurd (divides n m).assumption.assumption. +absurd (n \divides m).assumption.assumption. reflexivity. qed. (* divides and pi *) theorem divides_f_pi_f : \forall f:nat \to nat.\forall n,i:nat. -i < n \to divides (f i) (pi n f). +i < n \to f i \divides pi n f. intros 3.elim n.apply False_ind.apply not_le_Sn_O i H. simplify. apply le_n_Sm_elim (S i) n1 H1. @@ -237,23 +241,23 @@ qed. (* divides and fact *) theorem divides_fact : \forall n,i:nat. -O < i \to i \le n \to divides i (n !). +O < i \to i \le n \to i \divides n!. intros 3.elim n.absurd O H3. -apply witness ? ? (n1 !).reflexivity. +apply witness ? ? n1!.reflexivity. qed. theorem mod_S_fact: \forall n,i:nat. -(S O) < i \to i \le n \to mod (S (n !)) i = (S O). -intros.cut mod (n !) i = O. +(S O) < i \to i \le n \to mod (S n!) i = (S O). +intros.cut mod n! i = O. rewrite < Hcut. apply mod_S.apply trans_lt O (S O).apply le_n (S O).assumption. rewrite > Hcut.assumption. @@ -263,11 +267,11 @@ assumption. qed. theorem not_divides_S_fact: \forall n,i:nat. -(S O) < i \to i \le n \to \not (divides i (S (n !))). +(S O) < i \to i \le n \to i \ndivides S n!. intros. apply divides_b_false_to_not_divides. apply trans_lt O (S O).apply le_n (S O).assumption. -change with (eqb (mod (S (n !)) i) O) = false. +change with (eqb (mod (S n!) i) O) = false. rewrite > mod_S_fact.simplify.reflexivity. assumption.assumption. qed. @@ -275,7 +279,7 @@ qed. (* prime *) definition prime : nat \to Prop \def \lambda n:nat. (S O) < n \land -(\forall m:nat. divides m n \to (S O) < m \to m = n). +(\forall m:nat. m \divides n \to (S O) < m \to m = n). theorem not_prime_O: \lnot (prime O). simplify.intro.elim H.apply not_le_Sn_O (S O) H1. @@ -337,7 +341,7 @@ apply le_S_S.apply le_O_n. qed. theorem divides_smallest_factor_n : -\forall n:nat. O < n \to divides (smallest_factor n) n. +\forall n:nat. O < n \to smallest_factor n \divides n. intro. apply nat_case n.intro.apply False_ind.apply not_le_Sn_O O H. intro.apply nat_case m.intro. simplify. @@ -368,7 +372,7 @@ simplify.apply le_S_S.apply le_O_n. qed. theorem lt_smallest_factor_to_not_divides: \forall n,i:nat. -(S O) < n \to (S O) < i \to i < (smallest_factor n) \to \lnot (divides i n). +(S O) < n \to (S O) < i \to i < (smallest_factor n) \to i \ndivides n. intros 2. apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S O) H. intro.apply nat_case m.intro. apply False_ind.apply not_le_Sn_n (S O) H. @@ -389,13 +393,13 @@ qed. theorem prime_smallest_factor_n : \forall n:nat. (S O) < n \to prime (smallest_factor n). intro. change with (S(S O)) \le n \to (S O) < (smallest_factor n) \land -(\forall m:nat. divides m (smallest_factor n) \to (S O) < m \to m = (smallest_factor n)). +(\forall m:nat. m \divides smallest_factor n \to (S O) < m \to m = (smallest_factor n)). intro.split. apply lt_SO_smallest_factor.assumption. intros. cut le m (smallest_factor n). elim le_to_or_lt_eq m (smallest_factor n) Hcut. -absurd divides m n. +absurd m \divides n. apply transitive_divides m (smallest_factor n). assumption. apply divides_smallest_factor_n. @@ -417,7 +421,7 @@ intro.apply nat_case m.intro.apply False_ind.apply not_prime_SO H. intro. change with (S O) < (S(S m1)) \land -(\forall m:nat. divides m (S(S m1)) \to (S O) < m \to m = (S(S m1))) \to +(\forall m:nat. m \divides S(S m1) \to (S O) < m \to m = (S(S m1))) \to smallest_factor (S(S m1)) = (S(S m1)). intro.elim H.apply H2. apply divides_smallest_factor_n. @@ -455,7 +459,7 @@ qed. *) theorem primeb_to_Prop: \forall n. match primeb n with [ true \Rightarrow prime n -| false \Rightarrow \not (prime n)]. +| false \Rightarrow \lnot (prime n)]. intro. apply nat_case n.simplify.intro.elim H.apply not_le_Sn_O (S O) H1. intro.apply nat_case m.simplify.intro.elim H.apply not_le_Sn_n (S O) H1. @@ -463,13 +467,13 @@ intro. change with match eqb (smallest_factor (S(S m1))) (S(S m1)) with [ true \Rightarrow prime (S(S m1)) -| false \Rightarrow \not (prime (S(S m1)))]. +| false \Rightarrow \lnot (prime (S(S m1)))]. apply eqb_elim (smallest_factor (S(S m1))) (S(S m1)). intro.change with prime (S(S m1)). rewrite < H. apply prime_smallest_factor_n. simplify.apply le_S_S.apply le_S_S.apply le_O_n. -intro.change with \not (prime (S(S m1))). +intro.change with \lnot (prime (S(S m1))). change with prime (S(S m1)) \to False. intro.apply H. apply prime_to_smallest_factor. @@ -481,27 +485,27 @@ primeb n = true \to prime n. intros.change with match true with [ true \Rightarrow prime n -| false \Rightarrow \not (prime n)]. +| false \Rightarrow \lnot (prime n)]. rewrite < H. apply primeb_to_Prop. qed. theorem primeb_false_to_not_prime : \forall n:nat. -primeb n = false \to \not (prime n). +primeb n = false \to \lnot (prime n). intros.change with match false with [ true \Rightarrow prime n -| false \Rightarrow \not (prime n)]. +| false \Rightarrow \lnot (prime n)]. rewrite < H. apply primeb_to_Prop. qed. theorem decidable_prime : \forall n:nat.decidable (prime n). -intro.change with (prime n) \lor \not (prime n). +intro.change with (prime n) \lor \lnot (prime n). cut match primeb n with [ true \Rightarrow prime n -| false \Rightarrow \not (prime n)] \to (prime n) \lor \not (prime n). +| false \Rightarrow \lnot (prime n)] \to (prime n) \lor \lnot (prime n). apply Hcut.apply primeb_to_Prop. elim (primeb n).left.apply H.right.apply H. qed. @@ -511,18 +515,18 @@ prime n \to primeb n = true. intros. cut match (primeb n) with [ true \Rightarrow prime n -| false \Rightarrow \not (prime n)] \to ((primeb n) = true). +| false \Rightarrow \lnot (prime n)] \to ((primeb n) = true). apply Hcut.apply primeb_to_Prop. elim primeb n.reflexivity. absurd (prime n).assumption.assumption. qed. theorem not_prime_to_primeb_false: \forall n:nat. -\not(prime n) \to primeb n = false. +\lnot(prime n) \to primeb n = false. intros. cut match (primeb n) with [ true \Rightarrow prime n -| false \Rightarrow \not (prime n)] \to ((primeb n) = false). +| false \Rightarrow \lnot (prime n)] \to ((primeb n) = false). apply Hcut.apply primeb_to_Prop. elim primeb n. absurd (prime n).assumption.assumption. -- 2.39.2