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

7 files changed, 27 insertions, 8 deletions

diff --git a/src/Util/FixCoqMistakes.v b/src/Util/FixCoqMistakes.v
new file mode 100644
index 000000000..abacfa580
--- /dev/null
+++ b/src/Util/FixCoqMistakes.v
@@ -0,0 +1,13 @@
+(** * Fixes *)
+
+(** Coq is poorly designed in some ways.  We fix some of these issues
+    in this file. *)
+
+(** [intuition] means [intuition auto with *].  This is very wrong and
+    fragile and slow.  We make [intuition] mean [intuition auto]. *)
+Tactic Notation "intuition" tactic3(tactic) := intuition tactic.
+Tactic Notation "intuition" := intuition auto.
+
+(** A version of [intuition] that allows you to see how the old
+    [intuition] tactic solves the proof. *)
+Ltac debug_intuition := idtac "<infomsg>Warning: debug_intuition should not be used in production code.</infomsg>"; intuition debug auto with *.
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 1032e1dc2..74c2b8537 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -5,6 +5,7 @@ Require Import Coq.Classes.Morphisms.
 Require Import Crypto.Tactics.VerdiTactics.
 Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Crypto.Util.NatUtil.
+Require Export Crypto.Util.FixCoqMistakes.
 
 Create HintDb distr_length discriminated.
 Create HintDb simpl_set_nth discriminated.
@@ -72,14 +73,14 @@ Definition splice_nth {T} n (x:T) xs := firstn n xs ++ x :: skipn (S n) xs.
 Hint Unfold splice_nth.
 
 Ltac boring :=
-  simpl; intuition;
+  simpl; intuition auto with zarith datatypes;
   repeat match goal with
            | [ H : _ |- _ ] => rewrite H; clear H
            | [ |- appcontext[match ?pf with end] ] => solve [ case pf ]
            | _ => progress autounfold in *
            | _ => progress autorewrite with core
            | _ => progress simpl in *
-           | _ => progress intuition
+           | _ => progress intuition auto with zarith datatypes
          end; eauto.
 
 Ltac boring_list :=
@@ -1133,7 +1134,7 @@ Proof.
   induction n as [|n IHn]; destruct l as [|? l]; autorewrite with simpl_sum_firstn; simpl; try omega.
   { specialize (IHn l).
     destruct n; simpl; autorewrite with simpl_sum_firstn simpl_nth_default in *;
-      intuition. }
+      intuition auto with zarith. }
 Qed.
 
 Hint Resolve sum_firstn_nonnegative : znonzero.
diff --git a/src/Util/Notations.v b/src/Util/Notations.v
index 4526e6dce..3aa80406b 100644
--- a/src/Util/Notations.v
+++ b/src/Util/Notations.v
@@ -1,4 +1,5 @@
 (** * Reserved Notations *)
+Require Export Crypto.Util.FixCoqMistakes.
 
 (** Putting them all together in one file prevents conflicts.  Coq's
     parser (camlpX) is really bad at conflicting notation levels and
diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v
index c16b87639..29fedaa9b 100644
--- a/src/Util/NumTheoryUtil.v
+++ b/src/Util/NumTheoryUtil.v
@@ -3,6 +3,7 @@ Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
 Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil.
 Require Import Coqprime.Zp.
 Require Import Crypto.Tactics.VerdiTactics.
+Require Export Crypto.Util.FixCoqMistakes.
 Local Open Scope Z.
 
 (* TODO: move somewhere else for lemmas about Coqprime? *)
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index c881478dd..5ff9d203c 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -1,4 +1,5 @@
 (** * Generic Tactics *)
+Require Export Crypto.Util.FixCoqMistakes.
 
 (** Test if a tactic succeeds, but always roll-back the results *)
 Tactic Notation "test" tactic3(tac) :=
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v
index 05d47b7f8..15a248afe 100644
--- a/src/Util/Tuple.v
+++ b/src/Util/Tuple.v
@@ -1,6 +1,7 @@
 Require Import Coq.Classes.Morphisms.
 Require Import Relation_Definitions.
 Require Import Crypto.Util.Decidable.
+Require Export Crypto.Util.FixCoqMistakes.
 
 Fixpoint tuple' T n : Type :=
   match n with
@@ -194,4 +195,4 @@ Definition apply {R T} (n:nat) : function R T n -> tuple T n -> R :=
   match n with
   | O => fun r _ => r
   | S n' => fun f x =>  apply' n' f x
-  end.
\ No newline at end of file
+  end.
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 077ad25a8..294e9d8f2 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -3,6 +3,7 @@ Require Import Coq.omega.Omega Coq.micromega.Psatz Coq.Numbers.Natural.Peano.NPe
 Require Import Crypto.Util.NatUtil.
 Require Import Crypto.Util.Notations.
 Require Import Coq.Lists.List.
+Require Export Crypto.Util.FixCoqMistakes.
 Import Nat.
 Local Open Scope Z.
 
@@ -68,7 +69,7 @@ Module Z.
   Proof.
     intros; rewrite Z.gt_lt_iff.
     apply Z.div_str_pos.
-    split; intuition.
+    split; intuition auto with omega.
     apply Z.divide_pos_le; try (apply Zmod_divide); omega.
   Qed.
 
@@ -172,7 +173,7 @@ Module Z.
     rewrite div_mul' in divide_a by auto.
     replace (b * k) with (k * b) in divide_a by ring.
     replace (c * k * k0) with (k * (k0 * c)) in divide_a by ring.
-    rewrite Z.mul_cancel_l in divide_a by (intuition; rewrite H in divide_c_a; ring_simplify in divide_a; intuition).
+    rewrite Z.mul_cancel_l in divide_a by (intuition auto with nia; rewrite H in divide_c_a; ring_simplify in divide_a; intuition).
     eapply Zdivide_intro; eauto.
   Qed.
 
@@ -424,7 +425,7 @@ Module Z.
       omega.
     + intros.
       destruct (Z_lt_le_dec x n); try omega.
-      intuition.
+      intuition auto with zarith lia.
       left.
       rewrite shiftr_succ.
       replace (n - Z.succ x) with (Z.pred (n - x)) by omega.
@@ -563,7 +564,7 @@ Module Z.
     destruct (in_inv In_list); subst.
     + apply Z.le_max_l.
     + etransitivity.
-      - apply IHl; auto; intuition.
+      - apply IHl; auto; intuition auto with datatypes.
       - apply Z.le_max_r.
   Qed.