Tournament has a Hamiltonian Path

Stream: mathlib4

[Jafar Tanoukhi]

I am working on a PR related to the issue #26771, and I am not sure how to proceed from here. I can't seem to figure out what lemmas or direction I must take to prove this theorem.

variable (V : Type*) (G : Digraph V) [DecidableEq V] [Fintype V] [Nonempty V]

theorem tournament_isTraceable (hG : G.IsTournament) :
   ∃ (a b : V), ∃ (p : G.Walk a b), p.IsHamiltonian := by
  sorry

Here are my definitions of Walk and Hamiltonian for a Digraph :

universe u

namespace Digraph

variable {V : Type u}
variable (G : Digraph V)

inductive Walk : V → V → Type u
  | nil {u : V} : Walk u u
  | cons {u v w : V} (h : G.Adj u v) (p : Walk v w) : Walk u w
  deriving DecidableEq

namespace Walk

def support {u v : V} : G.Walk u v → List V
  | nil => [u]
  | cons _ p => u :: p.support

end Walk

namespace Walk

variable {V : Type u} [DecidableEq V] (G : Digraph V) (u v : V)

def IsHamiltonian (p : G.Walk u v) : Prop := ∀ a, p.support.count a = 1

end Walk

You can also find my definitions for Orientation and Tournament under this PR #28871

[Jafar Tanoukhi]

Though I can very easily prove this theorem with a piece of paper, the classical way, which is what's most frustrating to me.

[Jafar Tanoukhi]

Also here's an MWE :

import Mathlib.Order.CompleteBooleanAlgebra
import Mathlib.Data.Fintype.Pi
import Mathlib.Combinatorics.Digraph.Basic
import Mathlib.Combinatorics.Digraph.Orientation

universe u

namespace Digraph

variable {V : Type u}
variable (G : Digraph V)

inductive Walk : V → V → Type u
  | nil {u : V} : Walk u u
  | cons {u v w : V} (h : G.Adj u v) (p : Walk v w) : Walk u w
  deriving DecidableEq

namespace Walk

def support {u v : V} : G.Walk u v → List V
  | nil => [u]
  | cons _ p => u :: p.support

end Walk

end Digraph

namespace Digraph

namespace Walk

variable {V : Type u} [DecidableEq V] (G : Digraph V) (u v : V)

def IsHamiltonian (p : G.Walk u v) : Prop := ∀ a, p.support.count a = 1

end Walk

end Digraph

variable (V : Type*) (G : Digraph V)

namespace Digraph

structure IsTournament : Prop where
  loopless w : ¬ G.Adj w w
  one_edge w v : w ≠ v → (G.Adj w v ↔ ¬ G.Adj v w)

variable [DecidableEq V] [Fintype V] [Nonempty V]

  theorem tournament_isTraceable (hG : G.IsTournament) :
   ∃ (a b : V), ∃ (p : G.Walk a b), p.IsHamiltonian := by
  sorry

  end Digraph

[Aaron Liu]

oh I remember this theorem

[Aaron Liu]

I did this as an exercise before

[Aaron Liu]

using docs#Fintype.induction_empty_option

[Aaron Liu]

and lots of list lemmas

[Aaron Liu]

Jafar Tanoukhi said:

Though I can very easily prove this theorem with a piece of paper, the classical way, which is what's most frustrating to me.

What's your paper proof? Is it the same one I know?

[Jafar Tanoukhi]

Aaron Liu said:

What's your paper proof? Is it the same one I know?

Induction on the number of vertices for a tournament
For 1 vertex, the Hamiltonian path is the vertex itself
For n + 1 vertices, we start with the Hamiltonian path that exists for n (we can assume this because of induction)
let's say this hamiltonian path is H : v1, v2, v3... vn and let's say the extra vertex is V

Three cases occur :
case 1: V is adjacent to v1 -> hence the hamiltonian path for n + 1 vertices would be V, v1, v2 ...vn
case 2: vn is adjacent to V -> hence the hamiltonian path for n + 1 vertices would be v1, v2...vn, V
case 3: if neither case 1 nor case 2 is true, then there will be some v in H such that vi -> V and V -> vi+1, hence the hamiltonian path for n + 1 vertices would be v1, v2,...,vi, V, vi+1,...,vn

This is it in a nutshell.

[Jafar Tanoukhi]

Aaron Liu said:

using docs#Fintype.induction_empty_option

I tried with this, but I was not able to figure out how exactly I'm supposed to use this.

apply Fintype.induction_empty_option at V yielded 5 goals, as there are other hypotheses like of_equiv, h_empty, and h_option that are required. Not sure how to get ride of those.

[Snir Broshi]

It looks Digraph is missing a lot of API that's needed here.
For example, I think we'd need these:

def map {V V' : Type*} (f : V → V') (G : Digraph V) : Digraph V' where
  Adj := Relation.Map G.Adj f f

def comap {V V' : Type*} (f : V → V') (G : Digraph V') : Digraph V where
  Adj u v := G.Adj (f u) (f v)

then theorems about when the IsTournament property is preserved across maps/comaps.
To use the induction hypothesis in h_option you would then have to show that G.comap some is a tournament.

[Snir Broshi]

I think that for the proof itself, the solution is to define docs#SimpleGraph.Walk.getVert for digraphs, prove docs#SimpleGraph.Walk.adj_getVert_succ, then prove that the getVert of a hamiltonian walk is a bijection from V to Fin n. Then the proof can use that bijection with docs#Fin.Lt.isWellOrder to get the first vertex v : α in the path from the induction hypothesis such that G.Adj (some v) none. If there is no such v we're in case 1, otherwise case 2 or 3.

[Aaron Liu]

Jafar Tanoukhi said:

Aaron Liu said:

using docs#Fintype.induction_empty_option

I tried with this, but I was not able to figure out how exactly I'm supposed to use this.

apply Fintype.induction_empty_option at V yielded 5 goals, as there are other hypotheses like of_equiv, h_empty, and h_option that are required. Not sure how to get ride of those.

With induction tactic

[Aaron Liu]

actually I think it has a bug which makes this not work

[Snir Broshi]

Oh we don't even have homomorphisms for Digraph :cold_sweat:

namespace Digraph
variable {V V' : Type*} (G : Digraph V) (G' : Digraph V')
abbrev Hom :=
  RelHom G.Adj G'.Adj
abbrev Embedding :=
  RelEmbedding G.Adj G'.Adj
abbrev Iso :=
  RelIso G.Adj G'.Adj
@[inherit_doc] infixl:50 " →g " => Hom
@[inherit_doc] infixl:50 " ↪g " => Embedding
@[inherit_doc] infixl:50 " ≃g " => Iso
end Digraph

Define Walk.map:

def Walk.map {V V' : Type*} {G : Digraph V} {G' : Digraph V'} (f : G →g G') {u v : V} : G.Walk u v → G'.Walk (f u) (f v)
  | nil => nil
  | cons h p => cons (f.map_rel' h) (p.map f)

Then we need docs#SimpleGraph.Embedding.comap or docs#SimpleGraph.Embedding.map for digraphs, and we're really close to solving the simple part of the proof:

theorem tournament_isTraceable (hG : G.IsTournament) :
    ∃ (a b : V), ∃ (p : G.Walk a b), p.IsHamiltonian := by
  revert G
  expose_names
  revert inst inst_2
  apply Fintype.induction_empty_option (P := fun α _ ↦ [DecidableEq α] → [Nonempty α] →
    ∀ G, IsTournament α G → ∃ a b p, Walk.IsHamiltonian G a b p)
  · intro α β _ f hα _ _ G ht
    classical
    have := Equiv.nonempty_congr f |>.mpr ‹Nonempty _›
    have : G.comap f |>.IsTournament := sorry
    have ⟨a, b, p, h⟩ := hα (G.comap f) this
    use f a, f b
    -- TODO: `use p.map (SimpleGraph.Embedding.comap f G)`
    sorry
  · aesop
  · intro α _ h _ _ G ht
    by_cases he : Nonempty α; rotate_left
    · use none, none, Walk.nil
      intro a
      have : IsEmpty α := not_nonempty_iff.mp he
      rw [show a = none by exact Unique.uniq _ _]
      simp [Walk.support]
    sorry

[Jafar Tanoukhi]

Snir said:

Oh we don't even have homomorphisms for Digraph :cold_sweat:

It seems to give these warnings :
@Hom does not have a doc string
@Embedding does not have a doc string
@Iso does not have a doc string

does it require some import other than importing the Digraph definition?

[Jafar Tanoukhi]

I removed the @[inherit_doc], which made the warning go away. Not sure what this is about though.

[Damiano Testa]

I think that Hom, Embedding and Iso should have a docstring and then the inherit_doc should be restored (and will not complain).

[Jafar Tanoukhi]

What's a docstring ?

[Ruben Van de Velde]

/-- explain what the thing does -/

[Jafar Tanoukhi]

ohh, alright haha.