feat: shortlex order on lists

[hannahfechtner]

Given a relation r on a type α, the shortlex order over r on lists (first compare by length; if equal, then compare by lexicographic order over r) is defined. We prove that this inherits properties from the underlying relation r such as trichotomous-icity, asymmetry, order-connectedness.

Most importantly, Shortlex r is well-founded if r is well-founded, giving a well-founded order on lists. (Notably, List.Lex is not well-founded).

---

[github-actions]

messageFile.md

[eric-wieser]

Some initial comments, sorry for not having time right now for a more thorough review.

[eric-wieser]

The naming largely looks good now, thanks! (or at least, as good as the existing List.Lex naming...)

Perhaps @vihdzp has some opinions around the names of the WellFounded stuff, and whether some instances are missing.

[hannahfechtner]

I noticed that there is something going on with aux in a number of the List.Lex instances - it got too long to type here so I posted on Zulip: https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/aux.20appearing.20in.20instance

[vihdzp]

Initial remarks. I expect that there's a lot of golfing that can be done here.

[github-actions]

messageFile.md

[github-actions]

messageFile.md

[github-actions]

messageFile.md

[github-actions]

messageFile.md

[github-actions]

messageFile.md

[github-actions]

messageFile.md

[github-actions]

messageFile.md

[eric-wieser]

If you merge master, then the bot will stop posting such silly messages!

[github-actions]

PR summary ec90975413

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Data.List.Shortlex (new file)	605

---

Declarations diff

+ InvImage.isAsymm
+ InvImage.trichotomous
+ IsAsymm
+ Shortlex
+ _root_.Acc.shortlex
+ _root_.List.shortlex_def
+ _root_.List.shortlex_iff_lex
+ append_left
+ append_right
+ cons_iff
+ isAsymm
+ isTrichotomous
+ nil_left_or_eq_nil
+ not_nil_right
+ of_length_lt
+ of_lex
+ singleton_iff
+ wf

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 script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

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).

[madvorak]

We certainly want to have Shortlex in Mathlib!