From 331fe3fcfb27d87dcfb0585ced3c051f19aaedf2 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 4 Apr 2017 14:35:43 -0400 Subject: 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). --- src/Spec/Ed25519.v | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) (limited to 'src/Spec') 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 *) -- cgit v1.2.3