Default HSMul for !4#2212

Stream: mathlib4

[Arien Malec]

I think the solution for the instance failure in !4#2212 is to create a default HSMul instance along the lines of https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Heterogeneous.20scalar.20multiplication/near/320626039

Unfortunately, Subsemiringdoesn't currently have an HSMul instance -- what would be the right declaration to mirror (in RingTheory.Subsemiring.Basic)?

instance smul [SMul R' α] (S : Subsemiring R') : SMul S α :=
  S.toSubmonoid.smul

I've tried

@[default_instance]
instance hsmul [SMul R' α] (S: Subsemiring R') [SMul S α ] : HSMul α S S where
  hSMul := SMul.smul

but get:

failed to synthesize instance
  SMul α { x // x ∈ S }

[Arien Malec]

(It's possible I'm getting confused at which is the scalar here).

[Arien Malec]

We want (m • S).toSubsemiring = m • S.toSubsemiring to typecheck...

[Arien Malec]

And Lean isn't currently understanding that the smul on the rhs is just the ordinary smul on Subsemiring R that's already been defined.

[Eric Wieser]

Arien Malec said:

We want (m • S).toSubsemiring = m • S.toSubsemiring to typecheck...

This is a very different instance to the one you describe in the previous message.

[Arien Malec]

This one is the Pointwise smul in RingTheory.Subsemiring.Pointwise?

[Arien Malec]

If I do, behind Pointwise the similar:

instance hsmul [SMul M S] (S: Subsemiring R): HSMul M S S where
  hSMul := SMul.smul

I get...

failed to synthesize
  SMul M { x // x ∈ S }
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)

But again, I don't understand why Lean isn't seeing m • S.toSubsemiring as using the Pointwise smul instance...

[Arien Malec]

Huh, if I do:

theorem pointwise_smul_toSubsemiring (m : M) (S : Subring R) :
    (m • S).toSubsemiring = SMul.smul m (S.toSubsemiring : Subsemiring R) :=
  rfl

I get

failed to synthesize instance
  SMul M (Subsemiring R)

despite the open Pointwise previously in the file...

[Arien Malec]

which seems to be the root of the problem here?

[Eric Wieser]

I don't understand why you are writing

instance hsmul [SMul M S] (S: Subsemiring R): HSMul M S S where

(also this seems to have two different Ss?)

[Eric Wieser]

The instance we're looking for is

instance hsmul : HSMul M (Subsemiring R) (Subsemiring R) where

[Arien Malec]

Again, I think the root of the issue here is that Lean isn't finding the existing Pointwise instance of SMul.

[Arien Malec]

I was basing the declaration above on docs4#instHSMul but I cheerfully admit that I'm probably very confused...

[Arien Malec]

Your declaration works in the sense that it typechecks (:tada:) but doesn't work in the sense that we still can't find it in Subsemiring

[Arien Malec]

OK, so:

theorem pointwise_smul_toSubsemiring (m : M) (S : Subring R) :
    (m • S).toSubsemiring = Subsemiring.pointwiseMulAction.smul m S.toSubsemiring :=
  rfl

works just fine, which highlights that the issue here is that Lean can't find the instance of SMul for Subsemiring behind Pointwise

[Eric Wieser]

I would guess this is the structure eta in typeclas resolution problem

[Eric Wieser]

Can you make a mwe?

[Arien Malec]

Will work on it…

[Arien Malec]

The most trivial #mwe does what it says in the label...

import Mathlib.Tactic.scopedNS

class SMul (α : Type _) (β : Type _) where
  smul : α → β → β

class Monoid (M: Type _) where
  one : sorry

class MulAction  (α : Type _) (β : Type _) [Monoid α] extends SMul α β where
  /-- One is the neutral element for `•` -/
  protected one_smul : sorry

infixr:73 " • " => SMul.smul

structure Point (α : Type _) where
  mk :: (x : α) (y : α)

namespace Pointwise
end Pointwise

namespace Point
protected def pointwiseMulAction(α : Type _) [Monoid α] : MulAction α (Point α) where
  smul := sorry
  one_smul := sorry

scoped[Foo] attribute [instance] Point.pointwiseMulAction

end Point

structure PointX (α : Type _) where
  mk :: (x : α) (y : α)

namespace PointX
variable {α : Type _}
protected def pointwiseMulAction [Monoid α]: MulAction α (PointX α) where
  smul := sorry
  one_smul := sorry

scoped[Foo] attribute [instance] PointX.pointwiseMulAction

def toPoint {α : Type _} (self: PointX α): Point α:= sorry

open Foo

theorem pointX_smul_toPoint (a: α) [Monoid α] (p : PointX α) :
    (a • p).toPoint = a • p.toPoint := sorry

end PointX

Any pointers to the most effective way to complexify this to make it break would be appreciated...

[Eric Wieser]

Note that mathport is also having problems with subrings at the moment...