diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-07-20 15:35:01 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-07-20 18:53:43 -0400 |
| commit | a5caf332df39f57bf25829cf5c127aa54fb8d3e4 (patch) | |
| tree | 35fa8d69124edec7ae0c7ae42ffb930f491f780a /src/Experiments | |
| parent | 476f078855a221a2ec47a63e7efdceaa35acd488 (diff) | |
experiments wd25519: simplify proof for a
Diffstat (limited to 'src/Experiments')
| -rw-r--r-- | src/Experiments/SpecEd25519.v | 11 |
1 files changed, 1 insertions, 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. |