ocaml 3.09 transition

[helm.git] / helm / matita / library / nat / permutation.ma

diff --git a/helm/matita/library/nat/permutation.ma b/helm/matita/library/nat/permutation.ma
index cc0f4102789a60bf49144a043f4077222e8eb7cb..3e987e9e8c0df185f4c2a48271fef43dee2a2a1d 100644 (file)
--- 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.