The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Andrew McCreight wrote:
> Section 6 of the Coq FAQ is very useful for these sorts of things.  It has a
> series of questions like " My goal is a conjunction, how can I prove
> it?<http://coq.inria.fr/V8.1/faq.html#htoc53>",
> which is useful when you have some goal you want to prove, but no idea what
> tactic should be used.  (That's kind of the opposite of what you asked for,
> but I think knowing what tactic solves a particular goal is more useful when
> starting out than knowing what a particular tactic does.)
>   
I did not know that this faq existed.  The only point here is that there 
appears to
be no question corresponding to a use of discriminate, something like:

"My goal is a disequality, how can I prove it?"

and the answer would be:

"in many cases, disequalities relate directly two constructors of an 
inductive type,
in these case you can use the "discriminate" tactic.  If you don't know 
whether the
two members of your disequality are constructors, calling discriminate 
is still worth a
try."

Going much more into details, about the difference between constructors 
and other
functions, etc. requires a long answer, probably not adapted to a faq 
(although
some of the answers of the current faq are quite long, because they 
contain examples).