not porting pi_instance

Stream: mathlib4

[Floris van Doorn]

I think we should not port the pi_instance tactic. If we would use it, suppose that we faithfully port the following two instances from Lean 3.

-- Lean 3
@[to_additive]
instance group [∀ i, group $ f i] : group (Π i : I, f i) :=
by refine_struct { one := (1 : Π i, f i), mul := (*), inv := has_inv.inv, div := has_div.div,
  npow := monoid.npow, zpow := div_inv_monoid.zpow }; tactic.pi_instance_derive_field

@[to_additive]
instance comm_group [∀ i, comm_group $ f i] : comm_group (Π i : I, f i) :=
by refine_struct { one := (1 : Π i, f i), mul := (*), inv := has_inv.inv, div := has_div.div,
  npow := monoid.npow, zpow := div_inv_monoid.zpow }; tactic.pi_instance_derive_field

Now we're just making it very hard for Lean 4 to see that Pi.commGroup.toGroup is definitionally equal to Pi.group.
I think we should give these instances manually with a proper { Pi.group with ... } instance for CommGroup.

This leads to one issue: currently the pi instance for AddMonoidWithOne is in data/nat/cast/basic which doesn't import algebra/group/pi, which defines the pi instance for AddMonoid. So I think we should move the pi instance for AddMonoidWithOne to Algebra.Group.Pi and add an import from Data.Nat.Cast.Defs there. Does that mean we also have to backport that to mathlib 3?

Related Zulip: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/pi_instance.28_derive_field.29.3A.20possible.20changes.3F
Pinging @Thomas Murrills

[Scott Morrison]

I've added a link to this zulip discussion in mathlib4#980, which can proceed for now with a manually written instance.

[Thomas Murrills]

I of course can't speak to whether it would be useful or not to port it—I just don't have the knowledge yet—but I can mention that:

1. currently it's a bit of a bag of heuristics. I've been thinking about how to make it more well-rooted in mathematical practice. Given this discussion, maybe it would be better to eventually just make a wholly new tactic called e.g. defined_pointwise which only does what mathematicians regard as a pointwise definition, and nothing else. (This would, I figure, be after the port, and in this scenario we'd port without pi_instance.) This might then make it easier to trust that things are definitionally equal? I'm not sure though, since I'm not sure what actually causes the definitional equality problem referred to here.
2. Using pi_instance with the ported refine_struct functionality would still allow people to construct { Pi.group with <...> } before using pi_instance to solve the unspecified fields. (Just wanted to make sure that was clear, since I'm still not totally clear on the problem.)
3. If I instead port pi_instance as planned, and stay faithful to what's written in mathlib3, it would depend on the refine_struct functionality being added to core, which would mean we'd be waiting on that. It might help the port to say "just do it manually"? (Though, there miiiight be a workaround if people want pi_instance ASAP—I'm not totally sure, but I could think about it.)

[Eric Wieser]

Is pi_instance used much in mathlib3?

[Yaël Dillies]

Its job is very straightforward, so I've never used it myself even when I had the chance.

[Eric Wieser]

Yes, I guess you can almost always just write some_proj := λ _ _, funext $ λ _, some_proj _ _

[Eric Wieser]

I'm very puzzled by the fact that pi_instance is using set.image

[Eric Wieser]

Is that for Sup/Inf?

[Thomas Murrills]

(I do think sometimes there are many, many fields one would have to rewrite, which pi_instance could be useful for—not sure it's essential in the port though.)

[Thomas Murrills]

Also, not everything that needs to be provided is of the same form, as shown by the dependence on set.image. (I think this could be generalized so it's not so ad-hoc, though.)

[Thomas Murrills]

So, where did we land on this? algreba.group.pi is ready to port, which uses it (or rather, its component non-interactive tactic, pi_instance_derive_field) extensively. I'd be happy either

1. taking on the port of this file immediately without pi_instance by using all the instances as with-sources manually and filling in any missing fields by hand
2. making/rushing a basic version of pi_instance that doesn't depend on the refine_struct functionality and hopefully takes care of most cases while being imperfect (time needed: a couple to a few days?)

(If I did (1), I figure I could go back and clean it up after pi_instance is available.)

(Though, @Floris van Doorn, just checking, was the implication that you were planning on porting it? I'm more than happy doing it myself, I just want to make sure I'm not stepping on any toes if I do.)

In terms of urgency: looking at the graphs, it might be a little while until this file is needed in algebra.big_operators.basic, but having it sooner might make some progress in the thicket of topology.metric_space.basic.

[Thomas Murrills]

It also seems fairly high up in data.real.basic.

[Thomas Murrills]

If there are no objections I'll start porting it manually, and convert explicit data fields into with-sources where I can, as per Floris' suggestion?

[Floris van Doorn]

I was not claiming it. Please go ahead and port it manually!