Make the library 20% faster: [auto with *] is evil

I do hereby revoke the privilege of [intuition] to grab random hints
from random databases.  This privilege is reserved for
[debug_intuition], which comes with a warning about not being used in
production code.  This tactic is useful in conjunction with `Print Hint
*`, to discover what hint databases the hints were grabbed from.

(Suggestions for renaming [debug_intuition] welcome.)

Any file using [intuition] must [Require Export
Crypto.Util.FixCoqMistakes.].  It's possible we could lift this
restriction by compiling [FixCoqMistakes] separately, and passing along
`-require FixCoqMistakes` to Coq.  Should we do this?

After    | File Name                                         | Before   || Change
------------------------------------------------------------------------------------
3m29.54s | Total                                             | 4m33.13s || -1m03.59s
------------------------------------------------------------------------------------
0m03.75s | BaseSystemProofs                                  | 0m43.84s || -0m40.09s
0m42.57s | CompleteEdwardsCurve/ExtendedCoordinates          | 0m34.48s || +0m08.09s
0m03.04s | Util/ListUtil                                     | 0m11.18s || -0m08.14s
0m01.62s | ModularArithmetic/PrimeFieldTheorems              | 0m09.53s || -0m07.90s
0m00.87s | Util/NumTheoryUtil                                | 0m07.61s || -0m06.74s
0m01.61s | Encoding/PointEncodingPre                         | 0m06.93s || -0m05.31s
0m51.95s | Specific/GF25519                                  | 0m47.52s || +0m04.42s
0m12.30s | Experiments/SpecEd25519                           | 0m11.29s || +0m01.01s
0m09.22s | Specific/GF1305                                   | 0m08.17s || +0m01.05s
0m03.48s | CompleteEdwardsCurve/Pre                          | 0m04.77s || -0m01.28s
0m02.70s | Assembly/State                                    | 0m04.09s || -0m01.38s
0m01.55s | ModularArithmetic/ModularArithmeticTheorems       | 0m02.93s || -0m01.38s
0m01.16s | Assembly/Pseudize                                 | 0m02.34s || -0m01.17s
0m15.67s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m16.37s || -0m00.70s
0m06.02s | Algebra                                           | 0m06.67s || -0m00.65s
0m05.90s | Experiments/GenericFieldPow                       | 0m06.68s || -0m00.77s
0m04.65s | WeierstrassCurve/Pre                              | 0m05.27s || -0m00.61s
0m03.93s | ModularArithmetic/Pow2BaseProofs                  | 0m03.94s || -0m00.00s
0m03.70s | ModularArithmetic/Tutorial                        | 0m03.85s || -0m00.14s
0m02.83s | ModularArithmetic/ModularBaseSystemOpt            | 0m02.84s || -0m00.00s
0m02.74s | Experiments/EdDSARefinement                       | 0m01.80s || +0m00.94s
0m02.35s | Util/ZUtil                                        | 0m02.51s || -0m00.15s
0m01.86s | Assembly/Wordize                                  | 0m02.32s || -0m00.45s
0m01.23s | ModularArithmetic/ExtendedBaseVector              | 0m01.20s || +0m00.03s
0m01.21s | BaseSystem                                        | 0m01.63s || -0m00.41s
0m01.03s | Experiments/SpecificCurve25519                    | 0m00.98s || +0m00.05s
0m01.01s | ModularArithmetic/ModularBaseSystemProofs         | 0m01.11s || -0m00.10s
0m00.95s | ModularArithmetic/BarrettReduction/Z              | 0m01.38s || -0m00.42s
0m00.92s | Experiments/DerivationsOptionRectLetInEncoding    | 0m01.81s || -0m00.89s
0m00.85s | ModularArithmetic/ModularBaseSystemField          | 0m00.86s || -0m00.01s
0m00.82s | ModularArithmetic/ModularBaseSystemListProofs     | 0m00.79s || +0m00.02s
0m00.80s | Assembly/QhasmEvalCommon                          | 0m00.93s || -0m00.13s
0m00.73s | Spec/EdDSA                                        | 0m00.59s || +0m00.14s
0m00.72s | Util/Tuple                                        | 0m00.71s || +0m00.01s
0m00.70s | Util/IterAssocOp                                  | 0m00.72s || -0m00.02s
0m00.67s | Encoding/ModularWordEncodingTheorems              | 0m00.71s || -0m00.03s
0m00.66s | Assembly/Pipeline                                 | 0m00.64s || +0m00.02s
0m00.65s | Testbit                                           | 0m00.65s || +0m00.00s
0m00.65s | Assembly/PseudoConversion                         | 0m00.65s || +0m00.00s
0m00.64s | Util/AdditionChainExponentiation                  | 0m00.63s || +0m00.01s
0m00.63s | ModularArithmetic/ExtPow2BaseMulProofs            | 0m00.64s || -0m00.01s
0m00.63s | Assembly/Pseudo                                   | 0m00.65s || -0m00.02s
0m00.62s | ModularArithmetic/ModularBaseSystem               | 0m00.57s || +0m00.05s
0m00.61s | ModularArithmetic/ModularBaseSystemList           | 0m00.57s || +0m00.04s
0m00.60s | Encoding/ModularWordEncodingPre                   | 0m00.69s || -0m00.08s
0m00.60s | ModularArithmetic/PseudoMersenneBaseParamProofs   | 0m00.59s || +0m00.01s
0m00.56s | Assembly/StringConversion                         | 0m00.56s || +0m00.00s
0m00.54s | Spec/ModularWordEncoding                          | 0m00.61s || -0m00.06s
0m00.54s | Assembly/QhasmUtil                                | 0m00.46s || +0m00.08s
0m00.52s | Assembly/Qhasm                                    | 0m00.53s || -0m00.01s
0m00.48s | Assembly/AlmostQhasm                              | 0m00.52s || -0m00.04s
0m00.48s | ModularArithmetic/Pre                             | 0m00.48s || +0m00.00s
0m00.46s | Assembly/Vectorize                                | 0m00.72s || -0m00.25s
0m00.45s | Spec/WeierstrassCurve                             | 0m00.44s || +0m00.01s
0m00.44s | Assembly/AlmostConversion                         | 0m00.44s || +0m00.00s
0m00.43s | ModularArithmetic/Pow2Base                        | 0m00.51s || -0m00.08s
0m00.42s | ModularArithmetic/PseudoMersenneBaseParams        | 0m00.38s || +0m00.03s
0m00.41s | Spec/CompleteEdwardsCurve                         | 0m00.43s || -0m00.02s
0m00.34s | Spec/ModularArithmetic                            | 0m00.36s || -0m00.01s
0m00.03s | Util/FixCoqMistakes                               |   N/A    || +0m00.03s
0m00.02s | Util/Notations                                    | 0m00.04s || -0m00.02s
0m00.02s | Util/Tactics                                      | 0m00.02s || +0m00.00s

1 files changed, 26 insertions, 25 deletions

diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v
index 4c64d8681..9760dc869 100644
--- a/src/Assembly/QhasmEvalCommon.v
+++ b/src/Assembly/QhasmEvalCommon.v
@@ -1,7 +1,8 @@
-Require Import QhasmCommon QhasmUtil State.
-Require Import ZArith Sumbool.
+Require Import Crypto.Assembly.QhasmCommon Crypto.Assembly.QhasmUtil Crypto.Assembly.State.
+Require Import Coq.ZArith.ZArith Coq.Bool.Sumbool.
 Require Import Bedrock.Word.
-Require Import Logic.Eqdep_dec ProofIrrelevance.
+Require Import Coq.Logic.Eqdep_dec Coq.Logic.ProofIrrelevance.
+Require Export Crypto.Util.FixCoqMistakes.
 
 Module EvalUtil.
   Definition evalTest {n} (o: TestOp) (a b: word n): bool :=
@@ -78,13 +79,13 @@ Module EvalUtil.
   Proof. induction a; unfold getWidth; simpl; intuition. Qed.
 
   Lemma width_eq {n} (a b: Width n): a = b.
-  Proof. 
+  Proof.
     assert (Some a = Some b) as H by (
       replace (Some a) with (getWidth n) by (rewrite getWidth_eq; intuition);
       replace (Some b) with (getWidth n) by (rewrite getWidth_eq; intuition);
       intuition).
     inversion H; intuition.
-  Qed. 
+  Qed.
 
   (* Mapping Conversions *)
 
@@ -102,29 +103,29 @@ Module EvalUtil.
 
   Definition mapping_dec {n} (a b: Mapping n): {a = b} + {a <> b}.
     refine (match (a, b) as p' return (a, b) = p' -> _ with
-    | (regM v, regM v') => fun _ => 
+    | (regM v, regM v') => fun _ =>
         if (Nat.eq_dec (regName v) (regName v'))
         then left _
         else right _
 
-    | (stackM v, stackM v') => fun _ => 
+    | (stackM v, stackM v') => fun _ =>
         if (Nat.eq_dec (stackName v) (stackName v'))
         then left _
         else right _
 
-    | (constM v, constM v') => fun _ => 
+    | (constM v, constM v') => fun _ =>
         if (Nat.eq_dec (constValueN v) (constValueN v'))
         then left _
         else right _
 
-    | (memM _ v i, memM _ v' i') => fun _ => 
-        if (Nat.eq_dec (memName v) (memName v')) 
+    | (memM _ v i, memM _ v' i') => fun _ =>
+        if (Nat.eq_dec (memName v) (memName v'))
         then if (Nat.eq_dec (memLength v) (memLength v'))
         then if (Nat.eq_dec (proj1_sig i) (proj1_sig i'))
         then left _ else right _ else right _ else right _
 
     | _ => fun _ => right _
-    end (eq_refl (a, b))); 
+    end (eq_refl (a, b)));
       try destruct v, v'; subst;
       unfold regName, stackName, constValueN, memName, memLength in *;
       repeat progress (try apply f_equal; subst; match goal with
@@ -158,10 +159,10 @@ Module EvalUtil.
       | [ H: proj1_sig ?a <> proj1_sig ?b |- _ ] =>
         let l0 := fresh in let l1 := fresh in
         destruct a, b; simpl in H; subst
-      | [ H: existT ?a ?b _ = existT ?a ?b _ |- _ ] => 
+      | [ H: existT ?a ?b _ = existT ?a ?b _ |- _ ] =>
         apply (inj_pair2_eq_dec _ Nat.eq_dec) in H;
             subst; intuition
-      | [ H: exist _ _ _ = exist _ _ _ |- _ ] => 
+      | [ H: exist _ _ _ = exist _ _ _ |- _ ] =>
         inversion H; subst; intuition
 
         (* Single specialized wordToNat proof *)
@@ -176,12 +177,12 @@ Module EvalUtil.
 
   Definition dec_lt (a b: nat): {(a < b)%nat} + {(a >= b)%nat}.
     assert ({(a <? b)%nat = true} + {(a <? b)%nat <> true})
-      by abstract (destruct (a <? b)%nat; intuition);
+      by abstract (destruct (a <? b)%nat; intuition auto with bool);
       destruct H.
 
     - left; abstract (apply Nat.ltb_lt; intuition).
 
-    - right; abstract (rewrite Nat.ltb_lt in *; intuition).
+    - right; abstract (rewrite Nat.ltb_lt in *; intuition auto with zarith).
   Defined.
 
   Fixpoint stackNames {n} (lst: list (Mapping n)): list nat :=
@@ -216,12 +217,12 @@ Module QhasmEval.
       omap (getReg r state) (fun v =>
         if (Nat.eq_dec O (wordToNat v))
         then Some true
-        else Some false) 
+        else Some false)
     | CReg n o a b =>
       omap (getReg a state) (fun va =>
         omap (getReg b state) (fun vb =>
           Some (evalTest o va vb)))
-    | CConst n o a c => 
+    | CConst n o a c =>
       omap (getReg a state) (fun va =>
         Some (evalTest o va (constValueW c)))
     end.
@@ -245,35 +246,35 @@ Module QhasmEval.
             let (v', co) := (evalIntOp o va vb) in
             Some (setCarryOpt co (setReg a v' state))))
 
-    | IOpMem _ _ o r m i => 
+    | IOpMem _ _ o r m i =>
       omap (getReg r state) (fun va =>
         omap (getMem m i state) (fun vb =>
             let (v', co) := (evalIntOp o va vb) in
             Some (setCarryOpt co (setReg r v' state))))
 
-    | DOp _ o a b (Some x) => 
+    | DOp _ o a b (Some x) =>
       omap (getReg a state) (fun va =>
         omap (getReg b state) (fun vb =>
             let (low, high) := (evalDualOp o va vb) in
             Some (setReg x high (setReg a low state))))
 
-    | DOp _ o a b None => 
+    | DOp _ o a b None =>
       omap (getReg a state) (fun va =>
         omap (getReg b state) (fun vb =>
             let (low, high) := (evalDualOp o va vb) in
             Some (setReg a low state)))
 
-    | ROp _ o r i => 
+    | ROp _ o r i =>
       omap (getReg r state) (fun v =>
         let v' := (evalRotOp o v i) in
         Some (setReg r v' state))
 
-    | COp _ o a b => 
+    | COp _ o a b =>
       omap (getReg a state) (fun va =>
         omap (getReg b state) (fun vb =>
             match (getCarry state) with
             | None => None
-            | Some c0 => 
+            | Some c0 =>
             let (v', c') := (evalCarryOp o va vb c0) in
             Some (setCarry c' (setReg a v' state))
             end))
@@ -281,7 +282,7 @@ Module QhasmEval.
 
   Definition evalAssignment (a: Assignment) (state: State): option State :=
     match a with
-    | ARegMem _ _ r m i => 
+    | ARegMem _ _ r m i =>
       omap (getMem m i state) (fun v => Some (setReg r v state))
     | AMemReg _ _ m i r =>
       omap (getReg r state) (fun v => Some (setMem m i v state))
@@ -289,7 +290,7 @@ Module QhasmEval.
       omap (getReg b state) (fun v => Some (setStack a v state))
     | ARegStack _ a b =>
       omap (getStack b state) (fun v => Some (setReg a v state))
-    | ARegReg _ a b => 
+    | ARegReg _ a b =>
       omap (getReg b state) (fun v => Some (setReg a v state))
     | AConstInt _ r c =>
       Some (setReg r (constValueW c) state)