feat: run-length encoding

[vihdzp]

---

• depends on: [Merged by Bors] - feat: characterization of List.splitBy #30898

Moved from #17105.

[github-actions]

PR summary c11f04c211

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Data.List.RunLength (new file)	299

---

Declarations diff

+ flatten_map_runLength
+ isChain_runLength
+ isChain_runLengthAux
+ runLength
+ runLengthRecOn
+ runLengthRecOnAux
+ runLengthRecOn_append
+ runLengthRecOn_nil
+ runLength_append
+ runLength_append_cons
+ runLength_eq_nil
+ runLength_flatten_map
+ runLength_inj
+ runLength_injective
+ runLength_nil
+ runLength_replicate
+ splitBy_beq
+ splitBy_beq_replicate
+ splitBy_eq_singleton

You can run this locally as follows

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

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

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

---

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

Current number	Change	Type
6902	1	backward.isDefEq.respectTransparency

Current commit 61fa908e8c
Reference commit c11f04c211

You can run this locally as

./scripts/reporting/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).

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - feat: characterization of List.splitBy #30898
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[joneugster]

runLength seems reasonable to add.

Please avoid empty PR descriptions in future PRs. Even a single sentence about what you're adding or why you need it would be helpful for context when first opening a PR.

[joneugster]

since you're already using ℕ+ wouldn't it be nicer to formulate these lemmas in terms of (n : ℕ+)?

[joneugster]

Suggested change

	(l.runLength.map fun x ↦ replicate x.1 x.2).flatten = l := by
	(l.runLength.map fun (n, a) ↦ replicate n a).flatten = l := by

and in other places

[plp127]

This creates a fun x => match x with | (n, a) => ..., which looks ugly when pretty-printed.