# 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:

```lean
⊢ P ∧ Q
```

you introduce conjunction by proving both sides:

```lean
constructor
```

When the context contains:

```lean
h : P ∧ Q
```

you eliminate conjunction by extracting its fields:

```lean
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.

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

A more direct example:

```lean
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:

```lean
assume P, then prove Q
```

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

```lean
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.

```lean
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.

```lean
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:

```lean
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.

```lean
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.

```lean
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`.

```lean
¬ P
```

means:

```lean
P -> False
```

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

```lean
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.

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

The direct form is:

```lean
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.

```lean
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.

```lean
theorem true_intro : True := by
  trivial
```

Eliminating `True` gives no useful information.

```lean
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.

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

To eliminate equality, rewrite.

```lean
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.

```lean
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.

```lean
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.

```lean
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.

```lean
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.

```lean
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.

```lean
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:

```lean
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

| Goal shape | Introduction move |
| ---------- | ----------------- |
| `P -> Q`   | `intro hp`        |
| `P ∧ Q`    | `constructor`     |
| `P ∨ Q`    | `left` or `right` |
| `¬ P`      | `intro hp`        |
| `True`     | `trivial`         |
| `a = a`    | `rfl`             |
| `∃ x, P x` | `use a`           |
| `∀ x, P x` | `intro x`         |

## Hypothesis Shape Table

| Hypothesis shape | Elimination move           |
| ---------------- | -------------------------- |
| `h : P -> Q`     | apply `h` to `hp : P`      |
| `h : P ∧ Q`      | use `h.left` and `h.right` |
| `h : P ∨ Q`      | `cases h`                  |
| `h : ¬ P`        | apply `h` to `hp : P`      |
| `h : False`      | `cases h`                  |
| `h : a = b`      | `rw [h]`                   |
| `h : ∃ x, P x`   | `rcases h with ⟨x, hx⟩`    |
| `h : ∀ x, P x`   | apply `h` to a value       |

## 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.