dfoldrM #
theorem
Fin.dfoldrM_loop_zero
{m : Type u_1 → Type u_2}
{n : Nat}
{α : Fin (n + 1) → Type u_1}
{h : 0 < n + 1}
[Monad m]
(f : (i : Fin n) → α i.succ → m (α i.castSucc))
(x : α ⟨0, h⟩)
:
dfoldrM.loop n α f 0 h x = pure x
theorem
Fin.dfoldrM_loop_succ
{m : Type u_1 → Type u_2}
{n : Nat}
{α : Fin (n + 1) → Type u_1}
{i : Nat}
{h : i + 1 < n + 1}
[Monad m]
(f : (i : Fin n) → α i.succ → m (α i.castSucc))
(x : α ⟨i + 1, h⟩)
:
dfoldrM.loop n α f (i + 1) h x = f ⟨i, ⋯⟩ x >>= dfoldrM.loop n α f i ⋯
theorem
Fin.dfoldrM_loop
{m : Type u_1 → Type u_2}
{n : Nat}
{α : Fin (n + 1 + 1) → Type u_1}
{i : Nat}
{h : i + 1 < n + 1 + 1}
[Monad m]
[LawfulMonad m]
(f : (i : Fin (n + 1)) → α i.succ → m (α i.castSucc))
(x : α ⟨i + 1, h⟩)
:
dfoldrM.loop (n + 1) α f (i + 1) h x = dfoldrM.loop n (α ∘ succ) (fun (x : Fin n) => f x.succ) i ⋯ x >>= f 0
@[simp]
theorem
Fin.dfoldrM_eq_foldrM
{m : Type u_1 → Type u_2}
{n : Nat}
{α : Type u_1}
[Monad m]
[LawfulMonad m]
(f : Fin n → α → m α)
(x : (fun (x : Fin (n + 1)) => α) (last n))
:
dfoldrM n (fun (x : Fin (n + 1)) => α) f x = foldrM n f x
theorem
Fin.dfoldr_eq_dfoldrM
{n : Nat}
{α : Fin (n + 1) → Type u_1}
(f : (i : Fin n) → α i.succ → α i.castSucc)
(x : α (last n))
:
dfoldr #
@[simp]
theorem
Fin.dfoldr_zero
{α : Fin (0 + 1) → Type u_1}
(f : (i : Fin 0) → α i.succ → α i.castSucc)
(x : α (last 0))
:
dfoldr 0 α f x = x
theorem
Fin.dfoldr_succ
{n : Nat}
{α : Fin (n + 1 + 1) → Type u_1}
(f : (i : Fin (n + 1)) → α i.succ → α i.castSucc)
(x : α (last (n + 1)))
:
theorem
Fin.dfoldr_succ_last
{n : Nat}
{α : Fin (n + 2) → Type u_1}
(f : (i : Fin (n + 1)) → α i.succ → α i.castSucc)
(x : α (last (n + 1)))
:
theorem
Fin.dfoldr_eq_foldr
{n : Nat}
{α : Type u_1}
(f : Fin n → α → α)
(x : (fun (x : Fin (n + 1)) => α) (last n))
:
dfoldr n (fun (x : Fin (n + 1)) => α) f x = foldr n f x
dfoldlM #
theorem
Fin.dfoldlM_loop_lt
{m : Type u_1 → Type u_2}
{n : Nat}
{α : Fin (n + 1) → Type u_1}
{i : Nat}
[Monad m]
(f : (i : Fin n) → α i.castSucc → m (α i.succ))
(h : i < n)
(x : α ⟨i, ⋯⟩)
:
dfoldlM.loop n α f i ⋯ x = f ⟨i, h⟩ x >>= dfoldlM.loop n α f (i + 1) ⋯
theorem
Fin.dfoldlM_loop_eq
{m : Type u_1 → Type u_2}
{n : Nat}
{α : Fin (n + 1) → Type u_1}
[Monad m]
(f : (i : Fin n) → α i.castSucc → m (α i.succ))
(x : α ⟨n, ⋯⟩)
:
dfoldlM.loop n α f n ⋯ x = pure x
@[simp]
@[irreducible]
theorem
Fin.dfoldlM_loop
{m : Type u_1 → Type u_2}
{n : Nat}
{α : Fin (n + 1 + 1) → Type u_1}
{i : Nat}
[Monad m]
(f : (i : Fin (n + 1)) → α i.castSucc → m (α i.succ))
(h : i < n + 1)
(x : α ⟨i, ⋯⟩)
:
dfoldlM.loop (n + 1) α f i ⋯ x = do
let x ← f ⟨i, h⟩ x
dfoldlM.loop n (α ∘ succ) (fun (x1 : Fin n) (x2 : (α ∘ succ) x1.castSucc) => f x1.succ x2) i h x
theorem
Fin.dfoldlM_eq_foldlM
{m : Type u_1 → Type u_2}
{n : Nat}
{α : Type u_1}
[Monad m]
(f : Fin n → α → m α)
(x : α)
:
dfoldlM n (fun (x : Fin (n + 1)) => α) f x = foldlM n (fun (x : α) (i : Fin n) => f i x) x
dfoldl #
@[simp]
theorem
Fin.dfoldl_zero
{α : Fin (0 + 1) → Type u_1}
(f : (i : Fin 0) → α i.castSucc → α i.succ)
(x : α 0)
:
dfoldl 0 α f x = x
theorem
Fin.dfoldl_succ
{n : Nat}
{α : Fin (n + 1 + 1) → Type u_1}
(f : (i : Fin (n + 1)) → α i.castSucc → α i.succ)
(x : α 0)
:
theorem
Fin.dfoldl_succ_last
{n : Nat}
{α : Fin (n + 1 + 1) → Type u_1}
(f : (i : Fin (n + 1)) → α i.castSucc → α i.succ)
(x : α 0)
:
theorem
Fin.dfoldl_eq_dfoldlM
{n : Nat}
{α : Fin (n + 1) → Type u_1}
(f : (i : Fin n) → α i.castSucc → α i.succ)
(x : α 0)
:
theorem
Fin.dfoldl_eq_foldl
{n : Nat}
{α : Type u_1}
(f : Fin n → α → α)
(x : α)
:
dfoldl n (fun (x : Fin (n + 1)) => α) f x = foldl n (fun (x : α) (i : Fin n) => f i x) x
Fin.fold{l/r}{M} equals List.fold{l/r}{M} #
theorem
Fin.foldl_eq_foldl_finRange
{α : Type u_1}
{n : Nat}
(f : α → Fin n → α)
(x : α)
:
foldl n f x = List.foldl f x (List.finRange n)
theorem
Fin.foldr_eq_foldr_finRange
{n : Nat}
{α : Type u_1}
(f : Fin n → α → α)
(x : α)
:
foldr n f x = List.foldr f x (List.finRange n)