The Coq mailing list

[Tom Prince <tom.prince AT ualberta.net>]

On 2011-05-06, Daniel Schepler wrote:
> On Friday 06 May 2011 00:54:46 Robbert Krebbers wrote:
> 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 just implemented this the other day for categories.dual.flipA (from
math-classes). I don't know of a better way, or how to implement it without 
the
extraneous let. I think though, you probably want to make
BlcokCommutesWithRev a CoInductive (I got the idea from
Classes.Morphisms.normalization_done. The benifit of CoInductive is that
it isn't convertible with anything, but does generate any induction
principles.

I don't think the extraneous let is a problem for CommutesWith, since
the structure of proof terms doesn't matter.

In my case however, the class lives in Type, so I care which case is
picked. I want it deduced where other things force it, but if I do the
following, then when I try to get it to deduce something that isn't
constrained as dual.flipA, it still applies the tactic.

Class Arrows (O: Type): Type := Arrow: O → O → Type.
Instance flipA {Object} {A: Arrows Object}: Arrows Object := flip A.
CoInductive dual_arrows_done (T: Type) : Prop := did_dual_arrows.             
           
Hint Extern 100 (Arrows ?x) => match goal with                                
           
                                 | _ : dual_arrows_done x |- _ => fail 1      
           
                                 | |- _ => let H:=fresh "H" in set 
(H:=did_dual_arrows x); class_apply @flipA
                               end : typeclass_instances.  

  Tom

P.S. The development of math-classes is open, so if you are building on
top of it, we would like to fold back in any improvements.