## Stream: maths

### Topic: Hedetniemi

#### Johan Commelin (Mar 26 2020 at 20:51):

Several people have been playing with graph theory in Lean. Recently @David Wärn, and in the past @Vincent Beffara and @Vaibhav Karve. I think we should try to carve out a little library. I'm certainly not an expert in this area, but I would like to do propose a project similar to what happened after the sensitivity conjecture was proven. We formalised it as a community in a matter of days.
Last year the Hedetniemi conjecture was disproven, in 3 pages: https://arxiv.org/pdf/1905.02167.pdf
We could try to take this as a target. It will require formalising some graph theory, but not too much (hopefully). Experts are welcome to chime in.

Here is a little start:

import tactic

universe variables v v₁ v₂ v₃ u u₁ u₂ u₃

set_option old_structure_cmd true

structure multigraph (V : Type u) :=
(edge : V → V → Sort v)

attribute [class] multigraph

def multigraph.vertices {V : Type u} (G : multigraph V) := V

structure directed_graph (V : Type u) extends multigraph.{0} V.

attribute [class] directed_graph

def directed_graph.vertices {V : Type u} (G : directed_graph V) := V

structure graph (V : Type u) extends directed_graph V :=
(symm {} : symmetric edge)

attribute [class] graph

notation x ~[G] y := G.edge x y

namespace graph
variables {V : Type u} {V₁ : Type u₁} {V₂ : Type u₂} {V₃ : Type u₃}
variables (G : graph V) (G₁ : graph V₁) (G₂ : graph V₂) (G₃ : graph V₃)

def vertices (G : graph V) := V

def edge.symm {G : graph V} {x y : V} (e : x ~[G] y) : y ~[G] x := G.symm e

def is_linked (G : graph V) (x y : V) : Prop :=
relation.refl_trans_gen G.edge x y

def is_connected (G : graph V) : Prop :=
∀ x y, G.is_linked x y

def is_loopless (G : graph V) : Prop :=
∀ x, ¬ (x ~[G] x)

def complete (V : Type u) : graph V :=
{ edge := assume x y, x ≠ y,
symm := assume x y h, h.symm }

lemma complete_is_loopless (V : Type u) :
(complete V).is_loopless :=
assume x, ne.irrefl

section

/-- A homomorphism of graphs is a function on the vertices that preserves edges. -/
structure hom (G₁ : graph V₁) (G₂ : graph V₂) :=
(to_fun    : V₁ → V₂)
(map_edge' : ∀ {x y}, (x ~[G₁] y) → (to_fun x ~[G₂] to_fun y) . obviously)

instance hom.has_coe_to_fun : has_coe_to_fun (hom G₁ G₂) :=
{ F := λ f, V₁ → V₂,
coe := hom.to_fun }

@[simp] lemma hom.to_fun_eq_coe (f : hom G₁ G₂) (x : V₁) :
f.to_fun x = f x := rfl

section
variables {G₁ G₂ G₃}

@[simp, ematch] lemma hom.map_edge (f : hom G₁ G₂) :
∀ {x y}, (x ~[G₁] y) → (f x ~[G₂] f y) :=
f.map_edge'

@[ext] lemma hom.ext {f g : hom G₁ G₂} (h : (f : V₁ → V₂) = g) : f = g :=
by { cases f, cases g, congr, exact h }

lemma hom.ext_iff (f g : hom G₁ G₂) : f = g ↔ (f : V₁ → V₂) = g :=
⟨congr_arg _, hom.ext⟩

def hom.id : hom G G :=
{ to_fun := id }

def hom.comp (g : hom G₂ G₃) (f : hom G₁ G₂) : hom G₁ G₃ :=
{ to_fun    := g ∘ f,
map_edge' := assume x y, g.map_edge ∘ f.map_edge }

end

/-- The internal hom in the category of graphs. -/
instance ihom : graph (V₁ → V₂) :=
{ edge := assume f g, ∀ {x y}, (x ~[G₁] y) → (f x ~[G₂] g y),
symm := assume f g h x y e,
show g x ~[G₂] f y, from G₂.symm $h e.symm } /-- The product in the category of graphs. -/ instance prod : graph (V₁ × V₂) := { edge := assume p q, (p.1 ~[G₁] q.1) ∧ (p.2 ~[G₂] q.2), symm := assume p q ⟨e₁, e₂⟩, ⟨e₁.symm, e₂.symm⟩ } def prod.fst : hom (G₁.prod G₂) G₁ := { to_fun := λ p, p.1 } def prod.snd : hom (G₁.prod G₂) G₂ := { to_fun := λ p, p.2 } @[simps] def hom.pair (f : hom G G₁) (g : hom G G₂) : hom G (G₁.prod G₂) := { to_fun := λ x, (f x, g x), map_edge' := by { intros x y e, split; simp only [e, hom.map_edge] } } @[simps] def icurry : hom ((G₁.prod G₂).ihom G₃) (G₁.ihom (G₂.ihom G₃)) := { to_fun := function.curry, map_edge' := assume f g h x₁ y₁ e₁ x₂ y₂ e₂, h$ by exact ⟨e₁, e₂⟩ }

@[simps]
def iuncurry : hom (G₁.ihom (G₂.ihom G₃)) ((G₁.prod G₂).ihom G₃) :=
{ to_fun    := λ f p, f p.1 p.2,
map_edge' := assume f g h p q e, h e.1 e.2 }

section
variables {G₁ G₂ G₃}

@[simps]
def hom.curry (f : hom (G₁.prod G₂) G₃) : hom G₁ (G₂.ihom G₃) :=
{ to_fun    := icurry G₁ G₂ G₃ f,
map_edge' := assume x₁ y₁ e₁ x₂ y₂ e₂, f.map_edge ⟨e₁, e₂⟩ }

@[simps]
def hom.uncurry (f : hom G₁ (G₂.ihom G₃)) : hom (G₁.prod G₂) G₃ :=
{ to_fun    := iuncurry G₁ G₂ G₃ f,
map_edge' := assume p q e, f.map_edge e.1 e.2 }

end

def adj : (hom (G.prod G₁) G₂) ≃ (hom G (graph.ihom G₁ G₂)) :=
{ to_fun := hom.curry,
inv_fun := hom.uncurry,
left_inv := λ f, hom.ext $funext$ λ ⟨x,y⟩, rfl,
right_inv := λ f, hom.ext $funext$ λ p, rfl }

end

def colouring (W : Type) (G : graph V) := hom G (complete W)

structure is_nat_colouring (n : ℕ) (G : graph V) (f : V → ℕ) : Prop :=
(is_lt : ∀ x, f x < n)
(edge  : ∀ {x y}, (x ~[G] y) → f x ≠ f y)

structure chromatic_number (G : graph V) (n : ℕ) : Prop :=
(col_exists : ∃ f, is_nat_colouring n G f)
(min        : ∀ {k f}, is_nat_colouring k G f → n ≤ k)

def is_nat_colouring.colouring_fin {n} {G : graph V} {f} (h : is_nat_colouring n G f) :
G.colouring (fin n) :=
{ to_fun    := λ x, ⟨f x, h.is_lt x⟩,
map_edge' := λ x y e H, h.edge e $fin.veq_of_eq H } variables {G₁ G₂} lemma is_nat_colouring.comp {n} {g} (h : is_nat_colouring n G₂ g) (f : hom G₁ G₂) : is_nat_colouring n G₁ (g ∘ f) := { is_lt := assume x, h.is_lt _, edge := assume x y e, h.edge$ f.map_edge e }

section hedetniemi
variables {n₁ n₂ n : ℕ}
variables (h₁ : chromatic_number G₁ n₁)
variables (h₂ : chromatic_number G₂ n₂)
variables (h : chromatic_number (G₁.prod G₂) n)

include h₁ h₂ h

/-- Hedetniemi's conjecture, which has been disproven in <https://arxiv.org/pdf/1905.02167.pdf>. -/
def hedetniemi : Prop :=
n = min n₁ n₂

lemma chromatic_number_prod_le_min : n ≤ min n₁ n₂ :=
begin
obtain ⟨f₁, hf₁⟩ : ∃ f₁ : V₁ → ℕ, is_nat_colouring n₁ G₁ f₁ := h₁.col_exists,
obtain ⟨f₂, hf₂⟩ : ∃ f₂ : V₂ → ℕ, is_nat_colouring n₂ G₂ f₂ := h₂.col_exists,
have c₁ : is_nat_colouring n₁ (G₁.prod G₂) (f₁ ∘ _) := hf₁.comp (prod.fst G₁ G₂),
have c₂ : is_nat_colouring n₂ (G₁.prod G₂) (f₂ ∘ _) := hf₂.comp (prod.snd G₁ G₂),
rw le_min_iff,
split,
{ exact h.min c₁ },
{ exact h.min c₂ }
end

end hedetniemi

end graph


#### Bhavik Mehta (Mar 26 2020 at 21:00):

I'm not sure if it would be useful for this, but just adding the tiny amount of graph theory I've done in case some of it helps: the handshaking lemma and a few finite Ramsey results for graphs, a different form of finite Ramsey for graphs and the pigeonhole principle, and infinite Ramsey for hypergraphs

#### Bhavik Mehta (Mar 26 2020 at 21:19):

Yup, my bad, I forgot what multigraph means

#### Scott Morrison (Mar 26 2020 at 22:51):

@Johan Commelin, this looks great. Put it on a branch so we can start hacking?

#### Johan Commelin (Mar 27 2020 at 05:54):

I just pushed to hedetniemi

#### Johan Commelin (Mar 27 2020 at 05:54):

There is a new graph_theory directory.

#### David Wärn (Mar 27 2020 at 09:58):

Can you prove that chromatic number is at most max degree plus one?

#### Johan Commelin (Mar 27 2020 at 10:15):

I haven't defined max degree yet (-;

#### Johan Commelin (Mar 27 2020 at 10:15):

I just proved that every colouring on the exponential graph can be turned into a suited one.

#### Johan Commelin (Mar 27 2020 at 10:51):

I pushed a proof of "Observation 1"

#### Vaibhav Karve (Mar 27 2020 at 18:17):

@Johan Commelin Thank you starting this! I have some basic definitions too. I was aiming towards two targets so far:

1. Seven Bridges of Königsberg because this problem is also on the 100 theorems list.
2. Results about Graph-satisfiability because this is my research -- but this will need lot more in terms of definitions.

#### Vaibhav Karve (Mar 27 2020 at 18:19):

import data.set.basic data.multiset data.finset data.fintype
import set_theory.cardinal
import logic.function logic.relation

import tactic tactic.elide tactic.find

namespace graph

variables {V : Type*}

structure digraph (V : Type*) :=
(adj : V → V → Prop)

@[reducible] def pair (V : Type*) := V × V
@[reducible] def is_edge (dg : digraph V) : pair V → Prop :=
function.uncurry' dg.adj  -- uncurry only works on Types.
-- uncurry' works on Sorts.
-- use uncurry'.

instance (dg : digraph V) [decidable_eq V] : decidable_eq (pair V) :=
by apply_instance

instance (dg : digraph V) [decidable_rel dg.adj] : decidable_pred (is_edge dg) :=
begin
unfold is_edge,
unfold function.uncurry',
apply_instance,
end

structure graph (V : Type*) extends (digraph V) :=

structure weighted_digraph (V W : Type*) extends (digraph V), (has_zero W) :=
(weight (v w : V) : W)
(weight_hom (v w : V) : ¬ adj v w → weight v w = 0)

structure weighted_graph (V W : Type*) extends weighted_digraph V W :=
(weight_symm (e : pair V) : weight e.1 e.2 = weight e.2 e.1)

def multi_digraph (V : Type*) := weighted_digraph V ℕ
def multi_graph (V : Type*) := weighted_graph V ℕ

def order {graph_type : Type* → Type*} (g : graph_type V) [fintype V] : ℕ :=
fintype.card V

@[reducible] def edges_digraph (dg : digraph V) : Type* :=
{e : pair V // is_edge dg e}

instance dec_eq_V_implies_dec_eq_edges_digraph
(dg : digraph V) [decidable_eq V] : decidable_eq (edges_digraph dg) :=
by apply_instance

(dg : digraph V) [fintype V] [decidable_rel dg.adj] :
fintype (edges_digraph dg) :=
by exact subtype.fintype _

def size_digraph (dg : digraph V) [fintype V] [decidable_rel dg.adj] : ℕ :=
fintype.card (edges_digraph dg)


#### Kevin Buzzard (Mar 27 2020 at 18:25):

You're the guy who spoke about this stuff in Pittsburgh right? Nice job getting the publication :-)

#### Johan Commelin (Mar 27 2020 at 18:25):

maybe we should all dump our code in the graph_theory folder of the hedetniemi branch. And then try to sort out the common definitions.

#### David Wärn (Mar 27 2020 at 20:01):

There's a definition of paths now that could be used for formalizing Königsberg

#### Scott Morrison (Mar 28 2020 at 03:19):

@David Wärn, in

def to_category : V ⥤ C :=
{ obj := f_obj,
map := λ a b p, to_hom f_obj @f_edge p,
map_comp' := λ _ _ _ _ _, to_hom.comp _ _ _ _ }

lemma to_category.obj : (to_category f_obj @f_edge).obj = f_obj := rfl
lemma to_category.map {a b} (p : G.path a b) :
(to_category f_obj @f_edge).map p = to_hom f_obj @f_edge p := rfl
rfl

1. You should make these lemmas simp lemmas!
2. Instead you can just write:
@[simps]
def to_category : V ⥤ C :=
{ obj := f_obj,
map := λ a b p, to_hom f_obj @f_edge p,
map_comp' := λ _ _ _ _ _, to_hom.comp _ _ _ _ }


which will automatically synthesize those lemmas for you.

#### Scott Morrison (Mar 28 2020 at 03:37):

@David Wärn, @Johan Commelin why do you have this messed up design where graph is sometimes a class, and sometimes not? It is a mess.

#### Scott Morrison (Mar 28 2020 at 03:37):

It will be so much easier if we just make up our minds. :-) Either way is viable, but at present the code switched back and forth.

#### Scott Morrison (Mar 28 2020 at 04:02):

Ok. It is no longer a class, and the "path category" David defined now used a type synonym, and has been cleaned up.

#### Scott Morrison (Mar 28 2020 at 04:27):

I've also moved the path category to a separate file. While I'm happy to have it, it's not very useful for doing graph theory. :-)

#### Scott Morrison (Mar 28 2020 at 04:27):

(Someone should use it however to prove the presentation of the simplex category, for when we start doing homological algebra!)

okay :-)

#### Johan Commelin (Mar 28 2020 at 06:07):

It's not clear to me what the best approach is (-;

#### Scott Morrison (Mar 28 2020 at 06:07):

well, I made up my mind :-)

#### Johan Commelin (Mar 28 2020 at 06:07):

I think in the end maybe tc is not the right approach here

#### Scott Morrison (Mar 28 2020 at 06:07):

I was just writing the statement of the Konigsberg problem

#### Scott Morrison (Mar 28 2020 at 06:07):

and realised the setup you sketched can't talk about undirected multigraphs

#### Scott Morrison (Mar 28 2020 at 06:08):

so I was thinking about doing that

#### Scott Morrison (Mar 28 2020 at 06:08):

but it is not super pretty

#### Scott Morrison (Mar 28 2020 at 06:08):

My proposal is

structure directed_multigraph (V : Type u) :=
(edge : V → V → Sort v)

def directed_multigraph.vertices {V : Type u} (G : directed_multigraph V) := V

structure multigraph (V : Type u) extends directed_multigraph V :=
(symm : Π (x y), edge x y ≃ edge y x)

structure directed_graph (V : Type u) extends directed_multigraph.{0} V.

def directed_graph.vertices {V : Type u} (G : directed_graph V) := V

structure graph (V : Type u) extends directed_graph V, multigraph V.


but then all the symm fields of graph become more work than they used to be

#### Scott Morrison (Mar 28 2020 at 06:08):

but perhaps a helper function does it

#### Scott Morrison (Mar 28 2020 at 06:09):

Ah --- let's call symm on multigraph involution, then define symm as a new field on graph, and provide a default value of symm in terms of it

That sounds good

#### Johan Commelin (Mar 28 2020 at 06:11):

And then a custom mk' that takes edge and symm and builds involution if you want to make a graph?

#### Scott Morrison (Mar 28 2020 at 06:11):

no, it's even easier than that

#### Johan Commelin (Mar 28 2020 at 06:11):

Ok, note that I just pushed.

#### Johan Commelin (Mar 28 2020 at 06:11):

A little commit to the end of that file.

#### Scott Morrison (Mar 28 2020 at 06:12):

graph will actually have two fields, symm, inv, and inv will just receive a default value in terms of symm

#### Johan Commelin (Mar 28 2020 at 06:12):

We should probably split the file now...

#### Scott Morrison (Mar 28 2020 at 06:12):

so the constructor will look the same

#### Johan Commelin (Mar 28 2020 at 06:12):

Aah, inv will get the default value. Sure.

#### Johan Commelin (Mar 28 2020 at 06:13):

One thing that isn't clear to me if we drop the tc approach is how easy it will be to apply statements about directed multigraphs to ordinary graphs.

#### Johan Commelin (Mar 28 2020 at 06:13):

Do we manually need to apply coercions?

#### Johan Commelin (Mar 28 2020 at 06:16):

@Scott Morrison Are you making this change atm?

yes

Cool

#### Johan Commelin (Mar 28 2020 at 06:17):

Did you see Vaibhav's code upstairs? He also has definitions of weighted graphs. I hope we can fit those in the mix.

#### Scott Morrison (Mar 28 2020 at 06:42):

Gah, I made the mistake of thinking "oooh, this belongs in data/equiv/basic, I'll just pop it in there". And now everything is recompiling.

I committed

#### Scott Morrison (Mar 28 2020 at 07:08):

I managed to state konigsberg in the current setup, and it locally doesn't look too bad:

def KonigsbergBridges : multigraph (fin 4) :=
multigraph_of_edges [(0,1), (0,2), (0,3), (1,2), (1,2), (2,3), (2,3)]

def KonigsbergBridgesProblem : Prop :=
¬ is_Eulerian KonigsbergBridges


#### Scott Morrison (Mar 28 2020 at 07:09):

using

def multigraph_of_edges {n : ℕ} (e : list (fin n × fin n)) : multigraph (fin n) :=
{ edge := λ x y, fin (e.countp (λ p, p = (x, y) ∨ p = (y, x))),
inv := λ x y, by { convert equiv.refl _, funext, rw or_comm, } }


to construct the graph from a list of edges

#### Scott Morrison (Mar 28 2020 at 07:10):

But it's absolutely disgusting that I have to have a coercion from multigraph to directed_multigraph

#### Scott Morrison (Mar 28 2020 at 07:10):

and struggling to make that coercion fire makes things ugly

#### Johan Commelin (Mar 28 2020 at 07:53):

@Scott Morrison Thanks!

#### Johan Commelin (Mar 28 2020 at 07:53):

Cleaning up the coercion issues seems to be an important issue

#### David Wärn (Mar 28 2020 at 09:00):

@Scott Morrison This looks good!

#### David Wärn (Mar 28 2020 at 09:03):

If you defined Eulerian paths by counting edge occurrences and demanding that the counts are all 1 : nat, then you could prove non-Eulerianess by appeal to the universal property of the path category, but maybe this is silly.

#### David Wärn (Mar 28 2020 at 09:11):

(Specifically, the two maps sending a path p : G.path x y to the additive monoid V -> zmod 2 given by "taking edge counts adjacent to a vertex" and "adding x and y", respectively, agree)

#### David Wärn (Mar 28 2020 at 09:14):

Shouldn't multigraph have a condition that inv (inv e) = e?

#### Mario Carneiro (Mar 28 2020 at 09:18):

At the risk of being "that guy", I think that this metamath proof of konigsberg is particularly relevant for this discussion. It appears that I used a list of unordered pairs (or rather, a function from some index set to unordered pairs) for the edge function.

#### Mario Carneiro (Mar 28 2020 at 09:19):

this is actually one of my favorite examples of computable data structures in metamath

#### Johan Commelin (Mar 28 2020 at 09:59):

@Mario Carneiro Do you have input on the general setup of the hierarchy of graphy definitions?

#### Mario Carneiro (Mar 28 2020 at 09:59):

I am growing more and more fond of the approach that doesn't bother with unifying different notions of graph

#### Mario Carneiro (Mar 28 2020 at 10:00):

use whatever is most convenient for the theorem in front of you

#### Mario Carneiro (Mar 28 2020 at 10:02):

In this case, a reasonable substitute for unordered pairs is the quotient of A x A by swap

#### Johan Commelin (Mar 28 2020 at 10:02):

And manually apply a functor when you need it...

#### Johan Commelin (Mar 28 2020 at 10:04):

@Scott Morrison That change to data/equiv is already part of an existing PR to mathlib, right?

yes

#### Johan Commelin (Mar 28 2020 at 10:04):

I hope it gets merged quickly (-;

#### Scott Morrison (Mar 28 2020 at 10:05):

You know that CI builds all branches?

#### Scott Morrison (Mar 28 2020 at 10:05):

So leanproject up should get you oleans.

#### Scott Morrison (Mar 28 2020 at 10:06):

and indeed, they are available now

#### Johan Commelin (Mar 28 2020 at 10:08):

I did leanproject get-cache which didn't work

#### Johan Commelin (Mar 28 2020 at 10:09):

But I was on a wrong commit... it seems

#### Johan Commelin (Mar 28 2020 at 10:19):

I have a one-line proof saying

repeat {apply or.imp <|> apply and.imp <|> apply edge.symm <|> apply eq.symm },


I thought that solve_by_elim should do this, but it didn't. What is the recommended way of writing this proof? Or is this the idiomatic, optimal form?

#### Scott Morrison (Mar 28 2020 at 10:20):

Are you sure? solve_by_elim [or.imp, and.imp, edge.symm, eq.symm] {max_steps:=100}?

#### Scott Morrison (Mar 28 2020 at 10:20):

max_steps got renamed recently, it may be something else still

#### Scott Morrison (Mar 28 2020 at 10:21):

solve_by_elim has a very conservative default for max_steps.

#### Johan Commelin (Mar 28 2020 at 10:25):

This doesn't work:

def strong_prod (G₁ : graph V₁) (G₂ : graph V₂) : graph (V₁ × V₂) :=
{ edge := assume p q,
((p.1 ~[G₁] q.1) ∧ (p.2 ~[G₂] q.2)) ∨
((p.1 = q.1) ∧ (p.2 ~[G₂] q.2)) ∨
((p.1 ~[G₁] q.1) ∧ (p.2 = q.2)),
symm := assume p q, by
{ solve_by_elim only [or.imp, and.imp, edge.symm, eq.symm] { max_steps := 100 } } }


#### Johan Commelin (Mar 28 2020 at 10:25):

I don't understand why.

#### Johan Commelin (Mar 28 2020 at 10:25):

I think 20 applys are more than enough.

#### Scott Morrison (Mar 28 2020 at 10:33):

commit something with the repeat { apply ... } proof and I'll see if I can get solve_by_elim going.

#### Johan Commelin (Mar 28 2020 at 10:39):

Scott Morrison said:

commit something with the repeat { apply ... } proof and I'll see if I can get solve_by_elim going.

Done.

#### Scott Morrison (Mar 28 2020 at 10:54):

hmm, okay, I don't see it yet.

#### Scott Morrison (Mar 28 2020 at 10:54):

by the way, did you notice the new show_term tactic?

#### Scott Morrison (Mar 28 2020 at 10:54):

 by show_term { repeat {apply or.imp <|> apply and.imp <|> apply edge.symm <|> apply eq.symm } }


#### Scott Morrison (Mar 28 2020 at 10:54):

it is a 3 line tactic, but also the best thing since sliced bread :-)

#### Scott Morrison (Mar 28 2020 at 11:00):

I need to sleep. Could you put a TODO: Scott, diagnose why solve_by_elim can't do this note at that line, and I'll try again with the latest version of solve_by_elim?

#### Johan Commelin (Mar 28 2020 at 11:02):

Ok, I'll do that. And thanks for show_term!

#### Johan Commelin (Mar 28 2020 at 11:03):

Sleep tight. See you tomorrow morning (-;

#### Scott Morrison (Mar 28 2020 at 11:48):

(Definitely a solve_by_elim bug, thank you.

solve_by_elim only [or.imp, and.imp, edge.symm, edge.symm, edge.symm, edge.symm, eq.symm, eq.symm] {max_steps:=15}


works. Something is going wrong with metavariables getting stuck between one application and the next.)

#### Patrick Massot (Mar 28 2020 at 11:49):

Aren't you sleeping?

#### Scott Morrison (Mar 28 2020 at 11:49):

Minimised as

example (P : ℕ → Type) (f : Π {n : ℕ}, P n) : P 2 × P 3 :=
begin
fsplit,
solve_by_elim* only [f], -- fails!
solve_by_elim* only [f, f]
end


:-)

#### Johan Commelin (Mar 28 2020 at 12:07):

Scott is a very effective sleeper (-;

#### David Wärn (Mar 29 2020 at 16:20):

inductive path : V → V → Type (max v u)
| nil  : Π (h : V), path h h
| cons : Π {h s t : V} (e : G.edge h s) (l : path s t), path h t


should this be defined differently to enable based path recursion?

#### Scott Morrison (Mar 30 2020 at 03:58):

Can't you do path based recursion with that? I don't understand.

#### Scott Morrison (Mar 30 2020 at 03:59):

Try cases p or induction p when p is a path?

#### David Wärn (Mar 30 2020 at 08:00):

For example this doesn't work:

def length' (t : V) : Π s (p : G.path s t), ℕ
| _ (path.nil _ _) := 0
| _ (_ :: p) := length' _ p


I get failed to prove recursive application is decreasing.

#### Kenny Lau (Mar 30 2020 at 08:08):

def length' (V : Type u) (G : graph V) (s t : V) (p : path V G s t) : ℕ :=
path.rec_on p (λ s t, 0) (λ h s t e p f t, f t + 1) s


#### Kenny Lau (Mar 30 2020 at 08:12):

def length : Π s t (p : G.path s t), ℕ
| _ _ (graph.path.nil G h) := 0
| x y (graph.path.cons e p) := length _ _ p + 1


#### Kenny Lau (Mar 30 2020 at 08:12):

looks like you need to put t inside the recursion as well

#### David Wärn (Mar 30 2020 at 08:21):

Yes, this works here. So path.rec does constructions on all paths, not on all paths ending at a specific vertex. What do I do if have a some assumptions about a specific vertex, and want to prove something that only makes sense for paths ending at that vertex?

#### David Wärn (Mar 30 2020 at 08:29):

You can do this:

def based_rec' : Π (s t : V) (p : G.path s t) (C : Π s' (p' : G.path s' t), Sort*)
(hn : C t (path.nil _ _)) (hc : Π s' m (e : G.edge s' m) (l : G.path m t),
C m l → C s' (e::l)), C s p
| _ _ (path.nil _ _) C hn _ := hn
| s t (@path.cons _ _ _ m _ e l) C hn hc := hc s m e l (based_rec' m t l C hn hc)

def based_rec_on {t : V} {C : Π s (p : G.path s t), Sort*} {s} (p : G.path s t)
(hn : C t (path.nil _ _)) (hc : Π s m (e : G.edge s m) (l : G.path m t),
C m l → C s (e::l)) : C s p :=
based_rec' s t p C hn hc


But I feel like this is a problem that the equation compiler should solve

#### Kevin Buzzard (Mar 30 2020 at 08:32):

I guess I would be more interested in just having the interface available to me rather than caring about what the equation compiler can do

#### David Wärn (Mar 30 2020 at 08:38):

I guess that makes sense. You'd need some sort of interface anyway e.g. for recursion on paths starting at a specific vertex; might as well make it symmetric

#### Kevin Buzzard (Mar 30 2020 at 08:42):

Of course there are those who are excited by the equation compiler. They tend to be the more computer science folk. I've seen the equation compiler solving some tricky problems before in a very efficient manner. But I don't even teach it to people at Xena, it tends not to come up in generic maths unless you're doing some kind of fancy induction which seems to be more commonplace in CS style constructions than mathematical ones.

#### Kevin Buzzard (Mar 30 2020 at 08:43):

In maths it's always just induction on size of thing

#### Reid Barton (Mar 30 2020 at 12:19):

I think this is happening because both s and t occur to the right of the colon in the definition of path

#### David Wärn (Mar 30 2020 at 12:57):

I think so too. With

inductive path' (s : V) : V → Type (max v u)
| nil : path' s
| app {h t} (p : path' h) (e : G.edge h t) : path' t


you get a based path recursor path'.rec

#### Johan Commelin (Mar 31 2020 at 08:55):

I've created two files basic.lean and chromatic_number.lean.

#### Bhavik Mehta (Mar 31 2020 at 13:18):

Out of interest, why not use list.chain G.edge instead of defining a new thing? list.chain already comes with a bunch of lemmas to work with it

#### Mario Carneiro (Mar 31 2020 at 13:20):

there is also something about transitive closure of a relation

#### Mario Carneiro (Mar 31 2020 at 13:22):

refl_trans_gen and trans_gen in logic.relation

#### Mario Carneiro (Mar 31 2020 at 13:26):

list.chain' is better if you want the path itself as a list, while refl_trans_gen G.edge will give you the path' inductive type above

#### Mario Carneiro (Mar 31 2020 at 13:27):

in particular, the library provides the ability to do recursion on either the head or the tail of the path, as well as proving that two paths make a path

#### David Wärn (Mar 31 2020 at 13:28):

Isn't refl_trans_gen Prop-valued?

#### Mario Carneiro (Mar 31 2020 at 13:29):

oh that's true, this is the "there is a path" relation

#### Mario Carneiro (Mar 31 2020 at 13:29):

list.chain' will give you the path itself

#### David Wärn (Mar 31 2020 at 13:34):

I didn't know list.chain existed! I guess this gives an untyped definition of paths. It's not clear to me that it would be easier to work with. But I guess if you prove that any path can be expressed as a list, then you'll be able to do recursion?

#### Bhavik Mehta (Mar 31 2020 at 13:42):

import logic.relation
import data.list
universe u

structure graph (α : Type*) :=
(edge : α → α → Prop)
(loopless : irreflexive edge)
(undirected : symmetric edge)

variables {α : Type u} (G : graph α)

lemma symmetric_edge : symmetric G.edge := G.undirected

def connected : α → α → Prop := relation.refl_trans_gen G.edge

lemma conn_symm : symmetric (connected G) := λ x y h,
begin
induction h,
apply relation.reflexive_refl_trans_gen,
apply G.undirected, assumption,
assumption
end
lemma equiv_con : equivalence (connected G) :=
begin
split,
exact relation.reflexive_refl_trans_gen,
split,
apply conn_symm,
exact relation.transitive_refl_trans_gen,
end

def is_path_from (a : α) : list α → Prop := list.chain G.edge a

lemma path_implies_connected (a : α) (p : list α) (hp₁ : is_path_from G a p) (hp₂ : p ≠ list.nil) :
connected G a (list.last p hp₂) :=
begin
rw is_path_from at hp₁,
induction p with b c h k l generalizing a,
{ exfalso, apply hp₂, refl },
cases hp₁,
cases c,
rw list.last_singleton,
apply relation.refl_trans_gen.single,
assumption,
rw list.last_cons_cons,
clear hp₂,
apply h,
assumption
end

lemma connected_gives_path [decidable_eq α] (a b : α) (h : connected G a b) (diff : a ≠ b) :
∃ (p : list α) (hp : p ≠ list.nil), list.last p hp = b ∧ is_path_from G a p :=
begin
rw is_path_from,
revert diff,
intro, exfalso, apply diff, refl,
clear h a,
intros c d e t ih cb,
by_cases d = b,
refine ⟨[d], list.cons_ne_nil _ _, h, _⟩,
rwa list.chain_singleton,
obtain ⟨p, hp₁, hp₂, hp₃⟩ := ih h,
refine ⟨d :: p, list.cons_ne_nil _ _, _, _⟩,
rwa list.last_cons _ hp₁,
rw list.chain_cons,
split,
assumption,
assumption
end


I put this together a while ago, I think you're using a different definition of graph but it might still be helpful

#### Bhavik Mehta (Mar 31 2020 at 13:43):

In particular I defined connected as the reflexive transitive closure of edge, and showed that it's equivalent to having a path in the sense of list.chain

#### Mario Carneiro (Mar 31 2020 at 13:43):

@David Wärn If you want a type of paths, you can define path a b := {l // list.chain G.edge l a b}

#### David Wärn (Mar 31 2020 at 13:47):

Ah. This definition makes a lot of sense for graphs without multiplicity

#### Mario Carneiro (Mar 31 2020 at 13:48):

Oh, that's a good point. I think in the metamath version I had to define a path as an alternating sequence of edges and vertices

#### Mario Carneiro (Mar 31 2020 at 13:51):

If G.edge is not prop-valued, then probably your inductive type is the simplest way to define this in lean

#### David Wärn (Mar 31 2020 at 13:53):

I guess the alternative would be to define the total type of edges, and a compatibility relation on it, and define a total type of paths using list.chain on this. I think it would make sense to prove that the inductive definition is equivalent to this

#### Kevin Buzzard (Mar 31 2020 at 14:23):

If you want a graph theory challenge, can you prove that a tree with $n$ vertices has $n-1$ edges?

#### Kevin Buzzard (Mar 31 2020 at 14:23):

I leave it to Mario to tell us what I am asserting in the impossible case where the tree has 0 vertices.

#### Johan Commelin (Mar 31 2020 at 14:24):

The empty tree has 37 edges... this was proven by Erdos several decades ago.

#### Sebastien Gouezel (Mar 31 2020 at 14:49):

If you're a crazy algebraist, the answer to this problem is to say that a graph with 0 vertices is not a tree.

Yes of course

#### Kevin Buzzard (Mar 31 2020 at 14:49):

this is why it can have 37 edges

#### Kevin Buzzard (Mar 31 2020 at 14:50):

@Shing Tak Lam just ran into the same issue in #2298 when trying to differentiate $X^0$, and deciding that it was $0\times X^{0-1}=0\times X^{37} = 0$.

#### David Wärn (Mar 31 2020 at 14:53):

We don't have trees yet, but there's rooted trees, or "arborescences". At some point you should be able to prove that any tree can be rooted at any vertex to give an arborescence, and the edge-counting result should follow

#### Johan Commelin (Mar 31 2020 at 17:17):

@Bhavik Mehta @David Wärn I would love to know whether you can integrate your definitions of graphs with the stuff in basic.lean. If so, I think we might have stuff for a 1st PR.

#### David Wärn (Mar 31 2020 at 19:39):

I pushed some things to arborescences.lean a while ago that might be useful for proving existence of spanning tree. It uses the definition of directed_multigraph from basic.lean

#### Johan Commelin (Mar 31 2020 at 20:27):

I finished a global framework of Shitov's proof. Now we just need to fill in some sorrys :rolling_on_the_floor_laughing: .
Among them a theorem by Erdos, saying that there exist finite graphs with arbitrary high girth and fractional chromatic number.

#### Scott Morrison (Apr 01 2020 at 05:48):

I pushed a refactor of (multi)chromatic numbers. No new content, just slicker proofs. This comes at the expense of a new to_mathlib file, with all the stuff that I found was missing all over finset/fintype/function.embedding...

#### Johan Commelin (Apr 01 2020 at 05:51):

@Scott Morrison Thanks, I'm taking a look right now!

#### Johan Commelin (Apr 01 2020 at 05:52):

I think we should PR changes outside graph_theory/ as soon as possible.

#### Johan Commelin (Apr 01 2020 at 06:01):

One of the gaps that needs to be filled in is the existence of the fractional chromatic number... I do not yet have a good idea how to do that.

#### Scott Morrison (Apr 01 2020 at 06:03):

The only proof I know of this is via the linear programming definition of the fractional chromatic number...

#### Scott Morrison (Apr 01 2020 at 06:04):

and the observation that the vertices of a polyhedron cut out by rational inequalities have rational coordinates

#### Scott Morrison (Apr 01 2020 at 06:04):

that seems like a lot of machinery we don't have yet

#### Johan Commelin (Apr 01 2020 at 06:04):

Is there an easy argument why it exists as a real number?

#### Scott Morrison (Apr 01 2020 at 06:05):

there's an easy lower bound, take the inf?

#### Johan Commelin (Apr 01 2020 at 06:05):

Right... of course :face_palm:

#### Scott Morrison (Apr 01 2020 at 06:07):

Regarding the to_mathlib file. I suggest whenever someone is bored (I realise I made the mess and should clean it up, but I can hope), we move these lemmas to their natural homes in mathlib, still in the hedetniemi branch.

#### Scott Morrison (Apr 01 2020 at 06:08):

Then we can make one or more PRs by checking out non graph_theory directories into new branches

#### Johan Commelin (Apr 01 2020 at 06:09):

But since mathlib moves fast, we better try to do this regularly. Also, big to_mathlib files never get PR'd (see perfectoid project...)

#### Johan Commelin (Apr 01 2020 at 08:39):

Lol.... we have a bug: all fractional chromatic numbers are zero:

lemma is_frac_chromatic_number_eq_zero (G : graph V) {q : ℚ} (h : is_frac_chromatic_number G q) :
q = 0 :=
begin
apply le_antisymm _ (h.nonneg),
suffices c : nat_multicolouring 1 0 G,
{ have := h.min c, simpa only [nat.cast_zero, div_zero] },
refine ⟨λ x, ⟨∅, finset.card_empty⟩, _⟩,
assume x y e, show disjoint ∅ ∅, rw disjoint_self, refl
end


#### Johan Commelin (Apr 01 2020 at 09:04):

I've pushed a bugfix

#### David Wärn (Apr 01 2020 at 09:39):

@Johan Commelin do you think it would be feasible to formalize Erdos' probabilistic method to show that there are graphs of large girth and small independence number?

#### Johan Commelin (Apr 01 2020 at 09:41):

I think it would be very interesting to try that. It's one of those methods where I don't see how to formalise it in a user-friendly way.

#### Johan Commelin (Apr 01 2020 at 09:44):

For the record, for others interested in this, we're talking about papers like

#### David Wärn (Apr 01 2020 at 14:02):

I suppose there is a general question of how to deal with concrete random variables on a fixed probability space, and how to compute expectations. Something something monadic computation? Other than that the method relies on reasoning about rates of growth of various functions, and things like "if this event has non-zero probability, then here's a point in the sample space where it happens", or "given $E(X) > E(Y)$, here's a point in the sample space where $X > Y$"

#### Johan Commelin (Apr 01 2020 at 14:17):

I think it would be a lot of fun to make this usable

#### Johan Commelin (Apr 01 2020 at 14:17):

We have something called the Giry monad. I've no clue if it would help in making a usable api here.

#### Kevin Buzzard (Apr 01 2020 at 16:35):

I always had the impression that the random graph method was really just using the language of probability theory rather than actually using any measure theory. It's just a way of explaining counting arguments in a way which is intuitive to humans.

#### David Wärn (Apr 01 2020 at 16:43):

Well yes, all sets involved are finite and so everything is measurable

#### David Wärn (Apr 01 2020 at 16:47):

My guess is that the difficulty will be something like this: suppose you define a function F that takes a graph on n vertices and returns the number of g-cycles. Then you define a probability measure on the set of graphs on n vertices (or a family of weights on the finite set if you like). How do you actually reason about the expectation of F(G)? You'll need to unfold the definition of F somehow, this time being careful about probabilities and expectations

#### David Wärn (Apr 01 2020 at 16:49):

Maybe this is the way to go. But maybe it's better to define F as a random variable (or probability distribution) to begin with, in a monadic context?

#### Bhavik Mehta (Apr 01 2020 at 16:59):

I've scrapped together an incredibly messy proof for a ramsey lower bound (that is, R(s) >= Omega(2^(s/2))) - there's one sorry in there but it should be just a calculation and i've sketched the idea in comments. The idea is exactly as Kevin says, I didn't use any ideas of probability, just counting the size of finsets - but the core idea is the standard probabilistic argument

#### Bhavik Mehta (Apr 01 2020 at 17:02):

I personally feel that if you're doing an argument which involves probability on finite sets, you're better off just using counting arguments on finsets and removing all probability language, but this might be just because I've done a lot of stuff with finsets in lean

#### Scott Morrison (Apr 02 2020 at 07:16):

@Johan Commelin, the lemma whut should just come from the fact that every k-colouring of G.strong_prod (K_ n) gives an (n,k)-multicolouring of G, by taking all the colours in a fibre.

#### Scott Morrison (Apr 02 2020 at 07:16):

I've stubbed this out in the branch, although something mysteriously doesn't typecheck, and there are some new sorries.

#### Scott Morrison (Apr 02 2020 at 07:27):

Fixed the typechecking issue. All these predicates is_chromatic_number G k seem like more trouble than they're worth.

#### Johan Commelin (Apr 02 2020 at 07:35):

Maybe... I know that in the perfectoid project is was happy with char_p R p instead of ring_char R. The problem with the latter is that you will have R → A → B and you will need to rewrite along ring_char R = ring_char A = ring_char B all the time, and sometimes your motive will not be correct etc... So then it helps if you just have p everywhere.
But maybe this is less of an issue with chromatic numbers.

#### Johan Commelin (Apr 02 2020 at 07:36):

Also, thanks for sketching a proof of whut, I'll look at it as soon as my github inbox is empty

:fencing:

#### Johan Commelin (Apr 02 2020 at 08:51):

@Scott Morrison The reason is again classical.decidable*

#### Johan Commelin (Apr 02 2020 at 08:52):

@multicolouring V
(fin
(@chromatic_number (V × fin n) (@prod.fintype V (fin n) _inst_1 (fin.fintype n))
(@strong_prod V (fin n) G (K_ n))
_))
(λ
(a b :
fin
(@chromatic_number (V × fin n) (@prod.fintype V (fin n) _inst_1 (fin.fintype n))
(@strong_prod V (fin n) G (K_ n))
_)), classical.prop_decidable (a = b))
n
G


versus

@multicolouring V
(fin
(@chromatic_number (V × fin n) (@prod.fintype V (fin n) _inst_1 (fin.fintype n))
(@strong_prod V (fin n) G (K_ n))
_))
(λ
(a b :
fin
(@chromatic_number (V × fin n) (@prod.fintype V (fin n) _inst_1 (fin.fintype n))
(@strong_prod V (fin n) G (K_ n))
_)),
fin.decidable_eq
(@chromatic_number (V × fin n) (@prod.fintype V (fin n) _inst_1 (fin.fintype n))
(@strong_prod V (fin n) G (K_ n))
_)
a
b)
n
G


#### Johan Commelin (Apr 02 2020 at 08:55):

If you use

  obtain ⟨c⟩ := hn.col_exists,
let mc := multicolouring_of_strong_prod_K_colouring c,
let mc' : nat_multicolouring k n G,
{ delta nat_multicolouring,
exact mc }
have := hχ.min,


then the error will be very clear.

And upsetting.

#### Johan Commelin (Apr 02 2020 at 09:01):

@Scott Morrison So... what do we do with

  @multicolouring V (fin k) (λ (a b : fin k), classical.prop_decidable (a = b)) n G
but is expected to have type
@multicolouring V (fin k) (λ (a b : fin k), fin.decidable_eq k a b) n G


#### Johan Commelin (Apr 02 2020 at 09:01):

Just make everything classical?

#### Johan Commelin (Apr 02 2020 at 09:02):

And ignore the fact that people might want to use decidability in the proof of Königsberg?

#### Johan Commelin (Apr 02 2020 at 09:08):

Ok, I've fixed this issue. (For now...)

#### Johan Commelin (Apr 02 2020 at 09:09):

See the commit I pushed.

#### Scott Morrison (Apr 02 2020 at 09:09):

I'm confused. What did you fix? I thought I'd fixed the typechecking problem already.

#### Johan Commelin (Apr 02 2020 at 09:10):

Ooh, wait, now I see there is a conflict...

#### Scott Morrison (Apr 02 2020 at 09:13):

I see how to resolve the conflict, but I'm not sure if you're in the midst of it already.

#### Kenny Lau (Apr 02 2020 at 09:14):

Then you can resolve the conflict that arises from the resolution of conflicts

#### Johan Commelin (Apr 02 2020 at 09:14):

@Scott Morrison I've pushed

#### Johan Commelin (Apr 02 2020 at 09:15):

Now there is no convert anymore

#### Scott Morrison (Apr 02 2020 at 09:15):

but there's also no proof?

#### Scott Morrison (Apr 02 2020 at 09:16):

it looks like in what you pushed you make less progress on the proof that we used to

#### Scott Morrison (Apr 02 2020 at 09:17):

oh, my mistake, ignore me

#### Scott Morrison (Apr 02 2020 at 09:17):

so great I couldn't even see where the proof was happening :-)

#### Johan Commelin (Apr 02 2020 at 09:18):

  have npos : 0 < n := sorry,
obtain ⟨c⟩ := hn.col_exists,
let mc := multicolouring_of_strong_prod_K_colouring c,
have := hχ.min mc npos,
rwa le_div_iff at this,
assumption_mod_cast,


#### Johan Commelin (Apr 02 2020 at 09:18):

Now we only need to argue that n is positive

#### Scott Morrison (Apr 02 2020 at 09:18):

So what's going on with helpme?

#### Johan Commelin (Apr 02 2020 at 09:19):

I think Shitov is not very careful there, but probably taking a slightly bigger c or something will make things work. I haven't thought about the issue yet.

#### Scott Morrison (Apr 02 2020 at 09:20):

In Erdos's theorem, why do you introduce the n?

#### Johan Commelin (Apr 02 2020 at 09:20):

Sorry, I meant a bigger q

#### Scott Morrison (Apr 02 2020 at 09:21):

Oh, I see, girth is only a predicate, not a function.

#### Scott Morrison (Apr 02 2020 at 09:21):

I'm really unconvinced by all these predicates.

#### Johan Commelin (Apr 02 2020 at 09:22):

I understand. For char_p it was really helpful. Here maybe less. I don't know.

#### Johan Commelin (Apr 02 2020 at 09:28):

@Scott Morrison Done

-- Scott: @Johan, why all these predicates?
-- Why not just write frac_chromatic_number G * n ≤ chromatic_number (G.strong_prod (K_ n))
lemma whut [fintype V] (G : graph V) (n : ℕ) {k : ℕ} {χ : ℚ}
(hk : is_chromatic_number (G.strong_prod (K_ n)) k) (hχ : is_frac_chromatic_number G χ) :
χ * n ≤ k :=
begin
by_cases hn : n = 0, { simp [hn] },
replace hn : 0 < n := nat.pos_of_ne_zero hn,
obtain ⟨c⟩ := hk.col_exists,
let mc := multicolouring_of_strong_prod_K_colouring c,
have := hχ.min mc hn,
rwa le_div_iff at this,
assumption_mod_cast,
end


Pushed

#### Scott Morrison (Apr 02 2020 at 09:32):

So... if I can take the current framework and de-predicate it, that would be okay? The remaining holes in the proof have nothing to do with the predicate stuff, right?

#### Scott Morrison (Apr 02 2020 at 09:32):

I really don't know what's happening with helpme, still. It looks alarming, but I have very little sense of the overall proof at this point.

#### Scott Morrison (Apr 02 2020 at 09:34):

Another design question: can't we just bundle is_loopless into a simple_graph?

#### Scott Morrison (Apr 02 2020 at 09:35):

It feels painful having to carry around all these loopless facts.

#### Scott Morrison (Apr 02 2020 at 09:35):

and just setup the whole chromatic number story for loopless graphs (the only ones for which the story has any interesting, anyway)?

#### Johan Commelin (Apr 02 2020 at 09:41):

Yup, bundling is_loopless seems a good move

#### Johan Commelin (Apr 02 2020 at 09:43):

If you depredicate everything, that's fine with me. If it turns out that it makes it really annoying to talk about a family of graphs whose chromatic number is equal to the characteristic of a certain ring, I'll know where to find you :stuck_out_tongue_wink:

#### Johan Commelin (Apr 02 2020 at 09:44):

@Scott Morrison I'll be having lunch pretty soon, so you can do whatever you want. I was planning to move lots of facts to their own files. But if you want to clean things up now, that's fine with me.

#### Scott Morrison (Apr 02 2020 at 09:44):

Okay. Ping me when you get back from lunch and I'll hand the files back over to you. I'll try to commit often in any case.

#### Johan Commelin (Apr 02 2020 at 09:45):

I'll think about the helpme issue. It might be that we just want to apply something with q+1 instead of q, and then everythings is fine again.

#### David Wärn (Apr 02 2020 at 09:54):

I'm under the impression that "girth" is only ever used in the phrase "the girth is at least X", i.e. "there is no cycle of length < X". Would it make sense to just have a predicate for this, something likegirth_is_at_least G k : Prop?

#### Johan Commelin (Apr 02 2020 at 09:54):

Re "only ever used". Do you mean in this project, or in maths in general?

#### David Wärn (Apr 02 2020 at 10:05):

Certainly in this project, and afaik in graph theory in general

#### David Wärn (Apr 02 2020 at 10:09):

"large girth" is an efficient way of saying "there's no short cycle"

#### David Wärn (Apr 02 2020 at 10:18):

In particular an acyclic graph should have very large girth (infinite according to Wikipedia). If I'm supposed to prove that a graph has girth at least 37, then I shouldn't have to exhibit a cycle

#### Johan Commelin (Apr 02 2020 at 10:56):

@David Wärn In the current setup, I'm not sure if you have to exhibit a cycle either...

#### Scott Morrison (Apr 02 2020 at 11:03):

ugh, I'm getting stuck on something

#### Scott Morrison (Apr 02 2020 at 11:04):

I've made a big mess, not sure if I should push...

(deleted)

(deleted)

(deleted)

#### Scott Morrison (Apr 02 2020 at 11:07):

my intuition for ihom directly is very poor

#### Scott Morrison (Apr 02 2020 at 11:08):

Why do I want this? I rewrote chromatic so it was all about simple_graph. That worked fine, in fact everything became marginally nicer.

#### Scott Morrison (Apr 02 2020 at 11:09):

But now the suited stuff at the top of Hedetniemi doesn't typecheck, because I don't know that G.ihom (complete _) is simple, so it doesn't even make sense to talk about colourings of it.

(deleted)

#### Scott Morrison (Apr 02 2020 at 11:33):

I'm really confused about what's going on. G.ihom H has a self-loop at every function which is a graph homomorphism. So if we're looking at G.ihom (K_ n), there is a self loop somewhere precisely if G is n-colourable.

#### Scott Morrison (Apr 02 2020 at 11:59):

I think I am going to declare my attempt to bundle simple_graph a failure. :-(

#### Johan Commelin (Apr 02 2020 at 12:06):

Right... G.ihom H will be simple if and only if card H < chromatic G

#### David Wärn (Apr 02 2020 at 12:07):

Johan Commelin said:

David Wärn In the current setup, I'm not sure if you have to exhibit a cycle either...

You don't if the current setup is to define "large girth" as "for any g s.t. g is the girth, g is large" (this seems a bit perverse to me, but maybe it works the best)

#### David Wärn (Apr 02 2020 at 12:08):

Do you ever use looplessness in the argument? Isn't it just a nice feature of the counter-example?

#### Johan Commelin (Apr 02 2020 at 12:16):

I guess it's a nice feature, hence maybe worth adding?

#### David Wärn (Apr 02 2020 at 12:26):

Of course, it's definitely worth mentioning. I was just confused about how it's relevant for the arguments

#### Scott Morrison (Apr 02 2020 at 12:35):

I'm starting to switch things over to using at_least predicates

#### Johan Commelin (Apr 02 2020 at 12:39):

Maybe the following is also a relevant source: https://arxiv.org/pdf/1906.06783.pdf

#### Johan Commelin (Apr 02 2020 at 12:40):

Some computations seem to have a bit more details

#### Johan Commelin (Apr 02 2020 at 12:40):

And it seems that without much extra work we can get a stronger result

#### Scott Morrison (Apr 02 2020 at 13:21):

Okay, I've found a route that avoids using the incorrect lemma

#### Scott Morrison (Apr 02 2020 at 13:21):

it requires applying Erdos' theorem with 4.1 instead of 3.1,

#### Johan Commelin (Apr 02 2020 at 13:27):

Ok thanks for figuring this out!

#### Johan Commelin (Apr 02 2020 at 13:28):

Some hack like that must have worked

#### Johan Commelin (Apr 02 2020 at 13:28):

I just didn't yet look into which knob I had to turn and fiddle with

#### Johan Commelin (Apr 02 2020 at 13:35):

@Scott Morrison Here's the sorry in helpme'

lemma helpme' (α : ℚ) (q : ℕ) (h : ¬ q = 0) : (⌈α * q⌉ : ℚ) < (α + 1) * q :=
calc (⌈α * q⌉ : ℚ) < α * q + 1 : ceil_lt_add_one _
... ≤ α * q + q : by { apply add_le_add_left, exact_mod_cast nat.pos_of_ne_zero h }
... = (α + 1) * q : by ring


#### Scott Morrison (Apr 02 2020 at 13:35):

I'm done on this for tonight

#### Johan Commelin (Apr 02 2020 at 13:35):

We should now probably also rename some of these (-;

#### Johan Commelin (Apr 02 2020 at 13:35):

Ok! Thanks for all you've done so far!

#### Johan Commelin (Apr 02 2020 at 13:36):

@Scott Morrison Have you pushed everything? Or should I wait for a second?

all pushed

#### Scott Morrison (Apr 02 2020 at 13:36):

sorry it is a mess

#### Johan Commelin (Apr 02 2020 at 13:37):

Ooh, I think I was the one to start the mess

#### Scott Morrison (Apr 02 2020 at 13:37):

and there are new sorries in a bunch of places, hopefully all straightforward, but I was getting tired

where's the git?

#### Scott Morrison (Apr 02 2020 at 13:37):

hedetniemi

#### Johan Commelin (Apr 02 2020 at 13:37):

branch hedetniemi

#### Scott Morrison (Apr 02 2020 at 13:38):

(I just pushed one more comment)

I also pushed

#### Kenny Lau (Apr 02 2020 at 13:40):

what language is hedetniemi?

#### Johan Commelin (Apr 02 2020 at 13:40):

It's the name of a mathematician

Lean

#### Kenny Lau (Apr 02 2020 at 13:43):

import data.rat

lemma function.injective.ne_iff {α β : Type*} {f : α → β} (hf : function.injective f) {x y : α} :
f x ≠ f y ↔ x ≠ y :=
⟨mt \$ congr_arg f, hf.ne⟩

lemma coe_monotone (a b : ℤ) (h : (a : ℚ) < (b : ℚ)) : a < b :=
by rw lt_iff_le_and_ne at h ⊢; rwa [int.cast_le, int.cast_injective.ne_iff] at h; apply_instance


#### Kenny Lau (Apr 02 2020 at 13:43):

yeah, but what language is this name in

#### Kenny Lau (Apr 02 2020 at 13:44):

it doesn't sound like any language I've heard of

#### Kenny Lau (Apr 02 2020 at 13:44):

maybe it's Polish

#### Mario Carneiro (Apr 02 2020 at 13:48):

Data on the internet about this seems to be scant. I suspect it is of Finnish origin

#### Johan Commelin (Apr 02 2020 at 13:53):

@Kenny Lau Wanna contribute? I just pushed some more sorry fixes.

#### Kenny Lau (Apr 02 2020 at 13:56):

"niemi" is a Finnish noun meaning "cape (form of land near lake or sea), (small) peninsula, ness"

#### Kenny Lau (Apr 02 2020 at 13:56):

so maybe you're right

#### Johan Commelin (Apr 02 2020 at 14:35):

I've pushed lots of stuff into other files.

#### Johan Commelin (Apr 02 2020 at 14:35):

And fixed some sorrys.

#### Johan Commelin (Apr 02 2020 at 14:35):

The remaining stuff has actual mathematical content

#### Markus Himmel (Apr 02 2020 at 14:53):

Johan Commelin said:

I've pushed lots of stuff into other files.

Did you forget to add frac_chromatic_number.lean?

#### Johan Commelin (Apr 02 2020 at 15:06):

Whooops, I forgot all the new files :face_palm:

Pushed

#### David Wärn (Apr 02 2020 at 16:30):

I pushed a cleaner version of the proof that for any directed graph with a vertex root s.t. every vertex has a path to root, there is a subgraph where every vertex has a unique path to root

#### David Wärn (Apr 02 2020 at 16:31):

It uses this definition: def subgraph := Π a b, set (G.edge a b). Is this sensible? It doesn't seem to typecheck if the edge-sets are Props

#### Scott Morrison (Apr 03 2020 at 07:52):

I installed some pnats in places, hopefully it is okay.

#### Johan Commelin (Apr 03 2020 at 09:29):

@Scott Morrison Thanks!

#### Johan Commelin (Apr 03 2020 at 09:29):

I've added independent sets, and shown |V| ≤ \alpha(G) * \chi(G)

#### Johan Commelin (Apr 03 2020 at 14:43):

@Scott Morrison I'm trying to prove graph.ext... but getting stuck on ugly ==s.

@[ext]
lemma graph.ext (G₁ G₂ : graph V) (h : ∀ x y, (x ~[G₁] y) ↔ (x ~[G₂] y)) : G₁ = G₂ :=
begin
repeat {cases G₁ with G₁, cases G₂ with G₂}, congr,
{ ext x y, exact h x y, },
{ dsimp at *, sorry }
end


#### Mario Carneiro (Apr 03 2020 at 14:44):

the technique for getting rid of == is to case on any equality that is preventing the heterogeneous equality from being homogeneous

#### Johan Commelin (Apr 03 2020 at 14:49):

@Mario Carneiro no equalities in my context :sad:

V : Type u,
G₁ : V → V → Prop,
G₁_inv : Π (x y : V), G₁ x y ≃ G₁ y x,
G₁_symm : symmetric G₁,
G₂ : V → V → Prop,
G₂_inv : Π (x y : V), G₂ x y ≃ G₂ y x,
G₂_symm : symmetric G₂,
h : ∀ (x y : V), G₁ x y ↔ G₂ x y
⊢ G₁_inv == G₂_inv


#### Reid Barton (Apr 03 2020 at 14:51):

Use propext on h?

#### Johan Commelin (Apr 03 2020 at 14:53):

But that's a forall type, right?

Use funext too

#### Reid Barton (Apr 03 2020 at 14:54):

In fact you already proved this earlier I think ({ ext x y, exact h x y, })

#### Mario Carneiro (Apr 03 2020 at 14:55):

Yeah, actually the equality in that proof is the one you want to case on

Aha

#### Mario Carneiro (Apr 03 2020 at 14:56):

@[ext]
lemma graph.ext {V} (G₁ G₂ : graph V) (h : ∀ x y, (x ~[G₁] y) ↔ (x ~[G₂] y)) : G₁ = G₂ :=
begin
repeat {cases G₁ with G₁, cases G₂ with G₂},
have : G₁ = G₂, { ext x y, exact h x y, },
cases this, congr,
funext x y,
end


Thanks!

#### Johan Commelin (Apr 07 2020 at 14:02):

I've merged master into hedetniemi.

#### Johan Commelin (Apr 08 2020 at 11:14):

@David Wärn I think that cycle should play nice with path. I'll try to merge this stuff. If you have good ideas, please let me know

#### David Wärn (Apr 11 2020 at 19:14):

You'd probably want to start by defining an equivalence between path and homs from "the path of length n"

#### David Wärn (Apr 11 2020 at 19:14):

We also want a notion of homomorphisms for directed_multigraph

#### David Wärn (Apr 11 2020 at 19:15):

Have you done any of this yet?

#### Kevin Buzzard (Apr 11 2020 at 19:16):

The theorem you're trying to prove is about a product of graphs, right?

#### Kevin Buzzard (Apr 11 2020 at 19:16):

Will it be the categorical product, if you define morphisms?

#### David Wärn (Apr 11 2020 at 19:17):

He's trying to disprove a conjecture about products of graphs I think

#### Kevin Buzzard (Apr 11 2020 at 19:17):

Yes, so the theorem you're trying to prove is that the conjecture is false.

#### David Wärn (Apr 11 2020 at 19:17):

We've shown that it's the categorical product in the category of simple graphs

#### Kevin Buzzard (Apr 11 2020 at 19:18):

Oh I see, yes the conjecture was just about graphs

#### David Wärn (Apr 11 2020 at 19:25):

Yes so I think currently we know a lot about graphs, i.e. undirected graphs with no repeated edges, but we don't have a notion of morphism for directed_multigraph.

#### David Wärn (Apr 11 2020 at 19:30):

Anyway, I tried to merge master into hedetniemi, but it seems like there are a few conflicts that I'm not sure how to resolve. (one thing that should be easy to fix is that the graph is now implicit in path.nil) @Johan Commelin , could you look into this?

#### Johan Commelin (Apr 11 2020 at 19:37):

I'll see if I can find some time. But probably not before monday :shrug:

#### Johan Commelin (Apr 11 2020 at 19:44):

@David Wärn I don't see any conflicts...

#### Johan Commelin (Apr 11 2020 at 19:46):

I merged latest master and pushed

#### David Wärn (Apr 11 2020 at 19:52):

Sorry, I meant that code didn't seem to compile, not that there were conflicts. I guess it should be easy to fix anyway

#### Johan Commelin (Apr 11 2020 at 19:58):

Aha... well I agree that there is probably quite a bit of broken code... I tried to experiment with random graphs. So far it was a failure.

#### Johan Commelin (Apr 11 2020 at 19:59):

Maybe we should try to flesh out a more stable part of the code, and move that to a different branch. I think there is stuff that is ready for a PR

#### Johan Commelin (Apr 11 2020 at 19:59):

But I agree that things like hom should (first) be generalised

#### David Wärn (Apr 11 2020 at 20:00):

That sounds like a good idea

#### David Michael Roberts (Apr 21 2020 at 04:44):

For what it's worth, there's been some improvement in the bounds: https://arxiv.org/abs/2004.09028. 7pages + references

#### Johan Commelin (Apr 21 2020 at 04:56):

Thanks for the pointer!

#### Johan Commelin (Apr 21 2020 at 04:57):

Sounds like it is now in Martijn Heule's territory...

#### Bhavik Mehta (Apr 23 2020 at 18:43):

Out of interest, how's this going?

#### Johan Commelin (Apr 23 2020 at 18:44):

It's been dormant...

#### Johan Commelin (Apr 23 2020 at 18:45):

Too many other stuff going on :expressionless:

Last updated: May 10 2021 at 07:15 UTC