X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fpermutation.ma;h=3ea405245eb82bee9df4e6eff13cb246caa22ed3;hb=7273c698dd60c1a8a0f35b44376acb548c6a4a33;hp=0aea7b76177b8e3579368a631b77cf5c08c7ba64;hpb=c3b6e22034e3029195031d31c94983c381ae659b;p=helm.git diff --git a/helm/matita/library/nat/permutation.ma b/helm/matita/library/nat/permutation.ma index 0aea7b761..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,18 +359,17 @@ 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 H. apply permut_S_to_permut_transpose. assumption.simplify. rewrite > eqb_n_n (f (S n1)).simplify.reflexivity. @@ -469,17 +499,17 @@ apply nat_elim1 k. intro. apply nat_case m ?. intros. -apply eq_map_iter_transpose_i_Si f H H1 g n i. +apply eq_map_iter_transpose_i_Si ? H H1. exact H3. intros. apply trans_eq ? ? (map_iter (S n) (\lambda m. g (transpose i (S(m1 + i)) m)) f a). -apply H2 m1 ? g. +apply H2. simplify. apply le_n. apply trans_le ? (S(S (m1+i))). apply le_S.apply le_n.assumption. apply trans_eq ? ? (map_iter (S n) (\lambda m. g (transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m))) f a). -apply H2 O ? ? (S(m1+i)) ?. +apply H2 O ? ? (S(m1+i)). simplify.apply le_S_S.apply le_O_n. exact H3. apply trans_eq ? ? (map_iter (S n) (\lambda m. g @@ -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).