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

[helm.git] / helm / matita / library / nat / permutation.ma

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).