How do I represent a graph?

Stream: new members

[Huỳnh Trần Khanh]

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

[Huỳnh Trần Khanh]

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]

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]

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]

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]

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]

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]

I think people aren't subscribed by default to it

[Kevin Buzzard]

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

[Kevin Buzzard]

docs#simple_graph ?

[Kevin Buzzard]

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]

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]

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]

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 :=
(adj_lists : list (list ℕ))
(has_verts : ∀ (adj_list ∈ adj_lists) (n ∈ adj_list), n < adj_lists.length)

[Bryan Gin-ge Chen]

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

[Kyle Miller]

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]

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]

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]

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]

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]

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

[Alena Gusakov]

Ah I see

[Alena Gusakov]

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]

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

[Alena Gusakov]

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

[Yakov Pechersky]

You might even say

(h : Mᵀ = M . dec_trivial)

[Yakov Pechersky]

If there's the proper decidable instance in place.