There has been a bit of work in the past on automating induction proofs.
In particular, the rippling plugin for Coq:
https://hal.inria.fr/inria-00489496/document
Has there been any follow-up on this work?
Are there better tools?
Bas
1 Like
Although it’s not the same kind of automation as in the rippling plugin, the patterns for “custom induction principles” in the Verdi Raft paper might be relevant.
I don’t see how these are related. Rippling is about finding the right induction hypothesis.
This line of research seems to have evolved into tools like HipSter and QuickSpec
Maybe the work on automation of implicit induction proofs is more along the lines of what you’re looking for? There is a tool that works fine with Coq 8.9.
I believe IsaHipster, which uses Isabelle, may be one of the most recent developments in this direction. It would be interesting to see whether it can be connected to CoqHammer or SMTCoq.
@splitters did you figure out if that can be done? 
One of my master students did some experiments along those lines:
1 Like