This commit adds a suite of 'mystery function' specifications—ranging from standard mathematical functions like factorial and Fibonacci to more abstract tree transformations—to the week-05 course exercises. These definitions serve as formal specification exercises for students in the Functional Programming in Proof (FPP) curriculum.

This commit introduces a substantial Coq worksheet centered on “mystery functions,” with formal specifications over naturals, booleans, tuples, and trees, plus example implementations and partial proof scripts. It looks like teaching or lab material: students are guided to identify functions from algebraic properties, write unit tests, and prove soundness or uniqueness where possible. The file adds real instructional content rather than boilerplate, and it expands the project with a reusable set of proof exercises and examples. Practically, it gives contributors a new verified-programming exercise set to work through.

This commit rewrites the Coq solutions for ladidah and toodeloo so they now use the opposite proof styles: ladidah is proved by destructing the disjunction early and replaying the implication chain in each branch, while toodeloo is proved by splitting early and rebuilding the same derivation for each conjunct. The surrounding commentary and shown proof terms were updated to match, with the notes now emphasizing how early destruct/split affects duplication and proof size. Practically, this makes exercise 13 a clearer comparison of forward vs. backward proof structure and their linear proof-term complexity.

This change finishes the pending 12c section in the Coq exercise file by replacing the TODO with an explicit comparison between the two existing proof styles. The added note highlights that one proof repeatedly reconstructs the same implication chain while the other avoids that redundancy, which clarifies the tradeoff the exercise is meant to illustrate. Practically, the file is now more complete as study material and makes the proof-structure lesson easier to understand.

This change reorganizes week-04_backward-and-forward-proofs.v for readers rather than altering the underlying proofs or definitions. It wraps auxiliary sections in hide markers and adds explicit exercise labels for the multiplication tasks, which should make the rendered material cleaner and easier for students to follow. The practical effect is better structure and readability in the teaching content, with no semantic change to the Coq development.

This commit extends the week-04 proofs file with a substantial new Coq development covering recursive and tail-recursive definitions of addition and multiplication over naturals. It adds unit tests, fold/unfold lemmas, and machine-checked proofs that two addition implementations are equivalent, that addition is neutral/associative/commutative, and that four multiplication variants agree via accumulator-distribution lemmas. The multiplication-properties section is only partially completed, with several later theorems still marked Abort, but the file already establishes the main proof structure and reusable lemmas for future exercises. Practical effect: the repository now has a much richer formalization of arithmetic reasoning to build on.

This change adds embedded formatting metadata to week-04_backward-and-forward-proofs.v, including title, authorship, date, and table-of-contents directives for PDF generation. It doesn’t alter any proof logic, but it improves how the exercise material is exported and presented outside the Coq editor. The practical effect is a more polished PDF output for sharing or submission.