Yet another semantics for simplify.

diff --git a/helm/matita/library/Q/q.ma b/helm/matita/library/Q/q.ma
index d69e459acde20c6523d82872d24c08fc42dc1b7d..340154979777529f94387cd1c630c6234cf21ab5 100644 (file)
--- a/helm/matita/library/Q/q.ma
+++ b/helm/matita/library/Q/q.ma
@@ -92,13 +92,13 @@ definition ftl \def
     | (cons x f) \Rightarrow f].
     
 theorem injective_pp : injective nat fraction pp.
     | (cons x f) \Rightarrow f].
     
 theorem injective_pp : injective nat fraction pp.

-simplify.intros.
+unfold injective.intros.

 change with ((aux (pp x)) = (aux (pp y))).
 apply eq_f.assumption.
 qed.
 
 theorem injective_nn : injective nat fraction nn.
 change with ((aux (pp x)) = (aux (pp y))).
 apply eq_f.assumption.
 qed.
 
 theorem injective_nn : injective nat fraction nn.

-simplify.intros.
+unfold injective.intros.

 change with ((aux (nn x)) = (aux (nn y))).
 apply eq_f.assumption.
 qed.
 change with ((aux (nn x)) = (aux (nn y))).
 apply eq_f.assumption.
 qed.


@@ -118,7 +118,7 @@ apply eq_f.assumption.
 qed.
 
 theorem not_eq_pp_nn: \forall n,m:nat. pp n \neq nn m.
 qed.
 
 theorem not_eq_pp_nn: \forall n,m:nat. pp n \neq nn m.

-intros.simplify. intro.
+intros.unfold Not. intro.

 change with match (pp n) with
 [ (pp n) \Rightarrow False
 | (nn n) \Rightarrow True
 change with match (pp n) with
 [ (pp n) \Rightarrow False
 | (nn n) \Rightarrow True


@@ -130,7 +130,7 @@ qed.
 theorem not_eq_pp_cons: 
 \forall n:nat.\forall x:Z. \forall f:fraction. 
 pp n \neq cons x f.
 theorem not_eq_pp_cons: 
 \forall n:nat.\forall x:Z. \forall f:fraction. 
 pp n \neq cons x f.

-intros.simplify. intro.
+intros.unfold Not. intro.

 change with match (pp n) with
 [ (pp n) \Rightarrow False
 | (nn n) \Rightarrow True
 change with match (pp n) with
 [ (pp n) \Rightarrow False
 | (nn n) \Rightarrow True


@@ -142,7 +142,7 @@ qed.
 theorem not_eq_nn_cons: 
 \forall n:nat.\forall x:Z. \forall f:fraction. 
 nn n \neq cons x f.
 theorem not_eq_nn_cons: 
 \forall n:nat.\forall x:Z. \forall f:fraction. 
 nn n \neq cons x f.

-intros.simplify. intro.
+intros.unfold Not. intro.

 change with match (nn n) with
 [ (pp n) \Rightarrow True
 | (nn n) \Rightarrow False
 change with match (nn n) with
 [ (pp n) \Rightarrow True
 | (nn n) \Rightarrow False


@@ -153,7 +153,7 @@ qed.
 
 theorem decidable_eq_fraction: \forall f,g:fraction.
 decidable (f = g).
 
 theorem decidable_eq_fraction: \forall f,g:fraction.
 decidable (f = g).

-intros.simplify.
+intros.unfold decidable.

 apply (fraction_elim2 (\lambda f,g. f=g \lor (f=g \to False))).
   intros.elim g1.
     elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)).
 apply (fraction_elim2 (\lambda f,g. f=g \lor (f=g \to False))).
   intros.elim g1.
     elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)).


@@ -188,16 +188,16 @@ intros.apply (fraction_elim2
   intros.elim g1.
     simplify.apply eqb_elim.
       intro.simplify.apply eq_f.assumption.
   intros.elim g1.
     simplify.apply eqb_elim.
       intro.simplify.apply eq_f.assumption.

-      intro.simplify.intro.apply H.apply injective_pp.assumption.
+      intro.simplify.unfold Not.intro.apply H.apply injective_pp.assumption.

     simplify.apply not_eq_pp_nn.
     simplify.apply not_eq_pp_cons.
   intros.elim g1.
     simplify.apply not_eq_pp_nn.
     simplify.apply not_eq_pp_cons.
   intros.elim g1.

-    simplify.intro.apply (not_eq_pp_nn n1 n).apply sym_eq. assumption.
+    simplify.unfold Not.intro.apply (not_eq_pp_nn n1 n).apply sym_eq. assumption.

     simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption.
     simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption.

-    intro.simplify.intro.apply H.apply injective_nn.assumption.
+    intro.simplify.unfold Not.intro.apply H.apply injective_nn.assumption.

   simplify.apply not_eq_nn_cons.
   simplify.apply not_eq_nn_cons.

-  intros.simplify.intro.apply (not_eq_pp_cons m x f1).apply sym_eq. assumption.
-  intros.simplify.intro.apply (not_eq_nn_cons m x f1).apply sym_eq. assumption.
+  intros.simplify.unfold Not.intro.apply (not_eq_pp_cons m x f1).apply sym_eq. assumption.
+  intros.simplify.unfold Not.intro.apply (not_eq_nn_cons m x f1).apply sym_eq. assumption.

   intros.
    change in match (eqfb (cons x f1) (cons y g1)) 
    with (andb (eqZb x y) (eqfb f1 g1)).
   intros.
    change in match (eqfb (cons x f1) (cons y g1)) 
    with (andb (eqZb x y) (eqfb f1 g1)).


@@ -205,8 +205,8 @@ intros.apply (fraction_elim2
       intro.generalize in match H.elim (eqfb f1 g1).
         simplify.apply eq_f2.assumption.
         apply H2.
       intro.generalize in match H.elim (eqfb f1 g1).
         simplify.apply eq_f2.assumption.
         apply H2.

-      simplify.intro.apply H2.apply (eq_cons_to_eq2 x y).assumption.
-      intro.simplify.intro.apply H1.apply (eq_cons_to_eq1 f1 g1).assumption.
+      simplify.unfold Not.intro.apply H2.apply (eq_cons_to_eq2 x y).assumption.
+      intro.simplify.unfold Not.intro.apply H1.apply (eq_cons_to_eq1 f1 g1).assumption.

 qed.
 
 let rec finv f \def
 qed.
 
 let rec finv f \def


@@ -243,7 +243,7 @@ let rec ftimes f g \def
         | (frac h) \Rightarrow frac (cons (x + y) h)]]].
         
 theorem symmetric2_ftimes: symmetric2 fraction ratio ftimes.
         | (frac h) \Rightarrow frac (cons (x + y) h)]]].
         
 theorem symmetric2_ftimes: symmetric2 fraction ratio ftimes.

-simplify. intros.apply (fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f)).
+unfold symmetric2. intros.apply (fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f)).

   intros.elim g.
     change with (Z_to_ratio (pos n + pos n1) = Z_to_ratio (pos n1 + pos n)).
      apply eq_f.apply sym_Zplus.
   intros.elim g.
     change with (Z_to_ratio (pos n + pos n1) = Z_to_ratio (pos n1 + pos n)).
      apply eq_f.apply sym_Zplus.

diff --git a/helm/matita/library/Z/compare.ma b/helm/matita/library/Z/compare.ma
index a59100885e791d8ba504fc07e970d57266bcb920..4a5025975fe3d8d4b3f610563b565dce39be6bac 100644 (file)
--- a/helm/matita/library/Z/compare.ma
+++ b/helm/matita/library/Z/compare.ma
@@ -49,17 +49,17 @@ elim x.
     simplify.apply not_eq_OZ_pos.
     simplify.apply not_eq_OZ_neg.
   elim y.
     simplify.apply not_eq_OZ_pos.
     simplify.apply not_eq_OZ_neg.
   elim y.

-    simplify.intro.apply (not_eq_OZ_pos n).apply sym_eq.assumption.
+    simplify.unfold Not.intro.apply (not_eq_OZ_pos n).apply sym_eq.assumption.

     simplify.apply eqb_elim.
       intro.simplify.apply eq_f.assumption.
     simplify.apply eqb_elim.
       intro.simplify.apply eq_f.assumption.

-      intro.simplify.intro.apply H.apply inj_pos.assumption.
+      intro.simplify.unfold Not.intro.apply H.apply inj_pos.assumption.

     simplify.apply not_eq_pos_neg.
   elim y.
     simplify.apply not_eq_pos_neg.
   elim y.

-    simplify.intro.apply (not_eq_OZ_neg n).apply sym_eq.assumption.
-    simplify.intro.apply (not_eq_pos_neg n1 n).apply sym_eq.assumption.
+    simplify.unfold Not.intro.apply (not_eq_OZ_neg n).apply sym_eq.assumption.
+    simplify.unfold Not.intro.apply (not_eq_pos_neg n1 n).apply sym_eq.assumption.

     simplify.apply eqb_elim.
       intro.simplify.apply eq_f.assumption.
     simplify.apply eqb_elim.
       intro.simplify.apply eq_f.assumption.

-      intro.simplify.intro.apply H.apply inj_neg.assumption.
+      intro.simplify.unfold Not.intro.apply H.apply inj_neg.assumption.

 qed.
 
 theorem eqZb_elim: \forall x,y:Z.\forall P:bool \to Prop.
 qed.
 
 theorem eqZb_elim: \forall x,y:Z.\forall P:bool \to Prop.

diff --git a/helm/matita/library/Z/orders.ma b/helm/matita/library/Z/orders.ma
index 186533ea08fb45ae82fd590c8e52f7ffded634c4..c39f693085398eedf4a95a9f15898f05e6cee264 100644 (file)
--- a/helm/matita/library/Z/orders.ma
+++ b/helm/matita/library/Z/orders.ma
@@ -71,9 +71,9 @@ theorem irreflexive_Zlt: irreflexive Z Zlt.
 change with (\forall x:Z. x < x \to False).
 intro.elim x.exact H.
 cut (neg n < neg n \to False).
 change with (\forall x:Z. x < x \to False).
 intro.elim x.exact H.
 cut (neg n < neg n \to False).

-apply Hcut.apply H.simplify.apply not_le_Sn_n.
+apply Hcut.apply H.simplify.unfold lt.apply not_le_Sn_n.

 cut (pos n < pos n \to False).
 cut (pos n < pos n \to False).

-apply Hcut.apply H.simplify.apply not_le_Sn_n.
+apply Hcut.apply H.simplify.unfold lt.apply not_le_Sn_n.

 qed.
 
 theorem irrefl_Zlt: irreflexive Z Zlt
 qed.
 
 theorem irrefl_Zlt: irreflexive Z Zlt

diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma
index 27266bf393c41e5457f5cd6723bb8276035df5c6..e5e1cdb452fa38ce33a8ba73f95b6ca4a5d5f27d 100644 (file)
--- a/helm/matita/library/Z/times.ma
+++ b/helm/matita/library/Z/times.ma
@@ -140,7 +140,7 @@ reflexivity.
 (* we now close all positivity conditions *)
 apply lt_O_times_S_S.                    
 apply lt_O_times_S_S.
 (* we now close all positivity conditions *)
 apply lt_O_times_S_S.                    
 apply lt_O_times_S_S.

-simplify.
+simplify.unfold lt.

 apply le_SO_minus.  exact H.
 qed.
 
 apply le_SO_minus.  exact H.
 qed.
 

diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma
index d1a846da4754c07161cbaf668a895c0b22846096..d18c80b23ac323b996280a835a52912fc2ffc8ce 100644 (file)
--- a/helm/matita/library/Z/z.ma
+++ b/helm/matita/library/Z/z.ma
@@ -54,15 +54,15 @@ match OZ_test z with
 |false \Rightarrow z \neq OZ].
 intros.elim z.
 simplify.reflexivity.
 |false \Rightarrow z \neq OZ].
 intros.elim z.
 simplify.reflexivity.

-simplify.intros (H).
+simplify. unfold Not. intros (H).

 discriminate H.
 discriminate H.

-simplify.intros (H).
+simplify. unfold Not. intros (H).

 discriminate H.
 qed.
 
 (* discrimination *)
 theorem injective_pos: injective nat Z pos.
 discriminate H.
 qed.
 
 (* discrimination *)
 theorem injective_pos: injective nat Z pos.

-simplify.
+unfold injective.

 intros.
 change with (abs (pos x) = abs (pos y)).
 apply eq_f.assumption.
 intros.
 change with (abs (pos x) = abs (pos y)).
 apply eq_f.assumption.


@@ -72,7 +72,7 @@ variant inj_pos : \forall n,m:nat. pos n = pos m \to n = m
 \def injective_pos.
 
 theorem injective_neg: injective nat Z neg.
 \def injective_pos.
 
 theorem injective_neg: injective nat Z neg.

-simplify.
+unfold injective.

 intros.
 change with (abs (neg x) = abs (neg y)).
 apply eq_f.assumption.
 intros.
 change with (abs (neg x) = abs (neg y)).
 apply eq_f.assumption.


@@ -82,22 +82,22 @@ variant inj_neg : \forall n,m:nat. neg n = neg m \to n = m
 \def injective_neg.
 
 theorem not_eq_OZ_pos: \forall n:nat. OZ \neq pos n.
 \def injective_neg.
 
 theorem not_eq_OZ_pos: \forall n:nat. OZ \neq pos n.

-simplify.intros (n H).
+unfold Not.intros (n H).

 discriminate H.
 qed.
 
 theorem not_eq_OZ_neg :\forall n:nat. OZ \neq neg n.
 discriminate H.
 qed.
 
 theorem not_eq_OZ_neg :\forall n:nat. OZ \neq neg n.

-simplify.intros (n H).
+unfold Not.intros (n H).

 discriminate H.
 qed.
 
 theorem not_eq_pos_neg :\forall n,m:nat. pos n \neq neg m.
 discriminate H.
 qed.
 
 theorem not_eq_pos_neg :\forall n,m:nat. pos n \neq neg m.

-simplify.intros (n m H).
+unfold Not.intros (n m H).

 discriminate H.
 qed.
 
 theorem decidable_eq_Z : \forall x,y:Z. decidable (x=y).
 discriminate H.
 qed.
 
 theorem decidable_eq_Z : \forall x,y:Z. decidable (x=y).

-intros.simplify.
+intros.unfold decidable.

 elim x.
 (* goal: x=OZ *)
   elim y.
 elim x.
 (* goal: x=OZ *)
   elim y.


@@ -110,25 +110,25 @@ elim x.
 (* goal: x=pos *)
   elim y.
   (* goal: x=pos y=OZ *)
 (* goal: x=pos *)
   elim y.
   (* goal: x=pos y=OZ *)

-    right.intro.
+    right.unfold Not.intro.

     apply (not_eq_OZ_pos n). symmetry. assumption.
   (* goal: x=pos y=pos *)
     elim (decidable_eq_nat n n1:((n=n1) \lor ((n=n1) \to False))).
     left.apply eq_f.assumption.
     apply (not_eq_OZ_pos n). symmetry. assumption.
   (* goal: x=pos y=pos *)
     elim (decidable_eq_nat n n1:((n=n1) \lor ((n=n1) \to False))).
     left.apply eq_f.assumption.

-    right.intros (H_inj).apply H. injection H_inj. assumption.
+    right.unfold Not.intros (H_inj).apply H. injection H_inj. assumption.

   (* goal: x=pos y=neg *)
   (* goal: x=pos y=neg *)

-    right.intro.apply (not_eq_pos_neg n n1). assumption.
+    right.unfold Not.intro.apply (not_eq_pos_neg n n1). assumption.

 (* goal: x=neg *)
   elim y.
   (* goal: x=neg y=OZ *)
 (* goal: x=neg *)
   elim y.
   (* goal: x=neg y=OZ *)

-    right.intro.
+    right.unfold Not.intro.

     apply (not_eq_OZ_neg n). symmetry. assumption.
   (* goal: x=neg y=pos *)
     apply (not_eq_OZ_neg n). symmetry. assumption.
   (* goal: x=neg y=pos *)

-    right. intro. apply (not_eq_pos_neg n1 n). symmetry. assumption.
+    right. unfold Not.intro. apply (not_eq_pos_neg n1 n). symmetry. assumption.

   (* goal: x=neg y=neg *)
     elim (decidable_eq_nat n n1:((n=n1) \lor ((n=n1) \to False))).
     left.apply eq_f.assumption.
   (* goal: x=neg y=neg *)
     elim (decidable_eq_nat n n1:((n=n1) \lor ((n=n1) \to False))).
     left.apply eq_f.assumption.

-    right.intro.apply H.apply injective_neg.assumption.
+    right.unfold Not.intro.apply H.apply injective_neg.assumption.

 qed.
 
 (* end discrimination *)
 qed.
 
 (* end discrimination *)

diff --git a/helm/matita/library/datatypes/bool.ma b/helm/matita/library/datatypes/bool.ma
index 11f1d7a8c49d48047e12caaeec555c207e1ca784..f4aec8167476b0d88204a06d3d23aaa798a323ac 100644 (file)
--- a/helm/matita/library/datatypes/bool.ma
+++ b/helm/matita/library/datatypes/bool.ma
@@ -32,7 +32,7 @@ theorem bool_elim: \forall P:bool \to Prop. \forall b:bool.
 qed.
 
 theorem not_eq_true_false : true \neq false.
 qed.
 
 theorem not_eq_true_false : true \neq false.

-simplify.intro.
+unfold Not.intro.

 change with 
 match true with
 [ true \Rightarrow False
 change with 
 match true with
 [ true \Rightarrow False

diff --git a/helm/matita/library/list/sort.ma b/helm/matita/library/list/sort.ma
index 2d60662a4d8f19e3d3d5894110782878a9927092..1cc127759f0b37f8778491389718224a0215a85f 100644 (file)
--- a/helm/matita/library/list/sort.ma
+++ b/helm/matita/library/list/sort.ma
@@ -74,7 +74,8 @@ lemma ordered_injective:
       [ generalize in match Hcut; 
         apply andb_elim;
         elim (le s s1);
       [ generalize in match Hcut; 
         apply andb_elim;
         elim (le s s1);

-        [ change with (ordered A le (s1::l2) = true \to ordered A le (s1::l2) = true).
+        [ simplify;
+          fold simplify (ordered ? le (s1::l2));

           intros; assumption;
         | simplify;
           intros (Habsurd);
           intros; assumption;
         | simplify;
           intros (Habsurd);


@@ -96,11 +97,11 @@ lemma insert_sorted:
     ordered A le l = true \to ordered A le (insert A le x l) = true.
   intros 5 (A le H l x).
   elim l;
     ordered A le l = true \to ordered A le (insert A le x l) = true.
   intros 5 (A le H l x).
   elim l;

-  [ 2: change with (ordered A le (match le x s with
-         [ true ⇒ x::(s::l1) | false ⇒ s::(insert A le x l1) ]) = true).
+  [ 2: simplify;

        apply (bool_elim ? (le x s));
        [ intros;
        apply (bool_elim ? (le x s));
        [ intros;

-         change with ((le x s \land ordered A le (s::l1)) = true);
+         simplify;
+         fold simplify (ordered ? le (s::l1));

          apply andb_elim;
          rewrite > H3;
          assumption;
          apply andb_elim;
          rewrite > H3;
          assumption;


@@ -112,22 +113,25 @@ lemma insert_sorted:
          [ simplify;
            rewrite > (H x a H2);
            reflexivity;
          [ simplify;
            rewrite > (H x a H2);
            reflexivity;

-         | change with ((ordered A le (a::match le x s with
-              [ true ⇒ x::s::l2 | false ⇒ s::(insert A le x l2) ])) = true).
+         | simplify in \vdash (? ? (? ? ? %) ?);

             apply (bool_elim ? (le x s));
             [ intros;
             apply (bool_elim ? (le x s));
             [ intros;

-              change with ((le a x \land (le x s \land ordered A le (s::l2))) = true).
+              simplify;
+              fold simplify (ordered A le (s::l2));

               apply andb_elim;
               rewrite > (H x a H3);
               apply andb_elim;
               rewrite > (H x a H3);

-              change with ((le x s \land ordered A le (s::l2)) = true).
+              simplify;
+              fold simplify (ordered A le (s::l2));

               apply andb_elim;
               rewrite > H4;
               apply (ordered_injective A le (a::s::l2));
               assumption;
             | intros;
               apply andb_elim;
               rewrite > H4;
               apply (ordered_injective A le (a::s::l2));
               assumption;
             | intros;

-              change with ((le a s \land ordered A le (s::(insert A le x l2))) = true);
+              simplify;
+              fold simplify (ordered A le (s::(insert A le x l2)));

               apply andb_elim;
               apply andb_elim;

-              change in H2 with ((le a s \land ordered A le (s::l2)) = true); 
+              simplify in H2;
+              fold simplify (ordered A le (s::l2)) in H2;

               generalize in match H2;
               apply (andb_elim (le a s));
               elim (le a s);
               generalize in match H2;
               apply (andb_elim (le a s));
               elim (le a s);

diff --git a/helm/matita/library/logic/equality.ma b/helm/matita/library/logic/equality.ma
index 40157d849f9baf53e9f871f07ef5432adba152c9..b87dc6c95656dcf5de3c3ceb00e9ed105067c6b8 100644 (file)
--- a/helm/matita/library/logic/equality.ma
+++ b/helm/matita/library/logic/equality.ma
@@ -41,14 +41,14 @@ simplify.intros.apply refl_eq.
 qed.
     
 theorem symmetric_eq: \forall A:Type. symmetric A (eq A).
 qed.
     
 theorem symmetric_eq: \forall A:Type. symmetric A (eq A).

-simplify.intros.elim H. apply refl_eq.
+unfold symmetric.intros.elim H. apply refl_eq.

 qed.
 
 theorem sym_eq : \forall A:Type.\forall x,y:A. x=y  \to y=x
 \def symmetric_eq.
 
 theorem transitive_eq : \forall A:Type. transitive A (eq A).
 qed.
 
 theorem sym_eq : \forall A:Type.\forall x,y:A. x=y  \to y=x
 \def symmetric_eq.
 
 theorem transitive_eq : \forall A:Type. transitive A (eq A).

-simplify.intros.elim H1.assumption.
+unfold transitive.intros.elim H1.assumption.

 qed.
 
 theorem trans_eq : \forall A:Type.\forall x,y,z:A. x=y  \to y=z \to x=z
 qed.
 
 theorem trans_eq : \forall A:Type.\forall x,y,z:A. x=y  \to y=z \to x=z

diff --git a/helm/matita/library/nat/chinese_reminder.ma b/helm/matita/library/nat/chinese_reminder.ma
index f14f16d2792c3f2d291db23ee8d4586d9520df01..30cc7440f8a723d99fc1b6cd8371ce5bdbcf1931 100644 (file)
--- a/helm/matita/library/nat/chinese_reminder.ma
+++ b/helm/matita/library/nat/chinese_reminder.ma
@@ -53,7 +53,7 @@ apply minus_to_plus.
 apply lt_to_le.
 change with (O + a2*m < a1*n).
 apply lt_minus_to_plus.
 apply lt_to_le.
 change with (O + a2*m < a1*n).
 apply lt_minus_to_plus.

-rewrite > H5.simplify.apply le_n.
+rewrite > H5.unfold lt.apply le_n.

 assumption.
 (* congruent to b *)
 cut (a2*m = a1*n - (S O)).
 assumption.
 (* congruent to b *)
 cut (a2*m = a1*n - (S O)).


@@ -84,7 +84,7 @@ apply minus_to_plus.
 apply lt_to_le.
 change with (O + a2*m < a1*n).
 apply lt_minus_to_plus.
 apply lt_to_le.
 change with (O + a2*m < a1*n).
 apply lt_minus_to_plus.

-rewrite > H5.simplify.apply le_n.
+rewrite > H5.unfold lt.apply le_n.

 assumption.
 (* and now the symmetric case; the price to pay for working
    in nat instead than Z *)
 assumption.
 (* and now the symmetric case; the price to pay for working
    in nat instead than Z *)


@@ -119,7 +119,7 @@ apply minus_to_plus.
 apply lt_to_le.
 change with (O + a1*n < a2*m).
 apply lt_minus_to_plus.
 apply lt_to_le.
 change with (O + a1*n < a2*m).
 apply lt_minus_to_plus.

-rewrite > H5.simplify.apply le_n.
+rewrite > H5.unfold lt.apply le_n.

 assumption.
 (* congruent to a *)
 cut (a2*m = a1*n + (S O)).
 assumption.
 (* congruent to a *)
 cut (a2*m = a1*n + (S O)).


@@ -149,7 +149,7 @@ apply minus_to_plus.
 apply lt_to_le.
 change with (O + a1*n < a2*m).
 apply lt_minus_to_plus.
 apply lt_to_le.
 change with (O + a1*n < a2*m).
 apply lt_minus_to_plus.

-rewrite > H5.simplify.apply le_n.
+rewrite > H5.unfold lt.apply le_n.

 assumption.
 (* proof of the cut *)
 rewrite < H2.
 assumption.
 (* proof of the cut *)
 rewrite < H2.

diff --git a/helm/matita/library/nat/compare.ma b/helm/matita/library/nat/compare.ma
index e85a802652e9ce8ba67d3b6b511eaf5b06bc6ea3..2647315804661a23db188e36b4955c0b01c5152a 100644 (file)
--- a/helm/matita/library/nat/compare.ma
+++ b/helm/matita/library/nat/compare.ma
@@ -42,13 +42,13 @@ intro.elim n1.
 simplify.reflexivity.
 simplify.apply not_eq_O_S.
 intro.
 simplify.reflexivity.
 simplify.apply not_eq_O_S.
 intro.

-simplify.
+simplify.unfold Not.

 intro. apply (not_eq_O_S n1).apply sym_eq.assumption.
 intros.simplify.
 generalize in match H.
 elim ((eqb n1 m1)).
 simplify.apply eq_f.apply H1.
 intro. apply (not_eq_O_S n1).apply sym_eq.assumption.
 intros.simplify.
 generalize in match H.
 elim ((eqb n1 m1)).
 simplify.apply eq_f.apply H1.

-simplify.intro.apply H1.apply inj_S.assumption.
+simplify.unfold Not.intro.apply H1.apply inj_S.assumption.

 qed.
 
 theorem eqb_elim : \forall n,m:nat.\forall P:bool \to Prop.
 qed.
 
 theorem eqb_elim : \forall n,m:nat.\forall P:bool \to Prop.


@@ -126,7 +126,7 @@ simplify.exact le_O_n.
 simplify.exact not_le_Sn_O.
 intros 2.simplify.elim ((leb n1 m1)).
 simplify.apply le_S_S.apply H.
 simplify.exact not_le_Sn_O.
 intros 2.simplify.elim ((leb n1 m1)).
 simplify.apply le_S_S.apply H.

-simplify.intros.apply H.apply le_S_S_to_le.assumption.
+simplify.unfold Not.intros.apply H.apply le_S_S_to_le.assumption.

 qed.
 
 theorem leb_elim: \forall n,m:nat. \forall P:bool \to Prop. 
 qed.
 
 theorem leb_elim: \forall n,m:nat. \forall P:bool \to Prop. 


@@ -191,12 +191,12 @@ apply (nat_elim2 (\lambda n,m.match (nat_compare n m) with
   | EQ \Rightarrow n=m
   | GT \Rightarrow m < n ])).
 intro.elim n1.simplify.reflexivity.
   | EQ \Rightarrow n=m
   | GT \Rightarrow m < n ])).
 intro.elim n1.simplify.reflexivity.

-simplify.apply le_S_S.apply le_O_n.
-intro.simplify.apply le_S_S. apply le_O_n.
+simplify.unfold lt.apply le_S_S.apply le_O_n.
+intro.simplify.unfold lt.apply le_S_S. apply le_O_n.

 intros 2.simplify.elim ((nat_compare n1 m1)).
 intros 2.simplify.elim ((nat_compare n1 m1)).

-simplify. apply le_S_S.apply H.
+simplify. unfold lt. apply le_S_S.apply H.

 simplify. apply eq_f. apply H.
 simplify. apply eq_f. apply H.

-simplify. apply le_S_S.apply H.
+simplify. unfold lt.apply le_S_S.apply H.

 qed.
 
 theorem nat_compare_n_m_m_n: \forall n,m:nat. 
 qed.
 
 theorem nat_compare_n_m_m_n: \forall n,m:nat. 

diff --git a/helm/matita/library/nat/count.ma b/helm/matita/library/nat/count.ma
index 60bdbadc4c228ebc5019eea85d783fd70e00757d..20913fa6041c103527cfd73e7a5c7708b15924de 100644 (file)
--- a/helm/matita/library/nat/count.ma
+++ b/helm/matita/library/nat/count.ma
@@ -78,7 +78,7 @@ rewrite < plus_n_O.
 rewrite < H.
 rewrite > (S_pred ((S n1)*(S m))).
 apply sigma_plus1.
 rewrite < H.
 rewrite > (S_pred ((S n1)*(S m))).
 apply sigma_plus1.

-simplify.apply le_S_S.apply le_O_n.
+simplify.unfold lt.apply le_S_S.apply le_O_n.

 qed.
 
 theorem eq_sigma_sigma1 : \forall n,m:nat.\forall f:nat \to nat.
 qed.
 
 theorem eq_sigma_sigma1 : \forall n,m:nat.\forall f:nat \to nat.


@@ -138,15 +138,15 @@ rewrite > (div_mod_spec_to_eq2 (i1*(S n) + i) (S n) ((i1*(S n) + i)/(S n))
                                         ((i1*(S n) + i) \mod (S n)) i1 i).
 rewrite > H3.
 apply bool_to_nat_andb.
                                         ((i1*(S n) + i) \mod (S n)) i1 i).
 rewrite > H3.
 apply bool_to_nat_andb.

-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.

 apply div_mod_spec_div_mod.
 apply div_mod_spec_div_mod.

-simplify.apply le_S_S.apply le_O_n.
-constructor 1.simplify.apply le_S_S.assumption.
+unfold lt.apply le_S_S.apply le_O_n.
+constructor 1.unfold lt.apply le_S_S.assumption.

 reflexivity.
 apply div_mod_spec_div_mod.
 reflexivity.
 apply div_mod_spec_div_mod.

-simplify.apply le_S_S.apply le_O_n.
-constructor 1.simplify.apply le_S_S.assumption.
+unfold lt.apply le_S_S.apply le_O_n.
+constructor 1.unfold lt.apply le_S_S.assumption.

 reflexivity.
 apply (trans_eq ? ? 
 (sigma n (\lambda n.((bool_to_nat (f1 n)) *
 reflexivity.
 apply (trans_eq ? ? 
 (sigma n (\lambda n.((bool_to_nat (f1 n)) *


@@ -170,13 +170,13 @@ rewrite < S_pred in \vdash (? ? %).
 change with ((g (i/(S n)) (i \mod (S n))) \lt (S n)*(S m)).
 apply H.
 apply lt_mod_m_m.
 change with ((g (i/(S n)) (i \mod (S n))) \lt (S n)*(S m)).
 apply H.
 apply lt_mod_m_m.

-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.

 apply (lt_times_to_lt_l n).
 apply (le_to_lt_to_lt ? i).
 rewrite > (div_mod i (S n)) in \vdash (? ? %).
 rewrite > sym_plus.
 apply le_plus_n.
 apply (lt_times_to_lt_l n).
 apply (le_to_lt_to_lt ? i).
 rewrite > (div_mod i (S n)) in \vdash (? ? %).
 rewrite > sym_plus.
 apply le_plus_n.

-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.

 unfold lt.
 rewrite > S_pred in \vdash (? ? %).
 apply le_S_S.
 unfold lt.
 rewrite > S_pred in \vdash (? ? %).
 apply le_S_S.


@@ -184,12 +184,12 @@ rewrite > plus_n_O in \vdash (? ? %).
 rewrite > sym_times. assumption.
 rewrite > (times_n_O O).
 apply lt_times.
 rewrite > sym_times. assumption.
 rewrite > (times_n_O O).
 apply lt_times.

-simplify. apply le_S_S.apply le_O_n.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.

 rewrite > (times_n_O O).
 apply lt_times.
 rewrite > (times_n_O O).
 apply lt_times.

-simplify. apply le_S_S.apply le_O_n.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.

 rewrite < plus_n_O.
 unfold injn.
 intros.
 rewrite < plus_n_O.
 unfold injn.
 intros.


@@ -206,40 +206,40 @@ rewrite < (H2 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3) in \vdash (? ? (? % ?) ?).
 rewrite < (H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5).
 rewrite < (H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5) in \vdash (? ? ? (? % ?)).
 rewrite > H6.reflexivity.
 rewrite < (H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5).
 rewrite < (H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5) in \vdash (? ? ? (? % ?)).
 rewrite > H6.reflexivity.

-simplify. apply le_S_S.apply le_O_n.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.

 apply (lt_times_to_lt_l n).
 apply (le_to_lt_to_lt ? j).
 rewrite > (div_mod j (S n)) in \vdash (? ? %).
 rewrite > sym_plus.
 apply le_plus_n.
 apply (lt_times_to_lt_l n).
 apply (le_to_lt_to_lt ? j).
 rewrite > (div_mod j (S n)) in \vdash (? ? %).
 rewrite > sym_plus.
 apply le_plus_n.

-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.

 rewrite < sym_times. assumption.
 apply lt_mod_m_m.
 rewrite < sym_times. assumption.
 apply lt_mod_m_m.

-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.

 apply (lt_times_to_lt_l n).
 apply (le_to_lt_to_lt ? i).
 rewrite > (div_mod i (S n)) in \vdash (? ? %).
 rewrite > sym_plus.
 apply le_plus_n.
 apply (lt_times_to_lt_l n).
 apply (le_to_lt_to_lt ? i).
 rewrite > (div_mod i (S n)) in \vdash (? ? %).
 rewrite > sym_plus.
 apply le_plus_n.

-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.

 rewrite < sym_times. assumption.
 apply lt_mod_m_m.
 rewrite < sym_times. assumption.
 apply lt_mod_m_m.

-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.

 unfold lt.
 rewrite > S_pred in \vdash (? ? %).
 apply le_S_S.assumption.
 rewrite > (times_n_O O).
 apply lt_times.
 unfold lt.
 rewrite > S_pred in \vdash (? ? %).
 apply le_S_S.assumption.
 rewrite > (times_n_O O).
 apply lt_times.

-simplify. apply le_S_S.apply le_O_n.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.

 unfold lt.
 rewrite > S_pred in \vdash (? ? %).
 apply le_S_S.assumption.
 rewrite > (times_n_O O).
 apply lt_times.
 unfold lt.
 rewrite > S_pred in \vdash (? ? %).
 apply le_S_S.assumption.
 rewrite > (times_n_O O).
 apply lt_times.

-simplify. apply le_S_S.apply le_O_n.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.

 intros.
 apply False_ind.
 apply (not_le_Sn_O m1 H4).
 intros.
 apply False_ind.
 apply (not_le_Sn_O m1 H4).

diff --git a/helm/matita/library/nat/div_and_mod.ma b/helm/matita/library/nat/div_and_mod.ma
index 9995830a9061b1662447a6d8f99329b4f4e50430..e9831f82ad1ec5cc01decf9e920f9e80518c3f64 100644 (file)
--- a/helm/matita/library/nat/div_and_mod.ma
+++ b/helm/matita/library/nat/div_and_mod.ma
@@ -70,7 +70,7 @@ qed.
 theorem lt_mod_m_m: \forall n,m. O < m \to (n \mod m) < m.
 intros 2.elim m.apply False_ind.
 apply (not_le_Sn_O O H).
 theorem lt_mod_m_m: \forall n,m. O < m \to (n \mod m) < m.
 intros 2.elim m.apply False_ind.
 apply (not_le_Sn_O O H).

-simplify.apply le_S_S.apply le_mod_aux_m_m.
+simplify.unfold lt.apply le_S_S.apply le_mod_aux_m_m.

 apply le_n.
 qed.
 
 apply le_n.
 qed.
 


@@ -108,7 +108,7 @@ definition div_mod_spec : nat \to nat \to nat \to nat \to Prop \def
 *)
 
 theorem div_mod_spec_to_not_eq_O: \forall n,m,q,r.(div_mod_spec n m q r) \to m \neq O.
 *)
 
 theorem div_mod_spec_to_not_eq_O: \forall n,m,q,r.(div_mod_spec n m q r) \to m \neq O.

-intros 4.simplify.intros.elim H.absurd (le (S r) O).
+intros 4.unfold Not.intros.elim H.absurd (le (S r) O).

 rewrite < H1.assumption.
 exact (not_le_Sn_O r).
 qed.
 rewrite < H1.assumption.
 exact (not_le_Sn_O r).
 qed.


@@ -188,7 +188,7 @@ qed.
 
 theorem div_mod_spec_times : \forall n,m:nat.div_mod_spec ((S n)*m) (S n) m O.
 intros.constructor 1.
 
 theorem div_mod_spec_times : \forall n,m:nat.div_mod_spec ((S n)*m) (S n) m O.
 intros.constructor 1.

-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.

 rewrite < plus_n_O.rewrite < sym_times.reflexivity.
 qed.
 
 rewrite < plus_n_O.rewrite < sym_times.reflexivity.
 qed.
 


@@ -198,7 +198,7 @@ intros.
 apply (div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O).
 goal 15. (* ?11 is closed with the following tactics *)
 apply div_mod_spec_div_mod.
 apply (div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O).
 goal 15. (* ?11 is closed with the following tactics *)
 apply div_mod_spec_div_mod.

-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.

 apply div_mod_spec_times.
 qed.
 
 apply div_mod_spec_times.
 qed.
 

diff --git a/helm/matita/library/nat/exp.ma b/helm/matita/library/nat/exp.ma
index 49e3bbd70f16a67399bacfa77d4d8001c2e231dd..11d84f74ca7deb3b676007693f72b585c0547435 100644 (file)
--- a/helm/matita/library/nat/exp.ma
+++ b/helm/matita/library/nat/exp.ma
@@ -48,14 +48,14 @@ rewrite < times_n_Sm.reflexivity.
 qed.
 
 theorem lt_O_exp: \forall n,m:nat. O < n \to O < n \sup m. 
 qed.
 
 theorem lt_O_exp: \forall n,m:nat. O < n \to O < n \sup m. 

-intros.elim m.simplify.apply le_n.
-simplify.rewrite > times_n_SO.
+intros.elim m.simplify.unfold lt.apply le_n.
+simplify.unfold lt.rewrite > times_n_SO.

 apply le_times.assumption.assumption.
 qed.
 
 theorem lt_m_exp_nm: \forall n,m:nat. (S O) < n \to m < n \sup m.
 apply le_times.assumption.assumption.
 qed.
 
 theorem lt_m_exp_nm: \forall n,m:nat. (S O) < n \to m < n \sup m.

-intros.elim m.simplify.reflexivity.
-simplify.
+intros.elim m.simplify.unfold lt.reflexivity.
+simplify.unfold lt.

 apply (trans_le ? ((S(S O))*(S n1))).
 simplify.
 rewrite < plus_n_Sm.apply le_S_S.apply le_S_S.
 apply (trans_le ? ((S(S O))*(S n1))).
 simplify.
 rewrite < plus_n_Sm.apply le_S_S.apply le_S_S.


@@ -83,7 +83,7 @@ intros.apply eq_f.
 apply H1.
 (* esprimere inj_times senza S *)
 cut (\forall a,b:nat.O < n \to n*a=n*b \to a=b).
 apply H1.
 (* esprimere inj_times senza S *)
 cut (\forall a,b:nat.O < n \to n*a=n*b \to a=b).

-apply Hcut.simplify. apply le_S_S_to_le. apply le_S. assumption.
+apply Hcut.simplify.unfold lt.apply le_S_S_to_le. apply le_S. assumption.

 assumption.
 intros 2.
 apply (nat_case n).
 assumption.
 intros 2.
 apply (nat_case n).

diff --git a/helm/matita/library/nat/factorial.ma b/helm/matita/library/nat/factorial.ma
index 22a799d07d33dade987df8242d1d7ba338442e54..14217bbcbdee58a7dba618d68642da3eb315d37c 100644 (file)
--- a/helm/matita/library/nat/factorial.ma
+++ b/helm/matita/library/nat/factorial.ma
@@ -52,10 +52,10 @@ intro.apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_O (S(S O)) H).
 intros.change with ((S m) < (S m)*m!).
 apply (lt_to_le_to_lt ? ((S m)*(S (S O)))).
 rewrite < sym_times.
 intros.change with ((S m) < (S m)*m!).
 apply (lt_to_le_to_lt ? ((S m)*(S (S O)))).
 rewrite < sym_times.

-simplify.
+simplify.unfold lt.

 apply le_S_S.rewrite < plus_n_O.
 apply le_plus_n.
 apply le_times_r.apply le_SSO_fact.
 apply le_S_S.rewrite < plus_n_O.
 apply le_plus_n.
 apply le_times_r.apply le_SSO_fact.

-simplify.apply le_S_S_to_le.exact H.
+simplify.unfold lt.apply le_S_S_to_le.exact H.

 qed.
 
 qed.
 

diff --git a/helm/matita/library/nat/factorization.ma b/helm/matita/library/nat/factorization.ma
index b64e3733b5fbe0e5b5de21e15e9ad957e49982f3..6a309430302ee18b576e2def76303d3333a6fdfd 100644 (file)
--- a/helm/matita/library/nat/factorization.ma
+++ b/helm/matita/library/nat/factorization.ma
@@ -40,10 +40,10 @@ rewrite > H1. apply le_smallest_factor_n.
 rewrite > H1.
 change with (divides_b (smallest_factor n) n = true).
 apply divides_to_divides_b_true.
 rewrite > H1.
 change with (divides_b (smallest_factor n) n = true).
 apply divides_to_divides_b_true.

-apply (trans_lt ? (S O)).simplify. apply le_n.
+apply (trans_lt ? (S O)).unfold lt. apply le_n.

 apply lt_SO_smallest_factor.assumption.
 apply divides_smallest_factor_n.
 apply lt_SO_smallest_factor.assumption.
 apply divides_smallest_factor_n.

-apply (trans_lt ? (S O)). simplify. apply le_n. assumption.
+apply (trans_lt ? (S O)). unfold lt. apply le_n. assumption.

 apply prime_to_nth_prime.
 apply prime_smallest_factor_n.assumption.
 qed.
 apply prime_to_nth_prime.
 apply prime_smallest_factor_n.assumption.
 qed.


@@ -167,7 +167,7 @@ match f with
 
 theorem lt_O_defactorize_aux: \forall f:nat_fact.\forall i:nat.
 O < defactorize_aux f i.
 
 theorem lt_O_defactorize_aux: \forall f:nat_fact.\forall i:nat.
 O < defactorize_aux f i.

-intro.elim f.simplify.
+intro.elim f.simplify.unfold lt. 

 rewrite > times_n_SO.
 apply le_times.
 change with (O < nth_prime i).
 rewrite > times_n_SO.
 apply le_times.
 change with (O < nth_prime i).


@@ -175,7 +175,7 @@ apply lt_O_nth_prime_n.
 change with (O < exp (nth_prime i) n).
 apply lt_O_exp.
 apply lt_O_nth_prime_n.
 change with (O < exp (nth_prime i) n).
 apply lt_O_exp.
 apply lt_O_nth_prime_n.

-simplify.
+simplify.unfold lt.

 rewrite > times_n_SO.
 apply le_times.
 change with (O < exp (nth_prime i) n).
 rewrite > times_n_SO.
 apply le_times.
 change with (O < exp (nth_prime i) n).


@@ -187,7 +187,7 @@ qed.
 
 theorem lt_SO_defactorize_aux: \forall f:nat_fact.\forall i:nat.
 S O < defactorize_aux f i.
 
 theorem lt_SO_defactorize_aux: \forall f:nat_fact.\forall i:nat.
 S O < defactorize_aux f i.

-intro.elim f.simplify.
+intro.elim f.simplify.unfold lt.

 rewrite > times_n_SO.
 apply le_times.
 change with (S O < nth_prime i).
 rewrite > times_n_SO.
 apply le_times.
 change with (S O < nth_prime i).


@@ -195,7 +195,7 @@ apply lt_SO_nth_prime_n.
 change with (O < exp (nth_prime i) n).
 apply lt_O_exp.
 apply lt_O_nth_prime_n.
 change with (O < exp (nth_prime i) n).
 apply lt_O_exp.
 apply lt_O_nth_prime_n.

-simplify.
+simplify.unfold lt.

 rewrite > times_n_SO.
 rewrite > sym_times.
 apply le_times.
 rewrite > times_n_SO.
 rewrite > sym_times.
 apply le_times.


@@ -233,7 +233,7 @@ rewrite < Hcut.reflexivity.
 cut (O < r \lor O = r).
 elim Hcut1.assumption.absurd (n1 = O).
 rewrite > Hcut.rewrite < H4.reflexivity.
 cut (O < r \lor O = r).
 elim Hcut1.assumption.absurd (n1 = O).
 rewrite > Hcut.rewrite < H4.reflexivity.

-simplify. intro.apply (not_le_Sn_O O).
+unfold Not. intro.apply (not_le_Sn_O O).

 rewrite < H5 in \vdash (? ? %).assumption.
 apply le_to_or_lt_eq.apply le_O_n.
 cut ((S O) < r \lor (S O) \nlt r).
 rewrite < H5 in \vdash (? ? %).assumption.
 apply le_to_or_lt_eq.apply le_O_n.
 cut ((S O) < r \lor (S O) \nlt r).


@@ -251,11 +251,11 @@ cut (r=(S O)).
 apply (nat_case n).
 left.split.assumption.reflexivity.
 intro.right.rewrite > Hcut2.
 apply (nat_case n).
 left.split.assumption.reflexivity.
 intro.right.rewrite > Hcut2.

-simplify.apply le_S_S.apply le_O_n.
+simplify.unfold lt.apply le_S_S.apply le_O_n.

 cut (r \lt (S O) \or r=(S O)).
 elim Hcut2.absurd (O=r).
 apply le_n_O_to_eq.apply le_S_S_to_le.exact H5.
 cut (r \lt (S O) \or r=(S O)).
 elim Hcut2.absurd (O=r).
 apply le_n_O_to_eq.apply le_S_S_to_le.exact H5.

-simplify.intro.
+unfold Not.intro.

 cut (O=n1).
 apply (not_le_Sn_O O).
 rewrite > Hcut3 in \vdash (? ? %).
 cut (O=n1).
 apply (not_le_Sn_O O).
 rewrite > Hcut3 in \vdash (? ? %).


@@ -309,14 +309,14 @@ cut (O < q \lor O = q).
 elim Hcut2.assumption.
 absurd (nth_prime p \divides S (S m1)).
 apply (divides_max_prime_factor_n (S (S m1))).
 elim Hcut2.assumption.
 absurd (nth_prime p \divides S (S m1)).
 apply (divides_max_prime_factor_n (S (S m1))).

-simplify.apply le_S_S.apply le_S_S. apply le_O_n.
+unfold lt.apply le_S_S.apply le_S_S. apply le_O_n.

 cut ((S(S m1)) = r).
 rewrite > Hcut3 in \vdash (? (? ? %)).
 change with (nth_prime p \divides r \to False).
 intro.
 apply (p_ord_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r).
 apply lt_SO_nth_prime_n.
 cut ((S(S m1)) = r).
 rewrite > Hcut3 in \vdash (? (? ? %)).
 change with (nth_prime p \divides r \to False).
 intro.
 apply (p_ord_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r).
 apply lt_SO_nth_prime_n.

-simplify.apply le_S_S.apply le_O_n.apply le_n.
+unfold lt.apply le_S_S.apply le_O_n.apply le_n.

 assumption.
 apply divides_to_mod_O.apply lt_O_nth_prime_n.assumption.
 rewrite > times_n_SO in \vdash (? ? ? %).
 assumption.
 apply divides_to_mod_O.apply lt_O_nth_prime_n.assumption.
 rewrite > times_n_SO in \vdash (? ? ? %).


@@ -330,18 +330,18 @@ cut ((S O) < r \lor S O \nlt r).
 elim Hcut2.
 right. 
 apply (p_ord_to_lt_max_prime_factor1 (S(S m1)) ? q r).
 elim Hcut2.
 right. 
 apply (p_ord_to_lt_max_prime_factor1 (S(S m1)) ? q r).

-simplify.apply le_S_S. apply le_O_n.
+unfold lt.apply le_S_S. apply le_O_n.

 apply le_n.
 assumption.assumption.
 cut (r=(S O)).
 apply (nat_case p).
 left.split.assumption.reflexivity.
 intro.right.rewrite > Hcut3.
 apply le_n.
 assumption.assumption.
 cut (r=(S O)).
 apply (nat_case p).
 left.split.assumption.reflexivity.
 intro.right.rewrite > Hcut3.

-simplify.apply le_S_S.apply le_O_n.
+simplify.unfold lt.apply le_S_S.apply le_O_n.

 cut (r \lt (S O) \or r=(S O)).
 elim Hcut3.absurd (O=r).
 apply le_n_O_to_eq.apply le_S_S_to_le.exact H2.
 cut (r \lt (S O) \or r=(S O)).
 elim Hcut3.absurd (O=r).
 apply le_n_O_to_eq.apply le_S_S_to_le.exact H2.

-simplify.intro.
+unfold Not.intro.

 apply (not_le_Sn_O O).
 rewrite > H3 in \vdash (? ? %).assumption.assumption.
 apply (le_to_or_lt_eq r (S O)).
 apply (not_le_Sn_O O).
 rewrite > H3 in \vdash (? ? %).assumption.assumption.
 apply (le_to_or_lt_eq r (S O)).


@@ -406,11 +406,11 @@ theorem divides_exp_to_eq:
 \forall p,q,m:nat. prime p \to prime q \to
 p \divides q \sup m \to p = q.
 intros.
 \forall p,q,m:nat. prime p \to prime q \to
 p \divides q \sup m \to p = q.
 intros.

-simplify in H1.
+unfold prime in H1.

 elim H1.apply H4.
 apply (divides_exp_to_divides p q m).
 assumption.assumption.
 elim H1.apply H4.
 apply (divides_exp_to_divides p q m).
 assumption.assumption.

-simplify in H.elim H.assumption.
+unfold prime in H.elim H.assumption.

 qed.
 
 theorem  not_divides_defactorize_aux: \forall f:nat_fact. \forall i,j:nat.
 qed.
 
 theorem  not_divides_defactorize_aux: \forall f:nat_fact. \forall i,j:nat.


@@ -442,7 +442,7 @@ cut (i = j).
 apply (not_le_Sn_n i).rewrite > Hcut1 in \vdash (? ? %).assumption.
 apply (injective_nth_prime ? ? H4).
 apply (H i (S j)).
 apply (not_le_Sn_n i).rewrite > Hcut1 in \vdash (? ? %).assumption.
 apply (injective_nth_prime ? ? H4).
 apply (H i (S j)).

-apply (trans_lt ? j).assumption.simplify.apply le_n.
+apply (trans_lt ? j).assumption.unfold lt.apply le_n.

 assumption.
 apply divides_times_to_divides.
 apply prime_nth_prime.assumption.
 assumption.
 apply divides_times_to_divides.
 apply prime_nth_prime.assumption.


@@ -473,10 +473,10 @@ qed.
 lemma not_eq_nf_cons_O_nf_cons: \forall f,g:nat_fact.\forall n,i:nat.
 \lnot (defactorize_aux (nf_cons O f) i= defactorize_aux (nf_cons (S n) g) i).
 intros.
 lemma not_eq_nf_cons_O_nf_cons: \forall f,g:nat_fact.\forall n,i:nat.
 \lnot (defactorize_aux (nf_cons O f) i= defactorize_aux (nf_cons (S n) g) i).
 intros.

-simplify.rewrite < plus_n_O.
+simplify.unfold Not.rewrite < plus_n_O.

 intro.
 apply (not_divides_defactorize_aux f i (S i) ?).
 intro.
 apply (not_divides_defactorize_aux f i (S i) ?).

-simplify.apply le_n.
+unfold lt.apply le_n.

 rewrite > H.
 rewrite > assoc_times.
 apply (witness ? ? ((exp (nth_prime i) n)*(defactorize_aux g (S i)))).
 rewrite > H.
 rewrite > assoc_times.
 apply (witness ? ? ((exp (nth_prime i) n)*(defactorize_aux g (S i)))).

diff --git a/helm/matita/library/nat/fermat_little_theorem.ma b/helm/matita/library/nat/fermat_little_theorem.ma
index bbd5e359a352066736b0c5003e80daa86b22bb14..cc18a8bb9e4249005d96e772d7e41f4d01409720 100644 (file)
--- a/helm/matita/library/nat/fermat_little_theorem.ma
+++ b/helm/matita/library/nat/fermat_little_theorem.ma
@@ -25,7 +25,7 @@ unfold S_mod.
 apply le_S_S_to_le.
 change with ((S i) \mod (S n) < S n).
 apply lt_mod_m_m.
 apply le_S_S_to_le.
 change with ((S i) \mod (S n) < S n).
 apply lt_mod_m_m.

-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.

 unfold injn.intros.
 apply inj_S.
 rewrite < (lt_to_eq_mod i (S n)).
 unfold injn.intros.
 apply inj_S.
 rewrite < (lt_to_eq_mod i (S n)).


@@ -37,14 +37,14 @@ elim Hcut1.
 (* i < n, j< n *)
 rewrite < mod_S.
 rewrite < mod_S.
 (* i < n, j< n *)
 rewrite < mod_S.
 rewrite < mod_S.

-apply H2.simplify.apply le_S_S.apply le_O_n.
+apply H2.unfold lt.apply le_S_S.apply le_O_n.

 rewrite > lt_to_eq_mod.
 rewrite > lt_to_eq_mod.

-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.apply le_O_n.

 rewrite > lt_to_eq_mod.
 rewrite > lt_to_eq_mod.

-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.

 (* i < n, j=n *)
 unfold S_mod in H2.
 simplify.
 (* i < n, j=n *)
 unfold S_mod in H2.
 simplify.


@@ -54,11 +54,11 @@ apply sym_eq.
 rewrite < (mod_n_n (S n)).
 rewrite < H4 in \vdash (? ? ? (? %?)).
 rewrite < mod_S.assumption.
 rewrite < (mod_n_n (S n)).
 rewrite < H4 in \vdash (? ? ? (? %?)).
 rewrite < mod_S.assumption.

-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.

 rewrite > lt_to_eq_mod.
 rewrite > lt_to_eq_mod.

-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.apply le_O_n.

 (* i = n, j < n *)
 elim Hcut1.
 apply False_ind.
 (* i = n, j < n *)
 elim Hcut1.
 apply False_ind.


@@ -66,19 +66,19 @@ apply (not_eq_O_S (j \mod (S n))).
 rewrite < (mod_n_n (S n)).
 rewrite < H3 in \vdash (? ? (? %?) ?).
 rewrite < mod_S.assumption.
 rewrite < (mod_n_n (S n)).
 rewrite < H3 in \vdash (? ? (? %?) ?).
 rewrite < mod_S.assumption.

-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.

 rewrite > lt_to_eq_mod.
 rewrite > lt_to_eq_mod.

-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.apply le_O_n.

 (* i = n, j= n*)
 rewrite > H3.
 rewrite > H4.
 reflexivity.
 apply le_to_or_lt_eq.assumption.
 apply le_to_or_lt_eq.assumption.
 (* i = n, j= n*)
 rewrite > H3.
 rewrite > H4.
 reflexivity.
 apply le_to_or_lt_eq.assumption.
 apply le_to_or_lt_eq.assumption.

-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.

 qed.
 
 (*
 qed.
 
 (*


@@ -95,19 +95,19 @@ qed.
 
 theorem prime_to_not_divides_fact: \forall p:nat. prime p \to \forall n:nat.
 n \lt p \to \not divides p n!.
 
 theorem prime_to_not_divides_fact: \forall p:nat. prime p \to \forall n:nat.
 n \lt p \to \not divides p n!.

-intros 3.elim n.simplify.intros.
+intros 3.elim n.unfold Not.intros.

 apply (lt_to_not_le (S O) p).
 unfold prime in H.elim H.
 apply (lt_to_not_le (S O) p).
 unfold prime in H.elim H.

-assumption.apply divides_to_le.simplify.apply le_n.
+assumption.apply divides_to_le.unfold lt.apply le_n.

 assumption.
 change with (divides p ((S n1)*n1!) \to False).
 intro.
 cut (divides p (S n1) \lor divides p n1!).
 elim Hcut.apply (lt_to_not_le (S n1) p).
 assumption.
 assumption.
 change with (divides p ((S n1)*n1!) \to False).
 intro.
 cut (divides p (S n1) \lor divides p n1!).
 elim Hcut.apply (lt_to_not_le (S n1) p).
 assumption.

-apply divides_to_le.simplify.apply le_S_S.apply le_O_n.
+apply divides_to_le.unfold lt.apply le_S_S.apply le_O_n.

 assumption.apply H1.
 assumption.apply H1.

-apply (trans_lt ? (S n1)).simplify. apply le_n.
+apply (trans_lt ? (S n1)).unfold lt. apply le_n.

 assumption.assumption.
 apply divides_times_to_divides.
 assumption.assumption.
 assumption.assumption.
 apply divides_times_to_divides.
 assumption.assumption.


@@ -120,19 +120,19 @@ split.intros.apply le_S_S_to_le.
 apply (trans_le ? p).
 change with (mod (a*i) p < p).
 apply lt_mod_m_m.
 apply (trans_le ? p).
 change with (mod (a*i) p < p).
 apply lt_mod_m_m.

-simplify in H.elim H.
-simplify.apply (trans_le ? (S (S O))).
+unfold prime in H.elim H.
+unfold lt.apply (trans_le ? (S (S O))).

 apply le_n_Sn.assumption.
 rewrite < S_pred.apply le_n.
 unfold prime in H.
 elim H.
 apply le_n_Sn.assumption.
 rewrite < S_pred.apply le_n.
 unfold prime in H.
 elim H.

-apply (trans_lt ? (S O)).simplify.apply le_n.assumption.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption.

 unfold injn.intros.
 apply (nat_compare_elim i j).
 (* i < j *)
 intro.
 absurd (j-i \lt p).
 unfold injn.intros.
 apply (nat_compare_elim i j).
 (* i < j *)
 intro.
 absurd (j-i \lt p).

-simplify.
+unfold lt.

 rewrite > (S_pred p).
 apply le_S_S.
 apply le_plus_to_minus.
 rewrite > (S_pred p).
 apply le_S_S.
 apply le_plus_to_minus.


@@ -141,9 +141,9 @@ rewrite > sym_plus.
 apply le_plus_n.
 unfold prime in H.
 elim H.
 apply le_plus_n.
 unfold prime in H.
 elim H.

-apply (trans_lt ? (S O)).simplify.apply le_n.assumption.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption.

 apply (le_to_not_lt p (j-i)).
 apply (le_to_not_lt p (j-i)).

-apply divides_to_le.simplify.
+apply divides_to_le.unfold lt.

 apply le_SO_minus.assumption.
 cut (divides p a \lor divides p (j-i)).
 elim Hcut.apply False_ind.apply H1.assumption.assumption.
 apply le_SO_minus.assumption.
 cut (divides p a \lor divides p (j-i)).
 elim Hcut.apply False_ind.apply H1.assumption.assumption.


@@ -152,7 +152,7 @@ rewrite > distr_times_minus.
 apply eq_mod_to_divides.
 unfold prime in H.
 elim H.
 apply eq_mod_to_divides.
 unfold prime in H.
 elim H.

-apply (trans_lt ? (S O)).simplify.apply le_n.assumption.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption.

 apply sym_eq.
 apply H4.
 (* i = j *)
 apply sym_eq.
 apply H4.
 (* i = j *)


@@ -160,7 +160,7 @@ intro. assumption.
 (* j < i *)
 intro.
 absurd (i-j \lt p).
 (* j < i *)
 intro.
 absurd (i-j \lt p).

-simplify.
+unfold lt.

 rewrite > (S_pred p).
 apply le_S_S.
 apply le_plus_to_minus.
 rewrite > (S_pred p).
 apply le_S_S.
 apply le_plus_to_minus.


@@ -169,9 +169,9 @@ rewrite > sym_plus.
 apply le_plus_n.
 unfold prime in H.
 elim H.
 apply le_plus_n.
 unfold prime in H.
 elim H.

-apply (trans_lt ? (S O)).simplify.apply le_n.assumption.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption.

 apply (le_to_not_lt p (i-j)).
 apply (le_to_not_lt p (i-j)).

-apply divides_to_le.simplify.
+apply divides_to_le.unfold lt.

 apply le_SO_minus.assumption.
 cut (divides p a \lor divides p (i-j)).
 elim Hcut.apply False_ind.apply H1.assumption.assumption.
 apply le_SO_minus.assumption.
 cut (divides p a \lor divides p (i-j)).
 elim Hcut.apply False_ind.apply H1.assumption.assumption.


@@ -180,7 +180,7 @@ rewrite > distr_times_minus.
 apply eq_mod_to_divides.
 unfold prime in H.
 elim H.
 apply eq_mod_to_divides.
 unfold prime in H.
 elim H.

-apply (trans_lt ? (S O)).simplify.apply le_n.assumption.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption.

 apply H4.
 qed.
 
 apply H4.
 qed.
 


@@ -238,7 +238,7 @@ change with ((S O) \le pred p).
 apply le_S_S_to_le.rewrite < S_pred.
 unfold prime in H.elim H.assumption.assumption.
 unfold prime in H.elim H.apply (trans_lt ? (S O)).
 apply le_S_S_to_le.rewrite < S_pred.
 unfold prime in H.elim H.assumption.assumption.
 unfold prime in H.elim H.apply (trans_lt ? (S O)).

-simplify.apply le_n.assumption.
+unfold lt.apply le_n.assumption.

 cut (O < a \lor O = a).
 elim Hcut.assumption.
 apply False_ind.apply H1.
 cut (O < a \lor O = a).
 elim Hcut.assumption.
 apply False_ind.apply H1.

diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma
index d42a57e8e8db6c1661d480d829bcf1d6289c96de..65f61b581691cdabbdaeeb34fc7d10ac21927a93 100644 (file)
--- a/helm/matita/library/nat/gcd.ma
+++ b/helm/matita/library/nat/gcd.ma
@@ -136,7 +136,7 @@ intros.change with
 \land 
 gcd_aux (S m1) m (S m1) \divides (S m1)).
 apply divides_gcd_aux_mn.
 \land 
 gcd_aux (S m1) m (S m1) \divides (S m1)).
 apply divides_gcd_aux_mn.

-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.

 assumption.apply le_n.
 simplify.intro.
 apply (nat_case1 m).
 assumption.apply le_n.
 simplify.intro.
 apply (nat_case1 m).


@@ -152,8 +152,8 @@ cut (gcd_aux (S m1) n (S m1) \divides n
 gcd_aux (S m1) n (S m1) \divides S m1).
 elim Hcut.split.assumption.assumption.
 apply divides_gcd_aux_mn.
 gcd_aux (S m1) n (S m1) \divides S m1).
 elim Hcut.split.assumption.assumption.
 apply divides_gcd_aux_mn.

-simplify.apply le_S_S.apply le_O_n.
-apply not_lt_to_le.simplify.intro.apply H.
+unfold lt.apply le_S_S.apply le_O_n.
+apply not_lt_to_le.unfold Not. unfold lt.intro.apply H.

 rewrite > H1.apply (trans_le ? (S n)).
 apply le_n_Sn.assumption.apply le_n.
 qed.
 rewrite > H1.apply (trans_le ? (S n)).
 apply le_n_Sn.assumption.apply le_n.
 qed.


@@ -221,13 +221,13 @@ apply (nat_case1 n).simplify.intros.assumption.
 intros.
 change with (d \divides gcd_aux (S m1) m (S m1)).
 apply divides_gcd_aux.
 intros.
 change with (d \divides gcd_aux (S m1) m (S m1)).
 apply divides_gcd_aux.

-simplify.apply le_S_S.apply le_O_n.assumption.apply le_n.assumption.
+unfold lt.apply le_S_S.apply le_O_n.assumption.apply le_n.assumption.

 rewrite < H2.assumption.
 apply (nat_case1 m).simplify.intros.assumption.
 intros.
 change with (d \divides gcd_aux (S m1) n (S m1)).
 apply divides_gcd_aux.
 rewrite < H2.assumption.
 apply (nat_case1 m).simplify.intros.assumption.
 intros.
 change with (d \divides gcd_aux (S m1) n (S m1)).
 apply divides_gcd_aux.

-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.

 apply lt_to_le.apply not_le_to_lt.assumption.apply le_n.assumption.
 rewrite < H2.assumption.
 qed.
 apply lt_to_le.apply not_le_to_lt.assumption.apply le_n.assumption.
 rewrite < H2.assumption.
 qed.


@@ -343,7 +343,7 @@ change with
 a*(S m1) - b*m = (gcd_aux (S m1) m (S m1)) 
 \lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1))).
 apply eq_minus_gcd_aux.
 a*(S m1) - b*m = (gcd_aux (S m1) m (S m1)) 
 \lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1))).
 apply eq_minus_gcd_aux.

-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.

 assumption.apply le_n.
 apply (nat_case1 m).
 simplify.intros.
 assumption.apply le_n.
 apply (nat_case1 m).
 simplify.intros.


@@ -370,7 +370,7 @@ apply (ex_intro ? ? a1).
 apply (ex_intro ? ? a).
 left.assumption.
 apply eq_minus_gcd_aux.
 apply (ex_intro ? ? a).
 left.assumption.
 apply eq_minus_gcd_aux.

-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.

 apply lt_to_le.apply not_le_to_lt.assumption.
 apply le_n.
 qed.
 apply lt_to_le.apply not_le_to_lt.assumption.
 apply le_n.
 qed.


@@ -397,7 +397,7 @@ intros.
 generalize in match (gcd_O_to_eq_O m n H1).
 intros.elim H2.
 rewrite < H4 in \vdash (? ? %).assumption.
 generalize in match (gcd_O_to_eq_O m n H1).
 intros.elim H2.
 rewrite < H4 in \vdash (? ? %).assumption.

-intros.simplify.apply le_S_S.apply le_O_n.
+intros.unfold lt.apply le_S_S.apply le_O_n.

 qed.
 
 theorem symmetric_gcd: symmetric nat gcd.
 qed.
 
 theorem symmetric_gcd: symmetric nat gcd.


@@ -435,7 +435,7 @@ intro.
 apply divides_to_le.
 apply lt_O_gcd.
 rewrite > (times_n_O O).
 apply divides_to_le.
 apply lt_O_gcd.
 rewrite > (times_n_O O).

-apply lt_times.simplify.apply le_S_S.apply le_O_n.assumption.
+apply lt_times.unfold lt.apply le_S_S.apply le_O_n.assumption.

 apply divides_d_gcd.
 apply (transitive_divides ? (S m1)).
 apply divides_gcd_m.
 apply divides_d_gcd.
 apply (transitive_divides ? (S m1)).
 apply divides_gcd_m.


@@ -457,7 +457,7 @@ qed.
 
 theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
 intro.
 
 theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
 intro.

-apply antisym_le.apply divides_to_le.simplify.apply le_n.
+apply antisym_le.apply divides_to_le.unfold lt.apply le_n.

 apply divides_gcd_n.
 cut (O < gcd (S O) n \lor O = gcd (S O) n).
 elim Hcut.assumption.
 apply divides_gcd_n.
 cut (O < gcd (S O) n \lor O = gcd (S O) n).
 elim Hcut.assumption.


@@ -502,7 +502,7 @@ qed.
 
 theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to n \ndivides m \to
 gcd n m = (S O).
 
 theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to n \ndivides m \to
 gcd n m = (S O).

-intros.simplify in H.change with (gcd n m = (S O)). 
+intros.unfold prime in H.change with (gcd n m = (S O)). 

 elim H.
 apply antisym_le.
 apply not_lt_to_le.
 elim H.
 apply antisym_le.
 apply not_lt_to_le.


@@ -557,8 +557,8 @@ rewrite < (prime_to_gcd_SO n p).
 apply eq_minus_gcd.
 assumption.assumption.
 apply (decidable_divides n p).
 apply eq_minus_gcd.
 assumption.assumption.
 apply (decidable_divides n p).

-apply (trans_lt ? (S O)).simplify.apply le_n.
-simplify in H.elim H. assumption.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.
+unfold prime in H.elim H. assumption.

 qed.
 
 theorem eq_gcd_times_SO: \forall m,n,p:nat. O < n \to O < p \to
 qed.
 
 theorem eq_gcd_times_SO: \forall m,n,p:nat. O < n \to O < p \to


@@ -576,11 +576,11 @@ rewrite < H2 in \vdash (? ? %).
 apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))).
 apply lt_SO_smallest_factor.assumption.
 apply divides_to_le.
 apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))).
 apply lt_SO_smallest_factor.assumption.
 apply divides_to_le.

-rewrite > H2.simplify.apply le_n.
+rewrite > H2.unfold lt.apply le_n.

 apply divides_d_gcd.assumption.
 apply (transitive_divides ? (gcd m (n*p))).
 apply divides_smallest_factor_n.
 apply divides_d_gcd.assumption.
 apply (transitive_divides ? (gcd m (n*p))).
 apply divides_smallest_factor_n.

-apply (trans_lt ? (S O)). simplify. apply le_n. assumption.
+apply (trans_lt ? (S O)). unfold lt. apply le_n. assumption.

 apply divides_gcd_n.
 apply (not_le_Sn_n (S O)).
 change with ((S O) < (S O)).
 apply divides_gcd_n.
 apply (not_le_Sn_n (S O)).
 change with ((S O) < (S O)).


@@ -588,18 +588,18 @@ rewrite < H3 in \vdash (? ? %).
 apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))).
 apply lt_SO_smallest_factor.assumption.
 apply divides_to_le.
 apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))).
 apply lt_SO_smallest_factor.assumption.
 apply divides_to_le.

-rewrite > H3.simplify.apply le_n.
+rewrite > H3.unfold lt.apply le_n.

 apply divides_d_gcd.assumption.
 apply (transitive_divides ? (gcd m (n*p))).
 apply divides_smallest_factor_n.
 apply divides_d_gcd.assumption.
 apply (transitive_divides ? (gcd m (n*p))).
 apply divides_smallest_factor_n.

-apply (trans_lt ? (S O)). simplify. apply le_n. assumption.
+apply (trans_lt ? (S O)). unfold lt. apply le_n. assumption.

 apply divides_gcd_n.
 apply divides_times_to_divides.
 apply prime_smallest_factor_n.
 assumption.
 apply (transitive_divides ? (gcd m (n*p))).
 apply divides_smallest_factor_n.
 apply divides_gcd_n.
 apply divides_times_to_divides.
 apply prime_smallest_factor_n.
 assumption.
 apply (transitive_divides ? (gcd m (n*p))).
 apply divides_smallest_factor_n.

-apply (trans_lt ? (S O)). simplify. apply le_n. assumption.
+apply (trans_lt ? (S O)).unfold lt. apply le_n. assumption.

 apply divides_gcd_m.
 change with (O < gcd m (n*p)).
 apply lt_O_gcd.
 apply divides_gcd_m.
 change with (O < gcd m (n*p)).
 apply lt_O_gcd.

diff --git a/helm/matita/library/nat/lt_arith.ma b/helm/matita/library/nat/lt_arith.ma
index 4897fb59875a8d8968e122f44ca66b59e9994870..b8339f374e6019dd054719c9928bf735c63aef4b 100644 (file)
--- a/helm/matita/library/nat/lt_arith.ma
+++ b/helm/matita/library/nat/lt_arith.ma
@@ -21,7 +21,7 @@ theorem monotonic_lt_plus_r:
 \forall n:nat.monotonic nat lt (\lambda m.n+m).
 simplify.intros.
 elim n.simplify.assumption.
 \forall n:nat.monotonic nat lt (\lambda m.n+m).
 simplify.intros.
 elim n.simplify.assumption.

-simplify.
+simplify.unfold lt.

 apply le_S_S.assumption.
 qed.
 
 apply le_S_S.assumption.
 qed.
 


@@ -51,7 +51,7 @@ intro.elim n.
 rewrite > plus_n_O.
 rewrite > (plus_n_O q).assumption.
 apply H.
 rewrite > plus_n_O.
 rewrite > (plus_n_O q).assumption.
 apply H.

-simplify.apply le_S_S_to_le.
+unfold lt.apply le_S_S_to_le.

 rewrite > plus_n_Sm.
 rewrite > (plus_n_Sm q).
 exact H1.
 rewrite > plus_n_Sm.
 rewrite > (plus_n_Sm q).
 exact H1.


@@ -65,7 +65,7 @@ qed.
 
 (* times and zero *)
 theorem lt_O_times_S_S: \forall n,m:nat.O < (S n)*(S m).
 
 (* times and zero *)
 theorem lt_O_times_S_S: \forall n,m:nat.O < (S n)*(S m).

-intros.simplify.apply le_S_S.apply le_O_n.
+intros.simplify.unfold lt.apply le_S_S.apply le_O_n.

 qed.
 
 (* times *)
 qed.
 
 (* times *)


@@ -172,7 +172,7 @@ rewrite < sym_times.
 rewrite < div_mod.
 rewrite > H2.
 assumption.
 rewrite < div_mod.
 rewrite > H2.
 assumption.

-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.

 qed.
 
 theorem lt_div_n_m_n: \forall n,m:nat. (S O) < m \to O < n \to n / m \lt n.
 qed.
 
 theorem lt_div_n_m_n: \forall n,m:nat. (S O) < m \to O < n \to n / m \lt n.


@@ -184,7 +184,7 @@ apply (lt_to_le_to_lt ? ((n / m)*m)).
 apply (lt_to_le_to_lt ? ((n / m)*(S (S O)))).
 rewrite < sym_times.
 rewrite > H2.
 apply (lt_to_le_to_lt ? ((n / m)*(S (S O)))).
 rewrite < sym_times.
 rewrite > H2.

-simplify.
+simplify.unfold lt.

 rewrite < plus_n_O.
 rewrite < plus_n_Sm.
 apply le_S_S.
 rewrite < plus_n_O.
 rewrite < plus_n_Sm.
 apply le_S_S.


@@ -195,13 +195,13 @@ assumption.
 rewrite < sym_plus.
 apply le_plus_n.
 apply (trans_lt ? (S O)).
 rewrite < sym_plus.
 apply le_plus_n.
 apply (trans_lt ? (S O)).

-simplify. apply le_n.assumption.
+unfold lt. apply le_n.assumption.

 qed.
 
 (* general properties of functions *)
 theorem monotonic_to_injective: \forall f:nat\to nat.
 monotonic nat lt f \to injective nat nat f.
 qed.
 
 (* general properties of functions *)
 theorem monotonic_to_injective: \forall f:nat\to nat.
 monotonic nat lt f \to injective nat nat f.

-simplify.intros.
+unfold injective.intros.

 apply (nat_compare_elim x y).
 intro.apply False_ind.apply (not_le_Sn_n (f x)).
 rewrite > H1 in \vdash (? ? %).apply H.apply H2.
 apply (nat_compare_elim x y).
 intro.apply False_ind.apply (not_le_Sn_n (f x)).
 rewrite > H1 in \vdash (? ? %).apply H.apply H2.

diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma
index 00a90acd83192ee2d79d6b8b59c7a1e37d2e21ff..710418d72644022cb4d799fb95f67354da4af89b 100644 (file)
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -170,7 +170,7 @@ qed.
 theorem lt_minus_m: \forall n,m:nat. O < n \to O < m \to n-m \lt n.
 intros.apply (lt_O_n_elim n H).intro.
 apply (lt_O_n_elim m H1).intro.
 theorem lt_minus_m: \forall n,m:nat. O < n \to O < m \to n-m \lt n.
 intros.apply (lt_O_n_elim n H).intro.
 apply (lt_O_n_elim m H1).intro.

-simplify.apply le_S_S.apply le_minus_m.
+simplify.unfold lt.apply le_S_S.apply le_minus_m.

 qed.
 
 theorem minus_le_O_to_le: \forall n,m:nat. n-m \leq O \to n \leq m.
 qed.
 
 theorem minus_le_O_to_le: \forall n,m:nat. n-m \leq O \to n \leq m.


@@ -230,14 +230,14 @@ theorem lt_minus_to_plus: \forall n,m,p. (lt n (p-m)) \to (lt (n+m) p).
 intros 3.apply (nat_elim2 (\lambda m,p.(lt n (p-m)) \to (lt (n+m) p))).
 intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption.
 simplify.intros.apply False_ind.apply (not_le_Sn_O n H).
 intros 3.apply (nat_elim2 (\lambda m,p.(lt n (p-m)) \to (lt (n+m) p))).
 intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption.
 simplify.intros.apply False_ind.apply (not_le_Sn_O n H).

-simplify.intros.
+simplify.intros.unfold lt.

 apply le_S_S.
 rewrite < plus_n_Sm.
 apply H.apply H1.
 qed.
 
 theorem distributive_times_minus: distributive nat times minus.
 apply le_S_S.
 rewrite < plus_n_Sm.
 apply H.apply H1.
 qed.
 
 theorem distributive_times_minus: distributive nat times minus.

-simplify.
+unfold distributive.

 intros.
 apply ((leb_elim z y)).
   intro.cut (x*(y-z)+x*z = (x*y-x*z)+x*z).
 intros.
 apply ((leb_elim z y)).
   intro.cut (x*(y-z)+x*z = (x*y-x*z)+x*z).

diff --git a/helm/matita/library/nat/nat.ma b/helm/matita/library/nat/nat.ma
index fb7d1686efa6631d75e131aae4700384ff017843..a75032d7123b7018f40af65285712d5c3c4da9c1 100644 (file)
--- a/helm/matita/library/nat/nat.ma
+++ b/helm/matita/library/nat/nat.ma
@@ -30,7 +30,7 @@ intros. reflexivity.
 qed.
 
 theorem injective_S : injective nat nat S.
 qed.
 
 theorem injective_S : injective nat nat S.

-simplify.
+unfold injective.

 intros.
 rewrite > pred_Sn.
 rewrite > (pred_Sn y).
 intros.
 rewrite > pred_Sn.
 rewrite > (pred_Sn y).


@@ -42,7 +42,7 @@ theorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m
 
 theorem not_eq_S  : \forall n,m:nat. 
 \lnot n=m \to S n \neq S m.
 
 theorem not_eq_S  : \forall n,m:nat. 
 \lnot n=m \to S n \neq S m.

-intros. simplify. intros.
+intros. unfold Not. intros.

 apply H. apply injective_S. assumption.
 qed.
 
 apply H. apply injective_S. assumption.
 qed.
 


@@ -53,7 +53,7 @@ definition not_zero : nat \to Prop \def
   | (S p) \Rightarrow True ].
 
 theorem not_eq_O_S : \forall n:nat. O \neq S n.
   | (S p) \Rightarrow True ].
 
 theorem not_eq_O_S : \forall n:nat. O \neq S n.

-intros. simplify. intros.
+intros. unfold Not. intros.

 cut (not_zero O).
 exact Hcut.
 rewrite > H.exact I.
 cut (not_zero O).
 exact Hcut.
 rewrite > H.exact I.


@@ -91,7 +91,7 @@ intros.apply H2. apply H3.
 qed.
 
 theorem decidable_eq_nat : \forall n,m:nat.decidable (n=m).
 qed.
 
 theorem decidable_eq_nat : \forall n,m:nat.decidable (n=m).

-intros.simplify.
+intros.unfold decidable.

 apply (nat_elim2 (\lambda n,m.(Or (n=m) ((n=m) \to False)))).
 intro.elim n1.
 left.reflexivity.
 apply (nat_elim2 (\lambda n,m.(Or (n=m) ((n=m) \to False)))).
 intro.elim n1.
 left.reflexivity.

diff --git a/helm/matita/library/nat/nth_prime.ma b/helm/matita/library/nat/nth_prime.ma
index 5fa636301425eb1354b40403b374c54e860134f1..5330f52adbb923ddd84fc91ac1a876b373751ccc 100644 (file)
--- a/helm/matita/library/nat/nth_prime.ma
+++ b/helm/matita/library/nat/nth_prime.ma
@@ -45,10 +45,10 @@ apply not_le_to_lt.
 change with (smallest_factor (S n!) \le n \to False).intro.
 apply (not_divides_S_fact n (smallest_factor(S n!))).
 apply lt_SO_smallest_factor.
 change with (smallest_factor (S n!) \le n \to False).intro.
 apply (not_divides_S_fact n (smallest_factor(S n!))).
 apply lt_SO_smallest_factor.

-simplify.apply le_S_S.apply le_SO_fact.
+unfold lt.apply le_S_S.apply le_SO_fact.

 assumption.
 apply divides_smallest_factor_n.
 assumption.
 apply divides_smallest_factor_n.

-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.

 qed.
 
 theorem ex_prime: \forall n. (S O) \le n \to \exists m.
 qed.
 
 theorem ex_prime: \forall n. (S O) \le n \to \exists m.


@@ -66,7 +66,7 @@ apply le_smallest_factor_n.
 apply prime_smallest_factor_n.
 change with ((S(S O)) \le S (S n1)!).
 apply le_S.apply le_SSO_fact.
 apply prime_smallest_factor_n.
 change with ((S(S O)) \le S (S n1)!).
 apply le_S.apply le_SSO_fact.

-simplify.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.

 qed.
 
 let rec nth_prime n \def
 qed.
 
 let rec nth_prime n \def


@@ -147,14 +147,14 @@ apply increasing_nth_prime.
 qed.
 
 theorem lt_SO_nth_prime_n : \forall n:nat. (S O) \lt nth_prime n.
 qed.
 
 theorem lt_SO_nth_prime_n : \forall n:nat. (S O) \lt nth_prime n.

-intros. elim n.simplify.apply le_n.
+intros. elim n.unfold lt.apply le_n.

 apply (trans_lt ? (nth_prime n1)).
 assumption.apply lt_nth_prime_n_nth_prime_Sn.
 qed.
 
 theorem lt_O_nth_prime_n : \forall n:nat. O \lt nth_prime n.
 intros.apply (trans_lt O (S O)).
 apply (trans_lt ? (nth_prime n1)).
 assumption.apply lt_nth_prime_n_nth_prime_Sn.
 qed.
 
 theorem lt_O_nth_prime_n : \forall n:nat. O \lt nth_prime n.
 intros.apply (trans_lt O (S O)).

-simplify. apply le_n.apply lt_SO_nth_prime_n.
+unfold lt. apply le_n.apply lt_SO_nth_prime_n.

 qed.
 
 theorem ex_m_le_n_nth_prime_m: 
 qed.
 
 theorem ex_m_le_n_nth_prime_m: 


@@ -195,6 +195,6 @@ apply (lt_nth_prime_to_not_prime a).assumption.assumption.
 apply (ex_intro nat ? a).assumption.
 apply le_to_or_lt_eq.assumption.
 apply ex_m_le_n_nth_prime_m.
 apply (ex_intro nat ? a).assumption.
 apply le_to_or_lt_eq.assumption.
 apply ex_m_le_n_nth_prime_m.

-simplify.simplify in H.elim H.assumption.
+simplify.unfold prime in H.elim H.assumption.

 qed.
 
 qed.
 

diff --git a/helm/matita/library/nat/ord.ma b/helm/matita/library/nat/ord.ma
index b982accb37727b46841bbc7a8fc3e8a11dd31865..24874c08af2fd10d2e3286f01e388940f3390d51 100644 (file)
--- a/helm/matita/library/nat/ord.ma
+++ b/helm/matita/library/nat/ord.ma
@@ -167,7 +167,7 @@ generalize in match (H (n1 / m) m).
 elim (p_ord_aux n (n1 / m) m).
 apply H5.assumption.
 apply eq_mod_O_to_lt_O_div.
 elim (p_ord_aux n (n1 / m) m).
 apply H5.assumption.
 apply eq_mod_O_to_lt_O_div.

-apply (trans_lt ? (S O)).simplify.apply le_n.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.

 assumption.assumption.assumption.
 apply le_S_S_to_le.
 apply (trans_le ? n1).change with (n1 / m < n1).
 assumption.assumption.assumption.
 apply le_S_S_to_le.
 apply (trans_le ? n1).change with (n1 / m < n1).


@@ -175,9 +175,7 @@ apply lt_div_n_m_n.assumption.assumption.assumption.
 intros.
 change with (n1 \mod m \neq O).
 rewrite > H4.
 intros.
 change with (n1 \mod m \neq O).
 rewrite > H4.

-(* Andrea: META NOT FOUND !!!  
-rewrite > sym_eq. *)
-simplify.intro.
+unfold Not.intro.

 apply (not_eq_O_S m1).
 rewrite > H5.reflexivity.
 qed.
 apply (not_eq_O_S m1).
 rewrite > H5.reflexivity.
 qed.

diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma
index 0ddd4b5c59571e69b8fe995151356085ef283604..6ec0c9992a68b18e15976e96e74ef853c2fc04eb 100644 (file)
--- a/helm/matita/library/nat/orders.ma
+++ b/helm/matita/library/nat/orders.ma
@@ -54,7 +54,7 @@ interpretation "natural 'not greater than'" 'ngtr x y =
   (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/orders/gt.con x y)).
 
 theorem transitive_le : transitive nat le.
   (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/orders/gt.con x y)).
 
 theorem transitive_le : transitive nat le.

-simplify.intros.elim H1.
+unfold transitive.intros.elim H1.

 assumption.
 apply le_S.assumption.
 qed.
 assumption.
 apply le_S.assumption.
 qed.


@@ -63,7 +63,7 @@ theorem trans_le: \forall n,m,p:nat. n \leq m \to m \leq p \to n \leq p
 \def transitive_le.
 
 theorem transitive_lt: transitive nat lt.
 \def transitive_le.
 
 theorem transitive_lt: transitive nat lt.

-simplify.intros.elim H1.
+unfold transitive.unfold lt.intros.elim H1.

 apply le_S. assumption.
 apply le_S.assumption.
 qed.
 apply le_S. assumption.
 apply le_S.assumption.
 qed.


@@ -105,11 +105,11 @@ qed.
 
 (* not le *)
 theorem not_le_Sn_O: \forall n:nat. S n \nleq O.
 
 (* not le *)
 theorem not_le_Sn_O: \forall n:nat. S n \nleq O.

-intros.simplify.intros.apply (leS_to_not_zero ? ? H).
+intros.unfold Not.simplify.intros.apply (leS_to_not_zero ? ? H).

 qed.
 
 theorem not_le_Sn_n: \forall n:nat. S n \nleq n.
 qed.
 
 theorem not_le_Sn_n: \forall n:nat. S n \nleq n.

-intros.elim n.apply not_le_Sn_O.simplify.intros.cut (S n1 \leq n1).
+intros.elim n.apply not_le_Sn_O.unfold Not.simplify.intros.cut (S n1 \leq n1).

 apply H.assumption.
 apply le_S_S_to_le.assumption.
 qed.
 apply H.assumption.
 apply le_S_S_to_le.assumption.
 qed.


@@ -119,19 +119,19 @@ theorem le_to_or_lt_eq : \forall n,m:nat.
 n \leq m \to n < m \lor n = m.
 intros.elim H.
 right.reflexivity.
 n \leq m \to n < m \lor n = m.
 intros.elim H.
 right.reflexivity.

-left.simplify.apply le_S_S.assumption.
+left.unfold lt.apply le_S_S.assumption.

 qed.
 
 (* not eq *)
 theorem lt_to_not_eq : \forall n,m:nat. n<m \to n \neq m.
 qed.
 
 (* not eq *)
 theorem lt_to_not_eq : \forall n,m:nat. n<m \to n \neq m.

-simplify.intros.cut ((le (S n) m) \to False).
+unfold Not.intros.cut ((le (S n) m) \to False).

 apply Hcut.assumption.rewrite < H1.
 apply not_le_Sn_n.
 qed.
 
 (* le vs. lt *)
 theorem lt_to_le : \forall n,m:nat. n<m \to n \leq m.
 apply Hcut.assumption.rewrite < H1.
 apply not_le_Sn_n.
 qed.
 
 (* le vs. lt *)
 theorem lt_to_le : \forall n,m:nat. n<m \to n \leq m.

-simplify.intros.elim H.
+simplify.intros.unfold lt in H.elim H.

 apply le_S. apply le_n.
 apply le_S. assumption.
 qed.
 apply le_S. apply le_n.
 apply le_S. assumption.
 qed.


@@ -145,13 +145,13 @@ theorem not_le_to_lt: \forall n,m:nat. n \nleq m \to m<n.
 intros 2.
 apply (nat_elim2 (\lambda n,m.n \nleq m \to m<n)).
 intros.apply (absurd (O \leq n1)).apply le_O_n.assumption.
 intros 2.
 apply (nat_elim2 (\lambda n,m.n \nleq m \to m<n)).
 intros.apply (absurd (O \leq n1)).apply le_O_n.assumption.

-simplify.intros.apply le_S_S.apply le_O_n.
-simplify.intros.apply le_S_S.apply H.intros.apply H1.apply le_S_S.
+unfold Not.unfold lt.intros.apply le_S_S.apply le_O_n.
+unfold Not.unfold lt.intros.apply le_S_S.apply H.intros.apply H1.apply le_S_S.

 assumption.
 qed.
 
 theorem lt_to_not_le: \forall n,m:nat. n<m \to m \nleq n.
 assumption.
 qed.
 
 theorem lt_to_not_le: \forall n,m:nat. n<m \to m \nleq n.

-simplify.intros 3.elim H.
+unfold Not.unfold lt.intros 3.elim H.

 apply (not_le_Sn_n n H1).
 apply H2.apply lt_to_le. apply H3.
 qed.
 apply (not_le_Sn_n n H1).
 apply H2.apply lt_to_le. apply H3.
 qed.


@@ -165,7 +165,7 @@ qed.
 theorem le_to_not_lt: \forall n,m:nat. le n m \to Not (lt m n).
 intros.
 change with (Not (le (S m) n)).
 theorem le_to_not_lt: \forall n,m:nat. le n m \to Not (lt m n).
 intros.
 change with (Not (le (S m) n)).

-apply lt_to_not_le.simplify.
+apply lt_to_not_le.unfold lt.

 apply le_S_S.assumption.
 qed.
 
 apply le_S_S.assumption.
 qed.
 


@@ -195,12 +195,12 @@ qed.
 (* lt and le trans *)
 theorem lt_to_le_to_lt: \forall n,m,p:nat. lt n m \to le m p \to lt n p.
 intros.elim H1.
 (* lt and le trans *)
 theorem lt_to_le_to_lt: \forall n,m,p:nat. lt n m \to le m p \to lt n p.
 intros.elim H1.

-assumption.simplify.apply le_S.assumption.
+assumption.unfold lt.apply le_S.assumption.

 qed.
 
 theorem le_to_lt_to_lt: \forall n,m,p:nat. le n m \to lt m p \to lt n p.
 intros 4.elim H.
 qed.
 
 theorem le_to_lt_to_lt: \forall n,m,p:nat. le n m \to lt m p \to lt n p.
 intros 4.elim H.

-assumption.apply H2.simplify.
+assumption.apply H2.unfold lt.

 apply lt_to_le.assumption.
 qed.
 
 apply lt_to_le.assumption.
 qed.
 


@@ -217,7 +217,7 @@ qed.
 
 (* other abstract properties *)
 theorem antisymmetric_le : antisymmetric nat le.
 
 (* other abstract properties *)
 theorem antisymmetric_le : antisymmetric nat le.

-simplify.intros 2.
+unfold antisymmetric.intros 2.

 apply (nat_elim2 (\lambda n,m.(n \leq m \to m \leq n \to n=m))).
 intros.apply le_n_O_to_eq.assumption.
 intros.apply False_ind.apply (not_le_Sn_O ? H).
 apply (nat_elim2 (\lambda n,m.(n \leq m \to m \leq n \to n=m))).
 intros.apply le_n_O_to_eq.assumption.
 intros.apply False_ind.apply (not_le_Sn_O ? H).


@@ -232,11 +232,11 @@ theorem antisym_le: \forall n,m:nat. n \leq m \to m \leq n \to n=m
 theorem decidable_le: \forall n,m:nat. decidable (n \leq m).
 intros.
 apply (nat_elim2 (\lambda n,m.decidable (n \leq m))).
 theorem decidable_le: \forall n,m:nat. decidable (n \leq m).
 intros.
 apply (nat_elim2 (\lambda n,m.decidable (n \leq m))).

-intros.simplify.left.apply le_O_n.
-intros.simplify.right.exact (not_le_Sn_O n1).
-intros 2.simplify.intro.elim H.
+intros.unfold decidable.left.apply le_O_n.
+intros.unfold decidable.right.exact (not_le_Sn_O n1).
+intros 2.unfold decidable.intro.elim H.

 left.apply le_S_S.assumption.
 left.apply le_S_S.assumption.

-right.intro.apply H1.apply le_S_S_to_le.assumption.
+right.unfold Not.intro.apply H1.apply le_S_S_to_le.assumption.

 qed.
 
 theorem decidable_lt: \forall n,m:nat. decidable (n < m).
 qed.
 
 theorem decidable_lt: \forall n,m:nat. decidable (n < m).


@@ -265,7 +265,7 @@ definition increasing \def \lambda f:nat \to nat.
 
 theorem increasing_to_monotonic: \forall f:nat \to nat.
 increasing f \to monotonic nat lt f.
 
 theorem increasing_to_monotonic: \forall f:nat \to nat.
 increasing f \to monotonic nat lt f.

-simplify.intros.elim H1.apply H.
+unfold monotonic.unfold lt.unfold increasing.unfold lt.intros.elim H1.apply H.

 apply (trans_le ? (f n1)).
 assumption.apply (trans_le ? (S (f n1))).
 apply le_n_Sn.
 apply (trans_le ? (f n1)).
 assumption.apply (trans_le ? (S (f n1))).
 apply le_n_Sn.


@@ -278,7 +278,7 @@ intros.elim n.
 apply le_O_n.
 apply (trans_le ? (S (f n1))).
 apply le_S_S.apply H1.
 apply le_O_n.
 apply (trans_le ? (S (f n1))).
 apply le_S_S.apply H1.

-simplify in H. apply H.
+simplify in H. unfold increasing in H.unfold lt in H.apply H.

 qed.
 
 theorem increasing_to_le: \forall f:nat \to nat. (increasing f) 
 qed.
 
 theorem increasing_to_le: \forall f:nat \to nat. (increasing f) 


@@ -289,7 +289,7 @@ elim H1.
 apply (ex_intro ? ? (S a)).
 apply (trans_le ? (S (f a))).
 apply le_S_S.assumption.
 apply (ex_intro ? ? (S a)).
 apply (trans_le ? (S (f a))).
 apply le_S_S.assumption.

-simplify in H.
+simplify in H.unfold increasing in H.unfold lt in H.

 apply H.
 qed.
 
 apply H.
 qed.
 

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.
 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.
 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.
 
 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 
 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.
 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.
 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.
 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.
 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).
 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.
 (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)).
 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.
 
 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).
 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.
 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)).
 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.
 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.
 
 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.
 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.
 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.
 
 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.
 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.
 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)).
 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
 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.
 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.
 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.
 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.
 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))).
 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.
 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).
 (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.
 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.
 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.
 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.
 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 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.
 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.
 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.
 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.

diff --git a/helm/matita/library/nat/plus.ma b/helm/matita/library/nat/plus.ma
index 8043d9a526663efc3b2b526fb35466cf49fe20be..d595dad19113cb6626ec4e58cc1e8a2d389be2b1 100644 (file)
--- a/helm/matita/library/nat/plus.ma
+++ b/helm/matita/library/nat/plus.ma
@@ -43,7 +43,7 @@ simplify.rewrite > H.apply plus_n_Sm.
 qed.
 
 theorem associative_plus : associative nat plus.
 qed.
 
 theorem associative_plus : associative nat plus.

-simplify.intros.elim x.
+unfold associative.intros.elim x.

 simplify.reflexivity.
 simplify.apply eq_f.assumption.
 qed.
 simplify.reflexivity.
 simplify.apply eq_f.assumption.
 qed.

diff --git a/helm/matita/library/nat/primes.ma b/helm/matita/library/nat/primes.ma
index 452adc89c9788ac726cdd661ffb83294865353bd..50b7d1221bfdca8211184a664add8c73aa392bd5 100644 (file)
--- a/helm/matita/library/nat/primes.ma
+++ b/helm/matita/library/nat/primes.ma
@@ -27,7 +27,7 @@ interpretation "not divides" 'ndivides n m =
  (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/primes/divides.ind#xpointer(1/1) n m)).
 
 theorem reflexive_divides : reflexive nat divides.
  (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/primes/divides.ind#xpointer(1/1) n m)).
 
 theorem reflexive_divides : reflexive nat divides.

-simplify.
+unfold reflexive.

 intros.
 exact (witness x x (S O) (times_n_SO x)).
 qed.
 intros.
 exact (witness x x (S O) (times_n_SO x)).
 qed.


@@ -151,7 +151,7 @@ apply (decidable_le n m).
 qed.
 
 theorem antisymmetric_divides: antisymmetric nat divides.
 qed.
 
 theorem antisymmetric_divides: antisymmetric nat divides.

-simplify.intros.elim H. elim H1.
+unfold antisymmetric.intros.elim H. elim H1.

 apply (nat_case1 n2).intro.
 rewrite > H3.rewrite > H2.rewrite > H4.
 rewrite < times_n_O.reflexivity.
 apply (nat_case1 n2).intro.
 rewrite > H3.rewrite > H2.rewrite > H4.
 rewrite < times_n_O.reflexivity.


@@ -206,7 +206,7 @@ match eqb (m \mod n) O with
 | false \Rightarrow n \ndivides m].
 apply eqb_elim.
 intro.simplify.apply mod_O_to_divides.assumption.assumption.
 | false \Rightarrow n \ndivides m].
 apply eqb_elim.
 intro.simplify.apply mod_O_to_divides.assumption.assumption.

-intro.simplify.intro.apply H1.apply divides_to_mod_O.assumption.assumption.
+intro.simplify.unfold Not.intro.apply H1.apply divides_to_mod_O.assumption.assumption.

 qed.
 
 theorem divides_b_true_to_divides :
 qed.
 
 theorem divides_b_true_to_divides :


@@ -339,11 +339,11 @@ definition prime : nat \to  Prop \def
 (\forall m:nat. m \divides n \to (S O) < m \to  m = n).
 
 theorem not_prime_O: \lnot (prime O).
 (\forall m:nat. m \divides n \to (S O) < m \to  m = n).
 
 theorem not_prime_O: \lnot (prime O).

-simplify.intro.elim H.apply (not_le_Sn_O (S O) H1).
+unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_O (S O) H1).

 qed.
 
 theorem not_prime_SO: \lnot (prime (S O)).
 qed.
 
 theorem not_prime_SO: \lnot (prime (S O)).

-simplify.intro.elim H.apply (not_le_Sn_n (S O) H1).
+unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_n (S O) H1).

 qed.
 
 (* smallest factor *)
 qed.
 
 (* smallest factor *)


@@ -390,10 +390,10 @@ theorem lt_O_smallest_factor: \forall n:nat. O < n \to O < (smallest_factor n).
 intro.
 apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_n O H).
 intro.apply (nat_case m).intro.
 intro.
 apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_n O H).
 intro.apply (nat_case m).intro.

-simplify.apply le_n.
+simplify.unfold lt.apply le_n.

 intros.apply (trans_lt ? (S O)).
 intros.apply (trans_lt ? (S O)).

-simplify. apply le_n.
-apply lt_SO_smallest_factor.simplify. apply le_S_S.
+unfold lt.apply le_n.
+apply lt_SO_smallest_factor.unfold lt. apply le_S_S.

 apply le_S_S.apply le_O_n.
 qed.
 
 apply le_S_S.apply le_O_n.
 qed.
 


@@ -414,7 +414,7 @@ apply (ex_intro nat ? (S(S m1))).
 split.split.
 apply le_minus_m.apply le_n.
 rewrite > mod_n_n.reflexivity.
 split.split.
 apply le_minus_m.apply le_n.
 rewrite > mod_n_n.reflexivity.

-apply (trans_lt ? (S O)).apply (le_n (S O)).simplify.
+apply (trans_lt ? (S O)).apply (le_n (S O)).unfold lt.

 apply le_S_S.apply le_S_S.apply le_O_n.
 qed.
   
 apply le_S_S.apply le_S_S.apply le_O_n.
 qed.
   


@@ -423,9 +423,9 @@ theorem le_smallest_factor_n :
 intro.apply (nat_case n).simplify.reflexivity.
 intro.apply (nat_case m).simplify.reflexivity.
 intro.apply divides_to_le.
 intro.apply (nat_case n).simplify.reflexivity.
 intro.apply (nat_case m).simplify.reflexivity.
 intro.apply divides_to_le.

-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.

 apply divides_smallest_factor_n.
 apply divides_smallest_factor_n.

-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.

 qed.
 
 theorem lt_smallest_factor_to_not_divides: \forall n,i:nat. 
 qed.
 
 theorem lt_smallest_factor_to_not_divides: \forall n,i:nat. 


@@ -459,7 +459,7 @@ absurd (m \divides n).
 apply (transitive_divides m (smallest_factor n)).
 assumption.
 apply divides_smallest_factor_n.
 apply (transitive_divides m (smallest_factor n)).
 assumption.
 apply divides_smallest_factor_n.

-apply (trans_lt ? (S O)). simplify. apply le_n. exact H.
+apply (trans_lt ? (S O)). unfold lt. apply le_n. exact H.

 apply lt_smallest_factor_to_not_divides.
 exact H.assumption.assumption.assumption.
 apply divides_to_le.
 apply lt_smallest_factor_to_not_divides.
 exact H.assumption.assumption.assumption.
 apply divides_to_le.


@@ -481,7 +481,7 @@ change with
 smallest_factor (S(S m1)) = (S(S m1))).
 intro.elim H.apply H2.
 apply divides_smallest_factor_n.
 smallest_factor (S(S m1)) = (S(S m1))).
 intro.elim H.apply H2.
 apply divides_smallest_factor_n.

-apply (trans_lt ? (S O)).simplify. apply le_n.assumption.
+apply (trans_lt ? (S O)).unfold lt. apply le_n.assumption.

 apply lt_SO_smallest_factor.
 assumption.
 qed.
 apply lt_SO_smallest_factor.
 assumption.
 qed.


@@ -517,8 +517,8 @@ match primeb n with
 [ true \Rightarrow prime n
 | false \Rightarrow \lnot (prime n)].
 intro.
 [ true \Rightarrow prime n
 | false \Rightarrow \lnot (prime n)].
 intro.

-apply (nat_case n).simplify.intro.elim H.apply (not_le_Sn_O (S O) H1).
-intro.apply (nat_case m).simplify.intro.elim H.apply (not_le_Sn_n (S O) H1).
+apply (nat_case n).simplify.unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_O (S O) H1).
+intro.apply (nat_case m).simplify.unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_n (S O) H1).

 intro.
 change with 
 match eqb (smallest_factor (S(S m1))) (S(S m1)) with
 intro.
 change with 
 match eqb (smallest_factor (S(S m1))) (S(S m1)) with


@@ -528,7 +528,7 @@ apply (eqb_elim (smallest_factor (S(S m1))) (S(S m1))).
 intro.change with (prime (S(S m1))).
 rewrite < H.
 apply prime_smallest_factor_n.
 intro.change with (prime (S(S m1))).
 rewrite < H.
 apply prime_smallest_factor_n.

-simplify.apply le_S_S.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_S_S.apply le_O_n.

 intro.change with (\lnot (prime (S(S m1)))).
 change with (prime (S(S m1)) \to False).
 intro.apply H.
 intro.change with (\lnot (prime (S(S m1)))).
 change with (prime (S(S m1)) \to False).
 intro.apply H.

diff --git a/helm/matita/library/nat/times.ma b/helm/matita/library/nat/times.ma
index 70a4fd76ef5ab626a2d6a00d13fb075406c55f2a..2ae5ffd749b745783a2cf8c3eded7166cc4f8108 100644 (file)
--- a/helm/matita/library/nat/times.ma
+++ b/helm/matita/library/nat/times.ma
@@ -52,7 +52,7 @@ reflexivity.
 qed.
 
 theorem symmetric_times : symmetric nat times. 
 qed.
 
 theorem symmetric_times : symmetric nat times. 

-simplify.
+unfold symmetric.

 intros.elim x.
 simplify.apply times_n_O.
 simplify.rewrite > H.apply times_n_Sm.
 intros.elim x.
 simplify.apply times_n_O.
 simplify.rewrite > H.apply times_n_Sm.


@@ -62,7 +62,7 @@ variant sym_times : \forall n,m:nat. n*m = m*n \def
 symmetric_times.
 
 theorem distributive_times_plus : distributive nat times plus.
 symmetric_times.
 
 theorem distributive_times_plus : distributive nat times plus.

-simplify.
+unfold distributive.

 intros.elim x.
 simplify.reflexivity.
 simplify.rewrite > H. rewrite > assoc_plus.rewrite > assoc_plus.
 intros.elim x.
 simplify.reflexivity.
 simplify.rewrite > H. rewrite > assoc_plus.rewrite > assoc_plus.


@@ -74,7 +74,7 @@ variant distr_times_plus: \forall n,m,p:nat. n*(m+p) = n*m + n*p
 \def distributive_times_plus.
 
 theorem associative_times: associative nat times.
 \def distributive_times_plus.
 
 theorem associative_times: associative nat times.

-simplify.intros.
+unfold associative.intros.

 elim x.simplify.apply refl_eq.
 simplify.rewrite < sym_times.
 rewrite > distr_times_plus.
 elim x.simplify.apply refl_eq.
 simplify.rewrite < sym_times.
 rewrite > distr_times_plus.

diff --git a/helm/matita/library/nat/totient.ma b/helm/matita/library/nat/totient.ma
index ff425772cd276d31b239c15bb35d5f5e6345ef50..24c3920ed82571324c2977a7be798b492fbf43e7 100644 (file)
--- a/helm/matita/library/nat/totient.ma
+++ b/helm/matita/library/nat/totient.ma
@@ -68,35 +68,35 @@ rewrite < H4.
 rewrite > sym_gcd.
 rewrite > gcd_mod.
 apply (gcd_times_SO_to_gcd_SO ? ? (S m2)).
 rewrite > sym_gcd.
 rewrite > gcd_mod.
 apply (gcd_times_SO_to_gcd_SO ? ? (S m2)).

-simplify.apply le_S_S.apply le_O_n.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.

 assumption.
 assumption.

-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.

 rewrite < H5.
 rewrite > sym_gcd.
 rewrite > gcd_mod.
 apply (gcd_times_SO_to_gcd_SO ? ? (S m)).
 rewrite < H5.
 rewrite > sym_gcd.
 rewrite > gcd_mod.
 apply (gcd_times_SO_to_gcd_SO ? ? (S m)).

-simplify.apply le_S_S.apply le_O_n.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.

 rewrite > sym_times.
 assumption.
 rewrite > sym_times.
 assumption.

-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.

 intro.
 apply eqb_elim.
 intro.apply eqb_elim.
 intro.apply False_ind.
 apply H6.
 apply eq_gcd_times_SO.
 intro.
 apply eqb_elim.
 intro.apply eqb_elim.
 intro.apply False_ind.
 apply H6.
 apply eq_gcd_times_SO.

-simplify.apply le_S_S.apply le_O_n.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.

 rewrite < gcd_mod.
 rewrite > H4.
 rewrite > sym_gcd.assumption.
 rewrite < gcd_mod.
 rewrite > H4.
 rewrite > sym_gcd.assumption.

-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.

 rewrite < gcd_mod.
 rewrite > H5.
 rewrite > sym_gcd.assumption.
 rewrite < gcd_mod.
 rewrite > H5.
 rewrite > sym_gcd.assumption.

-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.

 intro.reflexivity.
 intro.reflexivity.
 qed.
\ No newline at end of file
 intro.reflexivity.
 intro.reflexivity.
 qed.
\ No newline at end of file

diff --git a/helm/matita/tests/simpl.ma b/helm/matita/tests/simpl.ma
index 75a1693f41d6b15f8afd82422f2b1dd678628748..1001d2351f0b97a50da92ef8a48cad25b17b4c47 100644 (file)
--- a/helm/matita/tests/simpl.ma
+++ b/helm/matita/tests/simpl.ma
@@ -28,7 +28,7 @@ theorem a :
  \forall x,y : A.
  not (x = y) \to not(y = x).
 intros.
  \forall x,y : A.
  not (x = y) \to not(y = x).
 intros.

-simplify.
+unfold not. (* simplify. *)

 intro. apply H.
 symmetry.
 exact H1.
 intro. apply H.
 symmetry.
 exact H1.