Strategy: Provide a witness

Pattern recognition

When you see: a goal of the form ∃ x, P(x)

Strategy: Name a specific value and prove it satisfies the property.

Tactic: use t or exact ⟨t, proof⟩

To prove something exists, you must produce it. The use tactic lets you supply a specific witness, then the goal changes to proving the property holds for that witness.

To use an existential hypothesis, obtain ⟨x, hx⟩ := h gives you the witness and its proof.

Watch the strategy in action

The rule

Goal shape:  ∃ x, P(x)
Action:      use t
Effect:      Goal becomes P(t) — prove the property for your witness
Think:       "I claim t works. Now I prove it."

Hypothesis:  h : ∃ x, P(x)
Action:      obtain ⟨x, hx⟩ := h
Effect:      x : T and hx : P(x) appear in context
Think:       "Name the thing that exists and its proof."

Your turn

Prove that there exists a natural number greater than 100.

theorem exists_big : ∃ n : Nat, n > 100 := by
  sorry

Hint

Use use 101. Then prove 101 > 100.

Solution

theorem exists_big : ∃ n : Nat, n > 100 := by
  use 101
  omega

← Induction Rewriting →