Equivalence Relation for Walks on Graphs

Stream: mathlib4

[Fred Rajasekaran]

I'm trying to define an equivalence relation for certain types of walks on simple graphs, but it's been somewhat challenging.

I am considering walks that have loops (consecutive visits to the same vertex) allowed which I defined an inductive type for (similar to how walks are in mathlib now). I am considering walks on the complete graph on n vertices, and I would like to establish an equivalence relation in which two walks are equivalent if they are the same up to a permutation of the vertices.

However, the inductive type LoopWalk u v depends on the starting and ending vertices, so in order to even write the statement that one walk is equal to another after relabeling the vertices by some permutation, I need to provide a proof that the endpoints are the same under the permutation. I'm having some trouble implementing this.

For example, in identityWalkMap, I'm not sure how to state the lemma correctly, and I had to modify loopWalkEquiv to be in its current form (requiring a proof that the endpoints are the same). Any advice for proving the equivalence relation properties in LoopWalkSetoid would also be greatly appreciated.

import Mathlib.Combinatorics.SimpleGraph.DeleteEdges
import Mathlib.Data.Finset.Basic

universe u v w

namespace SimpleGraph

variable {V : Type u} {V' : Type v}
variable (G : SimpleGraph V) (G' : SimpleGraph V')

/-A walk on a simple graph that allows consecutive visits to the same vertex.-/
inductive LoopWalk' : V → V → Type u
  | nil {u : V} : LoopWalk' u u
  | cons {u v w : V} (h : G.Adj u v) (p : LoopWalk' v w) : LoopWalk' u w
  | loop {u v : V} (p : LoopWalk' u v): LoopWalk' u v
  deriving DecidableEq

namespace LoopWalk'

variable {G}

/- The length of a walk is the number of edges/darts along it. -/
def length {u v : V} : G.LoopWalk' u v → ℕ
  | nil => 0
  | cons _ q => q.length.succ
  | loop q => q.length.succ

/-The pushforward of a graph homorphism to LoopWalks.-/
protected def map (f : G →g G') {u v : V} : G.LoopWalk' u v → G'.LoopWalk' (f u) (f v)
  | nil => nil
  | cons h p => cons (f.map_adj h) (p.map f)
  | loop p => loop (p.map f)

variable (n k : ℕ)
variable (K : SimpleGraph (Fin n)) (hk : K = completeGraph (Fin n))
variable (s : Equiv.Perm (Fin n))
variable {u v: Fin n}

/-A permuation of Fin n induces a graph isomorphims on the complete graph.-/
def permMap' (s : Equiv.Perm (Fin n)) : K ≃g K where
  toEquiv:= s
  map_rel_iff':=by
    intros a b
    rw[hk]
    rw[top_adj, top_adj]
    simp

/-The pushforward of a permutation on (Fin n) to walks on the complete graph.-/
def permMapWalk (s : Equiv.Perm (Fin n)) (p : K.LoopWalk' u v) : K.LoopWalk' (s u) (s v):=
  p.map K (permMap' n K hk s)


/-The type of all closed LoopWalks-/
abbrev ClosedLoopWalk (G : SimpleGraph V) := Σ u : V, G.LoopWalk' u u

/-The type of closed LoopWalks with length k -/
abbrev FixLengthClosedLoopWalk (k : ℕ) (G : SimpleGraph V) :=
   {p : ClosedLoopWalk G // p.2.length = k}

/-Two walks p and q are equivalent if there exists a permuation s such that q is the pushforward of
p under s.-/
def loopWalkEquiv (p q : FixLengthClosedLoopWalk k K): Prop :=
  ∃ (s : Equiv.Perm (Fin n)), ∃ (h_eq : s p.1.1 = q.1.1),
    h_eq ▸ (permMapWalk n K hk s p.1.2) = q.1.2

/-The identity permutation induces the identity map on LoopWalks.-/
lemma identityWalkMap (s : Equiv.Perm (Fin n)) (p : K.LoopWalk' u v) (hs : s = Equiv.refl (Fin n)):
  p.map K (permMap' n K hk s) = p := by sorry

/-This relation above defines an equivalence relation.-/
def LoopWalkSetoid : Setoid (FixLengthClosedLoopWalk k K) where
  r := loopWalkEquiv n k K hk
  iseqv := by
    constructor
    · intro x
      let s := Equiv.refl (Fin n)
      unfold loopWalkEquiv
      use s
      have hs (y : Fin n):  s y = y := by
        unfold s
        simp
      use hs x.1.1
      sorry
    · sorry
    · sorry

end LoopWalk'
end SimpleGraph

[Thomas Waring]

You might try taking a look at the API for SimpleGraph.Walk — particular the use of SimpleGraph.Walk.copy. I'm by no means confident with this kind of thing but I made a start at implementing something along those lines in your formalism, which let me state & prove your lemma loopWalkEquiv (mostly using simp).

import Mathlib.Combinatorics.SimpleGraph.DeleteEdges
import Mathlib.Data.Finset.Basic

universe u v w

namespace SimpleGraph

variable {V : Type u} {V' : Type v}
variable (G : SimpleGraph V) (G' : SimpleGraph V')

/-A walk on a simple graph that allows consecutive visits to the same vertex.-/
inductive LoopWalk' : V → V → Type u
  | nil {u : V} : LoopWalk' u u
  | cons {u v w : V} (h : G.Adj u v) (p : LoopWalk' v w) : LoopWalk' u w
  | loop {u v : V} (p : LoopWalk' u v): LoopWalk' u v
  deriving DecidableEq

namespace LoopWalk'

variable {G}

protected def copy {u v u' v'} (p : G.LoopWalk' u v) (hu : u = u') (hv : v = v') : G.LoopWalk' u' v' :=
  hu ▸ hv ▸ p

@[simp]
theorem copy_rfl_rfl {u v} (p : G.LoopWalk' u v) : p.copy rfl rfl = p := rfl

@[simp]
theorem copy_copy {u v u' v' u'' v''} (p : G.LoopWalk' u v)
    (hu : u = u') (hv : v = v') (hu' : u' = u'') (hv' : v' = v'') :
    (p.copy hu hv).copy hu' hv' = p.copy (hu.trans hu') (hv.trans hv') := by
  subst_vars
  rfl

@[simp]
theorem copy_nil {u u'} (hu : u = u') : (LoopWalk'.nil : G.LoopWalk' u u).copy hu hu = LoopWalk'.nil := by
  subst_vars
  rfl

theorem copy_cons {u v w u' w'} (h : G.Adj u v) (p : G.LoopWalk' v w) (hu : u = u') (hw : w = w') :
    (LoopWalk'.cons h p).copy hu hw = LoopWalk'.cons (hu ▸ h) (p.copy rfl hw) := by
  subst_vars
  rfl

@[simp]
theorem cons_copy {u v w v' w'} (h : G.Adj u v) (p : G.LoopWalk' v' w') (hv : v' = v) (hw : w' = w) :
    LoopWalk'.cons h (p.copy hv hw) = (LoopWalk'.cons (hv ▸ h) p).copy rfl hw := by
  subst_vars
  rfl

theorem copy_loop {u v u' v'} (p : G.LoopWalk' u v) (hu : u = u') (hv : v = v') :
    (LoopWalk'.loop p).copy hu hv = LoopWalk'.loop (p.copy hu hv) := by
  subst_vars
  rfl

@[simp]
theorem loop_copy {u v u' v'} (p : G.LoopWalk' u' v') (hu : u' = u) (hv : v' = v) :
    LoopWalk'.loop (p.copy hu hv) = (LoopWalk'.loop p).copy hu hv := by
  subst_vars
  rfl

/- The length of a walk is the number of edges/darts along it. -/
def length {u v : V} : G.LoopWalk' u v → ℕ
  | nil => 0
  | cons _ q => q.length.succ
  | loop q => q.length.succ

/-The pushforward of a graph homorphism to LoopWalks.-/
protected def map (f : G →g G') {u v : V} : G.LoopWalk' u v → G'.LoopWalk' (f u) (f v)
  | nil => nil
  | cons h p => cons (f.map_adj h) (p.map f)
  | loop p => loop (p.map f)

variable (n k : ℕ)
-- variable (K : SimpleGraph (Fin n)) (hk : K = completeGraph (Fin n))
abbrev K := completeGraph (Fin n)
variable (s : Equiv.Perm (Fin n))
variable {u v: Fin n}

/-A permuation of Fin n induces a graph isomorphims on the complete graph.-/
def permMap' (s : Equiv.Perm (Fin n)) : (K n) ≃g (K n) where
  toEquiv:= s
  map_rel_iff':=by
    intros a b
    rw[top_adj, top_adj]
    simp

/-The pushforward of a permutation on (Fin n) to walks on the complete graph.-/
def permMapWalk (s : Equiv.Perm (Fin n)) (p : (K n).LoopWalk' u v) : (K n).LoopWalk' (s u) (s v):=
  p.map (K n) (permMap' n s)


/-The type of all closed LoopWalks-/
abbrev ClosedLoopWalk (G : SimpleGraph V) := Σ u : V, G.LoopWalk' u u

/-The type of closed LoopWalks with length k -/
abbrev FixLengthClosedLoopWalk (k : ℕ) (G : SimpleGraph V) :=
   {p : ClosedLoopWalk G // p.2.length = k}

/-Two walks p and q are equivalent if there exists a permuation s such that q is the pushforward of
p under s.-/
def loopWalkEquiv (p q : FixLengthClosedLoopWalk k (K n)): Prop :=
  ∃ (s : Equiv.Perm (Fin n)), ∃ (h_eq : s p.1.1 = q.1.1),
    (permMapWalk n s p.1.2).copy h_eq h_eq = q.1.2

/-The identity permutation induces the identity map on LoopWalks.-/
lemma identityWalkMap (p : (K n).LoopWalk' u v) :
    p.map (K n) (permMap' n <| Equiv.refl (Fin n)) = p.copy (by simp [permMap']) (by simp [permMap']) := by
  simp only [permMap', copy_rfl_rfl]
  induction p
  case nil => simp [LoopWalk'.map]
  case cons h p ih => simpa [LoopWalk'.map]
  case loop p ih => simpa [LoopWalk'.map]


/-This relation above defines an equivalence relation.-/
def LoopWalkSetoid : Setoid (FixLengthClosedLoopWalk k (K n)) where
  r := loopWalkEquiv n k
  iseqv := by
    constructor
    · intro x
      let s := Equiv.refl (Fin n)
      unfold loopWalkEquiv
      use s
      have hs (y : Fin n):  s y = y := by
        unfold s
        simp
      use hs x.1.1
      have : _ := identityWalkMap n x.val.2
      simpa using this
    · sorry
    · sorry

end LoopWalk'
end SimpleGraph

(To make life easier I removed hypotheses like (K : SimpleGraph (Fin n)) (hK : K = completeGraph (Fin n)) by restating the theorem for completeGraph (Fin n) directly)