simp normal form for double casts

Stream: general

[Scott Morrison]

Can someone remind me what the preferred simp normal form should be in this example?

Say I have a s : subalgebra R A. Is ((s : subsemiring A) : set A) better, or (s : set A) directly?

(Currently mathlib seems to like the former in some places, and I'm wondering if it should be changed.)

[Scott Morrison]

Actually this is terrible. There's a diamond, because we can also do ((s : submodule R A) : set A).

[Scott Morrison]

ugh

[Scott Morrison]

And of course coe_coe unpacks the direct coercion...

[Johan Commelin]

I would think that the direct coercion is SNF

[Scott Morrison]

Except that coe_coe is marked as a simp lemma.

[Scott Morrison]

/-- Add an instance to "undo" coercion transitivity into a chain of coercions, because
   most simp lemmas are stated with respect to simple coercions and will not match when
   part of a chain. -/
@[simp] theorem coe_coe {α β γ} [has_coe α β] [has_coe_t β γ]
  (a : α) : (a : γ) = (a : β) := rfl

[Scott Morrison]

So I guess we're meant to cope with these diamonds... I seem to have done so in my local situation.

[Johan Commelin]

Yeah, I see why coe_coe should be simp

[Johan Commelin]

But I'm not sure what the principled approach to dealing with these diamonds is

[Eric Wieser]

I'm adding a direct coercion from subalgebra to set in #6768

[Eric Wieser]

Which is consistent with how all the other subobjects work

[Scott Morrison]

Ah, cool, thanks!

[Eric Wieser]

We deal with diamonds in the same way with bundled homs

[Eric Wieser]

Split to #6800, that PR grew too much