Documentation

Mathlib.Data.Nat.PSub

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 #

source
def Nat.ppred :
ℕ → Option ℕ

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

Equations
    Instances For
      source
      @[simp]
      theorem Nat.ppred_zero :
      ppred 0 = none
      source
      @[simp]
      theorem Nat.ppred_succ {n : ℕ} :
      n.succ.ppred = some n
      source
      def Nat.psub (m : ℕ) :
      ℕ → Option ℕ

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

      Equations
        Instances For
          source
          @[simp]
          theorem Nat.psub_zero {m : ℕ} :
          m.psub 0 = some m
          source
          @[simp]
          theorem Nat.psub_succ {m n : ℕ} :
          m.psub n.succ = m.psub n >>= ppred
          source
          theorem Nat.pred_eq_ppred (n : ℕ) :
          n.pred = n.ppred.getD 0
          source
          theorem Nat.sub_eq_psub (m n : ℕ) :
          m - n = (m.psub n).getD 0
          source
          @[simp]
          theorem Nat.ppred_eq_some {m n : ℕ} :
          n.ppred = some m ↔ m.succ = n
          source
          @[simp]
          theorem Nat.ppred_eq_none {n : ℕ} :
          n.ppred = none ↔ n = 0
          source
          theorem Nat.psub_eq_some {m n k : ℕ} :
          m.psub n = some k ↔ k + n = m
          source
          theorem Nat.psub_eq_none {m n : ℕ} :
          m.psub n = none ↔ m < n
          source
          theorem Nat.ppred_eq_pred {n : ℕ} (h : 0 < n) :
          n.ppred = some n.pred
          source
          theorem Nat.psub_eq_sub {m n : ℕ} (h : n ≤ m) :
          m.psub n = some (m - n)
          source
          theorem Nat.psub_add (m n k : ℕ) :
          m.psub (n + k) = do let __do_lift ← m.psub n __do_lift.psub k
          source
          @[inline]
          def Nat.psub' (m n : ℕ) :
          Option ℕ

          Same as psub, but with a more efficient implementation.

          Equations
            Instances For
              source
              theorem Nat.psub'_eq_psub (m n : ℕ) :
              m.psub' n = m.psub n