HasAdj

Stream: graph theory

[Iván Renison]

Creating a new topic for this discussion
I opened #35776 and #35777 as WIP, to work in this. I would appreciate your feedback on how I'm doing it
Some points about the first one defining HasAdj:

• For the set of vertices Graph uses vertexSet, but I used verts, as in #33466 for Digraph
• What variable name should I use for an arbitrary kind of graph? I used Gr, but I don't know if it is the best
• Should {left, right}_mem_vertexSet_of_adj have implicit or explicit parameters? I made them implicit, but when using them I was not sure

[Shreyas Srinivas]

Feel free to reuse my walk code with attribution. It’s solid at this point

[Iván Renison]

Yes, I have been looking at it. However having the vertex set makes it quite different

[Shreyas Srinivas]

You have a bunch of List.attach and List.unattach lemmas to use

[Shreyas Srinivas]

Here’s my subgraph version from a private repo

import Mathlib

namespace SimpleGraph

namespace Subgraph

structure Walk' {G : SimpleGraph V} (H : G.Subgraph) where
  support : List H.verts
  non_empty_support : support ≠ []
  chainAdj : List.IsChain H.Adj support

def Walk'.startsAt {G : SimpleGraph V} {H : G.Subgraph}
  (W : H.Walk') : V :=
  W.support.head W.non_empty_support

def Walk'.endsAt {G : SimpleGraph V} {H : G.Subgraph}
  (W : H.Walk') : V :=
  W.support.getLast W.non_empty_support

def IsCircuit {G : SimpleGraph V}
  {H : G.Subgraph}
  (W : H.Walk') : Prop :=
  W.support.length > 2 ∧ W.support.head = W.support.getLast


structure Path' {G : SimpleGraph V} (H : G.Subgraph) extends Walk' H where
  nodup : List.Nodup support

def IsCycle {G : SimpleGraph V}
  {H : G.Subgraph}
  (P : H.Path') : Prop :=
  IsCircuit P.toWalk'

def Walk'.Length {G : SimpleGraph V}
  {H : G.Subgraph}
  (W : H.Walk') :=
  W.support.length

def Walk'.Single
  {G : SimpleGraph V}
  {H : G.Subgraph} (u : H.verts) : H.Walk' where
  support := [u]
  non_empty_support := by simp
  chainAdj := by
    apply List.IsChain.singleton

def Path.Single {G : SimpleGraph V}
  {H : G.Subgraph}
  (u : H.verts) : H.Path' where
  support := [u]
  non_empty_support := by simp
  chainAdj := by
    apply List.IsChain.singleton
  nodup := by
    simp_all

def Walk'.cons {G : SimpleGraph V}
  {H : G.Subgraph}
  (u : H.verts) (W : H.Walk')
  (hAdj : (hnempty : W.support ≠ [])
    → H.Adj u (W.support.head hnempty))
  : H.Walk' where
  support := u :: W.support
  chainAdj := by
    have hchainW := W.chainAdj
    cases hW : W.support with
    | nil =>
        simp
    | cons head tail =>
        simp
        rw [hW] at hchainW hAdj
        constructor
        · simp_all only [ne_eq, reduceCtorEq, not_false_eq_true, List.head_cons, forall_const]
        · simp_all only [ne_eq, reduceCtorEq, not_false_eq_true, List.head_cons, forall_const, List.pure_def,
          List.bind_eq_flatMap, List.flatMap_cons, List.flatMap_subtype, List.flatMap_singleton', List.cons_append,
          List.nil_append]

  non_empty_support := by
    cases W.support <;> simp

def Walk'.tail {G : SimpleGraph V}
  {H : G.Subgraph}
  (W : H.Walk') (hW : W.support.length ≥ 2): H.Walk' where
  support := W.support.tail
  chainAdj := by
    have hWfull := W.chainAdj
    simp_all
    apply List.IsChain.tail
    sorry
  non_empty_support := by
    cases h : W.support with (simp_all)
    | cons head tail =>
        cases htail : tail with (simp_all)




def Path.cons {G : SimpleGraph V}
  {H : G.Subgraph}
  (u : H.verts) (W : H.Path')
  (hnewvertex : List.Nodup (u :: W.support))
  (hAdj : (hnempty : W.support ≠ [])
    → H.Adj u (W.support.head hnempty))
  : H.Path' where
  support :=
    match W.support with
    | [] => [u]
    | v :: vs => u :: v :: vs
  non_empty_support := by cases W.support <;> simp
  chainAdj := by
    have hchainW := W.chainAdj
    cases hW : W.support with
    | nil =>
        simp
    | cons head tail =>
        simp
        rw [hW] at hchainW hAdj
        constructor
        · simp_all only [ne_eq, reduceCtorEq, not_false_eq_true, List.head_cons, forall_const]
        · simp_all


  nodup := by
    induction hW : W.support with
    | nil =>
        simp
    | cons head tail ih =>
        simp_all

def Walk'.edgeList {G : SimpleGraph V}
  {H : G.Subgraph} (W : H.Walk') : List <| Sym2 H.verts :=
  match hW : W.support with
  | []
  | [_] => []
  | v :: w :: ws =>
      s(v,w) :: (edgeList <| W.tail (by simp [hW]))
  termination_by W.support.length
  decreasing_by
    simp [Walk'.tail, hW]

lemma isWalk'Edge_vert_support_left (G : SimpleGraph V)
  {H : G.Subgraph}
  (W : H.Walk') (x y : H.verts)
  (hxy : s(x, y) ∈ W.edgeList)
  : x ∈ W.support := by
  revert hxy
  fun_induction Walk'.edgeList
  · expose_names
    simp_all
  · expose_names
    grind
  · expose_names
    simp_all
    rintro (⟨x_eq_v, y_eq_w⟩ | hrest)
    · left
      assumption
    · right
      simp_all
    · specialize ih1 hrest
      right
      simp [hW, Walk'.tail] at ih1
      assumption

lemma isWalk'Edge_vert_support_right {G : SimpleGraph V}
  (H : G.Subgraph)
  (W : H.Walk') (x y : H.verts) (hxy : s(x, y) ∈ W.edgeList)
  : y ∈ W.support := by
  revert hxy
  fun_induction Walk'.edgeList
  · expose_names
    simp_all
  · expose_names
    grind
  · expose_names
    simp_all
    rintro (⟨x_eq_v, y_eq_w⟩ | hrest)
    · right; left
      assumption
    · expose_names
      left
      exact h.right
    · specialize ih1 hrest
      simp [hW, Walk'.tail] at ih1
      right
      assumption


abbrev Walk'.isWalkEdge {G : SimpleGraph V} {H : G.Subgraph}
  (W : H.Walk') (x y : H.verts) :=
    s(x,y) ∈ W.edgeList

abbrev Path'.isPathEdge {G : SimpleGraph V}
  {H : G.Subgraph}
  (P : H.Path') (x y : H.verts) :=
    s(x,y) ∈ P.edgeList

abbrev PathFromTo {G : SimpleGraph V}
  {H : G.Subgraph} (P : H.Path') (s t : H.verts) :=
  P.startsAt = s  ∧ P.endsAt = t

def Walk'.length {G : SimpleGraph V}
  {H : G.Subgraph}
  (W : H.Walk') := W.support.length - 1

def Path.length {G : SimpleGraph V} {H : G.Subgraph}
  (P : H.Path') := P.support.length


def Walk'.reverse {G : SimpleGraph V}
  {H : G.Subgraph}
  (W : H.Walk') : H.Walk' where
  support := W.support.reverse
  non_empty_support := by
    exact List.reverse_ne_nil_iff.mpr W.non_empty_support
  chainAdj := by
    refine List.isChain_reverse.mpr ?_
    have flip_eq_symm : flip (G.Adj) = G.Adj := by
      unfold flip
      apply funext
      intro v
      apply funext
      intro w
      apply propext
      constructor
      all_goals
        intro hadj
        apply G.symm
        assumption

    rw [flip_eq_symm]
    exact W.chainAdj

@[simp]
lemma Walk'.reverse_support_eq_support_reverse
  {G : SimpleGraph V}
  {H : G.Subgraph}
  (W : H.Walk')
  : W.reverse.support = W.support.reverse := by
    rfl

lemma Walk'.reverse_startsAt_endsAt {G : SimpleGraph V}
  {H : G.Subgraph}
  (W : H.Walk') : W.startsAt = v → W.reverse.endsAt = v := by
  intro hstart
  simp_all [startsAt, endsAt]


lemma Walk'.reverse_endsAt_startsAt {G : SimpleGraph V}
  {H : G.Subgraph}
  (W : H.Walk') : W.endsAt = v → W.reverse.startsAt = v := by
  intro hstart
  simp_all [startsAt, endsAt]

@[simp]
def Walk'.append₁ {G : SimpleGraph V} {H : G.Subgraph} (W W' : H.Walk')
  (hjoin : H.Adj W.endsAt W'.startsAt) : G.Walk' where
  support := W.support ++ W'.support
  non_empty_support := by
    exact List.append_ne_nil_of_left_ne_nil W.non_empty_support W'.support
  chainAdj := by
    have W_adj := W.chainAdj
    have W'_adj := W'.chainAdj
    cases h : W'.support with
    | nil =>
        simp_all

    | cons head tail =>
        refine List.isChain_append.mpr ?_
        simp_all
        intro x hx
        have s₁ : head = W'.startsAt := by
          simp [startsAt, h]
        have s₂ : x = W.endsAt := by
          simp [endsAt]
          exact Eq.symm (List.getLast_of_mem_getLast? hx)
        rw [s₁, s₂]
        exact hjoin

@[simp]
lemma Walk'.append₁_startsAt {G : SimpleGraph V}
  {H : G.Subgraph}
  (W₁ W₂ : H.Walk') (h12 : H.Adj W₁.endsAt W₂.startsAt)
  : (W₁.append₁ W₂ h12).startsAt = W₁.startsAt := by
  sorry

@[simp]
lemma Walk'.append₁_endsAt {G : SimpleGraph V}
  (W₁ W₂ : G.Walk') (h12 : G.Adj W₁.endsAt W₂.startsAt)
  : (W₁.append₁ W₂ h12).endsAt = W₂.endsAt := by
  sorry

@[simp]
def Walk'.append₂ {G : SimpleGraph V}
  {H : G.Subgraph}
  (W W' : H.Walk')
  (heq: W.endsAt = W'.startsAt) : H.Walk' where
  support := W.support ++ W'.support.tail
  non_empty_support := by
    apply List.append_ne_nil_of_left_ne_nil W.non_empty_support
  chainAdj := by
    have W_adj := W.chainAdj
    have W'_adj := W'.chainAdj
    cases hW'support : W'.support with
    | nil =>
        simp_all
    | cons W'head W'tail =>
        refine List.isChain_append.mpr ?_
        simp_all
        constructor
        · exact List.isChain_of_isChain_cons W'_adj
        · have s₁ : W'.startsAt = W'head := by
            simp_all [startsAt]
          rw [←s₁] at hW'support
          intro x x_is_Wlast
          -- Prove that x is actually W'head
          have s₂ : W.support.getLast W.non_empty_support = x := by
            exact List.getLast_of_mem_getLast? x_is_Wlast
          have s₃ : W.endsAt = x := by
            exact s₂
          simp_all
          -- now deal with W'tail and y
          intro y hW'tail
          cases hW'tail' : W'tail with
          | nil =>
              simp_all
          | cons W'tail'head W'tail'tail =>
              rw [hW'tail'] at W'_adj
              simp at W'_adj
              simp [hW'tail'] at hW'tail
              rw [←hW'tail]
              exact W'_adj.left



@[simp]
lemma Walk'.append₂_startsAt {G : SimpleGraph V}
  {H : G.Subgraph}
  (W₁ W₂ : H.Walk') (h12 : W₁.endsAt = W₂.startsAt)
  : (W₁.append₂ W₂ h12).startsAt = W₁.startsAt := by
  sorry

@[simp]
lemma Walk'.append₂_endsAt {G : SimpleGraph V}
  {H : G.Subgraph}
  (W₁ W₂ : H.Walk') (h12 : W₁.endsAt = W₂.startsAt)
  : (W₁.append₂ W₂ h12).endsAt = W₂.endsAt := by
  sorry


end Subgraph


end SimpleGraph

[Iván Renison]

For Darts I opened #35783, and now I will continue with Walk

[Iván Renison]

For the definition of Walk.darts (which is currently recursive) I wanted a function to get the pairs of consecutive elements of a list, and use that in the support, combined with a map. I found that in the documentation as docs#Mathlib.Tactic.BicategoryLike.pairs. It is exactly what I want, but in a strange namespace, should I move it to the files about List, it or use it as it is?

[Iván Renison]

Shreyas Srinivas said:

Here’s my subgraph version from a private repo

With this, I was thinking that, for having walks in subgraphs, maybe we could make subgraphs an instance of HasAdj. What do you think?

[Shreyas Srinivas]

Btw all my code snippets are Apache 2.0, which means you can freely use them with attribution.

[Shreyas Srinivas]

Iván Renison said:

Shreyas Srinivas said:

Here’s my subgraph version from a private repo

With this, I was thinking that, for having walks in subgraphs, maybe we could make subgraphs an instance of HasAdj. What do you think?

It might simplify things upto a point

[Shreyas Srinivas]

I don't see masses of simplification here.

[Snir Broshi]

Iván Renison said:

I found that in the documentation as docs#Mathlib.Tactic.BicategoryLike.pairs. It is exactly what I want, but in a strange namespace, should I move it to the files about List, it or use it as it is?

You could create a new function, or just inline support.zip support.tail |>.map ....
If you're creating a new function I suggest .tail over the existing .drop 1.

[Iván Renison]

Now #35831 has HasAdj.Walk with recursive definition

[Iván Renison]

And I marked the first one, #35776, as ready for review

[Iván Renison]

I was thinking, is HasAdj the best name for this? With it, it is not obvious that it is for graphs, I was thinking that maybe it could be named GraphLike, although that may be confusing because Graph in Mathlib is multigraphs. What do you think?