# Inductive proof automation

**URL:** <https://discourse.rocq-prover.org/t/inductive-proof-automation/226>\
**Category:** Using Rocq\
**Created:** [March 15, 2019, 11:28am UTC](https://discourse.rocq-prover.org/t/inductive-proof-automation/226 "2019-03-15T11:28:47Z")\
**Posts on this page:** 7\
**Page:** 1

<div class="post-metadata">

**Author:** ![spitters](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/spitters/32/125_2.png) [@spitters](https://discourse.rocq-prover.org/u/spitters)\
**Post date:** [March 15, 2019, 11:28am UTC](https://discourse.rocq-prover.org/t/inductive-proof-automation/226/1 "2019-03-15T11:28:48Z")

</div>

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](https://hal.inria.fr/inria-00489496/document)

> **[tomprince/rippling](https://github.com/tomprince/rippling)**
>
> Sean Wilson's rippling plugin. Contribute to tomprince/rippling development by creating an account on GitHub.

Has there been any follow-up on this work?  
Are there better tools?

Bas

---

<div class="post-metadata">

**Author:** ![palmskog](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/palmskog/32/38_2.png) [@palmskog](https://discourse.rocq-prover.org/u/palmskog)\
**Post date:** [March 17, 2019, 4:01pm UTC](https://discourse.rocq-prover.org/t/inductive-proof-automation/226/2 "2019-03-17T16:01:52Z")

</div>

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](http://verdi.uwplse.org/raft-proof.pdf) might be relevant.

---

<div class="post-metadata">

**Author:** ![spitters](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/spitters/32/125_2.png) [@spitters](https://discourse.rocq-prover.org/u/spitters)\
**Post date:** [March 18, 2019, 8:26pm UTC](https://discourse.rocq-prover.org/t/inductive-proof-automation/226/3 "2019-03-18T20:26:38Z")

</div>

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](https://arxiv.org/pdf/1405.3426) and [QuickSpec](http://www.cse.chalmers.se/~jomoa/papers/quickspec-JFP.pdf)

---

<div class="post-metadata">

**Author:** ![palmskog](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/palmskog/32/38_2.png) [@palmskog](https://discourse.rocq-prover.org/u/palmskog)\
**Post date:** [March 22, 2019, 12:30am UTC](https://discourse.rocq-prover.org/t/inductive-proof-automation/226/4 "2019-03-22T00:30:34Z")

</div>

Maybe the work on automation of [implicit induction proofs](https://doi.org/10.1016/j.jsc.2016.07.014) is more along the lines of what you’re looking for? There is a [tool](https://github.com/sorinica/spike-prover) that works fine with Coq 8.9.

---

<div class="post-metadata">

**Author:** ![spitters](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/spitters/32/125_2.png) [@spitters](https://discourse.rocq-prover.org/u/spitters)\
**Post date:** [March 22, 2019, 9:42am UTC](https://discourse.rocq-prover.org/t/inductive-proof-automation/226/5 "2019-03-22T09:42:38Z")

</div>

I believe [IsaHipster](https://github.com/moajohansson/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.

---

<div class="post-metadata">

**Author:** ![brando90](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/brando90/32/183_2.png) [@brando90](https://discourse.rocq-prover.org/u/brando90)\
**Post date:** [March 25, 2022, 12:23am UTC](https://discourse.rocq-prover.org/t/inductive-proof-automation/226/7 "2022-03-25T00:23:44Z")

</div>

> [@spitters](#):
>
> 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? 🙂

---

<div class="post-metadata">

**Author:** ![spitters](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/spitters/32/125_2.png) [@spitters](https://discourse.rocq-prover.org/u/spitters)\
**Post date:** [March 25, 2022, 9:13am UTC](https://discourse.rocq-prover.org/t/inductive-proof-automation/226/8 "2022-03-25T09:13:25Z")

</div>

One of my master students did some experiments along those lines:

> **[GitHub - mikkelmilo/rooster-spec: Automated Theory Exploration in Coq using...](https://github.com/mikkelmilo/rooster-spec)**
>
> Automated Theory Exploration in Coq using Haskell's QuickSpec - GitHub - mikkelmilo/rooster-spec: Automated Theory Exploration in Coq using Haskell's QuickSpec