# 2.14 Proof by Contradiction

Proof by contradiction is a classical proof pattern. To prove a proposition `P`, assume `¬ P`, derive `False`, and conclude `P`.

In Lean, this is usually written with `by_contra`.

## Problem

You want to prove:

```lean
P
```

but the easiest route is to show that assuming `¬ P` creates a contradiction.

## Solution

Use `by_contra`.

```lean
open Classical

theorem by_contra_basic
    (P : Prop)
    (h : ¬ P -> False) :
    P := by
  by_contra hnp
  exact h hnp
```

After:

```lean
by_contra hnp
```

Lean changes the proof state from:

```lean
⊢ P
```

to:

```lean
hnp : ¬ P
⊢ False
```

You then prove contradiction.

## Discussion

Constructively, proving `¬ P -> False` gives `¬ ¬ P`. It does not generally give `P`. The step from `¬ ¬ P` to `P` is classical.

This is why the proof begins with:

```lean
open Classical
```

The tactic `by_contra` uses classical reasoning unless the target already has a decidable structure that supports the argument.

## Direct Double Negation Form

Proof by contradiction is the same as double negation elimination.

```lean
open Classical

theorem by_contra_as_double_negation
    (P : Prop) :
    ¬ ¬ P -> P := by
  intro hnnp
  by_contra hnp
  exact hnnp hnp
```

Here:

```lean
hnnp : ¬ ¬ P
hnp  : ¬ P
⊢ False
```

The expression `hnnp hnp` produces `False`.

## Example with Equality

A common use is proving an equality by ruling out its negation.

```lean
open Classical

theorem equality_by_contradiction
    (a b : Nat)
    (h : ¬ a ≠ b) :
    a = b := by
  by_contra hne
  exact h hne
```

Since:

```lean
a ≠ b
```

means:

```lean
¬ (a = b)
```

the hypothesis `h : ¬ a ≠ b` says that inequality is impossible. Assuming `hne : a ≠ b` gives contradiction.

## Example with Disjunction

Classically, if `P` is not false, then `P` holds.

```lean
open Classical

theorem not_not_left
    (P Q : Prop)
    (h : ¬ ¬ P) :
    P ∨ Q := by
  left
  by_contra hnp
  exact h hnp
```

The proof chooses the left side. The remaining goal is `P`. It then proves `P` by contradiction using `h : ¬ ¬ P`.

## Example with Existentials

A useful classical pattern is deriving existence from the impossibility of universal negation.

```lean
open Classical

theorem exists_by_contradiction
    (α : Type)
    (P : α -> Prop)
    (h : ¬ ∀ x : α, ¬ P x) :
    ∃ x : α, P x := by
  by_contra hne
  apply h
  intro x
  intro hpx
  apply hne
  use x
```

The proof assumes:

```lean
hne : ¬ ∃ x : α, P x
```

Then it proves:

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

For an arbitrary `x`, assume `hpx : P x`. Then `use x` proves `∃ x, P x`, contradicting `hne`.

## `by_contra` Names the Negated Goal

The hypothesis introduced by `by_contra` has the negation of the original goal.

```lean
open Classical

theorem by_contra_goal_shape
    (P Q : Prop)
    (h : ¬ (P ∧ Q)) :
    ¬ P ∨ ¬ Q := by
  by_contra hnot
  apply h
  constructor
  · by_contra hp
    apply hnot
    left
    exact hp
  · by_contra hq
    apply hnot
    right
    exact hq
```

This example shows why proof by contradiction can become hard to read when nested. Each `by_contra` introduces the negation of the current goal, which may itself be complex.

For many beginner proofs, prefer direct proofs by introducing assumptions and applying hypotheses. Use contradiction when the direct construction is awkward.

## `by_cases` vs `by_contra`

`by_cases` splits a proposition into two cases.

```lean
open Classical

theorem by_cases_example
    (P Q : Prop)
    (hpq : P -> Q)
    (hnpq : ¬ Q) :
    ¬ P := by
  intro hp
  exact hnpq (hpq hp)
```

A classical version could split on `P`:

```lean
open Classical

theorem by_cases_example_classical
    (P Q : Prop)
    (hpq : P -> Q)
    (hnq : ¬ Q) :
    ¬ P := by
  by_cases hp : P
  · intro _
    exact hnq (hpq hp)
  · exact hp
```

The direct constructive proof is shorter. This illustrates an important rule: do not use classical case splits when implication and negation already give a direct proof.

## `exfalso` Inside Proof by Contradiction

`by_contra` changes the goal to `False`. In the reverse situation, `exfalso` changes any goal to `False`.

```lean
open Classical

theorem by_contra_with_exfalso
    (P Q : Prop)
    (hp : P)
    (hnp : ¬ P) :
    Q := by
  exfalso
  exact hnp hp
```

Here proof by contradiction is unnecessary because `False` is already available. Use `exfalso` when you can directly derive contradiction from existing hypotheses.

## Term Form

The classical theorem behind `by_contra` can be used directly.

```lean
open Classical

theorem by_contra_term
    (P : Prop)
    (h : ¬ P -> False) :
    P :=
  Classical.byContradiction h
```

The argument to `Classical.byContradiction` is a function from `¬ P` to `False`.

## Avoiding Unnecessary Classical Reasoning

This theorem is constructive:

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

A proof by contradiction version would be longer and introduce an unnecessary classical dependency.

Use `by_contra` mainly when the target itself must be obtained from a double-negated form, or when a classical excluded-middle argument is natural.

## Common Patterns

To prove `P` by contradiction:

```lean
open Classical

by_contra hnp
```

Then prove:

```lean
⊢ False
```

To prove from double negation:

```lean
by_contra hnp
exact hnnp hnp
```

To prove an equality from not-inequality:

```lean
by_contra hne
exact h hne
```

To avoid contradiction when proving negation:

```lean
intro hp
```

then prove `False` directly.

## Common Pitfalls

Do not use `by_contra` to prove a negation unless you really need a classical argument. To prove `¬ P`, the direct constructive move is `intro hp`.

Do not forget `open Classical` when proving a nonconstructive theorem.

Do not let nested `by_contra` blocks obscure the proof state. Inspect the goal after each use.

Do not use proof by contradiction when `exfalso` is enough. If contradiction is already derivable from existing hypotheses, prove `False` directly.

## Takeaway

Proof by contradiction proves `P` by assuming `¬ P` and deriving `False`. In Lean, `by_contra h` names the assumed negation and changes the goal to `False`. This is a classical pattern, useful for double negation elimination, excluded-middle arguments, and proofs where a direct witness or construction is unavailable.