semiring+algebra => ring

Stream: Is there code for X?

[Adam Topaz]

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,
  add_left_neg := λ 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]

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

[Eric Wieser]

Done in #4252, name suggestions appreciated

[Eric Wieser]

docs#semimodule.add_comm_monoid_to_add_comm_group, and docs#algebra.semiring_to_ring

[Eric Wieser]

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]

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]

That's a nice and simple proof, thanks!

[Eric Wieser]

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

[Reid Barton]

There are really two reasons this should not be an instance

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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]

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

[Eric Wieser]

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]

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]

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]

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]

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]

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]

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]

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

[Eric Wieser]

(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)