## Stream: Is there code for X?

### Topic: Instances on sum.elim A B i

#### Eric Wieser (Dec 01 2020 at 21:32):

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 (Dec 01 2020 at 21:57):

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

#### Eric Wieser (Dec 01 2020 at 22:00):

Can you elaborate on that?

#### Kevin Buzzard (Dec 01 2020 at 22:02):

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

#### Eric Wieser (Dec 01 2020 at 22:04):

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

#### Eric Wieser (Dec 01 2020 at 22:05):

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

#### Anne Baanen (Dec 01 2020 at 22:42):

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 (Dec 01 2020 at 22:43):

This surely can't be sustainable

#### Eric Wieser (Dec 01 2020 at 22:44):

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

#### Eric Wieser (Dec 01 2020 at 22:45):

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

#### Reid Barton (Dec 01 2020 at 22:47):

In principle it's every class

#### Reid Barton (Dec 01 2020 at 22:47):

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

#### Reid Barton (Dec 01 2020 at 22:51):

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

#### Eric Wieser (Dec 01 2020 at 22:53):

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 (Dec 01 2020 at 22:53):

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 (Dec 01 2020 at 22:53):

Those two things are equal by rfl though?

#### Eric Wieser (Dec 01 2020 at 22:54):

Is that iota reduction, or am I misremembering?

#### Reid Barton (Dec 01 2020 at 22:54):

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

#### Reid Barton (Dec 01 2020 at 22:56):

This stuff is easier with bundled objects I think

#### Reid Barton (Dec 01 2020 at 22:58):

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 (Dec 01 2020 at 22:59):

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 (Dec 01 2020 at 23:00):

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 (Dec 02 2020 at 09:36):

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 (Dec 02 2020 at 10:52):

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

#### Gabriel Ebner (Dec 02 2020 at 10:54):

That's because it's not definitionally equal.

Indeed

#### Gabriel Ebner (Dec 02 2020 at 11:01):

But you could add an instance like this:

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


#### Eric Wieser (Dec 02 2020 at 12:50):

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 (Dec 02 2020 at 12:51):

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

#### Eric Wieser (Dec 02 2020 at 14:09):

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

Last updated: May 17 2021 at 15:13 UTC