arbitrary computed fields in initialize_simps_projections

Stream: mathlib4

[Robert Maxton]

It would be nice to extend initialize_simps_projections to take advantage of generalized projection notation, as a sort of alternative to having derived fields. Right now, you can write whatever Foo.Simps.bar projections you like, but actually calling initialize_simps_projections gives

Failed to find constructor bar in structure Foo.

unless Foo was indeed defined with an explicit bar field. With the extension, we could automatically generate a standard set of derived-field lemmas for every instance/def of a structure, rather than having to explicitly write out a bunch of extra lemmas every time for any feature not originally present in the core definition.

If the community thinks this is a good idea, I wouldn't mind trying to implement this extension myself.

[Floris van Doorn]

initialize_simps_projections should already be able to generate projections of parents of a structure, and you should be able to define your custom name/definitionally equal version of such projections. E.g. here in the test file. Most of the work is done by docs#Simps.getCompositeOfProjections
What are you trying to do that doesn't work? Can you give a #mwe?

[Floris van Doorn]

If you want it to be the default behavior, without any manual configuration, that might be tricky: in some parts of Mathlib you actually care more about the parent structures than the fields of the parent structures. So I'm not sure if that is everywhere desired.

[Notification Bot]

3 messages were moved here from #general > "Missing Tactics" list by Floris van Doorn.

[Robert Maxton]

Floris van Doorn said:

If you want it to be the default behavior, without any manual configuration, that might be tricky: in some parts of Mathlib you actually care more about the parent structures than the fields of the parent structures. So I'm not sure if that is everywhere desired.

Sorry, by "derived fields" I don't mean "fields of parent structures", but rather "completely new definitions that make reference to the given structure." "Computed fields" might be a better term.

In particular, for docs#Topology.RelCWComplex, I'd like to be able to automatically generate definitions for openCell, closedCell, and cellFrontier whenever I define a new complex.

AFAIK, that's entirely new scope/behavior, so I thought it would fit better in a 'new' or 'major extension' to the existing tactic.