Zulip Chat Archive

Stream: new members

Topic: Double Negation and Proof by Contradiction


view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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
```

view this post on Zulip 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)

view this post on Zulip 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