81 lines
2.7 KiB
Plaintext
81 lines
2.7 KiB
Plaintext
|
[Problem Restatement]
|
|||
|
|
|
|||
|
|
For every natural number \(n\), adding zero to \(n\) leaves \(n\) unchanged. In symbols, the claim is
|
|||
|
|
|
|||
|
|
\[
|
|||
|
|
n + 0 = n.
|
|||
|
|
\]
|
|||
|
|
|
|||
|
|
This is one of the basic properties of addition on the natural numbers.
|
|||
|
|
|
|||
|
|
[Useful Observations]
|
|||
|
|
|
|||
|
|
1. **Zero is the additive identity.** In any algebraic structure with addition, the element \(0\) is defined by the property that adding it to any element does not change that element. For natural numbers, this is exactly the statement \(n + 0 = n\).
|
|||
|
|
|
|||
|
|
2. **Natural numbers are built recursively.** The natural numbers are generated from \(0\) by repeatedly applying the successor operation. This means any proof about all natural numbers can be reduced to checking the base case \(n = 0\) and then verifying that the property is preserved when moving from \(n\) to \(n+1\).
|
|||
|
|
|
|||
|
|
3. **The successor case is immediate.** If we already know \(n + 0 = n\), then adding one more zero gives \((n+1) + 0 = n+1\). This is just the same identity applied to the successor of \(n\).
|
|||
|
|
|
|||
|
|
[Reasoning Path]
|
|||
|
|
|
|||
|
|
To prove \(n + 0 = n\) for all natural numbers, we use the recursive definition of the natural numbers.
|
|||
|
|
|
|||
|
|
- **Base case:** When \(n = 0\), the statement becomes \(0 + 0 = 0\), which is true by the definition of addition.
|
|||
|
|
|
|||
|
|
- **Inductive step:** Assume the statement holds for some natural number \(n\), i.e., \(n + 0 = n\). We must show it holds for \(n+1\), i.e., \((n+1) + 0 = n+1\). But \((n+1) + 0\) is just \(n+1\) by the definition of addition, so the statement is true for \(n+1\) as well.
|
|||
|
|
|
|||
|
|
Since both the base case and the inductive step are immediate, the identity holds for every natural number \(n\).
|
|||
|
|
|
|||
|
|
[Key Derivation]
|
|||
|
|
|
|||
|
|
The entire derivation is captured by the two equations:
|
|||
|
|
|
|||
|
|
\[
|
|||
|
|
0 + 0 = 0,
|
|||
|
|
\]
|
|||
|
|
|
|||
|
|
and
|
|||
|
|
|
|||
|
|
\[
|
|||
|
|
(n+1) + 0 = n+1.
|
|||
|
|
\]
|
|||
|
|
|
|||
|
|
These are exactly the base and successor cases of the recursive definition of addition on natural numbers.
|
|||
|
|
|
|||
|
|
[Proof Type]
|
|||
|
|
|
|||
|
|
This is a direct proof by induction on the natural number \(n\).
|
|||
|
|
|
|||
|
|
[Formal Anchors]
|
|||
|
|
|
|||
|
|
The Lean proof uses induction on \(n\):
|
|||
|
|
|
|||
|
|
```lean4
|
|||
|
|
induction n with
|
|||
|
|
| zero => rfl
|
|||
|
|
| succ n ih => ...
|
|||
|
|
```
|
|||
|
|
|
|||
|
|
The base case is closed by reflexivity (`rfl`), and the successor case follows from the induction hypothesis (`ih`) together with the simplifier (`simp`), which uses the recursive definition of addition.
|
|||
|
|
|
|||
|
|
[Final Solution]
|
|||
|
|
|
|||
|
|
We prove that \(n + 0 = n\) for every natural number \(n\) by induction.
|
|||
|
|
|
|||
|
|
- For \(n = 0\), we have \(0 + 0 = 0\), which is true.
|
|||
|
|
- Assume \(n + 0 = n\). Then \((n+1) + 0 = n+1\), which is also true.
|
|||
|
|
|
|||
|
|
By induction, \(n + 0 = n\) for all natural numbers \(n\).
|
|||
|
|
|
|||
|
|
The complete typechecked Lean 4 proof is:
|
|||
|
|
|
|||
|
|
```lean4
|
|||
|
|
import Mathlib
|
|||
|
|
|
|||
|
|
|
|||
|
|
theorem demo (n : ℕ) : n + 0 = n := by
|
|||
|
|
induction n with
|
|||
|
|
| zero => rfl
|
|||
|
|
| succ n ih => simp_all
|
|||
|
|
```
|