New entry: fermat's little theorem (almost complete).

Corrected plus_to_minus, sparing an hypothesis.

diff --git a/helm/matita/contribs/LAMBDA-TYPES/.depend b/helm/matita/contribs/LAMBDA-TYPES/.depend
index 863e1349e6feabe7b866d2f13994069f81f353ea..98ea662141f617831365e20ef1ffc938ee51208f 100644 (file)
--- 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 520e99ea8f1e7a7d58f0a964fdd9021076b17938..71734fad3a58ff17c619da36325bbd13dca6c415 100644 (file)
--- 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 (file)
index 0000000..aafdc2f
--- /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 36c7a96597fef1f5b83169d5b08af8c842ba30b4..eb1053feb78cb5e88a70a9154ff9af271f15e08b 100644 (file)
--- 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 3b39ed43f1faa363340d95fbfe24ef191c98f15d..8302f7ce5873aee8dc6f7893065068e0fb38feb7 100644 (file)
--- 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 c64cb23de3c0a7a7b2074a458fb9df4917323fef..3ea405245eb82bee9df4e6eff13cb246caa22ed3 100644 (file)
--- 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 be3660187d7d1b126c7c35adf04554fa09b65ea4..1d0fed2967ceb30b3beacac7446c8aa11194efb2 100644 (file)
--- 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 470bb9d69f7ea3992ff413b7f63ad7ff3879228f..6bd6af38c52eae0f4163938fd245f3bfa4e1b657 100644 (file)
--- 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