From: Andrea Asperti Date: Mon, 26 Sep 2005 11:06:32 +0000 (+0000) Subject: permutation.ma added to the repository. X-Git-Tag: LAST_BEFORE_NEW~7 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c3b6e22034e3029195031d31c94983c381ae659b;p=helm.git permutation.ma added to the repository. --- diff --git a/helm/matita/library/nat/compare.ma b/helm/matita/library/nat/compare.ma index ba3151a3b..55e526c8f 100644 --- a/helm/matita/library/nat/compare.ma +++ b/helm/matita/library/nat/compare.ma @@ -64,6 +64,25 @@ apply (H H2). apply (H1 H2). qed. +theorem eqb_n_n: \forall n. eqb n n = true. +intro.elim n.simplify.reflexivity. +simplify.assumption. +qed. + +theorem eq_to_eqb_true: \forall n,m:nat. +n = m \to eqb n m = true. +intros.apply eqb_elim n m. +intros. reflexivity. +intros.apply False_ind.apply H1 H. +qed. + +theorem not_eq_to_eqb_false: \forall n,m:nat. +\lnot (n = m) \to eqb n m = false. +intros.apply eqb_elim n m. +intros. apply False_ind.apply H H1. +intros.reflexivity. +qed. + let rec leb n m \def match n with [ O \Rightarrow true diff --git a/helm/matita/library/nat/permutation.ma b/helm/matita/library/nat/permutation.ma new file mode 100644 index 000000000..0aea7b761 --- /dev/null +++ b/helm/matita/library/nat/permutation.ma @@ -0,0 +1,696 @@ +(**************************************************************************) +(* ___ *) +(* ||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 diff --git a/helm/matita/library/nat/sigma_and_pi.ma b/helm/matita/library/nat/sigma_and_pi.ma index 29df3a1df..470bb9d69 100644 --- a/helm/matita/library/nat/sigma_and_pi.ma +++ b/helm/matita/library/nat/sigma_and_pi.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/nat/sigma_and_pi". -include "nat/times.ma". +include "nat/lt_arith.ma". let rec sigma n f \def match n with @@ -24,4 +24,26 @@ let rec sigma n f \def let rec pi n f \def match n with [ O \Rightarrow (S O) - | (S p) \Rightarrow (f p)*(pi p f)]. \ No newline at end of file + | (S p) \Rightarrow (f p)*(pi p f)]. + +theorem eq_sigma: \forall f,g:nat \to nat. +\forall n:nat. (\forall m:nat. m < n \to f m = g m) \to +(sigma n f) = (sigma n g). +intros 3.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. + +theorem eq_pi: \forall f,g:nat \to nat. +\forall n:nat. (\forall m:nat. m < n \to f m = g m) \to +(pi n f) = (pi n g). +intros 3.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.