diff options
author | Andres Erbsen <andreser@mit.edu> | 2017-02-12 19:16:26 -0500 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2017-03-02 13:37:14 -0500 |
commit | bc46f85d089099aa92d3ea12555e6510cbcffa78 (patch) | |
tree | cac00ea0f50bc3b7ba101181161ab76dbd55e797 | |
parent | e8fab6b839e19da231333ca8173bbb2a3d8a4033 (diff) |
change weierstrass spec, prove most cases of associativity
-rw-r--r-- | src/Algebra/Ring.v | 9 | ||||
-rw-r--r-- | src/Spec/WeierstrassCurve.v | 20 |
2 files changed, 22 insertions, 7 deletions
diff --git a/src/Algebra/Ring.v b/src/Algebra/Ring.v index 2d8061ddc..3752c7562 100644 --- a/src/Algebra/Ring.v +++ b/src/Algebra/Ring.v @@ -60,6 +60,15 @@ Section Ring. eapply Group.cancel_left, mul_opp_l. Qed. + Lemma sub_zero_iff x y : x - y = 0 <-> x = y. + Proof. + split; intro E. + { rewrite <-(right_identity y), <- E, ring_sub_definition. + rewrite commutative, <-associative, commutative. + rewrite left_inverse, left_identity. reflexivity. } + { rewrite E, ring_sub_definition, right_inverse; reflexivity. } + Qed. + Lemma neq_sub_neq_zero x y (Hxy:x<>y) : x-y <> 0. Proof. intro Hsub. apply Hxy. rewrite <-(left_identity y), <-Hsub, ring_sub_definition. diff --git a/src/Spec/WeierstrassCurve.v b/src/Spec/WeierstrassCurve.v index 8b5480620..3f8ab2100 100644 --- a/src/Spec/WeierstrassCurve.v +++ b/src/Spec/WeierstrassCurve.v @@ -48,18 +48,24 @@ Module W. _ (match coordinates P1, coordinates P2 return _ with | (x1, y1), (x2, y2) => - if x1 =? x2 then - if y2 =? -y1 then ∞ - else ((3*x1^2+a)^2 / (2*y1)^2 - x1 - x1, - (2*x1+x1)*(3*x1^2+a) / (2*y1) - (3*x1^2+a)^3/(2*y1)^3-y1) - else ((y2-y1)^2 / (x2-x1)^2 - x1 - x2, - (2*x1+x2)*(y2-y1) / (x2-x1) - (y2-y1)^3 / (x2-x1)^3 - y1) + if x1 =? x2 + then + if y2 =? -y1 + then ∞ + else let k := (3*x1^2+a)/(2*y1) in + let x3 := k^2-x1-x1 in + let y3 := k*(x1-x3)-y1 in + (x3, y3) + else let k := (y2-y1)/(x2-x1) in + let x3 := k^2-x1-x2 in + let y3 := k*(x1-x3)-y1 in + (x3, y3) | ∞, ∞ => ∞ | ∞, _ => coordinates P2 | _, ∞ => coordinates P1 end) _. - Next Obligation. exact (Pre.unifiedAdd'_onCurve _ _ (proj2_sig _) (proj2_sig _)). Qed. + Next Obligation. Admitted. Fixpoint mul (n:nat) (P : point) : point := match n with |