Interactive Theorem Provers (ITPs) have recently gained attention as tools to support students in proof-based computer science (CS) courses. These tools facilitate human-machine collaboration in proof development, providing structured guidance, immediate feedback, and an interactive interface that displays remaining subgoals and potential errors. Historically used in industry for verification and in academia for research, ITPs are now being explored in educational contexts to address common challenges students face with mathematical proofs.
To introduce interested proof-based course instructors to these tools, we present a case study that applies two widely used ITPs, Coq and Lean, to five proof exercises spanning several proof techniques. The selected exerises are as follows:
-
Direct Proof - Propostional Logic: Prove that
$$(P \rightarrow (Q \land R)) \iff ((P \rightarrow Q) \land (P \rightarrow R))$$ -
Direct Proof - First-Order Logic: Prove that for every
$a \in \mathbb{Z}$ , if$5a+11$ is odd then$9a+3$ is odd. -
Proof by Contradiction: Prove that it is never the case for
$n \in \mathbb{N}$ to be odd and its square$n^2$ to be even. -
Proof by Cases: Prove that
$$\forall x \in \mathbb{R}, \forall y \in \mathbb{R}, \exists z \in \mathbb{R}, \lnot(x = y) \rightarrow ((x < z < y) \lor (y < z < x))$$ -
Proof by Induction: Prove that for every non-negatve
$n \in \mathbb{Z} 0$ , the sum$n^3 + (n+1)^3 + (n+2)^3$ is divisible by 9.
The Coq proofs are provided under coq_case_study/Exercises.v, and the Lean proofs are provided in lean_case_study/LeanCaseStudy/Exercises.lean. The Coq proofs were constructed using Coq's official IDE, CoqIDE, and the Lean proofs were constructed using Lean's official Visual Studio Code extension.
To run these proofs locally on your device, follow Coq's installation steps as well as Lean's installation steps.