feat(Combinatorics/GraphLike/Walks): add general walks for GraphLike structures

[Jun2M]

Per discussion at (#graph theory > HasAdj), This PR introduces the basic theory of walks as a general framework that works across different graph-like structures including SimpleGraph, Digraph, and Graph.

Main definitions

• Walk G u v: The type of walks from vertex u to vertex v in a graph-like structure G
• Walk.length: The number of edges in a walk
• Walk.support: The list of vertices visited by a walk
• Walk.darts: The list of darts (oriented edges) in a walk

---

• depends on: feat(Combinatorics/GraphLike): introduce GraphLike typeclass #36743
• depends on: feat(Combinatorics/GraphLike): GraphLike with no multi edges #39047
• depends on: feat(Combinatorics/GraphLike): introduce SymmGraphLike typeclass #36829

[github-actions]

PR summary cc26c21489

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Combinatorics.GraphLike.Basic (new file)	488
Mathlib.Combinatorics.GraphLike.Symm (new file) Mathlib.Combinatorics.GraphLike.Walks.Basic (new file)	489
Mathlib.Combinatorics.GraphLike.Walks.Simple (new file)	491

---

Declarations diff

+ Adj.left_mem
+ Adj.right_mem
+ Adj.symm
+ Adj.toStep
+ Adj.toStep_adj
+ DartAdj
+ GraphLike
+ Nil
+ Nil.eq
+ Nil.eq_nil
+ NoMultiEdgeGraphLike
+ SymmGraphLike
+ Walk
+ _root_.GraphLike.step.toWalk
+ adj_comm
+ adj_of_mem_darts
+ coe_support
+ cons'
+ cons_map_tgt_darts
+ dartStep
+ dartSym2
+ dartSym2_comp_inv
+ dartSym2_eq_iff
+ dartSym2_eq_mk'_iff
+ dartSym2_eq_mk'_iff'
+ dartSym2_inv
+ dartSym2_mk
+ dartSymm
+ dartSymm_dartSymm
+ dartSymm_involutive
+ dartSymm_mk
+ dart_eq_of_src_tgt_eq
+ dart_src_mem_support_of_mem_darts
+ darts
+ darts_cons
+ darts_eq_nil
+ darts_ext
+ darts_injective
+ darts_nil
+ darts_nodup_of_support_nodup
+ end_mem_support
+ end_mem_tail_support
+ end_mem_tail_support_of_ne
+ eq_of_length_eq_zero
+ exists_boundary_dart
+ exists_eq_cons_of_ne
+ exists_length_eq_one_iff
+ exists_length_eq_zero_iff
+ exists_step_iff_adj
+ getLast_support
+ head_support
+ instDecidable
+ instDecidableEq
+ instInhabited
+ instance (p : Walk G v w) : Decidable p.Nil
+ instance : Std.Symm (Adj G)
+ instance : Subsingleton (step G u v)
+ instance [DecidableEq D] : DecidableEq (step G u v) := Subtype.instDecidableEq
+ instance [DecidableRel (Adj G)] : DecidablePred (· ∈ darts G)
+ inv_mem_darts
+ isChain_adj_cons_support
+ isChain_adj_support
+ isChain_dartAdj_cons_darts
+ isChain_dartAdj_darts
+ length
+ length_cons
+ length_darts
+ length_eq_zero_iff
+ length_nil
+ length_support
+ map_src_darts
+ map_src_darts_append
+ map_tgt_darts
+ mem_darts_iff_adj
+ mem_darts_iff_fst_snd_infix_support
+ mem_darts_iff_infix_support
+ mem_support_iff
+ mem_support_nil_iff
+ nil'
+ nil_iff_eq_nil
+ nil_iff_length_eq
+ nil_iff_support_eq
+ nil_nil
+ noMultiEdgeSymmGraphLike
+ notNilRec
+ notNilRec_cons
+ not_nil_cons
+ not_nil_iff
+ not_nil_iff_lt_length
+ not_nil_of_ne
+ src_darts_getElem
+ src_tgt_inj
+ start_mem_support
+ step
+ step.adj
+ step.ext
+ step.ext_HEq
+ step.inv
+ step.inv_inv
+ step.inv_todart
+ step.left_eq_of_val_eq
+ step.left_mem
+ step.right_eq_of_val_eq
+ step.right_mem
+ step.src
+ step.tgt
+ step.todart
+ step.todart_dartSym2
+ step.todart_src
+ step.todart_tgt
+ step.todart_val
+ step_of_length_eq_one
+ support
+ support_cons
+ support_eq_cons
+ support_getElem_length
+ support_getElem_zero
+ support_ne_nil
+ support_nil
+ support_nonempty
+ support_subset_support_cons
+ tgt_darts_getElem
+ toProd
+ val_dartStep

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(Combinatorics/GraphLike): introduce GraphLike typeclass #36743
• feat(Combinatorics/GraphLike): GraphLike with no multi edges #39047
• feat(Combinatorics/GraphLike): introduce SymmGraphLike typeclass #36829
  By Dependent Issues (🤖). Happy coding!

[mathlib-bors]

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.