@[specialize #[]]

def Nat.fold {α : Type u} (n : Nat) (f : (i : Nat) → i < n → α → α) (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

• 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 : α) : α

Tail-recursive version of Nat.fold.

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

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

• Nat.foldRev f 3 init = f 0 <| f 1 <| f 2 <| init

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

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

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

Tail-recursive version of Nat.any.

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

all f n = true iff every i in [0, n-1] satisfies f i = 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

Tail-recursive version of Nat.all.

@[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 : α) : Nat.foldTR.loop n f j h init = Nat.foldTR.loop m (fun (i : Nat) (h : i < m) => f i ⋯) j ⋯ init

@[csimp]

theorem Nat.fold_eq_foldTR : @Nat.fold = @Nat.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 = Nat.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) : Nat.anyTR.loop n f j h = Nat.anyTR.loop m (fun (i : Nat) (h : i < m) => f i ⋯) j ⋯

@[csimp]

theorem Nat.any_eq_anyTR : Nat.any = Nat.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 ⋯) || Nat.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) : Nat.allTR.loop n f j h = Nat.allTR.loop m (fun (i : Nat) (h : i < m) => f i ⋯) j ⋯

@[csimp]

theorem Nat.all_eq_allTR : Nat.all = Nat.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 ⋯) && Nat.allTR.loop (m + n) f m ⋯)

@[simp]

theorem Nat.fold_zero {α : Type u} (f : (i : Nat) → i < 0 → α → α) (init : α) : Nat.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 : α) : Nat.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} : Nat.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} : Nat.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 → α → α) (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

@[inline]

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

(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

• 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

(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

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