X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fpermutation.ma;h=3e987e9e8c0df185f4c2a48271fef43dee2a2a1d;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=cc0f4102789a60bf49144a043f4077222e8eb7cb;hpb=fb94e5a71be508516514dfe50528ccfb3cd2da91;p=helm.git diff --git a/helm/matita/library/nat/permutation.ma b/helm/matita/library/nat/permutation.ma index cc0f41027..3e987e9e8 100644 --- a/helm/matita/library/nat/permutation.ma +++ b/helm/matita/library/nat/permutation.ma @@ -22,7 +22,7 @@ definition injn: (nat \to nat) \to nat \to Prop \def 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. @@ -31,7 +31,7 @@ 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. +unfold injective.unfold injn.intros.apply H.assumption. qed. definition permut : (nat \to nat) \to nat \to Prop @@ -199,9 +199,9 @@ simplify. 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. simplify. @@ -210,7 +210,7 @@ rewrite > (not_eq_to_eqb_false i j). simplify. 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). @@ -225,7 +225,7 @@ theorem permut_S_to_permut_transpose: \forall f:nat \to nat. (f n)) m. unfold permut.intros. elim H. -split.intros.simplify. +split.intros.simplify.unfold transpose. apply (eqb_elim (f i) (f (S m))). intro.apply False_ind. cut (i = (S m)). @@ -310,7 +310,7 @@ qed. theorem bijn_transpose : \forall n,i,j. i \le n \to j \le n \to bijn (transpose i j) n. -intros.simplify.intros. +intros.unfold bijn.unfold transpose.intros. cut (m = i \lor \lnot m = i). elim Hcut. apply (ex_intro ? ? j). @@ -354,7 +354,7 @@ 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. +elim n.unfold bijn.intros. apply (ex_intro ? ? m). split.assumption. apply (le_n_O_elim m ? (\lambda p. f p = p)). @@ -370,7 +370,7 @@ elim H1.apply H2.apply le_n.apply le_n. apply bijn_n_Sn. apply H. apply permut_S_to_permut_transpose. -assumption.simplify. +assumption.unfold transpose. rewrite > (eqb_n_n (f (S n1))).simplify.reflexivity. qed. @@ -395,9 +395,9 @@ simplify. 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. +unfold Not.intro. apply (not_le_Sn_n n1).rewrite < H5.assumption. qed. @@ -552,15 +552,15 @@ rewrite < H. rewrite < (H1 (g (S m + n))). apply eq_f. apply eq_map_iter_i. -intros.unfold transpose. +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 ((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.apply le_S_S.assumption. +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 @@ -579,11 +579,11 @@ 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. +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. @@ -608,13 +608,13 @@ 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 H2. -simplify. apply le_n.assumption. +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. +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. @@ -623,23 +623,23 @@ apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g (transpose (S(m1 + i)) (S(S(m1 + i))) (transpose i (S(m1 + i)) m)))) f n)). apply (H2 m1). -simplify. apply le_n.assumption. +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. +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. +unfold Not. intro. apply (not_le_Sn_n i). rewrite > H7 in \vdash (? ? %). apply le_S_S. apply le_plus_n. -simplify. intro. +unfold Not. intro. apply (not_eq_n_Sn (S m1+i)). apply sym_eq.assumption. qed. @@ -726,11 +726,11 @@ 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. +simplify.unfold lt.apply le_S_S.apply le_plus_n.assumption. unfold permut in H3.elim H3. -simplify.intro. +simplify.unfold Not.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 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.