X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fprimes.ma;h=6913562439f6e0f45d195241fa7fcecd8d3bc353;hb=8b55faddb06e3c4b0a13839210bb49170939b33e;hp=515388917482d366cffd19c7dc808bf4424a2d87;hpb=30b7e65d641fe7243c4f36ed448f56360a1c5e1c;p=helm.git diff --git a/helm/matita/library/nat/primes.ma b/helm/matita/library/nat/primes.ma index 515388917..691356243 100644 --- a/helm/matita/library/nat/primes.ma +++ b/helm/matita/library/nat/primes.ma @@ -33,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 n \divides 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 (m / n) O. intros.elim H1.rewrite > H2. constructor 1.assumption. apply lt_O_n_elim n H.intros. @@ -41,7 +41,7 @@ rewrite < plus_n_O. rewrite > div_times.apply sym_times. qed. -theorem div_mod_spec_to_div : +theorem div_mod_spec_to_divides : \forall n,m,p. div_mod_spec m n p O \to n \divides m. intros.elim H. apply witness n m p. @@ -50,17 +50,17 @@ rewrite > plus_n_O (p*n).assumption. qed. theorem divides_to_mod_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. +\forall n,m. O < n \to n \divides m \to (m \mod n) = O. +intros.apply div_mod_spec_to_eq2 m n (m / n) (m \mod n) (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 n \divides m. +\forall n,m. O< n \to (m \mod n) = O \to n \divides m. intros. -apply witness n m (div m n). -rewrite > plus_n_O (n*div m n). +apply witness n m (m / n). +rewrite > plus_n_O (n * (m / n)). rewrite < H1. rewrite < sym_times. (* Andrea: perche' hint non lo trova ?*) @@ -72,6 +72,10 @@ theorem divides_n_O: \forall n:nat. n \divides O. intro. apply witness n O O.apply times_n_O. qed. +theorem divides_n_n: \forall n:nat. n \divides n. +intro. apply witness n n (S O).apply times_n_SO. +qed. + theorem divides_SO_n: \forall n:nat. (S O) \divides n. intro. apply witness (S O) n n. simplify.apply plus_n_O. qed. @@ -105,14 +109,47 @@ rewrite > sym_times n2 m.apply assoc_times. apply sym_eq. apply assoc_times. qed. -theorem transitive_divides: \forall n,m,p. -n \divides m \to m \divides p \to n \divides p. +theorem transitive_divides: transitive ? divides. +unfold. intros. -elim H.elim H1. apply witness n p (n2*n1). +elim H.elim H1. apply witness x z (n2*n). rewrite > H3.rewrite > H2. apply assoc_times. qed. +variant trans_divides: \forall n,m,p. + n \divides m \to m \divides p \to n \divides p \def transitive_divides. + +theorem eq_mod_to_divides:\forall n,m,p. O< p \to +mod n p = mod m p \to divides p (n-m). +intros. +cut n \le m \or \not n \le m. +elim Hcut. +cut n-m=O. +rewrite > Hcut1. +apply witness p O O. +apply times_n_O. +apply eq_minus_n_m_O. +assumption. +apply witness p (n-m) ((div n p)-(div m p)). +rewrite > distr_times_minus. +rewrite > sym_times. +rewrite > sym_times p. +cut (div n p)*p = n - (mod n p). +rewrite > Hcut1. +rewrite > eq_minus_minus_minus_plus. +rewrite > sym_plus. +rewrite > H1. +rewrite < div_mod.reflexivity. +assumption. +apply sym_eq. +apply plus_to_minus. +rewrite > sym_plus. +apply div_mod. +assumption. +apply decidable_le n m. +qed. + (* divides le *) 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. @@ -138,7 +175,7 @@ qed. (* boolean divides *) definition divides_b : nat \to nat \to bool \def -\lambda n,m :nat. (eqb (mod m n) O). +\lambda n,m :nat. (eqb (m \mod n) O). theorem divides_b_to_Prop : \forall n,m:nat. O < n \to @@ -147,7 +184,7 @@ match divides_b n m with | false \Rightarrow n \ndivides m]. intros. change with -match eqb (mod m n) O with +match eqb (m \mod n) O with [ true \Rightarrow n \divides m | false \Rightarrow n \ndivides m]. apply eqb_elim. @@ -214,30 +251,33 @@ reflexivity. qed. (* divides and pi *) -theorem divides_f_pi_f : \forall f:nat \to nat.\forall n,i:nat. -i < n \to f i \divides pi n f. -intros 3.elim n.apply False_ind.apply not_le_Sn_O i H. +theorem divides_f_pi_f : \forall f:nat \to nat.\forall n,m,i:nat. +m \le i \to i \le n+m \to f i \divides pi n f m. +intros 5.elim n.simplify. +cut i = m.rewrite < Hcut.apply divides_n_n. +apply antisymmetric_le.assumption.assumption. simplify. -apply le_n_Sm_elim (S i) n1 H1. -intro. -apply transitive_divides ? (pi n1 f). -apply H.simplify.apply le_S_S_to_le. assumption. -apply witness ? ? (f n1).apply sym_times. -intro.cut i = n1. -rewrite > Hcut. -apply witness ? ? (pi n1 f).reflexivity. -apply inj_S.assumption. +cut i < S n1+m \lor i = S n1 + m. +elim Hcut. +apply transitive_divides ? (pi n1 f m). +apply H1.apply le_S_S_to_le. assumption. +apply witness ? ? (f (S n1+m)).apply sym_times. +rewrite > H3. +apply witness ? ? (pi n1 f m).reflexivity. +apply le_to_or_lt_eq.assumption. qed. +(* theorem mod_S_pi: \forall f:nat \to nat.\forall n,i:nat. -i < n \to (S O) < (f i) \to mod (S (pi n f)) (f i) = (S O). -intros.cut mod (pi n f) (f i) = O. +i < n \to (S O) < (f i) \to (S (pi n f)) \mod (f i) = (S O). +intros.cut (pi n f) \mod (f i) = O. rewrite < Hcut. apply mod_S.apply trans_lt O (S O).apply le_n (S O).assumption. rewrite > Hcut.assumption. apply divides_to_mod_O.apply trans_lt O (S O).apply le_n (S O).assumption. apply divides_f_pi_f.assumption. qed. +*) (* divides and fact *) theorem divides_fact : \forall n,i:nat. @@ -256,8 +296,8 @@ 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 (S n!) \mod i = (S O). +intros.cut n! \mod i = O. rewrite < Hcut. apply mod_S.apply trans_lt O (S O).apply le_n (S O).assumption. rewrite > Hcut.assumption. @@ -271,7 +311,7 @@ theorem not_divides_S_fact: \forall n,i:nat. 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 ((S n!) \mod i) O) = false. rewrite > mod_S_fact.simplify.reflexivity. assumption.assumption. qed. @@ -297,7 +337,7 @@ match n with | (S p) \Rightarrow match p with [ O \Rightarrow (S O) - | (S q) \Rightarrow min_aux q (S(S q)) (\lambda m.(eqb (mod (S(S q)) m) O))]]. + | (S q) \Rightarrow min_aux q (S(S q)) (\lambda m.(eqb ((S(S q)) \mod m) O))]]. (* it works ! theorem example1 : smallest_prime_factor (S(S(S O))) = (S(S(S O))). @@ -319,13 +359,13 @@ 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. intros. change with -S O < min_aux m1 (S(S m1)) (\lambda m.(eqb (mod (S(S m1)) m) O)). +S O < min_aux m1 (S(S m1)) (\lambda m.(eqb ((S(S m1)) \mod m) O)). apply lt_to_le_to_lt ? (S (S O)). apply le_n (S(S O)). cut (S(S O)) = (S(S m1)) - m1. rewrite > Hcut. apply le_min_aux. -apply sym_eq.apply plus_to_minus.apply le_S.apply le_n_Sn. +apply sym_eq.apply plus_to_minus. rewrite < sym_plus.simplify.reflexivity. qed. @@ -350,8 +390,8 @@ intros. apply divides_b_true_to_divides. apply lt_O_smallest_factor ? H. change with -eqb (mod (S(S m1)) (min_aux m1 (S(S m1)) - (\lambda m.(eqb (mod (S(S m1)) m) O)))) O = true. +eqb ((S(S m1)) \mod (min_aux m1 (S(S m1)) + (\lambda m.(eqb ((S(S m1)) \mod m) O)))) O = true. apply f_min_aux_true. apply ex_intro nat ? (S(S m1)). split.split. @@ -379,13 +419,12 @@ intro.apply nat_case m.intro. apply False_ind.apply not_le_Sn_n (S O) H. 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(S m1)) i) O) = false. +change with (eqb ((S(S m1)) \mod i) O) = false. apply lt_min_aux_to_false -(\lambda i:nat.eqb (mod (S(S m1)) i) O) (S(S m1)) m1 i. +(\lambda i:nat.eqb ((S(S m1)) \mod i) O) (S(S m1)) m1 i. cut (S(S O)) = (S(S m1)-m1). rewrite < Hcut.exact H1. apply sym_eq. apply plus_to_minus. -apply le_S.apply le_n_Sn. rewrite < sym_plus.simplify.reflexivity. exact H2. qed.