ExtendedCoordinates: group.

2 files changed, 20 insertions, 6 deletions

diff --git a/src/Algebra.v b/src/Algebra.v
index a46b010b5..ecc5e4209 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -292,9 +292,9 @@ Module Group.
           {Proper_inv:Proper(eq==>eq)inv}
           {phi iph} {Proper_phi:Proper(EQ==>eq)phi} {Proper_iph:Proper(eq==>EQ)iph}
           {surj:forall h, phi (iph h) = h}
-          {phi_op : forall a b, phi (OP a b) = op (phi a) (phi b)}
-          {phi_inv : forall a, phi (INV a) = inv (phi a)}
-          {phi_id : phi ID = id}
+          {phi_op : forall a b, eq (phi (OP a b)) (op (phi a) (phi b))}
+          {phi_inv : forall a, eq (phi (INV a)) (inv (phi a))}
+          {phi_id : eq (phi ID) id}
           : @group H eq op id inv.
     Proof.
       repeat split; eauto with core typeclass_instances; intros;
@@ -318,9 +318,9 @@ Module Group.
           {H eq op id inv} {groupG:@group H eq op id inv}
           {phi}
           {eq_phi_EQ: forall x y, eq (phi x) (phi y) -> EQ x y}
-          {phi_op : forall a b, phi (OP a b) = op (phi a) (phi b)}
-          {phi_inv : forall a, phi (INV a) = inv (phi a)}
-          {phi_id : phi ID = id}
+          {phi_op : forall a b, eq (phi (OP a b)) (op (phi a) (phi b))}
+          {phi_inv : forall a, eq (phi (INV a)) (inv (phi a))}
+          {phi_id : eq (phi ID) id}
           : @group G EQ OP ID INV.
     Proof.
       repeat split; eauto with core typeclass_instances; intros;
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.