Implication vs. Universal Quantification

Stream: lean4

[Dan Velleman]

In this example:

example (p : Nat → Prop) : ∀ x : Nat, ∃ y : Nat, p y :=

Lean displays the goal as Nat → ∃ y, p y, but surely it should be displayed as ∀ x : Nat, ∃ y, p y. I assume the problem is that both implication and universal quantification are represented by Expr.forallE. Perhaps Lean is trying to distinguish between the two by using Lean.Expr.isArrow, which appears to check to see if the body of the forallE depends on the bound variable. That's fine as a test to distinguish dependent vs. nondependent arrows, but it seems to me it's not the right test to distinguish implications from universal quantifications; sometimes mathematicians use vacuous quantifiers, and they should be displayed as quantifiers, not arrows. Perhaps the test, in the case of a Expr.forallE expression of type Prop, should be that it is an implication if the body doesn't depend on the bound variable and the type of the bound variable is a proposition, and otherwise it is a universal quantifier.

[Mario Carneiro]

I'm not sure I share your "obviously it should be a forall" intuition. In particular, if the body is large it can be very useful to see at a glance that the variable is unused because it is shown as an implication, and the fact that forall and implication are the same thing in lean is something that users will have to get used to anyway.

[Reid Barton]

I don't think it ever makes sense in ordinary math notation to write $X \to P$, where $X$ is a set and $P$ is a proposition. From that perspective I agree with "obviously it should be a forall".

[Reid Barton]

Given that there is already a heuristic for when to display $\Pi$ versus $\forall$, I think it would probably make sense to try to get this "right" as well

[Reid Barton]

That said, I see that Lean 3 has the same behavior and I don't think I ever noticed it before, so it probably comes up quite rarely.

[Dan Velleman]

Yes, I noticed it in Lean 3 as well.

If I were teaching a logic course using Lean, I would want to be able to use vacuous quantifiers and have them appear as quantifiers. I wouldn't want to have to explain to students how Lean represents implications and universally quantified statements internally.

Here is a somewhat contrived example.

example : ∀ z x : Nat, ∃ y : Nat, y = 2 * z := by
  intro z
  intro x
  apply Exists.intro (2 * z)
  exact rfl

At the beginning of the proof, the goal is displayed as ∀ (z x : Nat), ∃ y, y = 2 * z. After intro z, it is displayed as Nat → ∃ y, y = 2 * z, not ∀ x : Nat, ∃ y, y = 2 * z. That seems wrong to me.

In Lean 3, it was worse. If you do this same example in Lean 3, the original goal is displayed as ∀ (z : ℕ), ℕ → (∃ (y : ℕ), y = 2 * z). So something has been changed, but I don't think it's right yet.

[Kyle Miller]

(For Lean 3, here's where arrow/pi/forall is selected. There could easily be a setting that causes prop-valued implications that quantify over a Type to always display using forall.)

[Mario Carneiro]

Reid Barton said:

That said, I see that Lean 3 has the same behavior and I don't think I ever noticed it before, so it probably comes up quite rarely.

I've seen it a few times in lean 3. The majority of the time it means that I made a binding error like ∀ x, .... ∀ x, p x where I wanted the x to bind to the outer one. Possibly the unused variable linter can help here?