Move most notation level declarations into Util

This reveals and prevents notation clashes.

Notable breakage:
- `x {{ y }}` breaks `Context {forall x, {P x} + {~P x}}.`
  (@jadephilipoom)
- `x [[ y ]]` breaks `destruct x as [[a]|[b]].` (@jadephilipoom)
- `O :( A , B ): :?: L ::: R` breaks `((1):nat)` and `constr:(nat)`
  (@varomodt)

After    | File Name                                         | Before   || Change
------------------------------------------------------------------------------------
3m16.07s | Total                                             | 3m23.63s || -0m07.55s
------------------------------------------------------------------------------------
0m16.90s | ModularArithmetic/ModularBaseSystemProofs         | 0m19.02s || -0m02.12s
0m03.29s | ModularArithmetic/ModularBaseSystemOpt            | 0m05.30s || -0m02.00s
0m12.04s | Experiments/SpecEd25519                           | 0m13.89s || -0m01.85s
0m36.02s | CompleteEdwardsCurve/ExtendedCoordinates          | 0m36.12s || -0m00.09s
0m34.48s | Specific/GF25519                                  | 0m34.27s || +0m00.20s
0m15.62s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m15.76s || -0m00.14s
0m07.36s | Specific/GF1305                                   | 0m07.34s || +0m00.02s
0m06.64s | Algebra                                           | 0m06.14s || +0m00.50s
0m05.12s | WeierstrassCurve/Pre                              | 0m05.09s || +0m00.03s
0m04.58s | ModularArithmetic/Tutorial                        | 0m03.83s || +0m00.75s
0m04.46s | BaseSystemProofs                                  | 0m04.33s || +0m00.12s
0m04.26s | ModularArithmetic/Pow2BaseProofs                  | 0m05.16s || -0m00.90s
0m03.91s | CompleteEdwardsCurve/Pre                          | 0m04.62s || -0m00.71s
0m02.75s | Assembly/State                                    | 0m03.12s || -0m00.37s
0m02.55s | Experiments/EdDSARefinement                       | 0m01.85s || +0m00.69s
0m02.46s | Util/ZUtil                                        | 0m02.45s || +0m00.00s
0m01.86s | Assembly/Wordize                                  | 0m02.02s || -0m00.15s
0m01.68s | ModularArithmetic/ModularArithmeticTheorems       | 0m01.68s || +0m00.00s
0m01.67s | ModularArithmetic/PrimeFieldTheorems              | 0m01.96s || -0m00.29s
0m01.50s | Encoding/PointEncodingPre                         | 0m02.20s || -0m00.70s
0m01.46s | ModularArithmetic/BarrettReduction/Z              | 0m01.02s || +0m00.43s
0m01.26s | BaseSystem                                        | 0m01.21s || +0m00.05s
0m01.24s | Assembly/Pseudize                                 | 0m01.22s || +0m00.02s
0m01.20s | ModularArithmetic/ExtendedBaseVector              | 0m01.86s || -0m00.66s
0m01.04s | Util/IterAssocOp                                  | 0m00.74s || +0m00.30s
0m00.96s | ModularArithmetic/ExtPow2BaseMulProofs            | 0m00.67s || +0m00.28s
0m00.96s | Assembly/Pipeline                                 | 0m00.65s || +0m00.30s
0m00.93s | Experiments/DerivationsOptionRectLetInEncoding    | 0m00.98s || -0m00.04s
0m00.93s | ModularArithmetic/ModularBaseSystemField          | 0m00.95s || -0m00.01s
0m00.92s | Util/NumTheoryUtil                                | 0m01.19s || -0m00.26s
0m00.90s | ModularArithmetic/ModularBaseSystemListProofs     | 0m00.89s || +0m00.01s
0m00.82s | ModularArithmetic/PseudoMersenneBaseParamProofs   | 0m00.95s || -0m00.13s
0m00.81s | Assembly/QhasmEvalCommon                          | 0m00.86s || -0m00.04s
0m00.80s | Assembly/StringConversion                         | 0m00.60s || +0m00.20s
0m00.79s | Assembly/Qhasm                                    | 0m00.54s || +0m00.25s
0m00.73s | Assembly/Pseudo                                   | 0m00.98s || -0m00.25s
0m00.72s | Util/AdditionChainExponentiation                  | 0m00.92s || -0m00.20s
0m00.69s | Experiments/SpecificCurve25519                    | 0m00.72s || -0m00.03s
0m00.65s | Spec/ModularWordEncoding                          | 0m00.85s || -0m00.19s
0m00.65s | ModularArithmetic/ModularBaseSystemList           | 0m00.68s || -0m00.03s
0m00.65s | Assembly/PseudoConversion                         | 0m00.67s || -0m00.02s
0m00.64s | Encoding/ModularWordEncodingPre                   | 0m00.62s || +0m00.02s
0m00.64s | Spec/EdDSA                                        | 0m00.93s || -0m00.29s
0m00.64s | Testbit                                           | 0m00.94s || -0m00.29s
0m00.63s | Encoding/ModularWordEncodingTheorems              | 0m00.66s || -0m00.03s
0m00.62s | Assembly/AlmostQhasm                              | 0m00.49s || +0m00.13s
0m00.59s | ModularArithmetic/ModularBaseSystem               | 0m00.61s || -0m00.02s
0m00.49s | Spec/WeierstrassCurve                             | 0m00.43s || +0m00.06s
0m00.49s | Assembly/QhasmUtil                                | 0m00.51s || -0m00.02s
0m00.49s | ModularArithmetic/Pre                             | 0m00.47s || +0m00.02s
0m00.47s | Assembly/Vectorize                                | 0m00.51s || -0m00.04s
0m00.46s | Assembly/AlmostConversion                         | 0m00.44s || +0m00.02s
0m00.42s | ModularArithmetic/Pow2Base                        | 0m00.42s || +0m00.00s
0m00.41s | ModularArithmetic/PseudoMersenneBaseParams        | 0m00.45s || -0m00.04s
0m00.41s | Spec/ModularArithmetic                            | 0m00.41s || +0m00.00s
0m00.39s | Spec/CompleteEdwardsCurve                         | 0m00.41s || -0m00.01s
0m00.03s | Util/Notations                                    | 0m00.03s || +0m00.00s

2 files changed, 32 insertions, 4 deletions

diff --git a/src/Util/Notations.v b/src/Util/Notations.v
index 3aa80406b..b23fe37ac 100644
--- a/src/Util/Notations.v
+++ b/src/Util/Notations.v
@@ -17,8 +17,36 @@ Reserved Notation "x ^ 2" (at level 30, format "x ^ 2").
 Reserved Notation "x ^ 3" (at level 30, format "x ^ 3").
 Reserved Infix "mod" (at level 40, no associativity).
 Reserved Notation "'canonical' 'encoding' 'of' T 'as' B" (at level 50).
+Reserved Notation "@ 'is_eq_dec' T R" (at level 10, T at level 8, R at level 8).
 Reserved Infix "<<" (at level 30, no associativity).
 Reserved Infix ">>" (at level 30, no associativity).
 Reserved Infix "&" (at level 50).
 Reserved Infix "∣" (at level 50).
 Reserved Infix "~=" (at level 70).
+Reserved Infix "==" (at level 70, no associativity).
+Reserved Notation "a !== b" (at level 70, no associativity).
+Reserved Notation "$$ v" (at level 40).
+Reserved Notation "% A" (at level 20, right associativity).
+Reserved Notation "$ A" (at level 20, right associativity).
+Reserved Notation "A :[ B ]:" (at level 20, right associativity).
+Reserved Notation "# A" (at level 20, right associativity).
+Reserved Notation "A :+: B" (at level 60, right associativity).
+Reserved Notation "A :+c: B" (at level 60, right associativity).
+Reserved Notation "A :-: B" (at level 60, right associativity).
+Reserved Notation "A :&: B" (at level 45, right associativity).
+Reserved Notation "A :^: B" (at level 45, right associativity).
+Reserved Notation "A :>>: B" (at level 60, right associativity).
+Reserved Notation "A :<<: B" (at level 60, right associativity).
+Reserved Notation "A :*: B" (at level 55, right associativity).
+(*Reserved Notation "O :( A , B ): :?: L ::: R" (at level 70, right associativity).*) (* breaks everything *)
+Reserved Notation "F :**: e" (at level 70, right associativity).
+Reserved Notation "E :->: F" (at level 70, right associativity).
+Reserved Notation "A :|: B" (at level 65, left associativity).
+Reserved Notation "n ::: A :():" (at level 65, left associativity).
+Reserved Notation "& x" (at level 30).
+Reserved Notation "** x" (at level 30).
+Reserved Notation "A <- X ; B" (at level 70, right associativity).
+Reserved Notation "'plet' x := y 'in' z" (at level 60).
+Reserved Notation "u [ i ]" (at level 30).
+Reserved Notation "v [[ i ]]" (at level 30).
+Reserved Notation "u {{ i }}" (at level 30).
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 939ada461..ab844e9ad 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -214,7 +214,7 @@ Module Z.
     rewrite Z.mul_comm in c_id.
     apply Zdivide_intro in c_id.
     apply prime_divisors in c_id; auto.
-    destruct c_id; [omega | destruct H; [omega | destruct H; auto]].
+    destruct c_id; [omega | destruct H; [omega | destruct H; auto] ].
     pose proof (prime_ge_2 p prime_p); omega.
   Qed.
 
@@ -828,9 +828,9 @@ Module Z.
     | _ => lia
     | _ => progress subst
     | [ H : ?n * ?m < 0 |- _ ]
-      => apply (proj1 (Z.lt_mul_0 n m)) in H; destruct H as [[??]|[??]]
+      => apply (proj1 (Z.lt_mul_0 n m)) in H; destruct H as [ [??]|[??] ]
     | [ H : ?n / ?m < 0 |- _ ]
-      => apply (proj1 (lt_div_0 n m)) in H; destruct H as [[[??]|[??]]?]
+      => apply (proj1 (lt_div_0 n m)) in H; destruct H as [ [ [??]|[??] ] ? ]
     | [ H : (?x^?y) <= ?n < _, H' : ?n < 0 |- _ ]
       => assert (0 <= x^y) by zero_bounds; lia
     | [ H : (?x^?y) < 0 |- _ ]
@@ -841,7 +841,7 @@ Module Z.
          assert (x^y = 0) by lia;
          clear H H'
     | [ H : _^_ = 0 |- _ ]
-      => apply Z.pow_eq_0_iff in H; destruct H as [?|[??]]
+      => apply Z.pow_eq_0_iff in H; destruct H as [ ?|[??] ]
     | [ H : 0 <= ?x, H' : ?x - 1 < 0 |- _ ]
       => assert (x = 0) by lia; clear H H'
     | [ |- ?x <= ?y ] => is_evar x; reflexivity