From 53d6e0a991ce110864b2293eb25feca4042186eb Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 14 Jun 2017 00:36:23 -0400 Subject: ScalarMult: Z -> G -> G (closes #193) --- src/Algebra/Group.v | 18 +----- src/Algebra/ScalarMult.v | 164 ++++++++++++++++++++++++++++++++++------------- 2 files changed, 121 insertions(+), 61 deletions(-) (limited to 'src/Algebra') diff --git a/src/Algebra/Group.v b/src/Algebra/Group.v index 01325de3f..76c53bcb1 100644 --- a/src/Algebra/Group.v +++ b/src/Algebra/Group.v @@ -1,5 +1,5 @@ Require Import Coq.Classes.Morphisms Crypto.Util.Relations (*Crypto.Util.Tactics*). -Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Monoid Crypto.Algebra.ScalarMult. +Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Monoid. Section BasicProperties. Context {T eq op id inv} `{@group T eq op id inv}. @@ -86,22 +86,6 @@ Section Homomorphism. apply inv_unique. rewrite <- Monoid.homomorphism, left_inverse, homomorphism_id; reflexivity. Qed. - - Section ScalarMultHomomorphism. - Context {MUL} {MUL_is_scalarmult:@ScalarMult.is_scalarmult G EQ OP ID MUL }. - Context {mul} {mul_is_scalarmult:@ScalarMult.is_scalarmult H eq op id mul }. - Lemma homomorphism_scalarmult n P : phi (MUL n P) = mul n (phi P). - Proof using Type*. eapply ScalarMult.homomorphism_scalarmult, homomorphism_id. Qed. - - Import ScalarMult. - Lemma opp_mul : forall n P, inv (mul n P) = mul n (inv P). - Proof using groupH mul_is_scalarmult. - induction n; intros. - { rewrite !scalarmult_0_l, inv_id; reflexivity. } - { rewrite <-NPeano.Nat.add_1_l, Plus.plus_comm at 1. - rewrite scalarmult_add_l, scalarmult_1_l, inv_op, scalarmult_S_l, cancel_left; eauto. } - Qed. - End ScalarMultHomomorphism. End Homomorphism. Section GroupByIsomorphism. diff --git a/src/Algebra/ScalarMult.v b/src/Algebra/ScalarMult.v index 99c1f6bbf..e81f81c2f 100644 --- a/src/Algebra/ScalarMult.v +++ b/src/Algebra/ScalarMult.v @@ -1,91 +1,167 @@ +Require Import Coq.ZArith.BinInt Coq.omega.Omega Crypto.Util.ZUtil.Peano. Require Import Coq.Classes.Morphisms. -Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Monoid. - -Module Import ModuloCoq8485. - Import NPeano Nat. - Infix "mod" := modulo. -End ModuloCoq8485. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Group. +Local Open Scope Z_scope. Section ScalarMultProperties. - Context {G eq add zero} `{monoidG:@monoid G eq add zero}. - Context {mul:nat->G->G}. + Context {G eq add zero opp} `{groupG:@group G eq add zero opp}. + Context {mul:Z->G->G}. Local Infix "=" := eq : type_scope. Local Infix "=" := eq. Local Infix "+" := add. Local Infix "*" := mul. Class is_scalarmult := { scalarmult_0_l : forall P, 0 * P = zero; - scalarmult_S_l : forall n P, S n * P = P + n * P; + scalarmult_succ_l_nn : forall n P, 0 <= n -> Z.succ n * P = P + n * P; + scalarmult_pred_l_np : forall n P, n <= 0 -> Z.pred n * P = opp P + n * P; scalarmult_Proper : Proper (Logic.eq==>eq==>eq) mul }. Global Existing Instance scalarmult_Proper. Context `{mul_is_scalarmult:is_scalarmult}. - Fixpoint scalarmult_ref (n:nat) (P:G) {struct n} := - match n with - | O => zero - | S n' => add P (scalarmult_ref n' P) - end. + Lemma scalarmult_succ_l n P : Z.succ n * P = P + n * P. + Proof. + induction n using Z.peano_rect_strong; intros; rewrite ?Z.succ'_succ, ?Z.pred'_pred in * by omega; + repeat (rewrite ?scalarmult_0_l, ?scalarmult_succ_l_nn, ?scalarmult_pred_l_np, ?left_identity, ?right_identity, ?Z.succ_pred, ?Z.pred_succ, ?associative, ?right_inverse, ?left_inverse by omega); reflexivity. + Qed. + + Lemma scalarmult_pred_l n P : Z.pred n * P = opp P + n * P. + induction n using Z.peano_rect_strong; intros; rewrite ?Z.succ'_succ, ?Z.pred'_pred in * by omega; + repeat (rewrite ?scalarmult_0_l, ?scalarmult_succ_l_nn, ?scalarmult_pred_l_np, ?left_identity, ?right_identity, ?Z.succ_pred, ?Z.pred_succ, ?associative, ?right_inverse, ?left_inverse by omega); reflexivity. + Qed. + + Definition scalarmult_ref (n:Z) (P:G) : G := + Z.peano_rect + (fun _ => G) + (zero) + (fun _ => add P) + (fun _ => add (opp P)) + n + . Global Instance Proper_scalarmult_ref : Proper (Logic.eq==>eq==>eq) scalarmult_ref. - Proof using monoidG. - repeat intro; subst. - match goal with [n:nat |- _ ] => induction n; simpl @scalarmult_ref; [reflexivity|] end. - repeat match goal with [H:_ |- _ ] => rewrite H end; reflexivity. + Proof using groupG. + intros n n' H; subst n'; + induction n using Z.peano_rect_strong; + cbv [Proper respectful] in *; + intros; + cbv [scalarmult_ref] in *; break_match; try reflexivity; + rewrite ?Z.peano_rect_succ, ?Z.peano_rect_pred in * by omega; + rewrite IHn by eassumption; + match goal with H : _ = _ |- _ => rewrite H; reflexivity end. + Qed. + + Lemma scalarmult_ext n P : mul n P = scalarmult_ref n P. + Proof using Type*. + revert P. + destruct mul_is_scalarmult. + induction n using Z.peano_rect_strong; intros; + cbv [scalarmult_ref] in *; break_match; + rewrite ?Z.peano_rect_succ, ?Z.peano_rect_pred, ?Z.succ'_succ, ?Z.pred'_pred in *; + try rewrite <-IHn; try match goal with [H:_|-_] => eapply H end; omega. + Qed. + + Lemma scalarmult_1_l P : 1*P = P. + Proof using Type*. + intros. change 1 with (Z.succ 0). + rewrite scalarmult_succ_l, scalarmult_0_l, right_identity; reflexivity. + Qed. + + Lemma scalarmult_opp1_l P : -1*P = opp P. + change (-1) with (Z.pred 0). + rewrite scalarmult_pred_l, scalarmult_0_l, right_identity; reflexivity. + Qed. + + Lemma scalarmult_add_l (n m:Z) (P:G) : ((n + m)%Z * P = n * P + m * P). + Proof using Type*. + revert P. + induction n using Z.peano_rect_strong; intros; rewrite ?Z.succ'_succ, ?Z.pred'_pred in * by omega; + rewrite ?Z.add_0_l, ?Z.add_succ_l, ?Z.add_pred_l; + rewrite ?scalarmult_0_l, ?scalarmult_succ_l, ?scalarmult_pred_l, ?left_identity, <-?associative, <-?IHn; try reflexivity. Qed. - Lemma scalarmult_ext : forall n P, mul n P = scalarmult_ref n P. + Lemma scalarmult_opp_l (n:Z) (P:G) : (-n) * P = opp (n*P). Proof using Type*. - induction n as [|n IHn]; simpl @scalarmult_ref; intros; rewrite <-?IHn; (apply scalarmult_0_l || apply scalarmult_S_l). + revert P. + induction n using Z.peano_rect_strong; intros; rewrite ?Z.succ'_succ, ?Z.pred'_pred in * by omega. + { change (-0) with (0). rewrite !scalarmult_0_l, inv_id; reflexivity. } + { rewrite scalarmult_succ_l_nn, inv_op, <-IHn by omega. + replace (-Z.succ n) with (-n + (- 1))%Z by auto with zarith. + rewrite scalarmult_add_l, scalarmult_opp1_l; reflexivity. } + { rewrite scalarmult_pred_l_np, inv_op, <-IHn, inv_inv by omega. + replace (- Z.pred n) with (-n+1)%Z by auto with zarith. + rewrite scalarmult_add_l, scalarmult_1_l; reflexivity. } Qed. - Lemma scalarmult_1_l : forall P, 1*P = P. - Proof using Type*. intros. rewrite scalarmult_S_l, scalarmult_0_l, right_identity; reflexivity. Qed. + Lemma scalarmult_zero_r (n:Z) : n * zero = zero. + induction n using Z.peano_rect_strong; intros; rewrite ?Z.succ'_succ, ?Z.pred'_pred in * by omega; + rewrite ?scalarmult_0_l, ?scalarmult_succ_l_nn, ?scalarmult_pred_l_np, ?IHn, ?inv_id, ?left_identity by omega; + try reflexivity. + Qed. - Lemma scalarmult_add_l : forall (n m:nat) (P:G), ((n + m)%nat * P = n * P + m * P). + Lemma scalarmult_assoc (n m : Z) P : n * (m * P) = (m * n)%Z * P. Proof using Type*. - induction n as [|n IHn]; intros; - rewrite ?scalarmult_0_l, ?scalarmult_S_l, ?plus_Sn_m, ?plus_O_n, ?scalarmult_S_l, ?left_identity, <-?associative, <-?IHn; reflexivity. + revert P. + induction n using Z.peano_rect_strong; intros; rewrite ?Z.succ'_succ, ?Z.pred'_pred in * by omega. + { rewrite Z.mul_0_r, 2scalarmult_0_l by omega; reflexivity. } + { rewrite scalarmult_succ_l, IHn by omega. + rewrite (Z.mul_comm m (Z.succ n)), Z.mul_succ_l, (Z.mul_comm n m), (Z.add_comm (m*n) m). + rewrite scalarmult_add_l. reflexivity. } + { rewrite scalarmult_pred_l, IHn by omega. + rewrite (Z.mul_comm m (Z.pred n)), Z.mul_pred_l, (Z.mul_comm n m), <-Z.add_opp_l. + rewrite scalarmult_add_l, scalarmult_opp_l. reflexivity. } Qed. - Lemma scalarmult_zero_r : forall m, m * zero = zero. - Proof using Type*. induction m as [|? IHm]; rewrite ?scalarmult_S_l, ?scalarmult_0_l, ?left_identity, ?IHm; try reflexivity. Qed. + Lemma scalarmult_sub_l (a b:Z) (P:G) : (a - b)*P = a*P + opp(b*P). + Proof using Type*. + rewrite <-Z.add_opp_r, scalarmult_add_l, scalarmult_opp_l; reflexivity. + Qed. - Lemma scalarmult_assoc : forall (n m : nat) P, n * (m * P) = (m * n)%nat * P. + Lemma scalarmult_opp_r (n:Z) (P:G) : n*opp P = opp (n * P). Proof using Type*. - induction n as [|n IHn]; intros. - { rewrite <-mult_n_O, !scalarmult_0_l. reflexivity. } - { rewrite scalarmult_S_l, <-mult_n_Sm, <-Plus.plus_comm, scalarmult_add_l. - rewrite IHn. reflexivity. } + revert P. + induction n using Z.peano_rect_strong; intros; rewrite ?Z.succ'_succ, ?Z.pred'_pred in * by omega; + rewrite <-?Z.add_1_l, <-?Z.sub_1_r; + [|rewrite Z.add_comm at 1|rewrite <-Z.add_opp_l; rewrite Z.add_comm at 1]; + repeat (rewrite ?scalarmult_0_l, ?scalarmult_opp_l, ?scalarmult_add_l, ?inv_id, ?inv_op, ?inv_inv, ?IHn, ?scalarmult_1_l); + reflexivity. Qed. Lemma scalarmult_times_order : forall l B, l*B = zero -> forall n, (l * n) * B = zero. Proof using Type*. intros ? ? Hl ?. rewrite <-scalarmult_assoc, Hl, scalarmult_zero_r. reflexivity. Qed. - Lemma scalarmult_mod_order : forall l B, l <> 0%nat -> l*B = zero -> forall n, n mod l * B = n * B. + Lemma scalarmult_mod_order : forall l B, l <> 0 -> l*B = zero -> forall n, n mod l * B = n * B. Proof using Type*. intros l B Hnz Hmod n. - rewrite (NPeano.Nat.div_mod n l Hnz) at 2. + rewrite (Z.div_mod n l Hnz) at 2. rewrite scalarmult_add_l, scalarmult_times_order, left_identity by auto. reflexivity. Qed. + End ScalarMultProperties. Section ScalarMultHomomorphism. - Context {G EQ ADD ZERO} {monoidG:@monoid G EQ ADD ZERO}. - Context {H eq add zero} {monoidH:@monoid H eq add zero}. + Context {G EQ ADD ZERO OPP} {groupG:@group G EQ ADD ZERO OPP}. + Context {H eq add zero opp} {groupH:@group H eq add zero opp}. Local Infix "=" := eq : type_scope. Local Infix "=" := eq : eq_scope. - Context {MUL} {MUL_is_scalarmult:@is_scalarmult G EQ ADD ZERO MUL }. - Context {mul} {mul_is_scalarmult:@is_scalarmult H eq add zero mul }. + Context {MUL} {MUL_is_scalarmult:@is_scalarmult G EQ ADD ZERO OPP MUL}. + Context {mul} {mul_is_scalarmult:@is_scalarmult H eq add zero opp mul}. Context {phi} {homom:@Monoid.is_homomorphism G EQ ADD H eq add phi}. - Context (phi_ZERO:phi ZERO = zero). Lemma homomorphism_scalarmult : forall n P, phi (MUL n P) = mul n (phi P). Proof using Type*. - setoid_rewrite scalarmult_ext. - induction n as [|n IHn]; intros; simpl; rewrite ?Monoid.homomorphism, ?IHn; easy. + induction n using Z.peano_rect_strong; intros; rewrite ?Z.succ'_succ, ?Z.pred'_pred in * by omega; + rewrite ?scalarmult_0_l, ?scalarmult_succ_l, ?scalarmult_pred_l by omega. + { apply homomorphism_id. } + { rewrite <-IHn. rewrite Monoid.homomorphism. reflexivity. } + { rewrite <-IHn. rewrite Monoid.homomorphism, Group.homomorphism_inv. reflexivity. } Qed. End ScalarMultHomomorphism. -Global Instance scalarmult_ref_is_scalarmult {G eq add zero} `{@monoid G eq add zero} - : @is_scalarmult G eq add zero (@scalarmult_ref G add zero). -Proof. split; try exact _; intros; reflexivity. Qed. +Global Instance scalarmult_ref_is_scalarmult {G eq add zero opp} {groupG:@group G eq add zero opp} + : @is_scalarmult G eq add zero opp (@scalarmult_ref G add zero opp). +Proof. + split; try exact _; cbv [scalarmult_ref] in *; intros; + rewrite <-?Z.succ'_succ, <-?Z.pred'_pred, ?Z.peano_rect_succ, ?Z.peano_rect_pred in * by omega; + reflexivity. +Qed. \ No newline at end of file -- cgit v1.2.3