a combinatorial challenge

Stream: maths

[Johan Commelin]

Here is a nice little challenge that I don't really know how to formalise.
We need graphs. What is a graph? In this case it will be a bunch of nodes and edges. No multiple edges, no self-loops, no directed edges.
If g is a node, then N(g) is the set of its neighbouring nodes, so {g' : G | (g,g') ∈ E(G)}.

Let G be a finite connected graph. And let w : G → pnat be a function that labels the nodes of G with positive natural numbers. We say that (G, w) is good if it satisfies the following condition: for all g : G we have 2 * w(g) = sum_{g' ∈ N(g)} w(g').

Challenge: enumerate all good finite connected labeled graphs (G, w).

[Chris Hughes]

Define "enumerate"

[Mario Carneiro]

ah, this is a step in the CFSG I think

[Mario Carneiro]

these are dynkin diagrams?

[Johan Commelin]

Bingo! Now how do we put that in Lean?

[Johan Commelin]

(Note, you don't get all Dynkin diagrams. Only the ones without multi-edges. And you'll also miss $A_1$.)

[Mario Carneiro]

The list is pretty short, right? I thought it was a simple counting argument, but I doubt some general enumeration mechanism will help

[Johan Commelin]

Should Dynkin diagrams be some sort of inductive type?

[Johan Commelin]

I have no idea how to do graph theory in Lean.

[Mario Carneiro]

Actually I'm thinking more about the math part here

[Mario Carneiro]

the representation depends on how you intend to argue it

[Johan Commelin]

I guess I agree with "a simple counting argument".

[Mario Carneiro]

Do you know why the list is finite or how you argue for this?

[Johan Commelin]

But what does that mean for formalising this?

[Johan Commelin]

The list isn't exactly finite.

[Mario Carneiro]

do you know why it's tightly constrained

[Johan Commelin]

Yes

[Johan Commelin]

First you have to bound $\# N(g)$.

[Johan Commelin]

After that you need a little argument with arithmetic progressions (of very short length).

[Mario Carneiro]

So I guess you have an arbitrary graph, on an arbitrary type, and you produce a bijection to some known graph by cases

[Mario Carneiro]

the graph itself can be represented by a symmetric irreflexive edge relation like you said

[Mario Carneiro]

To prove graph isomorphism formally seems a little tedious. One general method: If you have an injective function on vertices, you know all the degrees of the vertices, and you have a list of edges that are mapped to the other graph, which matches the degrees, then you can prove that the map is a graph isomorphism

[Mario Carneiro]

(I hate doing graphs formally, there's no great method)

[Johan Commelin]

(I hate doing graphs formally, there's no great method)

That's discouraging.

[Mario Carneiro]

well, general graphs are fine, but small finite graphs are a pain

[Mario Carneiro]

just like small finite anything

[Mario Carneiro]

the less concretely you have to talk about the stuff, the better

[Mario Carneiro]

so in this case you might be able to avoid doing graph isomorphism entirely, and instead say something like "there is a vertex of degree 3 attached to vertices of degree 2, there is a path to such and such with this pattern, etc"

[Mario Carneiro]

and maybe that's good enough for whatever purpose you need this classification

[Johan Commelin]

structure graph (G : Type u) :=
(E     : G → G → Prop)
(symm  : ∀ g₁ g₂, E g₁ g₂ ↔ E g₂ g₁)
(irref : ∀ g, ¬ E g g)

def graph.unit : graph unit :=
{ E := λ _ _, false,
  symm := λ _ _, iff.rfl,
  irref := λ _, id }

def graph.glue {G₁ : Type u} (gr₁ : graph G₁) {G₂ : Type u} (gr₂ : graph G₂) (E : G₁ → G₂ → Prop) :
  graph (G₁ ⊕ G₂) :=
{ E := λ g g',
  begin
    cases g with g₁ g₂;
    cases g' with g₁' g₂',
    { exact gr₁.E g₁ g₁' },
    { exact E g₁ g₂' },
    { exact E g₁' g₂ },
    { exact gr₂.E g₂ g₂' }
  end,
  symm := λ g g',
  begin
    cases g with g₁ g₂;
    cases g' with g₁' g₂';
    try { exact graph.symm _ _ _ };
    try { exact iff.rfl }
  end,
  irref := λ g,
  begin
    cases g with g₁ g₂;
    exact graph.irref _ _
  end }

namespace Dynkin

def A (n : ℕ) : graph (fin n) :=
{ E := λ i j, j.val = i.val + 1 ∨ i.val = j.val + 1,
  symm := λ i j, ⟨or.symm, or.symm⟩,
  irref := λ i h, by cases h;
    { conv at h { to_lhs, rw ← nat.add_zero i.val },
      exact nat.no_confusion (nat.add_left_cancel h) } }

def D_type : Π (n : ℕ), Type
| 0     := fin 0
| (n+1) := fin n ⊕ unit

def D : Π (n : ℕ), graph (D_type n)
| 0     := A 0
| (n+1) := (A n).glue graph.unit (λ i _, i.val = 1)

end Dynkin

[Johan Commelin]

@Mario Carneiro Does it make sense to do something like this. Or is this asking for trouble somewhere down the road?

[Johan Commelin]

One can also do E6, E7, and E8 by gluing. But I guess these are better done as inductive types, to allow easy case bashing.

def E6_type : Type := fin 4 ⊕ fin 2

def E7_type : Type := fin 4 ⊕ fin 3

def E8_type : Type := fin 4 ⊕ fin 4

def E6 : graph E6_type :=
(A 4).glue (A 2) (λ i j, i.val = 2 ∧ j.val = 0)

def E7 : graph E7_type :=
(A 4).glue (A 3) (λ i j, i.val = 2 ∧ j.val = 0)

def E8 : graph E8_type :=
(A 4).glue (A 4) (λ i j, i.val = 2 ∧ j.val = 0)

[Mario Carneiro]

I think there is a good case for bundling here, it would allow you to skip the D and D_type thing

[Mario Carneiro]

at least based on these few examples

[Mario Carneiro]

Probably graph.symm should be unidirectional

[Johan Commelin]

Can you explain why? I'd like to get a better understanding for that kind of issues.

[Mario Carneiro]

well, all of the constructions you have done so far have to come in two parts

[Chris Hughes]

Because it's equivalent and easier to prove.

[Mario Carneiro]

and the type doesn't have much more semantic information than "the vertex type of the graph"

[Mario Carneiro]

There are other ways to use a data structure like this for which unbundled might make sense, but for building and manipulating small graphs I think it's more natural to bundle here

[Johan Commelin]

Aah, sorry for the confusion. I was asking about the unidirectional thing.

[Mario Carneiro]

well, it's equivalent, but easier to prove

[Johan Commelin]

Ok

[Mario Carneiro]

you want the thing in the structure to be the weakest constraint since that's what you have to show in constructions

[Johan Commelin]

Aah, of course

[Mario Carneiro]

you can prove the bidirectional version as a theorem

[Mario Carneiro]

now you still have to define a weight on G, and show that these guys have good weights

[Reid Barton]

will bundling make it awkward to prove theorems valid only for finite graphs?

[Mario Carneiro]

there will be a typeclass for finite graph

[Mario Carneiro]

which should include some kind of computational content to work with the graph, like an adjacency list

[Mario Carneiro]

unless you just want to say finite in the abstract, but you can still use fintype G.V or whatever

[Johan Commelin]

This is what I have now (after bundling):

import data.fin

structure graph
(V     : Type)
(E     : V → V → Prop)
(symm  : ∀ v₁ v₂, E v₁ v₂ → E v₂ v₁)
(irref : ∀ v, ¬ E v v)

instance : has_coe_to_sort graph :=
{ S := Type,
  coe := graph.V }

def graph.unit : graph :=
{ V := unit,
  E := λ _ _, false,
  symm := λ _ _, id,
  irref := λ _, id }

def graph.glue (G₁ : graph) (G₂ : graph) (E : G₁ → G₂ → Prop) : graph :=
{ V := G₁ ⊕ G₂,
  E := λ v v',
  begin
    cases v with v v;
    cases v' with v' v';
    try { exact graph.E _ v v' };
    try { exact E ‹G₁› ‹G₂› },
  end,
  symm := λ v v',
  begin
    cases v with v₁ v₂;
    cases v' with v₁' v₂';
    try { exact graph.symm _ _ _ };
    try { exact id }
  end,
  irref := λ v,
  begin
    cases v with v₁ v₂;
    exact graph.irref _ _
  end }

namespace Dynkin

def A (n : ℕ) : graph :=
{ V := fin n,
  E := λ i j, j.val = i.val + 1 ∨ i.val = j.val + 1,
  symm := λ i j, or.symm,
  irref := λ i h, by cases h;
    { conv at h { to_lhs, rw ← nat.add_zero i.val },
      exact nat.no_confusion (nat.add_left_cancel h) } }

def D : Π (n : ℕ), graph
| 0     := A 0
| (n+1) := (A n).glue graph.unit (λ i _, n = i.val + 2)

def E6 : graph :=
(A 4).glue (A 2) (λ i j, i.val = 2 ∧ j.val = 0)

def E7 : graph :=
(A 4).glue (A 3) (λ i j, i.val = 2 ∧ j.val = 0)

def E8 : graph :=
(A 4).glue (A 4) (λ i j, i.val = 2 ∧ j.val = 0)

end Dynkin

[Andrew Ashworth]

is the coq graph library no good? (sorry, didn't read all of the thread yet: https://github.com/coq-contribs/graph-basics)

[Johan Commelin]

Probably it is. But it needs to be ported :grinning_face_with_smiling_eyes:

[Bryan Gin-ge Chen]

That Coq library is LGPL licensed, which could complicate the incorporation of any port of it into mathlib. (not a lawyer and all that of course...)

[Johan Commelin]

which is why I am a very big fan of https://unlicense.org/

[Jesse Michael Han]

Floris has started on Dynkin diagrams for the formal abstract of the classification of finite simple groups. Many of the sporadics can be defined as a quotient of a generalized Coxeter-type presentation, for which we have Coxeter Y-diagrams.

[Johan Commelin]

Aah, that's good to know. Thanks for the heads up!

[Floris van Doorn]

Thanks, Jesse, for pointing to my file. It is very much WIP. My (current) definition of Dynkin diagram (with directed multiple edges and undirected single edges) is

structure dynkin_diagram :=
  (vertex : Type v)
  (edge : vertex → vertex → Prop)
  (annotation : Π{{x y}}, edge x y → ℕ+)
  (directed : Π{{x y}} (e : edge x y), annotation e = 1 ↔ edge y x)

If you want to talk about undirected graphs, I think you should index them by unordered pairs of distinct elements:

/-- unordered pairs of distinct elements -/
def upair (α : Type u) : Type u := {s : finset α // s.card = 2}

This would require some scaffolding to set up a library for these creatures, but after that I think it would be more convenient to work with these "undirected graphs" as opposed to "symmetric directed graphs". I was also considering this approach for Dynkin diagrams, but since some edges in Dynkin diagrams are directed, I decided to use a (mostly symmetric) directed graph.

[Floris van Doorn]

When thinking a bit about this upair object, I was wondering the following. upair is a subtype (of a subtype) of a quotient. Is it formalized in Lean that a subtype of a quotient is equivalent to a quotient of a subtype? That would probably be useful when reasoning about upair: they would correspond to (lists of length 2 with no duplicates) quotiented by permutation.