Pre-RFC: Synthing noncomputable instances in proofs?

Stream: lean4

[Thomas Murrills]

Some instances, like Classical.propDecidable or Fintype.ofFinite, noncomputably create data: this makes them unacceptable in defs and type signatures, but they are acceptable within proofs.

We seem to work around this in an ad-hoc way, by e.g. using the scoping tactic classical, term-mode open scoped Classical in, or asking the user to have the instance in manually (Fintype.ofFinite is not an instance, just a def you can have into the local context).

In principle, though: we could try to keep track of whether we are in a proof/noncomputable context in the TermElabM or MetaM context. We could then tag "proof-only" instances, and have typeclass synthesis only use them when the flag is passed or set.

This would mean we'd no longer need things like classical or have := Fintype.ofFinite to make the instances available; the instances would be usable within proofs automatically (and, by default, not available in type signatures or outside of proofs).

One challenge would be that we'd need to pin down when exactly we want to consider ourselves "within a proof". My first thought is simply when inside of something like a theorem declaration body, so that it's predictable (or by manually setting it). (This lets us avoid worrying about metavariable assignment times and such if we were to take a Prop-expected-type approach.)

So, one approach would be setting up this flag in three places:

• add a flag to the appropriate monad's context which signals being in a "noncomputable elaboration context" (like a theorem body), and turn it on in appropriate places
• record a flag for instances saying whether they're "proof-only"
• handle the (ambient) flag in typeclass synthesis to make it include or exclude such instances from the search

Some questions:

Are there other cases where "knowing whether we're elaborating something noncomputable" is useful? Instance synthesis is the motivation, but it seems plausible that this information could be useful in other situations.

Would there be any major drawbacks or hurdles, e.g. cases where this would systematically be "the wrong thing to do", and we'd have to manually set the flag?

Just wondering if this is worth exploring. :)

[Michael Rothgang]

Let me ask the dreaded question first: is this change a good idea?

I'm not sure. I also like that opting into classical logic is explicit (though this is not a strong opinion).
At the same time, I agree that starting a proof, realising you want to add classical and manually doing so breaks the loop. (And leads to not-as-experience users writing have := Classical.propDecidable and somesuch manually; I've cleaned up several such instances in the Carleson project.)

What do you think about a try this suggestion instead: if we're inside a proof, we need a classical instance and don't have one, have the error message contain a suggestion to use classical. This hopefully keeps friction relatively low, but keeps the current property "you can see where it is used".

[Thomas Murrills]

Hmm, so to be clear, this would be more or less the same change under the hood--i.e. we would have proof-only instances, typeclass synthesis would try them in proofs--but if typeclass synthesis failed, it would retry with proof-only instances activated, and if successful, make a try-this suggestion?

[Michael Rothgang]

(Perhaps only retrying if the right kind of instances were not found.)

[Thomas Murrills]

Michael Rothgang said:

I also like that opting into classical logic is explicit

Minor point: is it explicit, though? :grinning_face_with_smiling_eyes: by_cases introduces classicality silently, for example. I wonder if anything else does.

[Thomas Murrills]

My impression along those lines has been that Lean is intended to be a classical language when it comes to proofs, and that maybe we should embrace this and instead mark opting out explicitly, since it's not clear (to me!) how one could actually use constructivity of proofs in Lean's proofs, given proof irrelevance.

[Thomas Murrills]

(I'm imagining that with the original "it just works" approach, one could use an elaborator like constructive% to unset the flag and opt out.)

[Thomas Murrills]

But, in any case, since the infrastructure largely overlaps, maybe we can walk this question back to simply "is at least one of these options worth exploring?" :)