Testing a replacement of "cut" by "enough" on a couple of test files.

4 files changed, 31 insertions, 36 deletions

diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index a5e710504..99b631905 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -54,17 +54,17 @@ Theorem Z_lt_abs_rec :
 Proof.
   intros P HP p.
   set (Q := fun z => 0 <= z -> P z * P (- z)).
-  cut (Q (Z.abs p)); [ intros H | apply (Z_lt_rec Q); auto with zarith ].
-  elim (Zabs_dec p); intro eq; rewrite eq;
-    elim H; auto with zarith.
-  intros x H; subst Q. 
+  enough (H:Q (Z.abs p)) by
+    (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith).
+  apply (Z_lt_rec Q); auto with zarith.
+  subst Q; intros x H.
   split; apply HP.
-  rewrite Z.abs_eq; auto; intros.
-  elim (H (Z.abs m)); intros; auto with zarith.
-  elim (Zabs_dec m); intro eq; rewrite eq; trivial.
-  rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros.
-  elim (H (Z.abs m)); intros; auto with zarith.
-  elim (Zabs_dec m); intro eq; rewrite eq; trivial.
+  - rewrite Z.abs_eq; auto; intros.
+    destruct (H (Z.abs m)); auto with zarith.
+    destruct (Zabs_dec m) as [-> | ->]; trivial.
+  - rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros.
+    destruct (H (Z.abs m)); auto with zarith.
+    destruct (Zabs_dec m) as [-> | ->]; trivial.
 Qed.
 
 Theorem Z_lt_abs_induction :
@@ -74,16 +74,17 @@ Theorem Z_lt_abs_induction :
 Proof.
   intros P HP p.
   set (Q := fun z => 0 <= z -> P z /\ P (- z)) in *.
-  cut (Q (Z.abs p)); [ intros | apply (Z_lt_induction Q); auto with zarith ].
-  elim (Zabs_dec p); intro eq; rewrite eq; elim H; auto with zarith.
-  unfold Q; clear Q; intros.
+  enough (Q (Z.abs p)) by
+    (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith).
+  apply (Z_lt_induction Q); auto with zarith.
+  subst Q; intros.
   split; apply HP.
-  rewrite Z.abs_eq; auto; intros.
-  elim (H (Z.abs m)); intros; auto with zarith.
-  elim (Zabs_dec m); intro eq; rewrite eq; trivial.
-  rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros.
-  elim (H (Z.abs m)); intros; auto with zarith.
-  elim (Zabs_dec m); intro eq; rewrite eq; trivial.
+  - rewrite Z.abs_eq; auto; intros.
+    elim (H (Z.abs m)); intros; auto with zarith.
+    elim (Zabs_dec m); intro eq; rewrite eq; trivial.
+  - rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros.
+    destruct (H (Z.abs m)); auto with zarith.
+    destruct (Zabs_dec m) as [-> | ->]; trivial.
 Qed.
 
 (** To do case analysis over the sign of [z] *)
diff --git a/theories/ZArith/Zdigits.v b/theories/ZArith/Zdigits.v
index e5325aa75..043b68dd3 100644
--- a/theories/ZArith/Zdigits.v
+++ b/theories/ZArith/Zdigits.v
@@ -212,13 +212,10 @@ Section Z_BRIC_A_BRAC.
       (z < two_power_nat (S n))%Z -> (Z.div2 z < two_power_nat n)%Z.
   Proof.
     intros.
-    cut (2 * Z.div2 z < 2 * two_power_nat n)%Z; intros.
-    omega.
-
+    enough (2 * Z.div2 z < 2 * two_power_nat n)%Z by omega.
     rewrite <- two_power_nat_S.
     destruct (Zeven.Zeven_odd_dec z) as [Heven|Hodd]; intros.
     rewrite <- Zeven.Zeven_div2; auto.
-
     generalize (Zeven.Zodd_div2 z Hodd); omega.
   Qed.
 
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 32993b2c0..f7843ea74 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -666,17 +666,15 @@ Theorem Zdiv_eucl_extended :
       {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < Z.abs b}.
 Proof.
   intros b Hb a.
-  elim (Z_le_gt_dec 0 b); intro Hb'.
-  cut (b > 0); [ intro Hb'' | omega ].
-  rewrite Z.abs_eq; [ apply Zdiv_eucl_exist; assumption | assumption ].
-  cut (- b > 0); [ intro Hb'' | omega ].
-  elim (Zdiv_eucl_exist Hb'' a); intros qr.
-  elim qr; intros q r Hqr.
-  exists (- q, r).
-  elim Hqr; intros.
-  split.
-  rewrite <- Z.mul_opp_comm; assumption.
-  rewrite Z.abs_neq; [ assumption | omega ].
+  destruct (Z_le_gt_dec 0 b) as [Hb'|Hb'].
+  - assert (Hb'' : b > 0) by omega.
+    rewrite Z.abs_eq; [ apply Zdiv_eucl_exist; assumption | assumption ].
+  - assert (Hb'' : - b > 0) by omega.
+    destruct (Zdiv_eucl_exist Hb'' a) as ((q,r),[]).
+    exists (- q, r).
+    split.
+    + rewrite <- Z.mul_opp_comm; assumption.
+    + rewrite Z.abs_neq; [ assumption | omega ].
 Qed.
 
 Arguments Zdiv_eucl_extended : default implicits.
diff --git a/theories/ZArith/Zgcd_alt.v b/theories/ZArith/Zgcd_alt.v
index aeddeb70c..fa059313f 100644
--- a/theories/ZArith/Zgcd_alt.v
+++ b/theories/ZArith/Zgcd_alt.v
@@ -105,8 +105,7 @@ Open Scope Z_scope.
 
  Lemma fibonacci_pos : forall n, 0 <= fibonacci n.
  Proof.
-   cut (forall N n, (n<N)%nat -> 0<=fibonacci n).
-   eauto.
+   enough (forall N n, (n<N)%nat -> 0<=fibonacci n) by eauto.
    induction N.
    inversion 1.
    intros.