Instances on `sum.elim A B i`

Stream: Is there code for X?

[Eric Wieser]

Do instances like this exist somewhere? Should they?

instance sum.elim.add_comm_monoid {ι₁ ι₂ : Type}
  {M : ι₁ → Type*} [∀ i, add_comm_monoid (M i)]
  {N : ι₂ → Type*} [∀ i, add_comm_monoid (N i)]
  (i : ι₁ ⊕ ι₂)
  : add_comm_monoid (i.elim M N) := by cases i; dsimp; apply_instance

[Kevin Buzzard]

You can just take the pi type and then the product, right?

[Eric Wieser]

Can you elaborate on that?

[Kevin Buzzard]

Isn't this just (Pi i, M i) x (Pi j, N j)?

[Eric Wieser]

Isomorphic to, yes; but I can't express that as a bundled isomorphism without the instances on each end

[Eric Wieser]

And in this case, I need it as a single pi type in order to pass it to multilinear_map

[Anne Baanen]

There is precedent for sum.elim instance(-ish) definitions: docs#linear_independent.sum_type docs#measurable.sum_elim docs#category_theory.pi.sum_elim_category

[Reid Barton]

This surely can't be sustainable

[Eric Wieser]

@Reid Barton, because they'd be needed for other recursors too?

[Eric Wieser]

Duplicating the algebra pi instances for sum.elim doesn't strike me as too bad

[Reid Barton]

In principle it's every class

[Reid Barton]

The pi instances at least have something to do with the classes

[Eric Wieser]

Ah, I see your point

[Reid Barton]

I'm not sure what the right way to handle this is though

[Eric Wieser]

So to be clear, the issue here is not that it makes sum look special, but that a sum_elim instance ends up written for every typeclass

[Reid Barton]

I think there are more issues lurking around the corner, like whether Lean will realize that the instance for (sum.inl i).elim M N is the same as that for M i

[Eric Wieser]

Those two things are equal by rfl though?

[Eric Wieser]

Is that iota reduction, or am I misremembering?

[Reid Barton]

Sure but that doesn't mean instance selection will necessarily understand they are the same

[Reid Barton]

This stuff is easier with bundled objects I think

[Reid Barton]

Eric Wieser said:

So to be clear, the issue here is not that it makes sum look special, but that a sum_elim instance ends up written for every typeclass

You could also find other things in place of sum, like sigma or ite

[Reid Barton]

Like if C x is a group and C y is a group then C (if b then x else y) is a group

[Reid Barton]

or technically it could be nested too, like if C (X i) and C (Y j) are groups then C (s.elim X Y) is a group

[Gabriel Ebner]

Reid Barton said:

I think there are more issues lurking around the corner, like whether Lean will realize that the instance for (sum.inl i).elim M N is the same as that for M i

I don't expect any issues here. I'd be more worried about the ∀ i, ... assumption; this causes Lean to do higher-order unification. Sébastien has had all kinds of bad experiences with that. In any case, it's a lot of instances but that can and should be automated.

[Eric Wieser]

I did run into a problem here where I couldn't unify sum.elim (fun _, T) (fun _, T) with (fun _, T)

[Gabriel Ebner]

That's because it's not definitionally equal.

[Eric Wieser]

Indeed

[Gabriel Ebner]

But you could add an instance like this:

instance {α ι κ} [group α] (i : ι ⊕ κ) : group (i.elim (λ _, α) (λ _, α)) := by cases i; apply_instance

[Eric Wieser]

In my case my actual problem was that I had multilinear_map R (sum.elim (λ i : ι₁, M) (λ i : ι₂, M)) N but I wanted multilinear_map R (λ i : ι₁ ⊕ ι₂, M) N. I think I'm going to simplify things and avoid these sum.elim types - I only care about the non-dependent arguments anyway, and trying to generalize just creates headaches that no one needs right now.

[Reid Barton]

Yes, this kind of operation is a perfectly sensible thing to do, but unfortunately tricky to express in type theory :half_frown:

[Eric Wieser]

I spun #5178 out of what I was trying to do here, and am finding I need it even for some non-dependent functions