Improvement of proof for basic theorem on Nat?

Stream: new members

[Michael Lee]

I was writing a proof of a theorem and needed what seemed like a basic fact on the natural numbers, that c - b + a = c - (b - a) if a ≤ b and b ≤ c. Of course, I've just started learning Lean, so I'm not all that familiar with the basic toolbox yet, but I took a look at the theorems available for Nat and didn't see this precise statement. I took a crack at proving it myself and quickly found that the complexity of my proof got a bit out of hand:

theorem Nat.sub_add {a b c : ℕ} (hab : a ≤ b) (hbc : b ≤ c) : c - b + a = c - (b - a) := by
  have h1 (n : ℕ) := sub_succ c (c - (b - n))
  have h2 (n : ℕ) := Nat.sub_sub_self (le_trans (sub_le b n) hbc)
  have h3 (m n : ℕ) (h : succ m ≤ n) : (m < n) := Nat.lt_of_lt_of_le (lt_succ.mpr (le_refl m)) h
  have h4 (m n : ℕ) (hm : m > 0) (hn : n > 0) : succ (n - m) ≤ n := Nat.sub_lt_sub_left hn hm
  have h5 (m n : ℕ) (hmn : succ m ≤ n) := Nat.sub_pos_of_lt (h3 m n hmn)
  have h6 (l m n : ℕ) (hlm : succ l ≤ m) (hmn : m ≤ n) :=
    Nat.sub_sub_self (le_trans (h4 (m - l) n (h5 l m hlm)
      (Nat.lt_of_lt_of_le succ_pos' (le_trans hlm hmn))) (le_refl n))
  induction a with
  | zero => simp
  | succ a ih =>
    have h := h1 a
    rw [h2 a] at h
    rw [add_succ, sub_succ, ← h, h6 a b c hab hbc, ih (le_trans (le_succ a) hab)]

Surely there's a better way to show this?

[David Renshaw]

theorem Nat.sub_add {a b c : ℕ} (hab : a ≤ b) (hbc : b ≤ c) : c - b + a = c - (b - a) :=
  (tsub_tsub_assoc hbc hab).symm

[David Renshaw]

I found that using the exact? tactic

[Michael Lee]

Oh, that's nice. Didn't know about exact?. How does that work? Is it documented somewhere?

[David Renshaw]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/LibrarySearch.html

[David Renshaw]

Hm... I do wonder what the best way to prove your theorem would be without using mathlib

[Michael Lee]

I realize now that I could have saved about 12 hours of painstakingly looking through the library while working on the larger theorem with the help of apply? and exact?

[Mario Carneiro]

David Renshaw said:

Hm... I do wonder what the best way to prove your theorem would be without using mathlib

Most of these theorems are being migrated to std, although they need some decoding to revert them to their original Nat-based forms