The Coq mailing list

[Serge Leblanc <serge.leblanc AT wanadoo.fr>]

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

Attachment: signature.asc
Description: This is a digitally signed message part