# Zulip Chat Archive

## Stream: graph theory

### Topic: simple_graphs2

#### Alena Gusakov (Aug 24 2020 at 22:24):

I pushed an error fix that Kevin helped me out with

#### Alena Gusakov (Aug 24 2020 at 22:24):

Basically just got rid of the problem in

`degree_le`

where Lean didn't know why we were allowed to compare the degrees because it didn't know`degree (G'.in_subgraph hv)`

is a`fintype`

#### Alena Gusakov (Aug 24 2020 at 22:58):

just kidding, somehow there's still an error somewhere

#### Kyle Miller (Aug 24 2020 at 23:01):

I'm going to take a look -- I had some troubles with these instances because they caused class resolution to not terminate. (I'm trying to get my own changes to the branch in order so I can merge yours.)

#### Kyle Miller (Aug 25 2020 at 08:16):

Alena Gusakov said:

just kidding, somehow there's still an error somewhere

These instances are tricky, and I've been struggling with how to define these off and on for a while, but they might finally now be OK. It turns out you can't actually have them as instances because they "introduce metavariables", which are caused by variables on the LHS of the colon that cannot be totally inferred by either class resolution or the usual implicit argument elaboration.

Anyway, `degree_le`

is now a lemma (with proof!), and it makes use of some new lemmas involving graph embeddings. The idea is that it's not hard to prove that the neighbor set of a vertex in a subgraph embeds in the neighbor set of that vertex in a supergraph, and then `fintype.card_le_of_injective`

does the rest.

If you wanted, you could follow the same strategy with `embedding.map_edge_set`

to show that the cardinality of an edge set of a subgraph is less than or equal to the cardinality of the supergraph's edge set.

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

A couple of other sorry's:

`complete_graph_min_colors`

is that a complete graph on`n`

vertices needs at least`n`

colors in a proper coloring.`exists_path_eq_eqv_gen`

should follow from a lemma that if there is a walk between two vertices then there is a path between them.

#### Alena Gusakov (Aug 25 2020 at 13:16):

~~it seems like there are other errors now though - namely in the proofs of all of the ~~ oops, restarted lean and the errors went away`map_edge_set`

definitions

#### Kyle Miller (Aug 26 2020 at 05:13):

After some discussion with @Alena Gusakov, the branch now has what seems to be an easier-to-work-with definition of subgraphs:

```
structure subgraph :=
(V' : set (V G))
(adj' : V G → V G → Prop)
(adj_sub : ∀ ⦃v w : V G⦄, adj' v w → v ~g w)
(edge_vert : ∀ ⦃v w : V G⦄, adj' v w → v ∈ V')
(symm' : symmetric adj')
```

(It has the correct extensionality property, which I had trouble getting right with this sort of formulation, that there is exactly one term per subgraph. That's why the earlier definition used a subset of edges.)

As an experiment in a technique to show two definitions are equivalent, I kept the old definition as a protected definition in the `simple_graph.subgraph`

namespace:

```
protected structure of_edge_set' (G : α) :=
(V' : set (V G))
(edge_set' : set (sym2 (V G)))
(edge_sub : edge_set' ⊆ edge_set G)
(has_verts : ∀ ⦃e : sym2 (V G)⦄ ⦃v : V G⦄, e ∈ edge_set' → v ∈ e → v ∈ V')
```

Then I gave it a `simple_graphs`

instance and proved two statements:

```
protected def equiv_of_edge_set' : subgraph G ≃ of_edge_set' G
def iso_of_edge_set' (G' : subgraph G) : G' ≃g subgraph.equiv_of_edge_set' G'
```

That is to say, the types are equivalent, and that equivalence carries graphs to isomorphic graphs. (This is what I meant in the matroids topic -- matroids have multiple definitions, and this seems to be a structured way to formalize that the definitions are equivalent.)

#### Kyle Miller (Aug 26 2020 at 20:19):

I've added formalizations of the first two theorems in Bollobas's book in this branch.

```
-- The type of all embedded cycles in a given graph
def cycles (G : α) := Σ (n : {n : ℕ // 3 ≤ n}), cycle_graph n.1 n.2 ↪g G
/--
Veblen 1912 (theorem 1 in book). Every vertex has even degree iff there is a
partition of the graph into edge-disjoint cycles.
-/
theorem edge_partition_cycles (G : α) [fintype (V G)] :
(∀ v : V G, degree v % 2 = 0) ↔ (∃ partition : set (cycles G),
∀ (e : edge_set G), !∃ (c : cycles G), c ∈ partition ∧
e ∈ set.image (embedding.map_edge_set c.2) set.univ) :=
sorry
/--
Mantel 1907 (theorem 2 in book). If a graph with n vertices and m edges satisfies
floor(n^2 /4) < m, then it contains a triangle.
-/
theorem has_triangle (G : α) [fintype (V G)] (h : (fintype.card (V G))^2 / 4 < (edge_finset G).card) :
nonempty (cycle_graph 3 (by linarith) ↪g G) :=
sorry
```

(Proving these will take a good amount of theory building still.)

For the first theorem, it's probably better to formalize cycles as being subgraphs that are isomorphic to a cycle graph, since with the current formulation every cyclic shift of a cycle is considered to be a different cycle. It's probably also good to formalize the idea of edge-disjoint partitions by subgraphs.

#### Kyle Miller (Aug 26 2020 at 20:32):

Changed it to be in terms of subgraphs that are cycles:

```
/--
Veblen 1912 (theorem 1 in book). Every vertex has even degree iff there is a
partition of the graph into edge-disjoint cycles.
-/
theorem edge_partition_cycles (G : α) [fintype (V G)] :
(∀ v : V G, degree v % 2 = 0) ↔ (∃ partition : set (subgraph G), (∀ G' ∈ partition, subgraph.is_cycle G') ∧
∀ (e ∈ edge_set G), !∃ (c : subgraph G), c ∈ partition ∧
e ∈ c.edge_set') :=
sorry
```

#### Alena Gusakov (Aug 30 2020 at 17:12):

so for the second implication here

```
lemma exists_path_eq_exists_walk : exists_path G = exists_walk G :=
begin
ext v w,
split,
intro h,
rcases h with ⟨n, ⟨f, hf⟩⟩,
split,
use n,
rw walk,
use f.to_homomorphism,
exact hf,
intro h,
rcases h with ⟨n, ⟨f, hf⟩⟩,
sorry,
end
```

would having `open_locale classical`

and then contracting edges between repeated vertices be a good strategy? i'm kind of stumped with this one

#### Alena Gusakov (Aug 30 2020 at 17:24):

also, i wonder if it might be useful to define some notion of the image of a graph homomorphism (unless i'm missing something that's already defined)

#### Kyle Miller (Aug 30 2020 at 17:26):

Feel free to make the lemma `noncomputable`

and use the `classical`

tactic for now. (I think `classical`

does the equivalent of `open_locale classical`

inside a proof, but I'll have to check)

#### Kyle Miller (Aug 30 2020 at 17:27):

I was imagining doing strong induction on the length of a walk. If a walk isn't a path, then there must be a repeated vertex, and then if you cut out the portion of the walk that occurred between the two vertices, the walk length gets shorter, hence it has a corresponding path by induction

#### Aaron Anderson (Aug 30 2020 at 17:28):

Do you even need `noncomputable`

if you're just using `classical`

inside a proof of a `Prop`

?

#### Kyle Miller (Aug 30 2020 at 17:28):

Probably not

#### Alena Gusakov (Aug 30 2020 at 17:31):

also, is it possible to like, "concatenate" functions? like make a new function out of two that you already have

#### Kyle Miller (Aug 30 2020 at 17:32):

The easiest-to-remember way is using lambda expressions

#### Kyle Miller (Aug 30 2020 at 17:32):

There's a whole bunch of function combinators in the `function`

namespace, too, but they don't seem to be used much

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

I tried using `combine`

in the definition of graph homomorphisms, but there were some type errors (I think because it involved Prop?) and I reconsidered. It even has fancy notation: `(f -[h]- g) x y = h (f x y) (g x y)`

#### Alena Gusakov (Aug 30 2020 at 17:52):

I don't know if `combine`

is what I'm looking for - it looks like it takes functions with two arguments

#### Alena Gusakov (Aug 30 2020 at 17:57):

I'm currently working on the concatenation of walks definition

#### Kyle Miller (Aug 30 2020 at 18:03):

`combine`

was just one of the many examples of combinators. i don't think it's useful for what you're doing.

for walks, this is gluing walks together, right? I'm not sure how gluing functions together works elsewhere in mathlib (how do the sheaf axioms glue functions? maybe that's to general to be useful here)

(When you said "contract" earlier, this might be where it'd be nice to actually have a quotient construction, using the expanded notion of graph homomorphism that was in the ncatlab article)

#### Alena Gusakov (Aug 30 2020 at 18:09):

I think I might've found a way to do it, does this look legit?

`to_fun := λ x, if x ≤ n then p.1.to_fun x else q.1.to_fun x,`

#### Alena Gusakov (Aug 30 2020 at 18:09):

context:

```
def walk.concat {n : ℕ} {m : ℕ} {v w u : V G} (p : walk G n u v) (q : walk G m v w) :
walk G (n + m) u w :=
{ val :=
{ to_fun := λ x, if x ≤ n then p.1.to_fun x else q.1.to_fun x,
map_adj' := sorry},
property := sorry, }
```

#### Alena Gusakov (Aug 30 2020 at 18:10):

wait no it's not cause `x`

is a vertex. I'll smooth that out I guess

#### Alena Gusakov (Aug 30 2020 at 18:12):

It seems like it would just be `to_fun := λ x, if x.1 ≤ n then p.1.to_fun x else q.1.to_fun x,`

#### Kyle Miller (Aug 30 2020 at 18:24):

I just realized that I have this partially defined in that file already, it's just too big and disorganized, sorry. Take a look at `walk_join`

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

It still lacks the proof that the result is a walk

#### Kyle Miller (Aug 30 2020 at 18:26):

(I'm assuming you're using `simple_graphs2`

based on the `exists_path_eq_exists_walk`

lemma)

#### Alena Gusakov (Aug 30 2020 at 18:29):

ohhh okay, ty

#### Alena Gusakov (Aug 30 2020 at 21:19):

we can't have paths on a single vertex right? that contradicts the definition of path

#### Alena Gusakov (Aug 30 2020 at 21:19):

should we have a lemma that explicitly states that?

#### Kyle Miller (Aug 30 2020 at 21:21):

Are zero-length paths not ok?

#### Kyle Miller (Aug 30 2020 at 21:21):

for compositions of walks, I thought those would be identity elements

#### Kyle Miller (Aug 30 2020 at 21:25):

walks themselves should form a category (I forget the exact terminology, maybe a dagger category? some kind of category where objects are self-dual and morphisms have duals). objects of the category are vertices of the graph, morphisms are walks from a vertex to another vertex, composition of walks is the concatenation of the walks, identities are the zero-length walks, and duals are parameterization reversal

#### Kyle Miller (Aug 30 2020 at 21:26):

once you have all this set up, then "there exists a morphism from x to y" is an equivalence relation on objects of the category

#### Kyle Miller (Aug 30 2020 at 21:27):

i.e., "there exists a walk of any length from x to y" is an equivalence relation.

#### Jalex Stark (Aug 30 2020 at 23:47):

I remember writing path code that used `path.empty v`

to be the empty path rooted at vertex v

#### Alena Gusakov (Sep 01 2020 at 15:04):

I'm having trouble working with `simple_graph_from_rel`

- specifically, I can't seem to figure out how to treat the vertices in the graph as the original objects they were defined as

#### Kyle Miller (Sep 01 2020 at 17:14):

One trick is you can use the `change`

tactic to change the type to whatever it's actually equal to.

Another is to add this missing lemma and use it to rewrite `V G`

:

```
lemma simple_graph_on.verts_eq (α : Type u) (G : simple_graph_on α) : V G = α := rfl
```

Yet another thing you could do, I think, is to use `erw`

rather than `rw`

.

#### Alena Gusakov (Sep 01 2020 at 18:43):

now i'm getting hung up on trying to coerce the numbers from `fin`

to `nat`

#### Alena Gusakov (Sep 01 2020 at 19:07):

should we add `nontrivial`

to the definition of connected?

#### Alena Gusakov (Sep 01 2020 at 19:08):

actually wait no, i guess it's trivially true for...the trivial case

#### Alena Gusakov (Sep 01 2020 at 19:10):

I'm trying to prove that in a nontrivial connected graph, every vertex has degree at least one

#### Alena Gusakov (Sep 01 2020 at 19:10):

but it's an absolute nightmare

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

I'm maybe behind the times on what definition of connected you're using, but perhaps it'd actually be easier to prove something more general: if you have a set of vertices, and no vertex in the set is adjacent to any vertex outside the set, then no vertex in the set is path-connected to any vertex outside the set

#### Alena Gusakov (Sep 01 2020 at 19:27):

My definition of connected is there exists a path between every vertex, but what I want to prove is that this means every vertex has at least one edge to it

#### Alena Gusakov (Sep 01 2020 at 19:29):

also currently having trouble proving that a subgraph of an acyclic graph is also acyclic

#### Aaron Anderson (Sep 01 2020 at 19:30):

Alena Gusakov said:

also currently having trouble proving that a subgraph of an acyclic graph is also acyclic

This should be at least pretty easy if we're using an embedding or subgraph definition of acyclic

#### Aaron Anderson (Sep 01 2020 at 19:31):

I'm going over to `simple_graphs2`

to check out what I've missed

#### Alena Gusakov (Sep 01 2020 at 19:31):

My current problem is when I say `is_acyclic (subgraph G)`

it doesn't recognize the subgraph as a simple graph

#### Alena Gusakov (Sep 01 2020 at 19:32):

sorry, I should've said I'm having trouble stating it

#### Aaron Anderson (Sep 01 2020 at 19:39):

One note: @Kyle Miller, I know that we have good reasons to doubt whether graph homomorphisms should be modeled with `rel_hom`

s, but I'm confused why `simple_graphs2`

uses `rel_iso`

to define isomorphisms, but doesn't use `rel_embedding`

to define embeddings, when I'm pretty sure the custom structure for embeddings has the exact same information as `rel_embedding`

#### Kyle Miller (Sep 01 2020 at 19:40):

I was going to change it back eventually. Your new PR wasn't there yet

#### Kyle Miller (Sep 01 2020 at 19:40):

though my embedding was a mono, vs regular mono

#### Aaron Anderson (Sep 01 2020 at 19:42):

Kyle Miller said:

though my embedding was a mono, vs regular mono

Ah right, sorry

#### Aaron Anderson (Sep 01 2020 at 19:49):

Anyway, the main advantage of a non-regular mono is that an arbitrary subgraph has an inclusion embedding

#### Aaron Anderson (Sep 01 2020 at 19:50):

Have we put that in lean yet?

#### Aaron Anderson (Sep 01 2020 at 19:50):

Because I'd imagine that's how you'd prove that a subgraph of an acyclic graph is acyclic

#### Aaron Anderson (Sep 01 2020 at 19:50):

or I guess you redefine/show that it's equivalent to nonexistent of a subgraph which is a cycle

#### Aaron Anderson (Sep 01 2020 at 19:51):

in which case you want to use transitivity of subgraph

#### Aaron Anderson (Sep 01 2020 at 20:02):

Alena Gusakov said:

I'm trying to prove that in a nontrivial connected graph, every vertex has degree at least one

I think I have a sketch if you're willing to use the `eqv_gen`

version, which is defined on `simple_graphs2`

, but the equivalence is currently `sorry`

#### Aaron Anderson (Sep 01 2020 at 20:03):

Say you have a set `S`

of vertices. Then you define an equivalence relation (actually a `setoid`

) where two vertices are equivalent iff they're both in `S`

or both not in `S`

.

#### Aaron Anderson (Sep 01 2020 at 20:04):

Then you want to use https://leanprover-community.github.io/mathlib_docs/data/setoid/basic.html#setoid.eqv_gen_le

#### Aaron Anderson (Sep 01 2020 at 20:06):

What this tells you is that if (for all `x y : V`

, `x ~g y`

implies `s.rel x y`

), where `s.rel`

is our new equivalence relation

#### Aaron Anderson (Sep 01 2020 at 20:07):

then `(eqv_gen G.adj) x y`

implies `s.rel x y`

#### Aaron Anderson (Sep 01 2020 at 20:07):

In other words, `x`

being connected to `y`

implies `x`

and `y`

are both in `S`

or both not in `S`

#### Kyle Miller (Sep 01 2020 at 20:08):

Aaron Anderson said:

Have we put that in lean yet?

This is in there:

```
def subgraph.map {x y : subgraph G} (h : x ≤ y) : x ↪g y
```

#### Aaron Anderson (Sep 01 2020 at 20:08):

This basically proves the lemma that if a set `S`

is closed under adjacency, that its vertices are not connected to outside vertices

#### Aaron Anderson (Sep 01 2020 at 20:09):

and to prove the exact theorem you wanted, @Alena Gusakov , the only remaining step is to let `S`

be a singleton. Then you find that if your singleton has degree 0, then it's closed under adjacency, so its one element is not connected to anything else, the contrapositive of what you wanted.

#### Aaron Anderson (Sep 01 2020 at 20:09):

Does that make sense?

#### Aaron Anderson (Sep 01 2020 at 20:14):

Kyle Miller said:

Aaron Anderson said:

Have we put that in lean yet?

This is in there:

`def subgraph.map {x y : subgraph G} (h : x ≤ y) : x ↪g y`

Ok, so then it should be relatively easy to prove at least that if a subgraph `S`

is NOT acyclic, then there is an embedding from a cycle graph into `S`

, which you can then compose with `subgraph.map`

to get an embedding from the cycle graph into the subgraph `top`

#### Aaron Anderson (Sep 01 2020 at 20:15):

Then it's a matter of showing that a graph isomorphic to an acyclic graph is acyclic, which can also work by composing embeddings

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

(Speaking of `eqv_gen G.adj`

, one thing @Alena Gusakov is helping with is showing that three different definitions of connectivity are equal: there exists a path between vertices, there exists a walk between vertices, and `eqv_gen G.adj`

.)

#### Alena Gusakov (Sep 01 2020 at 21:15):

yeah i've been poking around those lemmas, they're also a nightmare

#### Kyle Miller (Sep 01 2020 at 21:16):

I'm sure we'll figure out how to make it nice eventually :smile:

#### Kyle Miller (Sep 01 2020 at 21:35):

@Aaron Anderson I was considering replacing `f : G ↪g G'`

with `f : G →g G'`

having some kind of `mono`

instance, not sure the right name. It's can't be the category theory one, unfortunately, for some of the usual reasons. It would be nice if `injective`

were a typeclass here, because `injective f`

ends up being the correct notation, given the `has_coe_to_fun`

instance for graph homomorphisms.

#### Kyle Miller (Sep 01 2020 at 21:39):

I hesitate to do this, though, because `↪g`

seems to have been convenient so far to mean monomorphism since it extends `function.embedding`

so can find some immediate use in some cardinality arguments. However, it seems possible to define a cast of a function with a `mono`

-like instance to get a `function.embedding`

as needed.

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

I've reorganized the `simple_graphs2`

repository in a number of ways:

- Now a simple graph is merely a term of
`simple_graph`

. This is a bundled`simple_graph_on α`

term, for simple graphs with vertex type`α`

. - To give the terms of a type the structure of a simple graph, one implements
`has_coe_to_simple_graph`

. This gives you access to a new coercion arrow,`↟`

, which coerces graph-like things to simple graphs. This circumvents an issue where typeclass resolution won't assert two universe metavariables are equal, so`has_coe`

cannot work, but perhaps in a future version of Lean this will be resolved. Until then,`↟`

works well enough. - The code has been broken up into multiple files in https://github.com/leanprover-community/mathlib/tree/simple_graphs2/src/combinatorics/simple_graph so hopefully it's easier to follow now!
- Graph homomorphisms have been changed to use
`order.rel_iso`

exclusively. Monomorphisms are graph homomorphisms that implement the`simple_graph.hom.mono`

typeclass.

More about `↟`

: Of the many ways of organizing the simple graph library so that derived objects like subgraphs can be graphs, too, this seems to be the least-bad of all of them, and it has the benefit that, in the future, these arrows might disappear entirely. While you might need to specify universe variables, like `(G : simple_graph.{u})`

, so far I don't think I've been required to do this and have only done so for clarity in definitions.

When writing theorems about graphs in general, make sure to do it for terms of type `simple_graph`

. I think the way new types of graphs should work is, after defining the coercion, there needs to be a number of simp lemmas that specialize the generic definitions.

I've also added walks to the library. There are two ways they are represented, either as an inductive type that's essentially a list of adjacent vertices or as graph homomorphisms from path graphs into the graph. There is a proof that these are structurally equivalent (I visited `heq`

on the way, one of the circles of dependent typed hell, but that's all gone now, thankfully -- I have a special version of heterogeneous equality in the library still, which seems like it could be useful, but if it finds no use it'll be removed). The `walk`

type is essentially defining a category of walks, and it might be nice to actually give it a category structure, too.

**Warning:** not every definition makes sense and not every lemma with a `sorry`

is provable -- I also, unfortunately, haven't necessarily fixed all errors. The documentation is probably not up to date either!

#### Kyle Miller (Sep 21 2020 at 01:34):

(The coercion arrow, by the way, didn't change the code much. The previous version still was about coercions, and it was just a matter of changing who is responsible for inserting them, so to speak.)

#### Jalex Stark (Sep 22 2020 at 01:47):

Wow! I guess there's a lot of shovel-ready work for filling in sorries and carving off PRs to mathlib.

#### Jalex Stark (Sep 22 2020 at 01:48):

Do you think that the current definition of simple graphs in mathlib should be replaced or just given an instance of the new coercion arrow?

#### Jalex Stark (Sep 22 2020 at 01:51):

Kyle Miller said:

When writing theorems about graphs in general, make sure to do it for terms of type

`simple_graph`

. I think the way new types of graphs should work is, after defining the coercion, there needs to be a number of simp lemmas that specialize the generic definitions.

I guess this implies that you think the current theorem statements should be rejiggered to be about terms of type `simple_graph`

. But if we give the old simple graph type an instance of the new coercion arrow, then e.g. the proof of freek 83 in the mathlib archive won't need changes, except maybe to add some arrows?

#### Jalex Stark (Sep 22 2020 at 01:54):

I am like 8000 messages in the hole in terms of staying up to date on the server... have you advertised this stuff on #maths or are you waiting until more of the sorries and errors are fixed?

#### Jalex Stark (Sep 22 2020 at 01:55):

(small meta note, hopefully this is more helpful than annoying. if your big message were broken up into smaller messages, it would be easier to quote / emoji for more specific things)

#### Kyle Miller (Sep 22 2020 at 02:23):

Jalex Stark said:

(small meta note, hopefully this is more helpful than annoying. if your big message were broken up into smaller messages, it would be easier to quote / emoji for more specific things)

Like this? (Good point :smile:)

#### Jalex Stark (Sep 22 2020 at 02:26):

Kyle Miller said:

Graph homomorphisms have been changed to use

`order.rel_iso`

exclusively. Monomorphisms are graph homomorphisms that implement the`simple_graph.hom.mono`

typeclass.

I guess @Aaron Anderson will be happy to hear this

#### Kyle Miller (Sep 22 2020 at 02:26):

The conversion to using `simple_graph`

is almost entirely just removing vertex type arguments and then doing `v : V G`

. It's pretty much painless.

#### Jalex Stark (Sep 22 2020 at 02:27):

What do you think the next PR from this branch should be?

#### Kyle Miller (Sep 22 2020 at 02:29):

It would be nice to sort out the coercion. There's a little discussion in #Is there code for X? (the auto-coercions thread) about how `has_coe`

is almost but not quite sufficient, but it seems fixing this involves modifying Lean itself.

#### Kyle Miller (Sep 22 2020 at 02:29):

But maybe making the arrow a local notation is good enough for now.

#### Kyle Miller (Sep 22 2020 at 04:00):

Jalex Stark said:

What do you think the next PR from this branch should be?

Most of `simple_graph/basic.lean`

seems good, except for the incomplete stuff about graph operations. Some simp lemmas relating `simple_graph_on`

to `simple_graph`

might not make sense. Also `simple_graph_from_rel_adj`

can probably wait.

The definitions in `simple_graph/hom.lean`

seem fine, but the lemmas should be reviewed since the api is underutilized and seems somewhat incomplete.

`simple_graph/subgraph.lean`

seems good, except for things about cycles and maybe induced graphs. Cardinality results should be reviewed -- there's no application of them yet so the design might not be good.

`simple_graph/simple_graph_on.lean`

is fine enough. It could certainly be expanded, but it at least has a `bounded_lattice`

instance.

`simple_graph/degree_sum.lean`

is close, but I think it can still be simplified a lot given a person sufficiently competent with `big_operators`

. It also would be nice to have an explicit handshake lemma.

#### Kyle Miller (Sep 22 2020 at 04:01):

`simple_graph/adj_matrix.lean`

is just the current `adj_matrix.lean`

but modified to use this new `simple_graph`

type.

#### Alena Gusakov (Oct 11 2020 at 22:17):

I think I completed the edge contraction definition

#### Alena Gusakov (Oct 11 2020 at 22:17):

I also created an edge deletion definition

#### Alena Gusakov (Oct 11 2020 at 22:17):

I tried messing around with paths and walks after that, as well as trees, but really didn't get anywhere

#### Alena Gusakov (Oct 11 2020 at 22:18):

I managed to prove the first direction of the statement `map_rel_iff'`

in `fin.flip.invol`

#### Alena Gusakov (Oct 11 2020 at 22:19):

but the other direction has me stumped

#### Bhavik Mehta (Oct 11 2020 at 22:33):

Since it's an involution can't you just use the first direction and some equivalence properties?

#### Bhavik Mehta (Oct 11 2020 at 22:33):

I might be misremembering what you're trying to prove though

#### Alena Gusakov (Oct 12 2020 at 01:55):

i think i got stuck trying to do exactly that

#### Alena Gusakov (Oct 12 2020 at 02:59):

Trying to figure out how to define matchings currently. I'm thinking some structure like

```
structure matching_on (G : simple_graph) :=
(disjoint : )
```

#### Alena Gusakov (Oct 12 2020 at 02:59):

where disjoint is the property that the edges are disjoint

#### Alena Gusakov (Oct 12 2020 at 03:00):

but I'm not quite sure how to get there

#### Alena Gusakov (Oct 12 2020 at 03:00):

maybe a `class`

? something like

```
class matching (M : set (sym2 (V G))) :=
(disjoint : ∀ e f ∈ M, ∀ v : V G, v ∈ e → v ∉ f)
```

#### Kyle Miller (Oct 13 2020 at 06:58):

A class seems like a reasonable approach. I haven't tested it, but maybe this definition?

```
class matching (M : set (sym2 (V G))) :=
(sub_edges : M ⊆ E G)
(disjoint : ∀ (e f ∈ M) (v : V G), v ∈ e → v ∈ f → e = f)
class perfect_matching (P : set (sym2 (V G))) extends matching P :=
(cover : ∀ v : V G, ∃ e ∈ P, v ∈ e)
```

#### Kyle Miller (Oct 13 2020 at 07:02):

There are upsides and downsides to classes for this, so you might need to experiment. Structures would be fine too, but if you had a perfect matching, you'd need to use its `to_matching`

function to turn it into a `matching`

when necessary.

Another thing to consider is predicates

```
def matching {G : simple_graph} (M : set (sym2 (V G)) := M ⊆ E G ∧ ∀ (e f ∈ M) (v : V G), v ∈ e → v ∈ f → e = f
def perfect_matching {G : simple_graph} (P : set (sym2 V G)) := matching P ∧ ∀ v : V G, ∃ e ∈ P, v ∈ e
```

but a downside here is that you can't access the sub-properties as easily.

#### Alena Gusakov (Oct 13 2020 at 21:45):

ah yeah thank you, the class definition you gave makes more sense

#### Alena Gusakov (Oct 13 2020 at 21:46):

forgot to add the part where the edges come from G

#### Bhavik Mehta (Oct 14 2020 at 12:55):

I feel like you want a structure rather than a class (they can also extend) since you might want to consider multiple matchings on the same set

#### Kyle Miller (Oct 14 2020 at 18:11):

I was thinking that too, but then I realized Alena's class was the matching itself, and all the fields are just propositions so the class is a subsingleton. It seems like it's similar to using `mono`

.

#### Bhavik Mehta (Oct 14 2020 at 21:16):

I think `mono`

should be a proposition though :) I think that change is gonna happen in the category theory library as soon as someone actually puts in the effort to make it

#### Alena Gusakov (Oct 17 2020 at 16:38):

Is there something we can do about the builds failing?

#### Alena Gusakov (Nov 23 2020 at 14:36):

I've been away for a bit so I'm a bit out of the loop, are we still trying to go with the definition `simple_graph_on`

where we turn it into `simple_graph`

later? Just looking at the file in mathlib and it doesn't seem to be the case right now

#### Alena Gusakov (Nov 23 2020 at 14:40):

If we are going to do that then I can start slicing off `simple_graphs2`

into PRs

#### Alena Gusakov (Nov 23 2020 at 14:50):

Btw I think when I was initially trying to figure things out I muddled up a lot of the code in simple_graphs2 so I'm sorry if that caused anyone to step back

#### Jalex Stark (Nov 24 2020 at 22:47):

I think the `simple_graph_on`

proposal is still the best one, and I'd support you in making PRs about it

#### Aaron Anderson (Nov 25 2020 at 00:19):

I’d be happy to help a PR to refactor to `simple_graph_on`

etc. if someone else gets it started

#### Aaron Anderson (Nov 25 2020 at 00:21):

(Mostly I’m volunteering to translate over the friendship graph material)

#### Alena Gusakov (Nov 25 2020 at 00:40):

~~I think we pretty much do have everything refactored~~ ah wait, forgot that we need to catch up to all of the mathlib changes since september

#### Alena Gusakov (Nov 25 2020 at 00:40):

Like, I didn't even need to do the work, it's already there in simple_graphs2

#### Alena Gusakov (Nov 25 2020 at 00:40):

But I'll pull the file into its own PR

#### Alena Gusakov (Dec 02 2020 at 20:40):

So I managed to adapt some of the lemmas and definitions from simple_graphs2 into a branch that doesn't rely on `simple_graph_on`

#### Alena Gusakov (Dec 02 2020 at 20:45):

@Bhavik Mehta just gonna pull you into this conversation cause I'm probably not going to be able to explain why I wasn't using `simple_graph_on`

very well

#### Alena Gusakov (Dec 02 2020 at 20:46):

Also @Eric Wieser

#### Aaron Anderson (Dec 02 2020 at 20:49):

I think it still makes sense to eventually have a PR that adds no new features, and just converts to `simple_graph_on`

, because I think that conversion will cause enough discussion by itself.

#### Aaron Anderson (Dec 02 2020 at 20:50):

You could always have another PR that is blocked by that `simple_graph_on`

PR, adding features on top of `simple_graph_on`

, if you think that those features would be a good demonstration of why `simple_graph_on`

is good.

#### Alena Gusakov (Dec 02 2020 at 20:55):

So far I haven't had any trouble switching everything from simple_graphs2 to the definition we currently have in mathlib

#### Alena Gusakov (Dec 02 2020 at 20:56):

The one annoying thing is not using `simple_graph_on`

means we don't have the special notation for adjacency

#### Alena Gusakov (Dec 02 2020 at 20:56):

But if I do find problems/advantages I'll try to do that

#### Kyle Miller (Dec 02 2020 at 21:20):

Alena Gusakov said:

So far I haven't had any trouble switching everything from simple_graphs2 to the definition we currently have in mathlib

We haven't gotten to subgraphs in mathlib yet is why :smile:

I think it's better to leave it as `simple_graph`

for now and then do the refactor later when a `simple_graph_on`

is clearly needed -- and since putting it off might cause more work, I'm willing to do it when it comes to that. (I think it will actually be less work long-term to not change it now.)

#### Alena Gusakov (Dec 02 2020 at 21:21):

Got it, I'll try to do subgraphs in the next PR (assuming this first one gets approved)

Last updated: May 08 2021 at 22:13 UTC