Documentation

Init.Data.Nat.Basic

@[specialize #[]]
def Nat.fold {α : Type u} (f : Natαα) (n : Nat) (init : α) :
α

Nat.fold evaluates f on the numbers up to n exclusive, in increasing order:

  • Nat.fold f 3 init = init |> f 0 |> f 1 |> f 2
Equations
Instances For
    @[inline]
    def Nat.foldTR {α : Type u} (f : Natαα) (n : Nat) (init : α) :
    α

    Tail-recursive version of Nat.fold.

    Equations
    Instances For
      @[specialize #[]]
      def Nat.foldTR.loop {α : Type u} (f : Natαα) (n : Nat) :
      Natαα
      Equations
      Instances For
        @[specialize #[]]
        def Nat.foldRev {α : Type u} (f : Natαα) (n : Nat) (init : α) :
        α

        Nat.foldRev evaluates f on the numbers up to n exclusive, in decreasing order:

        Equations
        Instances For
          @[specialize #[]]
          def Nat.any (f : NatBool) :
          NatBool

          any f n = true iff there is i in [0, n-1] s.t. f i = true

          Equations
          Instances For
            @[inline]
            def Nat.anyTR (f : NatBool) (n : Nat) :

            Tail-recursive version of Nat.any.

            Equations
            Instances For
              @[specialize #[]]
              def Nat.anyTR.loop (f : NatBool) (n : Nat) :
              NatBool
              Equations
              Instances For
                @[specialize #[]]
                def Nat.all (f : NatBool) :
                NatBool

                all f n = true iff every i in [0, n-1] satisfies f i = true

                Equations
                Instances For
                  @[inline]
                  def Nat.allTR (f : NatBool) (n : Nat) :

                  Tail-recursive version of Nat.all.

                  Equations
                  Instances For
                    @[specialize #[]]
                    def Nat.allTR.loop (f : NatBool) (n : Nat) :
                    NatBool
                    Equations
                    Instances For
                      @[specialize #[]]
                      def Nat.repeat {α : Type u} (f : αα) (n : Nat) (a : α) :
                      α

                      Nat.repeat f n a is f^(n) a; that is, it iterates f n times on a.

                      Equations
                      Instances For
                        @[inline]
                        def Nat.repeatTR {α : Type u} (f : αα) (n : Nat) (a : α) :
                        α

                        Tail-recursive version of Nat.repeat.

                        Equations
                        Instances For
                          @[specialize #[]]
                          def Nat.repeatTR.loop {α : Type u} (f : αα) :
                          Natαα
                          Equations
                          Instances For
                            def Nat.blt (a : Nat) (b : Nat) :

                            Boolean less-than of natural numbers.

                            Equations
                            Instances For

                              Helper "packing" theorems #

                              @[simp]
                              @[simp]
                              theorem Nat.add_eq {x : Nat} {y : Nat} :
                              Nat.add x y = x + y
                              @[simp]
                              theorem Nat.mul_eq {x : Nat} {y : Nat} :
                              Nat.mul x y = x * y
                              @[simp]
                              theorem Nat.sub_eq {x : Nat} {y : Nat} :
                              Nat.sub x y = x - y
                              @[simp]
                              theorem Nat.lt_eq {x : Nat} {y : Nat} :
                              Nat.lt x y = (x < y)
                              @[simp]
                              theorem Nat.le_eq {x : Nat} {y : Nat} :
                              Nat.le x y = (x y)

                              Helper Bool relation theorems #

                              @[simp]
                              theorem Nat.beq_refl (a : Nat) :
                              @[simp]
                              theorem Nat.beq_eq {x : Nat} {y : Nat} :
                              (Nat.beq x y = true) = (x = y)
                              @[simp]
                              theorem Nat.ble_eq {x : Nat} {y : Nat} :
                              (Nat.ble x y = true) = (x y)
                              @[simp]
                              theorem Nat.blt_eq {x : Nat} {y : Nat} :
                              (Nat.blt x y = true) = (x < y)
                              @[simp]
                              theorem Nat.beq_eq_true_eq (a : Nat) (b : Nat) :
                              ((a == b) = true) = (a = b)
                              @[simp]
                              theorem Nat.not_beq_eq_true_eq (a : Nat) (b : Nat) :
                              ((!a == b) = true) = ¬a = b

                              Nat.add theorems #

                              @[simp]
                              theorem Nat.zero_add (n : Nat) :
                              0 + n = n
                              theorem Nat.succ_add (n : Nat) (m : Nat) :
                              Nat.succ n + m = Nat.succ (n + m)
                              theorem Nat.add_succ (n : Nat) (m : Nat) :
                              n + Nat.succ m = Nat.succ (n + m)
                              theorem Nat.add_one (n : Nat) :
                              n + 1 = Nat.succ n
                              theorem Nat.add_comm (n : Nat) (m : Nat) :
                              n + m = m + n
                              theorem Nat.add_assoc (n : Nat) (m : Nat) (k : Nat) :
                              n + m + k = n + (m + k)
                              theorem Nat.add_left_comm (n : Nat) (m : Nat) (k : Nat) :
                              n + (m + k) = m + (n + k)
                              theorem Nat.add_right_comm (n : Nat) (m : Nat) (k : Nat) :
                              n + m + k = n + k + m
                              theorem Nat.add_left_cancel {n : Nat} {m : Nat} {k : Nat} :
                              n + m = n + km = k
                              theorem Nat.add_right_cancel {n : Nat} {m : Nat} {k : Nat} (h : n + m = k + m) :
                              n = k

                              Nat.mul theorems #

                              @[simp]
                              theorem Nat.mul_zero (n : Nat) :
                              n * 0 = 0
                              theorem Nat.mul_succ (n : Nat) (m : Nat) :
                              n * Nat.succ m = n * m + n
                              @[simp]
                              theorem Nat.zero_mul (n : Nat) :
                              0 * n = 0
                              theorem Nat.succ_mul (n : Nat) (m : Nat) :
                              Nat.succ n * m = n * m + m
                              theorem Nat.mul_comm (n : Nat) (m : Nat) :
                              n * m = m * n
                              @[simp]
                              theorem Nat.mul_one (n : Nat) :
                              n * 1 = n
                              @[simp]
                              theorem Nat.one_mul (n : Nat) :
                              1 * n = n
                              theorem Nat.left_distrib (n : Nat) (m : Nat) (k : Nat) :
                              n * (m + k) = n * m + n * k
                              theorem Nat.right_distrib (n : Nat) (m : Nat) (k : Nat) :
                              (n + m) * k = n * k + m * k
                              theorem Nat.mul_add (n : Nat) (m : Nat) (k : Nat) :
                              n * (m + k) = n * m + n * k
                              theorem Nat.add_mul (n : Nat) (m : Nat) (k : Nat) :
                              (n + m) * k = n * k + m * k
                              theorem Nat.mul_assoc (n : Nat) (m : Nat) (k : Nat) :
                              n * m * k = n * (m * k)
                              theorem Nat.mul_left_comm (n : Nat) (m : Nat) (k : Nat) :
                              n * (m * k) = m * (n * k)

                              Inequalities #

                              theorem Nat.succ_lt_succ {n : Nat} {m : Nat} :
                              n < mNat.succ n < Nat.succ m
                              theorem Nat.lt_succ_of_le {n : Nat} {m : Nat} :
                              n mn < Nat.succ m
                              @[simp]
                              theorem Nat.sub_zero (n : Nat) :
                              n - 0 = n
                              theorem Nat.pred_le (n : Nat) :
                              theorem Nat.pred_lt {n : Nat} :
                              n 0Nat.pred n < n
                              theorem Nat.sub_le (n : Nat) (m : Nat) :
                              n - m n
                              theorem Nat.sub_lt {n : Nat} {m : Nat} :
                              0 < n0 < mn - m < n
                              theorem Nat.sub_succ (n : Nat) (m : Nat) :
                              n - Nat.succ m = Nat.pred (n - m)
                              theorem Nat.succ_sub_succ (n : Nat) (m : Nat) :
                              @[simp]
                              theorem Nat.sub_self (n : Nat) :
                              n - n = 0
                              theorem Nat.sub_add_eq (a : Nat) (b : Nat) (c : Nat) :
                              a - (b + c) = a - b - c
                              theorem Nat.lt_of_lt_of_le {n : Nat} {m : Nat} {k : Nat} :
                              n < mm kn < k
                              theorem Nat.lt_of_lt_of_eq {n : Nat} {m : Nat} {k : Nat} :
                              n < mm = kn < k
                              instance Nat.instTransNatLtInstLTNat :
                              Trans (fun (x x_1 : Nat) => x < x_1) (fun (x x_1 : Nat) => x < x_1) fun (x x_1 : Nat) => x < x_1
                              Equations
                              instance Nat.instTransNatLeInstLENat :
                              Trans (fun (x x_1 : Nat) => x x_1) (fun (x x_1 : Nat) => x x_1) fun (x x_1 : Nat) => x x_1
                              Equations
                              instance Nat.instTransNatLtInstLTNatLeInstLENat :
                              Trans (fun (x x_1 : Nat) => x < x_1) (fun (x x_1 : Nat) => x x_1) fun (x x_1 : Nat) => x < x_1
                              Equations
                              instance Nat.instTransNatLeInstLENatLtInstLTNat :
                              Trans (fun (x x_1 : Nat) => x x_1) (fun (x x_1 : Nat) => x < x_1) fun (x x_1 : Nat) => x < x_1
                              Equations
                              theorem Nat.le_of_eq {n : Nat} {m : Nat} (p : n = m) :
                              n m
                              theorem Nat.le_of_succ_le {n : Nat} {m : Nat} (h : Nat.succ n m) :
                              n m
                              theorem Nat.le_of_lt {n : Nat} {m : Nat} (h : n < m) :
                              n m
                              theorem Nat.lt.step {n : Nat} {m : Nat} :
                              n < mn < Nat.succ m
                              theorem Nat.eq_zero_or_pos (n : Nat) :
                              n = 0 n > 0
                              theorem Nat.lt.base (n : Nat) :
                              theorem Nat.le_total (m : Nat) (n : Nat) :
                              m n n m
                              theorem Nat.eq_zero_of_le_zero {n : Nat} (h : n 0) :
                              n = 0
                              theorem Nat.lt_of_succ_lt {n : Nat} {m : Nat} :
                              Nat.succ n < mn < m
                              theorem Nat.lt_of_succ_lt_succ {n : Nat} {m : Nat} :
                              Nat.succ n < Nat.succ mn < m
                              theorem Nat.lt_of_succ_le {n : Nat} {m : Nat} (h : Nat.succ n m) :
                              n < m
                              theorem Nat.succ_le_of_lt {n : Nat} {m : Nat} (h : n < m) :
                              theorem Nat.zero_lt_of_lt {a : Nat} {b : Nat} :
                              a < b0 < b
                              theorem Nat.zero_lt_of_ne_zero {a : Nat} (h : a 0) :
                              0 < a
                              theorem Nat.ne_of_lt {a : Nat} {b : Nat} (h : a < b) :
                              a b
                              theorem Nat.le_or_eq_of_le_succ {m : Nat} {n : Nat} (h : m Nat.succ n) :
                              m n m = Nat.succ n
                              theorem Nat.le_add_right (n : Nat) (k : Nat) :
                              n n + k
                              theorem Nat.le_add_left (n : Nat) (m : Nat) :
                              n m + n
                              theorem Nat.le.dest {n : Nat} {m : Nat} :
                              n m∃ (k : Nat), n + k = m
                              theorem Nat.le.intro {n : Nat} {m : Nat} {k : Nat} (h : n + k = m) :
                              n m
                              theorem Nat.not_le_of_gt {n : Nat} {m : Nat} (h : n > m) :
                              ¬n m
                              theorem Nat.gt_of_not_le {n : Nat} {m : Nat} (h : ¬n m) :
                              n > m
                              theorem Nat.ge_of_not_lt {n : Nat} {m : Nat} (h : ¬n < m) :
                              n m
                              instance Nat.instAntisymmNatLeInstLENat :
                              Antisymm fun (x x_1 : Nat) => x x_1
                              Equations
                              theorem Nat.add_le_add_left {n : Nat} {m : Nat} (h : n m) (k : Nat) :
                              k + n k + m
                              theorem Nat.add_le_add_right {n : Nat} {m : Nat} (h : n m) (k : Nat) :
                              n + k m + k
                              theorem Nat.add_lt_add_left {n : Nat} {m : Nat} (h : n < m) (k : Nat) :
                              k + n < k + m
                              theorem Nat.add_lt_add_right {n : Nat} {m : Nat} (h : n < m) (k : Nat) :
                              n + k < m + k
                              theorem Nat.add_le_add {a : Nat} {b : Nat} {c : Nat} {d : Nat} (h₁ : a b) (h₂ : c d) :
                              a + c b + d
                              theorem Nat.add_lt_add {a : Nat} {b : Nat} {c : Nat} {d : Nat} (h₁ : a < b) (h₂ : c < d) :
                              a + c < b + d
                              theorem Nat.le_of_add_le_add_left {a : Nat} {b : Nat} {c : Nat} (h : a + b a + c) :
                              b c
                              theorem Nat.le_of_add_le_add_right {a : Nat} {b : Nat} {c : Nat} :
                              a + b c + ba c

                              Basic theorems for comparing numerals #

                              mul + order #

                              theorem Nat.mul_le_mul_left {n : Nat} {m : Nat} (k : Nat) (h : n m) :
                              k * n k * m
                              theorem Nat.mul_le_mul_right {n : Nat} {m : Nat} (k : Nat) (h : n m) :
                              n * k m * k
                              theorem Nat.mul_le_mul {n₁ : Nat} {m₁ : Nat} {n₂ : Nat} {m₂ : Nat} (h₁ : n₁ n₂) (h₂ : m₁ m₂) :
                              n₁ * m₁ n₂ * m₂
                              theorem Nat.mul_lt_mul_of_pos_left {n : Nat} {m : Nat} {k : Nat} (h : n < m) (hk : k > 0) :
                              k * n < k * m
                              theorem Nat.mul_lt_mul_of_pos_right {n : Nat} {m : Nat} {k : Nat} (h : n < m) (hk : k > 0) :
                              n * k < m * k
                              theorem Nat.mul_pos {n : Nat} {m : Nat} (ha : n > 0) (hb : m > 0) :
                              n * m > 0
                              theorem Nat.le_of_mul_le_mul_left {a : Nat} {b : Nat} {c : Nat} (h : c * a c * b) (hc : 0 < c) :
                              a b
                              theorem Nat.eq_of_mul_eq_mul_left {m : Nat} {k : Nat} {n : Nat} (hn : 0 < n) (h : n * m = n * k) :
                              m = k
                              theorem Nat.eq_of_mul_eq_mul_right {n : Nat} {m : Nat} {k : Nat} (hm : 0 < m) (h : n * m = k * m) :
                              n = k

                              power #

                              theorem Nat.pow_succ (n : Nat) (m : Nat) :
                              n ^ Nat.succ m = n ^ m * n
                              theorem Nat.pow_zero (n : Nat) :
                              n ^ 0 = 1
                              theorem Nat.pow_le_pow_of_le_left {n : Nat} {m : Nat} (h : n m) (i : Nat) :
                              n ^ i m ^ i
                              theorem Nat.pow_le_pow_of_le_right {n : Nat} (hx : n > 0) {i : Nat} {j : Nat} :
                              i jn ^ i n ^ j
                              theorem Nat.pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) :
                              0 < n ^ m

                              min/max #

                              @[inline, reducible]
                              abbrev Nat.min (n : Nat) (m : Nat) :

                              Nat.min a b is the minimum of a and b:

                              Equations
                              Instances For
                                theorem Nat.min_def {n : Nat} {m : Nat} :
                                min n m = if n m then n else m
                                Equations
                                @[inline, reducible]
                                abbrev Nat.max (n : Nat) (m : Nat) :

                                Nat.max a b is the maximum of a and b:

                                Equations
                                Instances For
                                  theorem Nat.max_def {n : Nat} {m : Nat} :
                                  max n m = if n m then m else n

                                  Auxiliary theorems for well-founded recursion #

                                  theorem Nat.not_eq_zero_of_lt {b : Nat} {a : Nat} (h : b < a) :
                                  a 0
                                  theorem Nat.pred_lt' {n : Nat} {m : Nat} (h : m < n) :

                                  sub/pred theorems #

                                  theorem Nat.add_sub_self_left (a : Nat) (b : Nat) :
                                  a + b - a = b
                                  theorem Nat.add_sub_self_right (a : Nat) (b : Nat) :
                                  a + b - b = a
                                  theorem Nat.sub_le_succ_sub (a : Nat) (i : Nat) :
                                  a - i Nat.succ a - i
                                  theorem Nat.zero_lt_sub_of_lt {i : Nat} {a : Nat} (h : i < a) :
                                  0 < a - i
                                  theorem Nat.sub_succ_lt_self (a : Nat) (i : Nat) (h : i < a) :
                                  a - (i + 1) < a - i
                                  theorem Nat.succ_pred {a : Nat} (h : a 0) :
                                  theorem Nat.sub_ne_zero_of_lt {a : Nat} {b : Nat} :
                                  a < bb - a 0
                                  theorem Nat.add_sub_of_le {a : Nat} {b : Nat} (h : a b) :
                                  a + (b - a) = b
                                  theorem Nat.sub_add_cancel {n : Nat} {m : Nat} (h : m n) :
                                  n - m + m = n
                                  theorem Nat.add_sub_add_right (n : Nat) (k : Nat) (m : Nat) :
                                  n + k - (m + k) = n - m
                                  theorem Nat.add_sub_add_left (k : Nat) (n : Nat) (m : Nat) :
                                  k + n - (k + m) = n - m
                                  theorem Nat.add_sub_cancel (n : Nat) (m : Nat) :
                                  n + m - m = n
                                  theorem Nat.add_sub_cancel_left (n : Nat) (m : Nat) :
                                  n + m - n = m
                                  theorem Nat.add_sub_assoc {m : Nat} {k : Nat} (h : k m) (n : Nat) :
                                  n + m - k = n + (m - k)
                                  theorem Nat.eq_add_of_sub_eq {a : Nat} {b : Nat} {c : Nat} (hle : b a) (h : a - b = c) :
                                  a = c + b
                                  theorem Nat.sub_eq_of_eq_add {a : Nat} {b : Nat} {c : Nat} (h : a = c + b) :
                                  a - b = c
                                  theorem Nat.le_add_of_sub_le {a : Nat} {b : Nat} {c : Nat} (h : a - b c) :
                                  a c + b
                                  theorem Nat.sub_lt_sub_left {k : Nat} {m : Nat} {n : Nat} :
                                  k < mk < nm - n < m - k
                                  @[simp]
                                  theorem Nat.zero_sub (n : Nat) :
                                  0 - n = 0
                                  theorem Nat.sub_self_add (n : Nat) (m : Nat) :
                                  n - (n + m) = 0
                                  theorem Nat.sub_eq_zero_of_le {n : Nat} {m : Nat} (h : n m) :
                                  n - m = 0
                                  theorem Nat.sub_le_of_le_add {a : Nat} {b : Nat} {c : Nat} (h : a c + b) :
                                  a - b c
                                  theorem Nat.add_le_of_le_sub {a : Nat} {b : Nat} {c : Nat} (hle : b c) (h : a c - b) :
                                  a + b c
                                  theorem Nat.le_sub_of_add_le {a : Nat} {b : Nat} {c : Nat} (h : a + b c) :
                                  a c - b
                                  theorem Nat.add_lt_of_lt_sub {a : Nat} {b : Nat} {c : Nat} (h : a < c - b) :
                                  a + b < c
                                  theorem Nat.lt_sub_of_add_lt {a : Nat} {b : Nat} {c : Nat} (h : a + b < c) :
                                  a < c - b
                                  @[simp]
                                  theorem Nat.pred_zero :
                                  @[simp]
                                  theorem Nat.pred_succ (n : Nat) :
                                  theorem Nat.sub.elim {motive : NatProp} (x : Nat) (y : Nat) (h₁ : y x∀ (k : Nat), x = y + kmotive k) (h₂ : x < ymotive 0) :
                                  motive (x - y)
                                  theorem Nat.mul_pred_left (n : Nat) (m : Nat) :
                                  Nat.pred n * m = n * m - m
                                  theorem Nat.mul_pred_right (n : Nat) (m : Nat) :
                                  n * Nat.pred m = n * m - n
                                  theorem Nat.sub_sub (n : Nat) (m : Nat) (k : Nat) :
                                  n - m - k = n - (m + k)
                                  theorem Nat.mul_sub_right_distrib (n : Nat) (m : Nat) (k : Nat) :
                                  (n - m) * k = n * k - m * k
                                  theorem Nat.mul_sub_left_distrib (n : Nat) (m : Nat) (k : Nat) :
                                  n * (m - k) = n * m - n * k

                                  Helper normalization theorems #

                                  theorem Nat.not_le_eq (a : Nat) (b : Nat) :
                                  (¬a b) = (b + 1 a)
                                  theorem Nat.not_ge_eq (a : Nat) (b : Nat) :
                                  (¬a b) = (a + 1 b)
                                  theorem Nat.not_lt_eq (a : Nat) (b : Nat) :
                                  (¬a < b) = (b a)
                                  theorem Nat.not_gt_eq (a : Nat) (b : Nat) :
                                  (¬a > b) = (a b)

                                  csimp theorems #

                                  theorem Nat.fold_eq_foldTR.go (α : Type u_1) (f : Natαα) (init : α) (m : Nat) (n : Nat) :
                                  Nat.foldTR.loop f (m + n) m (Nat.fold f n init) = Nat.fold f (m + n) init
                                  theorem Nat.any_eq_anyTR.go (f : NatBool) (m : Nat) (n : Nat) :
                                  (Nat.any f n || Nat.anyTR.loop f (m + n) m) = Nat.any f (m + n)
                                  theorem Nat.all_eq_allTR.go (f : NatBool) (m : Nat) (n : Nat) :
                                  (Nat.all f n && Nat.allTR.loop f (m + n) m) = Nat.all f (m + n)
                                  theorem Nat.repeat_eq_repeatTR.go (α : Type u_1) (f : αα) (init : α) (m : Nat) (n : Nat) :
                                  Nat.repeatTR.loop f m (Nat.repeat f n init) = Nat.repeat f (m + n) init
                                  @[inline]
                                  def Prod.foldI {α : Type u} (f : Natαα) (i : Nat × Nat) (a : α) :
                                  α

                                  (start, stop).foldI f a evaluates f on all the numbers from start (inclusive) to stop (exclusive) in increasing order:

                                  • (5, 8).foldI f init = init |> f 5 |> f 6 |> f 7
                                  Equations
                                  Instances For
                                    @[inline]
                                    def Prod.anyI (f : NatBool) (i : Nat × Nat) :

                                    (start, stop).anyI f a returns true if f is true for some natural number from start (inclusive) to stop (exclusive):

                                    • (5, 8).anyI f = f 5 || f 6 || f 7
                                    Equations
                                    Instances For
                                      @[inline]
                                      def Prod.allI (f : NatBool) (i : Nat × Nat) :

                                      (start, stop).allI f a returns true if f is true for all natural numbers from start (inclusive) to stop (exclusive):

                                      • (5, 8).anyI f = f 5 && f 6 && f 7
                                      Equations
                                      Instances For