diff options
author | 2017-04-04 14:35:43 -0400 | |
---|---|---|
committer | 2017-04-04 16:05:55 -0400 | |
commit | 331fe3fcfb27d87dcfb0585ced3c051f19aaedf2 (patch) | |
tree | a9af1a7f8bba3fb1f6e7d1610ca1553f5e5f23c2 /src/BoundedArithmetic/Double/Repeated/Proofs | |
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/BoundedArithmetic/Double/Repeated/Proofs')
-rw-r--r-- | src/BoundedArithmetic/Double/Repeated/Proofs/Multiply.v | 2 | ||||
-rw-r--r-- | src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/src/BoundedArithmetic/Double/Repeated/Proofs/Multiply.v b/src/BoundedArithmetic/Double/Repeated/Proofs/Multiply.v index 2c7a0ad1b..a00e0c891 100644 --- a/src/BoundedArithmetic/Double/Repeated/Proofs/Multiply.v +++ b/src/BoundedArithmetic/Double/Repeated/Proofs/Multiply.v @@ -64,7 +64,7 @@ Section multiply. : (is_mul_low_low (Z.of_nat 2^Z.of_nat exp * n_over_two) (multiply_low_low_repeated_double (exp:=exp)) * is_mul_high_low (Z.of_nat 2^Z.of_nat exp * n_over_two) (multiply_high_low_repeated_double (exp:=exp)) * is_mul_high_high (Z.of_nat 2^Z.of_nat exp * n_over_two) (multiply_high_high_repeated_double (exp:=exp)))%type. - Proof. + Proof using Type*. destruct exp as [|exp']; [ clear is_multi_multiply_repeated_double | specialize (is_multi_multiply_repeated_double exp') ]. { destruct decode; generalize ismulhwll, ismulhwhl, ismulhwhh. simpl. diff --git a/src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v b/src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v index 401e3a015..acda67158 100644 --- a/src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v +++ b/src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v @@ -32,7 +32,7 @@ Section shift_left_right. Fixpoint is_shift_left_right_immediate_repeated_double {exp : nat} : (is_shift_left_immediate (shift_left_immediate_repeated_double (exp:=exp)) * is_shift_right_immediate (shift_right_immediate_repeated_double (exp:=exp)))%type. - Proof. is_cls_fixpoint_t2 decode n exp is_shl is_shr (@is_shift_left_right_immediate_repeated_double). Qed. + Proof using Type*. is_cls_fixpoint_t2 decode n exp is_shl is_shr (@is_shift_left_right_immediate_repeated_double). Qed. Global Instance is_shift_left_immediate_repeated_double {exp : nat} : is_shift_left_immediate (shift_left_immediate_repeated_double (exp:=exp)) := fst (@is_shift_left_right_immediate_repeated_double exp). |