Merge branch 'master' of github.com:mit-plv/fiat-crypto

27 files changed, 244 insertions, 110 deletions

diff --git a/src/Algebra.v b/src/Algebra.v
index d47fc6acd..f4afcb935 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -5,6 +5,7 @@ Require Import Crypto.Util.Notations.
 Require Coq.Numbers.Natural.Peano.NPeano.
 Local Close Scope nat_scope. Local Close Scope type_scope. Local Close Scope core_scope.
 Require Crypto.Tactics.Algebra_syntax.Nsatz.
+Require Export Crypto.Util.FixCoqMistakes.
 
 Module Import ModuloCoq8485.
   Import NPeano Nat.
@@ -1299,6 +1300,21 @@ Ltac only_two_square_roots :=
     => repeat only_two_square_roots_step eq opp mul
   end.
 
+(*** Tactics for ring equations *)
+Require Import Coq.setoid_ring.Ring_tac.
+Ltac ring_simplify_subterms := tac_on_subterms ltac:(fun t => ring_simplify t).
+
+Ltac ring_simplify_subterms_in_all :=
+  reverse_nondep; ring_simplify_subterms; intros.
+
+Create HintDb ring_simplify discriminated.
+Create HintDb ring_simplify_subterms discriminated.
+Create HintDb ring_simplify_subterms_in_all discriminated.
+Hint Extern 1 => progress ring_simplify : ring_simplify.
+Hint Extern 1 => progress ring_simplify_subterms : ring_simplify_subterms.
+Hint Extern 1 => progress ring_simplify_subterms_in_all : ring_simplify_subterms_in_all.
+
+
 Section Example.
   Context {F zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div}.
   Local Infix "+" := add. Local Infix "*" := mul. Local Infix "-" := sub. Local Infix "/" := div.
diff --git a/src/Assembly/Pseudize.v b/src/Assembly/Pseudize.v
index c167dd6a1..ea14dc52e 100644
--- a/src/Assembly/Pseudize.v
+++ b/src/Assembly/Pseudize.v
@@ -1,7 +1,8 @@
 Require Export Bedrock.Word Bedrock.Nomega.
-Require Import NArith NPeano List Sumbool Compare_dec Omega.
-Require Import QhasmCommon QhasmEvalCommon QhasmUtil Pseudo State.
-Require Export Wordize Vectorize.
+Require Import Coq.NArith.NArith Coq.Numbers.Natural.Peano.NPeano Coq.Lists.List Coq.Bool.Sumbool Coq.Arith.Compare_dec Coq.omega.Omega.
+Require Import Crypto.Assembly.QhasmCommon Crypto.Assembly.QhasmEvalCommon Crypto.Assembly.QhasmUtil Crypto.Assembly.Pseudo Crypto.Assembly.State.
+Require Export Crypto.Assembly.Wordize Crypto.Assembly.Vectorize.
+Require Export Crypto.Util.FixCoqMistakes.
 
 Import Pseudo ListNotations StateCommon EvalUtil ListState.
 
@@ -34,8 +35,8 @@ Section Conversion.
     replace (k mod n) with k by (
       assert (n <> 0) as NZ by omega;
       pose proof (Nat.div_mod k n NZ);
-      replace (k mod n) with (k - n * (k / n)) by intuition;
-      rewrite (Nat.div_small k n); intuition).
+      replace (k mod n) with (k - n * (k / n)) by intuition auto with zarith;
+      rewrite (Nat.div_small k n); intuition auto with zarith).
 
     autounfold; simpl.
     destruct (nth_error x k); simpl; try inversion H0; intuition.
@@ -48,8 +49,8 @@ Section Conversion.
     intros; autounfold; simpl.
     unfold indexize;
       destruct (le_dec n 0), (le_dec len 0);
-      try replace n with 0 in * by intuition;
-      try replace len with 0 in * by intuition;
+      try replace n with 0 in * by intuition auto with zarith;
+      try replace len with 0 in * by intuition auto with zarith;
       autounfold; simpl in *; rewrite H;
       autounfold; simpl; rewrite NToWord_wordToN;
       intuition.
@@ -247,7 +248,7 @@ Section Conversion.
       simpl; intuition.
   Qed.
 
-  Definition pseudeq {w s} (n m: nat) (f: list (word w) -> list (word w)) : Type := 
+  Definition pseudeq {w s} (n m: nat) (f: list (word w) -> list (word w)) : Type :=
     {p: @Pseudo w s n m | forall x: (list (word w)),
       List.length x = n -> exists m' c',
       pseudoEval p (x, TripleM.empty N, None) = Some (f x, m', c')}.
diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v
index e3f1e63ff..b8aae4521 100644
--- a/src/Assembly/Pseudo.v
+++ b/src/Assembly/Pseudo.v
@@ -1,6 +1,7 @@
-Require Import QhasmCommon QhasmUtil State.
-Require Import Language QhasmEvalCommon.
-Require Import List Compare_dec Omega.
+Require Import Crypto.Assembly.QhasmCommon Crypto.Assembly.QhasmUtil Crypto.Assembly.State.
+Require Import Crypto.Assembly.Language Crypto.Assembly.QhasmEvalCommon.
+Require Import Coq.Lists.List Coq.Arith.Compare_dec Coq.omega.Omega.
+Require Export Crypto.Util.FixCoqMistakes.
 
 Module Pseudo <: Language.
   Import EvalUtil ListState.
@@ -96,7 +97,7 @@ Module Pseudo <: Language.
           else pseudoEval r st ))
 
     | PFunExp n p e =>
-      (fix funexpseudo (e': nat) (st': ListState w) := 
+      (fix funexpseudo (e': nat) (st': ListState w) :=
         match e' with
         | O => Some st'
         | S e'' =>
@@ -116,7 +117,7 @@ Module Pseudo <: Language.
   Definition indexize {n: nat} (x: nat): Index n.
     intros; destruct (le_dec n 0).
 
-    - exists 0; abstract intuition.
+    - exists 0; abstract intuition auto with zarith.
     - exists (x mod n)%nat; abstract (
         pose proof (Nat.mod_bound_pos x n); omega).
   Defined.
@@ -179,4 +180,3 @@ Module Pseudo <: Language.
 
   Close Scope pseudo_notations.
 End Pseudo.
-
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)
diff --git a/src/Assembly/QhasmUtil.v b/src/Assembly/QhasmUtil.v
index acf2b5c31..1ab894e94 100644
--- a/src/Assembly/QhasmUtil.v
+++ b/src/Assembly/QhasmUtil.v
@@ -1,6 +1,7 @@
-Require Import ZArith NArith NPeano.
-Require Import QhasmCommon.
+Require Import Coq.ZArith.ZArith Coq.NArith.NArith Coq.Numbers.Natural.Peano.NPeano.
+Require Import Crypto.Assembly.QhasmCommon.
 Require Export Bedrock.Word.
+Require Export Crypto.Util.FixCoqMistakes.
 
 Delimit Scope nword_scope with w.
 Local Open Scope nword_scope.
@@ -14,12 +15,12 @@ Section Util.
 
   Definition high {k n: nat} (p: (k <= n)%nat) (w: word n): word k.
     refine (split1 k (n - k) (convS w _)).
-    abstract (replace n with (k + (n - k)) by omega; intuition).
+    abstract (replace n with (k + (n - k)) by omega; intuition auto with arith).
   Defined.
 
   Definition low {k n: nat} (p: (k <= n)%nat) (w: word n): word k.
     refine (split2 (n - k) k (convS w _)).
-    abstract (replace n with (k + (n - k)) by omega; intuition).
+    abstract (replace n with (k + (n - k)) by omega; intuition auto with zarith).
   Defined.
 
   Definition extend {k n: nat} (p: (k <= n)%nat) (w: word k): word n.
@@ -61,7 +62,7 @@ Section Util.
     refine match (le_dec m n) with
     | left p => (extend _ (low p x), extend _ (@high (n - m) n _ x))
     | right p => (extend _ x, _)
-    end; try abstract intuition.
+    end; try abstract intuition auto with zarith.
 
     replace (n - m) with O by abstract omega; exact WO.
   Defined.
@@ -75,4 +76,4 @@ Section Util.
   Notation "A <- X ; B" := (omap X (fun A => B)) (at level 70, right associativity).
 End Util.
 
-Close Scope nword_scope.
\ No newline at end of file
+Close Scope nword_scope.
diff --git a/src/Assembly/State.v b/src/Assembly/State.v
index 8602c7f96..3467a5cad 100644
--- a/src/Assembly/State.v
+++ b/src/Assembly/State.v
@@ -1,12 +1,14 @@
-Require Export String List Logic.
+Require Export Coq.Strings.String Coq.Lists.List Coq.Init.Logic.
 Require Export Bedrock.Word.
 
-Require Import ZArith NArith NPeano Ndec.
-Require Import Compare_dec Omega.
-Require Import OrderedType Coq.Structures.OrderedTypeEx.
-Require Import FMapPositive FMapFullAVL JMeq.
+Require Import Coq.ZArith.ZArith Coq.NArith.NArith Coq.Numbers.Natural.Peano.NPeano Coq.NArith.Ndec.
+Require Import Coq.Arith.Compare_dec Coq.omega.Omega.
+Require Import Coq.Structures.OrderedType Coq.Structures.OrderedTypeEx.
+Require Import Coq.FSets.FMapPositive Coq.FSets.FMapFullAVL Coq.Logic.JMeq.
 
-Require Import QhasmUtil QhasmCommon.
+Require Import Crypto.Assembly.QhasmUtil Crypto.Assembly.QhasmCommon.
+
+Require Export Crypto.Util.FixCoqMistakes.
 
 (* We want to use pairs and triples as map keys: *)
 
@@ -50,16 +52,16 @@ Module Pair_as_OT <: UsualOrderedType.
       destruct (Nat_as_OT.compare x0 y0);
       unfold Nat_as_OT.lt, Nat_as_OT.eq in *.
 
-    - apply LT; abstract (unfold lt; simpl; destruct (Nat.eq_dec x0 y0); intuition).
+    - apply LT; abstract (unfold lt; simpl; destruct (Nat.eq_dec x0 y0); intuition auto with zarith).
 
     - destruct (Nat_as_OT.compare x1 y1);
         unfold Nat_as_OT.lt, Nat_as_OT.eq in *.
 
       + apply LT; abstract (unfold lt; simpl; destruct (Nat.eq_dec x0 y0); intuition).
-      + apply EQ; abstract (unfold lt; simpl; subst; intuition).
-      + apply GT; abstract (unfold lt; simpl; destruct (Nat.eq_dec y0 x0); intuition).
+      + apply EQ; abstract (unfold lt; simpl; subst; intuition auto with relations).
+      + apply GT; abstract (unfold lt; simpl; destruct (Nat.eq_dec y0 x0); intuition auto with zarith).
 
-    - apply GT; abstract (unfold lt; simpl; destruct (Nat.eq_dec y0 x0); intuition).
+    - apply GT; abstract (unfold lt; simpl; destruct (Nat.eq_dec y0 x0); intuition auto with zarith).
   Defined.
 
   Definition eq_dec (a b: t): {a = b} + {a <> b}.
@@ -69,14 +71,14 @@ Module Pair_as_OT <: UsualOrderedType.
     - right; abstract (
         unfold lt in *; simpl in *;
         destruct (Nat.eq_dec a0 b0); intuition;
-        inversion H; intuition).
+        inversion H; intuition auto with zarith).
 
     - left; abstract (inversion e; intuition).
 
     - right; abstract (
         unfold lt in *; simpl in *;
         destruct (Nat.eq_dec b0 a0); intuition;
-        inversion H; intuition).
+        inversion H; intuition auto with zarith).
   Defined.
 End Pair_as_OT.
 
@@ -132,7 +134,7 @@ Module Triple_as_OT <: UsualOrderedType.
       unfold Nat_as_OT.lt, Nat_as_OT.eq, lt, eq in *;
       destruct (Nat.eq_dec (get0 x) (get0 y));
       destruct (Nat.eq_dec (get1 x) (get1 y));
-      simpl; intuition).
+      simpl; intuition auto with zarith).
 
   Ltac compare_eq x y :=
     abstract (
@@ -163,14 +165,14 @@ Module Triple_as_OT <: UsualOrderedType.
     - right; abstract (
         unfold lt, get0, get1, get2 in *; simpl in *;
         destruct (Nat.eq_dec a0 b0), (Nat.eq_dec a1 b1);
-        intuition; inversion H; intuition).
+        intuition; inversion H; intuition auto with zarith).
 
     - left; abstract (inversion e; intuition).
 
     - right; abstract (
         unfold lt, get0, get1, get2 in *; simpl in *;
         destruct (Nat.eq_dec b0 a0), (Nat.eq_dec b1 a1);
-        intuition; inversion H; intuition).
+        intuition; inversion H; intuition auto with zarith).
   Defined.
 End Triple_as_OT.
 
diff --git a/src/Assembly/Vectorize.v b/src/Assembly/Vectorize.v
index d2fca3ce6..4eed28aad 100644
--- a/src/Assembly/Vectorize.v
+++ b/src/Assembly/Vectorize.v
@@ -1,6 +1,8 @@
 Require Export Bedrock.Word Bedrock.Nomega.
-Require Import NPeano NArith PArith Ndigits Compare_dec Arith.
-Require Import ProofIrrelevance Ring List Omega.
+Require Import Coq.Numbers.Natural.Peano.NPeano Coq.NArith.NArith Coq.PArith.PArith Coq.NArith.Ndigits Coq.Arith.Compare_dec Coq.Arith.Arith.
+Require Import Coq.Logic.ProofIrrelevance Coq.setoid_ring.Ring Coq.Lists.List Coq.omega.Omega.
+
+Require Export Crypto.Util.FixCoqMistakes.
 
 Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x :=
   let y := x in f y.
diff --git a/src/Assembly/Wordize.v b/src/Assembly/Wordize.v
index bac25db71..5e27a93b7 100644
--- a/src/Assembly/Wordize.v
+++ b/src/Assembly/Wordize.v
@@ -1,9 +1,11 @@
 
 Require Export Bedrock.Word Bedrock.Nomega.
-Require Import NArith PArith Ndigits Nnat NPow NPeano Ndec.
-Require Import Compare_dec Omega.
-Require Import FunctionalExtensionality ProofIrrelevance.
-Require Import QhasmUtil QhasmEvalCommon.
+Require Import Coq.NArith.NArith Coq.PArith.PArith Coq.NArith.Ndigits Coq.NArith.Nnat Coq.Numbers.Natural.Abstract.NPow Coq.Numbers.Natural.Peano.NPeano Coq.NArith.Ndec.
+Require Import Coq.Arith.Compare_dec Coq.omega.Omega.
+Require Import Coq.Logic.FunctionalExtensionality Coq.Logic.ProofIrrelevance.
+Require Import Crypto.Assembly.QhasmUtil Crypto.Assembly.QhasmEvalCommon.
+
+Require Export Crypto.Util.FixCoqMistakes.
 
 Hint Rewrite wordToN_nat Nat2N.inj_add N2Nat.inj_add
              Nat2N.inj_mul N2Nat.inj_mul Npow2_nat : N.
@@ -18,7 +20,7 @@ Section WordizeUtil.
     intros; unfold break in *; destruct (le_dec m n);
       inversion H; subst; clear H; simpl.
   Admitted.
- 
+
   Lemma mask_wand : forall (n: nat) (x: word n) m b,
       (& (mask (N.to_nat m) x) < b)%N
     -> (& (x ^& (@NToWord n (N.ones m))) < b)%N.
@@ -33,7 +35,7 @@ Section WordizeUtil.
   Qed.
 
   Lemma word_param_eq: forall n m, word n = word m -> n = m.
-  Proof. (* TODO: How do we prove this *) Admitted. 
+  Proof. (* TODO: How do we prove this *) Admitted.
 
   Lemma word_conv_eq: forall {n m} (y: word m) p,
       &y = &(@convS (word m) (word n) y p).
@@ -153,7 +155,7 @@ Section WordizeUtil.
     - intros; simpl; replace (a + 0) with a; nomega.
 
     - intros.
-      replace (a + S b) with (S a + b) by intuition.
+      replace (a + S b) with (S a + b) by intuition auto with zarith.
       rewrite (IHb (S a)); simpl; clear IHb.
       induction (Npow2 a), (Npow2 b); simpl; intuition.
       rewrite Pos.mul_xO_r; intuition.
@@ -180,7 +182,7 @@ Section Wordization.
     rewrite wordToN_NToWord; intuition.
     apply (N.lt_le_trans _ (b + &y)%N _).
 
-    - apply N.add_lt_le_mono; try assumption; intuition.
+    - apply N.add_lt_le_mono; try assumption; intuition auto with relations.
 
     - replace (Npow2 n) with (b + Npow2 n - b)%N by nomega.
         replace (b + Npow2 n - b)%N with (b + (Npow2 n - b))%N by (
@@ -402,7 +404,7 @@ Ltac wordize_ast :=
   | [ |- _ = _ ] => reflexivity
   end.
 
-Ltac lt_crush := try abstract (clear; vm_compute; intuition).
+Ltac lt_crush := try abstract (clear; vm_compute; intuition auto with zarith).
 
 (** Bounding Tactics **)
 
diff --git a/src/BaseSystem.v b/src/BaseSystem.v
index 840713168..48b6468cf 100644
--- a/src/BaseSystem.v
+++ b/src/BaseSystem.v
@@ -3,6 +3,7 @@ Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv.
 Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
 Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil.
 Require Import Crypto.Util.Notations.
+Require Export Crypto.Util.FixCoqMistakes.
 Import Nat.
 
 Local Open Scope Z.
@@ -140,11 +141,11 @@ Section PolynomialBaseCoefs.
     unfold bi.
     replace (Z.pos b1 ^ Z.of_nat (S i))
       with (Z.pos b1 * (Z.pos b1 ^ Z.of_nat i)) by
-      (rewrite Nat2Z.inj_succ; rewrite <- Z.pow_succ_r; intuition).
+      (rewrite Nat2Z.inj_succ; rewrite <- Z.pow_succ_r; intuition auto with zarith).
     replace (Z.pos b1 * Z.pos b1 ^ Z.of_nat i / Z.pos b1 ^ Z.of_nat i)
       with (Z.pos b1); auto.
     rewrite Z_div_mult_full; auto.
-    apply Z.pow_nonzero; intuition.
+    apply Z.pow_nonzero; intuition auto with lia.
   Qed.
 
   Lemma poly_base_good:
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
index 1d8b730cb..dbfdb023e 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -5,8 +5,9 @@ Require Import Crypto.CompleteEdwardsCurve.Pre.
 Require Import Coq.Logic.Eqdep_dec.
 Require Import Crypto.Tactics.VerdiTactics.
 Require Import Coq.Classes.Morphisms.
-Require Import Relation_Definitions.
+Require Import Coq.Relations.Relation_Definitions.
 Require Import Crypto.Util.Tuple Crypto.Util.Notations Crypto.Util.Tactics.
+Require Export Crypto.Util.FixCoqMistakes.
 
 Module E.
   Import Group ScalarMult Ring Field CompleteEdwardsCurve.E.
@@ -57,7 +58,7 @@ Module E.
       apply H;
       try common_denominator;
       [rewrite <-Hx; ring | ..].
-      
+
     Ltac bash_step :=
       let addCompletePlus := constr:(edwardsAddCompletePlus(char_gt_2:=char_gt_2)(d_nonsquare:=nonsquare_d)(a_square:=square_a)(a_nonzero:=nonzero_a)) in
       let addCompleteMinus := constr:(edwardsAddCompleteMinus(char_gt_2:=char_gt_2)(d_nonsquare:=nonsquare_d)(a_square:=square_a)(a_nonzero:=nonzero_a)) in
diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
index f3820aeac..ac3523889 100644
--- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v
+++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
@@ -5,9 +5,10 @@ Require Import Crypto.CompleteEdwardsCurve.Pre Crypto.CompleteEdwardsCurve.Compl
 Require Import Coq.Logic.Eqdep_dec.
 Require Import Crypto.Tactics.VerdiTactics.
 Require Import Coq.Classes.Morphisms.
-Require Import Relation_Definitions.
+Require Import Coq.Relations.Relation_Definitions.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Notations.
+Require Export Crypto.Util.FixCoqMistakes.
 
 Module Extended.
   Section ExtendedCoordinates.
diff --git a/src/Encoding/PointEncodingPre.v b/src/Encoding/PointEncodingPre.v
index 2ad567c92..e6305f798 100644
--- a/src/Encoding/PointEncodingPre.v
+++ b/src/Encoding/PointEncodingPre.v
@@ -11,6 +11,8 @@ Require Import Crypto.Algebra.
 
 Require Import Crypto.Spec.Encoding Crypto.Spec.ModularWordEncoding Crypto.Spec.ModularArithmetic.
 
+Require Export Crypto.Util.FixCoqMistakes.
+
 Generalizable All Variables.
 Section PointEncodingPre.
   Context {F eq zero one opp add sub mul inv div} `{field F eq zero one opp add sub mul inv div}.
@@ -22,7 +24,7 @@ Section PointEncodingPre.
   Local Notation "x '^' 2" := (x*x) (at level 30).
 
   Add Field EdwardsCurveField : (Field.field_theory_for_stdlib_tactic (T:=F)).
-  
+
   Context {eq_dec:forall x y : F, {x==y}+{x==y->False}}.
   Definition F_eqb x y := if eq_dec x y then true else false.
   Lemma F_eqb_iff : forall x y, F_eqb x y = true <-> x == y.
@@ -64,7 +66,7 @@ Section PointEncodingPre.
     symmetry.
     apply E.solve_correct; eassumption.
   Qed.
- 
+
   (* TODO : move? *)
   Lemma square_opp : forall x : F, (opp x ^2) == (x ^2).
   Proof.
@@ -97,7 +99,7 @@ Section PointEncodingPre.
           let p := (if Bool.eqb (whd w) (sign_bit x) then x else opp x, y) in
           if (andb (F_eqb x 0) (whd w))
           then None (* special case for 0, since its opposite has the same sign; if the sign bit of 0 is 1, produce None.*)
-          else Some p 
+          else Some p
         else None
     end.
 
@@ -112,7 +114,7 @@ Section PointEncodingPre.
     destruct x as [x1 x2].
     destruct y as [y1 y2].
     match goal with
-    | |- {prod_eq _ _ (?x1, ?x2) (?y1,?y2)} + {not (prod_eq _ _ (?x1, ?x2) (?y1,?y2))} => 
+    | |- {prod_eq _ _ (?x1, ?x2) (?y1,?y2)} + {not (prod_eq _ _ (?x1, ?x2) (?y1,?y2))} =>
       destruct (A_eq_dec x1 y1); destruct (A_eq_dec x2 y2) end;
       unfold prod_eq; intuition.
   Qed.
@@ -162,7 +164,7 @@ Section PointEncodingPre.
 
   Definition point_eq (p q : point) : Prop := prod_eq eq eq (proj1_sig p) (proj1_sig q).
   Definition option_point_eq := option_eq (point_eq).
-  
+
   Lemma option_point_eq_iff : forall p q,
     option_point_eq (Some p) (Some q) <->
     option_coordinates_eq (Some (proj1_sig p)) (Some (proj1_sig q)).
@@ -214,7 +216,7 @@ Section PointEncodingPre.
   Proof.
     unfold prod_eq; intros.
     repeat break_let.
-    intuition; etransitivity; eauto.
+    intuition auto with relations; etransitivity; eauto.
   Qed.
 
   Lemma option_coordinates_eq_sym : forall p q, option_coordinates_eq p q ->
diff --git a/src/Experiments/DerivationsOptionRectLetInEncoding.v b/src/Experiments/DerivationsOptionRectLetInEncoding.v
index 4f51f299d..3ae1daa75 100644
--- a/src/Experiments/DerivationsOptionRectLetInEncoding.v
+++ b/src/Experiments/DerivationsOptionRectLetInEncoding.v
@@ -2,17 +2,18 @@ Require Import Coq.omega.Omega.
 Require Import Bedrock.Word.
 Require Import Crypto.Spec.EdDSA.
 Require Import Crypto.Tactics.VerdiTactics.
-Require Import BinNat BinInt NArith Crypto.Spec.ModularArithmetic.
-Require Import ModularArithmetic.ModularArithmeticTheorems.
-Require Import ModularArithmetic.PrimeFieldTheorems.
+Require Import Coq.NArith.BinNat Coq.ZArith.BinInt Coq.NArith.NArith Crypto.Spec.ModularArithmetic.
+Require Import Crypto.ModularArithmetic.ModularArithmeticTheorems.
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Import Crypto.Spec.CompleteEdwardsCurve.
 Require Import Crypto.Spec.Encoding Crypto.Spec.ModularWordEncoding.
 Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates.
 Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
 Require Import Crypto.Util.IterAssocOp Crypto.Util.WordUtil.
 Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence.
-Require Import Zdiv.
+Require Import Coq.ZArith.Zdiv.
 Require Import Crypto.Util.Tuple.
+Require Export Crypto.Util.FixCoqMistakes.
 Local Open Scope equiv_scope.
 
 Generalizable All Variables.
@@ -98,7 +99,7 @@ Qed.
 
 Global Instance pair_Equivalence {A B} `{@Equivalence A RA} `{@Equivalence B RB} : @Equivalence (A*B) (fun x y => fst x = fst y /\ snd x === snd y).
 Proof.
-  constructor; repeat intro; intuition; try congruence.
+  constructor; repeat intro; intuition auto with relations; try congruence.
   match goal with [H : _ |- _ ] => solve [rewrite H; auto] end.
 Qed.
 
@@ -205,7 +206,7 @@ Proof.
   intros.
   case_eq (eqb a b); intros.
   { eapply eqb_iff; trivial. }
-  { specialize (eqb_iff a b). rewrite H in eqb_iff. intuition. }
+  { specialize (eqb_iff a b). rewrite H in eqb_iff. intuition auto with bool. }
 Qed.
 
 Definition eqb_eq_dec {T} (eqb:T->T->bool) (eqb_iff:forall a b, eqb a b = true <-> a = b) :
@@ -281,4 +282,4 @@ End with_unqualified_modulo2.
 Lemma F_eqb_iff {q} : forall x y : F q, F_eqb x y = true <-> x = y.
 Proof.
   split; eauto using F_eqb_eq, F_eqb_complete.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/src/Experiments/GenericFieldPow.v b/src/Experiments/GenericFieldPow.v
index b3d83dbe8..0fe092f6a 100644
--- a/src/Experiments/GenericFieldPow.v
+++ b/src/Experiments/GenericFieldPow.v
@@ -1,5 +1,6 @@
 Require Import Coq.setoid_ring.Cring.
 Require Import Coq.omega.Omega.
+Require Export Crypto.Util.FixCoqMistakes.
 Generalizable All Variables.
 
 
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v
index a1d47ae8f..be9307b50 100644
--- a/src/ModularArithmetic/ModularArithmeticTheorems.v
+++ b/src/ModularArithmetic/ModularArithmeticTheorems.v
@@ -9,6 +9,8 @@ Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid.
 Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Field_theory Coq.setoid_ring.Field_tac.
 Require Export Crypto.Util.IterAssocOp.
 
+Require Export Crypto.Util.FixCoqMistakes.
+
 Section ModularArithmeticPreliminaries.
   Context {m:Z}.
   Let ZToFm := ZToField : BinNums.Z -> F m. Hint Unfold ZToFm. Local Coercion ZToFm : Z >-> F.
@@ -76,13 +78,16 @@ Ltac eq_remove_proofs := lazymatch goal with
     simpl in *; apply Q; clear Q
 end.
 
+(** TODO FIXME(from jgross): This tactic is way too powerful for
+    arcane reasons.  It should not be using so many databases with
+    [intuition]. *)
 Ltac Fdefn :=
   intros;
   repeat match goal with [ x : F _ |- _ ] => destruct x end;
   try eq_remove_proofs;
   demod;
   rewrite ?Z.mul_1_l;
-  intuition; demod; try solve [ f_equal; intuition ].
+  intuition auto with zarith lia relations typeclass_instances; demod; try solve [ f_equal; intuition auto with zarith lia relations typeclass_instances ].
 
 Local Open Scope F_scope.
 
@@ -139,7 +144,7 @@ Section FandZ.
 
   Lemma ZToField_small_nonzero : forall z, (0 < z < m)%Z -> ZToField z <> (0:F m).
   Proof.
-    intuition; find_inversion; rewrite ?Z.mod_0_l, ?Z.mod_small in *; intuition.
+    intuition; find_inversion; rewrite ?Z.mod_0_l, ?Z.mod_small in *; intuition auto with zarith.
   Qed.
 
   Require Crypto.Algebra.
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index 436d309c7..5f748e0f6 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -16,6 +16,7 @@ Import ListNotations.
 Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
 Require Import Coq.QArith.QArith Coq.QArith.Qround.
 Require Import Crypto.Tactics.VerdiTactics.
+Require Export Crypto.Util.FixCoqMistakes.
 Local Open Scope Z.
 
 Class SubtractionCoefficient (m : Z) (prm : PseudoMersenneBaseParams m) := {
@@ -702,4 +703,4 @@ Section Canonicalization.
     auto using freeze_opt_preserves_rep.
   Qed.
 *)
-End Canonicalization.
\ No newline at end of file
+End Canonicalization.
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index 01c073f06..2baf2ccc2 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -17,6 +17,7 @@ Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil Crypt
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.Notations.
+Require Export Crypto.Util.FixCoqMistakes.
 Local Open Scope Z_scope.
 
 Local Opaque add_to_nth carry_simple.
diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v
index 4b616c288..da9bbac0d 100644
--- a/src/ModularArithmetic/Pow2BaseProofs.v
+++ b/src/ModularArithmetic/Pow2BaseProofs.v
@@ -4,6 +4,7 @@ Require Import Coq.Lists.List.
 Require Import Crypto.Util.ListUtil Crypto.Util.ZUtil Crypto.Util.NatUtil.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.ModularArithmetic.Pow2Base Crypto.BaseSystemProofs.
+Require Export Crypto.Util.FixCoqMistakes.
 Require Crypto.BaseSystem.
 Local Open Scope Z_scope.
 
@@ -779,7 +780,7 @@ Section carrying.
   (* TODO : move? *)
   Lemma make_chain_lt : forall x i : nat, In i (make_chain x) -> (i < x)%nat.
   Proof.
-    induction x; simpl; intuition.
+    induction x; simpl; intuition auto with arith lia.
   Qed.
 
   Lemma nth_default_carry_gen_full fc fi d i n us
diff --git a/src/ModularArithmetic/Pre.v b/src/ModularArithmetic/Pre.v
index 5e61278f6..8566d30ab 100644
--- a/src/ModularArithmetic/Pre.v
+++ b/src/ModularArithmetic/Pre.v
@@ -5,6 +5,7 @@ Require Import Crypto.Tactics.VerdiTactics.
 Require Import Coq.omega.Omega.
 Require Import Crypto.Util.NumTheoryUtil.
 Require Import Crypto.Tactics.VerdiTactics.
+Require Export Crypto.Util.FixCoqMistakes.
 
 Lemma Z_mod_mod x m : x mod m = (x mod m) mod m.
   symmetry.
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v
index 8d594e8ce..8d47e36ed 100644
--- a/src/ModularArithmetic/PrimeFieldTheorems.v
+++ b/src/ModularArithmetic/PrimeFieldTheorems.v
@@ -10,6 +10,7 @@ Require Import Coq.ZArith.BinInt Coq.NArith.BinNat Coq.ZArith.ZArith Coq.ZArith.
 Require Import Coq.Logic.Eqdep_dec.
 Require Import Crypto.Util.NumTheoryUtil Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tactics.
+Require Export Crypto.Util.FixCoqMistakes.
 Require Crypto.Algebra.
 
 Existing Class prime.
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 83ec603a0..aa8093308 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) :=
@@ -300,3 +301,24 @@ Tactic Notation "rewrite_hyp" "<-" "?*" "in" "*" := repeat do_with_hyp' ltac:(fu
 Tactic Notation "rewrite_hyp" "!*" "in" "*" := progress rewrite_hyp ?* in *.
 Tactic Notation "rewrite_hyp" "->" "!*" "in" "*" := progress rewrite_hyp -> ?* in *.
 Tactic Notation "rewrite_hyp" "<-" "!*" "in" "*" := progress rewrite_hyp <- ?* in *.
+
+(** Execute [progress tac] on all subterms of the goal.  Useful for things like [ring_simplify]. *)
+Ltac tac_on_subterms tac :=
+  repeat match goal with
+         | [ |- context[?t] ]
+           => progress tac t
+         end.
+
+(** Like [Coq.Program.Tactics.revert_last], but only for non-dependent hypotheses *)
+Ltac revert_last_nondep :=
+  match goal with
+  | [ H : _ |- _ ]
+    => lazymatch goal with
+       | [ H' : appcontext[H] |- _ ] => fail
+       | [ |- appcontext[H] ] => fail
+       | _ => idtac
+       end;
+       revert H
+  end.
+
+Ltac reverse_nondep := repeat revert_last_nondep.
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 5811aa1a8..20fd446e8 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.
 
@@ -14,28 +15,37 @@ Hint Extern 1 => lia : lia.
 Hint Extern 1 => lra : lra.
 Hint Extern 1 => nia : nia.
 Hint Extern 1 => omega : omega.
-Hint Resolve Z.log2_nonneg Z.div_small Z.mod_small Z.pow_neg_r Z.pow_0_l Z.pow_pos_nonneg Z.lt_le_incl Z.pow_nonzero : zarith.
+Hint Resolve Z.log2_nonneg Z.div_small Z.mod_small Z.pow_neg_r Z.pow_0_l Z.pow_pos_nonneg Z.lt_le_incl Z.pow_nonzero Z.div_le_upper_bound Z_div_exact_full_2 Z.div_same : zarith.
 Hint Resolve (fun a b H => proj1 (Z.mod_pos_bound a b H)) (fun a b H => proj2 (Z.mod_pos_bound a b H)) : zarith.
 
 (** Only hints that are always safe to apply (i.e., reversible), and
     which can reasonably be said to "simplify" the goal, should go in
     this database. *)
 Create HintDb zsimplify discriminated.
-Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r Z.opp_involutive Z.sub_0_r : zsimplify.
+Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r Z.opp_involutive Z.sub_0_r Z_mod_same_full Z.sub_simpl_r Z.sub_simpl_l : zsimplify.
 Hint Rewrite Z.div_mul Z.div_1_l Z.div_same Z.mod_same Z.div_small Z.mod_small Z.div_add Z.div_add_l Z.mod_add Z.div_0_l using lia : zsimplify.
 
 (** "push" means transform [-f x] to [f (-x)]; "pull" means go the other way *)
 Create HintDb push_Zopp discriminated.
 Create HintDb pull_Zopp discriminated.
+Create HintDb push_Zpow discriminated.
+Create HintDb pull_Zpow discriminated.
+Create HintDb push_Zmul discriminated.
+Create HintDb pull_Zmul discriminated.
+Hint Extern 1 => autorewrite with push_Zopp in * : push_Zopp.
+Hint Extern 1 => autorewrite with pull_Zopp in * : pull_Zopp.
+Hint Extern 1 => autorewrite with push_Zpow in * : push_Zpow.
+Hint Extern 1 => autorewrite with pull_Zpow in * : pull_Zpow.
+Hint Extern 1 => autorewrite with push_Zmul in * : push_Zmul.
+Hint Extern 1 => autorewrite with pull_Zmul in * : pull_Zmul.
 Hint Rewrite Z.div_opp_l_nz Z.div_opp_l_z using lia : pull_Zopp.
 Hint Rewrite Z.mul_opp_l : pull_Zopp.
 Hint Rewrite <- Z.opp_add_distr : pull_Zopp.
 Hint Rewrite <- Z.div_opp_l_nz Z.div_opp_l_z using lia : push_Zopp.
 Hint Rewrite <- Z.mul_opp_l : push_Zopp.
 Hint Rewrite Z.opp_add_distr : push_Zopp.
-
-Create HintDb push_Zmul discriminated.
-Create HintDb pull_Zmul discriminated.
+Hint Rewrite Z.pow_sub_r Z.pow_div_l Z.pow_twice_r Z.pow_mul_l Z.pow_add_r using lia : push_Zpow.
+Hint Rewrite <- Z.pow_sub_r Z.pow_div_l Z.pow_mul_l Z.pow_add_r Z.pow_twice_r using lia : pull_Zpow.
 Hint Rewrite Z.mul_add_distr_l Z.mul_add_distr_r Z.mul_sub_distr_l Z.mul_sub_distr_r : push_Zmul.
 Hint Rewrite <- Z.mul_add_distr_l Z.mul_add_distr_r Z.mul_sub_distr_l Z.mul_sub_distr_r : pull_Zmul.
 
@@ -68,7 +78,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 +182,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.
 
@@ -429,7 +439,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.
@@ -568,7 +578,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.
 
@@ -990,20 +1000,45 @@ Module Z.
 
   Hint Rewrite Z.div_mul_skip Z.div_mul_skip' using lia : zsimplify.
 
-  Lemma div_small_neg x y : 0 < -x < y -> x / y = -1.
+  Lemma mod_eq_le_to_eq a b : 0 < a <= b -> a mod b = 0 -> a = b.
+  Proof.
+    intros H H'.
+    assert (a = b * (a / b)) by auto with zarith lia.
+    assert (a / b = 1) by nia.
+    nia.
+  Qed.
+  Hint Resolve mod_eq_le_to_eq : zarith.
+
+  Lemma div_same' a b : b <> 0 -> a = b -> a / b = 1.
+  Proof.
+    intros; subst; auto with zarith.
+  Qed.
+  Hint Resolve div_same' : zarith.
+
+  Lemma mod_eq_le_div_1 a b : 0 < a <= b -> a mod b = 0 -> a / b = 1.
+  Proof. auto with zarith. Qed.
+  Hint Resolve mod_eq_le_div_1 : zarith.
+  Hint Rewrite mod_eq_le_div_1 using lia : zsimplify.
+
+  Lemma mod_neq_0_le_to_neq a b : a mod b <> 0 -> a <> b.
+  Proof. repeat intro; subst; autorewrite with zsimplify in *; lia. Qed.
+  Hint Resolve mod_neq_0_le_to_neq : zarith.
+
+  Lemma div_small_neg x y : 0 < -x <= y -> x / y = -1.
   Proof.
     intro H; rewrite <- (Z.opp_involutive x).
     rewrite Z.div_opp_l_complete by lia.
     generalize dependent (-x); clear x; intros x H.
-    autorewrite with zsimplify; edestruct Z_zerop; lia.
+    pose proof (mod_neq_0_le_to_neq x y).
+    autorewrite with zsimplify; edestruct Z_zerop; autorewrite with zsimplify in *; lia.
   Qed.
   Hint Rewrite div_small_neg using lia : zsimplify.
 
-  Lemma div_sub_small x y z : 0 <= x < z -> 0 <= y < z -> (x - y) / z = if x <? y then -1 else 0.
+  Lemma div_sub_small x y z : 0 <= x < z -> 0 <= y <= z -> (x - y) / z = if x <? y then -1 else 0.
   Proof.
     pose proof (Zlt_cases x y).
     (destruct (x <? y) eqn:?);
-      intros; autorewrite with zsimplify; lia.
+      intros; autorewrite with zsimplify; try lia.
   Qed.
   Hint Rewrite div_sub_small using lia : zsimplify.
 
@@ -1016,6 +1051,24 @@ Module Z.
     auto with zarith.
   Qed.
   Hint Resolve mul_div_lt_by_le : zarith.
+
+  Definition pow_sub_r'
+    := fun a b c y H0 H1 => @Logic.eq_trans _ _ _ y (@Z.pow_sub_r a b c H0 H1).
+  Definition pow_sub_r'_sym
+    := fun a b c y p H0 H1 => Logic.eq_sym (@Logic.eq_trans _ y _ _ (Logic.eq_sym p) (@Z.pow_sub_r a b c H0 H1)).
+  Hint Resolve pow_sub_r' pow_sub_r'_sym Z.eq_le_incl : zarith.
+  Hint Resolve (fun b => f_equal (fun e => b ^ e)) (fun e => f_equal (fun b => b ^ e)) : zarith.
+  Definition mul_div_le'
+    := fun x y z w p H0 H1 H2 H3 => @Z.le_trans _ _ w (@Z.mul_div_le x y z H0 H1 H2 H3) p.
+  Hint Resolve mul_div_le' : zarith.
+
+  Lemma two_p_two_eq_four : 2^(2) = 4.
+  Proof. reflexivity. Qed.
+  Hint Rewrite <- two_p_two_eq_four : push_Zpow.
+
+  Lemma two_sub_sub_inner_sub x y z : 2 * x - y - (x - z) = x - y + z.
+  Proof. clear; lia. Qed.
+  Hint Rewrite two_sub_sub_inner_sub : zsimplify.
 End Z.
 
 Module Export BoundsTactics.