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.