coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Andrew McCreight" <continuation AT gmail.com>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] can't work with eq
- Date: Tue, 23 Sep 2008 09:09:17 -0700
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:subject:cc:in-reply-to:mime-version :content-type:references; b=SNgRQjrsj6Gg/yhCjYogKSf0PxgrKgsC7kss232vkwIidrM8zQeUyfw1fVN6KwuOvo 5/j9xZ00uP+G87TqvBL8Z6Zp+/PQONndq0I+3x5P36EZ0K+4GGlqNrMNKgNnvO5A+sBO qt5MOr+9Ui3/ezyM5A/VkKyh8x7Hy7/iWHMlk=
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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
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
- [Coq-Club] can't work with eq, Thomas Nelson
- Re: [Coq-Club] can't work with eq,
Pierre Casteran
- Re: [Coq-Club] can't work with eq,
Serge Leblanc
- Re: [Coq-Club] can't work with eq, Andrew McCreight
- Re: [Coq-Club] can't work with eq,
Yves Bertot
- Re: [Coq-Club] can't work with eq, Andrew McCreight
- Re: [Coq-Club] can't work with eq,
Yves Bertot
- Re: [Coq-Club] can't work with eq, Andrew McCreight
- Re: [Coq-Club] can't work with eq,
Serge Leblanc
- Re: [Coq-Club] can't work with eq, Stefan Monnier
- Re: [Coq-Club] can't work with eq,
Pierre Casteran
Archive powered by MhonArc 2.6.16.