feat: add implementation-detail hypotheses

[gebner]

This PR adds a new flag to local declarations that indicates whether they are auxiliary declarations (for recursive calls, .auxDecl), implementation-detail hypotheses (temporary variables introduced by do-notation, etc., .implDetail), or just normal hypotheses (.default). As a result, we can remove the complicated ToHide heuristic. Assumptions are now hidden in the goal display if and only if they are implementation-detail, it does not matter whether they are inaccessible or in Prop. Relatedly, we also remove the .auxDecl binder info and the unhygienic mkAuxDiscr hack for match.

The only syntax to introduce these implementation-detail hypotheses is to give them a name beginning with two underscores (e.g., __x). Note that this happens in the elaborator: withLocalDecl is unchanged and will always create a default hypothesis (unless you supply the optional kind argument). (In the future we might want to change this to an attribute on the bound variable, i.e., something like let @[implDetail] x := 42; x.)

let __x : Inhabited Nat := ⟨42⟩
(‹Inhabited Nat›, -- fails
 (default : Nat), -- does not use __x instance, returns 0
 __x) -- only this works

(Earlier versions of this feature called for different bind-site and use-site names: let __x := 42; x. I have discarded this option because it introduces weird edge-case behavior with macros. Think e.g. of macro "foo" x:ident : term => `(let $x := 42; $x) which would break in that case.)

The goal display is now always the same, no matter whether you have a term goal or a tactic goal, no matter whether the assumption is in Prop or not. Fixes #1449.

https://leanprover.zulipchat.com/#narrow/stream/147302-lean4-maintainers/topic/.5BRFC.5D.20story.20for.20implementation-detail.20hypotheses/near/302550975

[gebner]

!bench

[leanprover-bot]

Here are the benchmark results for commit f05104a.
There were no significant changes.

[gebner]

There were no significant changes.

I think this might be a velcom bug. It just doesn't find a common ancestor commit for comparison. Here is the actual comparison: http://speedcenter.informatik.kit.edu/velcom/compare/434e57ec-67cb-4822-be48-14f108424a1f/to/bab50d33-13a1-40c4-85a0-fda5f93f8b22?hash2=f4b04216ebd6ff5e62e1814c2257a3b50075599a There are a few changes, but nothing big (certainly no explosion due to do-join-points or anything like that).

[gebner]

Note: there's one rough edge left over. The syntax matchers still add x : Syntax := { raw := __discr } to the local context. I tried changing them to have, but that fails for a completely unexpected reason: there is a test that checks whether we can do well-founded recursion on syntax. And of course that requires a let-binding (to know that x is smaller than the original discriminant)...

[Kha]

there is a test that checks whether we can do well-founded recursion on syntax

It's not clear to me how important that one is in practice. @leodemoura?

[digama0]

My suggestion is to abandon well founded recursion on syntax. We could reintroduce it with an option if users clamor for it but I think the vast majority of code written on Syntax just doesn't care about use of partial.

[leodemoura]

My initial reaction is similar to @digama0: abandon well founded recursion on syntax (at least for now).

It's not clear to me how important that one is in practice. @leodemoura?

I am assuming it is not important. @gebner Could you post a link to the test here?

[Kha]

It's https://github.com/leanprover/lean4/blob/master/tests/lean/run/syntaxWF.lean

[gebner]

Just to be clear: we don't well-founded recursion on syntax by default. The test only shows that this is possible, but we don't make use of that possibility anywhere AFAICT.