Zulip Chat Archive

Stream: general

Topic: aliases


Patrick Massot (Aug 16 2021 at 08:29):

Do we have a policy about lemma restating? In recent PRs we have both:

protected lemma lipschitz : lipschitz_with 1 e := e.isometry.lipschitz

protected lemma antilipschitz : antilipschitz_with 1 e := e.isometry.antilipschitz

@[simp] lemma ediam_image (s : set P) : emetric.diam (e '' s) = emetric.diam s :=
e.isometry.ediam_image s

@[simp] lemma diam_image (s : set P) : metric.diam (e '' s) = metric.diam s :=
e.isometry.diam_image s

@[simp] lemma comp_continuous_on_iff {f : α  P} {s : set α} :
  continuous_on (e  f) s  continuous_on f s :=
e.isometry.comp_continuous_on_iff

@[simp] lemma comp_continuous_iff {f : α  P} :
  continuous (e  f)  continuous f :=
e.isometry.comp_continuous_iff

in @Heather Macbeth #8660 and the whole #8693 by @Yaël Dillies

Patrick Massot (Aug 16 2021 at 08:29):

I don't have an opinion here. I'm frequently tempted to participate in this inflation but I'm always hesitant.

Heather Macbeth (Aug 16 2021 at 08:30):

I copied this from similar lemmas for linear_isometries, eg docs#linear_isometry.lipschitz

Eric Wieser (Aug 16 2021 at 08:32):

I think we do this routinely when structures and dot notation are involved

Yaël Dillies (Aug 16 2021 at 08:32):

The continuous lemmas were already duplicated (from when does git blame say?). I would be fine with not duplicating them but yeah the dot notation needed becomes quite unwieldy.

Eric Wieser (Aug 16 2021 at 08:34):

In particular, isn't e.isometry.diam_image a statement about ⇑e.isometry not ⇑e, meaning the lemmas aren't duplicates syntactically.

Yaël Dillies (Aug 16 2021 at 08:34):

Going on a tangent, could a extends b not only declare a.to_b, but also a.to_c when b extends c`?

Eric Wieser (Aug 16 2021 at 08:34):

That's a bad idea Yaël because you now need lemmas about every transitive conversion not just every direct conversion

Yaël Dillies (Aug 16 2021 at 08:35):

Ah okay. And how is it done for coercions ?

Eric Wieser (Aug 16 2021 at 08:36):

docs#coe_coe reduces transitive coercions to direct ones

Eric Wieser (Aug 16 2021 at 08:36):

In fact with new style structures lean will take a.to_c as syntax for a.to_b.to_c anyway.

Patrick Massot (Aug 16 2021 at 08:38):

I'm also asking in the context of https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/dot.20notation.20deficiency/near/249471794

Patrick Massot (Aug 16 2021 at 08:39):

which shows that some duplication is probably unavoidable to keep things under control.

Eric Wieser (Aug 16 2021 at 08:45):

I think the problem is less about keeping verbosity under control, and more about how our use of coercions in structures means that lemmas about a base structure are never a syntactic match for the derived structure; for instance, add_monoid_hom.map_add is a lemma about add_monoid_hom.coe_to_fun, linear_map.map_add is a lemma about linear_map.coe_to_fun, etc. If you use lm.to_add_monoid_hom.map_add instead of lm.map_add you get a proof about ⇑lm.to_add_monoid_hom (x + y) instead of ⇑lm (x + y). They're all defeq as proofs, but that's not enough for rw or simp.

Anne Baanen (Aug 16 2021 at 08:45):

I have a proposal for (part of a) solution: typeclasses!

Eric Wieser (Aug 16 2021 at 08:46):

This is the proposal that came up before, right?

Anne Baanen (Aug 16 2021 at 08:47):

Yes, I've been working on it a bit in the past months.

Eric Wieser (Aug 16 2021 at 08:47):

My memory of it is that https://github.com/leanprover-community/lean/pull/557 would probably not only make it easier, but would also make it more compatible with lean4

Anne Baanen (Aug 16 2021 at 08:49):

So the idea is that all types that extend e.g. mul_hom would have a mul_hom_class instance. Then map_mul can be a simp lemma assuming mul_hom_class. For example, see this section

Anne Baanen (Aug 16 2021 at 08:53):

Presumably this pattern can be generalized to a lipschitz_with proof for all types extending isometry.

Yaël Dillies (Aug 16 2021 at 08:54):

This fails if we don't get the common ground for a lemma as a typeclass.

Anne Baanen (Aug 16 2021 at 08:54):

Eric Wieser said:

My memory of it is that https://github.com/leanprover-community/lean/pull/557 would probably not only make it easier, but would also make it more compatible with lean4

Indeed, these lines are essentially the same backport.

Yaël Dillies (Aug 16 2021 at 08:55):

Eg, are there several ways to get a map_mul-like lemma?

Heather Macbeth (Aug 16 2021 at 08:55):

Anne Baanen said:

Presumably this pattern can be generalized to a lipschitz_with proof for all types extending linear_isometry.

docs#isometry, not docs#linear_isometry, not that it affects your point.

Yaël Dillies (Aug 16 2021 at 08:56):

If we replaced some words by others, this discussion starts very much looking like the order refactor

Anne Baanen (Aug 16 2021 at 08:57):

Yaël Dillies said:

Eg, are there several ways to get a map_mul-like lemma?

Definitely! There are many _homs that have map_mul: monoid_hom, monoid_with_zero_hom, ring_hom, ... Each of those can have a mul_hom_class instance (via monoid_hom_class.to_mul_hom_class in most cases I assume)

Anne Baanen (Aug 16 2021 at 09:00):

Yaël Dillies said:

If we replaced some words by others, this discussion starts very much looking like the order refactor

I claim this is not really a coincidence, since typeclasses provide a nice way to denote the set of all types with an operation (coe_fn, le) that satisfies some properties (map_mul, mul_le_mul).

Anne Baanen (Aug 16 2021 at 09:02):

By allowing typeclass search in simp we basically get automation for the positive fragment of proposition logic for specific propositions (namely those tagged @[class]), along with the automation for equality that simp provides.

Eric Wieser (Aug 16 2021 at 09:04):

Heather Macbeth said:

docs#isometry, not docs#linear_isometry, not that it affects your point.

Ah, this invalidates some of my messages above; I assumed that isometry was bundled and defined as roughly {f // isometry f}

Heather Macbeth (Aug 16 2021 at 09:06):

There is docs#isometric which is exactly this, and we have (or will have) linear_isometry.to_isometric, affine_isometry.to_isometric. So if it's more convenient the proof can go f.to_isometric.lipschitz.

Heather Macbeth (Aug 16 2021 at 09:08):

Heather Macbeth said:

There is docs#isometric which is exactly this,

Actually I guess that's not true, since docs#isometric requires it be an equivalence, not just a map. It's linear_isometry_equiv.to_isometric, not linear_isometry.to_isometric.

Eric Wieser (Aug 16 2021 at 09:09):

Using an adjective like isometric for the name of a structure in Type seems weird to me (especially since we call the linear version an *_isometry_*)

Yaël Dillies (Aug 16 2021 at 09:11):

Yeah, I would have expected isometric to be the Prop one

Yaël Dillies (Aug 16 2021 at 09:15):

So we can reuse the insight we gained from the order refactor! That is, have typeclasses "per lemma" and then the meaningful typeclasses each extending some of them.

Eric Wieser (Aug 16 2021 at 09:17):

I'm a little pessimistic we'll learn the opposite of what we learnt there; that the approach doesn't scale, and we got away with it because ordered monoids are used way less often than bundled maps. It would still be good to proceed; either we learn that the appoach isn't as good as we think it is, or the problem goes away.

Anne Baanen (Aug 16 2021 at 09:20):

I expect the opposite might turn out to be the case: we have an enormous pile of simp lemmas with head symbol coe_fn, so removing some of them from the simp set and using typeclasses instead, which have more recognizable head symbols, will scale better in number of _homs × number of map_s.

Yaël Dillies (Aug 16 2021 at 09:29):

Sooo... who will refactor?

Patrick Massot (Aug 16 2021 at 09:29):

Thanks for volunteering Yaël!

Anne Baanen (Aug 16 2021 at 10:16):

I'm slowly working on branch#fun_like. Feel free to fix the build errors :)

Kevin Buzzard (Aug 16 2021 at 10:39):

So the idea is that we used to deal with group homs as a typeclass predicate on bare functions, and then we switched to bundled homs, and now we're trying bundled homs together with a typeclass predicate on the bundled hom?

Anne Baanen (Aug 16 2021 at 10:52):

The predicate goes on the type of the bundled hom, not the hom itself

Kevin Buzzard (Aug 16 2021 at 11:04):

Aah yes! Perhaps that's a key difference!

Anne Baanen (Aug 16 2021 at 11:05):

Indeed, this should avoid all the defeq "abuse" that made the old typeclass predicates hard to work with. They aren't called type classes for nothing :)

Yaël Dillies (Aug 16 2021 at 11:23):

Anne Baanen said:

I'm slowly working on branch#fun_like. Feel free to fix the build errors :)

Will do!

Yaël Dillies (Feb 13 2022 at 19:52):

Patrick Massot said:

Thanks for volunteering Yaël!

Coming back to this, I actually am, now!


Last updated: Dec 20 2023 at 11:08 UTC