subtype simp normal form

Stream: general

[Floris van Doorn]

Is there a reason that when x is an element of a subtype, neither x.1 nor ↑x is in simp-normal-form?

example {α} {P : α → Prop} {x : subtype P} : x.1 = (x : α) :=
by { simp } -- fails

[Johan Commelin]

Clearly, we need to fix things here. The .ext lemma etc are not following standard conventions either.

[Floris van Doorn]

Which one would we want to be simp-normal form? The coe?

[Kevin Buzzard]

This has bitten me before too. There is no subtype.ext_iff, and the ext tactic does not work for subtypes

[Patrick Massot]

I think having the coe as simp normal form would be more consistent with our other choices.

[Reid Barton]

Yes, at one point I tried adding the ext lemma for subtype to @[ext], and it broke some things which were all avoided by phrasing it in terms of the coercion.

[Reid Barton]

(I'm still not sure whether it is actually a good idea to add it though.)

[Johan Commelin]

Why not?

[Reid Barton]

It can be too aggressive with things like nnreal (I don't remember whether this is an actual example, but it might be) defined directly as subtype where there currently is no ext lemma and outside the nnreal file itself you probably don't actually want to prove equalities of nnreal by proving equalities of the underlying value. (Okay maybe this isn't a great example, because real >> nnreal, but imagine you also want to use some hypotheses which are in nnreal language.)

[Reid Barton]

On the other hand I think it actually didn't break anything in mathlib at all, so maybe this isn't a real concern.
And if it is, one could argue that nnreal should use a custom structure type anyways and not be a def around subtype.

[Yury G. Kudryashov]

Does ext unfold definitions?

[Scott Morrison]

It does, although since it is using apply under the hood we _could_ turn this off.

[Scott Morrison]

(This would surely break a lot.)

[Reid Barton]

It seems unafraid to apply lemmas even if it would need semireducible transparency to do so, yes

[Scott Morrison]

Maybe we want ext and ext! (with the current behaviour)?

[Reid Barton]

Probably the things it would be break could be fixed by adding more ext lemmas, right?

[Yury G. Kudryashov]

I thought that ext stores lemmas sorted by head type name in order to apply only a small set of lemmas.

[Yury G. Kudryashov]

But it applies option ext lemma to ennreal.

[Yury G. Kudryashov]

So I have to use ext1 in measure_theory.

[Yury G. Kudryashov]

I think that applying only lemmas with the desired head symbol is the "least surprise" approach.

[Reid Barton]

I rely on the current behavior pretty heavily in lean-homotopy-theory to check whether two morphisms X \hom Y in Top are equal by function extensionality, and various other things like this, but I think I could add lemmas for these if ext refused to apply funext here.

[Reid Barton]

actually that might be a bad example, since that needs a separate extensionality lemma anyways.

[Reid Barton]

The other examples are things like checking equality of x y : Top.prod A B where A B : Top using ext for prod.

[Yury G. Kudryashov]

You can always use attribute [ext newtype] oldlemma.

[Reid Barton]

Here Top.prod A B is something whose underlying type will unfold to prod of the underlying types of A and B

[Yury G. Kudryashov]

Probably we should make an exception for the case "head symbol is coe_sort".

[Floris van Doorn]

Yes, I've also noticed that ext for option is applied to ennreal. It's not really a problem if you use ext1 instead.
(also, I regularly want to prove two nnreals equal and am sad that ext doesn't work).
I will try to do some low level changes to subtype.

[Floris van Doorn]

Ok, I'm working on it now: https://github.com/leanprover-community/mathlib/tree/subtype

I'm adding @[ext] for subtype and simplify x.val to ↑x. There is a lot of damage, but so far most of it is fixed just by

• using the coercion more, instead of subtype.val
• using ext1 if ext is too aggressive.
• There are a couple of places where I have to add -subtype.val_eq_coe as argument to simp. This happens when a new type is defined as a subtype, so the coercion doesn't fire anymore, and subtype.val is still used to get the first component.

Please voice any concerns of this change ASAP.

[Floris van Doorn]

A version of ext that doesn't unfold definitions (and making that the default version?) sounds useful as well!

[Johan Commelin]

So far, this sounds good to me! Thanks for battling through this