IsRegularOfDegree without DecidableRel

Stream: graph theory

[Iván Renison]

Hi, if I write this code:

import Mathlib
open SimpleGraph

abbrev V := Fin 5

def G : SimpleGraph V := sorry

theorem regular : G.IsRegularOfDegree 5 := by sorry

I get this error:

failed to synthesize instance of type class
G.LocallyFinite

However if I define instance : DecidableRel G.Adj it works.
However, it should be possible to work with IsRegularOfDegree even if G.Adj is not comutable, and, G.LocallyFinite is obvious from Fintype V. Do you know if there is any solution to this?

Also I think it should be possible to use IsSRGWith with out DecidableRel G.Adj, but it is needed as part of the definition, I don't know why

[Yaël Dillies]

The issue IMO stems from docs#SimpleGraph.degree being computable

[Snir Broshi]

Oh wow, I'm just now finishing up removing this from degrees

[Snir Broshi]

PR will be up soon, it solves this issue

[Iván Renison]

Ok, great! Thank you

[Snir Broshi]

Also, docs#SimpleGraph.IsRegularOfDegree.top already exists
I somehow confused the graph being on Fin with it being the complete graph, sorry

[Snir Broshi]

Snir Broshi said:

PR will be up soon

Opened #33501, it removes LocallyFinite from IsRegularOfDegree

[Snir Broshi]

Not sure what to do about the import increase :hurt:
Added imports for Data.ENat.Lattice and Data.Set.Card in SimpleGraph.Finite, which seem reasonable to me but they causes a big chain reaction of import increases

[Vlad Tsyrklevich]

do we need ENat for defining IsRegularOfDegree? It's still only using Nat. We don't need to define IsRegularOfDegree using edegree if we keep the locally finite assumption

[Vlad Tsyrklevich]

Defining it using edegree is odd anyway given that you can't use IsRegularOfDegree for infinite graphs anyway.

[Vlad Tsyrklevich]

Iván Renison said:

I get this error:

It works on the current lean playground? #synth G.LocallyFinite returns something in CategoryTheory though.

[Snir Broshi]

Vlad Tsyrklevich said:

do we need ENat for defining IsRegularOfDegree? It's still only using Nat. We don't need to define IsRegularOfDegree using edegree if we keep the locally finite assumption

But the point of the discussion above is to remove the locally finite assumption.

Vlad Tsyrklevich said:

Defining it using edegree is odd anyway given that you can't use IsRegularOfDegree for infinite graphs anyway.

Why not? The Hasse graph of ℤ (infinite path graph) is 2-regular.
Assuming you meant non-locally-finite, then I agree but as OP notes it's annoying to have to provide both Fintype for the neighbors of every vertex and then also a degree proof.

[Snir Broshi]

docs#SimpleGraph.dist and docs#SimpleGraph.diam are defined using ENat, and I really like that approach.
Also it's useful for me to be able to talk about degrees being infinite.

[Snir Broshi]

Vlad Tsyrklevich said:

It works on the current lean playground? #synth G.LocallyFinite returns something in CategoryTheory though.

To solve the specific Finite issue, we can add:

noncomputable instance {V : Type*} {G : SimpleGraph V} [Finite V] : G.LocallyFinite := by
  classical
  have := Fintype.ofFinite V
  infer_instance

[Aaron Liu]

don't make it a global instance I think

[Vlad Tsyrklevich]

Vlad Tsyrklevich said:

Assuming you meant non-locally-finite, then I agree but as OP notes it's annoying to have to provide both Fintype for the neighbors of every vertex and then also a degree proof.

Yes, sorry: I should have said infinite-degree graphs. To prove something is regular with degree n, you will anyways need to show the degree is finite so you get a local finiteness proof for free, no?

[Vlad Tsyrklevich]

I'm not against ENat (I like being able to work with infinite graphs as well), but the definition of edegree could then just live in a separate file. In this case, we also have a way of talking about infinite degree (e.g. \not LocallyFinite) though you don't get any algebraic properties out of it like you do with ENat. I'm not sure how often you want addition or multiplication versus just max though?

[Snir Broshi]

Vlad Tsyrklevich said:

To prove something is regular with degree n, you will anyways need to show the degree is finite so you get a local finiteness proof for free, no?

But you can't even state the theorem without first adding an instance of LocallyFinite. This may be fixed if we change IsRegularOfDegree to ∃ (_ : G.LocallyFinite), ∀ v, G.degree v = k

[Snir Broshi]

Vlad Tsyrklevich said:

I'm not against ENat (I like being able to work with infinite graphs as well), but the definition of edegree could then just live in a separate file.

Okay, so do you support changing degree to drop the Fintype? Using Set.ncard instead of Finset.card?

[Vlad Tsyrklevich]

Snir Broshi said:

Okay, so do you support changing degree to drop the Fintype? Using Set.ncard instead of Finset.card?

No strong opinion one way or the other.

[Kevin Buzzard]

Aaron Liu said:

don't make it a global instance I think

Oh wow it's not a Prop! We should rename SimpleGraph.LocallyFinite to SimpleGraph.LocallyFintype and then add the correct proposition SimpleGraph.LocallyFinite .