Path Sequences

Stream: mathlib4

[Ian Riley]

I'm working with theorems over path sequences. How would I generalize over a variable length tuple? So I have n : Nat which is the length of the path and I need n-order tuple of Nats. I also then need to define a set of all such sequences.

[Kevin Buzzard]

Can you post a #mwe with e.g. a sorried statement of what you want to do?

[Ian Riley]

Kevin Buzzard said:

Can you post a #mwe with e.g. a sorried statement of what you want to do?

I need to define a $\chi : V \rightarrow C$, where V is a set of vertices and C is a set of colors. Then I need to define $V^*$ which is the set of all finite sequence of vertices and then define $\chi(\pi) = \chi(\pi_0) \ldots \chi(\pi_n)$, where $\pi \in V^*$ and $\pi_i \in V$. I was hoping to define a function that maps a finite tuple of length n to another finite tuple of length n, where the first tuple is a tuple of vertices (which are currently nats) to another finite tuple of colors (which are also currently nats). I'll deal with replacing the nats with vertex and color types after.

[Kevin Buzzard]

A #mwe is Lean code rather than mathematics. Check the link to see exactly what I mean. It's the optimal way to ask a question around here.

[Ian Riley]

Kevin Buzzard said:

A #mwe is Lean code rather than mathematics. Check the link to see exactly what I mean. It's the optimal way to ask a question around here.

I understand. I'm just not sure how to write a variable length tuple in Lean. And I don't know how to define a set. That's why I used LaTeX. If I knew how to do those two things in Lean, I think I might be able to work through the rest. Absent that, I'm not really sure how to post a mwe and likely wouldn't need to if I could do those two things.

[Reid Barton]

It's sort of hard to answer at this level of abstraction. For instance, the type of all finite sequences of elements of $V$ could be represented by List V. There is not necessarily any reason to say "a natural number $n$, plus a tuple of length $n$"--but maybe you have some reason why that is better for you.
Also, I suspect it may be significant that you have written a tuple of length $n+1$, and not length $n$.

[Kyle Miller]

You also say "vertices" -- do you want consecutive vertices to be adjacent with respect to some graph structure?

[Kyle Miller]

docs#simple_graph.walk in mathlib3 is the type of walks between pairs of vertices in simple graphs, and you can use sigma types to get the type of all walks between all pairs of vertices.

[Ian Riley]

Reid Barton said:

It's sort of hard to answer at this level of abstraction. For instance, the type of all finite sequences of elements of $V$ could be represented by List V. There is not necessarily any reason to say "a natural number $n$, plus a tuple of length $n$"--but maybe you have some reason why that is better for you.
Also, I suspect it may be significant that you have written a tuple of length $n+1$, and not length $n$.

I understand what you mean. I'm not trying to be obtuse. I'm just working from a blank slate, so I don't have any other examples to lean on (pun intended). My first thought was actually to use a List and then define a structure that is a List and it's length to define a finite List with a specific length. I didn't think that would be a recommended approach though.

Here might be a mwe of what I was thinking though:

variable (C V : Type)
def VertexSeq := List V
def ColorSeq := List C
def FiniteList {τ : Type} := Nat → List τ
def χ {α β : Type} (n : Nat) := ((FiniteList α) n) → ((FiniteList β) n)

But the last line of that doesn't work and that doesn't seem quite right.

[Ian Riley]

Kyle Miller said:

You also say "vertices" -- do you want consecutive vertices to be adjacent with respect to some graph structure?

They would be. The graph is defined by a transition relation $\Delta := V \times \mathbb{R} \times V$

[Sky Wilshaw]

Your FiniteList type is the type of functions from Nat to List τ. To make the type of lists that have a specific length, you could either use a subtype:

def FiniteList {τ : Type} (n : Nat) := {list : List τ // list.length = n}

or a custom structure:

structure FiniteList {τ : Type} (n : Nat) where
    list : List τ
    length_eq : list.length = n

[Sky Wilshaw]

In particular, the following lines compile:

def FiniteList (τ : Type) (n : Nat) := {list : List τ // list.length = n}
def χ {α β : Type} (n : Nat) := FiniteList α n → FiniteList β n

[Ian Riley]

The custom structure looks really appealing. Would this be considered an idiomatic way to approach a variable-length ordered tuple? I've often seen the notation $\mathbb{N}^n$ to refer to a tuple of length n. In lean, we have $\mathbb{N} \times \mathbb{N}$ to represent a tuple of length 2. Is a list the standard way to represent tuples of larger dimensions in lean?

[Kevin Buzzard]

fin n -> Nat (or it might be Fin n in lean 4) docs4#Fin

[Yury G. Kudryashov]

See docs#vector. Is it ported to Lean 4? Let's see: docs4#Vector. No.

[Yury G. Kudryashov]

There are at least two ways to deal with finite tuples of fixed length: docs#vector and Fin n → α

[Yury G. Kudryashov]

I don't know which type is more convenient for you (and whether you care about computation or not).

[Reid Barton]

And then, there are at least two ways to handle a finite tuple of variable length, either List a, or a pair consisting of n together with a tuple of length n (however you decide to represent that).