Walk.support is injective

Stream: Is there code for X?

[Daniel Weber]

Is this theorem in Mathlib?

import Mathlib

lemma SimpleGraph.Walk.support_injective {V : Type*} {G : SimpleGraph V} {u v : V} :
    Function.Injective (support (G := G) (v := v) (u := u)) := by
  sorry

if not, what would be the easiest way to prove it?

[Daniel Weber]

I'm also looking for

theorem support_append' {u v w : V} (p : G.Walk u v) (p' : G.Walk v w) :
    (p.append p').support = p.support.dropLast ++ p'.support

I managed to prove it, but it's really long and ugly

[Rida Hamadani]

Daniel Weber said:

Is this theorem in Mathlib?

import Mathlib

lemma SimpleGraph.Walk.support_injective {V : Type*} {G : SimpleGraph V} {u v : V} :
    Function.Injective (support (G := G) (v := v) (u := u)) := by
  sorry

if not, what would be the easiest way to prove it?

It is not, my first thought is intro w w' h followed by cases w.

[Vincent Beffara]

That works and is ugly, but is not that long:

import Mathlib

lemma SimpleGraph.Walk.support_injective {V : Type*} {G : SimpleGraph V} {u v : V} :
    Function.Injective (support (G := G) (v := v) (u := u)) := by

  intro w1 w2 h
  induction w2 with
  | nil =>
    rwa [← SimpleGraph.Walk.nil_iff_eq_nil, SimpleGraph.Walk.nil_iff_support_eq]
  | cons h' p ih =>
    cases w1 with
    | nil =>
      rw [support_nil, support_cons, support_eq_cons] at h
      cases h
    | cons h'' p'' =>
      simp at h
      have hhh := h
      rw [p.support_eq_cons, p''.support_eq_cons] at hhh
      simp at hhh
      rcases hhh with ⟨rfl, -⟩
      rw [ih h]

[Rida Hamadani]

Nice! Slightly shorter (but still not good looking):

import Mathlib

lemma SimpleGraph.Walk.support_injective {V : Type*} {G : SimpleGraph V} {u v : V} :
    Function.Injective (support (G := G) (v := v) (u := u)) := by
  intro w1 w2 h
  induction w2 with
  | nil =>
    rwa [← SimpleGraph.Walk.nil_iff_eq_nil, SimpleGraph.Walk.nil_iff_support_eq]
  | cons h' p ih =>
    cases w1 with
    | nil =>
      simpa [support_ne_nil] using h.symm
    | cons h'' p'' =>
      have := (List.cons_inj_right _).mp h
      rw [p.support_eq_cons, p''.support_eq_cons] at this
      aesop

[Vincent Beffara]

  import Mathlib

  lemma SimpleGraph.Walk.support_injective {V : Type*} {G : SimpleGraph V} {u v : V} :
      Function.Injective (support (G := G) (v := v) (u := u)) := by

    intro w1 w2 h
    induction w2 with
    | nil =>
      rwa [← SimpleGraph.Walk.nil_iff_eq_nil, SimpleGraph.Walk.nil_iff_support_eq]
    | cons h' p ih =>
      cases w1 with
      | nil =>
        rw [support_nil, support_cons, support_eq_cons] at h
        cases h
      | cons h'' p'' =>
        have := h
        simp at h ; rw [p.support_eq_cons, p''.support_eq_cons] at h
        aesop

Hiding DTT hell behing aesop is a good trick.

[Rida Hamadani]

I tried making it look mathlib-y:

import Mathlib

open SimpleGraph Walk

lemma support_injective {V : Type*} {G : SimpleGraph V} {u v : V} :
    Function.Injective (@support V G v u) := by
  intro w₁ w₂ h
  induction w₂ with
  | nil => rwa [← nil_iff_eq_nil, nil_iff_support_eq]
  | cons _ p₁ =>
    cases w₁ with
    | nil => simpa using h.symm
    | cons _ p₂ =>
      have := p₁.support_eq_cons ▸ p₂.support_eq_cons ▸ (List.cons_inj_right _).mp h
      aesop

This feels like a useful addition to Walk.lean! Would you like to PR it?

[Vincent Beffara]

I would think that this is not the right way to do it. Rather, I would like to have a type for walks without specified endpoints (this is generally useful to have), with its appropriate induction principle (if it's true for any nil walk and anytime one adds a step, it is always true), and then state inductivity on that type (where it is true and follows in a nicer way by induction) and deduce that version by restriction.

[Rida Hamadani]

Oh yes, that would be nice!

[Vincent Beffara]

Something like this:

import Mathlib

open SimpleGraph

variable {V : Type*} {u v : V} {G : SimpleGraph V}

structure Walk' (G : SimpleGraph V) where
  a : V
  b : V
  w : G.Walk a b

def cons' (w : Walk' G) (h : G.Adj u w.a) : Walk' G where
  a := u
  b := w.b
  w := Walk.cons h w.w

theorem induct (P : Walk' G → Prop)
    (h0 : ∀ {v}, P ⟨v, v, Walk.nil⟩)
    (h1 : ∀ w : Walk' G, ∀ {u}, ∀ (h : G.Adj u w.a), P w → P (cons' w h)) :
    ∀ w : Walk' G, P w := by
  rintro ⟨a, b, w⟩
  induction w with
  | nil => exact h0
  | cons h p ih => exact h1 ⟨_, _, p⟩ h ih

theorem inject (w1 w2 : Walk' G) (h : w1.w.support = w2.w.support) : w1 = w2 := by
  let P (w : Walk' G) := ∀ w', w.w.support = w'.w.support → w = w'
  refine induct P ?_ ?_ w1 w2 h
  · rintro v ⟨a, b, w⟩
    cases w with
    | nil => aesop
    | cons h p =>
      have := p.support_ne_nil
      simp
      aesop
  · rintro w u h1 h2 ⟨a, b, w'⟩ h3
    cases w' with
    | nil => simp [cons'] at h3
    | cons h p =>
      simp [cons'] at h3
      rcases h3 with ⟨rfl, h3⟩
      cases h2 ⟨_, _, p⟩ h3
      simp [cons']

lemma SimpleGraph.Walk.support_injective {V : Type*} {G : SimpleGraph V} {u v : V} :
    Function.Injective (support (G := G) (v := v) (u := u)) := by

  intro w1 w2 h
  have := inject ⟨_, _, w1⟩ ⟨_, _, w2⟩ h
  aesop

[Rida Hamadani]

If anybody ends up working on this, I wonder if it is a good idea to let w be of type Option (G.Walk u v), as suggested by Kyle here.

[Vincent Beffara]

I missed that discussion, what would be the point?

[Kyle Miller]

@Rida Hamadani I wouldn't do the Option thing here, since you want Walk' to represent the type of walks-without-specified-endpoints. The Option idea is only for having an object that represents edist values, and I'm not sure it's worth developing all that theory. Maybe someone someday will decide it will simplify their work with edists.

[Rida Hamadani]

Kyle Miller said:

Rida Hamadani I wouldn't do the Option thing here, since you want Walk' to represent the type of walks-without-specified-endpoints. The Option idea is only for having an object that represents edist values, and I'm not sure it's worth developing all that theory. Maybe someone someday will decide it will simplify their work with edists.

But wouldn't it make sense to have this to simplify edist of Walk'?

[Kyle Miller]

import Mathlib

open SimpleGraph

variable {V : Type*} {G : SimpleGraph V}

theorem support_append' {u v w : V} (p : G.Walk u v) (p' : G.Walk v w) :
    (p.append p').support = p.support.dropLast ++ p'.support := by
  induction p with
  | nil => simp
  | cons _ p ih =>
    rw [Walk.cons_append, Walk.support_cons, ih, Walk.support_cons,
      List.dropLast_cons_of_ne_nil, List.cons_append]
    apply Walk.support_ne_nil

[Kyle Miller]

The injectivity theorem just needs a missing support lemma, and it's not so bad:

import Mathlib

open SimpleGraph

variable {V : Type*} {G : SimpleGraph V}

lemma SimpleGraph.Walk.fst_eq_of_support_eq {u v u' v' : V} {p : G.Walk u v} {p' : G.Walk u' v'}
    (h : p.support = p'.support) : u = u' := by
  cases p <;> cases p' <;> simp at h <;> simp [h]

lemma SimpleGraph.Walk.support_injective {u v : V} :
    Function.Injective (fun (p : G.Walk u v) ↦ p.support) := by
  intro p q
  induction p with
  | nil => cases q <;> simp
  | cons _ p' ih =>
    cases q with
    | nil => simp
    | cons _ q' =>
      simp only [support_cons, List.cons.injEq, true_and]
      intro h
      cases Walk.fst_eq_of_support_eq h
      cases ih h
      rfl

[Kyle Miller]

Well, I guess that's longer than what you all already found, but still, we should have this support lemma.

[Kyle Miller]

I would strongly suggest writing fun (p : G.Walk u v) ↦ p.support rather than support (G := G) (v := v) (u := u), since the latter isn't so clear (it's not immediately clear what it's a function of)