diff options
| m--------- | bbv | 0 | ||||
| m--------- | coqprime | 0 | ||||
| m--------- | etc/coq-scripts | 0 | ||||
| -rw-r--r-- | src/Util/WordUtil.v | 13 |
4 files changed, 3 insertions, 10 deletions
diff --git a/bbv b/bbv -Subproject eb51f6fc08e1b721cb913bd48555bf2063b0edd +Subproject 4dcd180f0605c6aa401097685593433d6806201 diff --git a/coqprime b/coqprime -Subproject e1fac2d7d1ce737233316f62848e350ed922b33 +Subproject bd626ee330cc28aadfc2d675772f5077b098f71 diff --git a/etc/coq-scripts b/etc/coq-scripts -Subproject b8e11b47376550ffd85ff7736dd45adcd40b384 +Subproject 7bd683da1fac8b5eb42de1e44a3274db4fd0ce4 diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index c1eeb138b..2faafe6c6 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -177,11 +177,6 @@ Section Natural. End Natural. Section Pow2. - Lemma pow2_id : forall n, pow2 n = 2 ^ n. - Proof. - induction n; intros; simpl; auto. - Qed. - Lemma Zpow_pow2 : forall n, pow2 n = Z.to_nat (2 ^ (Z.of_nat n)). Proof. induction n as [|n IHn]; intros; auto. @@ -750,7 +745,7 @@ Proof. rewrite <- Nnat.N2Nat.id, Npow2_nat. replace (Z.to_N x) with (N.of_nat (Z.to_nat x)) by apply Z_nat_N. apply (Nat2N_inj_lt _ (pow2 n)). - rewrite pow2_id; assumption. + assumption. Qed. Lemma weqb_false_iff : forall sz (x y : word sz), weqb x y = false <-> x <> y. @@ -887,8 +882,7 @@ Proof. end. generalize (split1 _ _ x); generalize (split2 _ _ x); clear x; simpl. apply Min.min_case_strong; intros Hbc x0 x1; - pose proof (wordToNat_bound x0); pose proof (wordToNat_bound x1); - rewrite pow2_id in *. + pose proof (wordToNat_bound x0); pose proof (wordToNat_bound x1). { assert (b - c = 0) by omega. assert (2^b <= 2^c) by auto using pow_le_mono_r with arith. generalize dependent (b - c); intros n x0 H0 H2; destruct x0; try omega; []. @@ -919,8 +913,7 @@ Proof. rewrite wand_combine, !wordToNat_combine, wand_kill, wand_unit, wordToNat_wzero. generalize (split1 _ _ x); generalize (split2 _ _ x); clear x; simpl. apply Min.min_case_strong; intros Hbc x0 x1; - pose proof (wordToNat_bound x0); pose proof (wordToNat_bound x1); - rewrite pow2_id in *. + pose proof (wordToNat_bound x0); pose proof (wordToNat_bound x1). { assert (b - c = 0) by omega. assert (2^b <= 2^c) by auto using pow_le_mono_r with arith. generalize dependent (b - c); intros n x0 H0 H2; destruct x0; try omega. |