Forall vs. if-then

Stream: lean4

[Dan Velleman]

Consider this example:

example : ∀ (n : Nat), ¬ ∃ (x : Fin n), x ≠ x := by

In the tactic state, the goal is shown as ℕ → ¬∃ x, x ≠ x. I have said before that I don't really like the algorithm that is used to distinguish between "forall" and "if-then," but in this case I'm really puzzled. I assumed that what was being used was Lean.Expr.isArrow, which checks to see if the body of the forallE has loose bound variables. Well, in this case the body does have a loose bound variable, namely the reference to n in Fin n. So why is this displayed using an arrow rather than a universal quantifier?

[Gabriel Ebner]

This is actually a pretty-printing bug... → is always non-dependent, while the specific ∀ here is dependent.

[Gabriel Ebner]

Please file an issue.

[Gabriel Ebner]

The following would be a valid use of → by the pretty-printer though:

#check ∀ n : Nat, ¬∃ x : Nat, x ≠ x

[Gabriel Ebner]

Ultimately this boils down to the underlying type theory; both implication and forall are represented as Expr.forallE. So the pretty-printer needs to make a choice whether to show the .forallE as an implication or a forall.

[Dan Velleman]

OK, I'll file an issue.
Yes, I understand that implication and forall are both represented as forallE. In my opinion, the pretty-printer algorithm should be changed. For an expression forallE name type body binderinfo that has type Prop, I think that if the type of type is not Prop then, even if body has no loose bvars, the expression should be displayed with a universal quantifier. In logic, it is not uncommon to have "vacuous quantifiers" like ∀ x : Nat, p. I understand that, to Lean, this is the same as Nat → p, but that's not how any mathematician would write it. For expressions of other types, the current algorithm makes sense. But if an expression has type Prop, then in my opinion it should be displayed so that it looks like a proposition. And that means the arrow should mean "implies", and therefore it should only be used if what's on the left is a proposition.

[Kevin Buzzard]

+1 for "Nat -> p looks weird to mathematicians"

[Kevin Buzzard]

On the other hand, it would be a bit weird to have a nat and then a prop which didn't depend on it ...

[Kyle Miller]

@Kevin Buzzard Sometimes these non-dependent foralls arise incidentally to rewrites (for example, if you have ∀ (n : ℕ), 1 ≤ f n and make use of ∀ (n : ℕ), f n = 37). I imagine you've had students become confused when their foralls turn into functions. There at least have been occasional questions on #new members about this.

[Dan Velleman]

I agree with @Kyle Miller that non-dependent foralls arise naturally in math. They also arise in formal logic. For example, there is a rule of logic that says that forall distributes over and: ∀ x, P ∧ Q is equivalent to (∀ x, P) ∧ (∀ x, Q). One would want to be able to apply this rule even in cases in which P is a statement about x but Q doesn't mention x. It would certainly be awkward to have separate versions of the rule depending on whether both P and Q mention x or only one of them does.

Here's a related point. Consider this example:

example (p1 : Nat → Type) (p2 : Nat → Prop) (h1 : ∀ n : Nat, p1 n) (h2 : ∀ n : Nat, p2 n) : True := by

In the tactic state, the type of h1 is displayed as (n : ℕ) → p1 n, and the type of h2 is ∀ (n : ℕ), p2 n. So it appears that there is a precedent for displaying expressions of type Prop differently from expressions of other types. The difference here makes sense to me: h2 is best thought of as a universally quantified statement, but h1 is best thought of as a function type. I think a similar principle applies to the case of ∀ n : Nat, p. If p is a proposition, then this is best thought of as a universally quantified statement (even though p doesn't refer to n), but if p is not a proposition then it makes sense to think of the expression as representing the type Nat → p.

Would there be a down side to making this change?

[Kyle Miller]

@Dan Velleman A couple days ago I experimented with making the change for Lean 3, and it was relatively straightforward. There didn't seem to be any downsides that surfaced through the test suite. (I just uploaded it: lean#770, and look at in particular pp_forall.lean for some tests.)