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

1 files changed, 103 insertions, 16 deletions

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).