Feeding rewrites and other hints into an omnibus tactic

Question

How do I feed rewrites that I've marked as safe into a custom tactic?

---

I'm trying to write shorter Coq proofs with more of the easy stuff hidden. To that end, in the script below I proved that (a + b) * (c + d) = a * c + a * d + b * c + b * d.

To that end, I wrote a tactic f, the intent of which is to make uninformative steps stand out less in the proof. I am okay with f being brittle and using every hint database, for example. I am also okay with f behaving differently over time as new rewrites get added to the database that it has access to. f probably shouldn't be exported because its behavior is too unpredictable, but I'm okay with it in a single file.

Ideally, I want f to have a happy path that finishes a goal, and a sad path that just applies simpl and some rewrites that I've explicitly marked. In the proof script below, I've tried to mark add_assoc, because rewriting according to associativity will terminate eventually, but I didn't mark add_comm because it'll just flip two things back and forth forever.

I tried using Hint Rewrite [name of theorem] as a way of shoveling additional rewrites into f, but I can't figure out how to get f to pick them up.

From Coq Require Import Setoid.

Ltac f := simpl; try easy; try intuition auto with *; try intuition eauto with *.

Lemma mul_0_r : forall a, a * 0 = 0.
Proof. f. Qed.
Hint Rewrite mul_0_r.

Lemma add_0_r : forall a, a + 0 = a.
Proof. f. Qed.
Hint Rewrite add_0_r.

(* we choose as a strategy moving all successors to the leftmost argument position *)
Lemma add_succ_r : forall a b, a + S b = S (a + b).
Proof. f. Qed.
Hint Rewrite add_succ_r.

Let add_assoc : forall a b c, a + (b + c) = a + b + c.
  intros a b c.
  induction a.
  all:f.
Qed.
Hint Rewrite add_assoc.

Lemma add_comm : forall a b, a + b = b + a.
Proof. f. induction a. f. f. rewrite IHa. f.
Qed.

Lemma four_add_swapper : forall a b c d, a + b + c + d = a + c + b + d.
Proof.
  intros.
  induction a.
  simpl.
  setoid_rewrite add_comm at 2.
  all:f.
Qed.

Lemma right_distributivity: forall b c d, b * (c + d) = b * c + b * d.
Proof.
  f. induction b. f. f. rewrite IHb. repeat rewrite add_assoc.
  rewrite four_add_swapper. f.
Qed.
Hint Rewrite right_distributivity.

Lemma six_add_swapper:
  forall x y z w v u, x + y + z + w + v + u = x + z + y + w + v + u.
Proof.
  intros.
  induction y.
  repeat rewrite add_0_r.
  f.
  repeat rewrite add_succ_r || rewrite add_assoc.
  f.
Qed.

Theorem full_distributivity:
  forall a b c d, (a + b) * (c + d) = a * c + a * d + b * c + b * d.
Proof.
  intros a b c d.
  induction a. f.
  pose right_distributivity. f.
  simpl.
  rewrite IHa.
  repeat rewrite add_assoc.
  pose six_add_swapper. f.
Qed.
Hint Rewrite full_distributivity.

```

Answer 1

To use rewriting hints from a hint database, you should use autorewrite (probably with the with keyword to pick a database). Here is how to tweak you example:

From Coq Require Import Setoid.

Create HintDb my_db.

#[local] Ltac f := simpl; autorewrite with my_db ; intuition eauto with *.

Lemma mul_0_r : forall a, a * 0 = 0.
Proof. eauto. Qed.
Hint Rewrite mul_0_r : my_db.

Lemma add_0_r : forall a, a + 0 = a.
Proof. f. Qed.
Hint Rewrite add_0_r : my_db.

(* we choose as a strategy moving all successors to the leftmost argument position *)
Lemma add_succ_r : forall a b, a + S b = S (a + b).
Proof. f. Qed.
Hint Rewrite add_succ_r : my_db.

Lemma add_assoc : forall a b c, a + (b + c) = a + b + c.
  intros a b c.
  induction a.
  all:f.
Qed.
Hint Rewrite add_assoc : my_db.

Lemma add_comm : forall a b, a + b = b + a.
Proof. f. induction a. f. f. rewrite IHa. f.
Qed.

Lemma four_add_swapper : forall a b c d, a + b + c + d = a + c + b + d.
Proof.
  intros.
  induction a.
  simpl.
  setoid_rewrite add_comm at 2.
  all:f.
Qed.

Lemma right_distributivity: forall b c d, b * (c + d) = b * c + b * d.
Proof.
  f. induction b. f. f. rewrite IHb. repeat rewrite add_assoc.
  rewrite four_add_swapper. f.
Qed.
Hint Rewrite right_distributivity : my_db.

Lemma six_add_swapper:
  forall x y z w v u, x + y + z + w + v + u = x + z + y + w + v + u.
Proof.
  intros.
  induction y.
  repeat rewrite add_0_r.
  f.
  repeat rewrite add_succ_r || rewrite add_assoc.
  f.
Qed.

Theorem full_distributivity:
  forall a b c d, (a + b) * (c + d) = a * c + a * d + b * c + b * d.
Proof.
  intros a b c d.
  induction a. f.
  simpl.
  rewrite IHa.
  f.
  now rewrite six_add_swapper.
Qed.
Hint Rewrite full_distributivity : my_db.

Due to the combination of using 1) a #[local] tactic and 2) a custom hint database, this should be very innocuous to the outside, at least until someone tries to define/use a database with the exact same name as yours. But even in that case there are solutions, using the new import categories (concretely you can use Require Import -(hints) Foo. to avoid importing hints from Foo).