Zulip Chat Archive

Stream: maths

Topic: a combinatorial challenge


view this post on Zulip 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).

view this post on Zulip Chris Hughes (Feb 05 2019 at 13:26):

Define "enumerate"

view this post on Zulip Mario Carneiro (Feb 05 2019 at 13:33):

ah, this is a step in the CFSG I think

view this post on Zulip Mario Carneiro (Feb 05 2019 at 13:33):

these are dynkin diagrams?

view this post on Zulip Johan Commelin (Feb 05 2019 at 14:02):

Bingo! Now how do we put that in Lean?

view this post on Zulip 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 A1A_1.)

view this post on Zulip 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

view this post on Zulip Johan Commelin (Feb 05 2019 at 14:06):

Should Dynkin diagrams be some sort of inductive type?

view this post on Zulip Johan Commelin (Feb 05 2019 at 14:06):

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

view this post on Zulip Mario Carneiro (Feb 05 2019 at 14:06):

Actually I'm thinking more about the math part here

view this post on Zulip Mario Carneiro (Feb 05 2019 at 14:07):

the representation depends on how you intend to argue it

view this post on Zulip Johan Commelin (Feb 05 2019 at 14:08):

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

view this post on Zulip Mario Carneiro (Feb 05 2019 at 14:10):

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

view this post on Zulip Johan Commelin (Feb 05 2019 at 14:10):

But what does that mean for formalising this?

view this post on Zulip Johan Commelin (Feb 05 2019 at 14:10):

The list isn't exactly finite.

view this post on Zulip Mario Carneiro (Feb 05 2019 at 14:10):

do you know why it's tightly constrained

view this post on Zulip Johan Commelin (Feb 05 2019 at 14:10):

Yes

view this post on Zulip Johan Commelin (Feb 05 2019 at 14:12):

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

view this post on Zulip Johan Commelin (Feb 05 2019 at 14:12):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 05 2019 at 14:17):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 05 2019 at 14:24):

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

view this post on Zulip Johan Commelin (Feb 05 2019 at 14:25):

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

That's discouraging.

view this post on Zulip Mario Carneiro (Feb 05 2019 at 14:26):

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

view this post on Zulip Mario Carneiro (Feb 05 2019 at 14:26):

just like small finite anything

view this post on Zulip Mario Carneiro (Feb 05 2019 at 14:27):

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

view this post on Zulip 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"

view this post on Zulip Mario Carneiro (Feb 05 2019 at 14:28):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 05 2019 at 15:45):

at least based on these few examples

view this post on Zulip Mario Carneiro (Feb 05 2019 at 15:46):

Probably graph.symm should be unidirectional

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Feb 05 2019 at 15:47):

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

view this post on Zulip Chris Hughes (Feb 05 2019 at 15:47):

Because it's equivalent and easier to prove.

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip Johan Commelin (Feb 05 2019 at 15:50):

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

view this post on Zulip Mario Carneiro (Feb 05 2019 at 15:50):

well, it's equivalent, but easier to prove

view this post on Zulip Johan Commelin (Feb 05 2019 at 15:51):

Ok

view this post on Zulip 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

view this post on Zulip Johan Commelin (Feb 05 2019 at 15:51):

Aah, of course

view this post on Zulip Mario Carneiro (Feb 05 2019 at 15:51):

you can prove the bidirectional version as a theorem

view this post on Zulip 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

view this post on Zulip Reid Barton (Feb 05 2019 at 15:54):

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

view this post on Zulip Mario Carneiro (Feb 05 2019 at 15:55):

there will be a typeclass for finite graph

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Johan Commelin (Feb 05 2019 at 16:27):

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

view this post on Zulip 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...)

view this post on Zulip Johan Commelin (Feb 05 2019 at 17:36):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Feb 05 2019 at 19:53):

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

view this post on Zulip 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.

view this post on Zulip 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