From 14bd0a5bfdbcc9899d4638d7681bfab75e7b93d0 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 3 Aug 2016 16:21:30 -0700 Subject: Add some autogenerated zsimplify lemmas After | File Name | Before || Change ---------------------------------------------------------------------------------- 1m46.74s | Total | 1m41.83s || +0m04.91s ---------------------------------------------------------------------------------- 0m33.71s | Specific/GF25519 | 0m32.43s || +0m01.28s 0m15.67s | ModularArithmetic/ModularBaseSystemProofs | 0m15.20s || +0m00.47s 0m11.62s | Experiments/SpecEd25519 | 0m11.26s || +0m00.35s 0m07.32s | Specific/GF1305 | 0m07.16s || +0m00.16s 0m04.42s | ModularArithmetic/Pow2BaseProofs | 0m04.05s || +0m00.37s 0m04.27s | ModularArithmetic/Tutorial | 0m03.69s || +0m00.57s 0m03.82s | BaseSystemProofs | 0m03.68s || +0m00.13s 0m03.21s | ModularArithmetic/ModularBaseSystemOpt | 0m03.24s || -0m00.03s 0m03.09s | Util/ZUtil | 0m02.86s || +0m00.23s 0m01.66s | Encoding/PointEncodingPre | 0m01.46s || +0m00.19s 0m01.56s | ModularArithmetic/ModularArithmeticTheorems | 0m01.53s || +0m00.03s 0m01.55s | ModularArithmetic/PrimeFieldTheorems | 0m01.48s || +0m00.07s 0m01.18s | BaseSystem | 0m01.17s || +0m00.01s 0m01.10s | ModularArithmetic/ExtendedBaseVector | 0m01.06s || +0m00.04s 0m01.00s | ModularArithmetic/BarrettReduction/Z | 0m00.98s || +0m00.02s 0m00.98s | Experiments/DerivationsOptionRectLetInEncoding | 0m00.95s || +0m00.03s 0m00.90s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.60s || +0m00.30s 0m00.90s | ModularArithmetic/ModularBaseSystemField | 0m00.87s || +0m00.03s 0m00.89s | ModularArithmetic/ModularBaseSystemList | 0m00.61s || +0m00.28s 0m00.85s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.75s || +0m00.09s 0m00.81s | ModularArithmetic/ModularBaseSystem | 0m00.54s || +0m00.27s 0m00.81s | Util/NumTheoryUtil | 0m00.81s || +0m00.00s 0m00.79s | Testbit | 0m00.63s || +0m00.16s 0m00.68s | Experiments/SpecificCurve25519 | 0m00.68s || +0m00.00s 0m00.63s | Encoding/ModularWordEncodingTheorems | 0m00.69s || -0m00.05s 0m00.61s | Encoding/ModularWordEncodingPre | 0m00.59s || +0m00.02s 0m00.60s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.55s || +0m00.04s 0m00.56s | Spec/ModularWordEncoding | 0m00.63s || -0m00.06s 0m00.43s | ModularArithmetic/Pre | 0m00.50s || -0m00.07s 0m00.40s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.41s || -0m00.00s 0m00.39s | ModularArithmetic/Pow2Base | 0m00.40s || -0m00.01s 0m00.33s | Spec/ModularArithmetic | 0m00.37s || -0m00.03s --- src/Util/ZUtil.v | 119 +++++++++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 103 insertions(+), 16 deletions(-) (limited to 'src') diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index f484a86c7..6cd59ccb7 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -1303,30 +1303,117 @@ Module Z. Proof. lia. Qed. Hint Rewrite simplify_twice_sub_add : zsimplify. - Lemma simplify_once_add_add_add x y z : x + y + (x + z) = 2 * x + y + z. + (* Naming convention: [X] for thing being aggregated, [p] for plus, + [m] for minus, [_] for parentheses *) + (* Python code to generate these hints: +<< +#!/usr/bin/env python + +def to_eqn(name): + vars_left = list('abcdefghijklmnopqrstuvwxyz') + ret = '' + close = '' + while name: + if name[0] == 'X': + ret += ' X' + name = name[1:] + else: + ret += ' ' + vars_left[0] + vars_left = vars_left[1:] + if name: + if name[0] == 'm': ret += ' -' + elif name[0] == 'p': ret += ' +' + name = name[1:] + if name and name[0] == '_': + ret += ' (' + close += ')' + name = name[1:] + if ret[-1] != 'X': + ret += ' ' + vars_left[0] + return (ret + close).strip().replace('( ', '(') + +def simplify(eqn): + counts = {} + sign_stack = [1, 1] + for i in eqn: + if i == ' ': continue + elif i == '(': sign_stack.append(sign_stack[-1]) + elif i == ')': sign_stack.pop() + elif i == '+': sign_stack.append(sign_stack[-1]) + elif i == '-': sign_stack.append(-sign_stack[-1]) + else: + counts[i] = counts.get(i,0) + sign_stack.pop() + ret = '' + for k in sorted(counts.keys()): + if counts[k] == 1: ret += ' + %s' % k + elif counts[k] == -1: ret += ' - %s' % k + elif counts[k] < 0: ret += ' - %d * %s' % (abs(counts[k]), k) + elif counts[k] > 0: ret += ' + %d * %s' % (abs(counts[k]), k) + if ret == '': ret = '0' + return ret.strip(' +') + + +def to_def(name): + eqn = to_eqn(name) + return r''' Lemma simplify_%s %s X : %s = %s. Proof. lia. Qed. - Hint Rewrite simplify_once_add_add_add : zsimplify. - Lemma simplify_once_add_add_sub x y z : x + y + (x - z) = 2 * x + y - z. + Hint Rewrite simplify_%s : zsimplify.''' % (name, ' '.join(sorted(set(eqn) - set('+-() X'))), eqn, simplify(eqn), name) + +names = [] +names += ['%sX%s%sX' % (a, b, c) for a in 'mp' for b in 'mp' for c in 'mp'] +names += ['X%s%s_X%s' % (a, b, c) for a in 'mp' for b in 'mp' for c in 'mp'] + +for name in names: + print(to_def(name)) +>> *) + Lemma simplify_mXmmX a b X : a - X - b - X = - 2 * X + a - b. + Proof. lia. Qed. + Hint Rewrite simplify_mXmmX : zsimplify. + Lemma simplify_mXmpX a b X : a - X - b + X = a - b. + Proof. lia. Qed. + Hint Rewrite simplify_mXmpX : zsimplify. + Lemma simplify_mXpmX a b X : a - X + b - X = - 2 * X + a + b. + Proof. lia. Qed. + Hint Rewrite simplify_mXpmX : zsimplify. + Lemma simplify_mXppX a b X : a - X + b + X = a + b. + Proof. lia. Qed. + Hint Rewrite simplify_mXppX : zsimplify. + Lemma simplify_pXmmX a b X : a + X - b - X = a - b. + Proof. lia. Qed. + Hint Rewrite simplify_pXmmX : zsimplify. + Lemma simplify_pXmpX a b X : a + X - b + X = 2 * X + a - b. + Proof. lia. Qed. + Hint Rewrite simplify_pXmpX : zsimplify. + Lemma simplify_pXpmX a b X : a + X + b - X = a + b. + Proof. lia. Qed. + Hint Rewrite simplify_pXpmX : zsimplify. + Lemma simplify_pXppX a b X : a + X + b + X = 2 * X + a + b. + Proof. lia. Qed. + Hint Rewrite simplify_pXppX : zsimplify. + Lemma simplify_Xmm_Xm a b X : X - a - (X - b) = - a + b. + Proof. lia. Qed. + Hint Rewrite simplify_Xmm_Xm : zsimplify. + Lemma simplify_Xmm_Xp a b X : X - a - (X + b) = - a - b. Proof. lia. Qed. - Hint Rewrite simplify_once_add_add_sub : zsimplify. - Lemma simplify_once_add_sub_add x y z : x + y - (x + z) = y - z. + Hint Rewrite simplify_Xmm_Xp : zsimplify. + Lemma simplify_Xmp_Xm a b X : X - a + (X - b) = 2 * X - a - b. Proof. lia. Qed. - Hint Rewrite simplify_once_add_sub_add : zsimplify. - Lemma simplify_once_add_sub_sub x y z : x + y - (x - z) = y + z. + Hint Rewrite simplify_Xmp_Xm : zsimplify. + Lemma simplify_Xmp_Xp a b X : X - a + (X + b) = 2 * X - a + b. Proof. lia. Qed. - Hint Rewrite simplify_once_add_sub_sub : zsimplify. - Lemma simplify_once_sub_add_add x y z : x - y + (x + z) = 2 * x - y + z. + Hint Rewrite simplify_Xmp_Xp : zsimplify. + Lemma simplify_Xpm_Xm a b X : X + a - (X - b) = a + b. Proof. lia. Qed. - Hint Rewrite simplify_once_sub_add_add : zsimplify. - Lemma simplify_once_sub_add_sub x y z : x - y + (x - z) = 2 * x - y - z. + Hint Rewrite simplify_Xpm_Xm : zsimplify. + Lemma simplify_Xpm_Xp a b X : X + a - (X + b) = a - b. Proof. lia. Qed. - Hint Rewrite simplify_once_sub_add_sub : zsimplify. - Lemma simplify_once_sub_sub_add x y z : x - y - (x + z) = -y - z. + Hint Rewrite simplify_Xpm_Xp : zsimplify. + Lemma simplify_Xpp_Xm a b X : X + a + (X - b) = 2 * X + a - b. Proof. lia. Qed. - Hint Rewrite simplify_once_sub_sub_add : zsimplify. - Lemma simplify_once_sub_sub_sub x y z : x - y - (x - z) = z - y. + Hint Rewrite simplify_Xpp_Xm : zsimplify. + Lemma simplify_Xpp_Xp a b X : X + a + (X + b) = 2 * X + a + b. Proof. lia. Qed. - Hint Rewrite simplify_once_sub_sub_sub : zsimplify. + Hint Rewrite simplify_Xpp_Xp : zsimplify. Section equiv_modulo. Context (N : Z). -- cgit v1.2.3