Teaching Divisibility and Binomials with Coq

TL;DR

This work targets teaching divisibility and binomial coefficients $binom n k$ to early-year students using Coq, balancing formal rigor with accessibility. It builds lightweight libraries for sums, factorials, and binomials (Nat_Compl, Nat_Sum, Nat_Factorial, Nat_Binomial) and two teaching-oriented worksheets (WS_Helper, WS_Binomial), keeping proofs explicit and avoiding heavy automation by default. It introduces pedagogical tools such as the 'study' tactic for modular case-splitting and a constructive 'findall' to enforce explicit solution sets, plus a script to generate student-friendly exercise versions. An initial small experiment with two first-year students demonstrates feasibility and informs interface decisions, and all materials are freely available for reuse and curricular customization.

Abstract

The goal of this contribution is to provide worksheets in Coq for students to learn about divisibility and binomials. These basic topics are a good case study as they are widely taught in the early academic years (or before in France). We present here our technical and pedagogical choices, the numerous exercises we developed and a small experiment we conducted on two students. As expected, it required additional Coq material such as other lemmas and dedicated tactics. The worksheets are freely available and flexible in several ways.