pi_instance(_derive_field): possible changes?

Stream: mathlib4

[Thomas Murrills]

I’ve been thinking about pi_instance_derive_field (which is a component of pi_instance) and pi_instance, which I’ve claimed on the tactic porting doc, and I think there might be a couple chances to improve them:

1) pi_instance_derive_field only ever occurs after refine_struct. This seems like a chance to write a better tactic—why not simply give (the new version of) pi_instance an optional argument, so that we don’t need to have a boilerplate refine beforehand? (Plus, then there’s only one concept floating around, instead of two separate-but-related ones.)

(Note: this accounts for about 1/2-2/3 of the uses of refine_struct in mathlib, depending on how you count, so while it’s significant, we still need refine_struct functionality separately!)

[Thomas Murrills]

2) Π as syntax for dependent function types is going away in Lean 4. As such, I think we should rename pi_instance. Also, many mathematicians don’t use or know the term “pi type”, and given that pi_instance is documented as “Automation for creating instances of mathematical structures for pi types”, it would be nice for it to be mathematician-friendly.

A couple options I can think of are

• fromPointwise
• instanceFromPointwise

since that’s roughly what this tactic does: take a pointwise definition of a structure and lift that structure to the function type. The notion of something being “defined pointwise” is pretty familiar to mathematicians, and so maybe this tactic could benefit from a name that involved “pointwise” somehow. :)

[Thomas Murrills]

Just wanted to see if people think these are good ideas and if I should enact them in the port! :)

[Mario Carneiro]

Hi @Thomas Murrills , as you know we are trying to avoid major refactors at this time. If it is possible, we would like to stick to the implementation as it exists, at least for backward compatibility purposes. Renaming Pi at this point seems like a bad idea given the number of places it shows up in various ways in mathlib. There also isn't a suitable replacement; forall is the name used in the lean 4 sources for this operator but this is confusing from a mathematical perspective to apply to any dependent function type. I think we should just stick to using Pi when referring to the dependent function type in theorem names and tactic names.

[Mario Carneiro]

Re: (1), I don't think it's necessarily always a good idea to combine tactics together, although this can certainly be done as a macro in lean 4 if it is easier to use that way. Note that pi_instance_derive_field is not even an interactive tactic in lean 3 (it is a direct call to tactic.pi_instance_derive_field), which indicates that making it easy to write is not a top priority in mathlib. If however it is more difficult to write the tactics separately rather than together, (and this doesn't involve duplicating all the code of refine_struct,) then it is reasonable to consider combining them for that reason.

[Thomas Murrills]

Re: renaming: Ah, I see. I only meant to suggest the rename of pi_instance, and I wasn’t aware the use of pi was so widespread in names! :) But I can see how renaming one might mean we want to rename them all, and how that would be very difficult…

[Thomas Murrills]

Re (2), the situation is that pi_instance itself is pretty much just an application of refine_struct followed by pi_instance_derive_field on every goal. It’s not that I expect it to be difficult to write them separately, but just that it would be easy to combine these (just have the optional argument to pi_instance get passed to the internal refine_struct, instead of depending on and replicating the internals of pi_instance everywhere). (That said, it might in fact be easier to write them together. I’ll find out soon!)

Though, I see how this might introduce complication in porting. There are 60-something instances of pi_instance_derive_field in mathlib, all of exactly the form refine_struct <partial structure>; tactic.pi_instance_derive_field which would have to become piInstance <partial structure> instead of refine <partial structure> <;> piInstanceDeriveField, and informing everyone porting of this could be a headache. (Unless piInstanceDeriveField had a docstring in mathlib4 that informed porters of the above? or unless it was done via something in synport, which is another headache. Either way, I’ll do whatever you (and/or others) advise here! :) )

[Mario Carneiro]

this can be done trivially in synport if required

[Mario Carneiro]

I don't think the user-side expression of the code is that important