[Merged by Bors] - perf: make Decidable Injective approximately twice as fast

[lambda-fairy]

The existing implementation takes the definition (∀ x y, f x = f y → x = y) directly. This is suboptimal because:

1. Every pair of values is checked twice (both (x, y) and (y, x))
2. The diagonals (x, x) are checked redundantly
3. The outputs of f are not cached, which might be a problem if f is expensive

This PR proposes a new implementation of Decidable Injective and Decidable InjOn. It collects the outputs in a Multiset, then decides Multiset.Nodup. Because Nodup is built upon List.Pairwise, which only checks unordered non-diagonal pairs, the above problems are addressed automatically.

This also allows for dropping DecidableEq on the input type, as that was to work around the diagonal case.

Thank you @edegeltje and @plp127 for suggesting List.Pairwise, and many other people in the Zulip thread for the discussion around Sym2 (which ended up being unused here, but was still valuable).

---

[github-actions]

PR summary 1f00aeb576

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ nodup_map_iff_injOn
+ nodup_map_univ_iff_injective

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

[lambda-fairy]

What's the standard way to benchmark a theorem?

I did a quick test with the snippet below, and did confirm that the old code is ~ 2x slower, but it would be nice to be more precise about this.

def testFn (i : Fin 100) : Fin 100 := i + 42

set_option maxRecDepth 100000 in
example : Function.Injective testFn := by decide

[grunweg]

A few comments: the implementation looks straightforward; I haven't really thought if there are better options.

[lambda-fairy]

Fixed conflicts from #21831.

[grunweg]

Do we want better benchmarking to confirm this? Otherwise, this looks good to me. Thanks for PRing it!
maintainer merge?

[github-actions]

🚀 Pull request has been placed on the maintainer queue by grunweg.

[j-loreaux]

While this seems straightforward and the benefit is self-evident, I'm hesitant to merge this myself because I don't know if it's possible to create diamonds here. Of course, it's a Subsingleton, so it shouldn't be too much of an issue, but I want to be sure. For that reason:

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by j-loreaux.

[urkud]

It's a pity we can't have a more efficient implementation if the codomain is a LinearOrder (this would create a non-defeq diamond).
Thanks!
bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build

[lambda-fairy]

With this code and this commit

set_option profiler true in
set_option profiler.threshold 10 in
theorem pieces_injective_of_ne_O {p : Piece} (hp : p ≠ .O) : Function.Injective (pieces p) := by
  cases p
  case O => contradiction
  all_goals decide

Before:

tactic execution of Lean.Parser.Tactic.decide took 79.6ms
tactic execution of Lean.Parser.Tactic.decide took 79.2ms
tactic execution of Lean.Parser.Tactic.decide took 69.8ms
tactic execution of Lean.Parser.Tactic.decide took 69.8ms
tactic execution of Lean.Parser.Tactic.decide took 70.9ms
tactic execution of Lean.Parser.Tactic.decide took 70.1ms
tactic execution of Lean.Parser.Tactic.tacticSeq1Indented took 14.1ms
type checking took 782ms

After:

tactic execution of Lean.Parser.Tactic.decide took 35.3ms
tactic execution of Lean.Parser.Tactic.decide took 28.9ms
tactic execution of Lean.Parser.Tactic.decide took 16.2ms
tactic execution of Lean.Parser.Tactic.decide took 15.5ms
tactic execution of Lean.Parser.Tactic.decide took 14.9ms
tactic execution of Lean.Parser.Tactic.decide took 15.1ms
type checking took 170ms

So I'm very happy with this change 😄