Learning Rocq

I'm working through Software Foundations Volume 1: Logical Foundations to learn Rocq and get more practice with formal proofs.

This is where I keep the code I write while following along, my attempts at the exercises, and notes on what I'm learning.

Learning materials

• Logical Foundations, part of Software Foundations
• Rocq tutorial video playlist

Chapters

I've organized the work by chapter under src. Each chapter source file contains the examples and exercises in book order, with tests and notes alongside it when they exist.

Chapter	Code and exercises	Notes
Basics	Basics.v	BasicsNotes.md
Induction	Induction.v	N/A

Compiling

From the repository root:

make

The Makefile maps src to the LF namespace and discovers the Rocq source files in that directory. To compile one file directly, use:

rocq compile -Q src LF src/Basics.v

To remove compiled Rocq artifacts and generated Makefile metadata:

make clean