From df93ba9ef9bad76969b7a667d985321890da9d44 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 28 Jul 2016 14:27:42 -0700 Subject: Add instances about congruence modulo After | File Name | Before || Change ---------------------------------------------------------------------------------- 1m44.65s | Total | 1m56.10s || -0m11.44s ---------------------------------------------------------------------------------- 0m32.68s | Specific/GF25519 | 0m34.42s || -0m01.74s 0m07.28s | Specific/GF1305 | 0m08.30s || -0m01.02s 0m03.89s | BaseSystemProofs | 0m04.91s || -0m01.02s 0m03.80s | ModularArithmetic/Tutorial | 0m05.65s || -0m01.85s 0m15.65s | ModularArithmetic/ModularBaseSystemProofs | 0m16.40s || -0m00.74s 0m11.87s | Experiments/SpecEd25519 | 0m12.04s || -0m00.16s 0m04.08s | ModularArithmetic/Pow2BaseProofs | 0m04.81s || -0m00.72s 0m03.22s | ModularArithmetic/ModularBaseSystemOpt | 0m03.37s || -0m00.14s 0m02.44s | Util/ZUtil | 0m02.46s || -0m00.02s 0m02.31s | Encoding/PointEncodingPre | 0m02.32s || -0m00.00s 0m01.56s | ModularArithmetic/PrimeFieldTheorems | 0m01.88s || -0m00.31s 0m01.55s | ModularArithmetic/ModularArithmeticTheorems | 0m02.30s || -0m00.74s 0m01.20s | BaseSystem | 0m01.86s || -0m00.66s 0m01.15s | Experiments/DerivationsOptionRectLetInEncoding | 0m01.07s || +0m00.07s 0m01.08s | ModularArithmetic/ExtendedBaseVector | 0m01.23s || -0m00.14s 0m00.95s | ModularArithmetic/BarrettReduction/Z | 0m01.03s || -0m00.08s 0m00.90s | Util/NumTheoryUtil | 0m01.29s || -0m00.39s 0m00.89s | ModularArithmetic/ModularBaseSystemField | 0m00.93s || -0m00.04s 0m00.80s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.84s || -0m00.03s 0m00.70s | Experiments/SpecificCurve25519 | 0m00.72s || -0m00.02s 0m00.69s | Encoding/ModularWordEncodingTheorems | 0m00.98s || -0m00.29s 0m00.66s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.68s || -0m00.02s 0m00.63s | Testbit | 0m00.71s || -0m00.07s 0m00.62s | Encoding/ModularWordEncodingPre | 0m00.95s || -0m00.32s 0m00.61s | ModularArithmetic/ModularBaseSystemList | 0m00.63s || -0m00.02s 0m00.60s | Spec/ModularWordEncoding | 0m00.63s || -0m00.03s 0m00.59s | ModularArithmetic/ModularBaseSystem | 0m00.57s || +0m00.02s 0m00.57s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.81s || -0m00.24s 0m00.49s | ModularArithmetic/Pre | 0m00.71s || -0m00.21s 0m00.42s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.58s || -0m00.15s 0m00.40s | ModularArithmetic/Pow2Base | 0m00.46s || -0m00.06s 0m00.38s | Spec/ModularArithmetic | 0m00.56s || -0m00.18s --- src/Util/ZUtil.v | 88 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 88 insertions(+) (limited to 'src/Util') diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 899d1711e..045ada019 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -1,4 +1,6 @@ Require Import Coq.ZArith.Zpower Coq.ZArith.Znumtheory Coq.ZArith.ZArith Coq.ZArith.Zdiv. +Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms. +Require Import Coq.Structures.Equalities. Require Import Coq.omega.Omega Coq.micromega.Psatz Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. Require Import Crypto.Util.NatUtil. Require Import Crypto.Util.Notations. @@ -58,6 +60,24 @@ Hint Rewrite Z.div_small_iff using lia : zstrip_div. We'll put, e.g., [mul_div_eq] into it below. *) Create HintDb zstrip_div. +Ltac comes_before ls x y := + match ls with + | context[cons x ?xs] + => match xs with + | context[y] => idtac + end + end. +Ltac canonicalize_comm_step mul ls comm comm3 := + match goal with + | [ |- appcontext[mul ?x ?y] ] + => comes_before ls y x; + rewrite (comm x y) + | [ |- appcontext[mul ?x (mul ?y ?z)] ] + => comes_before ls y x; + rewrite (comm3 x y z) + end. +Ltac canonicalize_comm mul ls comm comm3 := repeat canonicalize_comm_step mul ls comm comm3. + Module Z. Definition pow2_mod n i := (n & (Z.ones i)). @@ -68,6 +88,11 @@ Module Z. rewrite Z.land_ones; auto. Qed. + Lemma mul_comm3 x y z : x * (y * z) = y * (x * z). + Proof. lia. Qed. + + Ltac Zcanonicalize_comm ls := canonicalize_comm Z.mul ls Z.mul_comm mul_comm3. + Lemma positive_is_nonzero : forall x, x > 0 -> x <> 0. Proof. intros; omega. Qed. @@ -1078,6 +1103,69 @@ Module Z. Lemma two_sub_sub_inner_sub x y z : 2 * x - y - (x - z) = x - y + z. Proof. clear; lia. Qed. Hint Rewrite two_sub_sub_inner_sub : zsimplify. + + Lemma f_equal_mul_mod x y x' y' m : x mod m = x' mod m -> y mod m = y' mod m -> (x * y) mod m = (x' * y') mod m. + Proof. + intros H0 H1; rewrite Zmult_mod, H0, H1, <- Zmult_mod; reflexivity. + Qed. + Hint Resolve f_equal_mul_mod : zarith. + + Lemma f_equal_add_mod x y x' y' m : x mod m = x' mod m -> y mod m = y' mod m -> (x + y) mod m = (x' + y') mod m. + Proof. + intros H0 H1; rewrite Zplus_mod, H0, H1, <- Zplus_mod; reflexivity. + Qed. + Hint Resolve f_equal_add_mod : zarith. + + Lemma f_equal_opp_mod x x' m : x mod m = x' mod m -> (-x) mod m = (-x') mod m. + Proof. + intro H. + destruct (Z_zerop (x mod m)) as [H'|H'], (Z_zerop (x' mod m)) as [H''|H'']; + try congruence. + { rewrite !Z_mod_zero_opp_full by assumption; reflexivity. } + { rewrite Z_mod_nz_opp_full, H, <- Z_mod_nz_opp_full by assumption; reflexivity. } + Qed. + Hint Resolve f_equal_opp_mod : zarith. + + Lemma f_equal_sub_mod x y x' y' m : x mod m = x' mod m -> y mod m = y' mod m -> (x - y) mod m = (x' - y') mod m. + Proof. + rewrite <- !Z.add_opp_r; auto with zarith. + Qed. + Hint Resolve f_equal_sub_mod : zarith. + + Section equiv_modulo. + Context (N : Z). + Definition equiv_modulo x y := x mod N = y mod N. + Local Infix "==" := equiv_modulo. + + Local Instance equiv_modulo_Reflexive : Reflexive equiv_modulo := fun _ => Logic.eq_refl. + Local Instance equiv_modulo_Symmetric : Symmetric equiv_modulo := fun _ _ => @Logic.eq_sym _ _ _. + Local Instance equiv_modulo_Transitive : Transitive equiv_modulo := fun _ _ _ => @Logic.eq_trans _ _ _ _. + + Lemma mul_mod_Proper : Proper (equiv_modulo ==> equiv_modulo ==> equiv_modulo) Z.mul. + Proof. unfold equiv_modulo, Proper, respectful; auto with zarith. Qed. + + Lemma add_mod_Proper : Proper (equiv_modulo ==> equiv_modulo ==> equiv_modulo) Z.add. + Proof. unfold equiv_modulo, Proper, respectful; auto with zarith. Qed. + + Lemma sub_mod_Proper : Proper (equiv_modulo ==> equiv_modulo ==> equiv_modulo) Z.sub. + Proof. unfold equiv_modulo, Proper, respectful; auto with zarith. Qed. + + Lemma opp_mod_Proper : Proper (equiv_modulo ==> equiv_modulo) Z.opp. + Proof. unfold equiv_modulo, Proper, respectful; auto with zarith. Qed. + End equiv_modulo. + + Module EquivModuloInstances (dummy : Nop). (* work around https://coq.inria.fr/bugs/show_bug.cgi?id=4973 *) + Existing Instance equiv_modulo_Reflexive. + Existing Instance equiv_modulo_Symmetric. + Existing Instance equiv_modulo_Transitive. + Existing Instance mul_mod_Proper. + Existing Instance add_mod_Proper. + Existing Instance sub_mod_Proper. + Existing Instance opp_mod_Proper. + End EquivModuloInstances. + Module RemoveEquivModuloInstances (dummy : Nop). + Global Remove Hints equiv_modulo_Reflexive equiv_modulo_Symmetric equiv_modulo_Transitive mul_mod_Proper add_mod_Proper sub_mod_Proper opp_mod_Proper : typeclass_instances. + End RemoveEquivModuloInstances. End Z. Module Export BoundsTactics. -- cgit v1.2.3