From 2a321d84d1eceffbe35538c6f7fff2974e034e50 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 22 Feb 2017 14:11:41 -0500 Subject: use [positive] for [F] modulus, char_ge_C instead of char_gt_C --- src/ModularArithmetic/ModularArithmeticTheorems.v | 54 +++--- .../ModularBaseSystemListProofs.v | 8 +- src/ModularArithmetic/ModularBaseSystemProofs.v | 6 +- src/ModularArithmetic/PrimeFieldTheorems.v | 56 ++---- .../PseudoMersenneBaseParamProofs.v | 3 +- src/ModularArithmetic/PseudoMersenneBaseParams.v | 6 +- src/ModularArithmetic/Tutorial.v | 196 --------------------- 7 files changed, 48 insertions(+), 281 deletions(-) delete mode 100644 src/ModularArithmetic/Tutorial.v (limited to 'src/ModularArithmetic') diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index 262b20e3e..863300dde 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -31,8 +31,15 @@ Module F. Lemma pow_spec {m} a : F.pow a 0%N = 1%F :> F m /\ forall x, F.pow a (1 + x)%N = F.mul a (F.pow a x). Proof. change (@F.pow m) with (proj1_sig (@F.pow_with_spec m)); destruct (@F.pow_with_spec m); eauto. Qed. + Global Instance char_gt {m} : + @Ring.char_ge + (F m) Logic.eq F.zero F.one F.opp F.add F.sub F.mul + m. + Proof. + Admitted. + Section FandZ. - Context {m:Z}. + Context {m:positive}. Local Open Scope F_scope. Theorem eq_to_Z_iff (x y : F m) : x = y <-> F.to_Z x = F.to_Z y. @@ -145,34 +152,33 @@ Module F. Local Infix "mod" := modulo : nat_scope. Local Open Scope nat_scope. - Context {m} (m_pos: (0 < m)%Z). - Let to_nat_m_nonzero : Z.to_nat m <> 0. - rewrite Z2Nat.inj_lt in m_pos; omega. - Qed. + Context {m:BinPos.positive}. Lemma to_nat_of_nat (n:nat) : F.to_nat (F.of_nat m n) = (n mod (Z.to_nat m))%nat. Proof. unfold F.to_nat, F.of_nat. rewrite F.to_Z_of_Z. - pose proof (mod_Zmod n (Z.to_nat m) to_nat_m_nonzero) as Hmod. - rewrite Z2Nat.id in Hmod by omega. + assert (Pos.to_nat m <> 0)%nat as HA by (pose proof Pos2Nat.is_pos m; omega). + pose proof (mod_Zmod n (Pos.to_nat m) HA) as Hmod. + rewrite positive_nat_Z in Hmod. rewrite <- Hmod. - rewrite <-Nat2Z.id by omega. - reflexivity. + rewrite <-Nat2Z.id, Z2Nat.inj_pos; omega. Qed. Lemma of_nat_to_nat x : F.of_nat m (F.to_nat x) = x. unfold F.to_nat, F.of_nat. - rewrite Z2Nat.id; [ eapply F.of_Z_to_Z | eapply F.to_Z_range; trivial]. + rewrite Z2Nat.id; [ eapply F.of_Z_to_Z | eapply F.to_Z_range; reflexivity]. Qed. + Lemma Pos_to_nat_nonzero p : Pos.to_nat p <> 0%nat. + Admitted. + Lemma of_nat_mod (n:nat) : F.of_nat m (n mod (Z.to_nat m)) = F.of_nat m n. Proof. unfold F.of_nat. - replace (Z.of_nat (n mod Z.to_nat m)) with(Z.of_nat n mod Z.of_nat (Z.to_nat m))%Z - by (symmetry; eapply (mod_Zmod n (Z.to_nat m) to_nat_m_nonzero)). - rewrite Z2Nat.id by omega. - rewrite <-F.of_Z_mod; reflexivity. + rewrite (F.of_Z_mod (Z.of_nat n)), ?mod_Zmod, ?Z2Nat.id; [reflexivity|..]. + { apply Pos2Z.is_nonneg. } + { rewrite Z2Nat.inj_pos. apply Pos_to_nat_nonzero. } Qed. Lemma to_nat_mod (x:F m) (Hm:(0 < m)%Z) : F.to_nat x mod (Z.to_nat m) = F.to_nat x. @@ -192,7 +198,7 @@ Module F. End FandNat. Section RingTacticGadgets. - Context (m:Z). + Context (m:positive). Definition ring_theory : ring_theory 0%F 1%F (@F.add m) (@F.mul m) (@F.sub m) (@F.opp m) eq := Algebra.Ring.ring_theory_for_stdlib_tactic. @@ -252,22 +258,8 @@ Module F. Ltac is_constant t := match t with F.of_Z _ ?x => x | _ => NotConstant end. Ltac is_pow_constant t := Ncst t. - Module Type Modulus. Parameter modulus : Z. End Modulus. - - (* Example of how to instantiate the ring tactic *) - Module RingModulo (Export M : Modulus). - Add Ring _theory : (ring_theory modulus) - (morphism (ring_morph modulus), - constants [is_constant], - div (morph_div_theory modulus), - power_tac (power_theory modulus) [is_pow_constant]). - - Example ring_modulo_example : forall x y z, x*z + z*y = z*(x+y). - Proof. intros. ring. Qed. - End RingModulo. - Section VariousModulo. - Context {m:Z}. + Context {m:positive}. Local Open Scope F_scope. Add Ring _theory : (ring_theory m) @@ -284,7 +276,7 @@ Module F. End VariousModulo. Section Pow. - Context {m:Z}. + Context {m:positive}. Add Ring _theory' : (ring_theory m) (morphism (ring_morph m), constants [is_constant], diff --git a/src/ModularArithmetic/ModularBaseSystemListProofs.v b/src/ModularArithmetic/ModularBaseSystemListProofs.v index fd9483182..428239498 100644 --- a/src/ModularArithmetic/ModularBaseSystemListProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemListProofs.v @@ -164,7 +164,7 @@ Section ModulusDigitsProofs. rewrite encodeZ_spec by eauto using limb_widths_nonnil, limb_widths_good. apply Z.mod_small. cbv [upper_bound]. fold k. - assert (modulus = 2 ^ k - c) by (cbv [c]; ring). + assert (Z.pos modulus = 2 ^ k - c) by (cbv [c]; ring). omega. Qed. @@ -182,7 +182,7 @@ Section ModulusDigitsProofs. | |- _ => progress autorewrite with Ztestbit | |- _ => unique pose proof c_pos | |- _ => unique pose proof modulus_pos - | |- _ => unique assert (modulus = 2 ^ k - c) by (cbv [c]; ring) + | |- _ => unique assert (Z.pos modulus = 2 ^ k - c) by (cbv [c]; ring) | |- _ => break_if | |- _ => rewrite decode_modulus_digits | |- _ => rewrite Z.testbit_pow2_mod @@ -196,7 +196,7 @@ Section ModulusDigitsProofs. specialize_by (eauto || omega); rewrite sum_firstn_succ_default in *; split; zero_bounds; eauto) | |- Z.pow2_mod _ _ = Z.ones _ => apply Z.bits_inj' - | |- Z.testbit modulus ?i = true => transitivity (Z.testbit (2 ^ k - c) i) + | |- Z.testbit (Z.pos modulus) ?i = true => transitivity (Z.testbit (2 ^ k - c) i) | |- _ => congruence end. @@ -496,7 +496,7 @@ Section ConditionalSubtractModulusProofs. specialize_by auto. cbv [upper_bound] in *. fold k in *. - assert (modulus = 2 ^ k - c) by (cbv [c]; ring). + assert (Z.pos modulus = 2 ^ k - c) by (cbv [c]; ring). destruct (Z_le_dec modulus (BaseSystem.decode base u)). + split; try omega. apply Z.lt_le_trans with (m := 2 ^ k); try omega. diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 3b0231191..34a331fa1 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -30,12 +30,12 @@ Class CarryChain (limb_widths : list Z) := carry_chain_valid : forall i, In i carry_chain -> (i < length limb_widths)%nat }. - Class SubtractionCoefficient {m : Z} {prm : PseudoMersenneBaseParams m} := { + Class SubtractionCoefficient {m : positive} {prm : PseudoMersenneBaseParams m} := { coeff : tuple Z (length limb_widths); coeff_mod: decode coeff = 0%F }. - Class ExponentiationChain {m : Z} {prm : PseudoMersenneBaseParams m} (exp : Z) := { + Class ExponentiationChain {m : positive} {prm : PseudoMersenneBaseParams m} (exp : Z) := { chain : list (nat * nat); chain_correct : fold_chain 0%N N.add chain (1%N :: nil) = Z.to_N exp }. @@ -85,7 +85,7 @@ Section FieldOperationProofs. + apply F.of_Z_to_Z. + apply bv. + rewrite <-F.mod_to_Z. - match goal with |- appcontext [?a mod modulus] => + match goal with |- appcontext [?a mod (Z.pos modulus)] => pose proof (Z.mod_pos_bound a modulus modulus_pos) end. pose proof lt_modulus_2k. omega. diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index abc30056f..6f2970814 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -15,10 +15,11 @@ Require Export Crypto.Util.FixCoqMistakes. Require Crypto.Algebra Crypto.Algebra.Field. Existing Class prime. +Local Open Scope F_scope. Module F. Section Field. - Context (q:Z) {prime_q:prime q}. + Context (q:positive) {prime_q:prime q}. Lemma inv_spec : F.inv 0%F = (0%F : F q) /\ (prime q -> forall x : F q, x <> 0%F -> (F.inv x * x)%F = 1%F). Proof. change (@F.inv q) with (proj1_sig (@F.inv_with_spec q)); destruct (@F.inv_with_spec q); eauto. Qed. @@ -37,33 +38,10 @@ Module F. | _ => split end. Qed. - - Definition field_theory : field_theory 0%F 1%F F.add F.mul F.sub F.opp F.div F.inv eq - := Algebra.Field.field_theory_for_stdlib_tactic. End Field. - (** A field tactic hook that can be imported *) - Module Type PrimeModulus. - Parameter modulus : Z. - Parameter prime_modulus : prime modulus. - End PrimeModulus. - Module FieldModulo (Export M : PrimeModulus). - Module Import RingM := F.RingModulo M. - Add Field _field : (F.field_theory modulus) - (morphism (F.ring_morph modulus), - constants [F.is_constant], - div (F.morph_div_theory modulus), - power_tac (F.power_theory modulus) [F.is_pow_constant]). - End FieldModulo. - Section NumberThoery. - Context {q:Z} {prime_q:prime q} {two_lt_q: 2 < q}. - Local Open Scope F_scope. - Add Field _field : (field_theory q) - (morphism (F.ring_morph q), - constants [F.is_constant], - div (F.morph_div_theory q), - power_tac (F.power_theory q) [F.is_pow_constant]). + Context {q:positive} {prime_q:prime q} {two_lt_q: 2 < q}. (* TODO: move to PrimeFieldTheorems *) Lemma to_Z_1 : @F.to_Z q 1 = 1%Z. @@ -91,16 +69,15 @@ Module F. Global Instance Decidable_square (x:F q) : Decidable (exists y, y*y = x). Proof. destruct (dec (x = 0)). - { left. abstract (exists 0; subst; ring). } + { left. abstract (exists 0; subst; apply Ring.mul_0_l). } { eapply Decidable_iff_to_impl; [eapply euler_criterion; assumption | exact _]. } Defined. End NumberThoery. Section SquareRootsPrime3Mod4. - Context {q:Z} {prime_q: prime q} {q_3mod4 : q mod 4 = 3}. + Context {q:positive} {prime_q: prime q} {q_3mod4 : q mod 4 = 3}. - Local Open Scope F_scope. - Add Field _field2 : (field_theory q) + Add Field _field2 : (Algebra.Field.field_theory_for_stdlib_tactic(T:=F q)) (morphism (F.ring_morph q), constants [F.is_constant], div (F.morph_div_theory q), @@ -114,15 +91,13 @@ Module F. Lemma two_lt_q_3mod4 : 2 < q. Proof. pose proof (prime_ge_2 q _) as two_le_q. - apply Zle_lt_or_eq in two_le_q. - destruct two_le_q; auto. - subst_max. - discriminate. + destruct (Zle_lt_or_eq _ _ two_le_q) as [H|H]; [exact H|]. + rewrite <-H in q_3mod4; discriminate. Qed. Local Hint Resolve two_lt_q_3mod4. - Lemma sqrt_3mod4_correct : forall x, - ((exists y, y*y = x) <-> (sqrt_3mod4 x)*(sqrt_3mod4 x) = x). + Lemma sqrt_3mod4_correct (x:F q) : + ((exists y, y*y = x) <-> (sqrt_3mod4 x)*(sqrt_3mod4 x) = x)%F. Proof. cbv [sqrt_3mod4]; intros. destruct (F.eq_dec x 0); @@ -148,10 +123,9 @@ Module F. End SquareRootsPrime3Mod4. Section SquareRootsPrime5Mod8. - Context {q:Z} {prime_q: prime q} {q_5mod8 : q mod 8 = 5}. - + Context {q:positive} {prime_q: prime q} {q_5mod8 : q mod 8 = 5}. Local Open Scope F_scope. - Add Field _field3 : (field_theory q) + Add Field _field3 : (Algebra.Field.field_theory_for_stdlib_tactic(T:=F q)) (morphism (F.ring_morph q), constants [F.is_constant], div (F.morph_div_theory q), @@ -164,10 +138,8 @@ Module F. Lemma two_lt_q_5mod8 : 2 < q. Proof. pose proof (prime_ge_2 q _) as two_le_q. - apply Zle_lt_or_eq in two_le_q. - destruct two_le_q; auto. - subst_max. - discriminate. + destruct (Zle_lt_or_eq _ _ two_le_q) as [H|H]; [exact H|]. + rewrite <-H in *. discriminate. Qed. Local Hint Resolve two_lt_q_5mod8. diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v index 630fc102e..3a530c377 100644 --- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v +++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v @@ -33,7 +33,7 @@ Section PseudoMersenneBaseParamProofs. pose proof (NumTheoryUtil.lt_1_p _ prime_modulus); omega. Qed. Hint Resolve modulus_pos. - Lemma modulus_nonzero : modulus <> 0. + Lemma modulus_nonzero : Z.pos modulus <> 0. pose proof (Znumtheory.prime_ge_2 _ prime_modulus); omega. Qed. @@ -45,7 +45,6 @@ Section PseudoMersenneBaseParamProofs. rewrite Z.mul_add_distr_r, Zplus_mod. unfold c. rewrite Z.sub_sub_distr, Z.sub_diag. - simpl. rewrite Z.mul_comm, Z.mod_add_l; auto using modulus_nonzero. rewrite <- Zplus_mod; auto. Qed. diff --git a/src/ModularArithmetic/PseudoMersenneBaseParams.v b/src/ModularArithmetic/PseudoMersenneBaseParams.v index b564bcb05..6f6fd6556 100644 --- a/src/ModularArithmetic/PseudoMersenneBaseParams.v +++ b/src/ModularArithmetic/PseudoMersenneBaseParams.v @@ -4,16 +4,16 @@ Require Import Crypto.Util.ListUtil. Require Crypto.BaseSystem. Local Open Scope Z_scope. -Class PseudoMersenneBaseParams (modulus : Z) := { +Class PseudoMersenneBaseParams (modulus : positive) := { limb_widths : list Z; limb_widths_pos : forall w, In w limb_widths -> 0 < w; limb_widths_nonnil : limb_widths <> nil; limb_widths_good : forall i j, (i + j < length limb_widths)%nat -> sum_firstn limb_widths (i + j) <= sum_firstn limb_widths i + sum_firstn limb_widths j; - prime_modulus : Znumtheory.prime modulus; + prime_modulus : Znumtheory.prime (Z.pos modulus); k := sum_firstn limb_widths (length limb_widths); - c := 2 ^ k - modulus; + c := 2 ^ k - (Z.pos modulus); c_pos : 0 < c; limb_widths_match_modulus : forall i j, (i < length limb_widths)%nat -> diff --git a/src/ModularArithmetic/Tutorial.v b/src/ModularArithmetic/Tutorial.v deleted file mode 100644 index 4ec1ed82c..000000000 --- a/src/ModularArithmetic/Tutorial.v +++ /dev/null @@ -1,196 +0,0 @@ -Require Import Coq.ZArith.BinInt Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. -Require Import Crypto.Spec.ModularArithmetic Crypto.ModularArithmetic.PrimeFieldTheorems. - - -(* Example for modular arithmetic with a concrete modulus in a section *) -Section Mod24. - (* Set notations + - * / refer to F operations *) - Local Open Scope F_scope. - - (* Specify modulus *) - Let q := 24. - - (* Boilerplate for letting Z numbers be interpreted as field elements *) - Let ZToFq := F.of_Z _ : BinNums.Z -> F q. Hint Unfold ZToFq. - Local Coercion ZToFq : Z >-> F. - Local Coercion F.to_Z : F >-> Z. - - (* Boilerplate for [ring]. Similar boilerplate works for [field] if - the modulus is prime . *) - Add Ring _theory : (F.ring_theory q) - (morphism (F.ring_morph q), - preprocess [unfold ZToFq], - constants [F.is_constant], - div (F.morph_div_theory q), - power_tac (F.power_theory q) [F.is_pow_constant]). - - Lemma sumOfSquares : forall a b: F q, (a+b)^2 = a^2 + 2*a*b + b^2. - Proof. - intros. - ring. - Qed. -End Mod24. - -(* Example for modular arithmetic with an abstract modulus in a section *) -Section Modq. - Context {q:Z} {prime_q:prime q}. - Existing Instance prime_q. - - (* Set notations + - * / refer to F operations *) - Local Open Scope F_scope. - - (* Boilerplate for letting Z numbers be interpreted as field elements *) - Let ZToFq := F.of_Z _ : BinNums.Z -> F q. Hint Unfold ZToFq. - Local Coercion ZToFq : Z >-> F. - Local Coercion F.to_Z : F >-> Z. - - (* Boilerplate for [field]. Similar boilerplate works for [ring] if - the modulus is not prime . *) - Add Field _theory' : (F.field_theory q) - (morphism (F.ring_morph q), - preprocess [unfold ZToFq], - constants [F.is_constant], - div (F.morph_div_theory q), - power_tac (F.power_theory q) [F.is_pow_constant]). - - Lemma sumOfSquares' : forall a b c: F q, c <> 0 -> ((a+b)/c)^2 = a^2/c^2 + 2*(a/c)*(b/c) + b^2/c^2. - Proof. - intros. - field; trivial. - Qed. -End Modq. - -(*** The old way: Modules ***) - -Module Modulus31 <: F.PrimeModulus. - Definition modulus := 2^5 - 1. - Lemma prime_modulus : prime modulus. - Admitted. -End Modulus31. - -Module Modulus127 <: F.PrimeModulus. - Definition modulus := 2^127 - 1. - Lemma prime_modulus : prime modulus. - Admitted. -End Modulus127. - -Module Example31. - (* Then we can construct a field with that modulus *) - Module Import Field := F.FieldModulo Modulus31. - Import Modulus31. - - (* And pull in the appropriate notations *) - Local Open Scope F_scope. - - (* First, let's solve a ring example*) - Lemma ring_example: forall x: F modulus, x * (F.of_Z _ 2) = x + x. - Proof. - intros. - ring. - Qed. - - (* Unfortunately, the [ring] and [field] tactics need syntactic - (not definitional) equality to recognize the ring in question. - Therefore, it is necessary to explicitly rewrite the modulus - (usually hidden by implicitn arguments) match the one passed to - [FieldModulo]. *) - Lemma ring_example': forall x: F (2^5-1), x * (F.of_Z _ 2) = x + x. - Proof. - intros. - change (2^5-1)%Z with modulus. - ring. - Qed. - - (* Then a field example (we have to know we can't divide by zero!) *) - Lemma field_example: forall x y z: F modulus, z <> 0 -> - x * (y / z) / z = x * y / (z ^ 2). - Proof. - intros; simpl. - field; trivial. - Qed. - - (* Then an example with exponentiation *) - Lemma exp_example: forall x: F modulus, x ^ 2 + F.of_Z _ 2 * x + 1 = (x + 1) ^ 2. - Proof. - intros; simpl. - field; trivial. - Qed. - - (* In general, the rule I've been using is: - - - If our goal looks like x = y: - - + If we need to use assumptions to prove the goal, then before - we apply field, - - * Perform all relevant substitutions (especially subst) - - * If we have something more complex, we're probably going - to have to performe some sequence of "replace X with Y" - and solve out the subgoals manually before we can use - field. - - + Else, just use field directly - - - If we just want to simplify terms and put them into a canonical - form, then field_simplify or ring_simplify should do the trick. - Note, however, that the canonical form has lots of annoying "/1"s - - - Otherwise, do a "replace X with Y" to generate an equality - so that we can use field in the above case - - *) - -End Example31. - -(* Notice that the field tactics work whether we know what the modulus is *) -Module TimesZeroTransparentTestModule. - Module Import Theory := F.FieldModulo Modulus127. - Import Modulus127. - Local Open Scope F_scope. - - Lemma timesZero : forall a : F modulus, a*0 = 0. - intros. - field. - Qed. -End TimesZeroTransparentTestModule. - -(* An opaque modulus causes the field tactic to expand all constants - into matches on the modulus. Goals can still be proven, but with - significant overhead. Consider using an entirely abstract - [Algebra.field] instead. *) - -Module TimesZeroParametricTestModule (M: F.PrimeModulus). - Module Theory := F.FieldModulo M. - Import Theory M. - Local Open Scope F_scope. - - Lemma timesZero : forall a : F modulus, a*0 = 0. - intros. - field. - Qed. - - Lemma realisticFraction : forall x y d : F modulus, 1 <> F.of_Z modulus 0 -> (x * 1 + y * 0) / (1 + d * x * 0 * y * 1) = x. - Proof. - intros. - field; assumption. - Qed. - - Lemma biggerFraction : forall XP YP ZP TP XQ YQ ZQ TQ d : F modulus, - 1 <> F.of_Z modulus 0 -> - ZQ <> 0 -> - ZP <> 0 -> - ZP * ZQ * ZP * ZQ + d * XP * XQ * YP * YQ <> 0 -> - ZP * F.of_Z _ 2 * ZQ * (ZP * ZQ) + XP * YP * F.of_Z _ 2 * d * (XQ * YQ) <> 0 -> - ZP * F.of_Z _ 2 * ZQ * (ZP * ZQ) - XP * YP * F.of_Z _ 2 * d * (XQ * YQ) <> 0 -> - - ((YP + XP) * (YQ + XQ) - (YP - XP) * (YQ - XQ)) * - (ZP * F.of_Z _ 2 * ZQ - XP * YP / ZP * F.of_Z _ 2 * d * (XQ * YQ / ZQ)) / - ((ZP * F.of_Z _ 2 * ZQ - XP * YP / ZP * F.of_Z _ 2 * d * (XQ * YQ / ZQ)) * - (ZP * F.of_Z _ 2 * ZQ + XP * YP / ZP * F.of_Z _ 2 * d * (XQ * YQ / ZQ))) = - (XP / ZP * (YQ / ZQ) + YP / ZP * (XQ / ZQ)) / (1 + d * (XP / ZP) * (XQ / ZQ) * (YP / ZP) * (YQ / ZQ)). - Proof. - intros. - field; repeat split; assumption. - Qed. -End TimesZeroParametricTestModule. -- cgit v1.2.3