The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

I've been trying to extract and add to selected portions of MathClasses for some proof formalization I'm doing.  I ran into a problem in this:

Program Instance Ring_Semiring `{Ring R} : Semiring R.
Solve Obligations using repeat (typeclasses eauto || constructor).
Next Obligation.
intro x.
apply (left_cancel (x:=mult0 zero x) (op:=plus0)).
rewrite <- distr_l.
repeat rewrite (_:RightIdentity plus0 zero).
reflexivity.
Qed.
Next Obligation.
intro x.
apply (left_cancel (x:=mult0 x zero) (op:=plus0)).
rewrite <- distr_r.
repeat rewrite (_:RightIdentity plus0 zero).
reflexivity.
Qed.

Here I really wanted to use "repeat rewrite right_identity" instead of "repeat rewrite (_:RightIdentity plus0 zero)".  But for some reason that doesn't work: it does nothing, and the plain rewrite just displays "Found no subterm matching "?54072 ?65488 ?54073" in the current goal".  It even turns out that with "Check right_identity." the first instance it finds is exactly the one I want.  And if I "pose proof right_identity as H1; repeat rewrite H1" that works.

Does anybody have any ideas off the top of their heads why this might be happening?  I can send the whole file via private email if you want, but it's a bit large to post on the list.
-- 
Daniel Schepler