So far, we have defined addition and multiplication for MyNat and proved their algebraic laws. Starting with this article, we will move on to the “order” of natural numbers. As a preliminary step before defining order, we will first prove the cancellation laws for addition. The statement that b = c follows from a + b = a + c may seem intuitively obvious, but proving it formally requires us to go all the way back to the Peano axioms, making it a good exercise. I will continue using “Introduction to the Lean Language from Scratch: Learning Formal Mathematics Library Development Through Hands-On Practice” as the textbook.
The injection Tactic and the Peano Axioms
The proof uses the following properties of the Peano axioms:
- The results of applying
succto different natural numbers are different - 0 is always different from the result of applying
succ
These properties are automatically satisfied when a type is defined using the inductive keyword, and in Lean 4 they can be used through the injection tactic. This time, I used it to extract l + m = n + m from the equation (l + m) + 1 = (n + m) + 1. It is convenient that the injectivity of succ can be applied with a single tactic.
variable {l m n : MyNat}
theorem MyNat.add_right_cancel (h : l + m = n + m) : l = n := by
induction m with
| zero =>
simp_all
| succ m ih =>
-- ih : l + m = n + m → l = n
-- h : l + (m + 1) = n + (m + 1)
-- ⊢ l = n
have lem : (l + m) + 1 = (n + m) + 1 := calc
_ = l + (m + 1) := by ac_rfl
_ = n + (m + 1) := by rw [h]
_ = (n + m) + 1 := by ac_rfl
have : l + m = n + m := by
injection lem
exact ih this
theorem MyNat.add_left_cancel (h : l + m = l + n) : m = n := by
rw [MyNat.add_comm l m, MyNat.add_comm l n] at h
-- h : m + l = n + l
apply MyNat.add_right_cancel h
In the succ case, the induction hypothesis ih is not initially in a form that can be applied directly. Therefore, I first use calc to transform h into the form (l + m) + 1 = (n + m) + 1, and then use injection to extract the inner equality. As for add_left_cancel, it can be reduced to add_right_cancel simply by swapping the operands using add_comm, so the proof becomes considerably shorter.
Rewriting the Theorems into a Form Usable by simp
To make the proved theorems available to the simp tactic, we rewrite them as equivalences. This is where the @[simp ↓] attribute appears. The usual @[simp] attribute performs simplification in a bottom-up direction, from the inside of an expression toward the outside. Adding ↓ changes the direction to top-down, simplifying from the outside toward the inside. In this case, we want to simplify an entire expression such as l + m = n + m into l = n before simplifying its subexpressions, so the top-down setting is appropriate.
@[simp ↓] theorem MyNat.add_right_cancel_iff : l + m = n + m ↔ l = n := by
constructor
· apply MyNat.add_right_cancel
· intro h -- h : l = n ⊢ l + m = n + m
rw [h]
@[simp ↓] theorem MyNat.add_left_cancel_iff : l + m = l + n ↔ m = n := by
constructor
· apply MyNat.add_left_cancel
· intro h -- h : l = n ⊢ l + m = n + m
rw [h]
example : l + m = l + n → m = n := by
simp
Using constructor, the equivalence is split into its two directions. One direction can be proved by directly applying the existing theorem, while the other requires only rewriting with the assumption using rw. As shown in the final example, the cancellation law can now be applied with a single use of simp.
The cancellation laws can also be used to prove the following theorems.
@[simp] theorem MyNat.add_right_eq_self : m + n = m ↔ n = 0 := by
constructor <;> intro h
case mpr => simp_all
case mp =>
have : m + n = m + 0 := by
rw [h]
simp
simp_all
@[simp] theorem MyNat.add_left_eq_self : n + m = m ↔ n = 0 := by
rw [
MyNat.add_comm n m,
MyNat.add_right_eq_self,
]
@[simp] theorem MyNat.self_eq_add_right : m = m + n ↔ n = 0 := by
rw [show (m = m + n) ↔ (m + n = m) from by exact eq_comm]
exact add_right_eq_self
@[simp] theorem MyNat.self_eq_add_left : m = n + m ↔ n = 0 := by
rw [
MyNat.add_comm n m,
MyNat.self_eq_add_right,
] The code is maintained in the following repository. Please note that it contains many items that are still works in progress.
