Coq: make some uses of auto in the library more robust

2 files changed, 19 insertions, 18 deletions

diff --git a/lib/coq/Operators_mwords.v b/lib/coq/Operators_mwords.v
index ccb3b1de..337706fa 100644
--- a/lib/coq/Operators_mwords.v
+++ b/lib/coq/Operators_mwords.v
@@ -186,8 +186,8 @@ Defined.
 Definition update_subrange_vec_inc {n} (v : mword n) m o `{ArithFact (0 <=? m)} `{ArithFact (m <=? o <? n)} (w : mword (o - m + 1)) : mword n := update_subrange_vec_dec v (n-1-m) (n-1-o) (autocast w).
 
 Lemma mword_nonneg {a} : mword a -> a >= 0.
-destruct a;
-auto using Z.le_ge, Zle_0_pos with zarith.
+destruct a.
+1,2: auto using Z.le_ge, Zle_0_pos with zarith.
 destruct 1.
 Qed.
 
@@ -255,7 +255,7 @@ Defined.
 Lemma concat_eq {a b} : a >= 0 -> b >= 0 -> Z.of_nat (Z.to_nat b + Z.to_nat a)%nat = a + b.
 intros.
 rewrite Nat2Z.inj_add.
-rewrite Z2Nat.id; auto with zarith.
+rewrite Z2Nat.id. 2: solve [ auto with zarith ].
 rewrite Z2Nat.id; auto with zarith.
 Qed.
 
@@ -303,9 +303,9 @@ constructor.
   assert (2 ^ a - 1 = Z.of_N (2 ^ (Z.to_N a) - 1)). {
     rewrite N2Z.inj_sub.
     * rewrite N2Z.inj_pow.
-      rewrite Z2N.id; auto.
-      destruct a; auto with zarith. destruct x.
-    * apply N.le_trans with (m := (2^0)%N); auto using N.le_refl.
+      rewrite Z2N.id. solve [ auto ].
+      destruct a. 1,2: auto with zarith. destruct x.
+    * apply N.le_trans with (m := (2^0)%N). solve [ auto using N.le_refl ].
       apply N.pow_le_mono_r.
       inversion 1.
       apply N.le_0_l.
@@ -346,8 +346,8 @@ rewrite eq.
 rewrite Nat2Z.id.
 intro w.
 destruct (Word.wordToZ_size' w) as [LO HI].
-replace 1 with (Z.of_nat 1); auto.
-rewrite <- Nat2Z.inj_sub; auto with arith.
+replace 1 with (Z.of_nat 1). 2: solve [ auto ].
+rewrite <- Nat2Z.inj_sub. 2: solve [ auto with arith ].
 simpl.
 rewrite <- minus_n_O.
 rewrite Zpow_pow2.
@@ -489,8 +489,8 @@ end.
 Lemma replicate_ok {n a} `{ArithFact (n >=? 0)} `{ArithFact (a >=? 0)} :
    Z.of_nat (Z.to_nat n * Z.to_nat a) = a * n.
 destruct H. destruct H0. unbool_comparisons.
-rewrite <- Z2Nat.id; auto with zarith.
-rewrite Z2Nat.inj_mul; auto with zarith.
+rewrite <- Z2Nat.id. 2: solve [ auto with zarith ].
+rewrite Z2Nat.inj_mul. 2,3: solve [ auto with zarith ].
 rewrite Nat.mul_comm. reflexivity.
 Qed.
 Definition replicate_bits {a} (w : mword a) (n : Z) `{ArithFact (n >=? 0)} : mword (a * n) :=
diff --git a/lib/coq/Values.v b/lib/coq/Values.v
index 2cab87f8..4b48151a 100644
--- a/lib/coq/Values.v
+++ b/lib/coq/Values.v
@@ -213,7 +213,8 @@ Lemma ZEuclid_div_pos : forall x y, 0 < y -> 0 <= x -> 0 <= ZEuclid.div x y.
 intros.
 unfold ZEuclid.div.
 change 0 with (0 * 0).
-apply Zmult_le_compat; auto with zarith.
+apply Zmult_le_compat.
+3,4: auto with zarith.
 * apply Z.sgn_nonneg. auto with zarith.
 * apply Z_div_pos; auto. apply Z.lt_gt. apply Z.abs_pos. auto with zarith.
 Qed.
@@ -231,7 +232,7 @@ Qed.
 Lemma ZEuclid_div_ge : forall x y, y > 0 -> x >= 0 -> x - ZEuclid.div x y >= 0.
 intros.
 unfold ZEuclid.div.
-rewrite Z.sgn_pos; auto with zarith.
+rewrite Z.sgn_pos. 2: solve [ auto with zarith ].
 rewrite Z.mul_1_l.
 apply Z.le_ge.
 apply Zle_minus_le_0.
@@ -1152,9 +1153,9 @@ Qed.
 Lemma ArithFact_mword (a : Z) (w : mword a) : ArithFact (a >=? 0).
 constructor.
 destruct a.
-auto with zarith.
-auto using Z.le_ge, Zle_0_pos.
-destruct w.
+* auto with zarith.
+* auto using Z.le_ge, Zle_0_pos.
+* destruct w.
 Qed.
 (* Remove constructor from ArithFact(P)s and if they're used elsewhere
    in the context create a copy that rewrites will work on. *)
@@ -2205,9 +2206,9 @@ Hint Unfold neq_atom : sail.
 Lemma ReasonableSize_witness (a : Z) (w : mword a) : ReasonableSize a.
 constructor.
 destruct a.
-auto with zarith.
-auto using Z.le_ge, Zle_0_pos.
-destruct w.
+* auto with zarith.
+* auto using Z.le_ge, Zle_0_pos.
+* destruct w.
 Qed.
 
 Hint Extern 0 (ReasonableSize ?A) => (unwrap_ArithFacts; solve [apply ReasonableSize_witness; assumption | constructor; auto with zarith]) : typeclass_instances.