Folding over Fin

This file defines the prime versions of Fin.(d)fold{l/r} which has better definitional equalities (i.e. automatically unfold for 0 and for n.succ). We then show equivalences between the prime and non-prime versions, so that when compiling, the non-prime versions (which are more efficient) are used.

We also prove that the existing mathlib function finSumFinEquiv : ∑ i, Fin (n i) ≃ Fin (∑ i, n i) is equivalent to a version defined via Fin.dfoldl'.

def Fin.dfoldlM' {m : Type u → Type v} [Monad m] (n : ℕ) (α : Fin (n + 1) → Type u) (f : (i : Fin n) → α i.castSucc → m (α i.succ)) (init : α 0) : m (α (last n))

Heterogeneous left fold over Fin n in a monad, prime version with better defeq. Automatically unfolds for 0 and n.succ.

@[simp]

theorem Fin.dfoldlM'_zero {m : Type u → Type v} [Monad m] {α : Fin 1 → Type u} (f : (i : Fin 0) → α i.castSucc → m (α i.succ)) (x : α 0) : dfoldlM' 0 α f x = pure x

@[simp]

theorem Fin.dfoldlM'_succ {m : Type u → Type v} [Monad m] {n : ℕ} {α : Fin (n + 2) → Type u} (f : (i : Fin (n + 1)) → α i.castSucc → m (α i.succ)) (x : α 0) : dfoldlM' (n + 1) α f x = do let y ← dfoldlM' n (α ∘ castSucc) (fun (i : Fin n) => f i.castSucc) x f (last n) y

def Fin.dfoldl' (n : ℕ) (α : Fin (n + 1) → Type u) (f : (i : Fin n) → α i.castSucc → α i.succ) (init : α 0) : α (last n)

Heterogeneous left fold over Fin n, prime version with better defeq. Automatically unfolds for 0 and n.succ.

@[simp]

theorem Fin.dfoldl'_zero {α : Fin 1 → Type u} (f : (i : Fin 0) → α i.castSucc → α i.succ) (x : α 0) : dfoldl' 0 α f x = x

@[simp]

theorem Fin.dfoldl'_succ_last {n : ℕ} {α : Fin (n + 2) → Type u} (f : (i : Fin (n + 1)) → α i.castSucc → α i.succ) (x : α 0) : dfoldl' (n + 1) α f x = f (last n) (dfoldl' n (α ∘ castSucc) (fun (i : Fin n) => f i.castSucc) x)

@[csimp]

theorem Fin.dfoldl_eq_dfoldl' : dfoldl = dfoldl'

Compiler replacement rule: use dfoldl' instead of dfoldl for better defeq.

def Fin.foldl' {α : Type u} (n : ℕ) (f : Fin n → α → α) (init : α) : α

Left fold over Fin n, prime version with better defeq. Automatically unfolds for 0 and n.succ.

@[simp]

theorem Fin.foldl'_zero {α : Type u} (f : Fin 0 → α → α) (x : α) : foldl' 0 f x = x

@[simp]

theorem Fin.foldl'_succ {n : ℕ} {α : Type u} (f : Fin (n + 1) → α → α) (x : α) : foldl' (n + 1) f x = f (last n) (foldl' n (fun (i : Fin n) => f i.castSucc) x)

def Fin.dfoldrM' {m : Type u → Type v} [Monad m] (n : ℕ) (α : Fin (n + 1) → Type u) (f : (i : Fin n) → α i.succ → m (α i.castSucc)) (init : α (last n)) : m (α 0)

Heterogeneous right fold over Fin n in a monad, prime version with better defeq. Automatically unfolds for 0 and n.succ.

@[simp]

theorem Fin.dfoldrM'_zero {m : Type u → Type v} [Monad m] {α : Fin 1 → Type u} (f : (i : Fin 0) → α i.succ → m (α i.castSucc)) (x : α (last 0)) : dfoldrM' 0 α f x = pure x

@[simp]

theorem Fin.dfoldrM'_succ {m : Type u → Type v} [Monad m] {n : ℕ} {α : Fin (n + 1 + 1) → Type u} (f : (i : Fin (n + 1)) → α i.succ → m (α i.castSucc)) (x : α (last (n + 1))) : dfoldrM' (n + 1) α f x = do let y ← dfoldrM' n (α ∘ succ) (fun (i : Fin n) => f i.succ) x f 0 y

def Fin.dfoldr' (n : ℕ) (α : Fin (n + 1) → Type u) (f : (i : Fin n) → α i.succ → α i.castSucc) (init : α (last n)) : α 0

Heterogeneous right fold over Fin n, prime version with better defeq. Automatically unfolds for 0 and n.succ.

@[simp]

theorem Fin.dfoldr'_zero {α : Fin 1 → Type u} (f : (i : Fin 0) → α i.succ → α i.castSucc) (x : α (last 0)) : dfoldr' 0 α f x = x

@[simp]

theorem Fin.dfoldr'_succ {n : ℕ} {α : Fin (n + 1 + 1) → Type u} (f : (i : Fin (n + 1)) → α i.succ → α i.castSucc) (x : α (last (n + 1))) : dfoldr' (n + 1) α f x = f 0 (dfoldr' n (α ∘ succ) (fun (i : Fin n) => f i.succ) x)

@[csimp]

theorem Fin.dfoldr_eq_dfoldr' : dfoldr = dfoldr'

Compiler replacement rule: use dfoldr' instead of dfoldr for better defeq.

def Fin.foldr' {α : Type u} (n : ℕ) (f : Fin n → α → α) (init : α) : α

Right fold over Fin n, prime version with better defeq. Automatically unfolds for 0 and n.succ.

@[simp]

theorem Fin.foldr'_zero {α : Type u} (f : Fin 0 → α → α) (x : α) : foldr' 0 f x = x

@[simp]

theorem Fin.foldr'_succ {n : ℕ} {α : Type u} (f : Fin (n + 1) → α → α) (x : α) : foldr' (n + 1) f x = f 0 (foldr' n (f ∘ succ) x)

def Fin.IterType (n : ℕ) : Type

def Fin.PowerType (n : ℕ) : Type

def Fin.NestedList (n : ℕ) : Type

theorem Fin.dfoldl_congr {n : ℕ} {α α' : Fin (n + 1) → Type u} {f : (i : Fin n) → α i.castSucc → α i.succ} {f' : (i : Fin n) → α' i.castSucc → α' i.succ} {init : α 0} {init' : α' 0} (hα : ∀ (i : Fin (n + 1)), α i = α' i) (hf : ∀ (i : Fin n) (a : α i.castSucc), f i a = cast ⋯ (f' i (cast ⋯ a))) (hinit : init = cast ⋯ init') : dfoldl n α f init = cast ⋯ (dfoldl n α' f' init')

Congruence for dfoldl

theorem Fin.dfoldl_congr_dcast {n : ℕ} {ι : Type v} {α α' : Fin (n + 1) → ι} {β : ι → Type u} [DCast ι β] {f : (i : Fin n) → β (α i.castSucc) → β (α i.succ)} {f' : (i : Fin n) → β (α' i.castSucc) → β (α' i.succ)} {init : β (α 0)} {init' : β (α' 0)} (hα : ∀ (i : Fin (n + 1)), α i = α' i) (hf : ∀ (i : Fin n) (a : β (α i.castSucc)), f i a = dcast ⋯ (f' i (dcast ⋯ a))) (hinit : init = dcast ⋯ init') : dfoldl n (fun (i : Fin (n + 1)) => β (α i)) f init = cast ⋯ (dfoldl n (fun (i : Fin (n + 1)) => β (α' i)) f' init')

Congruence for dfoldl whose type vectors are indexed by ι and have a DCast instance

Note that we put cast (instead of dcast) in the theorem statement for easier matching, but dcast inside the hypotheses for downstream proving.

theorem Fin.dfoldl_dcast {ι : Type v} {β : ι → Type u} [DCast ι β] {n : ℕ} {α α' : Fin (n + 1) → ι} {f : (i : Fin n) → β (α i.castSucc) → β (α i.succ)} {init : β (α 0)} (hα : ∀ (i : Fin (n + 1)), α i = α' i) : dcast ⋯ (dfoldl n (fun (i : Fin (n + 1)) => β (α i)) f init) = dfoldl n (fun (i : Fin (n + 1)) => β (α' i)) (fun (i : Fin n) (a : (fun (i : Fin (n + 1)) => β (α' i)) i.castSucc) => dcast ⋯ (f i (dcast ⋯ a))) (dcast ⋯ init)

Distribute dcast inside dfoldl. Requires the minimal condition of α = α'