Rewrite with definitional equality and dependent types

Question

In Coq, there are some terms that are equal by definition, but there's not an easy way to replace one value with the other inside a proof. The two ways that I know that work in general are to use the change tactic (which can be cumbersome at times), and to make a lemma saying that the two things are equal and then using rewrite. However, the second approach can run into trouble with dependent types, as this example shows:

Definition a := O.

Theorem aO : a = O.
Proof.
  reflexivity.
Qed.

Theorem test : forall (S : nat -> Prop) (H : S O), ex_intro S O H = ex_intro S a H.
Proof.
  intros S H.
  rewrite aO. (* fails *)
Abort.

So, my question is, is there a way to do something like rewrite but that works in this situation? Of course, I could use change (which is what I currently do), but sometimes the terms being converted are quite large and I would rather not have to type them out.

Edit: Since I've now received two answers that aren't what I'm looking for I thought I would clarify this: I'm not talking about simple situations like in the example where it's just a single definition. I only provided the example to clarify what the fundamental issue is. What I'm asking is, given arbitrary, complicated terms A and B such that change A with B works, how can I get around having to write out A and B every time? Without dependent types I can just use a theorem A = B but I don't know of a way to do it with dependent types.

Answer 1

This works:

Theorem test : forall (S : nat -> Prop) (H : S O), ex_intro S O H = ex_intro S a H.
Proof.
  intros S H.
  change a with O.
Abort.

Is this what you need? See the docs. It might be better if you say exactly when you find change cumbersome in the question.

Answer 2

If you have ssreflect:

Definition a := O.

Theorem test : forall (S : nat -> Prop) (H : S O), ex_intro S O H = ex_intro S a H.
Proof.
  intros S H.
  rewrite /a.
  rewrite -/a.

If you don't have ssreflect:

Definition a := O.

Theorem test : forall (S : nat -> Prop) (H : S O), ex_intro S O H = ex_intro S a H.
Proof.
  intros S H.
  unfold a.
  fold a.

Sometimes you have to type the terms out. In this case, use (for example) rewrite -[O]/a.

Answer 3

Maybe I should have thought of this more before asking, but I thought of a solution that's at least better than everything I've thought of so far:

Definition a := O.

Theorem aO : a = O.
Proof.
  reflexivity.
Qed.

Ltac def_rewrite H := match type of H with | ?a = ?b => change a with b end.

Theorem test : forall (S : nat -> Prop) (H : S O), ex_intro S O H = ex_intro S a H.
Proof.
  intros S H.
  def_rewrite aO.
Abort.

However, this solution is not quite as versatile as rewrite is because rewrite can take theorems with parameters and work them out whereas def_rewrite has to take in a theorem with just the form a = b. I'll wait to accept this as the answer in case anybody else can think of a better solution.