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

Question

I am working on a proof, and one of my subgoals looks something 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 is independent of any external lemmas and simply consists in applying one hypothesis in context to another hypothesis and performing rewriting steps with a known hypothesis.

Is there a way to automate this? I tried to do it intros. auto., but it didn’t affect. I suspect this is because it autocan only perform steps apply, but not rewrite, but I'm not sure. Maybe I need a stronger tactic?

The reason I want to automate this is because in my original problem I really have a lot of sub-goals that are very similar to this, but with slight differences in the names of the hypotheses (H1, H2, etc.), the number of hypotheses (sometimes there is an additional hypothesis of induction or two) and the Boolean formula at the end. I think that if I could use automation to solve this problem, my general proof of the script would be more concise and reliable.

---

edit: What if forall is in one of the hypotheses?

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 repeating pattern in the way you prove some lemmas, you can often define your own tactics for automating evidence.

:

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.

, ( ) CPDT .

Answer 2

:

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

, destruct_all ( , ):

intros; destruct_all bool; intuition.

destr_bool, Coq.Bool.Bool:

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

-

destr_bool; intuition.

intuition destr_bool.

---

now Coq.Init.Tactics

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

easy ( ) .

intuition , () . . modus ponens.

H1 : p -> false = true
H2 : p

auto, , , .

, firstorder ( ) - intuition .