Home / Tracks / Proof Strategies / Contradiction

Strategy: Proof by contradiction

Pattern recognition

When you see: a goal of the form ¬P (negation)

Strategy: Assume P and derive False.

Tactic: intro h (because ¬P is really P → False)

In Lean 4, ¬P is defined as P → False. So proving a negation is just a special case of direct proof — you assume the thing you want to negate, and show it leads to False.

When you have both h : P and hn : ¬P (i.e., hn : P → False), applying hn to h gives you False. That's a contradiction.

Watch the strategy in action

The rule

Goal shape:  ¬P         (which is P → False)
Action:      intro h
Effect:      h : P appears in context, goal becomes False
Think:       "Assume P. Now I need a contradiction."

Having:      h : P  and  hn : ¬P
Action:      exact hn h
Effect:      Produces False. Contradiction closed.

Your turn

Prove double negation introduction: from P, derive ¬¬P.

theorem not_not_intro (P : Prop) (hp : P) : ¬¬P := by
  sorry

theorem not_not_intro (P : Prop) (hp : P) : ¬¬P := by
  intro hnp
  exact hnp hp

See also: Logic §06 — Negation | Proof Theory §08 — ¬-Intro