# Zulip Chat Archive

## 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

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

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

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

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

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

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