Skip to content

2.11 Existential Quantifiers

An existential statement says that some object exists with a given property.

lean proof-assistant type-theory logic proof-theory quantifiers

An existential statement says that some object exists with a given property. In Lean, a proof of Exists P contains two pieces of data: a witness and a proof that the witness satisfies the predicate.

The usual mathematical notation:

∃ x, P x

means:

Exists (fun x => P x)

Problem

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

∃ x : α, P x

To prove it, provide a witness x and then prove P x. To use it, unpack the witness and its proof.

Solution

Use use to provide a witness.

theorem exists_nat_example : ∃ n : Nat, n = 3 := by
  use 3

After use 3, the goal becomes:

⊢ 3 = 3

Lean closes it by reflexivity.

A more explicit version is:

theorem exists_nat_example_explicit : ∃ n : Nat, n = 3 := by
  use 3
  rfl

Providing a Witness with a Nontrivial Proof

The witness fixes the remaining goal.

theorem exists_even_example : ∃ n : Nat, n + n = 6 := by
  use 3

After use 3, Lean checks:

⊢ 3 + 3 = 6

This reduces by computation.

For a proof that needs a library theorem:

theorem exists_add_zero (a : Nat) : ∃ n : Nat, a + n = a := by
  use 0
  simp

The witness is 0. The remaining goal is:

⊢ a + 0 = a

which simp proves.

Constructing Existentials Directly

The constructor for existential statements is Exists.intro.

theorem exists_intro_term : ∃ n : Nat, n = 3 :=
  Exists.intro 3 rfl

The first argument is the witness. The second argument is the proof that the witness satisfies the predicate.

For:

∃ n : Nat, n = 3

the witness is:

3

and the proof is:

rfl : 3 = 3

Using an Existential Hypothesis

If you have:

h : ∃ x : α, P x

then you can extract a witness and its property proof by case analysis.

theorem exists_use_example
    (h : ∃ n : Nat, n = 3) :
    ∃ m : Nat, m + 1 = 4 := by
  cases h with
  | intro n hn =>
    use n
    rw [hn]

After cases h, Lean gives:

n : Nat
hn : n = 3
⊢ ∃ m : Nat, m + 1 = 4

The proof uses the same witness n, then rewrites n to 3.

Destructuring with rcases

For existential hypotheses, rcases gives compact destructuring.

theorem exists_use_rcases
    (h : ∃ n : Nat, n = 3) :
    ∃ m : Nat, m + 1 = 4 := by
  rcases h with ⟨n, hn⟩
  use n
  rw [hn]

The pattern:

⟨n, hn⟩

extracts the witness n and the proof hn.

Existentials with Multiple Conditions

Existential predicates often contain conjunctions.

theorem exists_with_and : ∃ n : Nat, n = 3 ∧ n + 1 = 4 := by
  use 3
  constructor
  · rfl
  · rfl

After use 3, the goal is:

⊢ 3 = 3 ∧ 3 + 1 = 4

Then constructor splits the conjunction.

Using Existentials with Conjunctions

When an existential contains a conjunction, unpack both layers.

theorem exists_and_use
    (h : ∃ n : Nat, n = 3 ∧ n + 1 = 4) :
    ∃ n : Nat, n + 1 = 4 := by
  rcases h with ⟨n, hn_eq, hn_add⟩
  use n
  exact hn_add

The pattern:

⟨n, hn_eq, hn_add⟩

is shorthand for unpacking:

⟨n, ⟨hn_eq, hn_add⟩⟩

The first component is the witness. The remaining components are proofs from the conjunction.

Changing the Witness

Sometimes the output witness differs from the input witness.

theorem exists_successor
    (h : ∃ n : Nat, n = 3) :
    ∃ m : Nat, m = 4 := by
  rcases h with ⟨n, hn⟩
  use n + 1
  rw [hn]

After rewriting n to 3, the goal becomes:

⊢ 3 + 1 = 4

which is solved by computation.

Existentials Over Arbitrary Types

Existentials are not limited to natural numbers.

theorem exists_self
    (α : Type)
    (a : α) :
    ∃ x : α, x = a := by
  use a

The witness is the given value a.

A predicate version:

theorem exists_from_predicate
    (α : Type)
    (P : α -> Prop)
    (a : α)
    (ha : P a) :
    ∃ x : α, P x := by
  use a

After use a, the goal is exactly P a, which is already available as ha. Lean can close it, but an explicit version is clearer:

theorem exists_from_predicate_explicit
    (α : Type)
    (P : α -> Prop)
    (a : α)
    (ha : P a) :
    ∃ x : α, P x := by
  use a
  exact ha

Existentials and Equality Transport

A common pattern is to unpack an existential, rewrite with an equality, and rebuild another existential.

theorem exists_transport
    (P : Nat -> Prop)
    (h : ∃ n : Nat, n = 3 ∧ P n) :
    P 3 := by
  rcases h with ⟨n, hn_eq, hnP⟩
  rw [← hn_eq]
  exact hnP

Here hn_eq : n = 3. The goal is P 3, while the available proof is hnP : P n. Rewriting backward changes P 3 to P n.

Nested Existentials

Multiple existential quantifiers are nested.

theorem exists_pair_example :
    ∃ n : Nat, ∃ m : Nat, n = m := by
  use 3
  use 3

This means:

∃ n : Nat, (∃ m : Nat, n = m)

To unpack:

theorem exists_pair_use
    (h : ∃ n : Nat, ∃ m : Nat, n = m) :
    ∃ k : Nat, k = k := by
  rcases h with ⟨n, m, hnm⟩
  use n

The pattern ⟨n, m, hnm⟩ unpacks both existential layers.

Existentials and apply

You can construct an existential with apply Exists.intro.

theorem exists_apply_intro : ∃ n : Nat, n = 5 := by
  apply Exists.intro 5
  rfl

This is more verbose than use, but it exposes the constructor.

Common Patterns

To prove:

⊢ ∃ x : α, P x

use:

use a

then prove:

⊢ P a

To use:

h : ∃ x : α, P x

use:

rcases h with ⟨x, hx⟩

or:

cases h with
| intro x hx => ...

To prove an existential with several properties:

use a
constructor

To unpack nested existential and conjunction data:

rcases h with ⟨x, hx₁, hx₂⟩

Common Pitfalls

Do not try to prove an existential without choosing a witness. Lean needs a concrete term for the quantified variable.

Do not assume the witness has a particular name. After unpacking an existential, choose names that reflect how the witness will be used.

Do not forget that ∃ x, P x ∧ Q x contains a witness and then a conjunction of proofs. You must unpack both layers when needed.

Do not rewrite in the wrong direction when moving a property from the witness to a known value.

Takeaway

An existential proof is a witness plus evidence. To prove ∃ x, P x, provide a witness and prove the predicate for that witness. To use ∃ x, P x, unpack the witness and the proof, then continue with those concrete objects in the local context.