@[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

• Nat.fold 0 f x✝ = x✝
• n.succ.fold f x✝ = f n ⋯ (n.fold (fun (i : Nat) (h : i < n) => f i ⋯) x✝)

@[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

• n.foldTR f init = Nat.foldTR.loop✝ n f n ⋯ init

@[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

• Nat.foldRev 0 f x✝ = x✝
• n.succ.foldRev f x✝ = n.foldRev (fun (i : Nat) (h : i < n) => f i ⋯) (f n ⋯ x✝)

@[specialize #[]]

def Nat.any (n : Nat) (f : (i : Nat) → i < n → Bool) : Bool

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

• Nat.any 0 f = false
• n.succ.any f = ((n.any fun (i : Nat) (h : i < n) => f i ⋯) || f n ⋯)

@[inline]

def Nat.anyTR (n : Nat) (f : (i : Nat) → i < n → Bool) : Bool

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:

• Nat.anyTR 4 (fun i _ => i < 5) = true
• Nat.anyTR 7 (fun i _ => i < 5) = true
• Nat.anyTR 7 (fun i _ => i % 2 = 0) = true
• Nat.anyTR 1 (fun i _ => i % 2 = 1) = false

Equations

• n.anyTR f = Nat.anyTR.loop✝ n f n ⋯

@[specialize #[]]

def Nat.all (n : Nat) (f : (i : Nat) → i < n → Bool) : Bool

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

• Nat.all 0 f = true
• n.succ.all f = ((n.all fun (i : Nat) (h : i < n) => f i ⋯) && f n ⋯)

@[inline]

def Nat.allTR (n : Nat) (f : (i : Nat) → i < n → Bool) : Bool

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:

• Nat.allTR 4 (fun i _ => i < 5) = true
• Nat.allTR 7 (fun i _ => i < 5) = false
• Nat.allTR 7 (fun i _ => i % 2 = 0) = false
• Nat.allTR 1 (fun i _ => i % 2 = 0) = true

Equations

• n.allTR f = Nat.allTR.loop✝ n f n ⋯

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

@[csimp]

theorem Nat.fold_eq_foldTR : @fold = @foldTR

theorem Nat.any_congr {n m : Nat} (w : n = m) (f : (i : Nat) → i < n → Bool) : n.any f = m.any fun (i : Nat) (h : i < m) => f i ⋯

@[csimp]

theorem Nat.any_eq_anyTR : any = anyTR

theorem Nat.all_congr {n m : Nat} (w : n = m) (f : (i : Nat) → i < n → Bool) : n.all f = m.all fun (i : Nat) (h : i < m) => f i ⋯

@[csimp]

theorem Nat.all_eq_allTR : all = allTR

dfold

@[specialize #[]]

def Nat.dfold (n : Nat) {α : (i : Nat) → autoParam (i ≤ n) _auto✝ → Type u} (f : (i : Nat) → (h : i < n) → α i ⋯ → α (i + 1) ⋯) (init : α 0 ⋯) : α n ⋯

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

• Nat.dfold f 3 init = init |> f 0 |> f 1 |> f 2 The input and output types of f are indexed by the current index, i.e. f : (i : Nat) → (h : i < n) → α i → α (i + 1).

Equations

• n.dfold f init = Nat.dfold.loop✝ n f n ⋯ (Nat.dfoldCast✝ α ⋯ init)

@[specialize #[]]

def Nat.dfoldRev (n : Nat) {α : (i : Nat) → autoParam (i ≤ n) _auto✝ → Type u} (f : (i : Nat) → (h : i < n) → α (i + 1) ⋯ → α i ⋯) (init : α n ⋯) : α 0 ⋯

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

• Nat.dfoldRev f 3 init = f 0 <| f 1 <| f 2 <| init The input and output types of f are indexed by the current index, i.e. f : (i : Nat) → (h : i < n) → α (i + 1) → α i.

Equations

• Nat.dfoldRev 0 f_2 init_2 = init_2
• n_2.succ.dfoldRev f_2 init_2 = n_2.dfoldRev (fun (i : Nat) (h : i < n_2) => f_2 i ⋯) (f_2 n_2 ⋯ init_2)

Theorems

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 < 0 → Bool} : any 0 f = false

@[simp]

theorem Nat.any_succ {n : Nat} (f : (i : Nat) → i < n + 1 → Bool) : (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 < n → Bool) : 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 < 0 → Bool} : all 0 f = true

@[simp]

theorem Nat.all_succ {n : Nat} (f : (i : Nat) → i < n + 1 → Bool) : (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 < n → Bool) : n.all f = (List.finRange n).all fun (x : Fin n) => match x with | ⟨i, h⟩ => f i h

dfold

@[simp]

theorem Nat.dfold_zero {α : (i : Nat) → autoParam (i ≤ 0) _auto✝ → Type u} (f : (i : Nat) → (h : i < 0) → α i ⋯ → α (i + 1) ⋯) (init : α 0 dfold_zero._proof_7) : dfold 0 f init = init

@[simp]

theorem Nat.dfold_succ {n : Nat} {α : (i : Nat) → autoParam (i ≤ n + 1) _auto✝ → Type u} (f : (i : Nat) → (h : i < n + 1) → α i ⋯ → α (i + 1) ⋯) (init : α 0 ⋯) : (n + 1).dfold f init = f n ⋯ (n.dfold (fun (i : Nat) (h : i < n) => f i ⋯) init)

theorem Nat.dfold_congr {n m : Nat} (w : n = m) {α : (i : Nat) → autoParam (i ≤ n) _auto✝ → Type u} (f : (i : Nat) → (h : i < n) → α i ⋯ → α (i + 1) ⋯) (init : α 0 ⋯) : n.dfold f init = cast ⋯ (m.dfold (fun (i : Nat) (h : i < m) => f i ⋯) init)

theorem Nat.dfold_add {n m : Nat} {α : (i : Nat) → autoParam (i ≤ n + m) _auto✝ → Type u} (f : (i : Nat) → (h : i < n + m) → α i ⋯ → α (i + 1) ⋯) (init : α 0 ⋯) : (n + m).dfold f init = m.dfold (fun (i : Nat) (h : i < m) => f (n + i) ⋯) (n.dfold (fun (i : Nat) (h : i < n) => f i ⋯) init)

@[simp]

theorem Nat.dfoldRev_zero {α : (i : Nat) → autoParam (i ≤ 0) _auto✝ → Type u} (f : (i : Nat) → (x : i < 0) → α (i + 1) ⋯ → α i ⋯) (init : α 0 dfold_zero._proof_7) : dfoldRev 0 f init = init

@[simp]

theorem Nat.dfoldRev_succ {n : Nat} {α : (i : Nat) → autoParam (i ≤ n + 1) _auto✝ → Type u} (f : (i : Nat) → (h : i < n + 1) → α (i + 1) ⋯ → α i ⋯) (init : α (n + 1) ⋯) : (n + 1).dfoldRev f init = n.dfoldRev (fun (i : Nat) (h : i < n) => f i ⋯) (f n ⋯ init)

theorem Nat.dfoldRev_congr {n m : Nat} (w : n = m) {α : (i : Nat) → autoParam (i ≤ n) _auto✝ → Type u} (f : (i : Nat) → (h : i < n) → α (i + 1) ⋯ → α i ⋯) (init : α n ⋯) : n.dfoldRev f init = m.dfoldRev (fun (i : Nat) (h : i < m) => f i ⋯) (cast ⋯ init)

theorem Nat.dfoldRev_add {n m : Nat} {α : (i : Nat) → autoParam (i ≤ n + m) _auto✝ → Type u} (f : (i : Nat) → (h : i < n + m) → α (i + 1) ⋯ → α i ⋯) (init : α (n + m) ⋯) : (n + m).dfoldRev f init = n.dfoldRev (fun (i : Nat) (h : i < n) => f i ⋯) (m.dfoldRev (fun (i : Nat) (h : i < m) => f (n + i) ⋯) init)

@[inline]

def Prod.foldI {α : Type u} (i : Nat × Nat) (f : (j : Nat) → i.fst ≤ j → j < 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

• i.foldI f init = (i.snd - i.fst).fold (fun (j : Nat) (x : j < i.snd - i.fst) => f (i.fst + j) ⋯ ⋯) init

@[inline]

def Prod.anyI (i : Nat × Nat) (f : (j : Nat) → i.fst ≤ j → j < i.snd → Bool) : Bool

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

• i.anyI f = (i.snd - i.fst).any fun (j : Nat) (x : j < i.snd - i.fst) => f (i.fst + j) ⋯ ⋯

@[inline]

def Prod.allI (i : Nat × Nat) (f : (j : Nat) → i.fst ≤ j → j < i.snd → Bool) : Bool

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

• i.allI f = (i.snd - i.fst).all fun (j : Nat) (x : j < i.snd - i.fst) => f (i.fst + j) ⋯ ⋯