diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-07-28 18:40:28 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-08-04 11:47:51 -0400 |
| commit | 4964f1ff2d40ba08573deddca56140c4ac4b19eb (patch) | |
| tree | 61b24623e414dfa3e09a32cf62e8acd1909dae37 /src/CompleteEdwardsCurve/Pre.v | |
| parent | fbb0f64892560322ed9dcd0f664e730e74de9b4e (diff) | |
Refactor ModularArithmetic into Zmod, expand Decidable
ModularArithmetic now uses Algebra lemmas in various places instead of
custom manual proofs. Similarly, Util.Decidable is used to state and
prove the relevant decidability results.
Backwards-incompatible changes:
F_some_lemma -> Zmod.some_lemma
Arguments ZToField _%Z _%Z : clear implicits.
inv_spec says inv x * x = 1, not x * inv x = 1
Diffstat (limited to 'src/CompleteEdwardsCurve/Pre.v')
| -rw-r--r-- | src/CompleteEdwardsCurve/Pre.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index 76dd97c72..705597e15 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -1,6 +1,6 @@ Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid. Require Import Crypto.Algebra Crypto.Algebra. -Require Import Crypto.Util.Notations. +Require Import Crypto.Util.Notations Crypto.Util.Decidable. Generalizable All Variables. Section Pre. @@ -44,7 +44,7 @@ Section Pre. (d*x1*x2*y1*y2)^2 <> 1. Proof. unfold onCurve, not; use_sqrt_a; intros. - destruct (eq_dec (sqrt_a*x2 + y2) 0); destruct (eq_dec (sqrt_a*x2 - y2) 0); + destruct (dec ((sqrt_a*x2 + y2) = 0)); destruct (dec ((sqrt_a*x2 - y2) = 0)); lazymatch goal with | [H: not (eq (?f (sqrt_a * x2) y2) 0) |- _ ] => apply d_nonsquare with (sqrt_d:= (f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1)) |