aliases

Stream: general

[Patrick Massot]

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]

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

[Heather Macbeth]

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

[Eric Wieser]

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

[Yaël Dillies]

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]

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]

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]

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

[Yaël Dillies]

Ah okay. And how is it done for coercions ?

[Eric Wieser]

docs#coe_coe reduces transitive coercions to direct ones

[Eric Wieser]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Eric Wieser]

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]

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

[Eric Wieser]

This is the proposal that came up before, right?

[Anne Baanen]

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

[Eric Wieser]

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]

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]

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

[Yaël Dillies]

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

[Anne Baanen]

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]

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

[Heather Macbeth]

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]

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

[Anne Baanen]

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]

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]

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]

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]

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]

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]

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]

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

[Yaël Dillies]

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]

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]

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]

Sooo... who will refactor?

[Patrick Massot]

Thanks for volunteering Yaël!

[Anne Baanen]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

Aah yes! Perhaps that's a key difference!

[Anne Baanen]

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]

Anne Baanen said:

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

Will do!

[Yaël Dillies]

Patrick Massot said:

Thanks for volunteering Yaël!

Coming back to this, I actually am, now!