Clarification on \forall in Lean4

Question

The following paragraph appears early in the chapter on quantifiers and equality in "Theorem Proving in Lean 4":

The Calculus of Constructions therefore identifies dependent arrow types with forall-expressions in this way. If p is any expression, ∀ x : α, p is nothing more than alternative notation for (x : α) → p, with the idea that the former is more natural than the latter in cases where p is a proposition. Typically, the expression p will depend on x : α. Recall that, in the case of ordinary function spaces, we could interpret α → β as the special case of (x : α) → β in which β does not depend on x. Similarly, we can think of an implication p → q between propositions as the special case of ∀ x : p, q in which the expression q does not depend on x.

The last sentence mentions the expression ∀ x : p, q, where q can depend on x, and compares it to p → q where p and q are propositions.

My question is this: Are there any real examples of ∀ x : p, q being used when the following hold?

• p is a proposition (so x is a proof of p)
• q depends on x

In normal mathematics the expression ∀ x : p, q would be used when p is a set rather than a proposition, so this use confuses me.

I tried to come up with examples of ∀ x : p, q where p and q are propositions and q depends on the proof of p. I couldn't find any situations where I've seen this in normal mathematics.

Answer 1

This might not count as a "real [mathematical] example", but List.head?_eq_head seems like an good example

@List.head?_eq_head :
  ∀ {α : Type u_1} (l : List α) (h : l ≠ []),
    List.head? l = some (List.head l h)

Your p is my l ≠ [] and your x is my h.

Here List.head produces the first element of a list; but this operation is impossible if the list is empty, so it has to take a proof that it is non-empty.

Answer 2

Lean 4 has consolidated ∀ with Π, allegedly to avoid confusing new users (at the cost of confusing older users/mathematicians with previous experience in dependent type theory.) The notation Π x: p, q is rare outside discussions of the Curry-Howard corrspondence, but is nevertheless standard in that context; it also appears in the Wikipedia article for dependent type theory in general.

The notation does not generally appear elsewhere in math for a simple reason: usually, it doesn't matter which proof of a theorem you use, so never mind having a special notation for meta-level problems about choice of proof, we don't even really have notation for distinguishing proofs in the first place. It is a problem somewhat unique to the field, and so has notation equally unique.