## Stream: graph theory

#### Alex Zhang (Sep 05 2021 at 19:25):

I have written more things about adjacency matrices as a part of my project mentioned here: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Contribute.20a.20project, including an adjacency matrix induces a graph,
and I am going to PR them.
When I was writing those stuff, I was thinking, should we change the condition [semiring R] for simple_graph.adj_matrix to [mul_zero_one_class α] [nontrivial α] or a weaker one [mul_zero_one_class α] (or even [has_zero α] [has_one α]), as the essence of an adjacency matrix is it has two distinguishable elements called 0 and 1 (or true and false).

#### Kyle Miller (Sep 05 2021 at 19:27):

Is the code you're PRing available anywhere yet? I'd like to take a look

#### Kyle Miller (Sep 05 2021 at 19:28):

Seems reasonable generalizing adj_matrix to the weakest condition needed to define it.

#### Alex Zhang (Sep 05 2021 at 19:28):

I can give you the link to my project. Please see the file srg.lean(some parts are still under construction, but which are all about srg).

#### Alex Zhang (Sep 05 2021 at 19:30):

https://github.com/l534zhan/my_project @Kyle Miller

#### Alex Zhang (Sep 05 2021 at 19:32):

Please let me know if you have any thoughts!

#### Alex Zhang (Sep 05 2021 at 19:39):

I think it might be reasonable to PR my code after we can determine what the conditions are we want to have for simple_graph.adj_matrix.

#### Kyle Miller (Sep 05 2021 at 19:40):

I'd recommend that adj_matrix be a structure, not a class. Rewriting tends to make Lean "forget" the association between a term and a class, and in practice you'll probably want to rewrite matrices

#### Kyle Miller (Sep 05 2021 at 19:41):

I think I see a typo in compl. That should be i = j, right?

#### Alex Zhang (Sep 05 2021 at 19:45):

Thanks for pointing the typo out!
As adj_matrix is a proposition and because of "proof-irrelevant", won't it be better to make it a class just like other algebraic structures group etc.?

#### Kyle Miller (Sep 05 2021 at 19:46):

Regarding classes: there was a time when things like subgroups were sets that had an associated is_subgroup class. I wasn't around then, but it seems that it caused many complications, and what happened is, eventually, subgroups were "bundled"

#### Kyle Miller (Sep 05 2021 at 19:47):

adj_matrix is more of a subtype of matrices, so more like a subgroup than a group

#### Kyle Miller (Sep 05 2021 at 19:47):

but it's not an algebraic structure, so it's not that good of a comparison

#### Kyle Miller (Sep 05 2021 at 19:50):

Here's how it would look bundled (mostly untested):

structure adj_matrix (α : Type*) (I : Type*) [fintype I] [mul_zero_one_class α] [nontrivial α] :=
(A : matrix I I α)
(zero_or_one : ∀ i j, (A i j) = 0 ∨ (A i j) = 1 . obviously)
(sym : A.is_sym . obviously)
(loopless : ∀ i, A i i = 0 . obviously)


#### Alex Zhang (Sep 05 2021 at 19:50):

Yeah, it's more like a "subgroup" than a "group".

#### Kyle Miller (Sep 05 2021 at 19:51):

The downside is you'd need to write a lot of boilerplate to use this as a matrix, so it seems easier to me to just have a Prop-valued structure

#### Alex Zhang (Sep 05 2021 at 19:51):

The downside of defining as a "class" or a "structure"?

#### Kyle Miller (Sep 05 2021 at 19:52):

The downside of the definition I just gave

#### Alex Zhang (Sep 05 2021 at 19:53):

Yeah. I guess I don't want the matrix itself to be a field...

#### Kyle Miller (Sep 05 2021 at 19:53):

You can make it work with coercions, but I expect it wouldn't be so nice to work with

#### Alex Zhang (Sep 05 2021 at 19:54):

How about just using my original definition or merely change "class" to "structure" both are just a proposition?

#### Kyle Miller (Sep 05 2021 at 19:56):

Yeah, my original suggestion was to change class to structure (and remove the []'s). Maybe go for has_one and has_zero for the typeclasses, too.

#### Alex Zhang (Sep 05 2021 at 19:57):

Sorry, what do you mean by "Maybe go for has_one and has_zero for the typeclasses, too"?

#### Kyle Miller (Sep 05 2021 at 19:57):

Instead of [mul_zero_one_class α] [nontrivial α], perhaps do [has_zero α] [has_one α]

Ah, right!

#### Alex Zhang (Sep 05 2021 at 19:58):

Why do you suggest removing []?

#### Kyle Miller (Sep 05 2021 at 19:58):

I don't expect them to be useful once it's a structure, that's all.

#### Alex Zhang (Sep 05 2021 at 20:00):

OK. I will have a look to see if they are useful.

#### Alex Zhang (Sep 05 2021 at 20:01):

I didn't quite get why we want to change "class" to "structure", could you please explain a little bit more?

#### Kyle Miller (Sep 05 2021 at 20:02):

I checked, the []'s had no effect. This is what I'd recommend (along with renaming sym to symm -- eventually simple_graph will use symm too):

structure adj_matrix [has_zero α] [has_one α] (A : matrix I I α) : Prop :=
(zero_or_one : ∀ i j, A i j = 0 ∨ A i j = 1 . obviously)
(symm : A.is_symm . obviously)
(loopless : ∀ i, A i i = 0 . obviously)


#### Kyle Miller (Sep 05 2021 at 20:04):

The issue with using a class is that it depends on the typeclass search system. Let's say A = B and you have an instance [adj_matrix A]. If you rewrite all A's in an expression with B, then B is no longer an adj_matrix since [adj_matrix B] is likely not an instance.

#### Alex Zhang (Sep 05 2021 at 20:05):

I thought "class" can be applied to all "bundled propositions" to avoid use "and".

#### Kevin Buzzard (Sep 05 2021 at 20:06):

It can, but that doesn't mean it's the correct design decision. The same is true for structures.

#### Kyle Miller (Sep 05 2021 at 20:06):

My rule of thumb: use typeclasses when the things aren't going to be rewritten, use structures when they are. You're going to be doing calculations with matrices (that is, they're going to be rewritten) so use structures.

#### Kyle Miller (Sep 05 2021 at 20:07):

By the way, class is short for @[class] structure. They're both structures, it's just a matter of whether they're going to participate in this automatic typeclass system.

#### Alex Zhang (Sep 05 2021 at 20:07):

Do you think I should PR to week the definition of simple_graph.adj_matrix first?

#### Alex Zhang (Sep 05 2021 at 20:08):

I will try to see if we can use has_zero α] [has_one α] there.

#### Kyle Miller (Sep 05 2021 at 20:08):

I think it's fine to do it in one PR (relax the typeclass constraints, introduce matrix.adj_matrix, and define to_graph), but feel free to break it up into two PRs if you want.

#### Alex Zhang (Sep 05 2021 at 20:09):

I think I might do one (as I am very lazy).

#### Kyle Miller (Sep 05 2021 at 20:10):

I'm saying this because it's probably ~50 lines, and I at least know what you're up to, so I'll be expecting it (make sure to add me as a reviewer)

#### Alex Zhang (Sep 05 2021 at 20:11):

Sure, I will add you as a reviewer. Should I create a new file for matrix.adj_matrix? @Kyle Miller

#### Kyle Miller (Sep 05 2021 at 20:12):

Hmm, good question. The lazy option is to put it in combinatorics/simple_graph/adj_matrix.lean in the matrix namespace. That seems thematically appropriate

#### Alex Zhang (Sep 05 2021 at 20:13):

Sounds good, Staring now!

#### Kyle Miller (Sep 05 2021 at 20:17):

(Here's another case study: docs#set.finite could have used the typeclass system, similar to how fintype works, but because sets are rewritten all the time it works out better to have it not use typeclasses.)

#### Kyle Miller (Sep 05 2021 at 20:18):

Suggestion: for to_graph make sure to have it be matrix.adj_matrix.to_graph, and make the matrix argument be implicit.

That way, if h : adj_matrix A, you can write h.to_graph to get the corresponding simple graph.

#### Yaël Dillies (Sep 05 2021 at 20:18):

Kyle Miller said:

(Here's another case study: docs#set.finite could have used the typeclass system, similar to how fintype works, but because sets are rewritten all the time it works out better to have it not use typeclasses.)

Yeah but in that case finset kind of is the bundled version of set.finite.

#### Kyle Miller (Sep 05 2021 at 20:19):

Indeed, that's how I've tended to think about finset, but amusingly everything is all backwards since set.finite goes through nonempty (fintype s), which goes through finset set.univ!

#### Alex Zhang (Sep 05 2021 at 20:21):

Do we really often want to rewrite a specific adjacency matrix? I can't think of such a case immediately.

#### Kevin Buzzard (Sep 05 2021 at 20:24):

If only finset was the bundled version of set.finite -- then it would be nonconstructive and I'd be able to use it :-)

#### Kyle Miller (Sep 05 2021 at 20:24):

One example: you have a graph written as an edge-disjoint-union of subgraphs, and you want to relate the adjacency matrix of the graph to the sum of the adjacency matrices of the subgraphs.

#### Alex Zhang (Sep 05 2021 at 20:27):

It's frustrating that "typeclass inference" isn't "rewrite" compatible.

#### Kyle Miller (Sep 05 2021 at 20:28):

There are many things in mathlib that depend on this exact quality.

#### Kyle Miller (Sep 05 2021 at 20:29):

def foo (a : Type*) := a is a technique to make mathlib forget all the typeclasses associated with a type, since by default it can't see through even this basic level of indirection

#### Kyle Miller (Sep 05 2021 at 20:30):

Here's one: docs#opposite

#### Kyle Miller (Sep 05 2021 at 20:33):

However, even if a adj_matrix class could survive rewrites, it seems to be more useful in practice to have either bundled objects (so a structure containing the matrix along with the proof it's an adjacency matrix) or having explicit proof objects that you pass around (the Prop-valued structure). It seems to be easier to write proofs because you can more easily refer to specific subterms in a formula without needing to write them out in full.

#### Alex Zhang (Sep 05 2021 at 20:52):

Yeah. I think we can only do things manually like this:

class test (a : Type*) : Prop := (f : true)

example {a b : Type*} [test a] (h : a = b) : test b :=
begin
rw h at *,
resetI,
apply_instance,
end


#### Kevin Buzzard (Sep 05 2021 at 21:11):

[In this particular case you can get away with

example {a b : Type*} [test a] (h : a = b) : test b :=
begin
subst h,
apply_instance,
end


]

#### Alex Zhang (Sep 06 2021 at 00:13):

@Kyle Miller I have PRed and invited you to review. #9021
Is there any maintainer who I should invite to be a reviewer?

#### Kyle Miller (Sep 06 2021 at 17:09):

It's specialized to just simple graphs (more general would be symmetric matrices with non-negative integer entries), so I'm wondering if matrix.is_adj_matrix isn't the right name -- I don't have any good ideas for alternatives, so I'm willing to go with it for now.

#### Bhavik Mehta (Sep 06 2021 at 17:16):

I think using this definition is fine for now - I agree a more general version would be better, but I'd prefer to have a special case than no case. For to_graph, it feels tempting to me to not make it partial; ie construct a graph from any matrix (eg by saying there's an edge iff the vertices are different and the entry is nonzero, on second thoughts this might not be symmetric, so maybe not) and have the is_adj_matrix condition on the relevant lemmas. This is more consistent with the usual pattern of definitions in mathlib, and we can have a docstring saying the intended case is where the matrix is an adjacency matrix

#### Kyle Miller (Sep 06 2021 at 17:19):

Yeah, to_graph could use docs#simple_graph.from_rel

Though, it's pleasing that you can write h.to_graph to get the graph for the adjacency matrix.

Last updated: Dec 20 2023 at 11:08 UTC