X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Flibrary%2Fnat%2Fpermutation.ma;fp=matita%2Flibrary%2Fnat%2Fpermutation.ma;h=884c18ddc17c0f2a3dafe344c38dabb24160ec38;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/matita/library/nat/permutation.ma b/matita/library/nat/permutation.ma
new file mode 100644
index 000000000..884c18ddc
--- /dev/null
+++ b/matita/library/nat/permutation.ma
@@ -0,0 +1,753 @@
+(**************************************************************************)
+(*       ___	                                                          *)
+(*      ||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         *)
+(*                                                                        *)
+(**************************************************************************)
+
+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.unfold injn.
+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.
+unfold injective.unfold injn.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 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.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.
+split.intros.
+cut (f i < S m \lor f i = S m).
+elim Hcut.
+apply le_S_S_to_le.assumption.
+apply False_ind.
+apply (not_le_Sn_n m).
+cut ((S m) = i).
+rewrite > Hcut1.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 *)
+
+definition transpose : nat \to nat \to nat \to nat \def
+\lambda i,j,n:nat.
+match eqb n i with
+  [ true \Rightarrow j
+  | false \Rightarrow 
+      match eqb n j with
+      [ true \Rightarrow i
+      | false \Rightarrow n]].
+
+notation < "(❲i↹j❳)n"
+  right associative with precedence 71 
+for @{ 'transposition $i $j $n}.
+
+notation < "(❲i \atop j❳)n"
+  right associative with precedence 71 
+for @{ 'transposition $i $j $n}.
+
+interpretation "natural transposition" 'transposition i j n =
+  (cic:/matita/nat/permutation/transpose.con i j n).
+
+lemma transpose_i_j_i: \forall i,j:nat. transpose i j i = j.
+intros.unfold transpose.
+rewrite > (eqb_n_n i).simplify. reflexivity.
+qed.
+
+lemma transpose_i_j_j: \forall i,j:nat. transpose i j j = i.
+intros.unfold transpose.
+apply (eqb_elim j i).simplify.intro.assumption.
+rewrite > (eqb_n_n j).simplify.
+intros. reflexivity.
+qed.
+      
+theorem transpose_i_i:  \forall i,n:nat. (transpose  i i n) = n.
+intros.unfold transpose.
+apply (eqb_elim n i).
+intro.simplify.apply sym_eq. assumption.
+intro.simplify.reflexivity.
+qed.
+
+theorem transpose_i_j_j_i: \forall i,j,n:nat.
+transpose i j n = transpose j i n.
+intros.unfold transpose.
+apply (eqb_elim n i).
+apply (eqb_elim n j).
+intros. simplify.rewrite < H. rewrite < H1.
+reflexivity.
+intros.simplify.reflexivity.
+apply (eqb_elim n j).
+intros.simplify.reflexivity.
+intros.simplify.reflexivity.
+qed.
+
+theorem transpose_transpose: \forall i,j,n:nat.
+(transpose i j (transpose i j n)) = n.
+intros.unfold transpose. unfold transpose.
+apply (eqb_elim n i).simplify.
+intro.
+apply (eqb_elim j i).
+simplify.intros.rewrite > H. rewrite > H1.reflexivity.
+rewrite > (eqb_n_n j).simplify.intros.
+apply sym_eq.
+assumption.
+apply (eqb_elim n j).simplify.
+rewrite > (eqb_n_n i).intros.simplify.
+apply sym_eq. assumption.
+simplify.intros.
+rewrite > (not_eq_to_eqb_false n i H1).
+rewrite > (not_eq_to_eqb_false n j H).
+simplify.reflexivity.
+qed.
+
+theorem injective_transpose : \forall i,j:nat. 
+injective nat nat (transpose i j).
+unfold injective.
+intros.
+rewrite < (transpose_transpose i j x).
+rewrite < (transpose_transpose i j y).
+apply eq_f.assumption.
+qed.
+
+variant inj_transpose: \forall i,j,n,m:nat.
+transpose i j n = transpose i j m \to n = m \def
+injective_transpose.
+
+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 (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.
+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: 
+\forall f:nat \to nat. \forall m,i,j:nat.
+i \le m \to j \le m \to permut f m \to permut (\lambda n.transpose i j (f n)) m.  
+intros.apply (permut_fg (transpose i j) f m ? ?).
+apply permut_transpose.assumption.assumption.
+assumption.
+qed.
+
+theorem permut_transpose_r: 
+\forall f:nat \to nat. \forall m,i,j:nat.
+i \le m \to j \le m \to permut f m \to permut (\lambda n.f (transpose i j n)) m.  
+intros.apply (permut_fg f (transpose i j) m ? ?).
+assumption.apply permut_transpose.assumption.assumption.
+qed.
+
+theorem eq_transpose : \forall i,j,k,n:nat. \lnot j=i \to
+ \lnot i=k \to \lnot j=k \to
+transpose i j n = transpose i k (transpose k j (transpose i k n)).
+(* uffa: triplo unfold? *)
+intros.unfold transpose.unfold transpose.unfold transpose.
+apply (eqb_elim n i).intro.
+simplify.rewrite > (eqb_n_n k).
+simplify.rewrite > (not_eq_to_eqb_false j i H).
+rewrite > (not_eq_to_eqb_false j k H2).
+reflexivity.
+intro.apply (eqb_elim n j).
+intro.
+cut (\lnot n = k).
+cut (\lnot n = i).
+rewrite > (not_eq_to_eqb_false n k Hcut).
+simplify.
+rewrite > (not_eq_to_eqb_false n k Hcut).
+rewrite > (eq_to_eqb_true n j H4).
+simplify.
+rewrite > (not_eq_to_eqb_false k i).
+rewrite > (eqb_n_n k).
+simplify.reflexivity.
+unfold Not.intro.apply H1.apply sym_eq.assumption.
+assumption.
+unfold Not.intro.apply H2.apply (trans_eq ? ? n).
+apply sym_eq.assumption.assumption.
+intro.apply (eqb_elim n k).intro.
+simplify.
+rewrite > (not_eq_to_eqb_false i k H1).
+rewrite > (not_eq_to_eqb_false i j).
+simplify.
+rewrite > (eqb_n_n i).
+simplify.assumption.
+unfold Not.intro.apply H.apply sym_eq.assumption.
+intro.simplify.
+rewrite > (not_eq_to_eqb_false n k H5).
+rewrite > (not_eq_to_eqb_false n j H4).
+simplify.
+rewrite > (not_eq_to_eqb_false n i H3).
+rewrite > (not_eq_to_eqb_false n k H5).
+simplify.reflexivity.
+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.
+unfold permut.intros.
+elim H.
+split.intros.simplify.unfold transpose.
+apply (eqb_elim (f i) (f (S m))).
+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)).
+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 *)
+
+definition bijn : (nat \to nat) \to nat \to Prop \def
+\lambda f:nat \to nat. \lambda n. \forall m:nat. m \le n \to
+ex nat (\lambda p. p \le n \land f p = m).
+
+theorem eq_to_bijn:  \forall f,g:nat\to nat. \forall n:nat.
+(\forall i:nat. i \le n \to (f i) = (g i)) \to 
+bijn f n \to bijn g n.
+intros 4.unfold bijn.
+intros.elim (H1 m).
+apply (ex_intro ? ? a).
+rewrite < (H a).assumption.
+elim H3.assumption.assumption.
+qed.
+
+theorem bijn_Sn_n: \forall f:nat \to nat. \forall n:nat.
+bijn f (S n) \to f (S n) = (S n) \to bijn f n.
+unfold bijn.intros.elim (H m).
+elim H3.
+apply (ex_intro ? ? a).split.
+cut (a < S n \lor a = S n).
+elim Hcut.apply le_S_S_to_le.assumption.
+apply False_ind.
+apply (not_le_Sn_n n).
+rewrite < H1.rewrite < H6.rewrite > H5.assumption.
+apply le_to_or_lt_eq.assumption.assumption.
+apply le_S.assumption.
+qed.
+
+theorem bijn_n_Sn: \forall f:nat \to nat. \forall n:nat.
+bijn f n \to f (S n) = (S n) \to bijn f (S n).
+unfold bijn.intros.
+cut (m < S n \lor m = S n).
+elim Hcut.
+elim (H m).
+elim H4.
+apply (ex_intro ? ? a).split.
+apply le_S.assumption.assumption.
+apply le_S_S_to_le.assumption.
+apply (ex_intro ? ? (S n)).
+split.apply le_n.
+rewrite > H3.assumption.
+apply le_to_or_lt_eq.assumption.
+qed.
+
+theorem bijn_fg: \forall f,g:nat\to nat. \forall n:nat.
+bijn f n \to bijn g n \to bijn (\lambda p.f(g p)) n.
+unfold bijn.
+intros.simplify.
+elim (H m).elim H3.
+elim (H1 a).elim H6.
+apply (ex_intro ? ? a1).
+split.assumption.
+rewrite > H8.assumption.
+assumption.assumption.
+qed.
+
+theorem bijn_transpose : \forall n,i,j. i \le n \to j \le n \to
+bijn (transpose i j) n.
+intros.unfold bijn.unfold transpose.intros.
+cut (m = i \lor \lnot m = i).
+elim Hcut.
+apply (ex_intro ? ? j).
+split.assumption.
+apply (eqb_elim j i).
+intro.simplify.rewrite > H3.rewrite > H4.reflexivity.
+rewrite > (eqb_n_n j).simplify.
+intros. apply sym_eq.assumption.
+cut (m = j \lor \lnot m = j).
+elim Hcut1.
+apply (ex_intro ? ? i).
+split.assumption.
+rewrite > (eqb_n_n i).simplify.
+apply sym_eq. assumption.
+apply (ex_intro ? ? m).
+split.assumption.
+rewrite > (not_eq_to_eqb_false m i).
+rewrite > (not_eq_to_eqb_false m j).
+simplify. reflexivity.
+assumption.
+assumption.
+apply (decidable_eq_nat m j).
+apply (decidable_eq_nat m i).
+qed.
+
+theorem bijn_transpose_r: \forall f:nat\to nat.\forall n,i,j. i \le n \to j \le n \to
+bijn f n \to bijn (\lambda p.f (transpose i j p)) n.
+intros.
+apply (bijn_fg f ?).assumption.
+apply (bijn_transpose n i j).assumption.assumption.
+qed.
+
+theorem bijn_transpose_l: \forall f:nat\to nat.\forall n,i,j. i \le n \to j \le n \to
+bijn f n \to bijn (\lambda p.transpose i j (f p)) n.
+intros.
+apply (bijn_fg ? f).
+apply (bijn_transpose n i j).assumption.assumption.
+assumption.
+qed.
+
+theorem permut_to_bijn: \forall n:nat.\forall f:nat\to nat.
+permut f n \to bijn f n.
+intro.
+elim n.unfold bijn.intros.
+apply (ex_intro ? ? m).
+split.assumption.
+apply (le_n_O_elim m ? (\lambda p. f p = p)).
+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.
+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.
+assumption.unfold transpose.
+rewrite > (eqb_n_n (f (S n1))).simplify.reflexivity.
+qed.
+
+let rec invert_permut n f m \def
+  match eqb m (f n) with
+  [true \Rightarrow n
+  |false \Rightarrow 
+     match n with
+     [O \Rightarrow O
+     |(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 injn f n\to invert_permut n f (f m) = m.
+intros 4.
+elim H.
+apply (nat_case1 m).
+intro.simplify.
+rewrite > (eqb_n_n (f O)).simplify.reflexivity.
+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.
+apply injn_Sn_n. assumption.
+unfold Not.intro.absurd (m = S n1).
+apply H3.apply le_S.assumption.apply le_n.assumption.
+unfold Not.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.
+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_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_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_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_i_fact: \forall n:nat. 
+map_iter_i n (\lambda m.m) times (S O) = (S n)!.
+intros.elim n.
+simplify.reflexivity.
+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.fold simplify (transpose n (S n) (S 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 < H.
+rewrite < (H1 (g (S m + n))).
+apply eq_f.
+apply eq_map_iter_i.
+intros.simplify.unfold transpose.
+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))).
+unfold lt.apply le_S_S.change with (m1 \leq S (m+n)).apply le_S.assumption.
+apply (lt_to_not_eq m1 (S m+n)).
+simplify.unfold lt.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.unfold Not.intro.
+apply (lt_to_not_eq i (S n1+n)).assumption.
+apply inj_S.apply sym_eq. assumption.
+simplify.unfold Not.intro.
+apply (lt_to_not_eq i (S (S n1+n))).simplify.unfold lt.
+apply le_S_S.assumption.
+apply sym_eq. assumption.
+apply H2.assumption.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_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 o).
+intro.
+apply (nat_case m ?).
+intros.
+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_i (S k) (\lambda m. g (transpose i (S(m1 + i)) m)) f n)).
+apply H2.
+unfold lt. apply le_n.assumption.
+apply (trans_le ? (S(S (m1+i)))).
+apply le_S.apply le_n.assumption.
+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))).
+unfold lt.apply le_S_S.apply le_O_n.id.
+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 n)).
+apply (H2 m1).
+unfold lt. apply le_n.assumption.
+apply (trans_le ? (S(S (m1+i)))).
+apply le_S.apply le_n.assumption.
+apply eq_map_iter_i.
+intros.apply eq_f.
+apply sym_eq. apply eq_transpose.
+unfold Not. intro.
+apply (not_le_Sn_n i).
+rewrite < H7 in \vdash (? ? %).
+apply le_S_S.apply le_S.
+apply le_plus_n.
+unfold Not. intro.
+apply (not_le_Sn_n i).
+rewrite > H7 in \vdash (? ? %).
+apply le_S_S.
+apply le_plus_n.
+unfold Not. intro.
+apply (not_eq_n_Sn (S m1+i)).
+apply sym_eq.assumption.
+qed.
+
+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 H3.
+cut ((S i) < j \lor (S i) = j).
+elim Hcut.
+cut (j = S ((j - (S i)) + i)).
+rewrite > Hcut1.
+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 < 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_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_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_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_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.
+     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))
+      [simplify.fold simplify (transpose (h (S n+n1)) (S n+n1) (S n+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 n1 (\lambda m.(g(transpose (h (S n+n1)) (S n+n1) m))))
+          [apply permut_S_to_permut_transpose.assumption
+          |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.unfold lt.apply le_S_S.apply le_plus_n]
+                |assumption
+                ]
+              ]
+            |unfold permut in H3.elim H3.
+             simplify.unfold Not.intro.
+             apply (lt_to_not_eq m (S n+n1))
+              [apply (trans_lt ? n1)
+                [assumption|simplify.unfold lt.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
+                ]
+              ]
+            ]
+          ]
+        ]
+      |apply eq_map_iter_i.intros.
+       rewrite > transpose_transpose.reflexivity
+      ]
+    ]
+  ]
+qed.
\ No newline at end of file