The Coq mailing list

["Andrew McCreight" <continuation AT gmail.com>]

There actually is a similar question, further down the list: "How can I prove that two constructors are different?"  It does not go into any detail, though.  But generally, the FAQ is a good starting point, as it will give you the name of a tactic.  Then you can switch over to the manual and read up on the details.  I think the manual has examples and talks about how discriminate is implemented, as Stefan described.

-Andrew

On Wed, Sep 24, 2008 at 2:44 AM, Yves Bertot <Yves.Bertot AT sophia.inria.fr> wrote:

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