RFC: pp using forall notation for all pi types from a Type to a Prop

[kmill]

The following shows the current way that many common variations on pi types are pretty printed:

variable (α : Nat → Type) (p q : Prop) (P : Nat → Prop)

#check (i : Nat) → Nat  -- Nat → Nat
#check {i : Nat} → Nat  -- {i : Nat} → Nat
#check (h : p) → q      -- p → q
#check (i : Nat) → p    -- Nat → p
#check (i : Nat) → α i  -- (i : Nat) → α i
#check {i : Nat} → α i  -- {i : Nat} → α i
#check (i : Nat) → P i  -- ∀ (i : Nat), P i
#check {i : Nat} → P i  -- ∀ {i : Nat}, P i
#check {i : Nat} → p    -- ∀ {i : Nat}, p

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 of Prop-valued pi type frequently appears in the course of rewrites, where a forall quantifier becomes non-dependent:

example (P : Nat → Prop) (q : Prop) (h : ∀ n, P n = q) (hq : q) :
  ∀ n, P n :=
by
  simp [h]
  -- ⊢ Nat → q
  exact λ _ => hq

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 when u > 0 and v = 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 and v = 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 is Prop-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 print Nat → 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

#check (α : Type) → [DecidableEq α] → True
-- ∀ (α : Type) [inst : DecidableEq α], True

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.)

[gebner]

Unlike Lean 3, ∀ _ : Nat, p and Nat → p have very different semantics now. With ∀, the p is elaborated in the local context _ : Nat ⊢ Prop, while with → it is elaborated in the local context ⊢ Prop (i.e., it cannot refer to the Nat hypothesis, not even with assumption).

I'm not sure if I understand the concrete proposal here. There seem to be several changes mixed in with the motivational text:

1. Output ∀ _ : Nat, p instead of Nat → p if p is a Prop and the forall is non-dependent.
2. Output ∀ [DecidableEq α] instead of ∀ [inst : DecidableEq α] if the forall is non-dependent (or maybe the inst doesn't appear in the body, which seems much more likely?).
3. Output {_ : α} → instead of {x : α} → if the forall is non-dependent.

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 (x := 42) notation).

[kmill]

@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 _ variable available in the context? I would have thought the semantics of a _ variable is to be inaccessible. Edit: as in unable-to-be-accessed, in the clear sense and not the Lean 4 sense. I don't immediately see problems with them working this way for pi type binders.

[digama0]

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 assumption. (This is by contrast to the clear tactic, which removes the variable entirely from the local context so tactics cannot reference it.)

[gebner]

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 assumption:

#check ∀ __ : Nat, ‹Nat› = 1 -- tactic 'assumption' failed
#check ∀ __ : Nat, __    = 1 -- ∀ (__ : Nat), __ = 1 : Prop

[djvelleman]

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 Lean.Expr.isArrow doesn't give what I consider to be the right answer to that question.