Stream: new members

Topic: How do I represent a graph?

Huỳnh Trần Khanh (Feb 10 2021 at 09:07):

A tree sounds like something inductive so I think that'd be easy to represent. How about a graph?

Huỳnh Trần Khanh (Feb 10 2021 at 09:08):

In competitive programming I'd represent a graph using an array of arrays where graph[vertex] is the list of nodes adjacent to that vertex.

Kevin Buzzard (Feb 10 2021 at 09:09):

There are 5 ways to represent a graph at least. You could use the version in mathlib but that might not be designed for performance issues but rather for reasoning. Another issue is that there are five different things which people mean when they say the word graph

Kevin Buzzard (Feb 10 2021 at 09:11):

As a mathematician I am mostly interested in reasoning about objects so I don't care about the internal implementation, all I need is an interface which is good enough for me to make whatever API I need. With your background I suspect that implementation issues might be more important to you, but then of course the implementation you go for will depend on exactly which operations you want to be quick

Kevin Buzzard (Feb 10 2021 at 09:13):

In short there are multiple answers to your question and the best one for you will depend on your use case

Huỳnh Trần Khanh (Feb 10 2021 at 09:15):

Hmm I want something that's easy to reason about, I don't really care about performance for now. But I just did a quick search on the mathlib page and I only saw moving octopuses :joy:

Kevin Buzzard (Feb 10 2021 at 09:17):

I've not been following the graph theory stuff, but there is an entire stream about it which you might not know about -- #graph theory

Kevin Buzzard (Feb 10 2021 at 09:17):

I think people aren't subscribed by default to it

Kevin Buzzard (Feb 10 2021 at 09:18):

I had assumed we'd got the definition by now!

Kevin Buzzard (Feb 10 2021 at 09:20):

Of course you might have another notion of graph in mind, the word is used to mean several related but different things in the mathematical literature

Huỳnh Trần Khanh (Feb 10 2021 at 09:25):

This is the notion of graph I had in mind https://csacademy.com/app/graph_editor/ and yeah, it looks like docs#simple_graph is the thing I'm looking for. The docs looks really intimidating though.

Kyle Miller (Feb 10 2021 at 19:18):

The simple_graph type is pretty much representing a simple graph as an adjacency matrix. If G : simple_graph V, then V is the vertex type and G.adj v w represents that v is adjacent to w. It doesn't support multiple edges or loops of course. If you want the finite set of vertices adjacent to a vertex, there's G.neighbor_finset v.

Kyle Miller (Feb 10 2021 at 19:19):

I just quickly wrote this, but if you want the array of arrays representation (well, linked list of linked lists) then you could try something like this:

structure graph :=


Bryan Gin-ge Chen (Feb 10 2021 at 19:20):

I suppose eventually we will have a simple_graph constructor that takes in an adjacency matrix as a matrix.

Kyle Miller (Feb 10 2021 at 19:25):

Here's another possible definition for a (locally finite) graph:

import data.finset

structure graph (V : Type*) :=
(adj_set : V → finset V)


What finset does, essentially, is to force your algorithm to not care about the ordering of an adjacency list. That might be difficult to write algorithms for, but if V is orderable then sort from data.finset.sort can give you a list of the adjacent vertices.

Kyle Miller (Feb 10 2021 at 19:29):

You could also work with graphs with ordered adjacency lists:

structure graph' (V : Type*) :=
(adj_list : V → list V)


There's a function graph' V -> graph V by sending each adjacency list to an adjacency finset. Maybe if you write algorithms for graph', you could then prove the algorithm descends to graph.

Kyle Miller (Feb 10 2021 at 19:34):

These three types I gave are all for some version of directed multigraphs, by the way. It would be up to you to add a condition for having edges going in both directions. For example, you might do

structure graph (V : Type*) :=
(adj_list : V → list V)
(symm : ∀ v (w ∈ adj_list v), v ∈ adj_list w)


Alena Gusakov (Feb 10 2021 at 20:34):

I suppose eventually we will have a simple_graph constructor that takes in an adjacency matrix as a matrix.

Could you not just use from_rel? I'm gonna try that

Bryan Gin-ge Chen (Feb 10 2021 at 20:36):

Oh, I meant giving Lean an actual matrix like:

import data.matrix.notation
-- adjacency matrix of a triangle
#check ![![0,1,1], ![1,0,1], ![1,1,0]]


Bryan Gin-ge Chen (Feb 10 2021 at 20:37):

Maybe what I'm describing should be a tactic or something? Not sure...

Ah I see

Alena Gusakov (Feb 10 2021 at 20:53):

Wait so like

def graph_from_matrix (M : matrix α α R) (h : Mᵀ = M) : simple_graph α :=
{ adj := λ v w, M v w = 1 ∧ v ≠ w,
sym := λ v w h2, by { rw [← transpose_apply M, h], exact ⟨h2.1, ne.symm h2.2⟩ },
loopless := λ v h, h.2 rfl }


Bryan Gin-ge Chen (Feb 10 2021 at 20:57):

Yep, exactly. This could make it easier to define / specify certain explicit graphs.

Alena Gusakov (Feb 10 2021 at 20:59):

Yeah I think it would be super useful for digraphs/multigraphs especially

Yakov Pechersky (Feb 10 2021 at 21:51):

You might even say

(h : Mᵀ = M . dec_trivial)


Yakov Pechersky (Feb 10 2021 at 21:52):

If there's the proper decidable instance in place.

Last updated: May 13 2021 at 22:15 UTC