Stream: Is there code for X?

Topic: semiring+algebra => ring

Adam Topaz (Jul 24 2020 at 21:22):

This is related to @Eric Wieser 's comment on #3531

by apply_instance failed for this:

import ring_theory.algebra
import linear_algebra

variables {R : Type*} [comm_ring R] {A : Type*} [semiring A] [algebra R A]

example : ring A :=
{ neg := λ a, (algebra_map R _  \$ -1) * a,
begin
have : (algebra_map R _ 1) * a = a, by simp,
conv_lhs { congr, skip, rw ←this}, clear this,
change (algebra_map R _ (-1)) * a + _ = _,
rw [←right_distrib,← (algebra_map R A).map_add (-1) 1],
simp,
end,
..show semiring A, by apply_instance }


Does mathlib have this?

Reid Barton (Jul 24 2020 at 21:25):

This isn't suitable as an instance (R is undetermined), but I don't know whether it exists as a def

Eric Wieser (Sep 25 2020 at 09:21):

Done in #4252, name suggestions appreciated

Eric Wieser (Sep 27 2020 at 12:40):

Is it true that the resulting add_comm_group structure is independent of the choice of R? If so, can this be made a type class anyway?

Scott Morrison (Sep 27 2020 at 13:00):

Additive inverses are unique since (-x)+x+(~x) can be simplified either to -x or ~x, so it can't matter which coefficient ring you use to construct the additive inverses? I'd still be pretty wary of adding these as instances.

Eric Wieser (Sep 27 2020 at 13:07):

That's a nice and simple proof, thanks!

Eric Wieser (Sep 27 2020 at 13:39):

Although I can't think of a way to exploit it to make the R arg implicit

Reid Barton (Sep 27 2020 at 13:48):

There are really two reasons this should not be an instance

Reid Barton (Sep 27 2020 at 13:48):

First, it just won't work because there is no way for Lean to guess what R you have in mind

Reid Barton (Sep 27 2020 at 13:48):

But even if that wasn't a problem, most of the time there will be a better instance available already

Reid Barton (Sep 27 2020 at 13:51):

So since you almost never want to use this instance anyways, much easier if it's not an instance and it's just used explicitly where desired

Reid Barton (Sep 27 2020 at 13:51):

As a general principle, instances shouldn't be for variables like in ring A.

Eric Wieser (Sep 27 2020 at 16:51):

Not sure what you mean by your last message. Either way, I've run into trouble making this an instance even for specific instantiations, as in #4289

Scott Morrison (Sep 27 2020 at 23:35):

Reid's last message is saying that you should never have "general" instances S A that work for any A. Instances like this will fire every time someone wants an S A, and so contribute very heavily to typeclass search (particularly if people looking for R A might be sent looking for S A along the way).

Instead ideally instances are doing a sort of "structural recursion", e.g. they provide an instance of some S (B A) in terms of S A. When this is happening, you can be more confident typeclass search will be efficient, and you're also much less likely to get non-definitionally equal instances colliding with each other.

Scott Morrison (Sep 27 2020 at 23:36):

There's a linter warning about general instances that will always match, which suggests lowering the priority. Arguably it should suggest thinking very carefully about whether you really want this instance available in typeclass search, and if you're sure you do to only create it with low priority (so all the honest instances get to fire first).

Eric Wieser (Sep 28 2020 at 09:03):

Would you be able to comment on whether the instances in #4289 are a bad idea, and if so how best to handle them?

Oliver Nash (Sep 28 2020 at 09:34):

I believe the instances in #4289 are fine because the scalars are part of the type (thus avoiding the underdetermined parameter in typeclass search). I agree with your assessment that the problem is a diamond issue, and I want to understand it. I bet there is also a simpler way to get it to manifest.

Scott Morrison (Sep 28 2020 at 09:50):

Yes, this is just non-definitionally equal typeclasses instances. Typeclass search is working fine, you just don't like what you're getting!

Scott Morrison (Sep 28 2020 at 09:50):

I'm worried that the only fix is going to be to tweak the inductive construction to do something different for the free ring...

Eric Wieser (Sep 28 2020 at 09:54):

Interestingly the free_algebra typeclass seems to cause no problem, it's just the tensor_algebra one that does

Eric Wieser (Sep 28 2020 at 09:55):

(as an aside, the derive [algebra R] attribute on tensor_algebra creates an instance tensor_algebra.inst instead of tensor_algebra.algebra, which is minorly unhelpful when debugging)

Last updated: May 16 2021 at 05:21 UTC