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 #

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

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

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

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

      Same as psub, but with a more efficient implementation.

      Equations
      • m.psub' n = if n m then some (m - n) else none
      Instances For
        theorem Nat.psub'_eq_psub (m : ) (n : ) :
        m.psub' n = m.psub n