Uglified proof

Stream: maths

[Patrick Massot]

@Yury G. Kudryashov Could please stop doing things like https://github.com/leanprover-community/mathlib/pull/18111/files#diff-5603eadded9b71047a01d203093c3a2b759582dad4f7d86ac16072c1c43bd094L186-R166? Why do you want mathlib to be ugly? This is a proof I'm showing in every propaganda talk I give. My proof was

calc
map (prod.map f f) (𝓤 α) = map (prod.map f f) (⨆ x, 𝓝 (x, x))  : by rw compact_space_uniformity
                     ... =  ⨆ x, map (prod.map f f) (𝓝 (x, x)) : by rw filter.map_supr
                     ... ≤ ⨆ x, 𝓝 (f x, f x)     : supr_mono (λ x, (h.prod_map h).continuous_at)
                     ... ≤ ⨆ y, 𝓝 (y, y)         : supr_comp_le (λ y, 𝓝 (y, y)) f
                     ... ≤ 𝓤 β                   : supr_nhds_le_uniformity

and you replace it by

have tendsto (prod.map f f) (𝓝ˢ (diagonal α)) (𝓝ˢ (diagonal β)),
  from (h.prod_map h).tendsto_nhds_set maps_to_prod_map_diagonal,
(this.mono_left nhds_set_diagonal_eq_uniformity.ge).mono_right nhds_set_diagonal_le_uniformity

Why are you doing this? Now your version has been ported to Lean4 as well so both versions need to be fixed.

[Yury G. Kudryashov]

I'll try to stop doing it.

[Patrick Massot]

Thanks.

[Yury G. Kudryashov]

If there are some important proofs that are included in propaganda talks, could you please mark them with something like -- don't uglify this proof?

[Yury G. Kudryashov]

Usually, I do it because I slightly break a proof, then it's easier for me to rewrite a proof than to read and understand the original proof.

[Yury G. Kudryashov]

(BTW, I think that using nhds_set here is not a bad thing)

[Patrick Massot]

I don't think there is any reason to uglify a proof. This should not require any marking.

[Patrick Massot]

Eric, I don't understand your thumb up reaction. Why should we be marking anything as "don't uglify"? Why do you want anything ugly in mathlib? I think we really developed a very toxic golfing culture here.

[Patrick Massot]

I opened !4#3954 with a fix.

[Mario Carneiro]

In metamath, there is a marker "(Proof modification is discouraged.)" which is placed on theorems where the proof itself is the point of the demonstration. This is a minority thing, and it does deserve a marking

[Mario Carneiro]

If you want something not to change you have to explicitly say so, because mathlib is aggressively refactored and people can't just know that this particular proof shows up in some lecture notes if you don't tell them

[Mario Carneiro]

It's not just about golfing. As Yury said, sometimes it is a casualty of refactoring, since the proof might need to be rewritten to accommodate a change and the person doing the rewriting might not have the same eye for beauty as you

[Patrick Massot]

I don't think we need refactors uglifying proofs.

[Mario Carneiro]

I think that it is not reasonable to ask everyone to write proofs which are as pretty as yours at all times

[Mario Carneiro]

You have to assume that the new proof is not being written with the old one as a guide

[Yury G. Kudryashov]

Then we should have some (semi-)formal guidelines on "golf or not".

[Mario Carneiro]

Unless you can define prettyness such that a linter can check it this is tilting at windmills

[Mario Carneiro]

or at least a relatively strict style guide requirement

[Yury G. Kudryashov]

A guideline may say, e.g., "a golfing PR can't be merged without consent of the author of the original proof if this author is still active".

[Mario Carneiro]

I don't like that rule, as it means that authorship allows exerting control on a proof-by-proof basis

[Mario Carneiro]

I think it would be detrimental to refactors of all kinds, since you will have to hunt down who knows how many authors to make sure everything is okay with them

[Yury G. Kudryashov]

Can we make github auto mention people who previously modified these lines?

[Mario Carneiro]

If the proof is "this is a demonstration of the calc tactic" then clearly we want to preserve that it is proved by calc. Most proofs are "this thing is true" and so that's what we preserve

[Patrick Massot]

I don't understand why anyone would need help from a guide or the original author to understand that this modification strictly deteriorated mathlib.

[Mario Carneiro]

modification does not strictly deteriorate mathlib!

[Mario Carneiro]

maybe this one does, to you, but modifications in general clearly do not

[Yury G. Kudryashov]

@Patrick Massot If I understood this without a guide (in this and some similar situations), then I would've not dot these PRs.

[Patrick Massot]

Sorry, I missed a word

[Mario Carneiro]

and we need to have a more objective criterion to generalize this

[Heather Macbeth]

For what it's worth, I have a variety of strong style opinions of my own, and I don't see this example as clear-cut.

[Heather Macbeth]

(Though I think I could be convinced)

[Yury G. Kudryashov]

/me is away: the kid woke up in the middle of the night
P.S.: I don't think that my proof is better, more like "don't care about the difference".

[Eric Wieser]

The marking wouldn't be "don't uglify" but "this proof is used as an example in @user's [some course/talk/paper], please try to preserve its structure"

[Eric Wieser]

Sometimes a refactor trivializes a proof such that a 5 line "pretty" calc proof becomes a special case of one or two other lemmas; while I'd argue deleting the calc proof is the right thing to do in general, I think most people would be ok leaving it if there were a comment specifically requesting it.

[Eric Wieser]

Patrick Massot said:

I don't think we need refactors uglifying proofs.

A refactor that unblocks new mathematics but uglifies a handful of proofs is probably better than no refactor at all.

[Yaël Dillies]

I agree with everyone here. Wanting to preserve the state of a specific lemma without letting anyone know within the source code is a lost cause, no matter how goodwilled the contributors are.

[Johan Commelin]

I think this was a very nice calc proof, and I understand Patrick is sad to see it is gone.

[Johan Commelin]

Eric Wieser said:

The marking wouldn't be "don't uglify" but "this proof is used as an example in @user's [some course/talk/paper], please try to preserve its structure"

I think this is a good idea. Having a few such comments in mathlib can only be helpful.
Because I also understand that in the "heat of the moment" trying to finish a refactor, preserving the structure of some proof is not the first thing on your mind.

[Anatole Dedecker]

I think the underlying question is really about calc block proofs. I don't think Patrick has any problem about replacing ⨆ x, 𝓝 (x, x) with 𝓝ˢ (diagonal α) (and I'd say this is definitely a good thing), the only issue that I see with the new proof is that it explicitly uses transitivity(-like) lemmas (tendsto.mono_[left, right]), so it clearly falls into the set of proofs that are more readable in calc-form. So maybe the good rule of thumb would be that if a proof is nontrivial and uses transitivity at least twice (in the same computation), then it should use a calc block.

[Anatole Dedecker]

Note that this is orthogonal to the question of adding tags to proof that are examples in a talk/article, I can imagine changes that preserve readability but break the structure of the proof to the extent that it's not a good example anymore.

[Eric Wieser]

Is it even possible to write calc proofs about tendsto without unfolding tendsto?

[Eric Wieser]

Or is the answer "you're supposed to unfold tendsto to prove things about it"?

[Anatole Dedecker]

No you can’t indeed. I’d argue that when you’re really playing with filter inequalities anyway it looks better if everything is written as filter inequalities, but that’s debatable.

[Pedro Sánchez Terraf]

I like it very much that this is discussed.

Patrick Massot said:

Why do you want anything ugly in mathlib? I think we really developed a very toxic golfing culture here.

I completely agree, especially with the last sentence. Actually, I believe that this toxicity is completely involuntary, triggered by reasons already exposed and for the will of obtaining the neatest (most elegant??) term. Whenever possible, I try to code as closely as it can get to blackboard math.

[Pedro Sánchez Terraf]

Anatole Dedecker said:

I think the underlying question is really about calc block proofs. I don't think Patrick has any problem about replacing ⨆ x, 𝓝 (x, x) with 𝓝ˢ (diagonal α) (and I'd say this is definitely a good thing)

I'd also say that this is a good thing, but I'd save the definitely: The pen and paper math (or, better, classroom math) I know usually tends to make binding variables explicit, favoring $\bigcup_x I(x)$ over something like $\bigcup \mathrm{range}(I)$.

[Pedro Sánchez Terraf]

To finish this rant, I think Patrick and many others are doing a great job writing expository proofs in Mathematics in Lean, TPIL, and similar works. My utopistic dream would be that I could find the same coding style in a randomly chosen piece of mathlib.

[Patrick Massot]

Anatole Dedecker said:

I think the underlying question is really about calc block proofs. I don't think Patrick has any problem about replacing ⨆ x, 𝓝 (x, x) with 𝓝ˢ (diagonal α) (and I'd say this is definitely a good thing), the only issue that I see with the new proof is that it explicitly uses transitivity(-like) lemmas (tendsto.mono_[left, right]), so it clearly falls into the set of proofs that are more readable in calc-form. So maybe the good rule of thumb would be that if a proof is nontrivial and uses transitivity at least twice (in the same computation), then it should use a calc block.

Sure, I have nothing against 𝓝ˢ, it simply didn't exist when this proof was first written. And indeed in my PR this morning used it. I restored the calc proof without changing the proof term at all. The question was simply: should this proof be readable, knowing that making it readable adds exactly one line and this is an important named theorem?

[Eric Wieser]

Patrick, what are your thoughts on the fact that your calc proof is relying on the defeq of tendsto (in the context of my comments above); should we make docs4#Filter.Tendsto reducible in order to mark this type of thing as ok encouraged?

[Yury G. Kudryashov]

You can write calc proofs about tendsto without unfolding the definition if

• you introduce a (local) infix notation for tendsto. Something like l →[f] l' for tendsto f l l'
• you add @[trans] attributes (Lean 3) or Trans instances (Lean 4).

[Yury G. Kudryashov]

The downside of this approach is that an infix notation with f in the middle is not intuitive.

[Yury G. Kudryashov]

OTOH, calc with filter.map f _ is not very intuitive as well.

[Yury G. Kudryashov]

@Eric Wieser We unfold the definition of Tendsto without rw/dsimp in many places.

[Yury G. Kudryashov]

But I suggest not to change it to reducible in the middle of porting.

[Patrick Massot]

Indeed let is not change this for now.

[Heather Macbeth]

Anatole Dedecker said:

maybe the good rule of thumb would be that if a proof is nontrivial and uses transitivity at least twice (in the same computation), then it should use a calc block.

I am very much in favour of this rule of Anatole's. The only part I am unsure about is whether the rule should be applied here (because of the question discussed above: whether the rule applies when you need to unfold definitions to see the preconditions of the rule)

[Heather Macbeth]

... but there are definitely many proofs in the library with no unfolding issue and repeated (...).trans, that's bad style!

[Eric Wieser]

My experience with transitivity proofs (at least in algebra) is that it's not actually very common to be able to assemble them into a nice calc proof; as soon as you have something like mul_le_mul _ _ you're forced out of the calc block and back into term mode

[Heather Macbeth]

True, but @Mario Carneiro and I should have something to help with this within the next few days ... :P

[Kevin Buzzard]

Looking forward to calc++!

[Yury G. Kudryashov]

@Patrick Massot What do you think about an infix notation for tendsto? Probably, not an arrow but something like Haskell-style l₁ `tendsto f` l₂? This way we can hide map _ in tendsto+calc proofs.

[Yury G. Kudryashov]

And a similar question about docs4#Set.MapsTo.

[Kevin Buzzard]

I would love to see "arrow-like" notation for filter.tendsto. When I first understood the notion I did a half-hearted literature search to see if I could find anything, but I didn't come up with anything; the concept is not particularly well-represented in the literature even though it's now got to the point where it feels totally natural to me.

[Yury G. Kudryashov]

In papers we write $f(x)\to b$ as $x\to a$ or $\lim_{x\to a}f(x)$. In both cases arrows are near the filters, not the function.

[Patrick Massot]

I don't understand why you want to hide map in those calc proof. For me the only advantage of tendsto is that it allows dot notation.

[Jireh Loreaux]

Arguably map is the thing to be preferred given the interpretation of filters as generalized sets.

[Yury G. Kudryashov]

My only reason is that tendsto (in the form of $\lim_{x\to a}f(x)=b$) is something I see in every paper on analysis and filter.map forces a user to think about the actual definition of filter.tendsto in terms of filters.

[Mario Carneiro]

Also using filters means I have to remember what direction the inequality goes and where the map goes, while tendsto makes it obvious. For formalization I would say it has dubious usefulness as a proof shortener, but it seems to have comparatively strong explanatory power

[Mario Carneiro]

especially map filters, you don't see those in the literature when you are using this kind of $\lim_{x\to a}$ notation

[Jake Levinson]

Yury G. Kudryashov said:

Then we should have some (semi-)formal guidelines on "golf or not".

The discussion has moved in the direction of "calc vs non-calc", but I for one would like to see a continuation of this point. I understand certain benefits of golfing -- #1 compilation speed, #2 legibility, #3 suppressing trivial/rote proofs -- but not others.

In particular some golfing seems focused on saving keystrokes or reducing the number of lines of code or commands, and those don't seem valuable to me. If a more human-readable proof compiles just as fast, I'd argue that's actually better than a "golfed" proof that is shorter but harder for anyone but the author to understand (and therefore harder to modify if needed).

[Jake Levinson]

I should say too, of course golfing can make proofs nicer and more elegant too, not just shorter or faster, and that's certainly desirable.

[Jireh Loreaux]

Mario, it's (I think) immediately obvious when you think of a filter as a generalized set. To be clear, I'm not saying we should get rid of tendsto. I'll have another brief comment on this later when I'm not on mobile.

[Mario Carneiro]

I think I could more likely than not guess the correct order, but knowing that it is flipped only makes things worse

[Heather Macbeth]

I think to understand when golfing is good, we need a different metric than "number of characters". For me, one part of the metric is "number of lemmas mentioned by name". The proof ring is better than the proof rw [add_comm] not because it's shorter but because it's more conceptual.

[Jireh Loreaux]

Just don't think of the order in terms of the definition. Think of it only in terms of the interpretation as generalized sets.

[Mario Carneiro]

(I wrote a large part of the initial theory of topological spaces back in the early days, so I should know, and I genuinely appreciated the neat algebraic proofs it produces, but there are a lot of parity issues that I would have to look back at the definition to recall)

[Mario Carneiro]

not just le but also map and comap, which one is using preimages and which one uses images

[Jake Levinson]

Heather, is ring slower than rw [add_comm]? That's a decent example of where I might write ring when developing the proof and then golf it to rw [add_comm, ...] later, and I agree the latter is uglier and less clear, but I had always figured it was faster to compile.

[Heather Macbeth]

I hope that with Lean 4 we don't need to care about this. I want a world in which rw [add_comm] is never used when ring is available.

[Mario Carneiro]

TBH I don't find rw [add_comm] less clear than ring plus a rather involved type ascription

[Mario Carneiro]

rw is a non-finishing tactic, which gives it certain advantages over ring which requires the proof around it to adjust to put it in terminal position

[Heather Macbeth]

Totally agree, I'm not a fan of the rw [(by ring : x + 3 * (z + x) = 4 * x + 3 * z)] one sometimes sees, but that's a separate discussion ...

[Mario Carneiro]

(to be clear, calc is also a rather involved type ascription as far as I am concerned)

[Jake Levinson]

Interesting, I have used that rw [(by ring : ...)] form many times, I don't know how else to arrange something in a desired form in a non-terminal step.

[Jake Levinson]

I think there will always be grey areas and differences of opinion on what is nicest (not to mention how much to emphasize niceness over efficiency). Still, I like the idea of trying to formulate some guiding vision for mathlib.

[Jake Levinson]

Another thought I've had is: could there be a nice way to record two proofs of the same proposition in mathlib -- one possibly very slow and inefficient, but easy to read; and a second one that is allowed to be golfed into oblivion? (For example a proof with a very slow terminal simp or reflthat can be extended into an efficient but hard to read simp only [very long list], or even just a storage of the generated proof term).

[Heather Macbeth]

My preferred style is something like, lots of clean-up steps upfront, then all the algebra at the end in a single ring, polyrith, linarith or similar. Of course that's not always possible! But often a proof with several ring can become a proof with one terminal ring/polyrith/linarith if you rearrange it carefully.

[Heather Macbeth]

My other preferred style is whatever calc you would naturally write on paper ... this requires less in the way of mental gymnastics to Lean-ify. And regarding this, may I advertise
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/New.20tactic.20for.20.22relational.20congruence.22
? :wink:

[Mario Carneiro]

I would also like to be able to support multiple proofs of the same statement. The main drawback is that people will want to make sure both proofs compile in the face of refactors etc, which means that you would basically just be making mathlib slower, and this excludes really slow proof strategies.

[Mario Carneiro]

I'm not really sure that lean proofs are the appropriate level to target when you are trying to construct a good demonstration, though. We should be using dedicated tools for that, like Patrick's informalizer display

[Mario Carneiro]

IMO mathlib should be optimized for reasonable compile time and easy refactorability as primary goals, and readability is only a tertiary goal (mainly as it affects maintainability and refactorability).

[Mario Carneiro]

It should of course be usable as a library though, meaning that it should be copiously documented at the top level

[Eric Wieser]

Heather Macbeth said:

The proof ring is better than the proof rw [add_comm] not because it's shorter but because it's more conceptual.

The problem with this approach is that I can no longer change the theorem from assuming comm_ring R to assuming ring R or add_comm_group R without changing back to the rw proof. So using ring in proofs makes generalization refactors harder.

[Yaël Dillies]

... especially because it's not just a matter of turning the ring back into a rw, since Alex J. Best now has tools that detect whether some typeclasses can be weakened, and ring might trick them into thinking they can't.

[Patrick Massot]

Mario Carneiro said:

I'm not really sure that lean proofs are the appropriate level to target when you are trying to construct a good demonstration, though. We should be using dedicated tools for that, like Patrick's informalizer display

My hope is indeed that the output of that informalizer will be the readability target eventually. A proof that doesn't look good once informalized should be considered as bad. We are still far from ready to run this on mathlib unfortunately. I am very busy with administration and teaching as usual and lots of people, very often myself, keep distracting Kyle by asking for meta-programming help.