From a5caf332df39f57bf25829cf5c127aa54fb8d3e4 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 20 Jul 2016 15:35:01 -0400 Subject: experiments wd25519: simplify proof for a --- src/Experiments/SpecEd25519.v | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) diff --git a/src/Experiments/SpecEd25519.v b/src/Experiments/SpecEd25519.v index 30d8ce13d..111aaff0b 100644 --- a/src/Experiments/SpecEd25519.v +++ b/src/Experiments/SpecEd25519.v @@ -18,16 +18,7 @@ Lemma two_lt_q : (2 < q)%Z. reflexivity. Qed. Definition a : F q := opp 1%F. -(* TODO (jadep) : make the proofs about a and d more general *) -Lemma nonzero_a : a <> 0%F. -Proof. - unfold a. - intro eq_opp1_0. - apply (@Fq_1_neq_0 q prime_q). - rewrite <- (F_opp_spec 1%F). - rewrite eq_opp1_0. - symmetry; apply F_add_0_r. -Qed. +Lemma nonzero_a : a <> 0%F. Proof. rewrite F_eq; compute; discriminate. Qed. Ltac q_bound := pose proof two_lt_q; omega. Lemma square_a : isSquare a. -- cgit v1.2.3