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

TL;DR

This paper presents a multi-step approach to help students transfer proof skills from formal Coq proofs to more informal textbook proofs, introducing intermediate proof styles to ease the transition.

Contribution

It introduces three intermediate proof styles to bridge the gap between formal Coq proofs and textbook proofs, facilitating student learning.

Findings

Successful implementation of intermediate proof styles

Positive student feedback on the transfer process

Practical experience with the approach reported

Abstract

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.