diff options
author | jadep <jade.philipoom@gmail.com> | 2016-06-27 17:05:53 -0400 |
---|---|---|
committer | jadep <jade.philipoom@gmail.com> | 2016-06-27 17:05:53 -0400 |
commit | e3adf7c5ee29aeff4887367e8aef38a63ebdc7ac (patch) | |
tree | 36ebee2c1f3b9418f06a6053c762b2f42813d942 /src/CompleteEdwardsCurve | |
parent | a5e707be4ea86ecf0ad40fc0f0b1c1029a9b88b0 (diff) | |
parent | 1da660b30f87a161f866deb44717d0ba5c78cd9d (diff) |
Merge branch 'master' of github.mit.edu:plv/fiat-crypto
Diffstat (limited to 'src/CompleteEdwardsCurve')
-rw-r--r-- | src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | 23 |
1 files changed, 6 insertions, 17 deletions
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index e3809bb8a..0afc07c5d 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -138,25 +138,14 @@ Module E. match goal with | |- _ <> 0 => admit end. Admitted. - (* TODO: move to [Group] and [AbelianGroup] as appropriate *) - Lemma mul_0_l : forall P, (0 * P = zero)%E. - Proof. intros; reflexivity. Qed. - Lemma mul_S_l : forall n P, (S n * P = P + n * P)%E. - Proof. intros; reflexivity. Qed. - Lemma mul_add_l : forall (n m:nat) (P:point), ((n + m)%nat * P = n * P + m * P)%E. + Global Instance Proper_mul : Proper (Logic.eq==>eq==>eq) mul. Proof. - induction n; intros; - rewrite ?plus_Sn_m, ?plus_O_n, ?mul_S_l, ?left_identity, <-?associative, <-?IHn; reflexivity. + intros n m Hnm P Q HPQ. rewrite <-Hnm; clear Hnm m. + induction n; simpl; rewrite ?IHn, ?HPQ; reflexivity. Qed. - Lemma mul_assoc : forall (n m : nat) P, (n * (m * P) = (n * m)%nat * P)%E. - Proof. - induction n; intros; [reflexivity|]. - rewrite ?mul_S_l, ?Mult.mult_succ_l, ?mul_add_l, ?IHn, commutative; reflexivity. - Qed. - Lemma mul_zero_r : forall m, (m * E.zero = E.zero)%E. - Proof. induction m; rewrite ?mul_S_l, ?left_identity, ?IHm; try reflexivity. Qed. - Lemma opp_mul : forall n P, (opp (n * P) = n * (opp P))%E. - Admitted. + + Global Instance mul_is_scalarmult : @is_scalarmult point eq add zero mul. + Proof. split; intros; reflexivity || typeclasses eauto. Qed. Section PointCompression. Local Notation "x ^ 2" := (x*x). |