feat: private elaborator for proofs

[thorimur]

This PR adds the private <term> term elaborator which wraps term-mode proofs in a public auxiliary declaration so that they can use private constants in public positions. For example, a term-mode proof appearing in a public declaration's type will error if it uses a private declaration.

Currently, by exact will wrap the proof in a private declaration as private does, but sprinkling code with by exacts hurts readability, since it's difficult to tell at a glance what motivated its presence. Also, private reports when it's unnecessary, unlike by exact.

Disclosure: I had Claude review this before PRing, seeing if I could get rid of elaborating by. It found a good reason to do so, and made some changes, which I then reviewed and iterated on myself. I've preserved the (only) LLM-generated changes via the authorship of the commit history.

---

[github-actions]

PR summary 53b0ce2064

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
../mathlib-ci/scripts/pr_summary/import_trans_difference.sh all
There are 8250 files with changed transitive imports taking up over 359885 characters: this is too many to display!
You can run this locally from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

---

Declarations diff (regex)

+ F
+ FEq
+ aPriv
+ bPriv
+ f
+ f'
+ fImplicit
+ fImplicit'
+ fLocal
+ fNestedBy
+ fProofsInPublic
+ foo
+ fooPub
+ fooThm
+ fα
+ fα'
+ fα''
+ fαPub'
+ fαPub''
+ gImplicit
+ implicitThm
+ sup_aux
+ truncatedSup
+ usePriv

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 53b0ce2).

• +1 new declarations
• −0 removed declarations

+Mathlib.Tactic.PrivateProof.privateElab

---

Increase in strong tech debt: (relative, absolute) = (1.00, 1.00)

Current number	Change	Type (strong)
685	1	backward.privateInPublic
1	1	backward.proofsInPublic

No changes to weak technical debt.

Current commit 53b0ce2064
Reference commit 87adeaebd3

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[JovanGerb]

I'm not sure if it makes sense to reserve the private keyword for just proofs. In principle, you could want to wrap a definition in private, similar to how we can already do this with unsafe.

Also, there is already a private syntax that can be used when declaring fields of an instance (... := private ...), which I think works for proofs and values.

[thorimur]

Maybe...but I do think we want to be able to have something that is dedicated to proofs and performs the wrapping that by exact does in the same circumstances but in a more readable way.

The argument for the current design might look like this: I claim that proofs are qualitatively different when it comes to to wrapping them in aux decls thanks to proof irrelevance, and that wrapping a non-proof is correspondingly a bigger deal (and you should use private_decl% or an aux definition to signal this). Structure instance fields are a bit of an outlier since each field is more like a separate body.

The argument against is what you said; it's inconsistent. :)

Maybe either (1) the error message should point to private_decl% or (2) this should be called private_proof(%).

(EDIT: I've tentatively done (1), at least.)

[JovanGerb]

I think I would prefer (2) because of how general the word private is, and it seems unreasonable to restrict it to only proofs. If you're looking to have a short name, we could potentially just call it proof%.

[thorimur]

After thinking about it a bit, I do worry that it might become very easy to "hold it wrong" if private could be used without error for non-proofs. You don't want to make it so that bad decisions are too easy to make. I'm worried that "I'll just fix this unknown identifier error by putting private on there" should really only work for proofs (if anything), because they do behave qualitatively differently than terms.

This is to say that I think it actually is reasonable to disallow private for non-proofs 🙃 But that's not to say we should allow it for proof terms, if only because the ubiquity will make people think you should be able to write it everywhere. So my concern about private for non-proofs is compatible with both private-just-for-proofs and something-else-just-for-proofs (no private elaborator at all) 😁