The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hi,

  I don't think there is a better solution yet either. However I'm working
on adding a feature that would allow the user to specify cuts in the proof
search using regular expressions on paths to forbid. I think it would solve
this particular problem.

Le 6 mai 2011 à 20:44, Tom Prince a écrit :

> 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.  
> 

  There is no way to tell if a flipA should be triggerd here, is there? 
If you had a dummy [flipObject] definition to act as an index you could 
control its application using an [Arrows (flipObject ?x)] pattern, but
I guess you don't want that.

-- Matthieu