## Stream: maths

### Topic: a combinatorial challenge

#### Johan Commelin (Feb 05 2019 at 13:05):

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 (Feb 05 2019 at 13:26):

Define "enumerate"

#### Mario Carneiro (Feb 05 2019 at 13:33):

ah, this is a step in the CFSG I think

#### Mario Carneiro (Feb 05 2019 at 13:33):

these are dynkin diagrams?

#### Johan Commelin (Feb 05 2019 at 14:02):

Bingo! Now how do we put that in Lean?

#### Johan Commelin (Feb 05 2019 at 14:03):

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

#### Mario Carneiro (Feb 05 2019 at 14:05):

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 (Feb 05 2019 at 14:06):

Should Dynkin diagrams be some sort of inductive type?

#### Johan Commelin (Feb 05 2019 at 14:06):

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

#### Mario Carneiro (Feb 05 2019 at 14:06):

Actually I'm thinking more about the math part here

#### Mario Carneiro (Feb 05 2019 at 14:07):

the representation depends on how you intend to argue it

#### Johan Commelin (Feb 05 2019 at 14:08):

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

#### Mario Carneiro (Feb 05 2019 at 14:10):

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

#### Johan Commelin (Feb 05 2019 at 14:10):

But what does that mean for formalising this?

#### Johan Commelin (Feb 05 2019 at 14:10):

The list isn't exactly finite.

#### Mario Carneiro (Feb 05 2019 at 14:10):

do you know why it's tightly constrained

Yes

#### Johan Commelin (Feb 05 2019 at 14:12):

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

#### Johan Commelin (Feb 05 2019 at 14:12):

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

#### Mario Carneiro (Feb 05 2019 at 14:17):

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 (Feb 05 2019 at 14:17):

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

#### Mario Carneiro (Feb 05 2019 at 14:23):

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 (Feb 05 2019 at 14:24):

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

#### Johan Commelin (Feb 05 2019 at 14:25):

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

That's discouraging.

#### Mario Carneiro (Feb 05 2019 at 14:26):

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

#### Mario Carneiro (Feb 05 2019 at 14:26):

just like small finite anything

#### Mario Carneiro (Feb 05 2019 at 14:27):

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

#### Mario Carneiro (Feb 05 2019 at 14:28):

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 (Feb 05 2019 at 14:28):

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

#### Johan Commelin (Feb 05 2019 at 15:29):

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 (Feb 05 2019 at 15:29):

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

#### Johan Commelin (Feb 05 2019 at 15:35):

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 (Feb 05 2019 at 15:44):

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

#### Mario Carneiro (Feb 05 2019 at 15:45):

at least based on these few examples

#### Mario Carneiro (Feb 05 2019 at 15:46):

Probably graph.symm should be unidirectional

#### Johan Commelin (Feb 05 2019 at 15:46):

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

#### Mario Carneiro (Feb 05 2019 at 15:47):

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

#### Chris Hughes (Feb 05 2019 at 15:47):

Because it's equivalent and easier to prove.

#### Mario Carneiro (Feb 05 2019 at 15:48):

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

#### Mario Carneiro (Feb 05 2019 at 15:49):

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 (Feb 05 2019 at 15:50):

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

#### Mario Carneiro (Feb 05 2019 at 15:50):

well, it's equivalent, but easier to prove

Ok

#### Mario Carneiro (Feb 05 2019 at 15:51):

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

Aah, of course

#### Mario Carneiro (Feb 05 2019 at 15:51):

you can prove the bidirectional version as a theorem

#### Mario Carneiro (Feb 05 2019 at 15:54):

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

#### Reid Barton (Feb 05 2019 at 15:54):

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

#### Mario Carneiro (Feb 05 2019 at 15:55):

there will be a typeclass for finite graph

#### Mario Carneiro (Feb 05 2019 at 15:55):

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

#### Mario Carneiro (Feb 05 2019 at 15:57):

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

#### Johan Commelin (Feb 05 2019 at 15:58):

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 (Feb 05 2019 at 16:22):

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 (Feb 05 2019 at 16:27):

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

#### Bryan Gin-ge Chen (Feb 05 2019 at 17:21):

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 (Feb 05 2019 at 17:36):

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

#### Jesse Michael Han (Feb 05 2019 at 19:36):

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 (Feb 05 2019 at 19:53):

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

#### Floris van Doorn (Feb 05 2019 at 20:18):

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 (Feb 05 2019 at 20:24):

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.

Last updated: May 14 2021 at 20:13 UTC