Learning how to Prove: From the Coq Proof Assistant to Textbook Style

Sebastian Böhne
(Universität Potsdam)
Christoph Kreitz
(Universität Potsdam)

We have developed an alternative approach to teaching computer science students how to prove. First, students are taught how to prove theorems with the Coq proof assistant. In a second, more difficult, step students will transfer their acquired skills to the area of textbook proofs. In this article we present a realisation of the second step.

Proofs in Coq have a high degree of formality while textbook proofs have only a medium one. Therefore our key idea is to reduce the degree of formality from the level of Coq to textbook proofs in several small steps. For that purpose we introduce three proof styles between Coq and textbook proofs, called line by line comments, weakened line by line comments, and structure faithful proofs.

While this article is mostly conceptional we also report on experiences with putting our approach into practise.

In Pedro Quaresma and Walther Neuper: Proceedings 6th International Workshop on Theorem proving components for Educational software (ThEdu'17), Gothenburg, Sweden, 6 Aug 2017, Electronic Proceedings in Theoretical Computer Science 267, pp. 1–18.
Published: 2nd March 2018.

ArXived at: http://dx.doi.org/10.4204/EPTCS.267.1 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org