Proof stability and maintenance

Stream: general

[Damiano Testa]

While discussing the "flexible tactic" linter, the broader question of "what constitutes solid, maintainable code" arose. This would be a precursor to then implementing these changes (e.g. via style-guides, linters and code-review).

The typical example of a maintenance burden is simp in the middle of a proof.

What other stability/maintenance concerns do you have/want to discuss?

[David Loeffler]

I think there's a conversation to be had about the proper use of variable – some library files are prone to reusing type variables while repeatedly changing the instance assumptions on them, making it very hard to find what's being assumed at a given point.

Maybe we could make it a rule (enforced by a linter) that variable is only permitted at the start of a section (or other scoping construct e.g. namespace)?

[Sébastien Gouëzel]

#where tells you the current assumptions in scope.

[Kim Morrison]

I'd be in favor of reducing "non-locality" in uses of variables!

[Patrick Massot]

I agree that the situation described by David is problematic.

[Mario Carneiro]

Aren't variables mid-section isomorphic to just putting more sections? What does it buy exactly?

[Vincent Beffara]

Is there an official guideline saying that variables can be data or instance declarations but not assumptions? It is desirable that copy-pasting a declaration either works or fails with an error, but an assumption in a variable can make the copied declaration valid but with a different meaning.

[Patrick Massot]

Mario, it buys that variables are easier to find. But I think the main thing should be to use different names for the types that have different type classes.

[Mario Carneiro]

No, we have never made that recommendation explicitly, but maybe we should. This example was particularly compelling to me as a mistake caused by misreading a variable

[Mario Carneiro]

there's a big difference between PNT and ChebyshevBound -> PNT!

[Vincent Beffara]

Yes, that's exactly the example I had in mind

[Mario Carneiro]

Patrick Massot said:

Mario, it buys that variables are easier to find.

Is the idea here that you are using the document structure to find the variables? (e.g. folding regions or the sticky header feature) If so, then it's also possible to add this as a server functionality without changing the text: make variables also act as folding regions, and then they will show up in the sticky scroll as well

[Mario Carneiro]

that sounds even more useful in fact, since I'd rather see variable [Group G] in the sticky header than the section line that precedes it

[Anatole Dedecker]

That’s a good idea, except there are some files where that would take half of the reading space :sweat_smile:

[Kyle Miller]

I think the point is more to make sure that variables are used in a "structured" and scoped way, instead of altering them piecemeal. It helps with reasoning about them, for maintenance too.

[Kyle Miller]

Sometimes I've wondered (not very seriously) about variable and open being clauses to section and namespace, rather than being commands of their own.

[Anatole Dedecker]

One easy rule we can add is to prefer variable (x) in to make x explicit rather than do a lot of back and forth

[Mario Carneiro]

Anatole Dedecker said:

That’s a good idea, except there are some files where that would take half of the reading space :sweat_smile:

I believe VSCode already has some heuristics to avoid the sticky scroll taking up too much space. But I think it may not know what to prioritize in the case where the limit is exceeded

[Mario Carneiro]

you can try stacking up sections to see the behavior

[Bolton Bailey]

then it's also possible to add this as a server functionality without changing the text: make variables also act as folding regions, and then they will show up in the sticky scroll as well

This sounds incredibly useful. So often I have to scroll and search just to find out what the typeclass assumptions on a lemma are or make the mistake of thinking I have to declare a variable when it already exists in a variable above.

[Eric Wieser]

Patrick Massot said:

But I think the main thing should be to use different names for the types that have different type classes.

I think in the face of named arguments this is not so clear-cut idea. If I invoke a lemma as foo (R := _), and then someone comes along and say "actually, foo works for semirings", then it's a bit annoying for users to have to change to foo (S := _)

[Eric Wieser]

Obviously for rings/semirings this is perhaps close to desired behavior, but for large piles of typeclass variants without simple one-letter names, changing between (X := _) and (X''' := _) is going to be very annoying

[Patrick Massot]

That’s a good point that requires some attention.

[Martin Dvořák]

David Loeffler said:

I think there's a conversation to be had about the proper use of variable – some library files are prone to reusing type variables while repeatedly changing the instance assumptions on them, making it very hard to find what's being assumed at a given point.

Maybe we could make it a rule (enforced by a linter) that variable is only permitted at the start of a section (or other scoping construct e.g. namespace)?

I'd rather ban overriding declared variables. Forcing variables to be declared only at the start of a section will either make the Infoview messy or make the code "too much nested".

[Damiano Testa]

Kyle Miller said:

Sometimes I've wondered (not very seriously) about variable and open being clauses to section and namespace, rather than being commands of their own.

I like this idea a lot! I have often wished that variable {R} [Semiring R] in section ... end meant section variable {R} [Semiring R] ... end!

[Edward van de Meent]

i just thought of a small (probably fixable) issue with this:
i sometimes use multiple variable clauses to get variable? to work its magic. for flexibility, i then leave it behind like this:

variable {T:Type*} -- possibly also some other parameters to help `variable?` do its magic
variable --? [Foo T] =>
  [Bar T] [Baz T] [Foo T]

i don't know how this kind of pattern should/could be done (syntactically) when you make variable a clause to section or namespace, because the pattern (seems to) require multiple variable declarations...