POLL: Names of universally quantified variables

Stream: Equational

[Terence Tao]

Currently, the universally quantified variables we use for equations are ordered x y z w u v. This is not in alphabetical order, and also does not obviously continue into a seventh variable in the possible scenario that we may need to introduce such variables somehow. In #170, the alternate ordering x y z w v u was proposed, which could then continue downwards alphabetically for 20 more variables without difficulty. One could also just use the usual alphabetical ordering a b c d e f, or index x by natural numbers or positive integers. Given the high participation rate of previous polling, it seems this issue is another one that could be settled by a poll, so here we go.

[Terence Tao]

/poll How should universally quantified variables be ordered?
x y z w u v (current ordering)
x y z w v u
a b c d e f
x0 x1 x2 x3 x4 x5
x1 x2 x3 x4 x5 x6

[Terence Tao]

Hmm, while there seems to be reasonable consensus to change the ordering of variables, there is not strong consensus on what to change the ordering to. Some more discussion on this thread might be appropriate.

Furthermore, I would like to discuss the technical challenges of implementing a refactor. Changing the blueprint text is of course trivial. Changing Equations.lean and AllEquations.lean should also be easy, as well as the auto-generated list of equations such as https://github.com/teorth/equational_theories/blob/main/data/equations.txt , but we should also change any software that generates such lists.

As for the already millions of existing Lean proofs that (implicitly or explicitly) use the current ordering... perhaps they can just be left untouched? I believe changing the variable names will keep all EquationX definitions syntactically equivalent, and so if a legacy proof introduces variables with the "wrong" names, Lean should still compile. Of course going forward it would be good to align the notation of any computer generated proofs with the new naming, but I don't see it as a priority to make sure the legacy proofs have exactly the same notation. But maybe I'm missing something, would be happy to hear more thoughts.

[Terence Tao]

Given the lack of consensus on what new ordering of variables to switch to, I am proposing that we keep the status quo at present. However, if someone wishes to push for a new ordering, and is also willing to perform the refactor needed, I will keep the discussion open here so that they may make a proposal.

[Shreyas Srinivas]

I think the refactor is the big dampener here. Because the project has grown organically people will be hesitant to fix other people's code.