Documentation

Init.Data.Nat.Fold

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

Iterates the application of a function f to a starting value init, n times. At each step, f is applied to the current value and to the next natural number less than n, in increasing order.

Examples:

  • Nat.fold 3 f init = (init |> f 0 (by simp) |> f 1 (by simp) |> f 2 (by simp))
  • Nat.fold 4 (fun i _ xs => xs.push i) #[] = #[0, 1, 2, 3]
  • Nat.fold 0 (fun i _ xs => xs.push i) #[] = #[]
Equations
    Instances For
      @[inline]
      def Nat.foldTR {α : Type u} (n : Nat) (f : (i : Nat) → i < nαα) (init : α) :
      α

      Iterates the application of a function f to a starting value init, n times. At each step, f is applied to the current value and to the next natural number less than n, in increasing order.

      This is a tail-recursive version of Nat.fold that's used at runtime.

      Examples:

      • Nat.foldTR 3 f init = (init |> f 0 (by simp) |> f 1 (by simp) |> f 2 (by simp))
      • Nat.foldTR 4 (fun i _ xs => xs.push i) #[] = #[0, 1, 2, 3]
      • Nat.foldTR 0 (fun i _ xs => xs.push i) #[] = #[]
      Equations
        Instances For
          @[specialize #[]]
          def Nat.foldTR.loop {α : Type u} (n : Nat) (f : (i : Nat) → i < nαα) (j : Nat) :
          j nαα
          Equations
            Instances For
              @[specialize #[]]
              def Nat.foldRev {α : Type u} (n : Nat) (f : (i : Nat) → i < nαα) (init : α) :
              α

              Iterates the application of a function f to a starting value init, n times. At each step, f is applied to the current value and to the next natural number less than n, in decreasing order.

              Examples:

              • Nat.foldRev 3 f init = (f 0 (by simp) <| f 1 (by simp) <| f 2 (by simp) init)
              • Nat.foldRev 4 (fun i _ xs => xs.push i) #[] = #[3, 2, 1, 0]
              • Nat.foldRev 0 (fun i _ xs => xs.push i) #[] = #[]
              Equations
                Instances For
                  @[specialize #[]]
                  def Nat.any (n : Nat) (f : (i : Nat) → i < nBool) :

                  Checks whether there is some number less that the given bound for which f returns true.

                  Examples:

                  • Nat.any 4 (fun i _ => i < 5) = true
                  • Nat.any 7 (fun i _ => i < 5) = true
                  • Nat.any 7 (fun i _ => i % 2 = 0) = true
                  • Nat.any 1 (fun i _ => i % 2 = 1) = false
                  Equations
                    Instances For
                      @[inline]
                      def Nat.anyTR (n : Nat) (f : (i : Nat) → i < nBool) :

                      Checks whether there is some number less that the given bound for which f returns true.

                      This is a tail-recursive equivalent of Nat.any that's used at runtime.

                      Examples:

                      Equations
                        Instances For
                          @[specialize #[]]
                          def Nat.anyTR.loop (n : Nat) (f : (i : Nat) → i < nBool) (i : Nat) :
                          i nBool
                          Equations
                            Instances For
                              @[specialize #[]]
                              def Nat.all (n : Nat) (f : (i : Nat) → i < nBool) :

                              Checks whether f returns true for every number strictly less than a bound.

                              Examples:

                              • Nat.all 4 (fun i _ => i < 5) = true
                              • Nat.all 7 (fun i _ => i < 5) = false
                              • Nat.all 7 (fun i _ => i % 2 = 0) = false
                              • Nat.all 1 (fun i _ => i % 2 = 0) = true
                              Equations
                                Instances For
                                  @[inline]
                                  def Nat.allTR (n : Nat) (f : (i : Nat) → i < nBool) :

                                  Checks whether f returns true for every number strictly less than a bound.

                                  This is a tail-recursive equivalent of Nat.all that's used at runtime.

                                  Examples:

                                  Equations
                                    Instances For
                                      @[specialize #[]]
                                      def Nat.allTR.loop (n : Nat) (f : (i : Nat) → i < nBool) (i : Nat) :
                                      i nBool
                                      Equations
                                        Instances For

                                          csimp theorems #

                                          theorem Nat.fold_congr {α : Type u} {n m : Nat} (w : n = m) (f : (i : Nat) → i < nαα) (init : α) :
                                          n.fold f init = m.fold (fun (i : Nat) (h : i < m) => f i ) init
                                          theorem Nat.foldTR_loop_congr {α : Type u} {n m : Nat} (w : n = m) (f : (i : Nat) → i < nαα) (j : Nat) (h : j n) (init : α) :
                                          foldTR.loop n f j h init = foldTR.loop m (fun (i : Nat) (h : i < m) => f i ) j init
                                          theorem Nat.fold_eq_foldTR.go (α : Type u_1) (init : α) (m n : Nat) (f : (i : Nat) → i < m + nαα) :
                                          (m + n).fold f init = foldTR.loop (m + n) f m (n.fold (fun (i : Nat) (h : i < n) => f i ) init)
                                          theorem Nat.any_congr {n m : Nat} (w : n = m) (f : (i : Nat) → i < nBool) :
                                          n.any f = m.any fun (i : Nat) (h : i < m) => f i
                                          theorem Nat.anyTR_loop_congr {n m : Nat} (w : n = m) (f : (i : Nat) → i < nBool) (j : Nat) (h : j n) :
                                          anyTR.loop n f j h = anyTR.loop m (fun (i : Nat) (h : i < m) => f i ) j
                                          @[csimp]
                                          theorem Nat.any_eq_anyTR.go (m n : Nat) (f : (i : Nat) → i < m + nBool) :
                                          (m + n).any f = ((n.any fun (i : Nat) (h : i < n) => f i ) || anyTR.loop (m + n) f m )
                                          theorem Nat.all_congr {n m : Nat} (w : n = m) (f : (i : Nat) → i < nBool) :
                                          n.all f = m.all fun (i : Nat) (h : i < m) => f i
                                          theorem Nat.allTR_loop_congr {n m : Nat} (w : n = m) (f : (i : Nat) → i < nBool) (j : Nat) (h : j n) :
                                          allTR.loop n f j h = allTR.loop m (fun (i : Nat) (h : i < m) => f i ) j
                                          @[csimp]
                                          theorem Nat.all_eq_allTR.go (m n : Nat) (f : (i : Nat) → i < m + nBool) :
                                          (m + n).all f = ((n.all fun (i : Nat) (h : i < n) => f i ) && allTR.loop (m + n) f m )

                                          fold #

                                          @[simp]
                                          theorem Nat.fold_zero {α : Type u} (f : (i : Nat) → i < 0αα) (init : α) :
                                          fold 0 f init = init
                                          @[simp]
                                          theorem Nat.fold_succ {α : Type u} (n : Nat) (f : (i : Nat) → i < n + 1αα) (init : α) :
                                          (n + 1).fold f init = f n (n.fold (fun (i : Nat) (h : i < n) => f i ) init)
                                          theorem Nat.fold_eq_finRange_foldl {α : Type u} (n : Nat) (f : (i : Nat) → i < nαα) (init : α) :
                                          n.fold f init = List.foldl (fun (acc : α) (x : Fin n) => match x with | i, h => f i h acc) init (List.finRange n)

                                          foldRev #

                                          @[simp]
                                          theorem Nat.foldRev_zero {α : Type u} (f : (i : Nat) → i < 0αα) (init : α) :
                                          foldRev 0 f init = init
                                          @[simp]
                                          theorem Nat.foldRev_succ {α : Type u} (n : Nat) (f : (i : Nat) → i < n + 1αα) (init : α) :
                                          (n + 1).foldRev f init = n.foldRev (fun (i : Nat) (h : i < n) => f i ) (f n init)
                                          theorem Nat.foldRev_eq_finRange_foldr {α : Type u} (n : Nat) (f : (i : Nat) → i < nαα) (init : α) :
                                          n.foldRev f init = List.foldr (fun (x : Fin n) (acc : α) => match x with | i, h => f i h acc) init (List.finRange n)

                                          any #

                                          @[simp]
                                          theorem Nat.any_zero {f : (i : Nat) → i < 0Bool} :
                                          any 0 f = false
                                          @[simp]
                                          theorem Nat.any_succ {n : Nat} (f : (i : Nat) → i < n + 1Bool) :
                                          (n + 1).any f = ((n.any fun (i : Nat) (h : i < n) => f i ) || f n )
                                          theorem Nat.any_eq_finRange_any {n : Nat} (f : (i : Nat) → i < nBool) :
                                          n.any f = (List.finRange n).any fun (x : Fin n) => match x with | i, h => f i h

                                          all #

                                          @[simp]
                                          theorem Nat.all_zero {f : (i : Nat) → i < 0Bool} :
                                          all 0 f = true
                                          @[simp]
                                          theorem Nat.all_succ {n : Nat} (f : (i : Nat) → i < n + 1Bool) :
                                          (n + 1).all f = ((n.all fun (i : Nat) (h : i < n) => f i ) && f n )
                                          theorem Nat.all_eq_finRange_all {n : Nat} (f : (i : Nat) → i < nBool) :
                                          n.all f = (List.finRange n).all fun (x : Fin n) => match x with | i, h => f i h
                                          @[inline]
                                          def Prod.foldI {α : Type u} (i : Nat × Nat) (f : (j : Nat) → i.fst jj < i.sndαα) (init : α) :
                                          α

                                          Combines an initial value with each natural number from a range, in increasing order.

                                          In particular, (start, stop).foldI f init applies fon all the numbers from start (inclusive) to stop (exclusive) in increasing order:

                                          Examples:

                                          • (5, 8).foldI (fun j _ _ xs => xs.push j) #[] = (#[] |>.push 5 |>.push 6 |>.push 7)
                                          • (5, 8).foldI (fun j _ _ xs => xs.push j) #[] = #[5, 6, 7]
                                          • (5, 8).foldI (fun j _ _ xs => toString j :: xs) [] = ["7", "6", "5"]
                                          Equations
                                            Instances For
                                              @[inline]
                                              def Prod.anyI (i : Nat × Nat) (f : (j : Nat) → i.fst jj < i.sndBool) :

                                              Checks whether a predicate holds for any natural number in a range.

                                              In particular, (start, stop).allI f returns true if f is true for any natural number from start (inclusive) to stop (exclusive).

                                              Examples:

                                              • (5, 8).anyI (fun j _ _ => j == 6) = (5 == 6) || (6 == 6) || (7 == 6)
                                              • (5, 8).anyI (fun j _ _ => j % 2 = 0) = true
                                              • (6, 6).anyI (fun j _ _ => j % 2 = 0) = false
                                              Equations
                                                Instances For
                                                  @[inline]
                                                  def Prod.allI (i : Nat × Nat) (f : (j : Nat) → i.fst jj < i.sndBool) :

                                                  Checks whether a predicate holds for all natural numbers in a range.

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

                                                  Examples:

                                                  • (5, 8).allI (fun j _ _ => j < 10) = (5 < 10) && (6 < 10) && (7 < 10)
                                                  • (5, 8).allI (fun j _ _ => j % 2 = 0) = false
                                                  • (6, 7).allI (fun j _ _ => j % 2 = 0) = true
                                                  Equations
                                                    Instances For