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/Spec | |
| 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/Spec')
| -rw-r--r-- | src/Spec/Ed25519.v | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index 4fc3afce4..2a2847a31 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -65,10 +65,16 @@ Section Ed25519. { Crypto.Util.Decidable.vm_decide. } { Crypto.Util.Decidable.vm_decide. } Admitted. - Lemma nonzero_a : a <> 0%F. Crypto.Util.Decidable.vm_decide. Qed. + Lemma nonzero_a : a <> 0%F. + Proof using Type. + Crypto.Util.Decidable.vm_decide. Qed. Lemma square_a : exists sqrt_a : Fq, (sqrt_a * sqrt_a)%F = a. + Proof using Type. + pose (@PrimeFieldTheorems.F.Decidable_square q _ ltac:(Crypto.Util.Decidable.vm_decide) a); Crypto.Util.Decidable.vm_decide. Qed. Lemma nonsquare_d : forall x : Fq, (x * x)%F <> d. + Proof using Type. + pose (@PrimeFieldTheorems.F.Decidable_square q _ ltac:(Crypto.Util.Decidable.vm_decide) d); Crypto.Util.Decidable.vm_decide. Qed. Let add := E.add(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d). @@ -81,7 +87,7 @@ Section Ed25519. (Eeq:=E.eq) (* TODO: move defn *) (l:=l) (b:=b) (n:=n) (c:=c) (Eenc:=Eenc) (Senc:=Senc) (H:=SHA512). - Proof. + Proof using Type. split; match goal with | |- ?P => match goal with [H:P|-_] => exact H end (* COQBUG: https://coq.inria.fr/bugs/show_bug.cgi?id=5366 *) |