From 7273c698dd60c1a8a0f35b44376acb548c6a4a33 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 27 Sep 2005 16:17:16 +0000 Subject: [PATCH] New entry: fermat's little theorem (almost complete). Corrected plus_to_minus, sparing an hypothesis. --- helm/matita/contribs/LAMBDA-TYPES/.depend | 12 +-- helm/matita/library/nat/div_and_mod.ma | 2 - .../library/nat/fermat_little_theorem.ma | 90 ++++++++++++++++ helm/matita/library/nat/gcd.ma | 6 +- helm/matita/library/nat/minus.ma | 12 +-- helm/matita/library/nat/permutation.ma | 102 +++++++++++------- helm/matita/library/nat/primes.ma | 33 +++++- helm/matita/library/nat/sigma_and_pi.ma | 8 ++ 8 files changed, 208 insertions(+), 57 deletions(-) create mode 100644 helm/matita/library/nat/fermat_little_theorem.ma diff --git a/helm/matita/contribs/LAMBDA-TYPES/.depend b/helm/matita/contribs/LAMBDA-TYPES/.depend index 863e1349e..98ea66214 100644 --- a/helm/matita/contribs/LAMBDA-TYPES/.depend +++ b/helm/matita/contribs/LAMBDA-TYPES/.depend @@ -1,6 +1,6 @@ -/home/sacerdot/miohelm/matita/.matita/xml/matita/LAMBDA-TYPES/tlt_defs.moo: ./tlt_defs.ma /home/sacerdot/miohelm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo -./tlt_defs.mo: /home/sacerdot/miohelm/matita/.matita/xml/matita/LAMBDA-TYPES/tlt_defs.moo -/home/sacerdot/miohelm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo: ./terms_defs.ma -./terms_defs.mo: /home/sacerdot/miohelm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo -/home/sacerdot/miohelm/matita/.matita/xml/matita/LAMBDA-TYPES/lref_map_defs.moo: ./lref_map_defs.ma /home/sacerdot/miohelm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo -./lref_map_defs.mo: /home/sacerdot/miohelm/matita/.matita/xml/matita/LAMBDA-TYPES/lref_map_defs.moo +/home/andrea/helm/matita/.matita/xml/matita/LAMBDA-TYPES/tlt_defs.moo: ./tlt_defs.ma /home/andrea/helm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo +./tlt_defs.mo: /home/andrea/helm/matita/.matita/xml/matita/LAMBDA-TYPES/tlt_defs.moo +/home/andrea/helm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo: ./terms_defs.ma +./terms_defs.mo: /home/andrea/helm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo +/home/andrea/helm/matita/.matita/xml/matita/LAMBDA-TYPES/lref_map_defs.moo: ./lref_map_defs.ma /home/andrea/helm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo +./lref_map_defs.mo: /home/andrea/helm/matita/.matita/xml/matita/LAMBDA-TYPES/lref_map_defs.moo diff --git a/helm/matita/library/nat/div_and_mod.ma b/helm/matita/library/nat/div_and_mod.ma index 520e99ea8..71734fad3 100644 --- a/helm/matita/library/nat/div_and_mod.ma +++ b/helm/matita/library/nat/div_and_mod.ma @@ -144,7 +144,6 @@ rewrite > sym_times. rewrite < H5. rewrite < sym_times. apply plus_to_minus. -apply eq_plus_to_le ? ? ? H3. apply H3. apply le_times_r. apply lt_to_le. @@ -171,7 +170,6 @@ rewrite > sym_times. rewrite < H3. rewrite < sym_times. apply plus_to_minus. -apply eq_plus_to_le ? ? ? H5. apply H5. apply le_times_r. apply lt_to_le. diff --git a/helm/matita/library/nat/fermat_little_theorem.ma b/helm/matita/library/nat/fermat_little_theorem.ma new file mode 100644 index 000000000..aafdc2f19 --- /dev/null +++ b/helm/matita/library/nat/fermat_little_theorem.ma @@ -0,0 +1,90 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/nat/fermat_little_theorem". + +include "nat/gcd.ma". +include "nat/permutation.ma". + +theorem permut_mod: \forall p,a:nat. prime p \to +\lnot divides p a\to permut (\lambda n.(mod (a*n) p)) (pred p). +unfold permut.intros. +split.intros.apply le_S_S_to_le. +apply trans_le ? p. +change with mod (a*i) p < p. +apply lt_mod_m_m. +simplify in H.elim H. +simplify.apply trans_le ? (S (S O)). +apply le_n_Sn.assumption. +rewrite < S_pred.apply le_n. +unfold prime in H. +elim H. +apply trans_lt ? (S O).simplify.apply le_n.assumption. +unfold injn.intros. +apply nat_compare_elim i j. +(* i < j *) +intro. +absurd j-i \lt p. +simplify. +rewrite > S_pred p. +apply le_S_S. +apply le_plus_to_minus. +apply trans_le ? (pred p).assumption. +rewrite > sym_plus. +apply le_plus_n. +unfold prime in H. +elim H. +apply trans_lt ? (S O).simplify.apply le_n.assumption. +apply le_to_not_lt p (j-i). +apply divides_to_le.simplify. +apply le_SO_minus.assumption. +cut divides p a \lor divides p (j-i). +elim Hcut.apply False_ind.apply H1.assumption.assumption. +apply divides_times_to_divides.assumption. +rewrite > distr_times_minus. +apply eq_mod_to_divides. +unfold prime in H. +elim H. +apply trans_lt ? (S O).simplify.apply le_n.assumption. +apply sym_eq. +apply H4. +(* i = j *) +intro. assumption. +(* j < i *) +intro. +absurd i-j \lt p. +simplify. +rewrite > S_pred p. +apply le_S_S. +apply le_plus_to_minus. +apply trans_le ? (pred p).assumption. +rewrite > sym_plus. +apply le_plus_n. +unfold prime in H. +elim H. +apply trans_lt ? (S O).simplify.apply le_n.assumption. +apply le_to_not_lt p (i-j). +apply divides_to_le.simplify. +apply le_SO_minus.assumption. +cut divides p a \lor divides p (i-j). +elim Hcut.apply False_ind.apply H1.assumption.assumption. +apply divides_times_to_divides.assumption. +rewrite > distr_times_minus. +apply eq_mod_to_divides. +unfold prime in H. +elim H. +apply trans_lt ? (S O).simplify.apply le_n.assumption. +apply H4. +qed. + diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma index 36c7a9659..eb1053feb 100644 --- a/helm/matita/library/nat/gcd.ma +++ b/helm/matita/library/nat/gcd.ma @@ -46,13 +46,9 @@ rewrite < assoc_times. rewrite < H4. apply sym_eq. apply plus_to_minus. -rewrite > div_mod m n in \vdash (? ? %). rewrite > sym_times. -apply eq_plus_to_le ? ? (m \mod n). -reflexivity. +apply div_mod. assumption. -rewrite > sym_times. -apply div_mod.assumption. qed. theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma index 3b39ed43f..8302f7ce5 100644 --- a/helm/matita/library/nat/minus.ma +++ b/helm/matita/library/nat/minus.ma @@ -88,14 +88,16 @@ apply H.elim H1. apply sym_plus. qed. -theorem plus_to_minus :\forall n,m,p:nat.m \leq n \to +theorem plus_to_minus :\forall n,m,p:nat. n = m+p \to n-m = p. intros. apply inj_plus_r m. -rewrite < H1. +rewrite < H. rewrite < sym_plus. symmetry. -apply plus_minus_m_m.assumption. +apply plus_minus_m_m.rewrite > H. +rewrite > sym_plus. +apply le_plus_n. qed. theorem minus_S_S : \forall n,m:nat. @@ -237,7 +239,7 @@ theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p). intros. cut m+p \le n \or m+p \nleq n. elim Hcut. - symmetry.apply plus_to_minus.assumption. + symmetry.apply plus_to_minus. rewrite > assoc_plus.rewrite > sym_plus p.rewrite < plus_minus_m_m. rewrite > sym_plus.rewrite < plus_minus_m_m. reflexivity. @@ -259,8 +261,6 @@ p+(n-m) = n-(m-p). intros. apply sym_eq. apply plus_to_minus. -apply le_plus_to_minus. -apply trans_le ? n.assumption.rewrite < sym_plus.apply le_plus_n. rewrite < assoc_plus. rewrite < plus_minus_m_m. rewrite < sym_plus. diff --git a/helm/matita/library/nat/permutation.ma b/helm/matita/library/nat/permutation.ma index c64cb23de..3ea405245 100644 --- a/helm/matita/library/nat/permutation.ma +++ b/helm/matita/library/nat/permutation.ma @@ -17,23 +17,39 @@ set "baseuri" "cic:/matita/nat/permutation". include "nat/compare.ma". include "nat/sigma_and_pi.ma". +definition injn: (nat \to nat) \to nat \to Prop \def +\lambda f:nat \to nat.\lambda n:nat.\forall i,j:nat. +i \le n \to j \le n \to f i = f j \to i = j. + +theorem injn_Sn_n: \forall f:nat \to nat. \forall n:nat. +injn f (S n) \to injn f n.simplify. +intros.apply H. +apply le_S.assumption. +apply le_S.assumption. +assumption. +qed. + +theorem injective_to_injn: \forall f:nat \to nat. \forall n:nat. +injective nat nat f \to injn f n. +simplify.intros.apply H.assumption. +qed. + definition permut : (nat \to nat) \to nat \to Prop \def \lambda f:nat \to nat. \lambda m:nat. -\forall i:nat. i \le m \to (f i \le m \land -(\forall j:nat. f i = f j \to i = j)). +(\forall i:nat. i \le m \to f i \le m )\land injn f m. theorem permut_O_to_eq_O: \forall h:nat \to nat. permut h O \to (h O) = O. intros.unfold permut in H. -elim H O.apply sym_eq.apply le_n_O_to_eq. -assumption.apply le_n. +elim H.apply sym_eq.apply le_n_O_to_eq. +apply H1.apply le_n. qed. theorem permut_S_to_permut: \forall f:nat \to nat. \forall m:nat. permut f (S m) \to f (S m) = (S m) \to permut f m. unfold permut.intros. -elim H i. -elim H (S m).split. +elim H. +split.intros. cut f i < S m \lor f i = S m. elim Hcut. apply le_S_S_to_le.assumption. @@ -41,10 +57,10 @@ apply False_ind. apply not_le_Sn_n m. cut (S m) = i. rewrite > Hcut1.assumption. -apply H6.rewrite > H7.assumption. -apply le_to_or_lt_eq.assumption. -assumption.apply le_n. -apply le_S.assumption. +apply H3.apply le_n.apply le_S.assumption. +rewrite > H5.assumption. +apply le_to_or_lt_eq.apply H2.apply le_S.assumption. +apply injn_Sn_n f m H3. qed. (* transpositions *) @@ -126,21 +142,24 @@ theorem permut_transpose: \forall i,j,n:nat. i \le n \to j \le n \to permut (transpose i j) n. unfold permut.intros. split.unfold transpose. +intros. elim eqb i1 i.simplify.assumption. elim eqb i1 j.simplify.assumption. simplify.assumption. -apply inj_transpose. +apply injective_to_injn (transpose i j) n. +apply injective_transpose. qed. theorem permut_fg: \forall f,g:nat \to nat. \forall n:nat. permut f n \to permut g n \to permut (\lambda m.(f(g m))) n. unfold permut. intros. -split.simplify.elim H1 i. -elim H (g i).assumption.assumption.assumption. -intro.simplify.intros. -elim H1 i.apply H5. -elim H (g i). -apply H7.assumption.assumption.assumption. +elim H.elim H1. +split.intros.simplify.apply H2. +apply H4.assumption. +simplify.intros. +apply H5.assumption.assumption. +apply H3.apply H4.assumption.apply H4.assumption. +assumption. qed. theorem permut_transpose_l: @@ -204,19 +223,31 @@ qed. theorem permut_S_to_permut_transpose: \forall f:nat \to nat. \forall m:nat. permut f (S m) \to permut (\lambda n.transpose (f (S m)) (S m) (f n)) m. -intros. -cut permut (\lambda n.transpose (f (S m)) (S m) (f n)) (S m). -apply permut_S_to_permut.assumption. -simplify. -apply eqb_elim (f (S m)) (f (S m)).simplify. -intro.reflexivity. -intro.apply False_ind.apply H1.reflexivity. -apply permut_transpose_l. -unfold permut in H. -elim H (S m). -assumption.apply le_n. -apply le_n. -assumption. +unfold permut.intros. +elim H. +split.intros.simplify. +apply eqb_elim (f i) (f (S m)).simplify. +intro.apply False_ind. +cut i = (S m). +apply not_le_Sn_n m. +rewrite < Hcut.assumption. +apply H2.apply le_S.assumption.apply le_n.assumption. +intro.simplify. +apply eqb_elim (f i) (S m).simplify. +intro. +cut f (S m) \lt (S m) \lor f (S m) = (S m). +elim Hcut.apply le_S_S_to_le.assumption. +apply False_ind.apply H4.rewrite > H6.assumption. +apply le_to_or_lt_eq.apply H1.apply le_n. +intro.simplify. +cut f i \lt (S m) \lor f i = (S m). +elim Hcut.apply le_S_S_to_le.assumption. +apply False_ind.apply H5.assumption. +apply le_to_or_lt_eq.apply H1.apply le_S.assumption. +unfold injn.intros. +apply H2.apply le_S.assumption.apply le_S.assumption. +apply inj_transpose (f (S m)) (S m). +apply H5. qed. (* bounded bijectivity *) @@ -328,16 +359,15 @@ elim n.simplify.intros. apply ex_intro ? ? m. split.assumption. apply le_n_O_elim m ? (\lambda p. f p = p). -assumption. -elim H O.apply sym_eq. apply le_n_O_to_eq.assumption. -apply le_n. +assumption.unfold permut in H. +elim H.apply sym_eq. apply le_n_O_to_eq.apply H2.apply le_n. apply eq_to_bijn (\lambda p. (transpose (f (S n1)) (S n1)) (transpose (f (S n1)) (S n1) (f p))) f. intros.apply transpose_transpose. apply bijn_fg (transpose (f (S n1)) (S n1)). apply bijn_transpose. -simplify in H1. -elim H1 (S n1).assumption.apply le_n.apply le_n. +unfold permut in H1. +elim H1.apply H2.apply le_n.apply le_n. apply bijn_n_Sn. apply H. apply permut_S_to_permut_transpose. @@ -555,7 +585,7 @@ simplify.rewrite > permut_O_to_eq_O h.reflexivity.assumption. apply trans_eq ? ? (map_iter (S(S n1)) (\lambda m.g ((transpose (h (S n1)) (S n1)) m)) f a). apply eq_map_iter_transpose2 f H H1 (S n1) a ? ? g. unfold permut in H3. -elim H3 (S n1).assumption.apply le_n.apply le_n. +elim H3.apply H4.apply le_n.apply le_n. apply trans_eq ? ? (map_iter (S(S n1)) (\lambda m. (g(transpose (h (S n1)) (S n1) (transpose (h (S n1)) (S n1) (h m)))) )f a). diff --git a/helm/matita/library/nat/primes.ma b/helm/matita/library/nat/primes.ma index be3660187..1d0fed296 100644 --- a/helm/matita/library/nat/primes.ma +++ b/helm/matita/library/nat/primes.ma @@ -116,6 +116,36 @@ 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. @@ -328,7 +358,7 @@ 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. @@ -388,7 +418,6 @@ apply lt_min_aux_to_false 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. diff --git a/helm/matita/library/nat/sigma_and_pi.ma b/helm/matita/library/nat/sigma_and_pi.ma index 470bb9d69..6bd6af38c 100644 --- a/helm/matita/library/nat/sigma_and_pi.ma +++ b/helm/matita/library/nat/sigma_and_pi.ma @@ -14,6 +14,7 @@ set "baseuri" "cic:/matita/nat/sigma_and_pi". +include "nat/factorial.ma". include "nat/lt_arith.ma". let rec sigma n f \def @@ -47,3 +48,10 @@ apply eq_f2.apply H1.simplify. apply le_n. apply H.intros.apply H1. apply trans_lt ? n1.assumption.simplify.apply le_n. qed. + +theorem eq_fact_pi: \forall n. n! = pi n S. +intro.elim n. +simplify.reflexivity. +change with (S n1)*n1! = (S n1)*(pi n1 S). +apply eq_f.assumption. +qed. \ No newline at end of file -- 2.39.2