# 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`.

```lean
¬ P
```

is notation for:

```lean
P -> False
```

## Problem

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

```lean
¬ 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.

```lean
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:

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

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

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

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

## Using a Negated Hypothesis

If you have:

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

then:

```lean
hnp hp
```

is a proof of `False`.

```lean
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.

```lean
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:

```lean
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.

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

The term form is even more direct:

```lean
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`.

```lean
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:

```lean
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.

```lean
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:

```lean
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`.

```lean
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.

```lean
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:

```lean
by_cases hp : P
```

splits the proof into two cases:

```lean
hp : P
```

and:

```lean
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`.

```lean
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.

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

The notation:

```lean
a ≠ b
```

means:

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

So `hneq heq` is again ordinary function application.

## Common Patterns

To prove:

```lean
⊢ ¬ P
```

use:

```lean
intro hp
```

and then prove:

```lean
⊢ False
```

To use:

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

write:

```lean
exact hnp hp
```

To prove any goal from a contradiction:

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

or:

```lean
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.