[Question]: Proving false vs proving double negation

domfarolino commented 5 years ago

Prerequisites

[X] Put an X between the brackets on this line if you have done all of the following:
- Checked that your issue isn't already filed.
  - Specifically, check out the wishlist, open RFCs, or feature requests.
- Reduced the issue to a self-contained, reproducible test case.

Description

First off, sorry for filing this bug. I imagine this isn't the best place to ask questions, however it appears the (unofficial?) IRC channel is not really active, and I didn't know where else to ask.

So I know that given how negation (illustrated in chapter 3) works, to prove not A, we need to prove false from A:

In lean, a stupid example might look like:

example : ¬ B -> ¬ B :=
  assume h1 : ¬ B,
  assume h2: B,
  show false, from h1 h2

Basically, we get to assume two things:

The LHS (¬ B)
The un-negated RHS (B)

...as long as we can prove false from one of the contributing assumptions, we can prove the original negation of the RHS (probably not the best explanation, but that is kind of how I see it). I was reading chapter 5 about proof by contradiction, and saw that we can prove some fancy things, with double negations, like A ↔ ¬ ¬ A, via proof by contradiction. We can proof this in two steps:

A → ¬ ¬ A, with intuitionistic logic
¬ ¬ A → A, with classical logic, via proof by contradiction.

The book illustrated the first direction of the proof as:

...I figured that since this looked incredibly similar to the first example above, we can assume two things:

The LHS (A)
The un-negated version of the RHS, (¬ A) (to try and prove the original RHS)

...to me it seems that by proving false, from these contributing assumptions, we get to prove the original negation of the RHS (¬ ¬ A) holds. The program I came up with is as follows:

example : B -> ¬¬ B :=
  assume h1 : B,
  assume h2: ¬B,
  show ¬¬B, from h2 h1

...however Lean doesn't seem to like this. The error basically says what I expect to be valid h2 h1 has type false, expected ¬¬ B. I don't really see why this wouldn't be valid though, since we are essentially using the pattern from the first (simpler) version. I guess the double negation breaks some assumption I made when learning Lean. The real confusion is that the following works (and is what the book uses in an example):

example : B -> ¬¬ B :=
  assume h1 : B,
  show ¬¬B, from assume h2: ¬B, h2 h1

...AFAICT, h2 h1 still evaluates to false, and there only seems to be a positional change between the programs. Could someone please explain why the second works while the first fails, when they seem nearly semantically identical?

Thank you!

Versions

3.4.2

digama0 commented 5 years ago

The best place to ask questions like this is the Zulip chat: https://leanprover.zulipchat.com/

domfarolino commented 5 years ago

Thank you for checking out the chat thread. Will close this and continue there.

leanprover / lean3