The Coq mailing list

[Roman Beslik <beroal AT ukr.net>]

Thomas Braibant wrote:
> > > 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.
>   
I think 'firstorder' is definitely more powerful, e.g. it can do this:

Require Import Coq.Relations.Relation_Definitions.

Definition th : forall (U:Type) (r : relation U), equivalence _ r
   -> forall a b c d, r a b -> r c b -> r c d -> r d a.
Proof. firstorder. Qed.

--
Best regards,
 Roman Beslik.