feat: add Function.prod and Function.diag

[linesthatinterlace]

This PR adds Function.prod and Function.diag and develops API for them and Pi.prod.

---

[github-actions]

PR summary a8913b939b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
There are 6524 files with changed transitive imports taking up over 291544 characters: this is too many to display!
You can run ci-tools/scripts/pr_summary/import_trans_difference.sh all locally to see the whole output.

---

Declarations diff

+ comp_prod_comp
+ const_prod
+ diag
+ diag_apply
+ diag_eq_iff
+ diag_prod_diag
+ exists_diag_apply_iff
+ fst_diag
+ injective_diag
+ leftInverse_uncurry_prod_prod_fst_comp_snd_comp
+ map_comp_diag
+ map_comp_prod
+ map_diag
+ prodMap
+ prodMap_eq_prod_map
+ prod_comp
+ prod_comp_prod
+ prod_ext
+ rightInverse_uncurry_prod_prod_fst_comp_snd_comp
+ snd_diag
++ eq_prod_iff_fst_comp_snd_comp
++ eq_prod_of_fst_comp_snd_comp
++ exists_fst_comp
++ exists_prod_apply_eq
++ exists_snd_comp
++ fst_comp_prod
++ fst_prod
++ prod_apply
++ prod_const_const
++ prod_eq_iff
++ prod_ext_iff
++ prod_fst_snd_comp
++ snd_comp_prod
++ snd_prod
+-+ prod
-++ prod_fst_snd
-++ prod_snd_fst

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.

---

No changes to technical debt.

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

[SnirBroshi]

This looks very cool!

[SnirBroshi]

Question:
I don't understand why we need both Pi.prod and Function.prod. Can't we have just the general version (Pi.prod)? (Related: #36902)
If the issue is dot notation, then it's worth mentioning that leanprover/lean4#1629 had some progress recently.

[linesthatinterlace]

Yeah, that is exactly the issue I was concerned about (I also thought it was quite nice to have the dependent and non-dependent versions, in the same way that we have Function.dcomp and Function.comp). I also note that if this does get upstreamed (which I am hopeful for), Batteries and Core seem to make extremely minimal use of the "Pi" namespace. So if we do have the general version and we can make the dot notation work, I would rather call the general one Function.prod - it is more consistent with, say LinearMap.prod.

[linesthatinterlace]

Oh, that is the other reason it is quite nice to explictly have a non-dependent version - because Function.comp only works for non-dependent functions, I wanted to avoid future frustration of someone trying to use the non-dependent theorems for the dependent case. Arguably though you could just have the definition be Pi.prod and only separate the theorems by namespace, though.

It's weird because we obviously do differentiate Sigma and Prod despite the fact that in theory we could just define Prod as "Sigma in the non-dependent case". And actually as the links you post say, we also do differentiate Function.swap and flip. It feels more consistent to differentiate these.

[linesthatinterlace]

In general - why DO we have the Pi namespace?

[SnirBroshi]

I think that the difference between this situation and Sigma vs Prod (or DMatrix vs Matrix, or DFinsupp vs Finsupp) is that they are type constructors.
This means that if we were to define Prod A B := Sigma fun _ : A ↦ B then both Lean and humans would have a hard time type-checking, since it now involves comparing functions.
Here's an example of Lean getting confused because of using DMatrix with constant functions instead of Matrix.

But for Function.{flip,swap,prod,diag} I don't see any benefit in restricting when the function applies to only allow for non-dependent functions. In #36902 I also support getting rid of the duplication and only keeping the dependent version (but it requires a core PR).

I'm not sure I've articulated it well, but these feel like different situations to me.

[linesthatinterlace]

That makes sense to me. Do you see a need to keep the Pi namespace in any instance? That I think for me is the thing I don't quite understand the need for.

[SnirBroshi]

The dot-notation will only work once leanprover/lean4#13244 is merged, so if you want to use dot-notation for now I think you have to have the two separate versions and keep the non-dependent version under Function. Then the Pi namespace is a nice place to keep the dependent version.

But I thought that since you defined notation for everything here you don't use dot-notation, no?

[eric-wieser]

This change is surely out of scope

[linesthatinterlace]

I was mainly changing it because it seemed confusing to introduce the ▽ as notation and leave it in, but I am happy if you think that isn't an issue.