Rings as instances of non-unital, non-associative rings

Stream: maths

[Christopher Hoskin]

I can show that a ring is an instance of a non-unital non-associative ring, but this seems to mess up class inference elsewhere:

import algebra.ring.basic
import algebra.lie.of_associative

set_option old_structure_cmd true

lemma test1 (I :Type*) [ring I] (r s t : I) : ⁅r+s,t⁆ = ⁅r,t⁆ + ⁅s,t⁆ :=
begin
  rw add_lie,
end

/-- A not-necessarily-unital, not-necessarily-associative ring. -/
@[protect_proj, ancestor add_comm_group non_unital_non_assoc_semiring ]
class non_unital_non_assoc_ring (α : Type*) extends
  add_comm_group α, non_unital_non_assoc_semiring α

@[priority 100] -- see Note [lower instance priority]
instance ring.to_non_unital_non_assoc_semiring (B :Type*) [ring B] : non_unital_non_assoc_ring(B) := {
  add := (+),
  add_assoc := add_assoc,
  zero := (0),
  zero_add := zero_add,
  add_zero := add_zero,
  neg := λ a, -a,
  add_left_neg := add_left_neg,
  add_comm := add_comm,
  mul := (*),
  left_distrib := left_distrib,
  right_distrib := right_distrib,
  zero_mul := zero_mul,
  mul_zero :=mul_zero,
}

lemma test2 (I :Type*) [ring I] (r s t : I) : ⁅r+s,t⁆ = ⁅r,t⁆ + ⁅s,t⁆ :=
begin
  rw add_lie, -- rewrite tactic failed, did not find instance of the pattern in the target expression ⁅?m_6 + ?m_7,?m_8⁆
end

Lemma test1 works fine, but repeating the same result as test2 fails with "rewrite tactic failed, did not find instance of the pattern in the target expression ⁅?m_6 + ?m_7,?m_8⁆". Raising or lowing the priority of the instance doesn't seem to help.

I can convert the instance into a lemma, and everything is okay again. However, later I want to do:

class jordan (A : Type*) [non_unital_non_assoc_ring A] :=
...

--@[priority 100] -- see Note [lower instance priority]
instance  ring_jordan {B : Type*} [ring B] : jordan (B) :=
...

But then Lean will complain "failed to synthesize type class instance for B : Type ?, _inst_2 : ring B ⊢ non_unital_non_assoc_ring B" and I don't know how to manually tell Lean to use the ring.to_non_unital_non_assoc_semiring lemma.

Probably I am approaching this in the wrong way?

Thanks,

Christopher

[Christopher Hoskin]

(There's a branch with this code here: https://github.com/leanprover-community/mathlib/compare/jordan-algebras if it helps to see it in context.)

[Johan Commelin]

I think you are hitting an annoying diamond.

[Johan Commelin]

lemma test2 (I :Type*) [ring I] (r s t : I) : ⁅r+s,t⁆ = ⁅r,t⁆ + ⁅s,t⁆ :=
begin
  letI : lie_ring_module I I,
  { convert @lie_ring_self_module I _,
    -- look at the goal here
   },
  rw add_lie, -- rewrite tactic failed, did not find instance of the pattern in the target expression ⁅?m_6 + ?m_7,?m_8⁆
end

[Johan Commelin]

This works:

@[priority 100] -- see Note [lower instance priority]
instance ring.to_non_unital_non_assoc_semiring (B :Type*) [_i : ring B] :
  non_unital_non_assoc_ring B :=
{ zero_mul := zero_mul,
  mul_zero := mul_zero,
  .. _i }

lemma test2 (I :Type*) [ring I] (r s t : I) : ⁅r+s,t⁆ = ⁅r,t⁆ + ⁅s,t⁆ :=
begin
  rw add_lie, -- rewrite tactic failed, did not find instance of the pattern in the target expression ⁅?m_6 + ?m_7,?m_8⁆
end

[Christopher Hoskin]

Thanks very much!