Natural Number Game - Multiplication World Level 1~3, a glimpse of Lean’s naming paradigm

In the Lean naming paradigm,mul_succandsucc_mulThe naming convention reflects the following core principles:

1. Verb-first naming logic

Lean function names usually end withoperative verbBegins, followed by the operand or condition. For example:

• add (addition), mul (Multiplication) is a basic operation verb;
• succ (successor function, i.e. n + 1 ) is a core operation in natural numbers.

Therefore:

• mul_succ means "apply the subsequent operation after multiplication", that is mul a (succ b) , corresponding to in mathematics a * (b + 1) 。
• succ_mul It means "apply first and then multiply", that is, succ (mul a b) , corresponding to in mathematics (a + 1) * b 。

This naming paradigm directly reflects the operationExecution orderandLogical priority。

2. Explicitness of parameter order

Lean function names usually have the same argument order as in mathematical expressions.left associativityconsistent. For example:

• mul a b Correspond a * b ；
• succ_mul a b Correspond (a + 1) * b , that is, first a Application succ , then with b Multiply.

This is consistent with the order of operations in mathematics and is intuitive. Andmul_succ a bthen corresponds toa * (b + 1), that is, firstbApplicationsucc, then withaMultiply.

3. Distributive mapping of mathematical operations

In multiplication of natural numbers, the distributive property is a core property:

• left-hand distributive law ： succ a * b = a * b + b → Correspond succ_mul a b ；
• right distributive law ： a * succ b = a * b + a → Correspond mul_succ a b 。

This naming method directly encodes mathematical properties into the function name, making it easier for developers to quickly understand its mathematical meaning through the name.

4. Naming consistency with the standard library

Lean's standard math library (Mathlib) follows a similar naming convention. For example:

• nat.add_succ ： a + (b + 1) = (a + b) + 1 ；
• nat.mul_succ ： a * (b + 1) = a * b + a 。

This consistency reduces learning costs and allows developers to infer the behavior of new functions based on existing knowledge.

5. Currying feature of functional programming

Lean supports currying, that is, multi-parameter functions can be applied step by step. For example:

• mul_succ a is a function that accepts b return after a * (b + 1) ；
• succ_mul a In the same way, return (a + 1) * b 。

This design makes function combination and partial application more intuitive.

Summarize

In the natural number game,mul_succandsucc_mulThe naming reflects the following paradigm of Lean:

1. verb first: Operational behavior comes first;
2. The order of parameters is clear: Left associativity corresponds to mathematical expressions;
3. mathematical property encoding: Directly reflect properties such as the distributive law through the name;
4. Consistent with the standard library: Reduce cognitive load.

This naming paradigm is not only in line with the conventions of functional programming, but also highly consistent with the formal expression of mathematics. It is the embodiment of Lean's unified design philosophy as a theorem prover and programming language.

Machine-translated from the Chinese original 自然数游戏-乘法世界1~3关，一窥 Lean 的命名范式 (published 2025-06-04). WeChat original ↗