diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-02-21 18:01:18 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-03-02 13:37:14 -0500 |
| commit | f5c6a57c1453249aac448a33ac3443e45a0d3222 (patch) | |
| tree | 72919ee54472c746feab4b51898095ae5caad768 /src/Algebra/Group.v | |
| parent | c1c764ead6291e25f6da3508f1ae2b46c1e574d4 (diff) | |
rewrite ExtendedCoordinates, fix Ed25519
Diffstat (limited to 'src/Algebra/Group.v')
| -rw-r--r-- | src/Algebra/Group.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/Algebra/Group.v b/src/Algebra/Group.v index 7f580380f..c1c514171 100644 --- a/src/Algebra/Group.v +++ b/src/Algebra/Group.v @@ -115,10 +115,11 @@ Section Homomorphism_rev. {phi'_inv : forall a, phi' (inv a) = INV (phi' a)} {phi'_id : phi' id = ID}. - Local Instance group_from_redundant_representation - : @group H eq op id inv. + Lemma group_from_redundant_representation + : @group H eq op id inv /\ @Monoid.is_homomorphism G EQ OP H eq op phi /\ @Monoid.is_homomorphism H eq op G EQ OP phi'. Proof. repeat match goal with + | [ H : _/\_ |- _ ] => destruct H; try clear H | [ H : group |- _ ] => destruct H; try clear H | [ H : monoid |- _ ] => destruct H; try clear H | [ H : is_associative |- _ ] => destruct H; try clear H @@ -132,7 +133,7 @@ Section Homomorphism_rev. | [ H : eq _ _ |- _ ] => apply phi'_eq in H | [ |- eq _ _ ] => apply phi'_eq | [ H : EQ _ _ |- _ ] => rewrite H - | _ => progress erewrite ?phi'_op, ?phi'_inv, ?phi'_id by reflexivity + | _ => progress erewrite ?phi'_op, ?phi'_inv, ?phi'_id, ?phi'_phi_id by reflexivity | [ H : _ |- _ ] => progress erewrite ?phi'_op, ?phi'_inv, ?phi'_id in H by reflexivity | _ => solve [ eauto ] end. |