The Coq mailing list

[Robbert Krebbers <mail AT robbertkrebbers.nl>]

Hi,

I think it is because you don't refer to the "canonical names" of the 
operations. So, instead of:
 apply (left_cancel (x:=mult0 zero x) (op:=plus0)).
you should write:
 apply (left_cancel (x:=0 * x) (op:=(+))).

The problem is that you probably have an instance (theory.rings.plus_0_l in 
mathclasses) like:
  RightIdentity (@ring_plus R plus0) (@ring_zero R zero)
However, if your goal contains (plus0 zero zero), the system won't be able to 
figure out that it matches.

Moreover, there is another reason to refer to the canonical names: the names (plus0, mult0, zero) are automatically 
generated and hence very fragile. So I would prove the LeftAbsorb property as follows:

Require Import abstract_algebra theory.rings.

Instance ring_mult_0_r `{Ring R} : LeftAbsorb (.*.) 0.
Proof.
  intros x.
  apply (left_cancellation (+) (0 * x)).
  rewrite <-distribute_r.
  rewrite !right_identity.
  reflexivity.
Qed.

Best,

Robbert

On 05/06/2011 04:00 AM, Daniel Schepler wrote:
> 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