Hamiltonian paths define a bijection with Fin n

Stream: Is there code for X?

[Snir Broshi]

Hello, is there a way to convert a Hamiltonian path to a bijection with Fin n?
Something like the following:

def SimpleGraph.Walk.IsHamiltonian.equivFin {α : Type*} [DecidableEq α] (G : SimpleGraph α) {a b : α} (p : G.Walk a b) : α ≃ Fin p.support.length := sorry

and maybe even more specifically that p.getVert is that bijection, and an instance of Fintype.
Thanks!

[Jakub Nowak]

I was searching for something like that for docs#SimpleGraph.Walk.IsCycle and couldn't find anything.

[Vlad Tsyrklevich]

apply? followed by two exact?s proves the given statement (+ Hamiltonian hypothesis)

import Mathlib
def SimpleGraph.Walk.IsHamiltonian.equivFin {α : Type*} [DecidableEq α] (G : SimpleGraph α) {a b : α} (p : G.Walk a b) (h : p.IsHamiltonian) : α ≃ Fin p.support.length := by
  refine (List.Nodup.getEquivOfForallMemList p.support ?_ ?_).symm
  · exact List.nodup_iff_count_eq_one.mpr fun a_1 a => h a_1
  · exact fun x => mem_support h x

[Snir Broshi]

Wow, thanks! Do you think Mathlib will accept something like this?

[Vlad Tsyrklevich]

There is already https://leanprover-community.github.io/mathlib4_docs/Mathlib/Combinatorics/SimpleGraph/Hamiltonian.html#SimpleGraph.Walk.IsHamiltonian.length_eq for the case of Fintype \a, does that work?

[Jakub Nowak]

As a side note, I would suggest making (p : G.Walk a b) argument implicit. It can be deduced from (h : p.IsHamiltonian).

[Vlad Tsyrklevich]

This instance seems fairly nice to have:

instance SimpleGraph.Walk.IsHamiltonian.finite {V : Type*} [DecidableEq V] {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (h : p.IsHamiltonian) : Finite V := by
  refine finite_iff_exists_equiv_fin.mpr ⟨p.support.length, ⟨?_⟩⟩
  refine (List.Nodup.getEquivOfForallMemList p.support ?_ ?_).symm
  · exact List.nodup_iff_count_eq_one.mpr fun a_1 a => h a_1
  · exact fun x => mem_support h x

I'll clean it up and submit it

[Jakub Nowak]

What's the use case for SimpleGraph.Walk.IsHamiltonian.finite?

[Jakub Nowak]

Ah, it's an instance. Yeah, it does sound useful.

[Jakub Nowak]

I think, you could also do docs#Fintype ?

[Jakub Nowak]

Or even only docs#Fintype, as docs#Finite follows from docs#Fintype.

[Lawrence Wu (llllvvuu)]

I’m not sure if that instance will ever be synthesized, since it takes a proof (AFAIK instances only get synthesized from other instances). I wouldn’t add a Fintype instance for sure, because it’s data, you will get diamonds. You only want to add such an instance if it’s canonical.

[Vlad Tsyrklevich]

Is the proper procedure in cases like this to leave it as a def then? It seems useful to be able to able to get a Finite instance, and though I doubt there's many people working with SimpleGraph constructively, Fintype as well I suppose

[Robin Arnez]

I don't think it's possible to make this into an instance (even if IsHamiltonian would be a class) since instance search always goes backwards and there no way to determine h, p, u, v or G from Finite V

[Robin Arnez]

You can keep this as a theorem and then use have := h.finite at the use site though

[Jakub Nowak]

If it's def, and not instance, than wouldn't adding Fintype be fine?

[Vlad Tsyrklevich]

#29502

[Jakub Nowak]

The name's a bit ambiguous in my opinion. Maybe IsHamiltonian.finiteVerts or IsHamiltonian.finiteVertex? Not sure which one.

[Jakub Nowak]

Plural makes more sense grammatically to me. But e.g. SimpleGraph.instFiniteConnectedComponent uses singular.

[Snir Broshi]

FWIW there's also #30149 #30206 #30224