diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-06-24 18:06:57 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2016-06-24 18:06:57 -0400 |
commit | 61bdcf3de1f506907d62a2a7c32594c1a666d474 (patch) | |
tree | 66e8d5ef7153cc9cd404895c23b20a2d44bbfc55 /src/CompleteEdwardsCurve | |
parent | 7488addb5938b203d1c9402908cc9b440d9573b6 (diff) |
ExtendedCoordinates: group.
Diffstat (limited to 'src/CompleteEdwardsCurve')
-rw-r--r-- | src/CompleteEdwardsCurve/ExtendedCoordinates.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v index deeb795b1..364d7f9ec 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -63,6 +63,8 @@ Module Extended. (let '(X,Y,Z,T) := coordinates P in ((X/Z), (Y/Z))) _. Definition eq (P Q:point) := E.eq (to_twisted P) (to_twisted Q). + Global Instance DecidableRel_eq : Decidable.DecidableRel eq. + Proof. typeclasses eauto. Qed. Local Hint Unfold from_twisted to_twisted eq : bash. @@ -148,6 +150,18 @@ Module Extended. Lemma homomorphism_from_twisted : @Group.is_homomorphism Epoint E.eq E.add point eq add from_twisted. Proof. split; trivial using Proper_from_twisted, add_from_twisted. Qed. + Definition zero : point := from_twisted E.zero. + Definition opp P : point := from_twisted (E.opp (to_twisted P)). + Lemma extended_group : @group point eq add zero opp. + Proof. + eapply @isomorphism_to_subgroup_group; eauto with typeclass_instances core. + - apply DecidableRel_eq. + - unfold opp. repeat intro. match goal with [H:_|-_] => rewrite H; reflexivity end. + - intros. apply to_twisted_add. + - unfold opp; intros; rewrite to_twisted_from_twisted; reflexivity. + - unfold zero; intros; rewrite to_twisted_from_twisted; reflexivity. + Qed. + (* TODO: decide whether we still need those, then port *) (* Lemma unifiedAddM1_0_r : forall P, unifiedAddM1 P (mkExtendedPoint E.zero) === P. |