Zulip Chat Archive

Stream: general

Topic: Simp normal form: coe_norm_subgroup, submodule.norm_coe

Anne Baanen (Jan 13 2022 at 10:45):

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 (Jan 13 2022 at 10:50):

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

Riccardo Brasca (Jan 13 2022 at 10:51):

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 (Jan 13 2022 at 10:52):

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

Anne Baanen (Jan 13 2022 at 10:53):

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 (Jan 13 2022 at 10:53):

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 (Jan 13 2022 at 11:09):

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

Eric Wieser (Jan 13 2022 at 11:10):

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 (Jan 13 2022 at 11:25):

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

Eric Wieser (Jan 13 2022 at 11:29):

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

Anne Baanen (Jan 13 2022 at 11:31):

The attribute docs for norm_cast explain it a bit.

Anne Baanen (Jan 13 2022 at 11:32):

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

Anne Baanen (Jan 13 2022 at 11:57):

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 (Jan 13 2022 at 12:04):

/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 (Jan 13 2022 at 12:25):

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 (Jan 13 2022 at 14:49):

Since consensus points toward inserting the coercion: #11427

Last updated: Aug 03 2023 at 10:10 UTC