# Zulip Chat Archive

## Stream: new members

### Topic: Double Negation and Proof by Contradiction

#### Dan Knight (Apr 26 2020 at 03:34):

Hi All - I've done a little bit of formal mathematics in uni and have started with the publicly available "Logic and Proof" course using Lean. I'm looking for some help with proofs that prove the negation of a proposition (-A) by contradiction.

My problem arises as the type checker expects the negation of the already negated proposition (--A) to lead to false, rather than just the proposition (A) itself. If I use the have keyword to prove A from --A, my text then type checks to ... -> A -> -A and fails given this extra step (pseudo example at the bottom).

Is there a way around this double negation problem? I've tried rewriting the proofs but can't seem to do quite a few of the exercises without something of this form. Any all help would be greatly appreciated it. Moreover, apologize for the noob question, this has been quite the humbling evening/afternoon

-Example-

(assume hNNA : \not \not A,

have hA : A, from ...

show false, h? hA)

-Error-

type mismatch at application

A→ false

but is expected to have type

¬¬A → false

#### Shing Tak Lam (Apr 26 2020 at 03:38):

There is `theorem not_not [decidable a] : ¬¬a ↔ a`

, which might be useful. Although it may be helpful if you post example code?

#### Donald Sebastian Leung (Apr 26 2020 at 04:37):

To add to this: use triple backticks to get formatted code, e.g.

```lean example : 1 + 1 = 2 := rfl ```

#### Shing Tak Lam (Apr 26 2020 at 04:40):

Donald Sebastian Leung said:

To add to this: use triple backticks to get formatted code, e.g.

```lean example : 1 + 1 = 2 := rfl ```

(You don't need the `lean`

part anymore since this update, the default here is that three backticks is Lean, and you need to explicitly state when it is monospace text with `text`

. Obviously using `lean`

won't break anything)

#### Dan Knight (Apr 26 2020 at 20:18):

Shing Tak Lam said:

There is

`theorem not_not [decidable a] : ¬¬a ↔ a`

, which might be useful. Although it may be helpful if you post example code?

Thanks Shing I appreciate the thought! That theorem helped and I was able to debug it! Thank you!

Last updated: May 13 2021 at 05:21 UTC