Why do walks take both endpoints as indices rather than one?

Stream: graph theory

[Rémi Bottinelli]

Hey, in some proof I'm doing, I think it would have been easier to have one endpoint be a parameter (so that to induct over walks, I don't have to leave it free). Is there any reason for this choice?

[Kyle Miller]

The silly reason is that if G.walk u v is a walk from u to v, and walk.cons puts edges onto the front of a walk, then you'd want u to be an index and v to be a parameter, which you can't do in this order. And one reason walk.cons puts things onto the front is so that it parallels list, since there are definitions like walk.support, which is a list of vertices in order of appearance.

[Kyle Miller]

I'm not sure I've run into this being a problem. I'm not sure exactly why that is exactly.

But one workaround that comes to mind is to use generalize to turn the endpoints into variables before your induction.

[Kyle Miller]

Another is to write the recursor you want and then do induction p using myrecursor

[Rémi Bottinelli]

I see, so it was mostly a practical choice at that point, and it doesn't seem to hurt. Thanks!

[Kyle Miller]

It wouldn't hurt to have that recursor.

@[elab_as_eliminator]
protected def walk.rec' {v : V} {motive : Π (u : V), G.walk u v → Sort*}
  (hnil : motive v walk.nil)
  (hcons : Π {u w : V} (h : G.adj u w) (p : G.walk w v), motive w p → motive u (walk.cons h p)) :
  Π {u : V} (p : G.walk u v), motive u p
| _ walk.nil := hnil
| _ (walk.cons h p) := hcons h p (walk.rec' p)
using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ x, x.snd.length)⟩]}

(though the Lean 4 version in mathlib4)

[Kyle Miller]

Maybe it'd be good to do this for walk.concat_rec too, which is the tail-centric version.