2.16 Introduction and Elimination Rules

Every logical connective in Lean has two sides. An introduction rule explains how to prove the connective. An elimination rule explains how to use a proof of the connective. Most beginner proof failures come from applying the wrong side of this distinction.

Problem

You want a mechanical method for deciding what to do next from the shape of the goal or the shape of a hypothesis.

If the connective appears in the goal, use its introduction rule. If the connective appears in the local context, use its elimination rule.

Solution

Read the proof state in two directions.

When the goal is:

⊢ P ∧ Q

you introduce conjunction by proving both sides:

constructor

When the context contains:

h : P ∧ Q

you eliminate conjunction by extracting its fields:

h.left
h.right

The same pattern applies to implication, disjunction, negation, equality, existential quantifiers, and universal quantifiers.

Implication

To introduce an implication, assume its premise.

theorem imp_intro
    (P Q : Prop) :
    (P -> Q) -> (P -> Q) := by
  intro h
  exact h

A more direct example:

theorem imp_intro_direct
    (P Q : Prop)
    (h : P -> Q) :
    P -> Q := by
  intro hp
  exact h hp

The introduction rule for P -> Q is:

assume P, then prove Q

To eliminate an implication, apply it to a proof of its premise.

theorem imp_elim
    (P Q : Prop)
    (h : P -> Q)
    (hp : P) :
    Q := by
  exact h hp

This is ordinary function application.

Conjunction

To introduce a conjunction, prove both components.

theorem and_intro
    (P Q : Prop)
    (hp : P)
    (hq : Q) :
    P ∧ Q := by
  constructor
  · exact hp
  · exact hq

To eliminate a conjunction, project either component.

theorem and_elim_left
    (P Q : Prop)
    (h : P ∧ Q) :
    P := by
  exact h.left

theorem and_elim_right
    (P Q : Prop)
    (h : P ∧ Q) :
    Q := by
  exact h.right

You may also eliminate by case analysis:

theorem and_elim_cases
    (P Q R : Prop)
    (h : P ∧ Q)
    (f : P -> Q -> R) :
    R := by
  cases h with
  | intro hp hq =>
    exact f hp hq

Disjunction

To introduce a disjunction, choose one side.

theorem or_intro_left
    (P Q : Prop)
    (hp : P) :
    P ∨ Q := by
  left
  exact hp

theorem or_intro_right
    (P Q : Prop)
    (hq : Q) :
    P ∨ Q := by
  right
  exact hq

To eliminate a disjunction, handle both cases.

theorem or_elim
    (P Q R : Prop)
    (h : P ∨ Q)
    (hp : P -> R)
    (hq : Q -> R) :
    R := by
  cases h with
  | inl hp_proof =>
    exact hp hp_proof
  | inr hq_proof =>
    exact hq hq_proof

A disjunction is weak when introducing and strong only after both cases are handled.

Negation

Negation is implication into False.

¬ P

means:

P -> False

To introduce a negation, assume the proposition and derive False.

theorem not_intro
    (P Q : Prop)
    (h : P -> Q)
    (hnq : ¬ Q) :
    ¬ P := by
  intro hp
  exact hnq (h hp)

To eliminate a negation, apply it to a proof of the proposition it denies.

theorem not_elim
    (P R : Prop)
    (hnp : ¬ P)
    (hp : P) :
    R := by
  have hf : False := hnp hp
  cases hf

The direct form is:

theorem not_elim_direct
    (P R : Prop)
    (hnp : ¬ P)
    (hp : P) :
    R := by
  exact False.elim (hnp hp)

False

False has no introduction rule in ordinary consistent reasoning. You can prove False only from contradictory assumptions.

To eliminate False, perform case analysis on it.

theorem false_elim
    (P : Prop)
    (h : False) :
    P := by
  cases h

The absence of constructors is exactly why this works.

True

True has a trivial introduction rule.

theorem true_intro : True := by
  trivial

Eliminating True gives no useful information.

theorem true_elim_no_information
    (P : Prop)
    (h : True)
    (hp : P) :
    P := by
  cases h
  exact hp

Case analysis on True creates one branch and no useful data.

Equality

To introduce equality, use reflexivity when both sides are definitionally equal.

theorem eq_intro
    (a : Nat) :
    a = a := by
  rfl

To eliminate equality, rewrite.

theorem eq_elim
    (a b : Nat)
    (h : a = b) :
    a + 1 = b + 1 := by
  rw [h]

In dependent situations, equality elimination transports a proof across equal terms.

theorem eq_transport
    (a b : Nat)
    (P : Nat -> Prop)
    (h : a = b)
    (hp : P a) :
    P b := by
  rw [← h]
  exact hp

The goal P b is rewritten back to P a, where hp applies.

Existential Quantifier

To introduce an existential, provide a witness.

theorem exists_intro
    (P : Nat -> Prop)
    (a : Nat)
    (ha : P a) :
    ∃ x : Nat, P x := by
  use a
  exact ha

To eliminate an existential, unpack its witness and proof.

theorem exists_elim
    (P : Nat -> Prop)
    (R : Prop)
    (h : ∃ x : Nat, P x)
    (f : ∀ x : Nat, P x -> R) :
    R := by
  rcases h with ⟨x, hx⟩
  exact f x hx

The witness becomes a local variable, and the property proof becomes a local hypothesis.

Universal Quantifier

To introduce a universal statement, introduce an arbitrary variable.

theorem forall_intro
    (α : Type)
    (P : α -> Prop) :
    (∀ x : α, P x) -> (∀ y : α, P y) := by
  intro h
  intro y
  exact h y

To eliminate a universal statement, apply it to a specific value.

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

Universal elimination is function application.

Combining Rules

Most proofs combine introduction and elimination rules.

theorem combined_example
    (P Q R : Prop) :
    (P ∧ Q -> R) -> P -> Q -> R := by
  intro hpqr
  intro hp
  intro hq
  apply hpqr
  constructor
  · exact hp
  · exact hq

The proof reads as follows. To prove an implication, introduce assumptions. To use hpqr : P ∧ Q -> R, apply it. This changes the goal to P ∧ Q. To prove the conjunction, construct both parts.

Another example:

theorem combined_or_example
    (P Q R : Prop) :
    (P -> R) -> (Q -> R) -> P ∨ Q -> R := by
  intro hpr
  intro hqr
  intro hpq
  cases hpq with
  | inl hp =>
    exact hpr hp
  | inr hq =>
    exact hqr hq

Here disjunction is eliminated by two branches, and implication is eliminated by function application in each branch.

Goal Shape Table

Hypothesis Shape Table

Common Patterns

When stuck, inspect the goal first. If the top-level symbol is a connective, use its introduction rule.

When the goal has no obvious top-level connective, inspect the hypotheses. If one hypothesis has a connective, use its elimination rule.

When both apply, prefer the move that exposes useful information without creating unnecessary subgoals.

Common Pitfalls

Do not try to eliminate a connective that appears only in the goal. First introduce it.

Do not try to introduce a connective that appears only in a hypothesis. Use or destruct the hypothesis.

Do not split a disjunction goal unless you know which side you can prove.

Do not split a disjunction hypothesis incompletely. Both branches must be handled.

Do not use classical reasoning when an introduction or elimination rule gives a direct constructive proof.

Takeaway

Introduction rules build logical statements. Elimination rules use logical statements. In Lean, the next proof step is usually determined by whether a connective appears in the goal or in the context. This discipline turns proof construction into a local, mechanical process.