Duplicate IsPath API with explicit Walk argument?

Stream: graph theory

[Jakub Nowak]

Lot's of IsPath API is defined with IsPath argument explicit and Walk argument implicit, e.g. SimpleGraph.Walk.IsPath.length_lt. This is nice, as long as you have IsPath assumption in context. Unfortunately it is not so great if you don't. In this case you have to do either

example {u v : V} (p : G.Walk u v) : False := by
  have hp : p.IsPath := by sorry
  have := hp.length_lt

or

example {u v : V} (p : G.Walk u v) : False := by
  have := Walk.IsPath.length_lt (p := p) (by sorry)

If we add

theorem SimpleGraph.Walk.length_lt_of_isPath {u v : V} (p : G.Walk u v) (hp : p.IsPath) :
    p.length < Fintype.card V

we can use it like this:

example {u v : V} (p : G.Walk u v) : False := by
  have := p.length_lt_of_isPath (by sorry)

I was also considering deprecating SimpleGraph.Walk.IsPath.lenth_lt and making the argument in SimpleGraph.Walk.length_lt have a default, like this:

theorem SimpleGraph.Walk.length_lt_of_isPath {u v : V} (p : G.Walk u v) (hp : p.IsPath := by assumption) :
    p.length < Fintype.card V

which would allow replacing every hp.length_lt with p.length_lt_of_isPath. This requires having the Walk argument be named, not anonymous, though.

What do you think?

Code

import Mathlib

variable {V : Type*} [Fintype V] {G : SimpleGraph V}
open SimpleGraph

example {u v : V} (p : G.Walk u v) : False := by
  have hp : p.IsPath := by sorry
  have := hp.length_lt

example {u v : V} (p : G.Walk u v) : False := by
  have := Walk.IsPath.length_lt (p := p) (by sorry)

theorem SimpleGraph.Walk.length_lt_of_isPath {u v : V} (p : G.Walk u v) (hp : p.IsPath := by assumption) :
    p.length < Fintype.card V := by
  simp_all only [IsPath.length_lt]

example {u v : V} (p : G.Walk u v) (hp : p.IsPath) : ∃ n, p.length < n := by
  use Fintype.card V
  exact p.length_lt_of_isPath

[Snir Broshi]

AFAIK some theorems have multiple aliases to allow for more dot notation like you want, but most theorems just choose one of the arguments that makes the most sense to use for dot notation.
If you're suggesting adding alias Walk.length_lt_of_isPath := Walk.IsPath.length_lt then I'm for it, but if we're only keeping a single alias then I prefer the current IsPath version.

[John Talbot]

I think I also slightly prefer the current IsPath API pattern with the Walk argument typically implicit.

Even when you don't have the correct IsPath assumption in context the current version can still be very handy, e.g.

example {u v w : V} {p : G.Walk v w} (hp : p.IsPath) (h : u ∈ p.support) :
    (p.takeUntil u h).length < Fintype.card V := by
  exact (hp.takeUntil h).length_lt

[Jakub Nowak]

John Talbot said:

I think I also slightly prefer the current IsPath API pattern with the Walk argument typically implicit.

Even when you don't have the correct IsPath assumption in context the current version can still be very handy, e.g.

example {u v w : V} {p : G.Walk v w} (hp : p.IsPath) (h : u ∈ p.support) :
    (p.takeUntil u h).length < Fintype.card V := by
  exact (hp.takeUntil h).length_lt

If, instead of by assumption we use more advanced tactic (based on grind or simp maybe?), then this could be written as:

example {u v w : V} {p : G.Walk v w} (hp : p.IsPath) (h : u ∈ p.support) :
    (p.takeUntil u h).length < Fintype.card V := by
  exact (p.takeUntil u h).length_lt_of_isPath

So, not much change. But with let binding you could have avoided writing .takeUntil twice.

[Jakub Nowak]

So I think, we should strive to automate IsPath. Like automation of array bound checks e.g. So then, you actually don't have to prove it (manually) at all in many simple cases.

[John Talbot]

Perhaps, but just swapping assumption for grind / simp / aesop will currently fail in this example.

Also in most simple cases the corresponding lemma (like IsPath.takeUntil) should exist so perhaps adding missing lemmas of this form could help avoid the original problem?