## Stream: general

### Topic: Conventions for graph defs

#### Aaron Anderson (Jul 24 2020 at 05:08):

While working on #3458, @Kyle Miller and I had a lot of discussion about some defining and naming conventions in graph theory, and I'd like to get some more opinions.

#### Aaron Anderson (Jul 24 2020 at 05:13):

• For relations such as the edge relation or the incidence of vertices on edges, I prefer a Prop-valued definition (V → V → Prop), and he prefered a set-valued definition (V → set V). These are definitionally equal, but does it matter which we use?
• It is also useful to have finset-valued versions, given some fintype instances. At that point, there are several versions of the same thing floating around, and they all have to have distinct names.

#### Aaron Anderson (Jul 24 2020 at 05:14):

As building out more combinatorics will have a lot of variations on these themes, I'd like to have a consistent guideline. Also, probably there are actually analogies in mathlib already, but I haven't identified them yet. I think my preference is the following, but this just lines up with what I've found convenient this summer:

#### Aaron Anderson (Jul 24 2020 at 05:19):

• The original definition is Prop-valued, and is given as simple a name as possible, like G.adj v w or v ~[G] w
• To get the corresponding set, we use {w | G.adj v w} or similar, and it doesn't get a separate name
• To get the finset, which may require some bundled proofs and instances, we use the full name, like G.neighbors v

#### Aaron Anderson (Jul 24 2020 at 20:56):

Tagging @Scott Morrison just because you had useful reviews asking for consistency

#### Scott Morrison (Jul 24 2020 at 22:55):

As I started saying in my review, while V → V → Prop and V → set V are definitionally equal, it's best not to take constant advantage of that, as it ends up being hard to use: the set API expects you to "stay in the world of set" most of the time.

#### Scott Morrison (Jul 24 2020 at 22:56):

To me V → V → Prop feels like the safer choice because it makes the connections with other types of graphs (and categories) more transparent.

Last updated: Aug 03 2023 at 10:10 UTC