The Coq mailing list

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

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?", 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.)

http://coq.inria.fr/V8.1/faq.html

On Tue, Sep 23, 2008 at 8:57 AM, Serge Leblanc <serge.leblanc AT wanadoo.fr> wrote:

Is there a tutorial showing the typical conditions of use of a tactic?
Like the table from the chapter 5.4, page 130 of Coq'Art.

Sincery,





On mar, 2008-09-23 at 15:42 +0200, Pierre Casteran wrote:

>   
If you print for instance Gt.
Coq < Print Gt.
Inductive comparison : Set :=
    Eq : comparison | Lt : comparison | Gt : comparison

You notice that Gt and Eq are distinct constructors of the inductive type
comparison.

Then the tactic discriminate expresses this fact:

Coq < Lemma diff : Eq <> Gt.
1 subgoal
 
  ============================
   Eq <> Gt

diff < discriminate.
Proof completed.

diff < Qed.

Pierre

--
Serge Leblanc
gpg --keyserver hkp://subkeys.pgp.net --recv-keys 0x73791C2B
Fingerprint: 8E0C 0D6D E026 A278 9278 BF4F 1A93 D552 7379 1C2B