X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fpermutation.ma;h=3e987e9e8c0df185f4c2a48271fef43dee2a2a1d;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=c64cb23de3c0a7a7b2074a458fb9df4917323fef;hpb=15604016ce7ae57658a94b9b0b5f650441290ac5;p=helm.git diff --git a/helm/matita/library/nat/permutation.ma b/helm/matita/library/nat/permutation.ma index c64cb23de..3e987e9e8 100644 --- a/helm/matita/library/nat/permutation.ma +++ b/helm/matita/library/nat/permutation.ma @@ -17,34 +17,50 @@ 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.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 -(\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. -cut f i < S m \lor f i = S m. +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. +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 *) @@ -60,19 +76,19 @@ match eqb n i with 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. @@ -80,12 +96,12 @@ 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. @@ -93,19 +109,19 @@ 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. @@ -113,8 +129,8 @@ 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. +rewrite < (transpose_transpose i j x). +rewrite < (transpose_transpose i j y). apply eq_f.assumption. qed. @@ -126,27 +142,30 @@ 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. +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: \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. @@ -154,7 +173,7 @@ 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. @@ -163,60 +182,72 @@ theorem eq_transpose : \forall i,j,k,n:nat. \lnot j=i \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. +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. 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.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 *) @@ -229,21 +260,21 @@ 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. +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. @@ -252,14 +283,14 @@ 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. +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. @@ -269,9 +300,9 @@ 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. +elim (H m).elim H3. +elim (H1 a).elim H6. +apply (ex_intro ? ? a1). split.assumption. rewrite > H8.assumption. assumption.assumption. @@ -279,70 +310,68 @@ 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. +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). -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. +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_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 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 @@ -354,343 +383,358 @@ 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. +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)). -simplify.apply H2.assumption. -simplify.intro.absurd m = S n1. -apply H3.assumption.simplify.intro. -apply not_le_Sn_n n1.rewrite < H5.assumption. +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. +(* 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. -intros.unfold transpose. -rewrite > not_eq_to_eqb_false m n1. -rewrite > not_eq_to_eqb_false m (S n1). +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. intro.apply lt_to_not_eq m (S n1). -apply trans_lt ? n1.assumption.simplify. apply le_n. +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. -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 ?. +apply (nat_case m ?). intros. -apply eq_map_iter_transpose_i_Si ? H H1. -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 (trans_eq ? ? (map_iter_i (S k) (\lambda m. g (transpose i (S(m1 + i)) m)) f n)). apply H2. -simplify. apply le_n. -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 (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 +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 (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))). +(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. +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 (? ? %). +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. -rewrite > H5 in \vdash (? ? %). +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. -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. -cut (S i) < j \lor (S i) = j. +simplify in H3. +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_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. -apply trans_le ? j.assumption.assumption. +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. -rewrite > transpose_i_i j.reflexivity. +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 (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. -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 +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