Zulip Chat Archive

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