<p>I guess the resource you are looking for is Adam Chlipala's <a href="http://adam.chlipala.net/cpdt/" rel="nofollow">Certified Programming with Dependent Types</a> in which he builds up powerful tactics.</p>

CC BY-SA 3.0
2015-07-31T10:55:11.657Z
2015-07-31T10:55:11.657Z
gallais
<p>I try to imagine using Coq to implement large and complicated software with specifications and proof. However, the manual work of writing proof is daunting. As a Coq newbie,  to specify an insertion sort algorithm costs me a week and nearly one thousand lines accounting for specifications and proof.</p>

<p>Is there possibly to relieve the developer's burden and make computer prove arbitrary theorem, which is much stronger than 'auto' tactic? If not, what is the unsolved question in it?</p>

CC BY-SA 3.0
2015-07-31T06:15:20.280Z
[why3](https://github.com/jpdeplaix/why3) can be used to generate proof obligations and feed them to various automated provers like Z3 or Yices.
max taldykin
CC BY-SA 3.0
2015-07-31T08:40:55.037Z
[Entscheidungsproblem](https://en.wikipedia.org/wiki/Entscheidungsproblem)!
Martin Berger
<coq><automated-theorem-proving>
Is there an algorithm to generate proof in Coq?
xywang
# Is there an algorithm to generate proof in Coq?

(Asked by: username_0 on 2015-07-31)

I try to imagine using Coq to implement large and complicated software with specifications and proof. However, the manual work of writing proof is daunting. As a Coq newbie, to specify an insertion sort algorithm costs me a week and nearly one thousand lines accounting for specifications and proof.

Is there possibly to relieve the developer's burden and make computer prove arbitrary theorem, which is much stronger than 'auto' tactic? If not, what is the unsolved question in it?

**Tags:** coq, automated-theorem-proving

> **Comments:**
> **username_1**: [why3](https://github.com/jpdeplaix/why3) can be used to generate proof obligations and feed them to various automated provers like Z3 or Yices.  
> **username_2**: [Entscheidungsproblem](https://en.wikipedia.org/wiki/Entscheidungsproblem)!  

---

## 1 answers

### Answer by username_3 on 2015-07-31. Score: 2

I guess the resource you are looking for is Adam Chlipala's [Certified Programming with Dependent Types](http://adam.chlipala.net/cpdt/) in which he builds up powerful tactics.


---

