The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Tom Prince wrote:
> On 2011-02-10, Adam Chlipala wrote:
>    
> > The following doesn't strike me as so bad:
> > Hint Extern 1 =>  apply (laws_true law_1) || apply (laws_true law_2).
> > Hint Constructors rec.
> >
> > Goal rec A op.
> >     auto.
> > Qed.
> >
> >      
>
> That certainly works. I was hoping to avoid having to mention the names
> of all the constructors twice. If I am going to have to mention them
> twice anyway, I might as well just apply them by hand.
>    

That depends on the details of the theorems you want to prove.  Already, 
with each law used just used, the proof script I've suggested avoids the 
need to include any kind of dependency on the order in which the 
inductive type constructors were declared (e.g., the constructor numbers 
you were trying to use in your original attempt).  Also, if you prove 
multiple theorems that depend on the same facts, the same hint suffices 
to prove all of the theorems automatically.