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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

# csimp theorems #

source
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
source
theorem Nat.foldRev_congr {α : Type u} {n m : Nat} (w : n = m) (f : (i : Nat) → i < n → α → α) (init : α) :
n.foldRev f init = m.foldRev (fun (i : Nat) (h : i < m) => f i ⋯) init
source
@[csimp]
theorem Nat.fold_eq_foldTR :
@fold = @foldTR
source
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 ⋯
source
@[csimp]
theorem Nat.any_eq_anyTR :
any = anyTR
source
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 ⋯
source
@[csimp]
theorem Nat.all_eq_allTR :
all = allTR

# `dfold` #

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

Instances For

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

Instances For

# Theorems #

### `fold` #

source
@[simp]
theorem Nat.fold_zero {α : Type u} (f : (i : Nat) → i < 0 → α → α) (init : α) :
fold 0 f init = init
source
@[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)
source
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)
source
theorem Nat.fold_add {α : Type u_1} {n m : Nat} (f : (i : Nat) → i < n + m → α → α) (init : α) :
(n + m).fold f init = m.fold (fun (i : Nat) (h : i < m) => f (n + i) ⋯) (n.fold (fun (i : Nat) (h : i < n) => f i ⋯) init)

### `foldRev` #

source
@[simp]
theorem Nat.foldRev_zero {α : Type u} (f : (i : Nat) → i < 0 → α → α) (init : α) :
foldRev 0 f init = init
source
@[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)
source
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)
source
theorem Nat.foldRev_add {α : Type u_1} {n m : Nat} (f : (i : Nat) → i < n + m → α → α) (init : α) :
(n + m).foldRev f init = n.foldRev (fun (i : Nat) (h : i < n) => f i ⋯) (m.foldRev (fun (i : Nat) (h : i < m) => f (n + i) ⋯) init)

### `any` #

source
@[simp]
theorem Nat.any_zero {f : (i : Nat) → i < 0 → Bool} :
any 0 f = false
source
@[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 ⋯)
source
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` #

source
@[simp]
theorem Nat.all_zero {f : (i : Nat) → i < 0 → Bool} :
all 0 f = true
source
@[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 ⋯)
source
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` #

source
@[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
source
@[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)
source
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)
source
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)
source
@[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
source
@[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)
source
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)
source
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)
source
@[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 `f`on 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

Instances For

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

Instances For

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

Instances For