Proving That Addition Preserves Order

This time, we prove that addition preserves order (monotonicity). Along the way, we build a custom tactic called compatible so that we don't have to write the same style of proof over and over.

Monotonicity of addition

First, we prove that adding the same value to the left of both sides preserves the order relation.

variable {a b m n : MyNat}

theorem MyNat.add_le_add_left (h : n ≤ m) (l : MyNat) : l + n ≤ l + m := by
  rw [MyNat.le_iff_add] at *
  obtain ⟨k, hk⟩ := h
  -- h : ∃ k, n + k = m
  -- l : MyNat
  -- ⊢ ∃ k, n + k = m
  exists k
  rw [← hk] -- hk : n + k = m ⊢ l + n + k = l + (n + k)
  ac_rfl

theorem MyNat.add_le_add_right (h : m ≤ n) (l : MyNat) : m + l ≤ n + l := calc
  _ = l + m := by ac_rfl
  _ ≤ l + n := by apply MyNat.add_le_add_left h l
  _ = n + l := by ac_rfl

In the proof of MyNat.add_le_add_left, MyNat.le_iff_add rewrites \( n \le m \) into the form \( \exists k,\ n + k = m \), and the resulting \( k \) is used directly to show \( l + n \le l + m \). The proof is finished by applying ac_rfl to rearrange the order of the sum.

For MyNat.add_le_add_right, commutativity lets us reduce the statement to the "add on the left" case, so we can reuse MyNat.add_le_add_left, which was already proven.

More generally, we can prove that the order relation is preserved for the sum of two pairs.

theorem MyNat.add_le_add (h1 : m ≤ n) (h2 : a ≤ b) : m + a ≤ n + b := calc
  _ ≤ m + b := by exact add_le_add_left h2 m
  _ ≤ n + b := by exact add_le_add_right h1 b

Making the theorems reusable

Applying these theorems naively leads to code where we pass the hypothesis to apply directly, like this.

example (h : n ≤ m) (l : MyNat) : l + n ≤ l + m := by
  apply MyNat.add_le_add_left h

Instead of passing the hypothesis by hand, we can close the goal in one go with <;> assumption.

example (h : n ≤ m) (l : MyNat) : l + n ≤ l + m := by
  apply MyNat.add_le_add_left <;> assumption

To reuse this pattern across all three theorems, we define a tactic called compatible.

syntax "compatible" : tactic

section

  local macro_rules
    | `(tactic| compatible) =>
      `(tactic| apply MyNat.add_le_add_left <;> assumption)

  local macro_rules
    | `(tactic| compatible) =>
      `(tactic| apply MyNat.add_le_add_right <;> assumption)

  local macro_rules
    | `(tactic| compatible) =>
      `(tactic| apply MyNat.add_le_add <;> assumption)

  example (h : n ≤ m) (l : MyNat) : l + n ≤ l + m := by
    compatible

  example (hle : n ≤ m) (l : MyNat) : n + l ≤ m + l := by
    compatible

  example (h1 : m ≤ n) (h2 : a ≤ b) : m + a ≤ n + b := by
    compatible

end

Making it extensible with a label attribute

With the macro_rules implementation, adding a new theorem means editing the macro itself every time. So instead, we change it so that a theorem only needs the @[compatible] attribute to be registered.

First, we declare the attribute itself in a new file. register_label_attr only takes effect across file boundaries, so it needs to live in its own file.

import Lean

register_label_attr compatible

Next, we define the actual tactic using elab. Unlike macro, elab is suited to procedural metaprogramming. It collects the theorems tagged with [compatible] one by one and keeps trying apply $declStx <;> assumption until one succeeds.

open Lean Elab Tactic in

elab "compatible" : tactic => do
  let taggedDecls ← labelled `compatible
  if taggedDecls.isEmpty then
    throwError "theorem of [compatible] has not been assigned"
  for decl in taggedDecls do
    let declStx := mkIdent decl
    try
      evalTactic <| ← `(tactic| apply $declStx <;> assumption)

      return ()
    catch _ =>
      pure ()
  throwError "Unable to close the goal."

Now, simply tagging the target theorems makes them available through the compatible tactic.

attribute [compatible] MyNat.add_le_add_left MyNat.add_le_add_right MyNat.add_le_add

example (h : n ≤ m) (l : MyNat) : l + n ≤ l + m := by
  compatible

example (hle : n ≤ m) (l : MyNat) : n + l ≤ m + l := by
  compatible

example (h1 : m ≤ n) (h2 : a ≤ b) : m + a ≤ n + b := by
  compatible

Extending to strict order

Addition also preserves the strict order \( \lt \). By tagging these theorems with @[compatible], we can keep reusing compatible in later proofs too.

@[compatible]
theorem MyNat.add_lt_add_left {m n : MyNat} (h : m < n) (k : MyNat) : k + m < k + n := by
  notation_simp at *  -- h : m + 1 ≤ n ⊢ k + m + 1 ≤ k + n
  have : k + m + 1 ≤ k + n := calc
    _ = k + (m + 1) := by ac_rfl
    _ ≤ k + n := by compatible

  assumption

@[compatible]
theorem MyNat.add_lt_add_right {m n : MyNat} (h : m < n) (k : MyNat)
  : m + k < n + k := calc
  _ = k + m := by ac_rfl
  _ < k + n := by compatible
  _ = n + k := by ac_rfl

Order is preserved when subtracting the same value from both sides

Finally, we prove the converse direction: the order relation is preserved even when the same value is removed from both sides.

section
variable (m n k : MyNat)

theorem MyNat.le_of_add_le_add_left : k + m ≤ k + n → m ≤ n := by
  intro h
  -- h : k + m ≤ k + n ⊢ m ≤ n
  rw [MyNat.le_iff_add] at *
  -- h : ∃ k_1, k + m + k_1 = k + n ⊢ ∃ k, m + k = n
  obtain ⟨d, hd⟩ := h
  exists d -- hd : k + m + d = k + n ⊢ MyNat
  have : m + d + k = n + k := calc
    _ = k + m + d := by ac_rfl
    _ = k + n := by rw [hd]
    _ = n + k := by ac_rfl
  simp_all

theorem MyNat.le_of_add_le_add_right : m + k ≤ n + k → m ≤ n := by
  rw [MyNat.add_comm m k, MyNat.add_comm n k]
  apply MyNat.le_of_add_le_add_left

@[simp] theorem MyNat.add_le_add_iff_left : k + m ≤ k + n ↔ m ≤ n := by
  constructor
  · apply MyNat.le_of_add_le_add_left
  · intro h
    compatible

@[simp] theorem MyNat.add_le_add_iff_right : m + k ≤ n + k ↔ m ≤ n := by
  constructor
  · apply MyNat.le_of_add_le_add_right
  · intro h
    compatible

end

The full code is available in the following repository.

https://github.com/ringring-creator/LearnLean