# 2.12 Universal Quantifiers

A universal statement asserts that a property holds for every element of a type. In Lean, a proof of a universally quantified statement is a function that takes an arbitrary element and returns a proof of the property for that element.

The usual notation:

```lean
∀ x : α, P x
```

is implemented as a dependent function type.

## Problem

You want to prove or use a statement of the form:

```lean
∀ x : α, P x
```

To prove it, introduce an arbitrary element `x` and prove `P x`. To use it, apply the function to a specific argument.

## Solution

Use `intro` to introduce the quantified variable.

```lean
theorem forall_example
    (α : Type)
    (P : α -> Prop)
    (a : α)
    (ha : ∀ x : α, P x) :
    P a := by
  exact ha a
```

The hypothesis `ha` is a function. Applying it to `a` produces a proof of `P a`.

To prove a universal statement:

```lean
theorem forall_intro_example
    (α : Type)
    (P : α -> Prop) :
    (∀ x : α, P x) -> (∀ x : α, P x) := by
  intro h
  intro x
  exact h x
```

After `intro x`, the goal becomes:

```lean
⊢ P x
```

where `x` is arbitrary.

## Discussion

A universal quantifier behaves like a function:

```lean
∀ x : α, P x
```

is equivalent to:

```lean
(x : α) -> P x
```

The difference is that the result type depends on the input. The expression `P x` changes as `x` changes.

## Proving Universals

To prove:

```lean
⊢ ∀ x : α, P x
```

introduce a variable:

```lean
intro x
```

and then prove:

```lean
⊢ P x
```

Example:

```lean
theorem forall_identity
    (α : Type) :
    ∀ x : α, x = x := by
  intro x
  rfl
```

The proof works for any `x`, so it works for all `x`.

## Using Universals

If you have:

```lean
h : ∀ x : α, P x
```

then:

```lean
h a
```

is a proof of `P a`.

```lean
theorem forall_use
    (α : Type)
    (P : α -> Prop)
    (h : ∀ x : α, P x)
    (a : α) :
    P a := by
  exact h a
```

This is direct function application.

## Multiple Quantifiers

Multiple universal quantifiers introduce multiple variables.

```lean
theorem forall_two_variables
    (α : Type)
    (P : α -> α -> Prop) :
    (∀ x y : α, P x y) -> (∀ a b : α, P a b) := by
  intro h
  intro a b
  exact h a b
```

The type:

```lean
∀ x y : α, P x y
```

means:

```lean
∀ x : α, ∀ y : α, P x y
```

Each variable is introduced in order.

## Combining Universals and Implications

Universal quantifiers often appear with implications.

```lean
theorem forall_implication
    (α : Type)
    (P Q : α -> Prop) :
    (∀ x : α, P x -> Q x) ->
    (∀ x : α, P x) ->
    (∀ x : α, Q x) := by
  intro hPQ
  intro hP
  intro x
  exact hPQ x (hP x)
```

The structure is:

1. Introduce both hypotheses
2. Introduce an arbitrary `x`
3. Apply both functions at `x`

## Dependent Behavior

The key feature of `∀` is that the property depends on the chosen value.

```lean
theorem dependent_example
    (n : Nat) :
    ∀ m : Nat, m + 0 = m := by
  intro m
  simp
```

The property:

```lean
m + 0 = m
```

depends on `m`.

## Universals with Equality

Universal quantifiers are often used to state algebraic laws.

```lean
theorem add_zero_all :
    ∀ n : Nat, n + 0 = n := by
  intro n
  simp
```

This says that the identity holds for all natural numbers.

Using it:

```lean
theorem use_add_zero_all
    (h : ∀ n : Nat, n + 0 = n)
    (k : Nat) :
    k + 0 = k := by
  exact h k
```

## Universals and Existentials

A universal statement can produce an existential statement.

```lean
theorem forall_to_exists
    (α : Type)
    (P : α -> Prop)
    (h : ∀ x : α, P x)
    (a : α) :
    ∃ x : α, P x := by
  use a
  exact h a
```

The universal property guarantees that any chosen witness satisfies the predicate.

## Universals Over Propositions

Universal quantification also applies to propositions.

```lean
theorem forall_prop_identity :
    ∀ P : Prop, P -> P := by
  intro P
  intro hp
  exact hp
```

Here the variable `P` ranges over propositions, not data.

## Term Form

A universal proof is a function.

```lean
theorem forall_term
    (α : Type) :
    ∀ x : α, x = x :=
  fun x => rfl
```

The lambda abstraction corresponds directly to `intro`.

## Special Case: Nondependent Functions

If the property does not depend on the variable, the universal reduces to a simple function type.

```lean
theorem forall_nondependent
    (α : Type)
    (P : Prop) :
    (∀ _ : α, P) -> P := by
  intro h
  exact h arbitrary
```

Here the variable is unused in the predicate.

## Common Patterns

To prove:

```lean
⊢ ∀ x : α, P x
```

use:

```lean
intro x
```

then prove:

```lean
⊢ P x
```

To use:

```lean
h : ∀ x : α, P x
```

use:

```lean
h a
```

To handle multiple variables:

```lean
intro x y
```

To combine with implications:

```lean
hPQ x (hP x)
```

## Common Pitfalls

Do not forget to introduce the quantified variable. Without `intro`, the goal cannot be reduced.

Do not assume a specific value for `x`. The proof must work for an arbitrary element.

Do not confuse `∀ x, P x` with a conjunction over all elements. It is a function, not a finite collection of proofs.

Do not forget that the result type depends on the input. Each application produces a different proposition.

## Takeaway

A universal statement is a dependent function. To prove `∀ x, P x`, introduce an arbitrary `x` and prove `P x`. To use it, apply the function to a specific value. This correspondence between quantifiers and functions is a central pattern in Lean.