diff options
author | Andres Erbsen <andreser@mit.edu> | 2017-06-14 00:36:23 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2017-06-14 13:05:52 -0400 |
commit | 53d6e0a991ce110864b2293eb25feca4042186eb (patch) | |
tree | 5a63e122cd2444aa12531f5f7a3bef159c7cca69 /src/Arithmetic | |
parent | 362eaa5da1f291b86aa04e8d745738a647ee34ce (diff) |
ScalarMult: Z -> G -> G (closes #193)
Diffstat (limited to 'src/Arithmetic')
-rw-r--r-- | src/Arithmetic/ModularArithmeticTheorems.v | 74 | ||||
-rw-r--r-- | src/Arithmetic/PrimeFieldTheorems.v | 6 |
2 files changed, 46 insertions, 34 deletions
diff --git a/src/Arithmetic/ModularArithmeticTheorems.v b/src/Arithmetic/ModularArithmeticTheorems.v index 77186674f..88f25ec60 100644 --- a/src/Arithmetic/ModularArithmeticTheorems.v +++ b/src/Arithmetic/ModularArithmeticTheorems.v @@ -6,7 +6,7 @@ Require Import Coq.ZArith.BinInt Coq.ZArith.Zdiv Coq.ZArith.Znumtheory Coq.NArit Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid. Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Ring_tac. -Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Ring Crypto.Algebra.Field. +Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.ScalarMult Crypto.Algebra.Ring Crypto.Algebra.Field. Require Import Crypto.Util.Decidable Crypto.Util.ZUtil. Require Export Crypto.Util.FixCoqMistakes. @@ -184,7 +184,6 @@ Module F. Lemma to_nat_mod (x:F m) (Hm:(0 < m)%Z) : F.to_nat x mod (Z.to_nat m) = F.to_nat x. Proof using Type. - unfold F.to_nat. rewrite <-F.mod_to_Z at 2. apply Z.mod_to_nat; [assumption|]. @@ -287,17 +286,6 @@ Module F. power_tac (power_theory m) [is_pow_constant]). Local Open Scope F_scope. - Import Algebra.ScalarMult. - Global Instance pow_is_scalarmult - : is_scalarmult (G:=F m) (eq:=eq) (add:=F.mul) (zero:=1%F) (mul := fun n x => x ^ (N.of_nat n)). - Proof using Type. - split; [ intro P | intros n P | ]; rewrite ?Nat2N.inj_succ, <-?N.add_1_l; - match goal with - | [x:F m |- _ ] => solve [destruct (@pow_spec m P); auto] - | |- Proper _ _ => solve_proper - end. - Qed. - (* TODO: move this somewhere? *) Create HintDb nat2N discriminated. Hint Rewrite Nat2N.inj_iff @@ -311,36 +299,60 @@ Module F. Nat2N.inj_div2 Nat2N.inj_max Nat2N.inj_min Nat2N.id : nat2N. - Ltac pow_to_scalarmult_ref := - repeat (autorewrite with nat2N; - match goal with - | |- context [ (_^?n)%F ] => - rewrite <-(N2Nat.id n); generalize (N.to_nat n); clear n; - intro n - | |- context [ (_^N.of_nat ?n)%F ] => - let rw := constr:(scalarmult_ext(zero:=F.of_Z m 1) n) in - setoid_rewrite rw (* rewriting moduloa reduction *) - end). - Lemma pow_0_r (x:F m) : x^0 = 1. - Proof using Type. pow_to_scalarmult_ref. apply scalarmult_0_l. Qed. + Proof using Type. destruct (F.pow_spec x); auto. Qed. + + Lemma pow_succ_r (x:F m) n : x^(N.succ n) = x * x^n. + Proof using Type. + rewrite <-N.add_1_l; + destruct (F.pow_spec x); auto. + Qed. Lemma pow_add_r (x:F m) (a b:N) : x^(a+b) = x^a * x^b. - Proof using Type. pow_to_scalarmult_ref; apply scalarmult_add_l. Qed. + Proof using Type. + destruct (F.pow_spec x) as [A B]. + induction a as [|a IHa] using N.peano_ind; + rewrite ?N.add_succ_l, ?pow_0_r, ?pow_succ_r, ?N.add_0_l, ?IHa; try ring. + Qed. Lemma pow_0_l (n:N) : n <> 0%N -> 0^n = 0 :> F m. - Proof using Type. pow_to_scalarmult_ref; destruct n; simpl; intros; [congruence|ring]. Qed. + Proof using Type. + induction n as [|a IHa] using N.peano_ind; [contradiction|]. + rewrite <-N.add_1_l, pow_add_r; intros; ring. + Qed. + + Lemma pow_1_l (n:N) : 1^n = 1 :> F m. + Proof using Type. + induction n as [|n IHn] using N.peano_ind; + rewrite ?pow_0_r, ?pow_succ_r, ?pow_add_r, ?pow_1_l, ?IHn; ring. + Qed. + + Lemma pow_mul_l (x y:F m) (n:N) : (x*y)^n = x^n * y^n. + Proof using Type. + induction n as [|n IHn] using N.peano_ind; + repeat (rewrite ?pow_0_r, ?pow_succ_r, ?pow_1_l, <-?N.add_1_l, ?N.mul_add_distr_r, ?pow_add_r, ?N.mul_1_l, ?IHn); try ring. + Qed. Lemma pow_pow_l (x:F m) (a b:N) : (x^a)^b = x^(a*b). - Proof using Type. pow_to_scalarmult_ref. apply scalarmult_assoc. Qed. + Proof using Type. + induction a as [|a IHa] using N.peano_ind; + repeat (rewrite ?pow_0_r, ?pow_succ_r, ?pow_1_l, <-?N.add_1_l, ?N.mul_add_distr_r, ?pow_add_r, ?N.mul_1_l, ?pow_mul_l, ?IHa); + try ring. + Qed. Lemma pow_1_r (x:F m) : x^1 = x. - Proof using Type. pow_to_scalarmult_ref; simpl; ring. Qed. + Proof using Type. + change 1%N with (N.succ 0); repeat rewrite ?pow_succ_r, ?pow_0_r; ring. + Qed. Lemma pow_2_r (x:F m) : x^2 = x*x. - Proof using Type. pow_to_scalarmult_ref; simpl; ring. Qed. + Proof using Type. + change 1%N with (N.succ (N.succ 0)); repeat rewrite ?pow_succ_r, ?pow_0_r; ring. + Qed. Lemma pow_3_r (x:F m) : x^3 = x*x*x. - Proof using Type. pow_to_scalarmult_ref; simpl; ring. Qed. + Proof using Type. + change 1%N with (N.succ (N.succ (N.succ 0))); repeat rewrite ?pow_succ_r, ?pow_0_r; ring. + Qed. End Pow. End F. diff --git a/src/Arithmetic/PrimeFieldTheorems.v b/src/Arithmetic/PrimeFieldTheorems.v index 3d6260bba..2184d20c6 100644 --- a/src/Arithmetic/PrimeFieldTheorems.v +++ b/src/Arithmetic/PrimeFieldTheorems.v @@ -251,9 +251,8 @@ Module F. {phi'_opp : forall a : H, Logic.eq (phi' (opp a)) (F.opp (phi' a))} {phi'_add : forall a b : H, Logic.eq (phi' (add a b)) (F.add (phi' a) (phi' b))} {phi'_sub : forall a b : H, Logic.eq (phi' (sub a b)) (F.sub (phi' a) (phi' b))} - {phi'_mul : forall a b : H, Logic.eq (phi' (mul a b)) (F.mul (phi' a) (phi' b))} - {P:Type} {pow : H -> P -> H} {NtoP:N->P} - {pow_is_scalarmult:ScalarMult.is_scalarmult(G:=H)(eq:=eq)(add:=mul)(zero:=one)(mul:=fun (n:nat) (k:H) => pow k (NtoP (N.of_nat n)))}. + {phi'_mul : forall a b : H, Logic.eq (phi' (mul a b)) (F.mul (phi' a) (phi' b))}. + (* TODO: revive this once we figure out how to spec the pow impl Definition inv (x:H) := pow x (NtoP (Z.to_N (q - 2)%Z)). Definition div x y := mul (inv y) x. @@ -289,6 +288,7 @@ Module F. /\ @Ring.is_homomorphism H eq one add mul (F q) Logic.eq F.one F.add F.mul phi'. Proof using Type*. eapply @Field.field_and_homomorphism_from_redundant_representation; assumption || exact _ || exact inv_proof || exact div_proof. Qed. + *) End IsomorphicRings. End Iso. End F. |