The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 12/24/2014 06:44 PM, Abhishek Anand wrote:
> The lemma you are looking for is Z_zerop. Here's how I found it:
>
> SearchPattern ( {?z=0} + {?z<>0}).
>
> On bad days, I might have to issue more queries like
> SearchPattern ( {?z<>0} + {?z = 0}).
> SearchPattern ( {?z<>0} + {0 = ?z}).
> .... i.e their might be a lemma with a logically equivalent, but
> syntactically different form.
> My question to Coq gurus : Is there a smarter version of SearchPattern?
>
>   Regards,
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/

I tend to use the minimal covering pattern that wouldn't produce too 
many extra matches to look through - like

SearchPattern (which is ^C-^A-^O in PG) ({_} + {_}).

Then, since I'm using PG, I can incrementally search the result. It's 
also interesting to see the near misses - as one can get a feel for 
things like naming conventions.

-- Jonathan