lean-best-practices

# Lean 4 best practices Conventions for writing Lean 4 libraries in the Mathlib4 style. Distilled from the official Mathlib contributor docs plus painful lessons learned bootstrapping the [Solanalib](https://github.com/solana-foundation/leanprover-solanalib) library — examples below use Solanalib's code, but the rules are general. ## When this skill applies - Adding or modifying any `.lean` file in a library that aims to follow Mathlib conventions. - Editing `lakefile.lean`, `lean-toolchain`, `lake-manifest.json`, or `.github/workflows/` for a Lean project. - Reviewing a Lean PR for style or structure. - Bootstrapping a new Lean 4 library that should match the Mathlib ecosystem's conventions. ## Default decisions Make these without asking: - **Verify locally before pushing.** `elan` installs the right toolchain from the `lean-toolchain` file; `lake build` (and `lake test`) before any push. CI cycles cost minutes; local builds cost seconds. Never push a Lean change without a local build pass. - **Track Mathlib's `lean-toolchain` pin.** When bumping Lean, fetch `https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain`, set `lean-toolchain` to match, and update the Mathlib `require` rev in `lakefile.lean` to the same tag. `doc-gen4`'s `main` branch tracks this — drift breaks docs. - **Copyright authorship line is `<Project> Contributors`.** Never personal names, never the parent org. The `Copyright (c) YEAR <Owner>` line is the legal-owner statement and is separate. - **No AI-attribution trailers** (`Co-Authored-By: Claude …`) in commits. - **Commit `lake-manifest.json`** but not `.lake/`. Reproducible builds depend on the manifest; `.lake/` is per-machine cache. ## Operating procedure ### Adding a new module 1. Decide the file path. Organise by **domain concept**, not by **consumer or framework** (Mathlib organises by mathematical concept, not by who uses it; sibling libraries should organise the same way within their domain). 2. Write the file using the template in `## File template` below. 3. Add `import <Library>.<Concept>.<Aspect>` to the library root file (alphabetical within its block). 4. Run `lake build` locally. Fix any errors. Run `lake test`. 5. If the module introduces a load-bearing API surface, add a regression test under the test library mirror (`<Library>Test/<Concept>/<Aspect>Test.lean`) and import it from the test root. ### Adding a new theorem 1. Place it in the file whose subject it concerns, not in a global `Theorems.lean`. 2. Name it `<conclusion>_of_<hypothesis>` (Mathlib pattern: `add_pos_of_pos_of_nonneg`) or `<descriptive_name>` if self-explanatory (`Nat.sub_add_cancel`). 3. Write the statement with all binders explicit (`autoImplicit := false` is on globally in the lakefile — keep it that way). 4. Prefer term-mode proofs (`:= rfl`, `:= by simp`) over multi-line `by` blocks when feasible. Otherwise use the tactic style in `## Proof style` below. 5. Tag with `@[simp]` only if the lemma rewrites *toward* a normal form. Don't tag the headline result. ### Adding a new type **Default to `notation` over `abbrev` when the type is a synonym for `Nat`/`Int`.** See `## Type aliases: notation, not abbrev` below — this is the most-likely-to-bite gotcha. For real structures, use `structure`/`inductive` with `@[ext]`: ```lean @[ext] structure Slot where /-- The slot number on the cluster. -/ value : Nat deriving Repr, DecidableEq ``` ## File template Every `.lean` file starts with this exact shape: ```lean /- Copyright (c) <YEAR> <Legal Owner>. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: <Project> Contributors -/ import <Library>.<dep1> import <Library>.<dep2> -- alphabetical within their block /-! # <Module title — short, capitalised> <One-paragraph summary explaining what this module is for and why it exists. End at the level of "what does this file give to the rest of the library".> ## Main definitions * `<Library>.Foo` — <one-line gloss> * `<Library>.Foo.bar` — <one-line gloss> ## Main statements * `foo_property_baz` — <what it proves and why it matters> -/ namespace <Library> -- declarations end <Library> ``` **Critical ordering:** copyright `/- ... -/` comment first, then imports, then `/-! ... -/` module docstring. The module docstring is a *declaration*, not a comment, so it cannot precede `import`. Mistaking this produces `invalid 'import' command, it must be used in the beginning of the file`. **Subsection headers** (`## Main definitions`, `## Main statements`, `## Implementation notes`, `## References`) follow Mathlib's convention and are rendered as anchored sections in the doc-gen4 output. ## Naming conventions Inherited from Mathlib: | Kind | Convention | Example | |---|---|---| | Types, structures, classes, inductives | `UpperCamelCase` | `Account`, `TransferResult` | | Defs, functions, fields | `lowerCamelCase` | `credit`, `lamportsPerSol`, `source` | | Theorems, lemmas, propositions | `snake_case` | `transfer_preserves_total`, `credit_lamports` | | Files | `UpperCamelCase.lean` | `Transfer.lean` | | Folders | `UpperCamelCase` | `Account/`, `Primitives/` | Theorem-name pattern: `<conclusion>_of_<hypothesis>`. For projection-shape `@[simp]` lemmas, the form `<def>_<field>` is conventional (`credit_lamports`, `Account.mk_lamports`). ## Bounded types: bridging UInt64 to Nat for omega **`omega` in Lean 4.31.0-rc1 has very limited `UInt64` support.** Tests like `(a b : UInt64) (h : a ≤ b) : b - a + a = b := by omega` fail with `No usable constraints found`. The fix is to keep two parallel type-aliases and bridge between them with `.toNat`: ```lean notation "Lamports" => UInt64 -- strict on-chain shape notation "LamportsUnchecked" => Nat -- for omega-style reasoning ``` The pattern in practice: ```lean -- Define operations on UInt64 with explicit bounds proofs in the signature: def credit (a : Account) (amount : Lamports) (h : a.lamports.toNat + amount.toNat < UInt64.size) : Account := { a with lamports := a.lamports + amount } -- Provide a `_toNat` bridge lemma that drops the result into Nat: theorem credit_lamports_toNat (a : Account) (n : Lamports) (h : a.lamports.toNat + n.toNat < UInt64.size) : (credit a n h).lamports.toNat = a.lamports.toNat + n.toNat := by rw [credit_lamports, UInt64.toNat_add, Nat.mod_eq_of_lt h] ``` Then conservation-style proofs become: ```lean theorem transfer_preserves_total ... : (transfer ...).source.lamports.toNat + (transfer ...).destination.lamports.toNat = src.lamports.toNat + dst.lamports.toNat := by have h_under_nat := UInt64.le_iff_toNat_le.mp h_under -- bridge UInt64 ≤ → Nat ≤ simp only [transfer] rw [debit_lamports_toNat, credit_lamports_toNat] omega -- now in Nat-land ``` Key core lemmas to know (all in `Init.Data.UInt.Lemmas`): | Lemma | What it gives | |---|---| | `UInt64.le_iff_toNat_le` | `a ≤ b ↔ a.toNat ≤ b.toNat` (proved by `rfl`) | | `UInt64.toNat_add` (`@[simp]`) | `(a + b).toNat = (a.toNat + b.toNat) % UInt64.size` | | `UInt64.toNat_sub_of_le` (`@[simp]`) | `b ≤ a → (a - b).toNat = a.toNat - b.toNat` | | `UInt64.toNat_lt` (`@[simp]`) | `n.toNat < 2 ^ 64` | | `Nat.mod_eq_of_lt` | `n < m → n % m = n` (used with `toNat_add` to drop the `%`) | ### `.toNat` vs `.toBitVec` — which bridge? There are *two* possible bridges out of `UInt64`. Use the one that matches what you're proving: | Use | Bridge | Closer | |---|---|---| | Conservation / accounting / counting (Solanalib's core case) | `.toNat` | `omega` | | Wrap-aware arithmetic, ring algebra, explicit-overflow exploit proofs | `.toBitVec` | `bv_omega` | Mathlib's `Mathlib/Data/UInt` builds its `UInt64` algebra on `.toBitVec`, not `.toNat` — but it's scoped (`open scoped UInt64.CommRing`) precisely because the Mathlib authors flag that algebraic instances on `UInt64` *"interfere more with software-verification use-cases."* For Solanalib, `.toNat` is the default because **a conservation theorem stated at `.toNat` level needs fewer preconditions** than the equivalent UInt64-level statement: the natural sum doesn't need a "RHS-doesn't-overflow" side condition, since `Nat` is unbounded. Same trade as every comparable software-verification project (seL4, CompCert, Cardano Plutus). Don't pre-emptively `import Mathlib.Data.UInt` — it brings ~700 extra build jobs for the algebraic-instances chain we don't currently use. Import surgically when a specific theorem genuinely needs `bv_omega` or scoped ring tactics. ## Why not `abbrev`? The historical reason for using `notation` (over `abbrev`) was that **`omega` does not unfold `abbrev T : Type := Nat`.** Its preprocessor classifies hypotheses by their surface type and silently drops constraints over the alias, producing `omega could not prove the goal: No usable constraints found.` Wrong: ```lean abbrev Lamports : Type := Nat -- omega will refuse to see (a : Lamports) ≤ b ``` Right: ```lean namespace Solanalib.Lamports -- declarations using Nat directly (the namespace header is parsed BEFORE the -- notation is declared, so `Lamports` here is still an identifier). end Solanalib.Lamports /-- A lamport count: the smallest unit of native Solana value. -/ notation "Lamports" => Nat ``` `notation` is a parse-time substitution, so `(amount : Lamports)` is elaborated as `(amount : Nat)` from the start. omega and `simp`-set lemmas about `Nat` work without ceremony. The notation must be declared *after* any `namespace <SameName>` blocks in the same file, because the parser substitutes the token everywhere once the notation is in scope. **Escape hatch:** if/when strict typing is needed (e.g. to enforce `≤ 2^64 - 1` on a `u64`-like quantity), promote to a single-field `structure` with explicit conversion. Plan to migrate the call sites mechanically; the migration is breaking but tractable. ## Bundled structures vs typeclasses When a domain concept has *several mathematical properties* that must hold together (e.g. "this is a function that decays from peak to zero in a window"), prefer a **bundled structure** with the function and proofs embedded, not a `class`-based typeclass. ```lean -- ✓ Mathlib-aligned bundled-structure pattern (used by OrderHom, MulHom, -- LinearMap, RingHom, ...): structure WindowedDecay where tBegin : Nat tEnd : Nat peak : Nat apply : Nat → Nat bounded : ∀ t, apply t ≤ peak -- ... three more properties ... -- Concrete-shape providers expose a constructor: def LinearDecay.toWindowedDecay (tBegin tEnd peak : Nat) : WindowedDecay := { … } ``` Why bundled over typeclass: - **No instance-resolution surprises.** A `WindowedDecay` value is just a value; you pass it explicitly. No implicit-argument elaboration footguns (like the `fun p {_ _} h_begin …` workaround that `class Decay` needed). - **Mathlib does it this way.** Their `OrderHom`, `MulHom`, `RingHom`, `LinearMap`, etc. are all bundled structures, not classes. - **Composition is plain function-call syntax.** `d.complementary t`, `d.apply t` — no typeclass magic. - **Generic theorems live as methods on the structure**, not as separate generic functions over `[Decay T]`. When *to* reach for a `class`: when you have a true type-level interface (e.g. `Monoid α`, `AddCommGroup α`) where the typeclass system's instance resolution is doing useful work — finding the appropriate algebraic structure for `Nat`, `Int`, `Rat`, etc. For domain-specific finance shapes with concrete parameter values, bundled structures are usually the better tool. ## Numeric layer: `Solanalib.Numeric` A dedicated folder for numeric infrastructure that domain modules build on. Currently houses `Fraction` (Q68.60 fixed-point, common in Solana DeFi). Future additions: `Fraction128` (the bounded `u128`-backed refinement of `Fraction`), `Q.96`, etc. The convention for spec-layer numeric types is: 1. **`Nat` underneath, exposed through a `structure`** so domain code can talk about "a Fraction" without exposing the encoding. `omega` works directly on the underlying `Nat`. 2. **Operations carry their preconditions in the type** (`Fraction.sub (h : b.bits ≤ a.bits)`, like `Account.debit`). 3. **`@[ext]` plus `@[simp]` projection lemmas for every field / operation** so `ext; simp` proofs compose cleanly downstream. 4. **`LE`/`LT` instances delegate to the underlying `Nat` order**; provide `Decidable` instances explicitly — they don't come for free from the `LE` instance, and `decide` will fail mysteriously without them. ```lean instance : LE Fraction := ⟨fun a b => a.bits ≤ b.bits⟩ instance (a b : Fraction) : Decidable (a ≤ b) := Nat.decLe a.bits b.bits ``` Bounded `UIntN`-backed refinements live as separate types (e.g. `Fraction128`) with `.toNat`-style bridges to the unbounded spec version, mirroring the `Lamports` / `LamportsUnchecked` pattern. ## Attribute usage - **`@[ext]`** on every `structure`. Generates the extensionality lemma `Foo.ext : a.f₁ = b.f₁ → … → a = b`. Costs nothing now, saves writing it later. - **`@[simp]`** on lemmas that rewrite *toward* a normal form. The classic case: projection lemmas that expose a field after a constructor or update. ```lean @[simp] theorem credit_lamports (a : Account) (n : Lamports) : (credit a n).lamports = a.lamports + n := rfl ``` Don't tag the headline theorem (`transfer_preserves_total`) with `@[simp]` — it's not a rewrite rule, it's a result. - **`@[reducible]`** — almost never needed at small library scale. `notation` is the right answer for type synonyms. ## Proof style - `by` at the end of the preceding line, never alone on its own line. - Tactic block indented 2 spaces. - Subgoals marked with `·` (centered dot), not `case`. - `omega` for `Nat`/`Int` linear arithmetic. `linarith` for ordered field arithmetic. `decide` for closed decidable goals.