The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

Hi Razvan, this is a bit old but the functional induction command of
coq can be considered as an automated induction facility. It was
written by Julien Forest, Gilles Barthe and me some time ago. the
paper talking about it is the following:

G. Barthe and P. Courtieu. Efficient Reasoning about Executable
Specifications in Coq. In C. Muñoz V. A Carreno and S. Tahar, editors,
Proceedings of TPHOLs'02, volume 2410 of Lecture Notes in Computer
Science, springer.

You can also have a look at Konrad Slind work on reasoning on
recursive functions too:
http://www.cs.utah.edu/~slind/tfl.html

Best regards,
Pierre Courtieu

2009/4/28 Razvan Voicu 
<razvan AT comp.nus.edu.sg>:
>
> Dear Coq Users,
>
> I'm currently working on automating proofs by induction in Coq, and I would
> like to make sure I'm looking at all the relevant related work. I would
> appreciate any pointers to _recent_ work in induction automation (the
> references I get from Google are at least 5-6 years old).
>
> Thank you in advance,
>
> Razvan
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>         http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>