coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proof Help

From: Thomas Braibant <thomas.braibant AT gmail.com>
To: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Proof Help
Date: Tue, 14 Apr 2009 14:11:31 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :content-type:content-transfer-encoding; b=u5FMcziY2HQQnAcRQOLYxNLdCS4zZsTI3Ai7Pvn7WzvDKv+O8mJPwdl3urdNaLhn5e m61zk5KJZBhdMh4qlHpl0dja+NM7lxIFUAFqykxfYRj/l/fsn9b6NDh9pTm0Gf+tUBTy 3BgPfn8bBlhHo3orxaxscJ0OR1iJkp/denP3Q=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

>> I feel like I should jump in and bring up that the built-in [firstorder]
>> tactic solves this goal, so that's the right way to do it in real
>> developments. ;-)

At this point, I fell I should ask what are the relative
advantages/disadvantages of using intuition versus firstorder in a
real development ? The manual is not very clear about this.

Best regards,
Thomas Braibant

[Coq-Club] Proof Help, emily_p
- Re: [Coq-Club] Proof Help, Luke Palmer
- Re: [Coq-Club] Proof Help, muad
- <Possible follow-ups>
- Re: [Coq-Club] Proof Help, fdabrows
  - Re: [Coq-Club] Proof Help, Adam Chlipala
    - Re: [Coq-Club] Proof Help, fdabrows
    - Re: [Coq-Club] Proof Help, Roman Beslik
      - Re: [Coq-Club] Proof Help, Thomas Braibant
        
        Re: [Coq-Club] Proof Help, Adam Chlipala
        
        Re: [Coq-Club] Proof Help, Roman Beslik
      - Re: [Coq-Club] Proof Help, Adam Chlipala