diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-04 14:35:43 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-04-04 16:05:55 -0400 |
| commit | 331fe3fcfb27d87dcfb0585ced3c051f19aaedf2 (patch) | |
| tree | a9af1a7f8bba3fb1f6e7d1610ca1553f5e5f23c2 /src/Testbit.v | |
| parent | 6cba3c4e0572e9d917d3578c39f4f85cd3799b54 (diff) | |
Add [Proof using] to most proofs
This closes #146 and makes `make quick` faster.
The changes were generated by adding [Global Set Suggest Proof Using.]
to GlobalSettings.v, and then following [the instructions for a script I
wrote](https://github.com/JasonGross/coq-tools#proof-using-helper).
Diffstat (limited to 'src/Testbit.v')
| -rw-r--r-- | src/Testbit.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Testbit.v b/src/Testbit.v index 57362d10b..1da2c33e0 100644 --- a/src/Testbit.v +++ b/src/Testbit.v @@ -36,7 +36,7 @@ Section Testbit. Lemma testbit_spec' : forall a b us, (0 <= b < width) -> bounded limb_widths us -> (length us = length limb_widths)%nat -> Z.testbit (nth_default 0 us a) b = Z.testbit (decode base us) (Z.of_nat a * width + b). - Proof. + Proof using limb_width_pos limb_widths_uniform. repeat match goal with | |- _ => progress intros | |- _ => progress autorewrite with push_nth_default Ztestbit zsimplify in * @@ -67,7 +67,7 @@ Section Testbit. Lemma testbit_spec : forall n us, (length us = length limb_widths)%nat -> bounded limb_widths us -> testbit us n = Z.testbit (BaseSystem.decode base us) (Z.of_nat n). - Proof. + Proof using limb_width_pos limb_widths_uniform. cbv [testbit]; intros. pose proof limb_width_pos as limb_width_pos_nat. rewrite Z2Nat.inj_lt in limb_width_pos_nat by omega. |