(Undirected) hypergraphs

Stream: graph theory

[Evan Walter Clark Spotte-Smith]

Hello there.

I'm very new to Lean (and mathematics - I'm a materials scientist by training), and I saw that, while there are a couple of graph implementations in mathlib, there weren't any implementations of hypergraphs. I figured it could be a good project to try to formalize hypergraphs, getting to know Lean better and also potentially creating something useful for my research (hypergraphs happen to be quite useful for the area of chemistry that I work on).

I've got an initial implementation and some properties worked out. Before I got deeper on proofs, conversions between types, etc., I thought I should get some feedback from folks who actually know what they're doing.

The full code can be found here. My basic definition, which is heavily inspired by @Peter Nelson and Jun Kwon's work on Mathlib.Combinatorics.Graph, is below:

structure Hypergraph (α β : Type*) where
  /-- The vertex set -/
  vertexSet : Set α
  /-- The hyperedge predicate: a set of vertices `s : Set α` is contained in a hyperedge `e`. -/
  IsHyperedge : β → Set α → Prop
  /-- Incidence predicate stating that a vertex `x` is a member of hyperedge `e` -/
  IsIncident : α → β → Prop := fun x e => ∃ s, IsHyperedge e s ∧ x ∈ s
  /-- The hyperedge set -/
  hyperedgeSet: Set β := {e | ∃ s ⊆ vertexSet, IsHyperedge e s}
  /-- A hyperedge contains only one set of vertices -/
  eq_of_isHyperedge_of_isHyperedge : ∀ ⦃e s t⦄, IsHyperedge e s → IsHyperedge e t → s = t
  /-- If some vertex `x` is incident on an edge `e`, then `x ∈ V` -/
  mem_of_isIncident : ∀ ⦃e x⦄, IsIncident x e → x ∈ vertexSet
  /-- Vertices can be incident on a hyperedge `e` if and only if `e` is in the hyperedge set. -/
  -- TODO: should this be based on IsIncident?
  -- If so, then we'd be definine hyperedges to be non-empty
  hyperedge_mem_iff_exists_isHyperedge :
    ∀ e, e ∈ hyperedgeSet ↔ ∃ s ⊆ vertexSet, IsHyperedge e s := by exact fun _ ↦ Iff.rfl
  /--
  If a set of vertices `s` is contained in a hyperedge `e`, then all elements `x ∈ s` are
  incident on `e` and all elements in `V \ s` are not incident on `e`
  -/
  isIncident_and_not_isIncident_of_isHyperedge :
    ∀ ⦃e s⦄, IsHyperedge e s → (∀ x ∈ s, IsIncident x e) ∧ (∀ y ∈ vertexSet \ s, ¬IsIncident y e)

[Snir Broshi]

(disclaimer: I'm also new to Lean)
Looks cool, and seems based on the existing Graph, but I'm not sure what's the advantage of all these axioms as opposed to:

structure Hypergraph (V : Type*) where
  hyperedgeSet : Set (Set V)

or maybe

structure Hypergraph (α : Type*) where
  vertexSet : Set α
  hyperedgeSet : Set (Set α)

which is what it looks to me you're trying to model with IsHyperedge and IsIncident.
Maybe the authors of the relatively new Graph (Peter Nelson & Kyle Miller) can explain the advantages which I'm not seeing (not sure if tagging people is considered rude or not)
This is the original discussion about Multigraph

[Snir Broshi]

What do you think of this alternate version of the last axiom:

  isIncident_and_not_isIncident_of_isHyperedge :
    ∀ ⦃e s⦄, IsHyperedge e s → s = { x ∈ vertexSet | IsIncident x e }

It's almost equivalent, the current version allows s to have elements which are not vertices

[Evan Walter Clark Spotte-Smith]

Originally, I had a similar definition:

structure Hypergraph (α β : Type*) where
  vertexSet : Set α
  hyperedgeSet : Set β
  IsIncident : α → β → Prop

(your definition is even simpler, which is nice in a sense).

First, why two types (α and β). This comes down to flexibility (maybe a user has a separate object they want to treat as a hyperedge, for some reason) but also downstream applications. Often, in hypergraph theory we want to think about an incidence matrix. Having two types makes conversion into a matrix (which needs two index types) very natural.

In terms of why I included so many axioms, this is a big part of why I wanted to ask here for advice. Graph uses this approach (I think) with the logic that it makes creating a hypergraph initially more annoying but makes downstream proofs more facile. But DiGraph and SimpleGraph take an approach more similar to what you suggest. I'm not knowledgable enough to be confident that one is better than the other.

[Evan Walter Clark Spotte-Smith]

Does my current definition allow non-vertex elements? Since left_mem_of_isIncident... I guess you mean that, with that one axiom alone, that isn't guaranteed, which is valid.

[Evan Walter Clark Spotte-Smith]

I definitely like that your version of isIncident_and_not_isIncident_of_isHyperedge is more concise. Given the structure, though, I think it'd be better named something like isIncident_of_isHyperedge or some such.

[Ammar Husain]

Do appreciate being able to label the hyperedges with extra data in addition to what it is incident to especially if want multiple with the same incidence distinguished by those labels

[Snir Broshi]

Oh labeling sounds useful, and it also allows "parallel" hyperedges.
In that case I like the vertexSet + hyperedgeSet + IsIncident definition.
Two questions I have about it:

1. Set α is actually α → Prop, so toHyperedge : β → Set α is equivalent to IsIncident : α → β → Prop but might be more readable: a hyperedge is a set of vertices, like in the literature
2. Since sets can be types (they're auto-coerced to Subtype) why separate α from vertexSet and β from hyperedgeSet? We can:

structure Hypergraph where
  vertices : Type*
  hyperedges : Type*
  IsIncident : vertices → hyperedges → Prop

or

structure Hypergraph (V : Type*) where
  hyperedges : Type*
  IsIncident : V → hyperedges → Prop

It even makes the incidence matrix more straightforward, no sets involved.

[Shreyas Srinivas]

You don’t want vertices to be a Type. You want them to be Set V

[Shreyas Srinivas]

Sets are far more convenient to work with than types

[Evan Walter Clark Spotte-Smith]

@Ammar Husain @Shreyas Srinivas, do y'all have opinions about having a stripped down definition (e.g., with just vertexSet, hyperedgeSet, and some combination of IsIncident and IsHyperedge) vs. having multiple axioms in the definition?

[Shreyas Srinivas]

I personally think if you want to label hyperedges, it makes sense to extend

structure Hypergraph (α : Type*) where
  vertexSet : Set α
  hyperedgeSet : Set (Set α)

[Shreyas Srinivas]

you want the vertexSet to avoid creating a separate type for subhypergraphs and then face the annoying issue of proving lemmas for subhypergraphs that apply to all hypergraphs through tedious coercions

[Evan Walter Clark Spotte-Smith]

In that case, you'd want to have a guarantee that all α in a hyperedge were in the vertex set / each hyperedge is a subset of vertexSet, right?

[Shreyas Srinivas]

yes

[Shreyas Srinivas]

See the definition of docs#SimpleGraph.Subgraph

[Shreyas Srinivas]

you don't need adj_sub {v w : V} : self.Adj v w → G.Adj v w

[Shreyas Srinivas]

and you don't need edge.symm because it makes no sense here

[Evan Walter Clark Spotte-Smith]

Word, that's helpful feedback. I'll get started cleaning up my code.

Yeah, of course, symmetry isn't relevant here.

[Evan Walter Clark Spotte-Smith]

How does this look?

structure Hypergraph (α : Type*) where
  /-- The vertex set -/
  vertexSet : Set α
  /-- The hyperedge set -/
  hyperedgeSet : Set (Set α)
  /-- Incidence predicate stating that a vertex `x` is a member of hyperedge `e` -/
  IsIncident : α → Set α → Prop := fun x e => e ∈ hyperedgeSet ∧ x ∈ e
  /-- All hyperedges must be subsets of the vertex set -/
  hyperedge_isSubset_vertexSet : ∀ ⦃e⦄, e ∈ hyperedgeSet → e ⊆ vertexSet
  /-- If something is incident on a hyperedge, then it must be in the vertex set -/
  vertex_mem_if_isIncident :
    ∀ ⦃ x e ⦄, IsIncident x e → x ∈ vertexSet

[Evan Walter Clark Spotte-Smith]

Oh, there's one annoyance (so far). If hyperedges are just Set α, then defining the dual of a hypergraph becomes annoying.

If H = (V, E), then the dual H* = (E, V), and incidence is defined such that if a vertex v ∈ V was incident on e ∈ E in H, then e is incident on v in H*.

In the current system, dual(H : Hypergraph α) would create a hypergraph of type Hypergraph (Set α)... which would then have a hyperedge set of type Set (Set α). So, then you wouldn't have the property that dual(dual(H)) = H; rather, you'd have growing numbers of nested sets.

[Evan Walter Clark Spotte-Smith]

This makes me want to stick with having a β type for hyperedges (unless I'm missing some way to avoid this awkwardness with duals)

[Ammar Husain]

so one thing avoiding beta was for was to prevent parallel edges, should there be a proof that for every pair of such they are not the same adjacencies?

[Shreyas Srinivas]

IsIncident is not serving any purpose

[Shreyas Srinivas]

You have merely assigned it a default value. This does not constrain the relation to be defined this way

[Shreyas Srinivas]

I am not on a laptop and it isn’t convenient to type lean on a phone. What you want is to convert the last field to (\exists e \in hyperEdgeSet, v \in e -> v \in vertex Set

[Evan Walter Clark Spotte-Smith]

Ah, I misunderstood the syntax on IsIncident (as I said, quite new to Lean).

So, given that IsIncident isn't needed, we're talking about something like this:

structure Hypergraph (α : Type*) where
  /-- The vertex set -/
  vertexSet : Set α
  /-- The hyperedge set -/
  hyperedgeSet : Set (Set α)
  /-- All hyperedges must be subsets of the vertex set -/
  hyperedge_isSubset_vertexSet : ∀ ⦃e⦄, e ∈ hyperedgeSet → e ⊆ vertexSet
  /-- If something is incident on a hyperedge, then it must be in the vertex set -/
  vertex_mem_if_mem_hyperedge : ∀ ⦃x⦄, ∃ e ∈ hyperedgeSet, x ∈ e → x ∈ vertexSet

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

I was right in my deleted message. The fourth field is implied by the third field

[Shreyas Srinivas]

If all hyperedges are subsets of the vertex set, then every vertex edge in a hyperedge is surely in the vertex set by definition.

[Aaron Liu]

Shreyas Srinivas said:

I was right in my deleted message. The fourth field is implied by the third field

no it's not, since you can set hyperedgeSet := ∅

[Aaron Liu]

oh is there a missing parentheses around the exists here?

[Aaron Liu]

If that was supposed to be ∀ ⦃x⦄, (∃ e ∈ hyperedgeSet, x ∈ e) → x ∈ vertexSet then yes, it's equivalent to the third condition.

[Evan Walter Clark Spotte-Smith]

So, it's better that I prove the fourth condition based on the third?

[Aaron Liu]

you have a very weird statement of the fourth condition

[Aaron Liu]

it's also just two rewrites away from the third condition

[Aaron Liu]

docs#exists_imp and docs#Set.subset_def

[Evan Walter Clark Spotte-Smith]

Aaron Liu said:

docs#exists_imp and docs#Set.subset_def

Appreciate the pointer here.

[Shreyas Srinivas]

Aaron Liu said:

you have a very weird statement of the fourth condition

It was my fault. I first worked to remove the unnecessary IsIncident field which was being used in what was then the fifth field. Basically I was debugging one step at a time.

[Ammar Husain]

What happened with want to stick with having a \beta type?

[Evan Walter Clark Spotte-Smith]

Sorry, just saw this.

So, I still kind of like having the β type for hyperedges. I think it makes the hypergraph definition somewhat more general. But I've also come to the conclusion, having now made some additional definitions and lemmas both with hyperedges as β and with hyperedges as Set α, that the former is more cumbersome.

With β, you need to not only carry around vertices and hyperedges but also the sets of vertices associated with each hyperedge. You also need to be able to prove additional properties in order to create a hypergraph (see my original definition, though of course it's possible that some of the implications that I had weren't strictly necessary).

In contrast, with Set α, as @Shreyas Srinivas helped me see, you can get away with just:

structure Hypergraph (α : Type*) where
  /-- The vertex set -/
  vertexSet : Set α
  /-- The hyperedge set -/
  hyperedgeSet : Set (Set α)
  /-- All hyperedges must be subsets of the vertex set -/
  hyperedge_isSubset_vertexSet : ∀ ⦃e⦄, e ∈ hyperedgeSet → e ⊆ vertexSet

and then it's pretty easy to define things like a partial hypergraph:

/--
Given a subset of the hyperedge set `E(H)` of a hypergraph `H` (`l : Set (Set α)`), the
*partial hypergraph* `Hˡ` has `E(Hˡ) = l ∩ E(H)` and `V(Hˡ)` is the subset of `V(H)` which is
incident on at least one hyperedge in `E(Hˡ)`.
-/
def partialHypergraph (H : Hypergraph α) (l : Set (Set α)) :=
  Hypergraph.mk
  {x | ∃ e ∈ l, e ∈ E(H) ∧ x ∈ e}
  (l ∩ E(H))
  (by
    intro q hq
    have h0 : ∀ x ∈ q, ∃ e ∈ l, e ∈ E(H) ∧ x ∈ e := by
      intro x hx
      use q
      constructor
      · exact mem_of_mem_inter_left hq
      constructor
      · exact mem_of_mem_inter_right hq
      · exact hx
    exact h0
  )

[Tristan Figueroa-Reid]

If you do plan to put this in a repository somewhere, please let us know! I'm also tangentially involved with hypergraphs, so seeing some theorems on them formalized would be great.

(You can also golf down partialHypergraph a little):

def partialHypergraph (H : Hypergraph α) (l : Set (Set α)) : Hypergraph α where
  vertexSet := {x | ∃ e ∈ l, e ∈ E(H) ∧ x ∈ e}
  hyperedgeSet := l ∩ E(H)
  hyperedge_isSubset_vertexSet q hq _ hx := ⟨q, hq.1, hq.2, hx⟩

[Evan Walter Clark Spotte-Smith]

I'm planning on submitting a PR to mathlib. I just wanted to sort out the general design here first so that I didn't waste any of the maintainers' time.

If you're interested in contributing, I can get a work-in-progress PR out sooner rather than later.

[Evan Walter Clark Spotte-Smith]

Tristan Figueroa-Reid said:

If you do plan to put this in a repository somewhere, please let us know! I'm also tangentially involved with hypergraphs, so seeing some theorems on them formalized would be great.

(You can also golf down partialHypergraph a little):

def partialHypergraph (H : Hypergraph α) (l : Set (Set α)) : Hypergraph α where
  vertexSet := {x | ∃ e ∈ l, e ∈ E(H) ∧ x ∈ e}
  hyperedgeSet := l ∩ E(H)
  hyperedge_isSubset_vertexSet q hq _ hx := ⟨q, hq.1, hq.2, hx⟩

And I'm sure most of my proofs are on the inefficient side... definitely appreciate your suggestion.

[Evan Walter Clark Spotte-Smith]

Opened this PR: https://github.com/leanprover-community/mathlib4/pull/28613

[Bhavik Mehta]

This is nice to see, I have a pretty substantial development of hypergraph theory in a private repo, so I'm glad to see this discussion converged on the same definition that I had. I'll take a closer look at your PR tomorrow, thanks for making it.

[Evan Walter Clark Spotte-Smith]

Of course! Any feedback (or additions, if there's code you can share) is welcome.

[Evan Walter Clark Spotte-Smith]

Okay, so, my original Hypergraph PR is still in progress, but I've been continuing working in the background.

One thing that I'm a bit stuck on is defining walks on hypergraphs. SimpleGraph uses an inductive type:

inductive Walk : V → V → Type u
  | nil {u : V} : Walk u u
  | cons {u v w : V} (h : G.Adj u v) (p : Walk v w) : Walk u w
  deriving DecidableEq

where Walk u v is the type of all walks from u to v.

and you could do something similar for hypergraphs:

inductive Walk : α → α → Type u
  | nil {x : α} : Walk x x
  | cons {x y z : α} {e : Set α} (he : e ∈ E(H))
    (hx : x ∈ e) (hy : y ∈ e) (hxy : x ≠ y) (p : Walk y z) : Walk x z

This isn't quite as pretty because, while a graph's walk depends only on the string of vertices, here the identity of the hyperedge matters (this is why I have the three hypotheses (he : e ∈ E(H)) (hx : x ∈ e) (hy : y ∈ e) instead of just (h : H.Adj x y)).

It seemed simpler to me to just represent a walk as List (α × Set α), with a sort of validator predicate

def IsWalk (H : Hypergraph α) : List (α × Set α) → Prop
  | [] => True
  | (_, e) :: [] => e = ∅
  | (x, e) :: (y, e') :: W => e ∈ E(H) ∧ x ∈ e ∧ y ∈ e ∧ x ≠ y ∧ H.IsWalk ((y, e') :: W)

Is there a benefit to going with the new inductive type that I'm just not seeing?

[Jakub Nowak]

The main important difference is that nil walk doesn't have a vertex associated with. This means, that if you want to define source and target of a walk, you have to either return Option, or accept proof that walk is not nil, or use [Inhabited V].

Maybe you could try α × List (α × Set α) instead?

I was experimenting (not much yet though) with this definition of Walk for SimpleGraph. With the current definition, I've had some problems with type checker, because source and target vertex are part of the type.

import Mathlib

open SimpleGraph

variable {V : Type*} {G : SimpleGraph V} {u v : V}

inductive SimpleGraph.IsWalk (G : SimpleGraph V) : V → List (V × V) → Prop
| nil : IsWalk G _ []
| cons : ∀ {u v : V} {es : List (V × V)}, G.Adj u v → SimpleGraph.IsWalk G v es →
    SimpleGraph.IsWalk G u (.cons ⟨u, v⟩ es)

def SimpleGraph.IsWalk' (G : SimpleGraph V) : V → List (V × V) → Prop
| _, .nil => True
| u, .cons ⟨u', v⟩ es => u = u' ∧ G.Adj u' v ∧ SimpleGraph.IsWalk' G v es

theorem SimpleGraph.IsWalk.iff {es : List (V × V)} {G : SimpleGraph V} :
    IsWalk G u es ↔ IsWalk' G u es := by sorry

def SimpleGraph.Walk2 (G : SimpleGraph V) :=
  { p : (V × List (V × V)) // SimpleGraph.IsWalk G p.1 p.2 }

I've tried using inductive Prop definition to avoid u = u', but I'm not sure whether it's better or not like that.

[Evan Walter Clark Spotte-Smith]

Your α × List (α × Set α) suggestion is a good one. I can totally see the nil checking becoming quite onerous.

And I'm glad that I'm not the only one who's had some issues with the inductive Walk definitions and related derivations.

[Chelsea Edmonds]

Just came across this thread, and thought I'd mention that I've done a bunch of work formalising design theory/hypergraphs in Isabelle (https://www.isa-afp.org/authors/edmonds/). Could be interesting to compare! I'm playing around with Lean as well, so am hoping to port a few things across/try out some new proofs on some point, would be open to connecting with existing lean developments on it!

[Evan Walter Clark Spotte-Smith]

Ah! Thank you for sharing this! I hadn't realized that others had formalized hypergraphs. I will take a look at your work and probably come back with questions.

I link to the PR that I wrote (using some modified versions of @Bhavik Mehta's code) above. If you have thoughts/feedback, I'd love to hear it!

[Chelsea Edmonds]

Questions very welcome! Isabelle tends to be fairly readable online, but know there are some notable differences to Lean that can affect the approach - Bhavik and I have discussed in the past :) I'd note that on my end the design theory library was significantly more developed then the hypergraph work, but both modelled as incidence set systems at the end of the day so a lot would translate really easily (the hypergraph library basically showed how to translate a few concepts I needed across and I think overlaps with most of your initial PR). The design theory libraries include a lot of the concepts you've listed as future work (incidence matrices - which in hindsight I would do a different way, lots of variation on design types, dual designs etc).

[Evan Walter Clark Spotte-Smith]

Yeah, I suppose I'll have to look at the Isabelle design theory work to fully understand what you've done with hypergraphs.

[Chelsea Edmonds]

Yeah its pretty interconnected!

[Chelsea Edmonds]

I'm not actively working on formal maths projects at the moment (this was all from my PhD), but hopefully will have a little time for it again later this year once I start a new job so will definitely try out/have a closer look at your Lean library too then :)

[Evan Walter Clark Spotte-Smith]

Well, congrats on the new job. I hope the transition goes smoothly!