Deprecate `p = nil` in favor of `p.Nil`?

Stream: graph theory

[Jakub Nowak]

I couldn't find equivalent of SimpleGraph.Walk.isPath_iff_eq_nil, but for SimpleGraph.Walk.Nil. (I'll add it in a PR, but that's not the point.)

I was thinking, maybe we should deprecate p = nil form in favor of p.Nil? This would have avoided the problem in the first place. We would add @[simp] theorem p = nil ↔ p.Nil, and just state all theorems in terms of p.Nil.

[Jakub Nowak]

Alternatively, we could deprecate both p = nil and p.Nil and just use e.g. p.length = 0.

[Snir Broshi]

I'm in favor of whichever method makes is possible to complete these haves:

import Mathlib
theorem foo {V : Type*} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.length = p.length := by
  match p with
  | .nil =>
    have : p.Nil := sorry
    rfl
  | _ =>
    have : ¬p.Nil := sorry
    rfl

Also I don't think it's possible to replace these p.Nil with p = nil.

[Aaron Liu]

I don't think either of those methods let you complete those haves

[Jakub Nowak]

import Mathlib

theorem foo {V : Type*} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.length = p.length := by
  match h : p with
  | .nil =>
    have : p.Nil := by
      rename_i h₁
      subst h₁
      rw [heq_eq_eq] at h
      subst h
      exact SimpleGraph.Walk.Nil.nil
    _
  | .cons _ _ =>
    have : ¬p.Nil := by
      rename_i h₁
      subst h₁
      rw [heq_eq_eq] at h
      subst h
      exact SimpleGraph.Walk.not_nil_cons
    _

Ugh, match makes this complicated. We might need lemmas like p ≍ SimpleGraph.Walk.nil → p.Nil and p ≍ SimpleGraph.Walk.cons _ _ → ¬p.Nil.
We could also make custom recursor for SimpleGraph.Walk that introduces p.Nil assumption in the base case, but I think that only works for cases and induction and not for match.