# Zulip Chat Archive

## Stream: graph theory

### Topic: graph defs

#### Aaron Anderson (Aug 12 2020 at 04:25):

I think a lot of what we've done in #3458 is good, but looking at @Bhavik Mehta's definitions, I'm pretty sure that we should refactor the references to `sym2`

to use `powerset_len 2`

instead. https://github.com/b-mehta/combinatorics/blob/graphs/src/handshaking.lean

#### Aaron Anderson (Aug 12 2020 at 04:27):

There are already plenty of counting results proven about `powerset_len`

, and in general, if we want to count finite things, it's better IMO to use something as ingrained in the `finset`

library as possible.

#### Kyle Miller (Aug 12 2020 at 23:09):

There are some special properties about `sym2`

(i.e., unordered pairs) that other powerset lengths don't have, which is why we thought it was worth having when we added it. There is at least an equivalence to multigraphs of length 2 in the `sym2`

library. So, from another point of view, this means `sym2`

should be better developed to have all the features of `powerset_len 2`

.

#### Bhavik Mehta (Aug 12 2020 at 23:11):

Isn't `sym2`

just type-equivalent to `powerset_len 2`

? I used powerset_len in particular because I had in mind the generalisation to hypergraphs rather than multigraphs

#### Aaron Anderson (Aug 12 2020 at 23:27):

They are not type-equivalent, because `sym2`

includes the diagonal.

#### Aaron Anderson (Aug 12 2020 at 23:28):

Graphs with loops need `sym2`

, loopless graphs do not

#### Aaron Anderson (Aug 12 2020 at 23:30):

Also, it'd be very hard to develop `sym2`

to have all the features of `powerset_len 2`

, because `powerset_len 2`

is a subtype (actually a subset!) of `finset`

, which has a colossal amount of API available

#### Aaron Anderson (Aug 12 2020 at 23:31):

I also like the generalization to hypergraphs

#### Bhavik Mehta (Aug 12 2020 at 23:33):

Aaron Anderson said:

They are not type-equivalent, because

`sym2`

includes the diagonal.

ah of course, makes sense

#### Aaron Anderson (Aug 12 2020 at 23:34):

I think that a good model may be to have no data at all about the edge type E except for a function from E to `finset V`

#### Aaron Anderson (Aug 12 2020 at 23:35):

and a Prop that the image of that map always has a specified length (2 until we're ready to define hypergraphs)

#### Aaron Anderson (Aug 12 2020 at 23:36):

Then we can define the `has_mem`

instance in terms of that map, etc.

#### Kyle Miller (Aug 12 2020 at 23:59):

I would suggest defining `hypergraph`

if you'd like to have this generalization. It seems like a good one to have, but it's not clear there's much to be gained except for complexity by making all graphs hypergraphs with an additional restriction.

One definition I'd used for graphs before was a pair of types `V`

and `E`

and a map `E -> sym2 V`

. It was nice in some ways, but having to deal with quotient types all the time in proofs was annoying. Another option is to define directed graphs using a map `E -> V \times V`

and then taking the quotient of directed graphs by edge reversal to get unoriented graphs.

If there is a type that is the disjoint union of all finite cartesian powers of `V`

(let's call it `carpow V`

temporarily) then you might consider having oriented hypergraphs using a map `E -> carpow V`

, and then taking the quotient by the symmetric group action on each hyperedge to get unoriented hypergraphs. (This is a generalization of the `E -> finset V`

idea, because vertices are allowed to appear multiple times per simplex. The problem with generalization is to figure out how far one should generalize.)

#### Kyle Miller (Aug 13 2020 at 00:00):

Aaron Anderson said:

Also, it'd be very hard to develop

`sym2`

to have all the features of`powerset_len 2`

, because`powerset_len 2`

is a subtype (actually a subset!) of`finset`

, which has a colossal amount of API available

That's true, but how much of the API for `finset`

is really relevant to unordered pairs?

#### Bhavik Mehta (Aug 13 2020 at 00:06):

Kyle Miller said:

I would suggest defining

`hypergraph`

if you'd like to have this generalization. It seems like a good one to have, but it's not clear there's much to be gained except for complexity by making all graphs hypergraphs with an additional restriction.

From this perspective, why not define `multigraph`

to use `sym2`

if you care about multigraphs, and have `graph`

to be normal graphs

#### Aaron Anderson (Aug 13 2020 at 00:08):

Kyle Miller said:

Aaron Anderson said:

Also, it'd be very hard to develop

`sym2`

to have all the features of`powerset_len 2`

, because`powerset_len 2`

is a subtype (actually a subset!) of`finset`

, which has a colossal amount of API availableThat's true, but how much of the API for

`finset`

is really relevant to unordered pairs?

The half of `big_operators`

that pertains to sums

#### Kyle Miller (Aug 13 2020 at 00:12):

Bhavik Mehta said:

Kyle Miller said:

I would suggest defining

`hypergraph`

if you'd like to have this generalization. It seems like a good one to have, but it's not clear there's much to be gained except for complexity by making all graphs hypergraphs with an additional restriction.From this perspective, why not define

`multigraph`

to use`sym2`

if you care about multigraphs, and have`graph`

to be normal graphs

Sorry, I'm not understanding the suggestion. I referring to @Aaron Anderson's idea of having graphs be hypergraphs specialized to having order-2 hyperedges.

Hypergraph theorists: do you ever want hyperedges that contain a vertex multiple times? I'm wondering this because it matters whether you define hyperedges using finsets or multisets.

#### Bhavik Mehta (Aug 13 2020 at 00:15):

Kyle Miller said:

Sorry, I'm not understanding the suggestion. I referring to Aaron Anderson's idea of having graphs be hypergraphs specialized to having order-2 hyperedges.

Your argument seems to be that it's not a good idea to define graphs as a special case of hypergraphs, but it is a good idea to define graphs as a special case of multigraphs - my question is why are multigraphs inherently more interesting to you than hypergraphs? In particular, your criticism of the hypergraph method as "complexity by making all graphs hypergraphs with an additional restriction" transfers exactly to multigraphs

#### Kyle Miller (Aug 13 2020 at 00:15):

@Aaron Anderson I see, that's a good point. I sort of wish `big_operators`

had some interface where you could sum over summable things, rather than feeling like everything needs to be a `finset`

.

One thing the multigraph interface will definitely have is a map `E -> finset V`

, so maybe this will solve this problem.

#### Kyle Miller (Aug 13 2020 at 00:17):

Bhavik Mehta said:

Your argument seems to be that it's not a good idea to define graphs as a special case of hypergraphs, but it is a good idea to define graphs as a special case of multigraphs

Oh, no, I don't think it is good to define simple graphs as special cases of multigraphs. In fact, I was thinking of not defining multigraphs, per se, but instead having a multigraph interface (through a class). This is to be able to define things like the type of all subgraphs of a graph and such.

#### Kyle Miller (Aug 13 2020 at 00:18):

This has seemed to be the cleanest way of dealing with this... but I still need to get the interface code reviewed, so we'll see...

#### Kyle Miller (Aug 13 2020 at 00:21):

And, actually, it's possible that the simple graph definition will eventually become a class, too. Then the special case of hypergraphs with order-2 edges will be simple graphs through this interface. Similarly, the current definition of a simple graph from a relation will have an instance imbuing it with the structure of a graph.

#### Kyle Miller (Aug 13 2020 at 00:22):

I've been uncomfortable pushing this way of doing things because I don't feel like the technique has proven itself enough, so I was waiting to see how it was going to work with multigraphs first.

#### Bryan Gin-ge Chen (Aug 13 2020 at 00:26):

I sort of wish big_operators had some interface where you could sum over summable things, rather than feeling like everything needs to be a finset.

Patrick argued a while back that we should look carefully at the big operators library in mathcomp (in Coq), which apparently treat sums over various collectiony things more uniformly, but no one ever took him up on that. It looks like he ported some of it in the old mathlib repo: https://github.com/leanprover-fork/mathlib-backup/tree/bigop

#### Aaron Anderson (Aug 13 2020 at 01:10):

Why didn’t I make simple_graph extend rel?

#### Jalex Stark (Aug 13 2020 at 01:37):

Aaron Anderson said:

Why didn’t I make simple_graph extend rel?

i remember talking you out of it but not why

#### Kyle Miller (Aug 13 2020 at 01:39):

Here's what I meant about how simple graphs might be a class (though it's not as compelling as the way it works for multigraphs):

```
import combinatorics.simple_graph
universes u v
class simple_graphs (α : Type u) :=
(V : α → Type v)
(adj : Π (G : α), V G → V G → Prop)
(sym : Π (G : α), symmetric (adj G) . obviously)
(loopless : Π (G : α), irreflexive (adj G) . obviously)
instance (V : Type u) : simple_graphs (simple_graph V) :=
{ V := λ _ , V,
adj := λ G, G.adj,
sym := λ G, G.sym,
loopless := λ G, G.loopless }
open simple_graphs
structure subgraph {α : Type u} [simple_graphs α] (G : α) :=
(V' : set (V G))
(E' : set (sym2 (V G)))
(has_edges : E' ⊆ sym2.from_rel (sym G))
(has_ends : ∀ (e ∈ E') (v ∈ e), v ∈ V')
instance {α : Type u} [simple_graphs α] (G : α) : simple_graphs (subgraph G) :=
{ V := λ G', subgraph.V' G',
adj := λ G' v w, ⟦(v.1, w.1)⟧ ∈ subgraph.E' G',
sym := λ G' v w h, by rwa sym2.eq_swap,
loopless := λ G' ⟨v, _⟩ h,
loopless G v (sym2.from_rel_prop.mp (subgraph.has_edges G' h)) }
```

where `simple_graph`

might be renamed `from_rel`

. It just seems a bit weird doing that.

#### Aaron Anderson (Aug 13 2020 at 01:41):

How is this different from an indexed family of graphs?

#### Kyle Miller (Aug 13 2020 at 01:42):

It's an indexed family of graphs, but the `simple_graphs (subgraph G)`

instance is what makes it a bit more than that.

#### Aaron Anderson (Aug 13 2020 at 01:44):

so this isn't supposed to replace `simple_graph`

#### Aaron Anderson (Aug 13 2020 at 01:46):

I don't think I understand what `simple_graphs (subgraph G)`

gets you

#### Kyle Miller (Aug 13 2020 at 01:47):

It lets you talk about `G' : subgraph G`

as being a simple graph itself because of polymorphism

#### Kyle Miller (Aug 13 2020 at 01:48):

Every proof and construction about `simple_graph`

would be changed into one for `simple_graphs`

to make this all work.

#### Aaron Anderson (Aug 13 2020 at 01:48):

Why don't we just define a coercion like with subgroups? We can already talk about a subgroup being a group

#### Kyle Miller (Aug 13 2020 at 01:51):

There are two parts to my understanding of this.

(1) Other structures tend to have only a single carrier type that's used for synecdoche: you refer to a group by its carrier type, usually. For graphs, you have both the vertex type and the edge type

(2) The way substructures are implemented for other algebraic objects is to make, say, a group be a `class`

, and then give a group instance to the subgroup `structure`

.

#### Kyle Miller (Aug 13 2020 at 01:52):

I'm pretty sure subgroups are already groups without needing a coercion. (This is at least true with modules and submodules.) There *is* a coercion from submodules to a carrier type.

#### Aaron Anderson (Aug 13 2020 at 01:52):

You're right that you don't need the coercion

#### Kyle Miller (Aug 13 2020 at 01:55):

There's a class resolution trick in here for algebraic structures: when you multiply terms together from a subgroup of a group, the elaborator sees that they are terms of the subgroup coerced into its carrier type, and this subgroup-as-carrier is what has the group implementation. (I guess I wasn't correct about there being no coercion involved.)

#### Kyle Miller (Aug 13 2020 at 02:09):

Going back to the idea that using the class approach means you're not constrained to a particular definition, here's another example:

```
structure simple_graph' (V : Type u) :=
(E : Type v)
(edges : E → sym2 V)
(edge_inj : function.injective edges)
(loopless : ∀ (e : E), ¬sym2.is_diag (edges e))
instance (V : Type u) : simple_graphs (simple_graph' V) :=
{ V := λ _, V,
adj := λ G v w, ⟦(v, w)⟧ ∈ G.edges '' set.univ,
sym := λ G v w h, by rwa sym2.eq_swap,
loopless := λ G v, begin
rintro ⟨e, _, h⟩,
apply G.loopless e, use v, rw h, refl,
end }
```

Now we can talk about subgraphs of a `simple_graph'`

.

#### Kyle Miller (Aug 13 2020 at 02:13):

You can also go on to prove that subgraphs form a complete lattice, as do simple graphs on a particular vertex set. (Though you can't prove that for `simple_graph'`

in a nice way because of the `edges`

map.)

#### Aaron Anderson (Aug 13 2020 at 02:42):

we appear to be discussing how to implement subgraphs

#### Aaron Anderson (Aug 13 2020 at 02:42):

how did we get here?

#### Aaron Anderson (Aug 13 2020 at 02:44):

We should for sure have a function that sends a subgraph to a graph structure on a subtype, but does this require changing our definition of `simple_graph`

at all?

#### Aaron Anderson (Aug 13 2020 at 03:00):

Jalex Stark said:

Aaron Anderson said:

Why didn’t I make simple_graph extend rel?

i remember talking you out of it but not why

oops turns out `rel`

isn't a structure

#### Aaron Anderson (Aug 13 2020 at 04:23):

Spitballing some of the different definitions and how they could relate to each other:

```
@[ext] structure simple_graph :=
(adj : V → V → Prop)
(sym : symmetric adj . obviously)
(loopless : irreflexive adj . obviously)
@[ext] structure multigraph :=
(E : Type u)
(vertices_of : E → finset V)
(two_vertices : ∀ e : E, (vertices_of e).card = 2 . obviously)
@[ext] structure hypergraph (n : ℕ) (V : Type u) :=
(edges : set (finset V))
(card_edge : ∀ e : finset V, e ∈ edges → e.card = n )
variables {V}
namespace simple_graph
def to_multigraph (G : simple_graph V) : multigraph V :=
{ E := {e : finset V // e.card = 2 ∧ ∀ (x y : V), x ∈ e ∧ y ∈ e ∧ x ≠ y → G.adj x y },
vertices_of := subtype.val }
instance has_coe_to_multigraph : has_coe (simple_graph V) (multigraph V) :=
{ coe := simple_graph.to_multigraph }
def to_hypergraph [decidable_eq V] (G : simple_graph V) : hypergraph 2 V :=
{ edges := {e | ∃ (x y : V), e = {x, y} ∧ G.adj x y},
card_edge := λ e h, by { rcases h with ⟨x, y, rfl, xy⟩,
rw finset.card_insert_of_not_mem, simp,
rw finset.mem_singleton, intro con, rw con at xy, apply G.loopless y xy, }}
instance has_coe_to_hypergraph [decidable_eq V] : has_coe (simple_graph V) (hypergraph 2 V) :=
{ coe := simple_graph.to_hypergraph }
end simple_graph
namespace multigraph
variables (G : multigraph V)
/-- Allows us to refer to a vertex being a member of an edge. -/
instance has_mem : has_mem V G.E := { mem := λ v e, v ∈ G.vertices_of e }
def multigraph.to_simple_graph (G : multigraph V) : simple_graph V :=
{ adj := λ a b, ∃ e : G.E, a ∈ e ∧ b ∈ e ∧ a ≠ b }
end multigraph
```

#### Kyle Miller (Aug 13 2020 at 07:34):

Aaron Anderson said:

how did we get here?

Mathematicians speak about subobjects as if they are objects all the time. We should set things up so we can do this in Lean, too, if it's possible. The way I've demonstrated is the only reasonable way I've found to get this to work, given Lean's features, and given my experiments it seems to work quite well. (If `G`

is a graph and `G' : subgraph G`

, then wouldn't you want to be able to write `v : V G'`

and `degree v`

? This is what the technique lets you do.)

Other algebraic structures in Lean have the nice property that there is some single type of terms that satisfy some axioms, but (multi)graphs unfortunately have two types: vertices and edges. Because they use only a single type, you can refer to the type as if it were the algebraic structure itself (synecdoche). For example, if `G' : subgroup G`

for `G`

a group, then because of Lean's automatic coercions, you can write `x y : G'`

and then write `x * y`

to use the subgroup's inherited group operation. The trick the implementation uses is that `coe_to_sort (subgroup G)`

is given a `group`

instance, so class resolution can find how to multiply `x`

and `y`

. This sort of trick does not seem to apply directly to the case of graphs because there is no place automatic coersion might happen.

In principle, the way the group typeclass could have worked out is to declare that a given type consists of groups. I think about it like you are declaring that a type is the set of objects of a category with a given property (neglecting, for now, the morphisms). It's like you're pulling the typeclass back a level, so to speak, to the indexing set. A benefit is that you can now have structures containing multiple types, the composite of which can be referred to by a letter (like being able to refer to a graph `G`

rather than having a `V`

and `E`

floating around). You can still define `coe_to_sort`

instances if you want one of the sets to be primary.

Subgraphs are just one example of a type of graphs. Another substructure-like thing is graph minors, and this technique seems to let you define a type of all minors on a given graph, where each term may be regarded as a graph itself.

but does this require changing our definition of

`simple_graph`

at all?

No, it wouldn't, other than maybe lifting definitions and lemmas up to `simple_graphs`

. I'm not particularly motivated to change anything in the short term regarding this, but I figured I'd make a case for a seemingly workable design in case anyone wants to deal with subgraphs of simple graphs.

Regarding the spitballed definitions, I worry about using quotient-based definitions for multigraphs. One of the earliest definitions I used was, essentially, `vertices_of : E -> sym2 V`

, which should be simpler in some ways because of the image is, effectively, a quotient of a subtype rather than a subtype of quotients. (By the way, `finset`

is not correct because multigraphs can have self-loops; one fix is to make `two_vertices`

say the cardinality is 1 or 2, and other is to use `multiset`

instead). However, `sym2`

is still a quotient. Switching to another definition that doesn't involve quotients (I've posted variations to Zulip a few times and the paper it's based on) seems to reduce the sizes of proofs by an appreciable amount.

Take a look at `sym2.sym2_equiv_sym`

, which is part of the proof that `sym2`

is equivalent to cardinality-two multisets. Granted, this only needs to be done once, but it's oddly complicated and makes me worried that similar problems would be pervasive for graph theory theorems that don't deal with hypergraphs.

Yet another multigraph definition that is especially convenient for proving things like the degree-sum formula, is

```
structure multigraph (V : Type u) (E : Type v) :=
(D : Type v)
(dart_opp : D → D)
(dart_opp_inv : function.involutive dart_opp)
(dart_vert : D → V)
(dart_edge : D → E)
(dart_edge_surj : function.surjective dart_edge)
(two_to_one : ∀ (d : D), dart_edge d = dart_edge (dart_opp d))
```

A *dart* is one of the two ends of an edge. Or you can think of it as one of the two possible orientations of an edge. This is a combinatorial map that has forgotten its vertex rotation. (I'm partial to this definition because it's one step away from combinatorial maps, which would then immediately give us the definition of planar embeddings of (connected) graphs.)

#### Kyle Miller (Aug 13 2020 at 07:38):

I just realized another perspective on this: if you have a structure `X`

and a number of `has_coe a X`

instances for varying `a`

, perhaps it is better to define the structure as a class parameterized by `a`

so you don't have to have coercion arrows everywhere. This is exactly what the `simple_graphs`

example is doing.

#### Kyle Miller (Aug 13 2020 at 07:41):

A thing I find awkward about it is that there is always the tautological instance, since the class is a good enough definition in its own right. Before, I was using `simple_graph`

as the tautological instance, but you could also use `simple_graphs`

itself, since a class is just a structure with the `@[class]`

attribute.

#### Kyle Miller (Aug 13 2020 at 07:48):

Beyond all the coercion arrows, I remember another awkwardness when I had tried the `has_coe`

route earlier in the summer. It's that when you have subgraphs and want to treat them as graphs parameterized by a vertex type, you have to specify the vertex type in the instance's type, and that makes it more difficult as a user of the API to get the class resolution to find the coercion. This isn't an issue when the vertex type is not parameterized, but then that leads to a new fun issue that universe inference stops working as well.

#### Bhavik Mehta (Aug 13 2020 at 12:32):

It's worth of course looking at how groups and subgroups are defined, to see the mathlib standard practice of how to deal with the sub-object problem, since this is a question others have already thought about in detail

#### Kyle Miller (Aug 13 2020 at 17:35):

The second paragraph in what I wrote is about how mathlib deals with subobjects of things like groups. The issue is that a group is referred to by the type of its elements (i.e., let G be a group and g an element of G), but a graph consists of two types (i.e., let G be a graph, v a vertex in V(G) and e and edge in E(G)). Mathlib uses a trick involving `coe_to_sort`

and class resolution so that subgroups are groups, too. This trick does not apply to graphs, as far as I can tell: a group is a type, a graph is a term.

#### Alena Gusakov (Aug 13 2020 at 20:07):

I don't have much to say but I'd also like to throw in my vote in favor of treating subgraphs as their own objects lol

#### Alena Gusakov (Aug 13 2020 at 20:08):

That's something I was trying to do with my definition of subgraph/induced subgraph

#### Kyle Miller (Aug 13 2020 at 20:12):

I've posted a message to #general about the subobject problem, and hopefully the experts will weigh in. Ideally, if `G : graph`

and `G' : subgraph G`

, then you can use `G'`

as if it were a graph. For instance, write `degree v`

for `v : V G'`

.

#### Kyle Miller (Aug 14 2020 at 01:21):

@Jalex Stark @Aaron Anderson As an experiment, I redid the simple graph interface so that subgraphs of simple graphs are simple graphs, too. It's in mathlib:simple_graphs (see https://github.com/leanprover-community/mathlib/blob/simple_graphs/src/combinatorics/simple_graph.lean)

I'd appreciate it if anyone might take it for a spin and see if anything goes wrong with the interface. One change you have to make to use it is to not use dot notation since it's, unfortunately, not supported without some hacks. Another is that you need `V G`

rather than declaring the vertex type.

There are potentially too many implicit arguments, but I have not run into issues myself yet. Implicit arguments relieve us of the need to even mention `G`

, for example in `degree v`

for `v : V G`

. This uses the trick that `v`

knows it's from a graph `G`

because it is in its type. Similar things go for `neighbor_set v`

rather than `G.neighbor_set v`

.

The commit defines subgraphs, induced subgraphs, and the bounded lattice of subgraphs. To construct a subgraph from a relation, you can use `simple_graph.from_rel`

if you want, but the intended use is to write something like

```
variables {α : Type u} [simple_graphs α] (G : α)
```

to get an arbitrary simple graph `G`

. (There is a vague resemblance to section 3 of the paper https://hal.inria.fr/hal-00825074v1/document here.)

If you want, you can declare

```
local infix ` ~ ` := adj_rel
```

to use `v ~ w`

for the vertex adjacency relation for `v w : V G`

. (This uses `adj_rel`

instead of `adj G`

because of some implicit argument handling...)

#### Kyle Miller (Aug 14 2020 at 01:35):

(One thing I've noticed is that it seems like it'll take some more work so that you can compare the degrees of a vertex relative to two different subgraphs.)

#### Bhavik Mehta (Aug 14 2020 at 16:58):

Kyle Miller said:

The second paragraph in what I wrote is about how mathlib deals with subobjects of things like groups. The issue is that a group is referred to by the type of its elements (i.e., let G be a group and g an element of G), but a graph consists of two types (i.e., let G be a graph, v a vertex in V(G) and e and edge in E(G)). Mathlib uses a trick involving

`coe_to_sort`

and class resolution so that subgroups are groups, too. This trick does not apply to graphs, as far as I can tell: a group is a type, a graph is a term.

You're correct of course - I should have read your messages more carefully!

#### Kyle Miller (Aug 14 2020 at 18:29):

@Jalex Stark @Aaron Anderson Ok, here's my newest solution to the "synecdoche problem." I haven't really been happy with any of my proposals so far, hence all the discussion, but I think this one might finally be something that doesn't feel weird:

It's surprisingly simple:

```
class simple_graph {α : Type u} (G : α) :=
(V : Type v)
(adj : V → V → Prop)
(symm : symmetric adj . obviously)
(loopless : irreflexive adj . obviously)
```

You just say that a *term* has a `simple_graph`

instance. From then on you can write `V G`

and so on. This lets you define `simple_graph`

instances for subgraphs easily:

```
structure subgraph :=
(V' : set (V G))
(E' : set (sym2 (V G)))
(edge_sub : E' ⊆ edge_set G)
(has_verts : ∀ (e ∈ E') (v ∈ e), v ∈ V')
instance subgraph.simple_graph (G' : subgraph G) : simple_graph G' :=
{ V := G'.V',
adj := λ v w, ⟦(v.val, w.val)⟧ ∈ G'.E',
symm := λ v w h, by rwa sym2.eq_swap,
loopless := λ ⟨v, _⟩ h, loopless v (sym2.from_rel_prop.mp (G'.edge_sub h)) }
```

#### Kyle Miller (Aug 14 2020 at 18:31):

(Getting this right for simple graphs seems like a good test bed for other combinatorial objects that have subobjects and other derived objects.)

#### Jalex Stark (Aug 14 2020 at 21:40):

(I feel really busy, but i've set myself a calendar event to give this a hard look tomorrow.)

I've gotten as far as being confused about which lines of code lead to `V G`

being the type of vertices of `G`

. If whatever magic this is also makes it easier to talk about subgraphs, I'll be pretty happy with it :)

#### Aaron Anderson (Aug 14 2020 at 21:43):

I think I prefer this to the `simple_graphs`

type, but I have another potentially dumb question:

Why is this better than defining

```
class simple_graph :=
(V : Type v)
(adj : V → V → Prop)
(symm : symmetric adj . obviously)
(loopless : irreflexive adj . obviously)
```

and then just talking about `G.V`

instead of `V G`

?

#### Kyle Miller (Aug 14 2020 at 21:43):

@Jalex Stark Thanks -- I know how busy everyone is and how it can be a hard to find time to evaluate other people's work!

#### Kyle Miller (Aug 14 2020 at 21:45):

@Aaron Anderson That's a class with no parameters, right? How would you ever define instances?

(Are there tricks to make `G.V`

work? I think it only works if `G`

has a type in the `simple_graph`

namespace, but I could be wrong. I've been trying hard to find *some* way to make it work...)

#### Kyle Miller (Aug 14 2020 at 21:49):

Jalex Stark said:

I've gotten as far as being confused about which lines of code lead to

`V G`

being the type of vertices of`G`

.

The type of `simple_graph.V`

is `Π {α : Type u} (G : α) [c : simple_graph G], Type v`

. The `G`

parameter is automatically explicit because `V`

needs to depend on something.

#### Jalex Stark (Aug 14 2020 at 22:36):

Oh, thanks. I thought `V : Type u`

but in fact it's something like `simple_graph.V : simple_graph \to Type u`

#### Aaron Anderson (Aug 14 2020 at 23:40):

Kyle Miller said:

Aaron Anderson That's a class with no parameters, right? How would you ever define instances?

(Are there tricks to make

`G.V`

work? I think it only works if`G`

has a type in the`simple_graph`

namespace, but I could be wrong. I've been trying hard to findsomeway to make it work...)

```
class simple_graph :=
(V : Type*)
(adj : V → V → Prop)
(symm : symmetric adj . obviously)
(loopless : irreflexive adj . obviously)
variable (V : Type*)
def complete_graph : simple_graph := ⟨V, ne⟩
```

#### Kyle Miller (Aug 14 2020 at 23:54):

I'm not sure how you'd say that every `subgraph`

is a `simple_graph`

. It looks like you're using a `class`

as a `structure`

here (which works because `class`

is shorthand to declare a `structure`

with the `class`

attribute).

#### Aaron Anderson (Aug 15 2020 at 00:57):

I think I see what you mean

#### Aaron Anderson (Aug 15 2020 at 00:59):

To be sure, do we really want one definition of subgraphs?

#### Aaron Anderson (Aug 15 2020 at 00:59):

We want an `induced_subgraph`

function for sure

#### Aaron Anderson (Aug 15 2020 at 01:00):

But maybe then we just want a type for subgraphs on V

#### Kyle Miller (Aug 15 2020 at 01:00):

I'm not sure we want only a single definition -- I'd like to keep options open so that any number of derived objects can be defined. However, what I was thinking about `induced_subgraph`

is that it tends to be used within the lattice of subgraphs, so I made it a subgraph.

#### Aaron Anderson (Aug 15 2020 at 01:01):

That is, just changing the edge relation

#### Kyle Miller (Aug 15 2020 at 01:02):

The type for graphs on `V`

is `subgraph (complete_graph V)`

, I think

#### Kyle Miller (Aug 15 2020 at 01:03):

Whether that's the best way to deal with it, I'm not sure, but at least that means it's a bounded lattice.

#### Kyle Miller (Aug 15 2020 at 01:03):

Oh, I'm wrong. You'd want `spanning_subgraph (complete_graph V)`

#### Kyle Miller (Aug 15 2020 at 01:04):

where a `spanning_subgraph`

is a subgraph that contains all the vertices. These are used in the definition of Tutte polynomials.

#### Aaron Anderson (Aug 15 2020 at 01:04):

Yeah, I guess what I’m asking for is whether we really want `subgraph`

or just `spanning_subgraph`

#### Kyle Miller (Aug 15 2020 at 01:04):

I'm under the impression that subgraphs with varying vertex sets are important, so I'd lean toward eventually having both.

#### Kyle Miller (Aug 15 2020 at 01:05):

But I'm not sure. The theorems will guide the way.

#### Kyle Miller (Aug 15 2020 at 01:08):

Maybe what you're saying is that because every graph is a subgraph of the complete graph with the same vertex set, maybe subgraphs should always be within that particular bounded lattice?

#### Kyle Miller (Aug 15 2020 at 01:09):

though I could imagine having the lattice have a specific `top`

might be useful

#### Aaron Anderson (Aug 15 2020 at 01:18):

I meant that I would imagine having a `subgraph`

type that’s actually `spanning_subgraph`

, and any time we need the other kind, we talk about `{s: set G} subgraph s`

#### Aaron Anderson (Aug 15 2020 at 01:18):

No idea if this actually works until we have theorems about subgraphs to prove

#### Aaron Anderson (Aug 15 2020 at 01:19):

And inductions to do

#### Kyle Miller (Aug 15 2020 at 01:20):

Oh right, this is why `subgraph G`

is important as-is. There are inductions where you add individual vertices or edges.

#### Kyle Miller (Aug 15 2020 at 01:20):

and there are probably others where you only induct on adding edges, so you'd want `spanning_subgraph G`

for that

#### Kyle Miller (Aug 15 2020 at 20:27):

@Aaron Anderson On this test branch, I added `incident_set`

and showed it was equivalent to `neighbor_set`

, hence they have the same cardinality, if you want to try incidence matrices again. https://github.com/leanprover-community/mathlib/blob/simple_graphs2/src/combinatorics/simple_graph.lean#L106 There's also `incident_finset`

, but I haven't added any lemmas connecting it to `incident_set`

.

(This involved adding a decidable version of `sym2.mem.other`

called `sym2.mem.other'`

. @Jalex Stark if you want to code golf something you could take a look at that :smile:. I'm thinking of removing `vmem`

from `sym2`

because it is extremely specialized compared to `sym2.mem.other'`

. Being able to prove `other'`

is well-defined was outside my capabilities back when I defined `vmem`

.)

By the way, Jalex, what sorts of edge set cardinality issues are there? I remember you mentioning something about that.

#### Kyle Miller (Aug 17 2020 at 00:23):

This `simple_graphs2`

branch now has the degree-sum formula and a number of new `sym2`

lemmas to help out. The degree-sum formula is mostly combinatorial in the sense that there is a new type, `darts`

, with one term per orientation of each edge, and then each intermediate equality comes from some kind of bijection with this (I didn't explicitly construct these bijections all the time, though).

This is what the statement looks like:

```
variables {α : Type u} (G : α) [simple_graph G] [fintype (V G)]
-- and some decidable instances (not needed for classical locale)
variables [decidable_eq (V G)] [decidable_rel (adj_rel G)]
lemma degree_sum : ∑ v : V G, degree v = 2 * (edge_finset G).card
```

(@Bhavik Mehta I think I remember you mentioning you had a proof of this for simple graphs. Maybe you might be interested in helping to refactor this one?)

#### Jalex Stark (Aug 17 2020 at 21:22):

I think a path to getting a definitive answer about the right graph definition, without having to hold quite so much of a subjective notion about what's easy to program with in one's head, goes like:

Implement $n$ different APIs and prove that they are all equivalent. We should be able to extract a lot of information from the knowledge of which translations are hardest.

#### Jalex Stark (Aug 17 2020 at 21:24):

Also "write the translations" is parallelizable (I guess you expect there to be like $n \log n$ of them), so maybe we get more of a return to the existence of this stream.

#### Jalex Stark (Aug 17 2020 at 21:25):

I guess this is a special case of an idea of Mario, where "graphs API" is substituted with "entire theorem-provers"

#### Jalex Stark (Aug 18 2020 at 01:38):

I guess Kyle had a neat idea on how to make a central simple_graph type together with a class `has_coe_to_simple_graph`

which links graph implementations to graphs.

#### Bhavik Mehta (Aug 18 2020 at 01:46):

Kyle Miller said:

(Bhavik Mehta I think I remember you mentioning you had a proof of this for simple graphs. Maybe you might be interested in helping to refactor this one?)

Sure I can help out if needed but I'm pretty busy at the minute so I can't promise much

#### Kyle Miller (Aug 18 2020 at 02:25):

Jalex Stark said:

I guess Kyle had a neat idea on how to make a central simple_graph type together with a class

`has_coe_to_simple_graph`

which links graph implementations to graphs.

To expand on this, the definition in the `simple_graphs2`

branch sort of came out of the following design process. Let's say you started with this definition of a simple graph:

```
structure simple_graph (V : Type*) :=
(adj : V → V → Prop)
(symm : symmetric adj)
(loopless : irreflexive adj)
```

and then you define spanning subgraphs on a given graph (i.e., subgraphs with all the vertices) by something like

```
structure spanning_subgraph {V : Type*} (G : simple_graph V) :=
(adj : V → V → Prop)
(symm : symmetric adj)
(prop : ∀ (v w : V), adj v w → G.adj v w)
```

One basic definition for simple graphs is the set of neighboring vertices:

```
def neighbor_set {V : Type*} (G : simple_graph V) (v : V) := set_of (G.adj v)
```

However, if you have a `spanning_subgraph G`

, you cannot use `neighbor_set`

directly -- you would need some coercion. Let's define an interface for this. While you could try using `has_coe`

, there is a typeclass inference problem: `has_coe a b`

is a function of both `a`

and `b`

, so you would need to specify type hints to get it to coerce correctly (plus, we won't gain any benefits from Lean's automatic coercion features). This is not so bad for spanning subgraphs, but it is not so good for subgraphs since the vertex type needs to be referred to as the vertex subset coerced to a type. To make it so `b`

is a function of `a`

, we can define our own coercion class:

```
class has_coe_to_simple_graph (α : Type*) :=
(V : α → Type v)
(to_simple_graph : Π (G : α), simple_graph (V G))
```

Then, for example,

```
instance {V : Type*} (G : simple_graph V) :
has_coe_to_simple_graph (spanning_subgraph G) :=
{ V := λ _, V,
to_simple_graph := λ G',
{ adj := G'.adj,
symm := G'.symm,
loopless := λ x h, G.loopless x (G'.prop _ _ h) } }
```

However, we cannot yet do `neighbor_set G' v`

for `G' : spanning_subgraph G`

, since it is not literally a graph. Let's define some accessor functions to get some `simple_graph`

fields for coerceable terms and use them to define the `neighbor_set`

:

```
variables {α : Type*} [has_coe_to_simple_graph α]
def V (G : α) := has_coe_to_simple_graph.V G
def adj (G : α) := (has_coe_to_simple_graph.to_simple_graph G).adj
def neighbor_set (G : α) (v : V G) := set_of (adj G v)
```

While `spanning_subgraph G`

is not a `simple_graph`

*per se*, you can interact with it as if it were one.

This might be an OK interface as it is, but there is a simplification to this. If we were to take the fields of `simple_graph`

and put them into `has_coe_to_simple_graph`

, then we would have

```
class has_coe_to_simple_graph (α : Type*) :=
(V : α → Type v)
(adj : Π (G : α), V G → V G → Prop)
(symm : Π (G : α), symmetric (adj G))
(loopless : Π (G : α), irreflexive (adj G))
```

This is the class `simple_graphs`

that I had mentioned last week! A weird thing about it, though, is how every field is a function. What if we lifted the `G`

argument out? Let's also rename this class `simple_graph`

. We would obtain

```
class simple_graph {α : Type*} (G : α) :=
(V : Type v)
(adj : V → V → Prop)
(symm : symmetric adj)
(loopless : irreflexive adj)
```

This is the definition in the `simple_graphs2`

branch. It is the result of flattening the coercion class and the definition of the structure. This lets us not have to redefine all the fields using accessor functions that depend on a coercion class: the members of this class *are* the accessor functions.

In the `has_coe_to_simple_graph`

approach, note that to make things generic with respect to all things that are graph-like, lemmas and definitions would have to be in terms of the accessor functions anyway, so you would never refer to fields of `simple_graph`

. Thus, you lose nothing by folding it all in and defining this `simple_graph`

class.

One caveat is that to define a simple graph from a particular relation, you need a "tautological" instance:

```
structure simple_graph_on (V : Type u) :=
(rel : V → V → Prop)
(symm : symmetric rel)
(irrefl : irreflexive rel)
instance simple_graph_on.simple_graph (V : Type u) (G : simple_graph_on V) : simple_graph G :=
{ V := V,
adj := G.rel,
symm := G.symm,
loopless := G.irrefl }
```

Another caveat is that different graphs have vertex types that are referred to differently, even if the vertex types are definitionally equal. For graphs on the same vertex type, you would probably want to use the type `simple_graph_on V`

. One could define a bounded lattice instance for this.

#### Jalex Stark (Aug 18 2020 at 02:41):

Great write-up.

#### Kyle Miller (Aug 29 2020 at 22:38):

This definition of graphs has some issues, but it's kind of amusing so I'll put it here. It uses a bit of synecdoche, saying a graph *is* its adjacency relation. To coerce something like a subgraph into being a graph, you use the `⇑`

function coercion arrow.

```
class is_graph {V : Type*} (adj : V → V → Prop) :=
(symm' : symmetric adj)
(loopless' : irreflexive adj)
namespace graph
section accessors
variables {V : Type*} (G : V → V → Prop) [is_graph G]
def adj (v w : V) := G v w
def symm := @is_graph.symm' V G
def loopless := @is_graph.loopless' V G
end accessors
variables {V : Type*}
def neighbor_set (G : V → V → Prop) [is_graph G] (v : V) : set V := set_of (adj G v)
section subgraphs
structure subgraph (G : V → V → Prop) [is_graph G] :=
(V' : set V)
(adj' : V → V → Prop)
(adj_sub : ∀ ⦃v w : V⦄, adj' v w → adj G v w)
(edge_vert : ∀ ⦃v w : V⦄, adj' v w → v ∈ V')
(symm' : symmetric adj')
instance (G : V → V → Prop) [is_graph G] : has_coe_to_fun (subgraph G) :=
{ F := λ G', subtype G'.V' → subtype G'.V' → Prop,
coe := λ G', λ v w, G'.adj' v.val w.val }
instance (G : V → V → Prop) [is_graph G] (G' : subgraph G) : is_graph G' :=
{ symm' := λ v w h, G'.symm' h,
loopless' := λ ⟨v, _⟩ h, loopless G v (G'.adj_sub h) }
end subgraphs
end graph
```

#### Kyle Miller (Aug 29 2020 at 22:42):

but it seems to actually let you use a subgraph as if it were a graph:

```
example (G : V → V → Prop) [is_graph G] (G' : subgraph G) (v : V) (h : v ∈ G'.V') : true :=
begin
let s := neighbor_set G' ⟨v, h⟩,
end
```

Lean automatically coerces `G'`

into a function, so it's secretly `neighbor_set ⇑G' ⟨v, h⟩`

.

#### Bhavik Mehta (Aug 29 2020 at 22:48):

Isn't this the current situation with subgroups? You can use a subgroup as if it's a group.. I feel like I'm missing something here though

#### Kyle Miller (Aug 29 2020 at 22:49):

Subgroups rely on `has_coe_to_sort`

to work

#### Bhavik Mehta (Aug 29 2020 at 22:49):

A curiosity (not related to the current discussion) is that nlab defines a graph as a set equipped with a symmetric reflexive relation, not a symmetric irreflexive relation!

#### Bhavik Mehta (Aug 29 2020 at 22:50):

Kyle Miller said:

Subgroups rely on

`has_coe_to_sort`

to work

Sure, but you're using a coe to function instead to serve the same purpose?

#### Kyle Miller (Aug 29 2020 at 22:50):

Exactly, it's something I hadn't thought about trying before

#### Bhavik Mehta (Aug 29 2020 at 22:52):

Bhavik Mehta said:

A curiosity (not related to the current discussion) is that nlab defines a graph as a set equipped with a symmetric reflexive relation, not a symmetric irreflexive relation!

and this matters because it lets a quotient object in the category be a graph minor

#### Kyle Miller (Aug 29 2020 at 22:52):

If Lean just had a way to let you define functions that auto-coerce an argument using a user-specified coercion typeclass, there'd be no need for this sort of hack

#### Kyle Miller (Aug 29 2020 at 22:52):

Here, Lean knows that if an argument requires a function, then it'll try to coerce it for you using `has_coe_to_fun`

#### Kyle Miller (Aug 29 2020 at 23:09):

Bhavik Mehta said:

A curiosity (not related to the current discussion) is that nlab defines a graph as a set equipped with a symmetric reflexive relation, not a symmetric irreflexive relation!

Oh, I kept misreading this and now I understand what you're saying. When you define it as irreflexive, then things like the neighborhood set in the graph theory sense are easy to define. When it's a reflexive relation, you instead get what Bollobas defines to be the closed neighborhood set.

Edge contractions certainly do not correspond to homomorphisms when they are defined as irreflexive relations... You can change the definition of a homomorphism so that they do, but it's sort of ugly.

In my research, I've been thinking of a generalization multigraphs as being like the usual multigraphs, except some edges are labeled as being contractible. Two of these multigraphs are equivalent if they can be related by a sequence of contractions of contractible non-loop edges and deletions of contractible loop edges. Then the operation of edge contraction corresponds to labeling an edge as contractible. (This definition reduces to multigraphs with a special loop edge at each vertex, if you want.) I was using this generalization for a few reasons, one being that both deletion and contraction are homomorphisms.

#### Kyle Miller (Aug 29 2020 at 23:13):

Bhavik Mehta said:

Isn't this the current situation with subgroups? You can use a subgroup as if it's a group.. I feel like I'm missing something here though

But also, this new method is something to compare the `simple_graphs2`

branch to. There, I have subgraphs as graphs working just fine without needing any of these coercion hacks, though maybe it's less of a hack than I thought.

#### Bhavik Mehta (Aug 29 2020 at 23:13):

Yeah, I was basically just describing the discussion here which I hadn't considered before

#### Kyle Miller (Aug 29 2020 at 23:19):

The other reason I was considering these graphs, by the way, is that you can define a symmetric monoidal category of multigraphs when you have these special contractible edges (objects are sets of points, morphisms are graphs between them). You need contractible edges to have identity elements. I haven't done enough with it, but I'm pretty sure you can define a 2-category of multigraphs in a similar way. (I've been slowly writing a paper about these things, but then got distracted by Lean this summer...)

#### Bhavik Mehta (Aug 29 2020 at 23:23):

Makes sense

#### Nicolas Rouquette (Nov 08 2020 at 01:44):

I found an interesting formalization of directed graphs in a gist by Nick Scheel here:

https://gist.github.com/MonoidMusician/1c8cc2ec787ebaf91b95d67cbc5c3498

I adapted his gist to work with Lean 3.23.0 in a repo here:

https://github.com/NicolasRouquette/digraphs

As a newbie w/ lean, I ran into several questions: https://github.com/NicolasRouquette/digraphs#questions

I really would appreciate some guidance about this.

#### Bryan Gin-ge Chen (Nov 08 2020 at 18:38):

For Q3, you can use `#print`

to show the definition. `#check`

only displays the type. Note that for definitions constructed using the equation compiler, you may see that the definition is just something like `blah._main1`

and you'll have to do `#print blah._main1`

, possibly a few times.

#### Chris B (Nov 08 2020 at 22:04):

Since it's decidable, an easy solution for Q1 is:

```
def vt_mk (s : string) (h : s ∈ vs . tactic.exact_dec_trivial): vT := ⟨s, h⟩
def vt_a' : vT := vt_mk "a"
#print vt_a'
```

The binder style in `h`

uses the tactic after the `.`

to try and automatically make an argument of that type.

Someone touched on Q2 in the thread in new_members, showing how to destructure subtypes with the equation compiler. I'm not sure why it doesn't like subtypes over strings, so I can't help with that.

```
example : { s : string // s.length ≠ 0 } -> bool
| ⟨"a", h⟩ := tt
| _ := ff
/-
equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
nested exception message:
induction tactic failed, recursor 'or.dcases_on' can only eliminate into Prop
-/
```

#### Chris B (Nov 08 2020 at 22:07):

Seems like you can work around it by just matching on the string after.

```
def phi2: eT → option (arcT vT)
| ⟨s, _⟩ :=
match s with
| "e1" := some $ arc1
| "e2" := some $ arc2
| "e3" := some $ arc3
| _ := none
end
```

Last updated: May 08 2021 at 23:10 UTC