Dependent vector

Stream: Is there code for X?

[Martin Dvořák]

Do we have dependent vectors, that is, an explicit vector whose entries' types may depend on their index?
I want a list of length k where (β : Fin k → Type) specifies types of respective elements.

[Eric Wieser]

(β : Fin k → Type) (v : (i : Fin k) → β i)?

[Eric Wieser]

That's the type that docs#Fin.cons operates on

[Martin Dvořák]

Mathlib doesn't have a bundled version, does it?

[Richard Copley]

(i : Fin k) → β i is a.k.a. ∀ (i : Fin k), β i, or Π (i : Fin k), β i (with import Mathlib.Util.PiNotation).

[Richard Copley]

A structure might be more convenient, depending.

[Eric Wieser]

What would bundling mean here?

[Eric Wieser]

Are you trying to bundle β with v?

[Martin Dvořák]

Heh, not much. I just want to know whether somebody implemented it with API so I don't reïnvent the wheel.

[Martin Dvořák]

Eric Wieser said:

Are you trying to bundle β with v?

Basically a generic type that given {k : ℕ} (β : Vector Type k) allows me to write DepVec β or something like that.

[Eric Wieser]

You've given two different types for \beta now; do you have a preference between them?

[Martin Dvořák]

I don't care. However, if there exists API for one version, I'll pick that.

[Eric Wieser]

Eric Wieser said:

That's the type that docs#Fin.cons operates on

This API exists

[Martin Dvořák]

Ah thanks!

[Notification Bot]

Martin Dvořák has marked this topic as resolved.

[Eric Wieser]

If you wanted you could write def DepVec (β : Fin k → Type) := (i : _) → β i but it's not going to save you any typing over using Π i, β i or ∀ i, β i directly

[Notification Bot]

Martin Dvořák has marked this topic as unresolved.

[Martin Dvořák]

I am puzzled. Why does the following declaration work?

import Mathlib.Util.PiNotation
import Mathlib.Data.Fin.Tuple.Basic

def Co (α : Type) {k : ℕ} (β : Fin k → Type) : Type :=
  Π i, List ((Fin.cons α β : Fin k.succ → Type) i)

But, without type annotation, it doesn't?

import Mathlib.Util.PiNotation
import Mathlib.Data.Fin.Tuple.Basic

def Co (α : Type) {k : ℕ} (β : Fin k → Type) : Type :=
  Π i, List ((Fin.cons α β) i)

The following declaration doesn't work either. Why?

import Mathlib.Util.PiNotation
import Mathlib.Data.Fin.Tuple.Basic

def Co (α : Type) {k : ℕ} (β : Fin k → Type) : Type :=
  Π (i : Fin k.succ), List ((Fin.cons α β) i)

[Eric Wieser]

Does a :) annotation work?

[Martin Dvořák]

No.

[Kyle Miller]

It looks like it's not able to solve for the implicit argument to Fin.cons by unification? This works:

def Co (α : Type) {k : ℕ} (β : Fin k → Type) : Type :=
  Π i, List (Fin.cons (α := fun _ => Type) α β i)

[Martin Dvořák]

How can I construct a term of the type in question?

This works:

import Mathlib.Data.Fin.VecNotation
import Mathlib.Util.PiNotation

example : Π (i : Fin 2), ℕ := Matrix.vecCons 3 (Matrix.vecCons 5 Matrix.vecEmpty)

This doesn't work:

example : Π (i : Fin 2), ![ℕ, ℕ] i := Matrix.vecCons 3 (Matrix.vecCons 5 Matrix.vecEmpty)

This works:

example : Π (i : Fin 2), ℕ := Fin.cons 3 (Fin.cons 5 Fin.elim0)

This doesn't work:

example : Π (i : Fin 2), ![ℕ, ℕ] i := Fin.cons 3 (Fin.cons 5 Fin.elim0)

[Martin Dvořák]

I first thought I was missing the ![3, 5] notation for dependent vectors, but then I realized I didn't even know how to make the term by writing it explicitly.

[Floris van Doorn]

If at all possible, I would recommend against putting types in the ![_, _] notation.

[Martin Dvořák]

Notation aside, what constructors can I use?

[Martin Dvořák]

example : Π (i : Fin 2), (fun j => if j = 0 then ℕ else ℕ) i :=
  sorry -- I was to represent ![3, 5] here

[Floris van Doorn]

#xy
What are you really trying to do here? Is it important that it's a pi-type on Fin n? Fin n doesn't compute very well, i.e. a lemma like docs#Fin.succRecOn_succ is not true by rfl. This is often problematic for types, because if two types are not definitionally equal but only propositionally equal, you have to write casts between them.

[Floris van Doorn]

docs#List.TProd might be what you want though: if you have a list of explicit types, you take their product. docs#List.TProd.mk constructs elements.

[Floris van Doorn]

(this is used in measure theory to iterate the binary product of measures to the finitary product of measures)

[Martin Dvořák]

Floris van Doorn said:

#xy
What are you really trying to do here? Is it important that it's a pi-type on Fin n? Fin n doesn't compute very well, i.e. a lemma like docs#Fin.succRecOn_succ is not true by rfl. This is often problematic for types, because if two types are not definitionally equal but only propositionally equal, you have to write casts between them.

For illustration, imagine that I want to define a multi-tape Turing machine with a different alphabet on each tape. I don't really need to index the tapes by Fin n but it seemed like the most natural choice.

[Martin Dvořák]

Floris van Doorn said:

docs#List.TProd might be what you want though: if you have a list of explicit types, you take their product. docs#List.TProd.mk constructs elements.

TProd seems like overkill, but it definitely should work.

[Floris van Doorn]

In that case I would use a (finite) indexing type ι of tapes, not force the usage of Fin n.

[Martin Dvořák]

Is it an antipattern?

def MyPi (τ : List Type) : Type := List.TProd id τ

[Martin Dvořák]

Yes, it is an antipattern. Citing documentation:
"This type should not be used if ∀ i, α i or ∀ i ∈ l, α i can be used instead (in the last expression, we could also replace the list l by a set or a finset)."

[Martin Dvořák]

I have no idea how to construct terms of the type ∀ i ∈ l, α i unfortunately.

[Floris van Doorn]

fun x hx => ...

[Martin Dvořák]

Unfortunately, I struggle with the ... part.

[Martin Dvořák]

I thought the following would work...

import Mathlib.Data.Prod.TProd

def Pls (k : ℕ) (τ : ℕ → Type) : Type := List.TProd τ (List.range k)

def Tau (i : ℕ) : Type := if i = 0 then Char else Int

#reduce Pls 2 Tau -- gives `Char × Int × PUnit`

example : Char × Int × PUnit := ('A', 9, ()) -- works

example : Pls 2 Tau := ('A', 9, ()) -- fails `failed to synthesize instance OfNat (Tau 1) 9`

Any idea how to make it work?

[Eric Rodriguez]

you could probably do show ... from X but I think this is kind of on purpose

[Eric Rodriguez]

Pls is a type synonym in this case, and unless you make it reducible it shouldn't pass through

[Eric Rodriguez]

oh, show ... from is now a let binding instead of just a strong Id...

[Martin Dvořák]

Eric Rodriguez said:

Pls is a type synonym in this case, and unless you make it reducible it shouldn't pass through

If I write

@[reducible]
def Pls (k : ℕ) (τ : ℕ → Type) : Type := List.TProd τ (List.range k)

nothing changes.

[Martin Dvořák]

This works but looks absolutely horrible:

import Mathlib.Data.Prod.TProd

def Pls (k : ℕ) (τ : ℕ → Type) : Type := List.TProd τ (List.range k)

def Tau (i : ℕ) : Type := if i = 0 then Char else Int

def exampl : Pls 2 Tau := List.TProd.mk (List.range 2) fun
  | .zero => 'A'
  | .succ n => by
    simp [Tau]
    exact 9

#eval exampl -- gives `('A', 9, ())`

[Eric Rodriguez]

you can write := ('A', 9, () : Char \x Int \x PUnit)

[Martin Dvořák]

Indeed!

import Mathlib.Data.Prod.TProd

def Pls (k : ℕ) (τ : ℕ → Type) : Type := List.TProd τ (List.range k)

def Tau (i : ℕ) : Type := if i = 0 then Char else Int

example : Pls 2 Tau := (('A', 9, ()) : Char × Int × PUnit)

It works but I don't know why.

[Yaël Dillies]

because of the way docs#List.TProd is defined?

[Yaël Dillies]

Do

example : Pls 2 Tau = Char × Int × PUnit := rfl

[Martin Dvořák]

If you mean example : Pls 2 Tau = (Char × Int × PUnit) := rfl then it succeeds, yes.
I still don't know why example : Pls 2 Tau := ('A', 9, ()) fails.

[Eric Rodriguez]

The issue here is that Lean doesn't dig any deeper than Tau 1 before trying to find an instance of OfNat

[Eric Rodriguez]

Whether this is a bug or not, I'm not sure

[Eric Rodriguez]

I assume not, maybe you're expected to use deriving ...

[Eric Rodriguez]

Even inlining fails, wanting OfNat ((fun i ↦ if i = 0 then Char else ℤ) 1) 9. I would think that is definitely a bug, but not sure what level of reduciblity it would be expected to work until.

[Martin Dvořák]

In case it is a bug (I honestly don't know), should I make a bug report to Mathlib4 or to Lean4 directly?

[Eric Rodriguez]

Lean4, I think

[Mario Carneiro]

it's not a bug, the type of the second field is Tau 1 and Tau is not reducible

[Mario Carneiro]

You can use example : Pls 2 Tau := ('A', (9:Int), ())

[Mario Carneiro]

you can also make Tau reducible if you only use reducible parts in the definition:

@[reducible] def Tau (i : ℕ) : Type := match i with | 0 => Char | _ => Int

example : Pls 2 Tau := ('A', 9, ())

[Mario Carneiro]

dite is not reducible

[Martin Dvořák]

Mario Carneiro said:

You can use example : Pls 2 Tau := ('A', (9:Int), ())

Indeed!

import Mathlib.Data.Prod.TProd

@[reducible]
def Pls (k : ℕ) (τ : ℕ → Type) : Type := List.TProd τ (List.range k)

@[reducible]
def Tau (i : ℕ) : Type := if i = 0 then Char else Int

example : Pls 2 Tau := ('A', (9 : Int), ()) -- ok

example : Pls 2 Tau := ('A', 9, ()) -- fails

@[reducible]
def Bau (i : ℕ) : Type := if i = 0 then Int else Char

example : Pls 2 Bau := ((9 : Int), 'A', ()) -- ok

example : Pls 2 Bau := (9, 'A', ()) -- fails

Removing those @[reducible] doesn't change anything here.

[Martin Dvořák]

Mario Carneiro said:

you can also make Tau reducible if you only use reducible parts in the definition:

@[reducible] def Tau (i : ℕ) : Type := match i with | 0 => Char | _ => Int

example : Pls 2 Tau := ('A', 9, ())

If I have five types, do I have to do a cascade of four matchings on Nat?

[Martin Dvořák]

(deleted)

[Martin Dvořák]

I don't have to!

import Mathlib.Data.Prod.TProd

def Pls (k : ℕ) (τ : ℕ → Type) : Type := List.TProd τ (List.range k)

@[reducible]
def Tau : ℕ → Type
| 0 => Int
| 1 => Char
| 2 => Rat
| 3 => Bool
| _ => String

example : Pls 5 Tau := (9, 'A', 0.5, false, "hello", ()) -- ok

[Mario Carneiro]

If you have five types, why aren't you just writing Int × Char × Rat × Bool × String instead of this thing?

[Martin Dvořák]

Well, I have a general number of types, and in some instances, it might be instantiated by a 5-tuple.

[Martin Dvořák]

Does docs#List.TProd support something like docs#Function.update or a similar function that overwrites a single entry?

[Martin Dvořák]

I actually want to change the first entry, so something like (new_head :: TProd.tail old_term) : TProd would be perfect.

[Martin Dvořák]

Can you make the following into terms?

import Mathlib.Data.Prod.TProd

def List.TProd.tail {ι : Type} {α : ι → Type} {d : ι} {l : List ι}
    (x : (d::l).TProd α) : l.TProd α := by
  rw [List.TProd, List.foldr, ←List.TProd] at x
  exact x.snd

def List.TProd.replaceHead {ι : Type} {α : ι → Type} {d : ι} {l : List ι}
    (x : (d::l).TProd α) (v : α d) : (d::l).TProd α := by
  rw [List.TProd, List.foldr, ←List.TProd]
  exact ⟨v, x.tail⟩

[Damiano Testa]

What is below seems to work. Did you have something else in mind?

def List.TProd.tail {ι : Type} {α : ι → Type} {d : ι} {l : List ι}
    (x : (d::l).TProd α) : l.TProd α := x.snd

def List.TProd.replaceHead {ι : Type} {α : ι → Type} {d : ι} {l : List ι}
    (x : (d::l).TProd α) (v : α d) : (d::l).TProd α := ⟨v, x.tail⟩

[Martin Dvořák]

Thank you!!!
I can't believe I didn't see that an option.

[Damiano Testa]

The rw were simply doing/undoing definitions, so they are "transparent" to defeq.