Guided Labs
Download the offline proof and discrete structures kit
and extract it. It contains a starter, reference implementation, independent
checker, demonstration and evidence template. Python 3.10+ and its standard
library are sufficient. In the extracted proofs-discrete directory run:
python check.py starter
python run_labs.py starter
The unfinished starter fails intentionally. Implement one lab at a time; the
README defines all arguments, outputs, ordering and invalid-input behavior.
After your attempt, use python check.py reference to calibrate your setup.
The reference is teaching material, not a submission to copy.
| Lab | Implement | Written evidence | Planning time |
|---|---|---|---|
| 1 | Boolean evaluator and complete truth tables | Four-row contrapositive proof; converse counter-row; finite coverage argument | 3–4 h |
| 2 | Total-function report and relation-property witnesses | Negate each definition; explain empty carriers and a collision | 4–6 h |
| 3 | Typed composition, equivalence classes, partial-order report | Partition proof; minimal versus least; cover reconstruction | 4–6 h |
| 4 | Full binary tree counts with an explicit stack | Structural proof; shared-subtree fixture; unary-constructor variation | 3–4 h |
For each lab: derive a fixture by hand, implement it, run checks, explain one failure, then change one assumption. Save output and reasoning in the supplied evidence template. If your first implementation is correct, critique a deliberate fault rather than inventing a personal mistake.
The checker uses all relations on carriers of sizes zero through three, all small total functions through three inputs/outputs, all pairs of two-element relations for composition, tree shapes through five internal nodes, and invalid inputs. Passing these finite checks supports the implementation; the written proofs still establish the general mathematical claims.
The full API deliberately validates branches that Boolean short-circuit execution could skip. These are pure finite mathematical expressions. Software expressions with side effects, exceptions or divergence require a richer model.
Before the capstone, read Proof and Model Contracts. The demonstration prints a worked workflow fixture; attempt the project independently before consulting that implementation.