feat: deriving optics

[EdAyers]

This file defines the derive_optics T command where T is an inductive datatype.
For each constructor 𝑐 of T and each field 𝑎 : α of 𝑐, this will create the following definitions:

1. T.𝑐.𝑎? : T → Option α
2. T.𝑐.𝑎! : T → α
3. T.𝑐.with𝑎 : α → T → T
4. T.𝑐.modify𝑎 : (α → α) → T → T
5. T.𝑐.modifyM𝑎 : (α → M α) → T → M T

This eliminates some boilerplate when defining new inductive datatypes.

Additionally, if T has multiple constructors with the same field name 𝑎, it will create shortened versions of these (T.𝑎?, T.𝑎! etc).

[semorrison]

Oops, @EdAyers, I see you removed the awaiting-review tag yourself. What is the status of this PR?

[EdAyers]

Basically, I wasn't sure what the protocol was for mathlib4. I am also not sure whether this belongs in mathlib4.

[urkud]

How does modify behave if other fields depend on this one?

A semi-offtopic idea. There is .copy function used many times in mathlib that updates data fields to propositionally (but probably not definitionally) equal terms. See, e.g., local_equiv.copy. How hard would it be for you to write a command that generates this copy command (plus copy_eq and something like coe_copy/copy_apply/...)? Ideally, it should use simp-normal forms for projections (e.g., coercion instead to toFun) based on simps machinery.

[alexjbest]

@EdAyers are you interested in reviving this? Or having someone else revive it for you?
I think this is quite useful in programming applications and have been using it myself for the past couple of days (with some extra functionality) and think it deserves to be more widely available

[alexjbest]

Ah I just found https://github.com/EdAyers/lean-recursion-schemes, perhaps this PR should be closed and interested users can depend on that instead? To be fair this feels like the sort of thing that people might want without mathlib. But it seems less recently updated?

[EdAyers]

Yes I'm afraid I no longer have capacity to work on this but I think it's a valuable feature. Feel free to pick up or otherwise close.

[jcommelin]

This pull request has not seen any activity for quite a while, and it does not pass all CI checks. For these reasons, I am closing it now.

If you are still interested in getting this PR merged, please re-open the PR, update the branch, and make sure that all CI checks pass, Please label the PR with awaiting-review when ready.