diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-01-05 17:24:44 -0500 |
|---|---|---|
| committer |  Andres Erbsen <andreser@mit.edu> | 2018-01-09 10:09:46 -0500 |
| commit | aa28ca2993cb7f4a7663c9a54a6fa596a46a02ed (patch) | |
| tree | a4ceb58e8e0baa4d485843faccdd8fd4eaefe08c /src/Curves | |
| parent | fd6a2cd64f16da8dfb7d5dec8d892ade0c21c6cb (diff) | |
Replace char_ge_12 with char_ge_3
We no longer seem to need the stronger hypothesis.
Diffstat (limited to 'src/Curves')
| -rw-r--r-- | src/Curves/Weierstrass/Jacobian.v | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/src/Curves/Weierstrass/Jacobian.v b/src/Curves/Weierstrass/Jacobian.v index 323816b81..fcabae005 100644 --- a/src/Curves/Weierstrass/Jacobian.v +++ b/src/Curves/Weierstrass/Jacobian.v @@ -167,7 +167,7 @@ Module Jacobian. let yneq := if dec (r = 0) then false else true in if (negb xneq && negb yneq && z1nz && z2nz)%bool then proj1_sig (double P) - else + else let i := h + h in let i := i^2 in let j := h * i in @@ -208,9 +208,7 @@ Module Jacobian. Lemma Proper_add : Proper (eq ==> eq ==> eq) add. Proof. t. Qed. Import BinPos. - Lemma to_affine_add - {char_ge_12:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12} (* TODO: why do we need 12 instead of 3? *) - P Q + Lemma to_affine_add P Q : W.eq (to_affine (add P Q)) (W.add (to_affine P) (to_affine Q)). Proof. prept; trivial; try contradiction. Time all: abstract t. Time Qed. (* 306.478 secs (43.916u,1.032s) ;; 18.857 secs (18.856u,0.008s) *) |