Zulip Chat Archive

Stream: Is there code for X?

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


view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 01 2020 at 21:57):

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

view this post on Zulip Eric Wieser (Dec 01 2020 at 22:00):

Can you elaborate on that?

view this post on Zulip Kevin Buzzard (Dec 01 2020 at 22:02):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Dec 01 2020 at 22:43):

This surely can't be sustainable

view this post on Zulip Eric Wieser (Dec 01 2020 at 22:44):

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

view this post on Zulip Eric Wieser (Dec 01 2020 at 22:45):

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

view this post on Zulip Reid Barton (Dec 01 2020 at 22:47):

In principle it's every class

view this post on Zulip Reid Barton (Dec 01 2020 at 22:47):

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

view this post on Zulip Eric Wieser (Dec 01 2020 at 22:50):

Ah, I see your point

view this post on Zulip Reid Barton (Dec 01 2020 at 22:51):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Dec 01 2020 at 22:53):

Those two things are equal by rfl though?

view this post on Zulip Eric Wieser (Dec 01 2020 at 22:54):

Is that iota reduction, or am I misremembering?

view this post on Zulip Reid Barton (Dec 01 2020 at 22:54):

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

view this post on Zulip Reid Barton (Dec 01 2020 at 22:56):

This stuff is easier with bundled objects I think

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Gabriel Ebner (Dec 02 2020 at 10:54):

That's because it's not definitionally equal.

view this post on Zulip Eric Wieser (Dec 02 2020 at 11:00):

Indeed

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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