Dependent vector (tuple) notation

Stream: Is there code for X?

[Niklas Halonen]

Hi! I recently wanted to show the following equivalence using the vector notation for Fin d → α i.e. ![a, b, ...]:

import Mathlib.Tactic

def finTwoPiEquiv {α β : Type u} : ((i : Fin 2) → match i with | 0 => α | 1 => β) ≃ α × β where
  toFun := fun f => ⟨f 0, f 1⟩
  invFun := fun ⟨a, b⟩ => ![a, b]

However the above didn't type check because the vector notation doesn't support heterogeneous types, even though the underlying Fin code does support it. Do we have a notation for defining these dependent tuples and their types (my requirement is that it works without × and uses Fin d → ... instead)?

I'm sure it must exist but can't find it anywhere. In the meantime I just copied VecNotation.lean and made it dependent myself introducing a !(a, b, ...) notation:

import Mathlib.Tactic

/-- `!()` is the dependent vector with no entries. -/
def vecEmpty {α : Fin 0 → Type*} (i : Fin 0) : α i := i.elim0

/-- `vecCons h t` prepends an entry `h` to a dependent vector `t`.

The inverse functions are `vecHead` and `vecTail`.
The notation `!(a, b, ...)` expands to `vecCons a (vecCons b ...)`.
-/
def vecCons {n : ℕ} {α : Fin n.succ → Type*} (h : α 0) (t : (i : Fin n) → α i.succ) (i : Fin n.succ) : α i :=
  Fin.cons h t i

syntax (name := dvecNotation) "!(" term,* ")" : term

macro_rules
  | `(!($term:term, $terms:term,*)) => `(vecCons $term !($terms,*))
  | `(!($term:term)) => `(vecCons $term !())
  | `(!()) => `(vecEmpty)

@[app_unexpander vecCons]
def vecConsUnexpander : Lean.PrettyPrinter.Unexpander
  | `($_ $term !($term2, $terms,*)) => `(!($term, $term2, $terms,*))
  | `($_ $term !($term2)) => `(!($term, $term2))
  | `($_ $term !()) => `(!($term))
  | _ => throw ()

@[app_unexpander vecEmpty]
def vecEmptyUnexpander : Lean.PrettyPrinter.Unexpander
  | `($_:ident) => `(!())
  | _ => throw ()

variable {n : ℕ} {α : Fin (n + 1) → Type*} (v : (i : Fin n.succ) → α i) (x : α 0)

/-- `vecHead v` gives the first entry of the vector `v` -/
def vecHead : α 0 :=
  v 0

/-- `vecTail v` gives a vector consisting of all entries of `v` except the first -/
def vecTail (i : Fin n) : α i.succ :=
  v (i.succ)

#check !(1) -- not a complete type
#check !(1, 2, 3) -- not a complete type
#check (!((1 : ℕ), "a", [2]) : (i : Fin 3) → ![ℕ, String, List ℕ] i)

section Val

-- @[simp]
-- theorem head_fin_const (a : α) : (vecHead fun _ : Fin (n + 1) => a) = a :=
  -- rfl

variable {n : ℕ} {α : Fin (n + 1) → Type*} (v : (i : Fin n.succ) → α i) (x : α 0)
  (u : (i : Fin n) → α i.succ)

@[simp]
theorem cons_val_zero : vecCons x u 0 = x :=
  rfl

-- theorem cons_val_zero' (h : 0 < m.succ) (x : α) (u : Fin m → α) : vecCons x u ⟨0, h⟩ = x :=
  -- rfl

@[simp]
theorem cons_val_succ (i : Fin n) : vecCons x u i.succ = u i := by
  simp [vecCons]

-- @[simp]
-- theorem cons_val_succ' {i : ℕ} (h : i.succ < m.succ) (x : α) (u : Fin m → α) :
--     vecCons x u ⟨i.succ, h⟩ = u ⟨i, Nat.lt_of_succ_lt_succ h⟩ := by
--   simp only [vecCons, Fin.cons, Fin.cases_succ']

@[simp]
theorem head_cons : vecHead (vecCons x u) = x :=
  rfl

@[simp]
theorem tail_cons : vecTail (vecCons x u) = u := by
  ext
  simp [vecTail]

-- @[simp]
-- theorem empty_val' {n' : Type*} (j : n') : (fun i => (![] : Fin 0 → n' → α) i j) = ![] :=
  -- empty_eq _

@[simp]
theorem cons_head_tail : vecCons (vecHead v) (vecTail v) = v :=
  Fin.cons_self_tail _

-- [Skipped some stuff]

def vecAppend {α : Fin m → Type u} {β : Fin n → Type u} (u : (i : Fin m) → α i)
  (v : (i : Fin n) → β i) : (i : Fin (m + n)) → Fin.append α β i :=
  Fin.addCases
    (fun i => Fin.append_left α β i ▸ u i)
    (fun i => Fin.append_right α β i ▸ v i)

lemma Fin.eq_natAdd_sub (i : Fin (m + n)) (h : m ≤ i) : i = Fin.natAdd m ⟨(i : ℕ) - m, by omega⟩ := by
  simp [h]

theorem vecAppend_eq_ite {α : Fin m → Type u} {β : Fin n → Type u}
  (u : (i : Fin m) → α i) (v : (i : Fin n) → β i) :
    vecAppend u v = fun i : Fin (m + n) =>
      if h : (i : ℕ) < m then Fin.append_left α β ⟨i, h⟩ ▸ u ⟨i, h⟩
      else
        -- Need to chain these two equalities
        -- Fin.append α β i  =  Fin.append α β (Fin.natAdd m ⟨↑i - m, ⋯⟩)  =  β ⟨↑i - m, ⋯⟩
        (congrArg _ (Fin.eq_natAdd_sub i (not_lt.mp h))).trans
        (Fin.append_right α β ⟨(i : ℕ) - m, by omega⟩) ▸
          (v ⟨(i : ℕ) - m, by omega⟩) := by
  ext i
  simp [vecAppend, Fin.addCases]
  -- rw [vecAppend, Fin.addCases, Function.comp_apply, Fin.addCases]
  congr with hi
  simp [Fin.subNat]
  -- Don't know how to proceed
  -- rfl
  sorry

end Val



def finTwoPiEquiv {α β : Type u} : ((i : Fin 2) → match i with | 0 => α | 1 => β) ≃ α × β where
  toFun := fun f => ⟨f 0, f 1⟩
  invFun := fun ⟨a, b⟩ => !(a, b) -- Dependent VecNotation!
  -- invFun := Function.uncurry (!(., .)) also works
  left_inv := by
    intro f
    simp
    -- The goal is pretty printed as ⊢ !(f 0, f 1) = f
    ext i
    fin_cases i <;> rfl
  right_inv := by
    tauto

Now my original equivalence can be proved as above.

This still has a bit of a problem with instance synthesis, for example to define the Repr instance for ((i : Fin n) → α i):

instance {h : ∀ i, Repr (α i)} : Repr ((i : Fin n) → α i) where ...

it requires synthesis of Repr instances for arbitrarily (but finitely) many α is, but don't know if that exists in Lean or not.