graph defs

Stream: graph theory

[Aaron Anderson]

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]

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]

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]

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]

They are not type-equivalent, because sym2 includes the diagonal.

[Aaron Anderson]

Graphs with loops need sym2, loopless graphs do not

[Aaron Anderson]

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]

I also like the generalization to hypergraphs

[Bhavik Mehta]

Aaron Anderson said:

They are not type-equivalent, because sym2 includes the diagonal.

ah of course, makes sense

[Aaron Anderson]

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]

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

[Aaron Anderson]

Then we can define the has_mem instance in terms of that map, etc.

[Kyle Miller]

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]

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]

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]

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 available

That'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]

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]

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]

@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]

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]

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]

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]

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]

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]

Why didn’t I make simple_graph extend rel?

[Jalex Stark]

Aaron Anderson said:

Why didn’t I make simple_graph extend rel?

i remember talking you out of it but not why

[Kyle Miller]

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]

How is this different from an indexed family of graphs?

[Kyle Miller]

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]

so this isn't supposed to replace simple_graph

[Aaron Anderson]

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

[Kyle Miller]

It lets you talk about G' : subgraph G as being a simple graph itself because of polymorphism

[Kyle Miller]

Every proof and construction about simple_graph would be changed into one for simple_graphs to make this all work.

[Aaron Anderson]

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

[Kyle Miller]

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]

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]

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

[Kyle Miller]

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]

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]

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]

we appear to be discussing how to implement subgraphs

[Aaron Anderson]

how did we get here?

[Aaron Anderson]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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

[Kyle Miller]

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]

@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]

(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]

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]

@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:

https://github.com/leanprover-community/mathlib/blob/simple_graphs2/src/combinatorics/simple_graph.lean

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]

(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]

(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]

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]

@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]

@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]

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]

Oh, thanks. I thought V : Type u but in fact it's something like simple_graph.V : simple_graph \to Type u

[Aaron Anderson]

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 find some way 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]

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]

I think I see what you mean

[Aaron Anderson]

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

[Aaron Anderson]

We want an induced_subgraph function for sure

[Aaron Anderson]

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

[Kyle Miller]

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]

That is, just changing the edge relation

[Kyle Miller]

The type for graphs on V is subgraph (complete_graph V), I think

[Kyle Miller]

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]

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

[Kyle Miller]

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

[Aaron Anderson]

Yeah, I guess what I’m asking for is whether we really want subgraph or just spanning_subgraph

[Kyle Miller]

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

[Kyle Miller]

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

[Kyle Miller]

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]

though I could imagine having the lattice have a specific top might be useful

[Aaron Anderson]

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]

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

[Aaron Anderson]

And inductions to do

[Kyle Miller]

Oh right, this is why subgraph G is important as-is. There are inductions where you add individual vertices or edges.

[Kyle Miller]

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

[Kyle Miller]

@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]

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

https://github.com/leanprover-community/mathlib/blob/simple_graphs2/src/combinatorics/simple_graph.lean#L686

(@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]

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]

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]

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

[Jalex Stark]

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]

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]

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]

Great write-up.

[Kyle Miller]

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]

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]

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]

Subgroups rely on has_coe_to_sort to work

[Bhavik Mehta]

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]

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]

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

[Bhavik Mehta]

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]

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]

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]

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]

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]

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

[Kyle Miller]

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]

Makes sense

[Nicolas Rouquette]

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]

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]

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]

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