# 2.6 False and Contradiction

`False` is the proposition with no constructors. It represents an impossible proof state. If the local context contains a proof of `False`, Lean can prove any proposition from it.

## Problem

You want to use an impossible hypothesis to finish a proof, or you want to show that a collection of assumptions is contradictory.

## Solution

Use `cases` on a proof of `False`.

```lean
theorem false_elim_example (P : Prop) : False -> P := by
  intro h
  cases h
```

After `intro h`, the context is:

```lean
h : False
⊢ P
```

The command `cases h` performs case analysis on `h`. Since `False` has no constructors, there are no cases to prove, so the goal is closed.

## Discussion

Every inductive type is used by considering its constructors. For example, a proof of `P ∧ Q` must have been built with the constructor for conjunction, so `cases` exposes its two parts. A proof of `False` could not have been built at all, because `False` has no constructors. Case analysis therefore leaves no remaining goals.

This rule is sometimes called explosion, or ex falso. In logical form, it says:

```lean
False -> P
```

for any proposition `P`.

Lean provides this principle directly as `False.elim`.

```lean
theorem false_elim_term (P : Prop) : False -> P :=
  fun h => False.elim h
```

The expression `False.elim h` has any proposition as its target type, because from `h : False` Lean may construct a proof of the current goal.

## Deriving `False` from Inconsistent Hypotheses

A common proof shape is to derive `False` from incompatible assumptions, then use that contradiction to prove the required goal.

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

Here `hnp : ¬ P` means `P -> False`. Applying `hnp` to `hp` gives `False`.

The proof can be written more directly:

```lean
theorem contradiction_from_p_and_not_p_direct
    (P Q : Prop)
    (hp : P)
    (hnp : ¬ P) :
    Q := by
  exact False.elim (hnp hp)
```

Both proofs construct the same logical object.

## The `exfalso` Tactic

The tactic `exfalso` changes the current goal to `False`.

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

Before `exfalso`, the goal is:

```lean
⊢ Q
```

After `exfalso`, the goal is:

```lean
⊢ False
```

This is valid because proving `False` is enough to prove any proposition.

## The `contradiction` Tactic

The tactic `contradiction` searches the local context for an immediate contradiction.

```lean
theorem contradiction_tactic_example
    (P Q : Prop)
    (hp : P)
    (hnp : ¬ P) :
    Q := by
  contradiction
```

This tactic is useful when the contradiction is direct. It can recognize patterns such as:

```lean
hp : P
hnp : ¬ P
```

and:

```lean
h : False
```

For instructional code, the explicit version is often better because it shows exactly where `False` comes from.

## Contradiction from Equalities

Contradictions also arise from impossible equalities.

```lean
theorem zero_not_one_example : 0 ≠ 1 := by
  intro h
  contradiction
```

The target `0 ≠ 1` means:

```lean
¬ (0 = 1)
```

After `intro h`, the context is:

```lean
h : 0 = 1
⊢ False
```

Lean knows that the constructors of natural numbers make `0 = 1` impossible, so `contradiction` closes the goal.

A more explicit proof uses `cases`:

```lean
theorem zero_not_one_cases : 0 ≠ 1 := by
  intro h
  cases h
```

Case analysis on an impossible equality between distinct constructors leaves no goals.

## Contradiction Inside Case Analysis

When a hypothesis is a disjunction, one branch may be contradictory and the other may contain the useful proof.

```lean
theorem false_or_elim (P : Prop) : False ∨ P -> P := by
  intro h
  cases h with
  | inl hf =>
    cases hf
  | inr hp =>
    exact hp
```

In the left branch, the context contains:

```lean
hf : False
⊢ P
```

so `cases hf` closes that branch. In the right branch, the context contains:

```lean
hp : P
⊢ P
```

so `exact hp` closes the goal.

The dual theorem is similar:

```lean
theorem or_false_elim (P : Prop) : P ∨ False -> P := by
  intro h
  cases h with
  | inl hp =>
    exact hp
  | inr hf =>
    cases hf
```

## Contradiction with Conjunction

A conjunction may contain incompatible parts.

```lean
theorem not_and_self_not
    (P Q : Prop) :
    ¬ (P ∧ ¬ P) := by
  intro h
  exact h.right h.left
```

The goal `¬ (P ∧ ¬ P)` expands to:

```lean
P ∧ ¬ P -> False
```

After `intro h`, the context contains:

```lean
h.left  : P
h.right : ¬ P
```

Applying `h.right` to `h.left` gives `False`.

A version with explicit case analysis is:

```lean
theorem not_and_self_not_cases
    (P Q : Prop) :
    ¬ (P ∧ ¬ P) := by
  intro h
  cases h with
  | intro hp hnp =>
    exact hnp hp
```

The parameter `Q` is unused here. It can be removed:

```lean
theorem not_and_self_not_clean
    (P : Prop) :
    ¬ (P ∧ ¬ P) := by
  intro h
  exact h.right h.left
```

## Contradiction as a Local Step

Sometimes you need to prove an intermediate contradiction while building a larger proof.

```lean
theorem contradiction_inside_proof
    (P Q R : Prop)
    (hp : P)
    (hnp : ¬ P) :
    Q ∧ R := by
  have hf : False := hnp hp
  constructor
  · cases hf
  · cases hf
```

This works, but it duplicates the use of `hf`. A cleaner version uses `exfalso` before splitting the conjunction:

```lean
theorem contradiction_before_constructor
    (P Q R : Prop)
    (hp : P)
    (hnp : ¬ P) :
    Q ∧ R := by
  exfalso
  exact hnp hp
```

Once the whole goal is replaced by `False`, no separate proof of `Q` or `R` is needed.

## `False` vs `¬ P`

The proposition `False` is an immediate contradiction. The proposition `¬ P` is a function waiting for a proof of `P`.

These are different contexts:

```lean
h : False
⊢ Q
```

can be closed immediately by:

```lean
cases h
```

But:

```lean
hnp : ¬ P
⊢ Q
```

cannot be closed unless you also have a proof of `P`, or some other way to derive `False`.

For example:

```lean
theorem not_alone_not_enough
    (P Q : Prop)
    (hnp : ¬ P)
    (hp : P) :
    Q := by
  exact False.elim (hnp hp)
```

The hypothesis `hnp` becomes useful only after it is applied to `hp`.

## Common Patterns

To prove anything from `False`:

```lean
cases h
```

or:

```lean
exact False.elim h
```

To turn a contradiction into the current goal:

```lean
exfalso
```

then prove `False`.

To use incompatible hypotheses:

```lean
have hf : False := hnp hp
cases hf
```

or directly:

```lean
exact False.elim (hnp hp)
```

To let Lean search for a direct contradiction:

```lean
contradiction
```

## Common Pitfalls

Do not use `cases h` on a negated hypothesis `h : ¬ P` unless the hypothesis itself has an inductive structure worth splitting. A negation is a function, so you normally apply it to a proof of `P`.

Do not split the target too early when a contradiction is already available. If you can prove `False`, use `exfalso` before creating multiple subgoals.

Do not rely on `contradiction` for nonlocal contradictions. If the contradiction requires several intermediate rewrites or applications, derive `False` explicitly.

## Takeaway

`False` is the empty proposition. A proof of `False` closes any goal because there are no cases to consider. Most contradiction proofs follow one pattern: derive `False` from incompatible hypotheses, then eliminate it with `cases`, `False.elim`, `exfalso`, or `contradiction`.