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