The Coq mailing list

[harke AT cs.pdx.edu]

I suspect you can do it without having to resort to OCaml.

If you want to see a concrete instance of what double induction does,
take a proof and instead of invoking 'double induction m n' invoke
'info double induction m n'.  When I do that on an example with nats
I see that double induction expands to 3 uses of nat_ind and some
administrative stuff.

Sorry I can't be more concrete.  The phrases double and triple induction
are ambiguous.  What particular scheme did you have in mind?  Perhaps,
if you need to do more than one triple induction you can prove that
scheme as a lemma.  Perhaps functional induction is appropriate.

On Mon, Apr 26, 2010 at 03:53:07PM -0400, M. Scott Doerrie wrote:
> I need to perform triple induction in a similar way as double induction.  
> Is there a straightforward way to get this up and running in 8.2pl1, or 
> do I need to learn to write tactics in OCaml?  I'm looking at functional 
> induction and dependent induction, but can't seem to invoke them even 
> after importing the required libraries.
>
> Scott Doerrie

-- 
Tom Harke