--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/permutation".
+
+include "nat/compare.ma".
+include "nat/sigma_and_pi.ma".
+
+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)).
+
+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.
+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.
+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 H6.rewrite > H7.assumption.
+apply le_to_or_lt_eq.assumption.
+assumption.apply le_n.
+apply le_S.assumption.
+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]].
+
+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.
+elim eqb i1 i.simplify.assumption.
+elim eqb i1 j.simplify.assumption.
+simplify.assumption.
+apply inj_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.
+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.
+simplify.intro.apply H1.apply sym_eq.assumption.
+assumption.
+simplify.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.
+simplify.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.
+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.
+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.simplify.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.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.
+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.
+apply bijn_n_Sn.
+apply H ?.
+apply permut_S_to_permut_transpose.
+assumption.simplify.
+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 (\forall p:nat. f m = f p \to m = p) \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.assumption.
+simplify.intro.absurd m = S n1.
+apply H3.assumption.simplify.intro.
+apply not_le_Sn_n n1.rewrite < H5.assumption.
+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.
+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.
+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.
+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).
+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.
+rewrite < H.
+rewrite > H1 (g (S n1)).
+rewrite > H.reflexivity.
+apply eq_map_iter.
+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.
+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_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.
+intros 6.
+apply nat_elim1 k.
+intro.
+apply nat_case m ?.
+intros.
+apply eq_map_iter_transpose_i_Si f H H1 g n i.
+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.
+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)) ?.
+simplify.apply le_S_S.apply le_O_n.
+exact H3.
+apply trans_eq ? ? (map_iter (S n) (\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.
+apply trans_le ? (S(S (m1+i))).
+apply le_S.apply le_n.assumption.
+apply eq_map_iter.
+intros.apply eq_f.
+apply sym_eq. apply eq_transpose.
+simplify. intro.
+apply not_le_Sn_n i.
+rewrite < H5 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 (? ? %).
+apply le_S_S.
+apply le_plus_n.
+simplify. intro.
+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.
+intros.
+simplify in H2.
+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.
+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.
+simplify.
+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.
+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.
+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.
+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.
+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).
+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 n1)) (S n1)
+(transpose (h (S n1)) (S n1) (h (S n1)))))
+(map_iter (S n1)
+(\lambda m.
+(g(transpose (h (S n1)) (S n1)
+(transpose (h (S n1)) (S n1) (h m))))) f a).
+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 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.
+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.
+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.
+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
projects / helm.git / commitdiff