# Rewrite with definitional equality and dependent types

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.

• What about simpl? Mar 23 at 9:18
• Also, does rewrite aO in * work, if this extra lemma is acceptable? Mar 23 at 9:20
• Just a remark, but maybe you know this already: you do not always need to spell out the source of change in full: you only need to give a pattern that matches what you want to change in the target. Mar 23 at 9:57
• @mudri: simpl can only do certain conversions, and it sometimes does too much or too little. rewrite aO in * doesn't work at all (Coq just says "nothing to rewrite"). Mar 23 at 17:42

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.

• I already mentioned this in the last paragraph of my question: sometimes the terms being converted are quite large and I would rather not have to type them out. Mar 23 at 5:00
• @sudgy So it would not be a Definition, but some arbitrary term in need of changing to some other arbitrary term, right? I don't see how you could provide these two terms apart from writing them out... I mean, how should Coq figure out which two terms to rewrite, if you don't write them out, at least somewhere?
– Trebor
Mar 23 at 5:24
• rewrite with a separate theorem figures it out what I want to do just fine. It just doesn't work with dependent types. Mar 23 at 6:17
• @sudgy But you still need to write out what you want to rewrite for rewrite as a theorem. So do you mean you want the ability for Coq to correctly instantiate a theorem for you?
– Trebor
Mar 23 at 8:05
• I feel like my real life examples are way too complicated to describe easily here (you can try searching through github.com/sudgy/math-from-nothing but honestly I would advise against it). I'm fine with writing complicated things out in the statement of a theorem manually. I just don't like huge changes in the middle of a proof. Mar 23 at 17:39

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.

• This doesn't work when the thing you are trying to change is not just a simple definition. Mar 23 at 6:27
• As mentioned in the other answer, if you have complicated expressions which aren't simple definitions, there's no way for Coq to guess which expression you want to change into which other expression, so you'll have to specify the expressions regardless. The "rewrite -[a]/b" syntax works whenever you specify the expressions.
– djao
Mar 25 at 23:24

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.

• Not an answer but it seems likely to extend this using ltac: apply the theorem to evars, (optionally, unify the LHS against arbitrary subterms using match goal and context), then change with the RHS. Mar 24 at 12:47
• @Blaisorblade I'm not that great with ltac, could you expand on that? Mar 24 at 17:45