The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

Dear Coq-ers,

what is the status of the command:

  Hint Cut

that allows one to constraint (e)auto and type class instance search?

It has been introduced by commit 1011266b in November 2011, but has 
never been documented, nor mentioned in any Changelog.

However, it seems exceptionally useful to constraint type class search. 
For example, in our formalization of metric spaces we have the following 
hierarchy of functions:

  Setoid functions (Propers)
  Non-expansive functions
  Contractive functions

All of these are closed under composition. In the case of trying to 
derive a Proper for a function that is in fact not (which happens quite 
often because type class search takes a wrong branch), this gives an 
exponential blow-up. With the use of Hint Cut, this blow-up can be 
avoided, and the search becomes linear in the size of the expression.

I would like to try to make use of this feature, but since it has not 
been documented or mentioned anywhere, I am not sure what will happen 
with it in the future.

I have attached a small example that demonstrates the use of Hint Cut.

Best,

Robbert

Attachment: 20151021_hint_cut.v
Description: application/extension-v