chore: normalize naming convention in theorems

[digama0]

Now that the naming convention has been tested in mathlib, I think it is safe to backport the changes to lean core and normalize any remaining inconsistencies in theorem names. Here are the more prominent changes:

• {out, opt, auto}Param -> {Out, Opt, Auto}Param. This is because these operate on types to produce another type, even if they are just annotations.
• Lawful{Functor, Applicative, Monad} -> IsLawful{Functor, Applicative, Monad}. This is probably the most debatable of the changes here, but we want to keep the Is* naming convention for classes which are propositions, at least when the * is a noun, so that we can differentiate between IsGroup and Group. I did not apply the naming change to LawfulBEq because the grammar is a bit strained; discuss.
• I considered but did not rename Membership to HasMem. In mathlib we are finding that we still need Has* classes when the original name is already taken; AndOp is another example of this. Using Membership is a pattern that doesn't scale.
• Membership.mem -> Membership.Mem, following the practice that even structure fields are capitalized if they denote types or relations / propositions.
• congr{Arg, Fun} -> congr{_arg, _fun}. This one should not be too contentious.
• T.constr.injEq -> T.constr.inj_eq
• by{Cases, Contradiction} -> by{_cases, _contradiction}
• I considered but did not rename Ne -> NE. The rationale is that it is an acronym, matching the distinction between Eq and LE. Discuss.
• ofReduce{Bool, Nat} -> of_reduce{Bool, Nat}
• left_distrib -> mul_add, right_distrib -> add_mul. The names are more mnemonic and descriptive, and the latter names were already being provided as aliases. In mathlib4 the "distrib" aliases have already been removed and this is backporting the change to core.
• Membership.mem.{lower, upper} -> Std.Range.mem_{lower, upper}. It's unfortunate that we lose dot notation here but the original names were way too generic (they are about the upper and lower bounds induced by membership in a Std.Range). You can still use dot notation with the less mnemonic h.1, h.2 though.
• and_true -> and_true_eq, true_or -> true_or_eq and so on. We talked about this before. These are simp lemmas that use equality on proposition and std/mathlib would like to use the unadorned names for the iff version. Since they are usually not referenced directly, it seems reasonable to disambiguate these lemmas.

[semorrison]

Because this has stage0 changes, there's no possibility of merging master. We'd either need to do a rather tedious rebase, or effectively start over.

I will be a bit sad if we don't do this (or at least a big chunk of it). Naming consistency is really nice, even if it is not immediately high impact.

Perhaps we could get this done in smaller parcels...?

[digama0]

Because this has stage0 changes, there's no possibility of merging master. We'd either need to do a rather tedious rebase, or effectively start over.

There is a standard procedure for rebasing PRs that contain update-stage0 commits, which is to git rebase -i, and replace the update stage0 commit with x update-stage0.sh where update-stage0.sh is:

#!/bin/sh
cd build/release
make update-stage0
git add ../../stage0/
git ci -m "chore: update stage0"

In other words, rebase the other commits normally but delete and recreate the update-stage0 commits. This is exactly why they are kept separate.

[semorrison]

Interesting! This script should live somewhere. :-)

It could also do with a -j 32 on the make, and use git commit instead of git ci for portability.

Also for anyone coming afterwards, you need a path to the update-stage0.sh script, e.g. x ./update-stage0.sh.

It's taken me a few tries to resolve the first set of conflicts so that update-stage0.sh succeeds... we'll see where it goes.

---

I've attempted the rebase, but I don't really like the result. In particular, the rename iff_self to iff_self_eq results in every call to simp failing, because it is a simpOnlyBuiltin (and just renaming it there doesn't help). I'm not quite sure how this was working out previously.

Init/Data/Nat/Basic.lean:626:17: error: unknown constant 'iff_self'

[digama0]

I've attempted the rebase, but I don't really like the result. In particular, the rename iff_self to iff_self_eq results in every call to simp failing, because it is a simpOnlyBuiltin (and just renaming it there doesn't help). I'm not quite sure how this was working out previously.

The follow up changes were never performed, it was pending a clearer 👍 regarding the specific renames in question before it seemed worth it to fix the issues.