From 56386768def6db7d139e0876a1d41c84c0fdd200 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Fri, 30 Oct 2026 20:48:43 +0000 Subject: [PATCH] docs(CONTRIBUTING): named components instead of positional projection chains (#1764) Public statements and definition bodies avoid projection chains like c.1.2; prefer named binders, uncurry/Prod.map, small structures or named accessors, keeping forms definitionally equal for automation. Co-Authored-By: Claude Opus 5.5 --- CONTRIBUTING.md | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 400207a8b..039e08594 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -64,6 +64,23 @@ Mathlib's standard linter set already enforces the mechanical part; reviews enfo Preserve existing guarantees when rewriting tests: exact bounds or probabilities must not become weaker inequalities, and regression cases must not become tautologies. +**Named components instead of positional projections** +([#1764](https://github.com/cslib-community/complexitylib/issues/1764)). Public statements and +the bodies of public definitions do not reach into nested tuples with projection chains such as +`c.1.2` or `s.1.1.2`. A reader should not have to reconstruct the tuple layout. In order of +preference: + +1. Bind the components by name: `fun ((d, x), c) => step d x c`, not + `fun c => step c.1.1 c.1.2 c.2`. +2. Use `Function.uncurry`, `Prod.map` or composed projections, as the plain calculus rules + already do. +3. Turn a recurring tuple context into a small `structure` with named fields. +4. If restructuring is too invasive, add named `abbrev` accessors such as `Ctx.desc`. + +The rewritten form should stay definitionally equal to the old one, so that clients and automation +(`fun_prop`, `@[program_certificate]`) keep working. Single projections (`p.1`) and +destructuring inside proofs (`obtain ⟨⟨d, x⟩, c⟩ := s`) are fine. + Improving an interface never weakens the mathematics: keep the models, encodings, independent resource bounds and nonvacuity of the results it touches.