2024-09-13 00:43:27 +00:00
|
|
|
|
# Commutativity of addition
|
|
|
|
|
|
|
|
|
|
This document shows how to prove commutativity of addition on natural numbers.
|
|
|
|
|
|
|
|
|
|
<details>
|
|
|
|
|
<summary>Imports</summary>
|
|
|
|
|
|
2024-09-12 23:38:07 +00:00
|
|
|
|
```
|
|
|
|
|
module Simple where
|
|
|
|
|
|
|
|
|
|
open import Agda.Primitive
|
|
|
|
|
open import Relation.Binary.PropositionalEquality.Core
|
|
|
|
|
|
|
|
|
|
variable
|
2024-09-13 00:43:27 +00:00
|
|
|
|
l : Level
|
|
|
|
|
```
|
2024-09-12 23:38:07 +00:00
|
|
|
|
|
2024-09-13 00:43:27 +00:00
|
|
|
|
</details>
|
|
|
|
|
|
|
|
|
|
Declare our data structures:
|
|
|
|
|
|
|
|
|
|
```
|
2024-09-12 23:38:07 +00:00
|
|
|
|
data ℕ : Set where
|
2024-09-13 00:43:27 +00:00
|
|
|
|
zero : ℕ
|
|
|
|
|
suc : ℕ → ℕ
|
|
|
|
|
```
|
2024-09-12 23:38:07 +00:00
|
|
|
|
|
2024-09-13 00:43:27 +00:00
|
|
|
|
Define addition:
|
|
|
|
|
|
|
|
|
|
```
|
2024-09-12 23:38:07 +00:00
|
|
|
|
_+_ : ℕ → ℕ → ℕ
|
|
|
|
|
zero + b = b
|
|
|
|
|
suc a + b = suc (a + b)
|
2024-09-13 00:43:27 +00:00
|
|
|
|
```
|
|
|
|
|
|
|
|
|
|
Prove commutativity:
|
2024-09-12 23:38:07 +00:00
|
|
|
|
|
2024-09-13 00:43:27 +00:00
|
|
|
|
```
|
2024-09-12 23:38:07 +00:00
|
|
|
|
+-comm : (m n : ℕ) → m + n ≡ n + m
|
|
|
|
|
+-comm zero n = lemma n where
|
2024-09-13 00:43:27 +00:00
|
|
|
|
lemma : (n : ℕ) → n ≡ n + zero
|
|
|
|
|
lemma zero = refl
|
|
|
|
|
lemma (suc n) = cong suc (lemma n)
|
2024-09-12 23:38:07 +00:00
|
|
|
|
+-comm (suc m) n = trans (cong suc (+-comm m n)) (sym (lemma n m)) where
|
2024-09-13 00:43:27 +00:00
|
|
|
|
lemma : (m n : ℕ) → m + suc n ≡ suc (m + n)
|
|
|
|
|
lemma zero n = refl
|
|
|
|
|
lemma (suc m) n = cong suc (lemma m n)
|
|
|
|
|
```
|
|
|
|
|
|
|
|
|
|
That's it!
|