mathlib3 documentation

data.nat.psub

Partial predecessor and partial subtraction on the natural numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The usual definition of natural number subtraction (nat.sub) returns 0 as a "garbage value" for a - b when a < b. Similarly, nat.pred 0 is defined to be 0. The functions in this file wrap the result in an option type instead:

Main definitions #

source
@[simp]
def nat.ppred  :
ℕ → option ℕ

Partial predecessor operation. Returns ppred n = some m if n = m + 1, otherwise none.

Equations
source
@[simp]
def nat.psub (m : ℕ) :
ℕ → option ℕ

Partial subtraction operation. Returns psub m n = some k if m = n + k, otherwise none.

Equations
source
theorem nat.pred_eq_ppred (n : ℕ) :
n.pred = n.ppred.get_or_else 0
source
theorem nat.sub_eq_psub (m n : ℕ) :
m - n = (m.psub n).get_or_else 0
source
@[simp]
theorem nat.ppred_eq_some {m n : ℕ} :
n.ppred = option.some m ↔ m.succ = n
source
@[simp]
theorem nat.ppred_eq_none {n : ℕ} :
n.ppred = option.none ↔ n = 0
source
theorem nat.psub_eq_some {m n k : ℕ} :
m.psub n = option.some k ↔ k + n = m
source
theorem nat.psub_eq_none {m n : ℕ} :
m.psub n = option.none ↔ m < n
source
theorem nat.ppred_eq_pred {n : ℕ} (h : 0 < n) :
n.ppred = option.some n.pred
source
theorem nat.psub_eq_sub {m n : ℕ} (h : n ≤ m) :
m.psub n = option.some (m - n)
source
theorem nat.psub_add (m n k : ℕ) :
m.psub (n + k) = m.psub n >>= λ (x : ℕ), x.psub k
source
def nat.psub' (m n : ℕ) :
option ℕ

Same as psub, but with a more efficient implementation.

Equations
source
theorem nat.psub'_eq_psub (m n : ℕ) :
m.psub' n = m.psub n