This repository contains my own Coq/Rocq proof scripts and notes while working through exercises from Software Foundations, Volume 1: Logical Foundations.
These are not official solutions, not endorsed by the authors, and may be incomplete, inelegant, or simply wrong in places.
- A scratchpad / archive of my attempts at the exercises
- Extra lemmas, alternative proofs, and small experiments I found helpful
- Not an “answer key”
- Not guaranteed-correct solutions
- Not something to use for coursework / graded assignments
-
Software Foundations (Logical Foundations):
https://softwarefoundations.cis.upenn.edu/lf-current/ -
Example chapter link (Basics):
https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html
Note: the text sometimes says Coq and sometimes Rocq (the project is in a transition period).
Basics.v,Lists.v,Poly.v, ...: my working files for each chapterMakefile,_CoqProject: build configuration (if present)
If you have a Makefile already:
makeClean build artifacts:
make cleanIf your repo uses _CoqProject, you can typically regenerate a makefile like this:
coq_makefile -f _CoqProject -o Makefile
make- I try to keep proofs readable over clever.
- When something gets messy, I add helper lemmas rather than piling on tactics.
These are exercise solutions. If you’re using Software Foundations for a class or self-study, consider keeping solutions private to avoid spoiling the learning process for others.
My contributions in this repo are mine.
The upstream Software Foundations materials (text and accompanying files) have their own licensing terms—please refer to the official site for details.