adj_matrix

Stream: graph theory

[Alex Zhang]

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).

https://leanprover-community.github.io/mathlib_docs/combinatorics/simple_graph/adj_matrix.html#simple_graph.adj_matrix

[Kyle Miller]

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

[Kyle Miller]

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

[Alex Zhang]

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]

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

[Alex Zhang]

Please let me know if you have any thoughts!

[Alex Zhang]

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]

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]

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

[Alex Zhang]

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]

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]

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

[Kyle Miller]

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

[Kyle Miller]

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]

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

[Kyle Miller]

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]

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

[Kyle Miller]

The downside of the definition I just gave

[Alex Zhang]

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

[Kyle Miller]

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

[Alex Zhang]

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

[Kyle Miller]

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]

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

[Kyle Miller]

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

[Alex Zhang]

Ah, right!

[Alex Zhang]

Why do you suggest removing []?

[Kyle Miller]

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

[Alex Zhang]

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

[Alex Zhang]

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

[Kyle Miller]

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]

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]

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

[Kevin Buzzard]

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

[Kyle Miller]

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]

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]

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

[Alex Zhang]

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

[Kyle Miller]

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]

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

[Kyle Miller]

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]

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

[Alex Zhang]

or add in the file https://leanprover-community.github.io/mathlib_docs/combinatorics/simple_graph/adj_matrix.html?

[Kyle Miller]

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]

Sounds good, Staring now!

[Kyle Miller]

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

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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

[Kyle Miller]

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

[Kyle Miller]

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]

Here's one: docs#opposite

[Kyle Miller]

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]

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]

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

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

@Bhavik Mehta Do you have any thoughts about this definition for an adjacency matrix?

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]

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]

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.