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.
+injn f (S n) \to injn f n.unfold injn.
intros.apply H.
apply le_S.assumption.
apply le_S.assumption.
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.
+unfold injective.unfold injn.intros.apply H.assumption.
qed.
definition permut : (nat \to nat) \to nat \to Prop
unfold permut.intros.
elim H.
split.intros.
-cut f i < S m \lor f i = S m.
+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.
+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.
+apply (injn_Sn_n f m H3).
qed.
(* transpositions *)
lemma transpose_i_j_i: \forall i,j:nat. transpose i j i = j.
intros.unfold transpose.
-rewrite > eqb_n_n i.simplify. reflexivity.
+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.
+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.
+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.
+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.
+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.
+apply (eqb_elim n i).simplify.
intro.
-apply eqb_elim j i.
+apply (eqb_elim j i).
simplify.intros.rewrite > H. rewrite > H1.reflexivity.
-rewrite > eqb_n_n j.simplify.intros.
+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 (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.
+rewrite > (not_eq_to_eqb_false n i H1).
+rewrite > (not_eq_to_eqb_false n j H).
simplify.reflexivity.
qed.
injective nat nat (transpose i j).
unfold injective.
intros.
-rewrite < transpose_transpose i j x.
-rewrite < transpose_transpose i j y.
+rewrite < (transpose_transpose i j x).
+rewrite < (transpose_transpose i j y).
apply eq_f.assumption.
qed.
unfold permut.intros.
split.unfold transpose.
intros.
-elim eqb i1 i.simplify.assumption.
-elim eqb i1 j.simplify.assumption.
+elim (eqb i1 i).simplify.assumption.
+elim (eqb i1 j).simplify.assumption.
simplify.assumption.
-apply injective_to_injn (transpose i j) n.
+apply (injective_to_injn (transpose i j) n).
apply injective_transpose.
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 ? ?.
+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 ? ?.
+intros.apply (permut_fg f (transpose i j) m ? ?).
assumption.apply permut_transpose.assumption.assumption.
qed.
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.
+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.apply (eqb_elim n j).
intro.
-cut \lnot n = k.
-cut \lnot n = i.
-rewrite > not_eq_to_eqb_false n k Hcut.
+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.
+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.
+rewrite > (not_eq_to_eqb_false k i).
+rewrite > (eqb_n_n k).
simplify.reflexivity.
-simplify.intro.apply H1.apply sym_eq.assumption.
+unfold Not.intro.apply H1.apply sym_eq.assumption.
assumption.
-simplify.intro.apply H2.apply trans_eq ? ? n.
+unfold Not.intro.apply H2.apply (trans_eq ? ? n).
apply sym_eq.assumption.assumption.
-intro.apply eqb_elim n k.intro.
+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.
+rewrite > (not_eq_to_eqb_false i k H1).
+rewrite > (not_eq_to_eqb_false i j).
simplify.
-rewrite > eqb_n_n i.
+rewrite > (eqb_n_n i).
simplify.assumption.
-simplify.intro.apply H.apply sym_eq.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.
+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.
+rewrite > (not_eq_to_eqb_false n i H3).
+rewrite > (not_eq_to_eqb_false n k H5).
simplify.reflexivity.
qed.
(f n)) m.
unfold permut.intros.
elim H.
-split.intros.simplify.
-apply eqb_elim (f i) (f (S m)).simplify.
+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.
+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.
+apply (eqb_elim (f i) (S m)).
intro.
-cut f (S m) \lt (S m) \lor f (S m) = (S m).
+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).
+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 (inj_transpose (f (S m)) (S m)).
apply H5.
qed.
(\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.
+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.
+unfold bijn.intros.elim (H m).
elim H3.
-apply ex_intro ? ? a.split.
-cut a < S n \lor a = S n.
+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.
+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.
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.
+cut (m < S n \lor m = S n).
elim Hcut.
-elim H m.
+elim (H m).
elim H4.
-apply ex_intro ? ? a.split.
+apply (ex_intro ? ? a).split.
apply le_S.assumption.assumption.
apply le_S_S_to_le.assumption.
-apply ex_intro ? ? (S n).
+apply (ex_intro ? ? (S n)).
split.apply le_n.
rewrite > H3.assumption.
apply le_to_or_lt_eq.assumption.
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.
+elim (H m).elim H3.
+elim (H1 a).elim H6.
+apply (ex_intro ? ? a1).
split.assumption.
rewrite > H8.assumption.
assumption.assumption.
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.
+intros.unfold bijn.unfold transpose.intros.
+cut (m = i \lor \lnot m = i).
elim Hcut.
-apply ex_intro ? ? j.
+apply (ex_intro ? ? j).
split.assumption.
-apply eqb_elim j i.
+apply (eqb_elim j i).
intro.simplify.rewrite > H3.rewrite > H4.reflexivity.
-rewrite > eqb_n_n j.simplify.
+rewrite > (eqb_n_n j).simplify.
intros. apply sym_eq.assumption.
-cut m = j \lor \lnot m = j.
+cut (m = j \lor \lnot m = j).
elim Hcut1.
-apply ex_intro ? ? i.
+apply (ex_intro ? ? i).
split.assumption.
-rewrite > eqb_n_n i.simplify.
+rewrite > (eqb_n_n i).simplify.
apply sym_eq. assumption.
-apply ex_intro ? ? m.
+apply (ex_intro ? ? m).
split.assumption.
-rewrite > not_eq_to_eqb_false m i.
-rewrite > not_eq_to_eqb_false m j.
+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.
+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.
+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.
+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.
+elim n.unfold bijn.intros.
+apply (ex_intro ? ? m).
split.assumption.
-apply le_n_O_elim m ? (\lambda p. f p = p).
+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.
+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_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.simplify.
-rewrite > eqb_n_n (f (S n1)).simplify.reflexivity.
+assumption.unfold transpose.
+rewrite > (eqb_n_n (f (S n1))).simplify.reflexivity.
qed.
let rec invert_permut n f m \def
m \le n \to injn f n\to invert_permut n f (f m) = m.
intros 4.
elim H.
-apply nat_case1 m.
+apply (nat_case1 m).
intro.simplify.
-rewrite > eqb_n_n (f O).simplify.reflexivity.
+rewrite > (eqb_n_n (f O)).simplify.reflexivity.
intros.simplify.
-rewrite > eqb_n_n (f (S m1)).simplify.reflexivity.
+rewrite > (eqb_n_n (f (S m1))).simplify.reflexivity.
simplify.
-rewrite > not_eq_to_eqb_false (f m) (f (S n1)).
+rewrite > (not_eq_to_eqb_false (f m) (f (S n1))).
simplify.apply H2.
apply injn_Sn_n. assumption.
-simplify.intro.absurd m = S n1.
+unfold Not.intro.absurd (m = S n1).
apply H3.apply le_S.assumption.apply le_n.assumption.
-simplify.intro.
-apply not_le_Sn_n n1.rewrite < H5.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.
+cut (bijn f n).
unfold bijn in Hcut.
-generalize in match Hcut i H1.intro.
-generalize in match Hcut j H2.intro.
+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 < (invert_permut_f f n a).
+rewrite < (invert_permut_f f n a1).
rewrite > H8.
rewrite > H11.
assumption.assumption.
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.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.
+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.
+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.
+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.
+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.
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.
+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 (? ? ? %).
+rewrite < (f_invert_permut h n n) in \vdash (? ? ? %).
apply eq_f.
-rewrite < f_invert_permut h n n in \vdash (? ? % ?).
+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 (f_invert_permut h).apply le_n.assumption.
apply le_to_or_lt_eq.
-cut permut (invert_permut n h) n.
+cut (permut (invert_permut n h) n).
unfold permut in Hcut.elim Hcut.
apply H4.apply le_n.
apply permut_invert_permut.assumption.
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.
+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.
+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.
+apply (decidable_lt (h j) k).
qed.
(* applications *)
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)!.
+(((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.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)).
+(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 (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)).
+(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)).
+rewrite < (H1 (g (S m + n))).
apply eq_f.
apply eq_map_iter_i.
-intros.unfold transpose.
-rewrite > not_eq_to_eqb_false m1 (S m+n).
-rewrite > not_eq_to_eqb_false m1 (S (S m)+n).
+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).
-simplify.apply le_S_S.apply le_S.assumption.
-apply lt_to_not_eq m1 (S m+n).
-simplify.apply le_S_S.assumption.
+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.
+intros 6.elim k.cut (i=n).
rewrite > Hcut.
-apply eq_map_iter_i_transpose_l f H H1 g n O.
+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.
+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).
+(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).
+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 i (S n1+n).assumption.
+simplify.unfold Not.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.
+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 (eq_map_iter_i_transpose_l f H H1 g n (S n1)).
apply le_to_or_lt_eq.assumption.
qed.
\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.
+apply (nat_elim1 o).
intro.
-apply nat_case m ?.
+apply (nat_case m ?).
intros.
-apply eq_map_iter_i_transpose_i_Si ? H H1.
+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 (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))).
+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)).
-simplify.apply le_S_S.apply le_O_n.
-apply trans_le ? i.assumption.
-change with i \le (S m1)+i.apply le_plus_n.
+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.
+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
+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.
-simplify. apply le_n.assumption.
-apply trans_le ? (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.
-simplify. intro.
-apply not_le_Sn_n i.
+unfold Not. intro.
+apply (not_le_Sn_n i).
rewrite < H7 in \vdash (? ? %).
apply le_S_S.apply le_S.
apply le_plus_n.
-simplify. intro.
-apply not_le_Sn_n i.
+unfold Not. intro.
+apply (not_le_Sn_n i).
rewrite > H7 in \vdash (? ? %).
apply le_S_S.
apply le_plus_n.
-simplify. intro.
-apply not_eq_n_Sn (S m1+i).
+unfold Not. intro.
+apply (not_eq_n_Sn (S m1+i)).
apply sym_eq.assumption.
qed.
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.
+cut ((S i) < j \lor (S i) = j).
elim Hcut.
-cut j = S ((j - (S i)) + i).
+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.
+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.
+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 (trans_le ? j).assumption.assumption.
apply le_to_or_lt_eq.assumption.
qed.
\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.
+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.
+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 (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.
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).
+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 (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.
+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).
+(transpose (h (S n+n1)) (S n+n1) (h m)))) )f n1)).
change with
-f (g (transpose (h (S n+n1)) (S n+n1) (S n+n1)))
+(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)
=
(map_iter_i n
(\lambda m.
(g(transpose (h (S n+n1)) (S n+n1)
-(transpose (h (S n+n1)) (S n+n1) (h m))))) f 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 n1 (\lambda m.(g(transpose (h (S n+n1)) (S n+n1) m))).
+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).
+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.
+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.intro.
-apply lt_to_not_eq m (S n+n1).apply trans_lt ? n1.assumption.
-simplify.apply le_S_S.apply le_plus_n.
+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 (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.
-
+qed.
\ No newline at end of file
projects / helm.git / blobdiff