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
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.
rewrite aO in *work, if this extra lemma is acceptable? $\endgroup$
changein full: you only need to give a pattern that matches what you want to
changein the target. $\endgroup$
simplcan 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"). $\endgroup$