X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fpermutation.ma;h=5d99f657b52df9d29a51887906913931a4d147fd;hb=aeb7f0539398561dc84cadf38df14a051dd1ba75;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..5d99f657b 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. @@ -354,7 +384,7 @@ let rec invert_permut n f m \def |(S p) \Rightarrow invert_permut p f m]]. theorem invert_permut_f: \forall f:nat \to nat. \forall n,m:nat. -m \le n \to (\forall p:nat. f m = f p \to m = p) \to invert_permut n f (f m) = m. +m \le n \to injn f n\to invert_permut n f (f m) = m. intros 4. elim H. apply nat_case1 m. @@ -364,143 +394,250 @@ intros.simplify. rewrite > eqb_n_n (f (S m1)).simplify.reflexivity. simplify. rewrite > not_eq_to_eqb_false (f m) (f (S n1)). -simplify.apply H2.assumption. +simplify.apply H2. +apply injn_Sn_n. assumption. simplify.intro.absurd m = S n1. -apply H3.assumption.simplify.intro. +apply H3.apply le_S.assumption.apply le_n.assumption. +simplify.intro. apply not_le_Sn_n n1.rewrite < H5.assumption. qed. +theorem injective_invert_permut: \forall f:nat \to nat. \forall n:nat. +permut f n \to injn (invert_permut n f) n. +intros. +unfold injn.intros. +cut bijn f n. +unfold bijn in Hcut. +generalize in match Hcut i H1.intro. +generalize in match Hcut j H2.intro. +elim H4.elim H6. +elim H5.elim H9. +rewrite < H8. +rewrite < H11. +apply eq_f. +rewrite < invert_permut_f f n a. +rewrite < invert_permut_f f n a1. +rewrite > H8. +rewrite > H11. +assumption.assumption. +unfold permut in H.elim H. assumption. +assumption. +unfold permut in H.elim H. assumption. +apply permut_to_bijn.assumption. +qed. + +theorem permut_invert_permut: \forall f:nat \to nat. \forall n:nat. +permut f n \to permut (invert_permut n f) n. +intros.unfold permut.split. +intros.simplify.elim n. +simplify.elim eqb i (f O).simplify.apply le_n.simplify.apply le_n. +simplify.elim eqb i (f (S n1)).simplify.apply le_n. +simplify.apply le_S. assumption. +apply injective_invert_permut.assumption. +qed. + +theorem f_invert_permut: \forall f:nat \to nat. \forall n,m:nat. +m \le n \to permut f n\to f (invert_permut n f m) = m. +intros. +apply injective_invert_permut f n H1. +unfold permut in H1.elim H1. +apply H2. +cut permut (invert_permut n f) n.unfold permut in Hcut. +elim Hcut.apply H4.assumption. +apply permut_invert_permut.assumption.assumption. +(* uffa: lo ha espanso troppo *) +change with invert_permut n f (f (invert_permut n f m)) = invert_permut n f m. +apply invert_permut_f. +cut permut (invert_permut n f) n.unfold permut in Hcut. +elim Hcut.apply H2.assumption. +apply permut_invert_permut.assumption. +unfold permut in H1.elim H1.assumption. +qed. + +theorem permut_n_to_eq_n: \forall h:nat \to nat.\forall n:nat. +permut h n \to (\forall m:nat. m < n \to h m = m) \to h n = n. +intros.unfold permut in H.elim H. +cut invert_permut n h n < n \lor invert_permut n h n = n. +elim Hcut. +rewrite < f_invert_permut h n n in \vdash (? ? ? %). +apply eq_f. +rewrite < f_invert_permut h n n in \vdash (? ? % ?). +apply H1.assumption.apply le_n.assumption.apply le_n.assumption. +rewrite < H4 in \vdash (? ? % ?). +apply f_invert_permut h.apply le_n.assumption. +apply le_to_or_lt_eq. +cut permut (invert_permut n h) n. +unfold permut in Hcut.elim Hcut. +apply H4.apply le_n. +apply permut_invert_permut.assumption. +qed. + +theorem permut_n_to_le: \forall h:nat \to nat.\forall k,n:nat. +k \le n \to permut h n \to (\forall m:nat. m < k \to h m = m) \to +\forall j. k \le j \to j \le n \to k \le h j. +intros.unfold permut in H1.elim H1. +cut h j < k \lor \not(h j < k). +elim Hcut.absurd k \le j.assumption. +apply lt_to_not_le. +cut h j = j.rewrite < Hcut1.assumption. +apply H6.apply H5.assumption.assumption. +apply H2.assumption. +apply not_lt_to_le.assumption. +apply decidable_lt (h j) k. +qed. + (* applications *) -let rec map_iter n (g:nat \to nat) f (a:nat) \def - match n with - [ O \Rightarrow a - | (S p) \Rightarrow f (g p) (map_iter p g f a)]. - -theorem eq_map_iter: \forall g1,g2:nat \to nat. -\forall f:nat \to nat \to nat. \forall n,a:nat. -(\forall m:nat. m \lt n \to g1 m = g2 m) \to -map_iter n g1 f a = map_iter n g2 f a. -intros 5.elim n.simplify.reflexivity. -simplify.apply eq_f2.apply H1.simplify.apply le_n. -apply H.intros.apply H1.apply trans_lt ? n1.assumption. -simplify.apply le_n. +let rec map_iter_i k (g:nat \to nat) f (i:nat) \def + match k with + [ O \Rightarrow g i + | (S k) \Rightarrow f (g (S (k+i))) (map_iter_i k g f i)]. + +theorem eq_map_iter_i: \forall g1,g2:nat \to nat. +\forall f:nat \to nat \to nat. \forall n,i:nat. +(\forall m:nat. i\le m \to m \le n+i \to g1 m = g2 m) \to +map_iter_i n g1 f i = map_iter_i n g2 f i. +intros 5.elim n.simplify.apply H.apply le_n. +apply le_n.simplify.apply eq_f2.apply H1.simplify. +apply le_S.apply le_plus_n.simplify.apply le_n. +apply H.intros.apply H1.assumption.simplify.apply le_S.assumption. qed. (* map_iter examples *) -theorem eq_map_iter_sigma: \forall g:nat \to nat. \forall n:nat. -map_iter n g plus O = sigma n g. + +theorem eq_map_iter_i_sigma: \forall g:nat \to nat. \forall n,m:nat. +map_iter_i n g plus m = sigma n g m. intros.elim n.simplify.reflexivity. simplify. apply eq_f.assumption. qed. -theorem eq_map_iter_pi: \forall g:nat \to nat. \forall n:nat. -map_iter n g times (S O) = pi n g. +theorem eq_map_iter_i_pi: \forall g:nat \to nat. \forall n,m:nat. +map_iter_i n g times m = pi n g m. intros.elim n.simplify.reflexivity. simplify. apply eq_f.assumption. qed. -theorem eq_map_iter_transpose_i_Si : \forall f:nat\to nat \to nat.associative nat f \to -symmetric2 nat nat f \to \forall g:nat \to nat. \forall n,i,a:nat. i \lt n \to -map_iter (S n) g f a = map_iter (S n) (\lambda m. g (transpose i (S i) m)) f a. -intros 5.elim n.apply False_ind.apply not_le_Sn_O i H2. -simplify in H3. -cut i < n1 \lor i = n1. -change with -f (g (S n1)) (map_iter (S n1) g f a) = -f (g (transpose i (S i) (S n1))) (map_iter (S n1) (\lambda m. g (transpose i (S i) m)) f a). -elim Hcut. -cut g (transpose i (S i) (S n1)) = g (S n1). -rewrite > Hcut1. -rewrite < H2 i a H4.reflexivity. -unfold transpose. -rewrite > not_eq_to_eqb_false (S n1) i. -rewrite > not_eq_to_eqb_false (S n1) (S i). +theorem eq_map_iter_i_fact: \forall n:nat. +map_iter_i n (\lambda m.m) times (S O) = (S n)!. +intros.elim n. simplify.reflexivity. -simplify.intro. -apply lt_to_not_eq i n1 H4. -apply injective_S i.apply sym_eq.assumption. -simplify. intro. -apply lt_to_not_eq i (S n1). -apply trans_lt ? n1.assumption.simplify.apply le_n. -apply sym_eq.assumption. -(* interesting case *) -rewrite > H4. -change with f (g (S n1)) (f (g n1) (map_iter n1 g f a)) = -f (g (transpose n1 (S n1) (S n1))) -(f (g (transpose n1 (S n1) n1)) -(map_iter n1 (\lambda m. g (transpose n1 (S n1) m)) f a)). -cut (g (transpose n1 (S n1) (S n1))) = g n1. -cut (g (transpose n1 (S n1) n1)) = g (S n1). -cut map_iter n1 (\lambda m. g (transpose n1 (S n1) m)) f a = map_iter n1 g f a. -rewrite > Hcut1.rewrite > Hcut2.rewrite > Hcut3. +change with +((S n1)+(S O))*(map_iter_i n1 (\lambda m.m) times (S O)) = (S(S n1))*(S n1)!. +rewrite < plus_n_Sm.rewrite < plus_n_O. +apply eq_f.assumption. +qed. + +theorem eq_map_iter_i_transpose_l : \forall f:nat\to nat \to nat.associative nat f \to +symmetric2 nat nat f \to \forall g:nat \to nat. \forall n,k:nat. +map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose (k+n) (S k+n) m)) f n. +intros.apply nat_case1 k. +intros.simplify. +change with +f (g (S n)) (g n) = +f (g (transpose n (S n) (S n))) (g (transpose n (S n) n)). +rewrite > transpose_i_j_i. +rewrite > transpose_i_j_j. +apply H1. +intros. +change with +f (g (S (S (m+n)))) (f (g (S (m+n))) (map_iter_i m g f n)) = +f (g (transpose (S m + n) (S (S m) + n) (S (S m)+n))) +(f (g (transpose (S m + n) (S (S m) + n) (S m+n))) +(map_iter_i m (\lambda m1. g (transpose (S m+n) (S (S m)+n) m1)) f n)). +rewrite > transpose_i_j_i. +rewrite > transpose_i_j_j. rewrite < H. -rewrite > H1 (g (S n1)). -rewrite > H.reflexivity. -apply eq_map_iter. +rewrite < H. +rewrite < H1 (g (S m + n)). +apply eq_f. +apply eq_map_iter_i. intros.unfold transpose. -rewrite > not_eq_to_eqb_false m n1. -rewrite > not_eq_to_eqb_false m (S n1). +rewrite > not_eq_to_eqb_false m1 (S m+n). +rewrite > not_eq_to_eqb_false m1 (S (S m)+n). +simplify. +reflexivity. +apply lt_to_not_eq m1 (S (S m)+n). +simplify.apply le_S_S.apply le_S.assumption. +apply lt_to_not_eq m1 (S m+n). +simplify.apply le_S_S.assumption. +qed. + +theorem eq_map_iter_i_transpose_i_Si : \forall f:nat\to nat \to nat.associative nat f \to +symmetric2 nat nat f \to \forall g:nat \to nat. \forall n,k,i:nat. n \le i \to i \le k+n \to +map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i (S i) m)) f n. +intros 6.elim k.cut i=n. +rewrite > Hcut. +apply eq_map_iter_i_transpose_l f H H1 g n O. +apply antisymmetric_le.assumption.assumption. +cut i < S n1 + n \lor i = S n1 + n. +elim Hcut. +change with +f (g (S (S n1)+n)) (map_iter_i (S n1) g f n) = +f (g (transpose i (S i) (S (S n1)+n))) (map_iter_i (S n1) (\lambda m. g (transpose i (S i) m)) f n). +apply eq_f2.unfold transpose. +rewrite > not_eq_to_eqb_false (S (S n1)+n) i. +rewrite > not_eq_to_eqb_false (S (S n1)+n) (S i). simplify.reflexivity. -simplify. intro.apply lt_to_not_eq m (S n1). -apply trans_lt ? n1.assumption.simplify. apply le_n. +simplify.intro. +apply lt_to_not_eq i (S n1+n).assumption. +apply inj_S.apply sym_eq. assumption. +simplify.intro. +apply lt_to_not_eq i (S (S n1+n)).simplify. +apply le_S_S.assumption. +apply sym_eq. assumption. +apply H2.assumption.apply le_S_S_to_le. assumption. -simplify. intro.apply lt_to_not_eq m n1. -assumption.assumption. -unfold transpose. -rewrite > eqb_n_n n1.simplify.reflexivity. -unfold transpose. -rewrite > not_eq_to_eqb_false.simplify. -rewrite > eqb_n_n n1.simplify.reflexivity. -simplify. intro. -apply not_eq_n_Sn n1. apply sym_eq.assumption. -apply le_to_or_lt_eq. -apply le_S_S_to_le.assumption. +rewrite > H5. +apply eq_map_iter_i_transpose_l f H H1 g n (S n1). +apply le_to_or_lt_eq.assumption. qed. -theorem eq_map_iter_transpose: \forall f:nat\to nat \to nat.associative nat f \to -symmetric2 nat nat f \to \forall n,a,k:nat. -\forall g:nat \to nat. \forall i:nat. S (k + i) \le n \to -map_iter (S n) g f a = map_iter (S n) (\lambda m. g (transpose i (S(k + i)) m)) f a. +theorem eq_map_iter_i_transpose: +\forall f:nat\to nat \to nat. +associative nat f \to symmetric2 nat nat f \to \forall n,k,o:nat. +\forall g:nat \to nat. \forall i:nat. n \le i \to S (o + i) \le S k+n \to +map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i (S(o + i)) m)) f n. intros 6. -apply nat_elim1 k. +apply nat_elim1 o. intro. apply nat_case m ?. intros. -apply eq_map_iter_transpose_i_Si f H H1 g n i. -exact H3. +apply eq_map_iter_i_transpose_i_Si ? H H1. +exact H3.apply le_S_S_to_le.assumption. intros. -apply trans_eq ? ? (map_iter (S n) (\lambda m. g (transpose i (S(m1 + i)) m)) f a). -apply H2 m1 ? g. -simplify. apply le_n. +apply trans_eq ? ? (map_iter_i (S k) (\lambda m. g (transpose i (S(m1 + i)) m)) f n). +apply H2. +simplify. apply le_n.assumption. 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 trans_eq ? ? (map_iter_i (S k) (\lambda m. g +(transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m))) f n). +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 +apply trans_le ? i.assumption. +change with i \le (S m1)+i.apply le_plus_n. +exact H4. +apply trans_eq ? ? (map_iter_i (S k) (\lambda m. g (transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) -(transpose i (S(m1 + i)) m)))) f a). -apply H2 m1 ?. -simplify. apply le_n. +(transpose i (S(m1 + i)) m)))) f n). +apply H2 m1. +simplify. apply le_n.assumption. apply trans_le ? (S(S (m1+i))). apply le_S.apply le_n.assumption. -apply eq_map_iter. +apply eq_map_iter_i. intros.apply eq_f. apply sym_eq. apply eq_transpose. simplify. intro. apply not_le_Sn_n i. -rewrite < H5 in \vdash (? ? %). +rewrite < H7 in \vdash (? ? %). apply le_S_S.apply le_S. apply le_plus_n. simplify. intro. apply not_le_Sn_n i. -rewrite > H5 in \vdash (? ? %). +rewrite > H7 in \vdash (? ? %). apply le_S_S. apply le_plus_n. simplify. intro. @@ -508,189 +645,98 @@ apply not_eq_n_Sn (S m1+i). apply sym_eq.assumption. qed. -theorem eq_map_iter_transpose1: \forall f:nat\to nat \to nat.associative nat f \to -symmetric2 nat nat f \to \forall n,a,i,j:nat. -\forall g:nat \to nat. i < j \to j \le n \to -map_iter (S n) g f a = map_iter (S n) (\lambda m. g (transpose i j m)) f a. +theorem eq_map_iter_i_transpose1: \forall f:nat\to nat \to nat.associative nat f \to +symmetric2 nat nat f \to \forall n,k,i,j:nat. +\forall g:nat \to nat. n \le i \to i < j \to j \le S k+n \to +map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i j m)) f n. intros. -simplify in H2. +simplify in H3. cut (S i) < j \lor (S i) = j. elim Hcut. cut j = S ((j - (S i)) + i). rewrite > Hcut1. -apply eq_map_iter_transpose f H H1 n a (j - (S i)) g i. +apply eq_map_iter_i_transpose f H H1 n k (j - (S i)) g i. +assumption. rewrite < Hcut1.assumption. rewrite > plus_n_Sm. apply plus_minus_m_m.apply lt_to_le.assumption. -rewrite < H4. -apply eq_map_iter_transpose_i_Si f H H1 g. +rewrite < H5. +apply eq_map_iter_i_transpose_i_Si f H H1 g. simplify. +assumption.apply le_S_S_to_le. apply trans_le ? j.assumption.assumption. apply le_to_or_lt_eq.assumption. qed. -theorem eq_map_iter_transpose2: \forall f:nat\to nat \to nat.associative nat f \to -symmetric2 nat nat f \to \forall n,a,i,j:nat. -\forall g:nat \to nat. i \le n \to j \le n \to -map_iter (S n) g f a = map_iter (S n) (\lambda m. g (transpose i j m)) f a. +theorem eq_map_iter_i_transpose2: \forall f:nat\to nat \to nat.associative nat f \to +symmetric2 nat nat f \to \forall n,k,i,j:nat. +\forall g:nat \to nat. n \le i \to i \le (S k+n) \to n \le j \to j \le (S k+n) \to +map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i j m)) f n. intros. apply nat_compare_elim i j. -intro.apply eq_map_iter_transpose1 f H H1 n a i j g H4 H3. -intro.rewrite > H4. -apply eq_map_iter.intros. +intro.apply eq_map_iter_i_transpose1 f H H1 n k i j g H2 H6 H5. +intro.rewrite > H6. +apply eq_map_iter_i.intros. rewrite > transpose_i_i j.reflexivity. intro. -apply trans_eq ? ? (map_iter (S n) (\lambda m:nat.g (transpose j i m)) f a). -apply eq_map_iter_transpose1 f H H1 n a j i g H4 H2. -apply eq_map_iter. +apply trans_eq ? ? (map_iter_i (S k) (\lambda m:nat.g (transpose j i m)) f n). +apply eq_map_iter_i_transpose1 f H H1 n k j i g H4 H6 H3. +apply eq_map_iter_i. intros.apply eq_f.apply transpose_i_j_j_i. qed. -theorem permut_to_eq_map_iter:\forall f:nat\to nat \to nat.associative nat f \to -symmetric2 nat nat f \to \forall a,n:nat.\forall g,h:nat \to nat. -permut h n \to -map_iter (S n) g f a = map_iter (S n) (\lambda m.g(h m)) f a. -intros 5.elim n. -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. +theorem permut_to_eq_map_iter_i:\forall f:nat\to nat \to nat.associative nat f \to +symmetric2 nat nat f \to \forall k,n:nat.\forall g,h:nat \to nat. +permut h (k+n) \to (\forall m:nat. m \lt n \to h m = m) \to +map_iter_i k g f n = map_iter_i k (\lambda m.g(h m)) f n. +intros 4.elim k. +simplify.rewrite > permut_n_to_eq_n h.reflexivity.assumption.assumption. +apply trans_eq ? ? (map_iter_i (S n) (\lambda m.g ((transpose (h (S n+n1)) (S n+n1)) m)) f n1). unfold permut in H3. -elim H3 (S n1).assumption.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). +elim H3. +apply eq_map_iter_i_transpose2 f H H1 n1 n ? ? g. +apply permut_n_to_le h n1 (S n+n1). +apply le_plus_n.assumption.assumption.apply le_plus_n.apply le_n. +apply H5.apply le_n.apply le_plus_n.apply le_n. +apply trans_eq ? ? (map_iter_i (S n) (\lambda m. +(g(transpose (h (S n+n1)) (S n+n1) +(transpose (h (S n+n1)) (S n+n1) (h m)))) )f n1). change with -f (g (transpose (h (S n1)) (S n1) (S n1))) -(map_iter (S n1) (\lambda m. -g (transpose (h (S n1)) (S n1) m)) f a) +f (g (transpose (h (S n+n1)) (S n+n1) (S n+n1))) +(map_iter_i n (\lambda m. +g (transpose (h (S n+n1)) (S n+n1) m)) f n1) = f -(g(transpose (h (S n1)) (S n1) -(transpose (h (S n1)) (S n1) (h (S n1))))) -(map_iter (S n1) +(g(transpose (h (S n+n1)) (S n+n1) +(transpose (h (S n+n1)) (S n+n1) (h (S n+n1))))) +(map_iter_i n (\lambda m. -(g(transpose (h (S n1)) (S n1) -(transpose (h (S n1)) (S n1) (h m))))) f a). +(g(transpose (h (S n+n1)) (S n+n1) +(transpose (h (S n+n1)) (S n+n1) (h m))))) f n1). apply eq_f2.apply eq_f. rewrite > transpose_i_j_j. rewrite > transpose_i_j_i. rewrite > transpose_i_j_j.reflexivity. -apply H2 (\lambda m.(g(transpose (h (S n1)) (S n1) m))). +apply H2 n1 (\lambda m.(g(transpose (h (S n+n1)) (S n+n1) m))). apply permut_S_to_permut_transpose. assumption. -apply eq_map_iter.intros. -rewrite > transpose_transpose.reflexivity. -qed. - -theorem eq_sigma_transpose_i_Si: \forall n,i:nat. \forall f:nat \to nat. i \lt n \to -sigma (S n) f = sigma (S n) (\lambda m. f (transpose i (S i) m)). -intro.elim n.apply False_ind.apply not_le_Sn_O i H. -simplify in H1. -cut i < n1 \lor i = n1. -change with -(f (S n1))+(sigma (S n1) f) = -(f (transpose i (S i) (S n1)))+(sigma (S n1) (\lambda m. f (transpose i (S i) m))). -elim Hcut. -cut f (transpose i (S i) (S n1)) = f (S n1). -rewrite > Hcut1. -rewrite < H i f.reflexivity. -assumption.unfold transpose. -rewrite > not_eq_to_eqb_false (S n1) i. -rewrite > not_eq_to_eqb_false (S n1) (S i). -simplify.reflexivity. +intros. +unfold transpose. +rewrite > not_eq_to_eqb_false (h m) (h (S n+n1)). +rewrite > not_eq_to_eqb_false (h m) (S n+n1). +simplify.apply H4.assumption. +rewrite > H4. +apply lt_to_not_eq.apply trans_lt ? n1.assumption. +simplify.apply le_S_S.apply le_plus_n.assumption. +unfold permut in H3.elim H3. simplify.intro. -apply lt_to_not_eq i n1 H2. -apply injective_S i.apply sym_eq.assumption. -simplify. intro. -apply lt_to_not_eq i (S n1). -apply trans_lt ? n1.assumption.simplify.apply le_n. -apply sym_eq.assumption. -rewrite > H2. -change with (f (S n1))+((f n1)+(sigma n1 f)) = -(f (transpose n1 (S n1) (S n1)))+ -((f (transpose n1 (S n1) n1))+ -(sigma n1 (\lambda m. f (transpose n1 (S n1) m)))). -cut (f (transpose n1 (S n1) (S n1))) = f n1. -cut (f (transpose n1 (S n1) n1)) = f (S n1). -cut sigma n1 (\lambda m. f (transpose n1 (S n1) m)) = sigma n1 f. -rewrite > Hcut1.rewrite > Hcut2.rewrite > Hcut3. -rewrite < assoc_plus.rewrite > sym_plus (f (S n1)). -rewrite > assoc_plus.reflexivity. -apply eq_sigma. -intros.unfold transpose. -rewrite > not_eq_to_eqb_false m n1. -rewrite > not_eq_to_eqb_false m (S n1). -simplify.reflexivity. -simplify. intro.apply lt_to_not_eq m (S n1). -apply trans_lt ? n1.assumption.simplify. apply le_n. +apply lt_to_not_eq m (S n+n1).apply trans_lt ? n1.assumption. +simplify.apply le_S_S.apply le_plus_n. +unfold injn in H7. +apply H7 m (S n+n1).apply trans_le ? n1. +apply lt_to_le.assumption.apply le_plus_n.apply le_n. assumption. -simplify. intro.apply lt_to_not_eq m n1. -assumption.assumption. -unfold transpose. -rewrite > eqb_n_n n1.simplify.reflexivity. -unfold transpose. -rewrite > not_eq_to_eqb_false.simplify. -rewrite > eqb_n_n n1.simplify.reflexivity. -simplify. intro. -apply not_eq_n_Sn n1. apply sym_eq.assumption. -apply le_to_or_lt_eq. -apply le_S_S_to_le.assumption. -qed. - -theorem eq_sigma_transpose: \forall n,k:nat. \forall f:nat \to nat. -\forall i. S (k + i) \le n \to -sigma (S n) f = sigma (S n) (\lambda m. f (transpose i (S(k + i)) m)). -intros 2. -apply nat_elim1 k. -intro. -apply nat_case m ?. -intros. -apply eq_sigma_transpose_i_Si n i f. -exact H1. -intros. -apply trans_eq ? ? (sigma (S n) (\lambda m. f (transpose i (S(m1 + i)) m))). -apply H m1 ? f ?. -simplify. apply le_n. -apply trans_le ? (S(S (m1+i))). -apply le_S.apply le_n.assumption. -apply trans_eq ? ? (sigma (S n) (\lambda m. f -(transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m)))). -apply H O ? ? (S(m1+i)) ?. -simplify.apply le_S_S.apply le_O_n. -exact H1. -apply trans_eq ? ? (sigma (S n) (\lambda m. f -(transpose i (S(m1 + i)) -(transpose (S(m1 + i)) (S(S(m1 + i))) -(transpose i (S(m1 + i)) m))))). -apply H m1 ? ? i. -simplify. apply le_n. -apply trans_le ? (S(S (m1+i))). -apply le_S.apply le_n.assumption. -apply eq_sigma. -intros.apply eq_f. -apply sym_eq. apply eq_transpose. -simplify. intro. -apply not_le_Sn_n i. -rewrite < H3 in \vdash (? ? %). -apply le_S_S.apply le_S. -apply le_plus_n. -simplify. intro. -apply not_le_Sn_n i. -rewrite > H3 in \vdash (? ? %). -apply le_S_S. -apply le_plus_n. -simplify. intro. -apply not_eq_n_Sn (S m1+i). -apply sym_eq.assumption. +apply eq_map_iter_i.intros. +rewrite > transpose_transpose.reflexivity. qed. -(* -theorem bad: \forall n:nat. \forall f:nat \to nat. -permut f n \to sigma (S n) f = sigma (S n) (\lambda n.n). -intro.elim n. -simplify.unfold permut in H.elim H O. -rewrite < (le_n_O_to_eq (f O)).simplify. reflexivity.apply le_n. -cut permut (\lambda n.transpose (f (S n1)) (S n1) (f n)) n1. -apply trans_eq ? ? -(sigma (S(S n1)) (\lambda n.transpose (f (S n1)) (S n1) (f n))). -*) \ No newline at end of file