The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Friday 06 May 2011 00:54:46 Robbert Krebbers wrote:
> 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:=(+))).

Thanks, indeed first doing a "change (0*x==0)" and then using canonical names 
did seem to work.

Now, my next question: I have a class and instances:

Class CommutesWith `{Eqv X} (op:X->X->X) (x y:X) : Prop :=
| commutes_with: op x y == op y x.

Program Instance CommutesWithSelf `{Eqv X} `{!Reflexive eqv} x :
  CommutesWith op x x.

Program Lemma CommutesWithRev `{Eqv X} `{!Symmetric eqv}
  `{!CommutesWith op x y} : CommutesWith op y x.

It seems that directly making the last one into an instance creates loops, 
which is understandable.  My solution to this was:

Definition BlockCommutesWithRev {X} (op:X->X->X) (x y:X) : Prop := True.
Ltac try_CommutesWithRev :=
  match goal with
  | [ _:BlockCommutesWithRev ?op ?x ?y |- CommutesWith ?op ?x ?y ] => fail 1
  | [ |- CommutesWith ?op ?x ?y ] =>
       pose proof (I:BlockCommutesWithRev op y x);
           class_apply @CommutesWithRev
  end.
Hint Extern 10 (CommutesWith _ _ _) => try_CommutesWithRev :
  typeclass_instances.

I was wondering if there was some easier way to accomplish this.  Or at least 
a way that would avoid creating the extraneous "let H2:=I in ..." that 
results 
in the generated proof terms.  (I see in the original MathClasses files I 
downloaded, there was a commented question about similar things for 
LeftIdentity -> Commutative -> RightIdentity and vice versa.)
-- 
Daniel Schepler