-
Notifications
You must be signed in to change notification settings - Fork 350
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
RFC: pp using forall notation for all pi types from a Type to a Prop #1834
Comments
Unlike Lean 3, I'm not sure if I understand the concrete proposal here. There seem to be several changes mixed in with the motivational text:
I think (2) is uncontroversial. I'm not sure how I feel about dropping the names in favor of underscores, the names are semantically relevant (since they determine whether you can use the |
@gebner I've tried to clarify what this RFC is about. The primary suggestion is roughly 1 (without saying anything about what to do to indicate dependence). The goal is to somehow get pi types that are morally universal quantifiers to display as universal quantifiers. Everything in the RFC about placeholders is to solve the problem that this does cause loss of information for an expert Lean user. The specific implementation is very Lean-3-specific and it might not be appropriate for Lean 4, espcially given what you say about differences in elaboration. I wonder though -- why is a |
An inaccessible variable is still in the local context, it just doesn't have a name you can write. So you can still pick it up with things like |
For additional confusion, there's also implementation-detail hypotheses (beginning with a double underscore). These are in the local context (but hidden), have a name you can write, but are not picked up by tactics like #check ∀ __ : Nat, ‹Nat› = 1 -- tactic 'assumption' failed
#check ∀ __ : Nat, __ = 1 -- ∀ (__ : Nat), __ = 1 : Prop |
I agree with kmill. "Vacuous quantifiers" come up all the time in logic and mathematics, and mathematicians expect them to be displayed as quantifiers. In writing my own tactics, I have found it necessary to implement the test proposed by kmill for whether a proposition is a quantified statement or an implication, because |
The following shows the current way that many common variations on pi types are pretty printed:
This RFC is primarily about the
Nat → p
case, which tends to be the most surprising (it is a source of questions on Zulip). This sort ofProp
-valued pi type frequently appears in the course of rewrites, where a forall quantifier becomes non-dependent:The meaning of a non-dependent pi from a Type to a Prop is generally a universal quantification, so the pretty printer should represent such pi types in some way such that this is clear.
Concretely, given
ι : Sort u
andα : ι → Sort v
, then whenu > 0
andv = 0
we should make sure to use∀
when pretty printing the corresponding pi type forα
, even if the pi type is nondependent.The nondependent
u = 0
andv = 0
case should be left alone since the implication arrow serves its purpose just fine.There are a couple of additional considerations presentation-wise.
While pretty printing pi types using
∀
gives the user the information that it isProp
-valued, this leads to the user not being able to immediately see whether the quantifier is dependent or not; in discussion, it was brought up that this information is important for expert Lean users. One possible solution to this is to pretty printNat → p
as∀ (_ : Nat), p
(rather than∀ (i : Nat), p
) with a placeholder for the variable. This way one can immediately see it is a Prop-valued non-implication non-dependent pi type.This leads to some inconsistency when it comes to non-default binders for other nondependent pi types. One might entertain using placeholders in every context where a non-dependent pi would print a binder. For example,
{_ : Nat} → Nat
rather than{i : Nat} → Nat
. This does lead to loss of information that is important for(i := 22)
argument notation. There are other solutions (such as using a tombstone, or using semantic coloring in an editor), or we can simply choose to tolerate any potential inconsistency here.In a similar direction, for instance binders we currently have
With suggestions above, this would pretty print as
∀ (α : Type) [_ : DecidableEq α], True
since the instance binder is non-dependent, but one may as well pretty print it as∀ (α : Type) [DecidableEq α], True
since it gives the same amount of information while looking prettier.(The Lean 3 version of this RFC is lean PR 770.)
The text was updated successfully, but these errors were encountered: