From 0deb004886acf74a23d375683731f96897d7da25 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 7 Nov 2017 23:36:27 -0500 Subject: Add karatsuba, goldilocks lemmas to rewrite dbs --- src/Arithmetic/Karatsuba.v | 19 +++++++++++++++++-- .../Framework/ArithmeticSynthesis/Karatsuba.v | 2 +- 2 files changed, 18 insertions(+), 3 deletions(-) (limited to 'src') diff --git a/src/Arithmetic/Karatsuba.v b/src/Arithmetic/Karatsuba.v index fcd16baf3..ad5e25be8 100644 --- a/src/Arithmetic/Karatsuba.v +++ b/src/Arithmetic/Karatsuba.v @@ -1,4 +1,5 @@ Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. Require Import Crypto.Algebra.Nsatz. Require Import Crypto.Util.ZUtil Crypto.Util.LetIn Crypto.Util.CPSUtil. Require Import Crypto.Arithmetic.Core. Import B. Import Positional. @@ -55,6 +56,8 @@ Context (weight : nat -> Z) autorewrite with cancel_pair push_id uncps. reflexivity. Qed. + Hint Opaque karatsuba_mul : uncps. + Hint Rewrite karatsuba_mul_id : uncps. Lemma eval_karatsuba_mul s x y (s_nonzero:s <> 0) : eval weight (karatsuba_mul s x y) = eval weight x * eval weight y. @@ -199,9 +202,21 @@ Context (weight : nat -> Z) apply f_equal2; nsatz. assumption. assumption. omega. Qed. + + Lemma eval_goldilocks_mul (p : positive) s (s_nonzero : s <> 0) (s2_modp : mod_eq p (s^2) (s+1)) xs ys : + mod_eq p (eval weight (goldilocks_mul s xs ys)) (eval weight xs * eval weight ys). + Proof. + apply goldilocks_mul_correct; auto; lia. + Qed. End Karatsuba. -Hint Opaque goldilocks_mul : uncps. -Hint Rewrite goldilocks_mul_id : uncps. +Hint Opaque karatsuba_mul goldilocks_mul : uncps. +Hint Rewrite karatsuba_mul_id goldilocks_mul_id : uncps. + +Hint Rewrite + @eval_karatsuba_mul + @eval_goldilocks_mul + @goldilocks_mul_correct + using (assumption || (div_mod_cps_t; auto)) : push_basesystem_eval. Ltac basesystem_partial_evaluation_unfolder t := let t := (eval cbv delta [goldilocks_mul karatsuba_mul goldilocks_mul_cps karatsuba_mul_cps] in t) in diff --git a/src/Specific/Framework/ArithmeticSynthesis/Karatsuba.v b/src/Specific/Framework/ArithmeticSynthesis/Karatsuba.v index 454a27329..7274d2c35 100644 --- a/src/Specific/Framework/ArithmeticSynthesis/Karatsuba.v +++ b/src/Specific/Framework/ArithmeticSynthesis/Karatsuba.v @@ -76,7 +76,7 @@ Section gen. autorewrite with pattern_runtime; reflexivity | ]. - apply goldilocks_mul_correct; auto; try congruence. + reflexivity. Defined. End gen. -- cgit v1.2.3