Is there a way to automate a Coq proof with rewrite steps?

Question

I am working on a proof and one of my subgoals looks a bit like this:

Goal forall
  (a b : bool)
  (p: Prop)
  (H1: p -> a = b)
  (H2: p),
  negb a = negb b.
Proof.
  intros.
  apply H1 in H2. rewrite H2. reflexivity.
Qed.

The proof does not rely on any outside lemmas and just consists of applying one hypothesis in the context to another hypothesis and doing rewriting steps with a known hypothesis.

Is there a way to automate this? I tried doing intros. auto. but it had no effect. I suspect that this is because auto can only do apply steps but no rewrite steps but I am not sure. Maybe I need some stronger tactic?

The reason I want to automate this is that in my original problem I actually have a large number of subgoals that are very similar to this one, but with small differences in the names of the hypotheses (H1, H2, etc), the number of hypotheses (sometimes there is an extra induction hypothesis or two) and the boolean formula at the end. I think that if I could use automation to solve this my overall proof script would be more concise and robust.

---

edit: What if there is a forall in one of the hypothesis?

Goal forall
  (a b c : bool)
  (p: bool -> Prop)
  (H1: forall x, p x -> a = b)
  (H2: p c),
  negb a = negb b.
Proof.
  intros.
  apply H1 in H2. subst. reflexivity.
Qed

Answer 1

When you see a repetitive pattern in the way you prove some lemmas, you can often define your own tactics to automate the proofs.

In your specific case, you could write the following:

Ltac rewrite_all' :=
  match goal with
  | H  : _ |- _ => rewrite H; rewrite_all'
  | _ => idtac
 end.

Ltac apply_in_all :=
  match goal with
  | H  : _, H2 : _ |- _ => apply H in H2; apply_in_all
  | _ => idtac
 end.

Ltac my_tac :=
  intros;
  apply_in_all;
  rewrite_all';
  auto.

Goal forall (a b : bool) (p: Prop) (H1: p -> a = b) (H2: p), negb a = negb b.
Proof.
  my_tac.
Qed.

Goal forall (a b c : bool) (p: bool -> Prop)
  (H1: forall x, p x -> a = b)
  (H2: p c),
  negb a = negb b.
Proof.
  my_tac.
Qed.

If you want to follow this path of writing proofs, a reference that is often recommended (but that I haven't read) is CPDT by Adam Chlipala.

Answer 2

This particular goal can be solved like this:

Goal forall (a b : bool) (p: Prop) (H1: p -> a = b) (H2: p),
  negb a = negb b.
Proof.
  now intuition; subst.
Qed.

Or, using the destruct_all tactic (provided you don't have a lot of boolean variables):

intros; destruct_all bool; intuition.

The above has been modeled after the destr_bool tactic, defined in Coq.Bool.Bool:

Ltac destr_bool :=
  intros; destruct_all bool; simpl in *; trivial; try discriminate.  

You could also try using something like

destr_bool; intuition.

to fire up powerful intuition after simpler destr_bool.

---

now is defined in Coq.Init.Tactics as follows

Tactic Notation "now" tactic(t) := t; easy.

easy is defined right above it and (as its name suggests) can solve easy goals.

intuition can solve goals which require applying the laws of (intuitionistic) logic. E.g. the following two hypotheses from the original version of the question require an application of the modus ponens law.

H1 : p -> false = true
H2 : p

auto, on the other hand, doesn't do that by default, it also doesn't solve contradictions.

If your hypotheses include some first-order logic statements, the firstorder tactic may be the answer (like in this case) -- just replace intuition with it.