Double Negation and Proof by Contradiction

Stream: new members

[Dan Knight]

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]

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]

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

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

[Shing Tak Lam]

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]

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!