Zulip Chat Archive

Stream: maths

Topic: Hedetniemi


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

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

view this post on Zulip David Wärn (Mar 26 2020 at 21:04):

Isn't infinite Ramsey about hypergraphs?

view this post on Zulip Bhavik Mehta (Mar 26 2020 at 21:19):

Yup, my bad, I forgot what multigraph means

view this post on Zulip Scott Morrison (Mar 26 2020 at 22:51):

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

view this post on Zulip Johan Commelin (Mar 27 2020 at 05:54):

I just pushed to hedetniemi

view this post on Zulip Johan Commelin (Mar 27 2020 at 05:54):

There is a new graph_theory directory.

view this post on Zulip Johan Commelin (Mar 27 2020 at 09:37):

I've pushed some updates

view this post on Zulip David Wärn (Mar 27 2020 at 09:58):

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

view this post on Zulip Johan Commelin (Mar 27 2020 at 10:15):

I haven't defined max degree yet (-;

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

view this post on Zulip Johan Commelin (Mar 27 2020 at 10:51):

I pushed a proof of "Observation 1"

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

view this post on Zulip 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) :=
  (symm : symmetric adj)


  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 :=
  (symm : symmetric adj)
  (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

  instance fintype_V_and_dec_rel_adj_implies_fintype_edges_digraph
  (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)

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

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

view this post on Zulip David Wärn (Mar 27 2020 at 20:01):

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

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

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

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

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

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

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

view this post on Zulip Johan Commelin (Mar 28 2020 at 06:06):

@Scott Morrison It's because we hadn't made up our mind yet.

view this post on Zulip Scott Morrison (Mar 28 2020 at 06:07):

okay :-)

view this post on Zulip Johan Commelin (Mar 28 2020 at 06:07):

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

view this post on Zulip Scott Morrison (Mar 28 2020 at 06:07):

well, I made up my mind :-)

view this post on Zulip Johan Commelin (Mar 28 2020 at 06:07):

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

view this post on Zulip Scott Morrison (Mar 28 2020 at 06:07):

I was just writing the statement of the Konigsberg problem

view this post on Zulip Scott Morrison (Mar 28 2020 at 06:07):

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

view this post on Zulip Scott Morrison (Mar 28 2020 at 06:08):

so I was thinking about doing that

view this post on Zulip Scott Morrison (Mar 28 2020 at 06:08):

but it is not super pretty

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

view this post on Zulip Scott Morrison (Mar 28 2020 at 06:08):

but perhaps a helper function does it

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

view this post on Zulip Johan Commelin (Mar 28 2020 at 06:10):

That sounds good

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

view this post on Zulip Scott Morrison (Mar 28 2020 at 06:11):

no, it's even easier than that

view this post on Zulip Johan Commelin (Mar 28 2020 at 06:11):

Ok, note that I just pushed.

view this post on Zulip Johan Commelin (Mar 28 2020 at 06:11):

A little commit to the end of that file.

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

view this post on Zulip Johan Commelin (Mar 28 2020 at 06:12):

We should probably split the file now...

view this post on Zulip Scott Morrison (Mar 28 2020 at 06:12):

so the constructor will look the same

view this post on Zulip Johan Commelin (Mar 28 2020 at 06:12):

Aah, inv will get the default value. Sure.

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

view this post on Zulip Johan Commelin (Mar 28 2020 at 06:13):

Do we manually need to apply coercions?

view this post on Zulip Johan Commelin (Mar 28 2020 at 06:16):

@Scott Morrison Are you making this change atm?

view this post on Zulip Scott Morrison (Mar 28 2020 at 06:16):

yes

view this post on Zulip Johan Commelin (Mar 28 2020 at 06:16):

Cool

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

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

view this post on Zulip Scott Morrison (Mar 28 2020 at 07:07):

I committed

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

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

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

view this post on Zulip Scott Morrison (Mar 28 2020 at 07:10):

and struggling to make that coercion fire makes things ugly

view this post on Zulip Johan Commelin (Mar 28 2020 at 07:53):

@Scott Morrison Thanks!

view this post on Zulip Johan Commelin (Mar 28 2020 at 07:53):

Cleaning up the coercion issues seems to be an important issue

view this post on Zulip David Wärn (Mar 28 2020 at 09:00):

@Scott Morrison This looks good!

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

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

view this post on Zulip David Wärn (Mar 28 2020 at 09:14):

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

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

view this post on Zulip Mario Carneiro (Mar 28 2020 at 09:19):

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

view this post on Zulip Johan Commelin (Mar 28 2020 at 09:59):

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

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

view this post on Zulip Mario Carneiro (Mar 28 2020 at 10:00):

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

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

view this post on Zulip Johan Commelin (Mar 28 2020 at 10:02):

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

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

view this post on Zulip Scott Morrison (Mar 28 2020 at 10:04):

yes

view this post on Zulip Johan Commelin (Mar 28 2020 at 10:04):

I hope it gets merged quickly (-;

view this post on Zulip Scott Morrison (Mar 28 2020 at 10:05):

You know that CI builds all branches?

view this post on Zulip Scott Morrison (Mar 28 2020 at 10:05):

So leanproject up should get you oleans.

view this post on Zulip Scott Morrison (Mar 28 2020 at 10:06):

and indeed, they are available now

view this post on Zulip Johan Commelin (Mar 28 2020 at 10:08):

I did leanproject get-cache which didn't work

view this post on Zulip Johan Commelin (Mar 28 2020 at 10:09):

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

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

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

view this post on Zulip Scott Morrison (Mar 28 2020 at 10:20):

max_steps got renamed recently, it may be something else still

view this post on Zulip Scott Morrison (Mar 28 2020 at 10:21):

solve_by_elim has a very conservative default for max_steps.

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

view this post on Zulip Johan Commelin (Mar 28 2020 at 10:25):

I don't understand why.

view this post on Zulip Johan Commelin (Mar 28 2020 at 10:25):

I think 20 applys are more than enough.

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

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

view this post on Zulip Scott Morrison (Mar 28 2020 at 10:54):

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

view this post on Zulip Scott Morrison (Mar 28 2020 at 10:54):

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

view this post on Zulip Scott Morrison (Mar 28 2020 at 10:54):

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

view this post on Zulip Scott Morrison (Mar 28 2020 at 10:54):

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

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

view this post on Zulip Johan Commelin (Mar 28 2020 at 11:02):

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

view this post on Zulip Johan Commelin (Mar 28 2020 at 11:03):

Sleep tight. See you tomorrow morning (-;

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

view this post on Zulip Patrick Massot (Mar 28 2020 at 11:49):

Aren't you sleeping?

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

view this post on Zulip Scott Morrison (Mar 28 2020 at 11:49):

:-)

view this post on Zulip Johan Commelin (Mar 28 2020 at 12:07):

Scott is a very effective sleeper (-;

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

view this post on Zulip Scott Morrison (Mar 30 2020 at 03:58):

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

view this post on Zulip Scott Morrison (Mar 30 2020 at 03:59):

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

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

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

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

view this post on Zulip Kenny Lau (Mar 30 2020 at 08:12):

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

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

view this post on Zulip Kenny Lau (Mar 30 2020 at 08:25):

too bad

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

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

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

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

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 08:43):

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

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

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

view this post on Zulip Johan Commelin (Mar 31 2020 at 08:55):

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

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

view this post on Zulip Mario Carneiro (Mar 31 2020 at 13:20):

there is also something about transitive closure of a relation

view this post on Zulip Mario Carneiro (Mar 31 2020 at 13:22):

refl_trans_gen and trans_gen in logic.relation

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

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

view this post on Zulip David Wärn (Mar 31 2020 at 13:28):

Isn't refl_trans_gen Prop-valued?

view this post on Zulip Mario Carneiro (Mar 31 2020 at 13:29):

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

view this post on Zulip Mario Carneiro (Mar 31 2020 at 13:29):

list.chain' will give you the path itself

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

view this post on Zulip 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 relation.refl_trans_gen.head,
  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 relation.refl_trans_gen.head hp₁_a_1,
  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,
  apply relation.refl_trans_gen.head_induction_on h,
    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

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

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

view this post on Zulip David Wärn (Mar 31 2020 at 13:47):

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

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

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

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

view this post on Zulip Kevin Buzzard (Mar 31 2020 at 14:23):

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

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

view this post on Zulip Johan Commelin (Mar 31 2020 at 14:24):

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

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

view this post on Zulip Kevin Buzzard (Mar 31 2020 at 14:49):

Yes of course

view this post on Zulip Kevin Buzzard (Mar 31 2020 at 14:49):

this is why it can have 37 edges

view this post on Zulip Kevin Buzzard (Mar 31 2020 at 14:50):

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

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

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

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

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

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

view this post on Zulip Johan Commelin (Apr 01 2020 at 05:51):

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

view this post on Zulip Johan Commelin (Apr 01 2020 at 05:52):

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

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

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

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

view this post on Zulip Scott Morrison (Apr 01 2020 at 06:04):

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

view this post on Zulip Johan Commelin (Apr 01 2020 at 06:04):

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

view this post on Zulip Scott Morrison (Apr 01 2020 at 06:05):

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

view this post on Zulip Johan Commelin (Apr 01 2020 at 06:05):

Right... of course :face_palm:

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

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

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

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

view this post on Zulip Johan Commelin (Apr 01 2020 at 09:04):

I've pushed a bugfix

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

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

view this post on Zulip Johan Commelin (Apr 01 2020 at 09:44):

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

view this post on Zulip 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)E(X) > E(Y), here's a point in the sample space where X>YX > Y"

view this post on Zulip Johan Commelin (Apr 01 2020 at 14:17):

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

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

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

view this post on Zulip David Wärn (Apr 01 2020 at 16:43):

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

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

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

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

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

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

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

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

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

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

view this post on Zulip Johan Commelin (Apr 02 2020 at 07:58):

:fencing:

view this post on Zulip Johan Commelin (Apr 02 2020 at 08:51):

@Scott Morrison The reason is again classical.decidable*

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

view this post on Zulip 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 := .min,

then the error will be very clear.

view this post on Zulip Johan Commelin (Apr 02 2020 at 08:55):

And upsetting.

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

view this post on Zulip Johan Commelin (Apr 02 2020 at 09:01):

Just make everything classical?

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

view this post on Zulip Johan Commelin (Apr 02 2020 at 09:08):

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

view this post on Zulip Johan Commelin (Apr 02 2020 at 09:09):

See the commit I pushed.

view this post on Zulip Scott Morrison (Apr 02 2020 at 09:09):

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

view this post on Zulip Johan Commelin (Apr 02 2020 at 09:10):

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

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

view this post on Zulip Kenny Lau (Apr 02 2020 at 09:14):

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

view this post on Zulip Johan Commelin (Apr 02 2020 at 09:14):

@Scott Morrison I've pushed

view this post on Zulip Johan Commelin (Apr 02 2020 at 09:15):

Now there is no convert anymore

view this post on Zulip Scott Morrison (Apr 02 2020 at 09:15):

but there's also no proof?

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

view this post on Zulip Scott Morrison (Apr 02 2020 at 09:17):

oh, my mistake, ignore me

view this post on Zulip Scott Morrison (Apr 02 2020 at 09:17):

your push is great

view this post on Zulip Scott Morrison (Apr 02 2020 at 09:17):

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

view this post on Zulip 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 := .min mc npos,
  rwa le_div_iff at this,
  assumption_mod_cast,

view this post on Zulip Johan Commelin (Apr 02 2020 at 09:18):

Now we only need to argue that n is positive

view this post on Zulip Scott Morrison (Apr 02 2020 at 09:18):

So what's going on with helpme?

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

view this post on Zulip Scott Morrison (Apr 02 2020 at 09:20):

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

view this post on Zulip Johan Commelin (Apr 02 2020 at 09:20):

Sorry, I meant a bigger q

view this post on Zulip Scott Morrison (Apr 02 2020 at 09:21):

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

view this post on Zulip Scott Morrison (Apr 02 2020 at 09:21):

I'm really unconvinced by all these predicates.

view this post on Zulip Johan Commelin (Apr 02 2020 at 09:22):

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

view this post on Zulip 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) ( : 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 := .min mc hn,
  rwa le_div_iff at this,
  assumption_mod_cast,
end

view this post on Zulip Johan Commelin (Apr 02 2020 at 09:30):

Pushed

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

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

view this post on Zulip Scott Morrison (Apr 02 2020 at 09:34):

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

view this post on Zulip Scott Morrison (Apr 02 2020 at 09:35):

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

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

view this post on Zulip Johan Commelin (Apr 02 2020 at 09:41):

Yup, bundling is_loopless seems a good move

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

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

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

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

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

view this post on Zulip Johan Commelin (Apr 02 2020 at 09:54):

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

view this post on Zulip David Wärn (Apr 02 2020 at 10:05):

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

view this post on Zulip David Wärn (Apr 02 2020 at 10:09):

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

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

view this post on Zulip David Wärn (Apr 02 2020 at 10:18):

Similar points could be made about chromatic number

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

view this post on Zulip Scott Morrison (Apr 02 2020 at 11:03):

ugh, I'm getting stuck on something

view this post on Zulip Scott Morrison (Apr 02 2020 at 11:04):

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

view this post on Zulip Scott Morrison (Apr 02 2020 at 11:05):

(deleted)

view this post on Zulip Scott Morrison (Apr 02 2020 at 11:05):

(deleted)

view this post on Zulip Scott Morrison (Apr 02 2020 at 11:07):

(deleted)

view this post on Zulip Scott Morrison (Apr 02 2020 at 11:07):

my intuition for ihom directly is very poor

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

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

view this post on Zulip Scott Morrison (Apr 02 2020 at 11:24):

(deleted)

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

view this post on Zulip Scott Morrison (Apr 02 2020 at 11:59):

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

view this post on Zulip Johan Commelin (Apr 02 2020 at 12:06):

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

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

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

view this post on Zulip Johan Commelin (Apr 02 2020 at 12:16):

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

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

view this post on Zulip Scott Morrison (Apr 02 2020 at 12:35):

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

view this post on Zulip Johan Commelin (Apr 02 2020 at 12:39):

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

view this post on Zulip Johan Commelin (Apr 02 2020 at 12:40):

Some computations seem to have a bit more details

view this post on Zulip Johan Commelin (Apr 02 2020 at 12:40):

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

view this post on Zulip Scott Morrison (Apr 02 2020 at 13:21):

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

view this post on Zulip Scott Morrison (Apr 02 2020 at 13:21):

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

view this post on Zulip Johan Commelin (Apr 02 2020 at 13:27):

Ok thanks for figuring this out!

view this post on Zulip Johan Commelin (Apr 02 2020 at 13:28):

Some hack like that must have worked

view this post on Zulip Johan Commelin (Apr 02 2020 at 13:28):

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

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

view this post on Zulip Scott Morrison (Apr 02 2020 at 13:35):

I'm done on this for tonight

view this post on Zulip Johan Commelin (Apr 02 2020 at 13:35):

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

view this post on Zulip Johan Commelin (Apr 02 2020 at 13:35):

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

view this post on Zulip Johan Commelin (Apr 02 2020 at 13:36):

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

view this post on Zulip Scott Morrison (Apr 02 2020 at 13:36):

all pushed

view this post on Zulip Scott Morrison (Apr 02 2020 at 13:36):

sorry it is a mess

view this post on Zulip Johan Commelin (Apr 02 2020 at 13:37):

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

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

view this post on Zulip Kenny Lau (Apr 02 2020 at 13:37):

where's the git?

view this post on Zulip Scott Morrison (Apr 02 2020 at 13:37):

hedetniemi

view this post on Zulip Johan Commelin (Apr 02 2020 at 13:37):

branch hedetniemi

view this post on Zulip Scott Morrison (Apr 02 2020 at 13:38):

(I just pushed one more comment)

view this post on Zulip Johan Commelin (Apr 02 2020 at 13:38):

I also pushed

view this post on Zulip Kenny Lau (Apr 02 2020 at 13:40):

what language is hedetniemi?

view this post on Zulip Johan Commelin (Apr 02 2020 at 13:40):

It's the name of a mathematician

view this post on Zulip Kevin Buzzard (Apr 02 2020 at 13:40):

Lean

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

view this post on Zulip Kenny Lau (Apr 02 2020 at 13:43):

yeah, but what language is this name in

view this post on Zulip Kenny Lau (Apr 02 2020 at 13:44):

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

view this post on Zulip Kenny Lau (Apr 02 2020 at 13:44):

maybe it's Polish

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

view this post on Zulip Johan Commelin (Apr 02 2020 at 13:53):

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

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

view this post on Zulip Kenny Lau (Apr 02 2020 at 13:56):

so maybe you're right

view this post on Zulip Johan Commelin (Apr 02 2020 at 14:35):

I've pushed lots of stuff into other files.

view this post on Zulip Johan Commelin (Apr 02 2020 at 14:35):

And fixed some sorrys.

view this post on Zulip Johan Commelin (Apr 02 2020 at 14:35):

The remaining stuff has actual mathematical content

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

view this post on Zulip Johan Commelin (Apr 02 2020 at 15:06):

Whooops, I forgot all the new files :face_palm:

view this post on Zulip Johan Commelin (Apr 02 2020 at 15:06):

Pushed

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

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

view this post on Zulip Scott Morrison (Apr 03 2020 at 07:52):

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

view this post on Zulip Johan Commelin (Apr 03 2020 at 09:29):

@Scott Morrison Thanks!

view this post on Zulip Johan Commelin (Apr 03 2020 at 09:29):

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

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

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

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

view this post on Zulip Reid Barton (Apr 03 2020 at 14:51):

Use propext on h?

view this post on Zulip Johan Commelin (Apr 03 2020 at 14:53):

But that's a forall type, right?

view this post on Zulip Reid Barton (Apr 03 2020 at 14:54):

Use funext too

view this post on Zulip Reid Barton (Apr 03 2020 at 14:54):

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

view this post on Zulip Mario Carneiro (Apr 03 2020 at 14:55):

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

view this post on Zulip Johan Commelin (Apr 03 2020 at 14:56):

Aha

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

view this post on Zulip Johan Commelin (Apr 03 2020 at 15:04):

Thanks!

view this post on Zulip Johan Commelin (Apr 07 2020 at 14:02):

I've merged master into hedetniemi.

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

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

view this post on Zulip David Wärn (Apr 11 2020 at 19:14):

We also want a notion of homomorphisms for directed_multigraph

view this post on Zulip David Wärn (Apr 11 2020 at 19:15):

Have you done any of this yet?

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 19:16):

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

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 19:16):

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

view this post on Zulip David Wärn (Apr 11 2020 at 19:17):

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

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 19:17):

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

view this post on Zulip David Wärn (Apr 11 2020 at 19:17):

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

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 19:18):

Oh I see, yes the conjecture was just about graphs

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

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

view this post on Zulip Johan Commelin (Apr 11 2020 at 19:37):

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

view this post on Zulip Johan Commelin (Apr 11 2020 at 19:44):

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

view this post on Zulip Johan Commelin (Apr 11 2020 at 19:46):

I merged latest master and pushed

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

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

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

view this post on Zulip Johan Commelin (Apr 11 2020 at 19:59):

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

view this post on Zulip David Wärn (Apr 11 2020 at 20:00):

That sounds like a good idea

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

view this post on Zulip Johan Commelin (Apr 21 2020 at 04:56):

Thanks for the pointer!

view this post on Zulip Johan Commelin (Apr 21 2020 at 04:57):

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

view this post on Zulip Bhavik Mehta (Apr 23 2020 at 18:43):

Out of interest, how's this going?

view this post on Zulip Johan Commelin (Apr 23 2020 at 18:44):

It's been dormant...

view this post on Zulip Johan Commelin (Apr 23 2020 at 18:45):

Too many other stuff going on :expressionless:


Last updated: May 10 2021 at 07:15 UTC