refactor(Combinatorics): move Walk from SimpleGraph to HasAdj

[IvanRenison]

---

Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/252551-graph-theory/topic/HasAdj/with/575843445

• depends on: feat(Combinatorics): define HasAdj for capturing the common structure of different kinds of (simple) graphs #35776
• depends on: refactor(Combinatorics): move Dart from SimpleGraph to HasAdj #35783

Replaces #35777

[github-actions]

PR summary 9b809f3970

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
60 files Mathlib.Combinatorics.Additive.Corner.Roth Mathlib.Combinatorics.Extremal.RuzsaSzemeredi Mathlib.Combinatorics.SimpleGraph.Acyclic Mathlib.Combinatorics.SimpleGraph.AdjMatrix Mathlib.Combinatorics.SimpleGraph.Bipartite Mathlib.Combinatorics.SimpleGraph.Circulant Mathlib.Combinatorics.SimpleGraph.Clique Mathlib.Combinatorics.SimpleGraph.Coloring Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite Mathlib.Combinatorics.SimpleGraph.ConcreteColorings Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp Mathlib.Combinatorics.SimpleGraph.Copy Mathlib.Combinatorics.SimpleGraph.Dart Mathlib.Combinatorics.SimpleGraph.DegreeSum Mathlib.Combinatorics.SimpleGraph.DeleteEdges Mathlib.Combinatorics.SimpleGraph.Diam Mathlib.Combinatorics.SimpleGraph.EdgeLabeling Mathlib.Combinatorics.SimpleGraph.Ends.Defs Mathlib.Combinatorics.SimpleGraph.Ends.Properties Mathlib.Combinatorics.SimpleGraph.Extremal.Basic Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity Mathlib.Combinatorics.SimpleGraph.Extremal.Turan Mathlib.Combinatorics.SimpleGraph.Finite Mathlib.Combinatorics.SimpleGraph.Finsubgraph Mathlib.Combinatorics.SimpleGraph.FiveWheelLike Mathlib.Combinatorics.SimpleGraph.Girth Mathlib.Combinatorics.SimpleGraph.Hall Mathlib.Combinatorics.SimpleGraph.Hamiltonian Mathlib.Combinatorics.SimpleGraph.Hasse Mathlib.Combinatorics.SimpleGraph.IncMatrix Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.Combinatorics.SimpleGraph.Maps Mathlib.Combinatorics.SimpleGraph.Matching Mathlib.Combinatorics.SimpleGraph.Metric Mathlib.Combinatorics.SimpleGraph.Operations Mathlib.Combinatorics.SimpleGraph.Partition Mathlib.Combinatorics.SimpleGraph.Paths Mathlib.Combinatorics.SimpleGraph.Prod Mathlib.Combinatorics.SimpleGraph.StronglyRegular Mathlib.Combinatorics.SimpleGraph.Subgraph Mathlib.Combinatorics.SimpleGraph.Sum Mathlib.Combinatorics.SimpleGraph.Trails Mathlib.Combinatorics.SimpleGraph.Triangle.Basic Mathlib.Combinatorics.SimpleGraph.Triangle.Counting Mathlib.Combinatorics.SimpleGraph.Triangle.Removal Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite Mathlib.Combinatorics.SimpleGraph.Tutte Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic Mathlib.Combinatorics.SimpleGraph.UniversalVerts Mathlib.Combinatorics.SimpleGraph.VertexCover Mathlib.Combinatorics.SimpleGraph.Walks.Basic Mathlib.Combinatorics.SimpleGraph.Walks.Maps Mathlib.Combinatorics.SimpleGraph.Walks.Operations Mathlib.Combinatorics.SimpleGraph.Walks.Subwalks Mathlib.Combinatorics.SimpleGraph.Walks.Traversal	3
Mathlib.Combinatorics.HasAdj.Basic (new file)	214
Mathlib.Combinatorics.HasAdj.Dart (new file)	491
Mathlib.Combinatorics.HasAdj.Walks.Basic (new file)	492
Mathlib.Combinatorics.Digraph.HasAdj (new file)	502
Mathlib.Combinatorics.SimpleGraph.HasAdj (new file)	524

---

Declarations diff

+ Adj.left_mem_verts
+ Adj.right_mem_verts
+ Adj.toWalk
+ HasAdj
+ Nil
+ Nil.eq
+ Nil.eq_nil
+ Walk
+ Walk.instInhabited
+ _root_.HasAdj.Dart.edge_fiber
+ adj_of_length_eq_one
+ coe_support
+ cons'
+ cons_map_snd_darts
+ dart_fst_mem_support_of_mem_darts
+ darts_cons
+ darts_eq_nil
+ 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
+ fst_darts_getElem
+ getLast_support
+ head_support
+ instance (p : Walk G v w) : Decidable p.Nil
+ instance : HasAdj α (Digraph α)
+ instance : HasAdj α (SimpleGraph α)
+ instance [DecidableEq α] (G : Gr) : DecidableEq (Dart G)
+ isChain_adj_cons_support
+ isChain_adj_support
+ length
+ length_cons
+ length_darts
+ length_eq_zero_iff
+ length_nil
+ length_support
+ map_fst_darts
+ map_fst_darts_append
+ map_snd_darts
+ 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
+ notNilRec
+ notNilRec_cons
+ not_nil_cons
+ not_nil_iff
+ not_nil_iff_lt_length
+ not_nil_of_ne
+ snd_darts_getElem
+ start_mem_support
+ support
+ support_cons
+ support_eq_cons
+ support_getElem_length
+ support_getElem_zero
+ support_ne_nil
+ support_nil
+ support_nonempty
+ support_subset_support_cons
++- isChain_dartAdj_cons_darts
+-+ darts
+-+ darts_injective
+-+ isChain_dartAdj_darts
+-+ mem_darts_iff_fst_snd_infix_support
- Dart.edge_fiber
- Dart.fst_ne_snd
- Dart.snd_ne_fst

You can run this locally as follows

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

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for scripts/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
470	1	porting notes

Current commit 39587e83a1
Reference commit 9b809f3970

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(Combinatorics): define HasAdj for capturing the common structure of different kinds of (simple) graphs #35776
• refactor(Combinatorics): move Dart from SimpleGraph to HasAdj #35783
  By Dependent Issues (🤖). Happy coding!

[IvanRenison]

#36756 is replacing this pr