2.5 Negation

Negation represents “not”. In Lean, ¬ P means that a proof of P would lead to False. So a proof of ¬ P is a function from P to False.

¬ P

is notation for:

P -> False

Problem

You want to prove or use a statement of the form:

¬ P

To prove it, assume P and derive a contradiction. To use it, apply it to a proof of P to obtain False.

Solution

Use intro to assume the proposition being negated.

theorem not_intro_example (P : Prop) : P -> ¬ ¬ P := by
  intro hp
  intro hnp
  exact hnp hp

The theorem says: if P is true, then it is impossible for P to be false.

After the first intro, the context is:

hp : P
⊢ ¬ ¬ P

Since ¬ ¬ P means (P -> False) -> False, the second intro gives:

hp : P
hnp : ¬ P
⊢ False

Now hnp hp has type False, so the goal is solved.

Using a Negated Hypothesis

If you have:

hnp : ¬ P
hp : P

then:

hnp hp

is a proof of False.

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

Once False is available, any goal can be proved. The command cases hf closes the goal because False has no constructors.

The contradiction Tactic

Lean can often find a direct contradiction automatically.

theorem contradiction_tactic
    (P Q : Prop)
    (hnp : ¬ P)
    (hp : P) :
    Q := by
  contradiction

The tactic searches the local context for incompatible hypotheses, such as P and ¬ P.

For beginner proofs, it is useful to first write the explicit version:

have hf : False := hnp hp
cases hf

This shows the underlying proof.

Negation as a Function

Because ¬ P is P -> False, ordinary function application works.

theorem apply_negation
    (P : Prop) :
    ¬ P -> P -> False := by
  intro hnp
  intro hp
  exact hnp hp

The term form is even more direct:

theorem apply_negation_term
    (P : Prop) :
    ¬ P -> P -> False :=
  fun hnp hp => hnp hp

This proof is just function application.

Proving a Negation

To prove a negation, assume the proposition and reach False.

theorem not_and_not_right
    (P Q : Prop) :
    ¬ Q -> ¬ (P ∧ Q) := by
  intro hnq
  intro hpq
  exact hnq hpq.right

The goal ¬ (P ∧ Q) expands to:

P ∧ Q -> False

So intro hpq assumes a proof of P ∧ Q. From that proof, hpq.right : Q. Since hnq : ¬ Q, the expression hnq hpq.right produces False.

Negation and Disjunction

Negation is often used after case analysis.

theorem not_or_left
    (P Q : Prop) :
    ¬ (P ∨ Q) -> ¬ P := by
  intro hn_or
  intro hp
  apply hn_or
  left
  exact hp

The proof says: assume P. Then P ∨ Q follows by the left injection. But this contradicts hn_or : ¬ (P ∨ Q).

A similar proof gives the right side:

theorem not_or_right
    (P Q : Prop) :
    ¬ (P ∨ Q) -> ¬ Q := by
  intro hn_or
  intro hq
  apply hn_or
  right
  exact hq

Double Negation Introduction

Constructively, P implies ¬ ¬ P.

theorem double_negation_intro
    (P : Prop) :
    P -> ¬ ¬ P := by
  intro hp
  intro hnp
  exact hnp hp

This theorem is accepted without classical reasoning. A proof of P rules out the possibility that P leads to contradiction.

Double Negation Elimination

The converse direction, ¬ ¬ P -> P, is not constructively provable in general. It requires classical reasoning.

open Classical

theorem double_negation_elim
    (P : Prop) :
    ¬ ¬ P -> P := by
  intro hnnp
  by_cases hp : P
  · exact hp
  · exfalso
    exact hnnp hp

The command:

by_cases hp : P

splits the proof into two cases:

hp : P

and:

hp : ¬ P

In the first case, the goal is solved by hp. In the second case, hnnp hp gives False, and exfalso changes the goal to False.

The exfalso Tactic

The tactic exfalso replaces the current goal with False.

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

This works because from False, every proposition follows. Instead of proving Q directly, the proof proves that the assumptions are contradictory.

Negated Equality

Negation frequently appears with equality.

theorem not_equal_apply
    (a b : Nat)
    (hneq : a ≠ b)
    (heq : a = b) :
    False := by
  exact hneq heq

The notation:

a ≠ b

means:

¬ (a = b)

So hneq heq is again ordinary function application.

Common Patterns

To prove:

⊢ ¬ P

use:

intro hp

and then prove:

⊢ False

To use:

hnp : ¬ P
hp : P

write:

exact hnp hp

To prove any goal from a contradiction:

have hf : False := hnp hp
cases hf

or:

exfalso
exact hnp hp

Common Pitfalls

Do not treat ¬ P as a boolean value. It is a function from P to False.

Do not expect Lean to prove ¬ ¬ P -> P without classical reasoning. Constructively, double negation elimination is not available in general.

Do not forget that to prove a negation, the target after intro is False, not the opposite proposition.

Do not confuse P -> False with evidence that P is false in a computational sense. It is a proof that any assumed proof of P would produce contradiction.

Takeaway

Negation is implication into False. To prove ¬ P, assume P and derive contradiction. To use ¬ P, apply it to a proof of P. This explains intro, function application, exfalso, cases on False, and the basic structure of contradiction proofs.