diff options
| -rw-r--r-- | lib/coq/Operators_mwords.v | 20 | ||||
| -rw-r--r-- | lib/coq/Values.v | 17 |
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. |