directed graphs

Stream: graph theory

[Kyle Miller]

This could potentially be a way (among others) to define simple directed graphs:

@[ext]
structure simple_digraph (V : Type u) :=
(adj : V → V → Prop)
(loopless : irreflexive adj . obviously)

@[ext]
structure simple_graph (V : Type u) extends simple_digraph V :=
(sym : symmetric adj . obviously)

You would then have to define a number of things having to do with edges of directed graphs (represented as pairs of vertices), and relate them to edges of simple graphs (represented as unordered pairs of vertices). There is some precedent to call an ordered edge a "dart," but it's probably fine (if potentially a name collision) to call them "edges." (Maybe "dedge" for "directed edge" is an ok compromise?)

There would be a 2-1 map from directed edges to edges. All of this can be then used to simplify the degree_sum module.

[Yakov Pechersky]

The digraph here allows a two vertex cycle. Is that desired?

[Kyle Miller]

Yakov Pechersky said:

The digraph here allows a two vertex cycle. Is that desired?

I'm not sure!

[Kyle Miller]

Though I believe this follows the usual definition of a simple directed graph.

[Yakov Pechersky]

Ah, I'm used to thinking about oriented graphs. Those are ones that have no such cycles.

[Kyle Miller]

It seems like it would be nice having a predicate for whether a simple digraph is an oriented graph. If there's also a function from digraphs to simple graphs by symmetrizing the relation, then there could be a recursion principle where you define/prove something about a simple graph given an oriented representative.

[Yakov Pechersky]

Something like?

universe u

@[ext]
structure simple_digraph (V : Type u) :=
(adj : V → V → Prop)
(loopless : irreflexive adj . obviously)

class oriented {V : Type u} (G : simple_digraph V) : Prop :=
(uncycled (v w : V) : G.adj v w → ¬ G.adj w v)

@[ext]
structure simple_graph (V : Type u) extends simple_digraph V :=
(sym : symmetric adj . obviously)

def undi {V : Type u} (G : simple_digraph V) : simple_graph V :=
{ adj := λ v w, G.adj v w ∨ G.adj w v,
  loopless := λ x h, or.cases_on h (G.loopless x) (G.loopless x),
  sym := λ x y h, or.cases_on h or.inr or.inl }

lemma orienting_induction {V : Type u} {C : simple_graph V → Prop}
  (g : simple_graph V)
  (IH : ∀ (g' : simple_digraph V), C (undi g')) : C g := sorry

[Kyle Miller]

though you should be able to restrict to these oriented diagraphs for the induction hypothesis. (Changed the class to a def to make it easier to state.)

universe u

@[ext]
structure simple_digraph (V : Type u) :=
(adj : V → V → Prop)
(loopless : irreflexive adj . obviously)

def simple_digraph.ori {V : Type u} (G : simple_digraph V) : Prop :=
∀ (v w : V), G.adj v w → ¬ G.adj w v
-- this could also be stated as `antisymm G.adj` since `irreflexive G.adj`

@[ext]
structure simple_graph (V : Type u) extends simple_digraph V :=
(sym : symmetric adj . obviously)

def simple_digraph.to_simple_graph {V : Type u} (G : simple_digraph V) : simple_graph V :=
{ adj := λ v w, G.adj v w ∨ G.adj w v,
  loopless := λ x h, or.cases_on h (G.loopless x) (G.loopless x),
  sym := λ x y h, or.cases_on h or.inr or.inl }

lemma simple_graph.ori_ind {V : Type u} {C : simple_graph V → Prop}
  (IH : ∀ (g' : simple_digraph V), g'.ori → C g'.to_simple_graph) : ∀ g, C g := sorry

[Yakov Pechersky]

Another option is to have simple_graph be the quotient of simple_digraph.

[Yakov Pechersky]

Because the induction you stated right now will only work if there is an according statement that for all g : simple_graph there is a dg : simple_digraph such that dg.to_simple_graph = g.

[Kyle Miller]

Yeah, simple_graph is indeed a quotient of simple_digraph (and in fact a quotient of the subtype of simple_digraph satisfying ori), and you can say that ori_ind is part of the proof of this.

It seems like it's better to explicitly construct quotient types if you can rather than using quot, and then providing the recursor, unless quot somehow makes everything more elegant. I guess a principle is that something doesn't have to be represented as something to be something -- you just need the right universal properties. Simple graphs are very concrete, so the question is whether the benefits of having the quot API would outweigh the loss of concreteness -- I suspect it wouldn't provide that much, but it's hard to say without experiments.

(I'd thought about making multigraphs be quotients of directed multigraphs before, but I decided not to pursue it because at least initially it seemed difficult to work with.)

[Kyle Miller]

This would be nicer with more library support, and it can be golfed, but proving ori_ind wasn't so bad:

import tactic
import data.sym2

universe u

@[ext]
structure simple_digraph (V : Type u) :=
(adj : V → V → Prop)
(loopless : irreflexive adj . obviously)

def simple_digraph.is_ori {V : Type u} (G : simple_digraph V) : Prop :=
∀ (v w : V), G.adj v w → ¬ G.adj w v
-- this could also be stated as `antisymm G.adj` since `irreflexive G.adj`

@[ext]
structure simple_graph (V : Type u) extends simple_digraph V :=
(sym : symmetric adj . obviously)

def simple_digraph.to_simple_graph {V : Type u} (G : simple_digraph V) : simple_graph V :=
{ adj := λ v w, G.adj v w ∨ G.adj w v,
  loopless := λ x h, or.cases_on h (G.loopless x) (G.loopless x),
  sym := λ x y h, or.cases_on h or.inr or.inl }

lemma simple_graph.exists_ori {V : Type u} (G : simple_graph V) :
  ∃ (G' : simple_digraph V), G'.is_ori ∧ G = G'.to_simple_graph :=
begin
  have h : ∀ (e : sym2 V), ∃ v, v ∈ e,
  { intro e,
    refine quotient.ind (λ e, _) e,
    cases e with v w,
    exact ⟨v, sym2.mk_has_mem v w⟩, },
  choose f hf using h,
  use {adj := λ v w, G.adj v w ∧ f ⟦(v, w)⟧ = v, loopless := λ _ h, G.loopless _ h.1},
  split,
  { rintros v w ⟨ha, hv⟩ ⟨hb, hw⟩,
    rw sym2.eq_swap at hw,
    rw hv at hw,
    rw hw at ha,
    exact G.loopless _ ha, },
  { ext v w,
    dsimp [simple_digraph.to_simple_graph],
    split,
    { intro h,
      simp [h, G.sym h, true_and],
      rw @sym2.eq_swap _ w,
      specialize hf ⟦(v, w)⟧,
      rwa sym2.mem_iff at hf, },
    { rintro (h|h),
      { exact h.1, },
      { exact G.sym h.1, } } }
end

lemma simple_graph.ori_ind {V : Type u} {C : simple_graph V → Prop}
  (ih : ∀ (G' : simple_digraph V), G'.is_ori → C G'.to_simple_graph) : ∀ G, C G :=
begin
  intro G,
  obtain ⟨G', hG', rfl⟩ := G.exists_ori,
  exact ih G' hG',
end

[Kyle Miller]

This approach won't work for getting a computable simple_graph.ori_rec. If simple_graph were a quot then you should be able to make it computable, but I don't think this is high priority for mathlib.

[Yakov Pechersky]

I made cycles a quotient of lists, using is_rotated as the relation. Most proofs and definitions ended up being two-liners with quotient.induction_on', and defs were either quotient.map' or quotient.hrec_on'. It's the ability to do dependent recursion that I really like from quotients. In this case, we'd get the lemmas "by definition" with exists_rep and the automatic recursors. But of course one has to make the boilerplate coe simp lemmas. Either way works!

[Kyle Miller]

Cycles as quotients of lists makes a whole lot of sense to me, since there's no normal form for a cycle unless you have something like a total ordering on elements

[Kyle Miller]

Oh, I guess the alternative is a perm with a single orbit

[Yakov Pechersky]

A lot of recent work was done to show that that alternative holds!

[Yakov Pechersky]

And a direct correspondence is not exactly correct, because an empty cycle, and a cycle of a single element both interpret as the trivial perm.

[Yakov Pechersky]

And one could have a cycle with duplicates in it too.

[Kyle Miller]

Oh, right, forgot about all that!

[Kyle Miller]

I tried writing the ori_rec, but suspiciously (due to the use of the axiom of choice) it doesn't need the h hypothesis:

noncomputable
def simple_graph.ori_rec {V : Type u} {β : simple_graph V → Sort u}
  (f : Π {G' : simple_digraph V}, G'.is_ori → β G'.to_simple_graph)
  (h : ∀ {G' G'' : simple_digraph V} (hG' : G'.is_ori) (hG'' : G''.is_ori) (he : G'.to_simple_graph = G''.to_simple_graph),
    @eq.rec _ G'.to_simple_graph β (f hG') G''.to_simple_graph he = f hG'') :
  Π G, β G :=
begin
  intro G,
  obtain ⟨G', hG', rfl⟩ := classical.indefinite_description _ G.exists_ori,
  exact f hG',
end

Though to reduce ori_rec you do use h:

variables {V : Type u} {β : simple_graph V → Sort u}
variables (f : Π {G' : simple_digraph V}, G'.is_ori → β G'.to_simple_graph)
variables (h : ∀ {G' G'' : simple_digraph V} (hG' : G'.is_ori) (hG'' : G''.is_ori) (he : G'.to_simple_graph = G''.to_simple_graph),
             @eq.rec _ G'.to_simple_graph β (f hG') G''.to_simple_graph he = f hG'')

def simple_graph.ori_rec.prop (G : simple_digraph V) (hG : G.is_ori) :
  G.to_simple_graph.ori_rec @f @h = f hG :=
begin
  unfold simple_graph.ori_rec,
  obtain ⟨G', hG', he⟩ := classical.indefinite_description _ G.to_simple_graph.exists_ori,
  rw ←h hG' hG,
end

[Yakov Pechersky]

In any case, cycles can now help us define cyclic walks on graphs, if we redefine walks as chains on lists of vertices :-). That was one of the motivations for them.

[Kyle Miller]

I'm wondering: what if cycle is generalized to accept any type that has a rotate function with certain properties? The type Σ (v : V), G.walk v v would certainly support this. It'd support a reverse, too. For it to be useful, there should probably be a map to list V such that rotate and reverse commute with this map, so in this case there would be this walk cycle, but you could also view it as a cycle of vertices.

[Kyle Miller]

This would be more useful for cycles in multigraphs. Cycles in simple graphs are the same as their vertex cycles. Though for multigraphs, oriented cycles are determined by a cycle of (v, e) pairs with v a vertex of edge e.