Simp normal form: coe_norm_subgroup, submodule.norm_coe

Stream: general

[Anne Baanen]

docs#coe_norm_subgroup and docs#submodule.norm_coe are two simp lemmas pointing in opposite directions. Is there a reason for this discrepancy?

The reason I ask is that I'm defining subobject classes in the same style as morphism classes. The instance docs#add_subgroup.semi_normed_group can be easily generalized to add_subgroup_class, but that would lead to a cycle in the simp set since submodule is also an add_subgroup_class.

[Anne Baanen]

Outside of implicit use by simp or norm_cast, I see only one use for each (in a forward rw)

[Riccardo Brasca]

I think docs#submodule.norm_mk is perfectly fine: morally x=⟨x, hx⟩, so if simp throws hx away I don't see how one cannot be happy.

[Riccardo Brasca]

docs#coe_norm_subgroup is probably rarely used, we don't have x : ↥s very often

[Anne Baanen]

That was my impression too, without any real experience of this part of the library. I'll see what breaks if I turn coe_norm_subgroup the other way (in preparation for removing it entirely).

[Riccardo Brasca]

Sorry, for some reason my browser pointed at docs#submodule.norm_mk instead of docs#submodule.norm_coe so I misunderstood your question

[Eric Wieser]

∥x∥ = ∥↑x∥ seems like the better direction to me - most of the coe_* lemmas are about pushing coe to the innermost position

[Eric Wieser]

In this case it just so happens there is no outermost coe, but it still turns an operation on the subtype into an operation on the underlying type.

[Anne Baanen]

On the other hand, norm_cast wants coe_norm_subgroup to be reversed since it introduces a cast as-is.

[Eric Wieser]

Is there any documentation on the rules for annotating things with norm_cast or norm_cast move or ...?

[Anne Baanen]

The attribute docs for norm_cast explain it a bit.

[Anne Baanen]

As I understand it, the LHS generally should have more casts.

[Anne Baanen]

I created two branches, both seem to work fine on the basic files: branch#reverse-coe_norm_subgroup and branch#reverse-submodule_norm_coe

[Anne Baanen]

/poll ∥(↑x : E)∥ = ∥(x : s)∥ or ∥(x : s)∥ = ∥(↑x : E)∥
∥(↑x : E)∥ = ∥(x : s)∥ (branch#reverse-coe_norm_subgroup)
∥(x : s)∥ = ∥(↑x : E)∥ (branch#reverse-submodule_norm_coe)

[Kevin Buzzard]

It's just a fact that sometimes mathematicians want to push coercions in and sometimes pull them out, so it's difficult to know what "the right direction" is.

[Anne Baanen]

Since consensus points toward inserting the coercion: #11427