Add useful tactics and util lemmas

3 files changed, 85 insertions, 6 deletions

diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 8260058f1..8823a177e 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -633,11 +633,6 @@ Lemma length_cons : forall {T} (x:T) xs, length (x::xs) = S (length xs).
   reflexivity.
 Qed.
 
-Lemma S_pred_nonzero : forall a, (a > 0 -> S (pred a) = a)%nat.
-Proof.
-  destruct a; omega.
-Qed.
-
 Lemma cons_length : forall A (xs : list A) a, length (a :: xs) = S (length xs).
 Proof.
   auto.
@@ -976,6 +971,14 @@ Qed.
 
 Hint Rewrite @sum_firstn_succ_default : simpl_sum_firstn.
 
+Lemma sum_firstn_0 : forall xs,
+  sum_firstn xs 0 = 0%Z.
+Proof.
+  destruct xs; reflexivity.
+Qed.
+
+Hint Rewrite @sum_firstn_0 : simpl_sum_firstn.
+
 Lemma sum_firstn_succ : forall l i x,
   nth_error l i = Some x ->
   sum_firstn l (S i) = (x + sum_firstn l i)%Z.
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v
index c8a6e8247..02122719e 100644
--- a/src/Util/NatUtil.v
+++ b/src/Util/NatUtil.v
@@ -1,10 +1,14 @@
+Require Coq.Logic.Eqdep_dec.
 Require Import Coq.Numbers.Natural.Peano.NPeano Coq.omega.Omega.
 Require Import Coq.micromega.Psatz.
 Import Nat.
 
 Create HintDb natsimplify discriminated.
 
-Hint Rewrite @Nat.mod_small using omega : natsimplify.
+Hint Resolve mod_bound_pos : arith.
+Hint Resolve (fun x y p q => proj1 (@Nat.mod_bound_pos x y p q)) (fun x y p q => proj2 (@Nat.mod_bound_pos x y p q)) : arith.
+
+Hint Rewrite @mod_small @mod_mod @mod_1_l @mod_1_r succ_pred using omega : natsimplify.
 
 Local Open Scope nat_scope.
 
@@ -134,7 +138,52 @@ Qed.
 
 Hint Resolve pow_nonzero : arith.
 
+Lemma S_pred_nonzero : forall a, (a > 0 -> S (pred a) = a)%nat.
+Proof.
+  destruct a; omega.
+Qed.
+
+Hint Rewrite S_pred_nonzero using omega : natsimplify.
+
 Lemma mod_same_eq a b : a <> 0 -> a = b -> b mod a = 0.
 Proof. intros; subst; apply mod_same; assumption. Qed.
 
 Hint Rewrite @mod_same_eq using omega : natsimplify.
+Hint Resolve mod_same_eq : arith.
+
+Lemma mod_mod_eq a b c : a <> 0 -> b = c mod a -> b mod a = b.
+Proof. intros; subst; autorewrite with natsimplify; reflexivity. Qed.
+
+Hint Rewrite @mod_mod_eq using (reflexivity || omega) : natsimplify.
+
+Local Arguments minus !_ !_.
+
+Lemma S_mod_full a b : a <> 0 -> (S b) mod a = if eq_nat_dec (S (b mod a)) a
+                                               then 0
+                                               else S (b mod a).
+Proof.
+  change (S b) with (1+b); intros.
+  pose proof (mod_bound_pos b a).
+  rewrite add_mod by assumption.
+  destruct (eq_nat_dec (S (b mod a)) a) as [H'|H'];
+    destruct a as [|[|a]]; autorewrite with natsimplify in *;
+      try congruence; try reflexivity.
+Qed.
+
+Hint Rewrite S_mod_full using omega : natsimplify.
+
+Lemma S_mod a b : a <> 0 -> S (b mod a) <> a -> (S b) mod a = S (b mod a).
+Proof.
+  intros; rewrite S_mod_full by assumption.
+  edestruct eq_nat_dec; omega.
+Qed.
+
+Hint Rewrite S_mod using (omega || autorewrite with natsimplify; omega) : natsimplify.
+
+Lemma eq_nat_dec_refl x : eq_nat_dec x x = left (Logic.eq_refl x).
+Proof.
+  edestruct eq_nat_dec; try congruence.
+  apply f_equal, Eqdep_dec.UIP_dec, eq_nat_dec.
+Qed.
+
+Hint Rewrite eq_nat_dec_refl : natsimplify.
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index 304ae3c20..4630e4ab7 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -260,3 +260,30 @@ Ltac side_conditions_before_to_side_conditions_after tac_in H :=
        here, after evars are instantiated, and not above. *)
     move H after H'; clear H'
   | .. ].
+
+(** Do something with every hypothesis. *)
+Ltac do_with_hyp' tac :=
+  match goal with
+    | [ H : _ |- _ ] => tac H
+  end.
+
+(** Rewrite with any applicable hypothesis. *)
+Tactic Notation "rewrite_hyp" "*" := do_with_hyp' ltac:(fun H => rewrite H).
+Tactic Notation "rewrite_hyp" "->" "*" := do_with_hyp' ltac:(fun H => rewrite -> H).
+Tactic Notation "rewrite_hyp" "<-" "*" := do_with_hyp' ltac:(fun H => rewrite <- H).
+Tactic Notation "rewrite_hyp" "?*" := repeat do_with_hyp' ltac:(fun H => rewrite !H).
+Tactic Notation "rewrite_hyp" "->" "?*" := repeat do_with_hyp' ltac:(fun H => rewrite -> !H).
+Tactic Notation "rewrite_hyp" "<-" "?*" := repeat do_with_hyp' ltac:(fun H => rewrite <- !H).
+Tactic Notation "rewrite_hyp" "!*" := progress rewrite_hyp ?*.
+Tactic Notation "rewrite_hyp" "->" "!*" := progress rewrite_hyp -> ?*.
+Tactic Notation "rewrite_hyp" "<-" "!*" := progress rewrite_hyp <- ?*.
+
+Tactic Notation "rewrite_hyp" "*" "in" "*" := do_with_hyp' ltac:(fun H => rewrite H in * ).
+Tactic Notation "rewrite_hyp" "->" "*" "in" "*" := do_with_hyp' ltac:(fun H => rewrite -> H in * ).
+Tactic Notation "rewrite_hyp" "<-" "*" "in" "*" := do_with_hyp' ltac:(fun H => rewrite <- H in * ).
+Tactic Notation "rewrite_hyp" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => rewrite !H in * ).
+Tactic Notation "rewrite_hyp" "->" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => rewrite -> !H in * ).
+Tactic Notation "rewrite_hyp" "<-" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => rewrite <- !H in * ).
+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 *.