Hedetniemi

Stream: maths

[Johan Commelin]

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]

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

[David Wärn]

Isn't infinite Ramsey about hypergraphs?

[Bhavik Mehta]

Yup, my bad, I forgot what multigraph means

[Scott Morrison]

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

[Johan Commelin]

I just pushed to hedetniemi

[Johan Commelin]

There is a new graph_theory directory.

[Johan Commelin]

I've pushed some updates

[David Wärn]

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

[Johan Commelin]

I haven't defined max degree yet (-;

[Johan Commelin]

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

[Johan Commelin]

I pushed a proof of "Observation 1"

[Vaibhav Karve]

@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]

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)

[Kevin Buzzard]

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

[Johan Commelin]

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]

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

[Scott Morrison]

@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]

@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]

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]

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]

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]

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

[Johan Commelin]

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

[Scott Morrison]

okay :-)

[Johan Commelin]

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

[Scott Morrison]

well, I made up my mind :-)

[Johan Commelin]

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

[Scott Morrison]

I was just writing the statement of the Konigsberg problem

[Scott Morrison]

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

[Scott Morrison]

so I was thinking about doing that

[Scott Morrison]

but it is not super pretty

[Scott Morrison]

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]

but perhaps a helper function does it

[Scott Morrison]

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

[Johan Commelin]

That sounds good

[Johan Commelin]

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

[Scott Morrison]

no, it's even easier than that

[Johan Commelin]

Ok, note that I just pushed.

[Johan Commelin]

A little commit to the end of that file.

[Scott Morrison]

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

[Johan Commelin]

We should probably split the file now...

[Scott Morrison]

so the constructor will look the same

[Johan Commelin]

Aah, inv will get the default value. Sure.

[Johan Commelin]

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]

Do we manually need to apply coercions?

[Johan Commelin]

@Scott Morrison Are you making this change atm?

[Scott Morrison]

yes

[Johan Commelin]

Cool

[Johan Commelin]

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]

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.

[Scott Morrison]

I committed

[Scott Morrison]

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]

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]

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

[Scott Morrison]

and struggling to make that coercion fire makes things ugly

[Johan Commelin]

@Scott Morrison Thanks!

[Johan Commelin]

Cleaning up the coercion issues seems to be an important issue

[David Wärn]

@Scott Morrison This looks good!

[David Wärn]

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]

(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]

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

[Mario Carneiro]

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]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Scott Morrison]

yes

[Johan Commelin]

I hope it gets merged quickly (-;

[Scott Morrison]

You know that CI builds all branches?

[Scott Morrison]

So leanproject up should get you oleans.

[Scott Morrison]

and indeed, they are available now

[Johan Commelin]

I did leanproject get-cache which didn't work

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Scott Morrison]

max_steps got renamed recently, it may be something else still

[Scott Morrison]

solve_by_elim has a very conservative default for max_steps.

[Johan Commelin]

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]

I don't understand why.

[Johan Commelin]

I think 20 applys are more than enough.

[Scott Morrison]

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

[Johan Commelin]

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]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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

[Johan Commelin]

Sleep tight. See you tomorrow morning (-;

[Scott Morrison]

(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]

Aren't you sleeping?

[Scott Morrison]

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

[Scott Morrison]

:-)

[Johan Commelin]

Scott is a very effective sleeper (-;

[David Wärn]

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]

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

[Scott Morrison]

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

[David Wärn]

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]

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]

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]

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

[David Wärn]

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?

[Kenny Lau]

too bad

[David Wärn]

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]

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]

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]

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]

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

[Reid Barton]

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]

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]

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

[Bhavik Mehta]

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]

there is also something about transitive closure of a relation

[Mario Carneiro]

refl_trans_gen and trans_gen in logic.relation

[Mario Carneiro]

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]

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]

Isn't refl_trans_gen Prop-valued?

[Mario Carneiro]

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

[Mario Carneiro]

list.chain' will give you the path itself

[David Wärn]

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]

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

[Bhavik Mehta]

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]

@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]

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

[Mario Carneiro]

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]

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

[David Wärn]

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]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

[Sebastien Gouezel]

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

[Kevin Buzzard]

Yes of course

[Kevin Buzzard]

this is why it can have 37 edges

[Kevin Buzzard]

@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]

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]

@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]

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]

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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Johan Commelin]

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

[Scott Morrison]

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

[Johan Commelin]

Right... of course :face_palm:

[Scott Morrison]

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]

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

[Johan Commelin]

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]

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]

I've pushed a bugfix

[David Wärn]

@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]

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]

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

• https://www.cambridge.org/core/journals/canadian-journal-of-mathematics/article/graph-theory-and-probability/154EF813293BC7D0652C4CBCD9D18E84
• https://www.renyi.hu/~p_erdos/1959-11.pdf

[David Wärn]

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]

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

[Johan Commelin]

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

[Kevin Buzzard]

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]

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

[David Wärn]

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]

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]

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]

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]

@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]

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

[Scott Morrison]

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

[Johan Commelin]

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]

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

[Johan Commelin]

:fencing:

[Johan Commelin]

@Scott Morrison The reason is again classical.decidable*

[Johan Commelin]

@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]

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.

[Johan Commelin]

And upsetting.

[Johan Commelin]

@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]

Just make everything classical?

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

See the commit I pushed.

[Scott Morrison]

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

[Johan Commelin]

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

[Scott Morrison]

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

[Kenny Lau]

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

[Johan Commelin]

@Scott Morrison I've pushed

[Johan Commelin]

Now there is no convert anymore

[Scott Morrison]

but there's also no proof?

[Scott Morrison]

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

[Scott Morrison]

oh, my mistake, ignore me

[Scott Morrison]

your push is great

[Scott Morrison]

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

[Johan Commelin]

  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]

Now we only need to argue that n is positive

[Scott Morrison]

So what's going on with helpme?

[Johan Commelin]

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]

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

[Johan Commelin]

Sorry, I meant a bigger q

[Scott Morrison]

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

[Scott Morrison]

I'm really unconvinced by all these predicates.

[Johan Commelin]

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

[Johan Commelin]

@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

[Johan Commelin]

Pushed

[Scott Morrison]

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]

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]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Johan Commelin]

Yup, bundling is_loopless seems a good move

[Johan Commelin]

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]

@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]

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]

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]

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]

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

[David Wärn]

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

[David Wärn]

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

[David Wärn]

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

[David Wärn]

Similar points could be made about chromatic number

[Johan Commelin]

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

[Scott Morrison]

ugh, I'm getting stuck on something

[Scott Morrison]

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

[Scott Morrison]

(deleted)

[Scott Morrison]

(deleted)

[Scott Morrison]

(deleted)

[Scott Morrison]

my intuition for ihom directly is very poor

[Scott Morrison]

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]

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.

[Scott Morrison]

(deleted)

[Scott Morrison]

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]

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

[Johan Commelin]

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

[David Wärn]

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]

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

[Johan Commelin]

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

[David Wärn]

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

[Scott Morrison]

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

[Johan Commelin]

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

[Johan Commelin]

Some computations seem to have a bit more details

[Johan Commelin]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Johan Commelin]

Ok thanks for figuring this out!

[Johan Commelin]

Some hack like that must have worked

[Johan Commelin]

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

[Johan Commelin]

@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]

I'm done on this for tonight

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Scott Morrison]

all pushed

[Scott Morrison]

sorry it is a mess

[Johan Commelin]

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

[Scott Morrison]

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

[Kenny Lau]

where's the git?

[Scott Morrison]

hedetniemi

[Johan Commelin]

branch hedetniemi

[Scott Morrison]

(I just pushed one more comment)

[Johan Commelin]

I also pushed

[Kenny Lau]

what language is hedetniemi?

[Johan Commelin]

It's the name of a mathematician

[Kevin Buzzard]

Lean

[Kenny Lau]

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]

yeah, but what language is this name in

[Kenny Lau]

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

[Kenny Lau]

maybe it's Polish

[Mario Carneiro]

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

[Johan Commelin]

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

[Kenny Lau]

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

[Kenny Lau]

so maybe you're right

[Johan Commelin]

I've pushed lots of stuff into other files.

[Johan Commelin]

And fixed some sorrys.

[Johan Commelin]

The remaining stuff has actual mathematical content

[Markus Himmel]

Johan Commelin said:

I've pushed lots of stuff into other files.

Did you forget to add frac_chromatic_number.lean?

[Johan Commelin]

Whooops, I forgot all the new files :face_palm:

[Johan Commelin]

Pushed

[David Wärn]

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]

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]

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

[Johan Commelin]

@Scott Morrison Thanks!

[Johan Commelin]

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

[Johan Commelin]

@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]

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

[Johan Commelin]

@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]

Use propext on h?

[Johan Commelin]

But that's a forall type, right?

[Reid Barton]

Use funext too

[Reid Barton]

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

[Mario Carneiro]

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

[Johan Commelin]

Aha

[Mario Carneiro]

@[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

[Johan Commelin]

Thanks!

[Johan Commelin]

I've merged master into hedetniemi.

[Johan Commelin]

@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]

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

[David Wärn]

We also want a notion of homomorphisms for directed_multigraph

[David Wärn]

Have you done any of this yet?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[David Wärn]

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

[Kevin Buzzard]

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

[David Wärn]

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

[Kevin Buzzard]

Oh I see, yes the conjecture was just about graphs

[David Wärn]

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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

I merged latest master and pushed

[David Wärn]

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]

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]

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]

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

[David Wärn]

That sounds like a good idea

[David Michael Roberts]

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

[Johan Commelin]

Thanks for the pointer!

[Johan Commelin]

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

[Bhavik Mehta]

Out of interest, how's this going?

[Johan Commelin]

It's been dormant...

[Johan Commelin]

Too many other stuff going on :expressionless: