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/Util/AdditionChainExponentiation.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/Util/AdditionChainExponentiation.v')
| -rw-r--r-- | src/Util/AdditionChainExponentiation.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Util/AdditionChainExponentiation.v b/src/Util/AdditionChainExponentiation.v index 97c3e02a3..fc082a54a 100644 --- a/src/Util/AdditionChainExponentiation.v +++ b/src/Util/AdditionChainExponentiation.v @@ -38,7 +38,7 @@ Section AddChainExp. (H:forall i, nth_default id acc i = (nth_default 0 ref i) * x) (Hl:Logic.eq (length acc) (length ref)), fold_chain id op is acc = (fold_chain 0 N.add is ref) * x. - Proof. + Proof using Type*. induction is; intros; simpl @fold_chain. { repeat break_match; specialize (H 0%nat); rewrite ?nth_default_cons, ?nth_default_cons_S in H; solve [ simpl length in *; discriminate | apply H | rewrite scalarmult_0_l; reflexivity ]. } @@ -51,7 +51,7 @@ Section AddChainExp. Qed. Lemma fold_chain_exp x is: fold_chain id op is [x] = (fold_chain 0 N.add is [1]) * x. - Proof. + Proof using Type*. eapply fold_chain_exp'; intros; trivial. destruct i; try destruct i; rewrite ?nth_default_cons_S, ?nth_default_cons, ?nth_default_nil; rewrite ?scalarmult_1_l, ?scalarmult_0_l; reflexivity. |