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.

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

After intro h, the context is:

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:

False -> P

for any proposition P.

Lean provides this principle directly as False.elim.

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.

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:

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.

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

Before exfalso, the goal is:

⊢ Q

After exfalso, the goal is:

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

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:

hp : P
hnp : ¬ P

and:

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.

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

The target 0 ≠ 1 means:

¬ (0 = 1)

After intro h, the context is:

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:

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.

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:

hf : False
⊢ P

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

hp : P
⊢ P

so exact hp closes the goal.

The dual theorem is similar:

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.

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

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

P ∧ ¬ P -> False

After intro h, the context contains:

h.left  : P
h.right : ¬ P

Applying h.right to h.left gives False.

A version with explicit case analysis is:

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:

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.

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:

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:

h : False
⊢ Q

can be closed immediately by:

cases h

But:

hnp : ¬ P
⊢ Q

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

For example:

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:

cases h

or:

exact False.elim h

To turn a contradiction into the current goal:

exfalso

then prove False.

To use incompatible hypotheses:

have hf : False := hnp hp
cases hf

or directly:

exact False.elim (hnp hp)

To let Lean search for a direct contradiction:

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.