Partial predecessor and partial subtraction on the natural numbers

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

• Nat.ppred: a partial predecessor operation
• Nat.psub: a partial subtraction operation

def Nat.ppred : ℕ → Option ℕ

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

Equations

• Nat.ppred x = match x with | 0 => none | Nat.succ n => some n

@[simp]

theorem Nat.ppred_zero : Nat.ppred 0 = none

@[simp]

theorem Nat.ppred_succ {n : ℕ} : Nat.ppred (Nat.succ n) = some n

def Nat.psub (m : ℕ) : ℕ → Option ℕ

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

Equations

• Nat.psub m 0 = some m
• Nat.psub m (Nat.succ n) = Nat.psub m n >>= Nat.ppred

@[simp]

theorem Nat.psub_zero {m : ℕ} : Nat.psub m 0 = some m

@[simp]

theorem Nat.psub_succ {m : ℕ} {n : ℕ} : Nat.psub m (Nat.succ n) = Nat.psub m n >>= Nat.ppred

theorem Nat.pred_eq_ppred (n : ℕ) : Nat.pred n = Option.getD (Nat.ppred n) 0

theorem Nat.sub_eq_psub (m : ℕ) (n : ℕ) : m - n = Option.getD (Nat.psub m n) 0

@[simp]

theorem Nat.ppred_eq_some {m : ℕ} {n : ℕ} : Nat.ppred n = some m ↔ Nat.succ m = n

@[simp]

theorem Nat.ppred_eq_none {n : ℕ} : Nat.ppred n = none ↔ n = 0

theorem Nat.psub_eq_some {m : ℕ} {n : ℕ} {k : ℕ} : Nat.psub m n = some k ↔ k + n = m

theorem Nat.psub_eq_none {m : ℕ} {n : ℕ} : Nat.psub m n = none ↔ m < n

theorem Nat.ppred_eq_pred {n : ℕ} (h : 0 < n) : Nat.ppred n = some (Nat.pred n)

theorem Nat.psub_eq_sub {m : ℕ} {n : ℕ} (h : n ≤ m) : Nat.psub m n = some (m - n)

theorem Nat.psub_add (m : ℕ) (n : ℕ) (k : ℕ) : Nat.psub m (n + k) = do let __do_lift ← Nat.psub m n Nat.psub __do_lift k

@[inline]

def Nat.psub' (m : ℕ) (n : ℕ) : Option ℕ

Same as psub, but with a more efficient implementation.

Equations

• Nat.psub' m n = if n ≤ m then some (m - n) else none

theorem Nat.psub'_eq_psub (m : ℕ) (n : ℕ) : Nat.psub' m n = Nat.psub m n