自然数与列表结合性证明对比：为何nat_add_assoc无需归纳？

Great question—this is a common point of confusion when first working with inductive structures in proof assistants like Coq or Lean. The short answer is: yes, built-in automation for natural numbers is a big part of it, but there are a few more nuanced reasons worth breaking down:

1. Arithmetic-focused automation strategies do the heavy lifting #

Most proof assistants come with specialized tactics tailored for integer arithmetic (like Coq's lia, Lean's ring, or Isabelle's arith). These tactics are pre-programmed to recognize and apply algebraic properties like associativity, commutativity, and distributivity for natural numbers (and other numeric types) without you having to write out induction steps manually.

For example, in Coq, proving nat_add_assoc can be as simple as:

Theorem nat_add_assoc : forall a b c : nat, a + (b + c) = (a + b) + c.
Proof. lia. Qed.

The lia tactic under the hood leverages decision procedures for linear arithmetic, which already know how to handle the inductive structure of natural numbers to verify these properties.

2. Natural numbers are a "special case" in standard libraries #

Natural numbers are one of the most fundamental inductive structures in proof assistants, so their core properties (like nat_add_assoc) are often pre-proven in the standard library and wired into automation tools. When you use tactics like auto or lia, they automatically pull in these pre-existing theorems to close goals without explicit induction.

Lists, on the other hand, are a generic recursive structure (they can hold any type of element), and their append operation's properties aren't tied to the same arithmetic automation. While list associativity (app_assoc) is also in most standard libraries, proving it from scratch requires you to explicitly guide the proof assistant through the induction step—because the tool can't guess which list variable you want to induct on, or how to unfold the recursive ++ definition for all cases.

3. Recursive structure complexity differs #

Natural numbers have a very simple inductive definition: only two constructors (O for zero, S for successor). This simplicity makes it easy for automation to encode and reason about their properties without explicit guidance.

Lists, by contrast, are a nested inductive structure (nil for empty list, cons x l for a list with head x and tail l). Proving associativity for list append requires unfolding the ++ definition across both the base case (empty list) and inductive case (cons element), which needs explicit induction to tell the proof assistant how to break down the problem.

Here's what that explicit induction looks like for list associativity in Coq:

Theorem app_assoc : forall A (l1 l2 l3 : list A), l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3.
Proof.
  intros A l1 l2 l3.
  induction l1 as [|x l1' IH].
  - reflexivity. (* Base case: empty list *)
  - simpl. rewrite IH. reflexivity. (* Inductive case: cons element *)
Qed.

Wrapping up #

So to recap: the lack of explicit induction for nat_add_assoc is due to specialized automation that handles arithmetic properties out of the box, combined with natural numbers' status as a foundational, simple inductive structure. Lists, being generic and more complex in their recursion, require you to explicitly trigger induction to guide the proof assistant through their unique recursive cases.

内容的提问来源于stack exchange，提问作者Niki