blob: 3a48bf9982524a09ce5be77e8fdafe5f6c5fb7c4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
Require Import Crypto.Spec.WeierstrassCurve.
Require Import Crypto.Algebra.Field.
Require Import Crypto.Util.Decidable Crypto.Util.Tactics.DestructHead Crypto.Util.Tactics.BreakMatch.
Module W.
Section W.
Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {a b:F}
{field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
{Feq_dec:DecidableRel Feq}.
Program Definition opp (P:@W.point F Feq Fadd Fmul a b) : @W.point F Feq Fadd Fmul a b
:= match W.coordinates P return F*F+_ with
| inl (x1, y1) => inl (x1, Fopp y1)
| inr tt => inr tt
end.
Next Obligation.
cbv [W.coordinates]; break_match; trivial; fsatz.
Qed.
End W.
End W.
|
