FinVec Option to Option FinVec

Stream: new members

[Jesse Slater]

I am using Fin n -> A as my vector type. I want to write a function to convert from FinVec Option A, and I want to convert it into a FinVec A, with a default FinVec if any of the indices are none.

I have working code that does it by converting to a vector using Vector.mOfFn, which gives Option Vector Nat, and then converting back to a function. I was wondering if there was some way I could do it without converting to a Vector.

Here is the MWE which converts to Vector:

import Mathlib.Data.Fin.VecNotation
import Mathlib.Data.Vector.Basic

def f1 : Fin 2 → Option Nat
  | 0 => some 2
  | 1 => none

def f2 : Fin 2 → Option Nat
  | 0 => some 2
  | 1 => some 3

def default : Fin 2 → Nat
  | 0 => 0
  | 1 => 0

def optfn_or_default
  (f : Fin 2 → Option Nat) : Fin 2 → Nat :=
  Vector.mOfFn f
  |>.getD default
  |>.get

#eval optfn_or_default f1

#eval optfn_or_default f2

[Chris Wong]

That function looks a lot like docs#Traversable. I wonder if such an instance is viable in Lean (functions cannot be Traversable in general, as the argument may be infinite, but that doesn't apply to Fin _ -> .).

[Yaël Dillies]

I have a traversable instance for Fin-indexed functions in my computer project from last year. Let me dig it up.

[Chris Wong]

Is it generalizable to Fintype too? :eyes:

[Yaël Dillies]

Actually, it's not quite a Traversable instance that I've got, but pretty sure it's what Jesse wants:

import Mathlib.Data.Vector

namespace Vector

infixr:67 " ::ᵥ " => Vector.cons

/-- Apply a monadic function to each component of a vector, returning a vector inside the monad. -/
def mapM {m} [Monad m] {α} {β : Type _} (f : α → m β) : ∀ {n}, Vector α n → m (Vector β n)
  | 0, _ => pure nil
  | n + 1, xs => do
    let h' ← f xs.head
    let t' ← @mapM m _ _ _ f n xs.tail
    pure (h' ::ᵥ t')

end Vector

import Mathlib.Data.Fin.Basic
import Mathlib.Data.List.Range
import TheFileAbove

/-!
# Enumeration of types
-/

class Enum (α : Type _) where
  enum : List α
  enum_nodup : enum.Nodup
  index : α → Fin enum.length
  enum_index : ∀ a, enum.get (index a) = a

instance {n : ℕ} : Enum (Fin n) :=
{ enum := List.finRange _,
  enum_nodup := List.nodup_finRange _,
  index := λ n ↦ ⟨n, by rw [List.length_finRange]; exact n.2⟩,
  enum_index := λ a ↦ by simp }

instance {α : Type _} {β : α → Type _} [Enum α] [∀ a, ToString (β a)] : ToString (∀ a, β a) :=
⟨λ f ↦ toString $ Enum.enum.map $ λ a ↦ toString $ f a⟩

instance [Enum α] [Nonempty α] : NeZero (Enum.enum : List α).length :=
⟨λ h ↦ by
  haveI := ‹Nonempty α›.map Enum.index
  rw [h] at this
  exact not_isEmpty_of_nonempty (Fin 0) (inferInstance : IsEmpty (Fin 0))⟩

namespace Monad
universe u v
variable {α : Type u} {β : Type (max u v)} {m : Type (max u v) → Type _}

-- TODO: Generalise to dependent types
/-- Return a random function from random results for each input. -/
def pi [Enum α] [Monad m] (r : α → m β) : m (α → β) :=
(λ l a ↦ l.toList.get ⟨Enum.index a, by simp⟩) <$> Vector.mapM r ⟨Enum.enum, rfl⟩

end Monad

[Eric Wieser]

I think I have a PR with PiFin.mapM

[Eric Wieser]

docs3#pi_fin.mmap