@[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.foldTR.loop {α : Type u} (n : Nat) (f : (i : Nat) → i < n → α → α) (j : Nat) : j ≤ n → α → α

Equations

• Nat.foldTR.loop n f 0 h x = x
• Nat.foldTR.loop n f m.succ h x = Nat.foldTR.loop n f m ⋯ (f (n - m.succ) ⋯ x)

@[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.anyTR.loop (n : Nat) (f : (i : Nat) → i < n → Bool) (i : Nat) : i ≤ n → Bool

Equations

• Nat.anyTR.loop n f 0 h = false
• Nat.anyTR.loop n f m.succ h = (f (n - m.succ) ⋯ || Nat.anyTR.loop n f m ⋯)

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

@[specialize #[]]

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

Equations

• Nat.allTR.loop n f 0 h = true
• Nat.allTR.loop n f m.succ h = (f (n - m.succ) ⋯ && Nat.allTR.loop n f m ⋯)

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

@[csimp]

theorem Nat.fold_eq_foldTR : @fold = @foldTR

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 < n → Bool) : 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 < n → Bool) (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 : any = anyTR

theorem Nat.any_eq_anyTR.go (m n : Nat) (f : (i : Nat) → i < m + n → Bool) : (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 < n → Bool) : 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 < n → Bool) (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 : all = allTR

theorem Nat.all_eq_allTR.go (m n : Nat) (f : (i : Nat) → i < m + n → Bool) : (m + n).all f = ((n.all fun (i : Nat) (h : i < n) => f i ⋯) && allTR.loop (m + n) f m ⋯)

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

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

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

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

@[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 in 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) ⋯ ⋯