# Zulip Chat Archive

## Stream: general

### Topic: Proving false vs double negation

#### Dominic Farolino (Feb 10 2019 at 08:12):

Hey, I originally posted the question here (https://github.com/leanprover/lean/issues/1993#issuecomment-462112225) if reading it there wouldn’t be too much trouble. The question basically revolves around why two nearly identical proofs of false are interpreted differently in Lean. One proof shows false and results in a negation, then other results in a double negation. The natural deduction for each are both very similar, however the Lean proofs must vary in where the assumptions are placed for it to be valid, which I don’t understand.

#### Mario Carneiro (Feb 10 2019 at 08:14):

This example:

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

is almost correct, but the type of the `show`

is wrong - it should be `show false, from h2 h1`

#### Mario Carneiro (Feb 10 2019 at 08:15):

`show`

will assert the type of the thing you are about to write. I can insert a bunch more shows to see how the `assume`

lines change things:

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

#### Mario Carneiro (Feb 10 2019 at 08:17):

This reflects how the first line above an ->I rule is the consequent of the implication, without mentioning the LHS which has gone into an assumption

#### Dominic Farolino (Feb 10 2019 at 08:33):

Ahh ok so that makes it more clear how it can be broken down. So the only reason we can say show not not B, from assume h2: not B, is because of the line after it then? I think that makes more sense to me now

#### Kevin Buzzard (Feb 10 2019 at 10:02):

`show X`

means "the goal is X", not " I can show X"

#### Dominic Farolino (Feb 10 2019 at 16:57):

Sure, but the only reason we can show ¬¬B from ¬B, is if we show false right after, using ¬B (so that we can negate ¬B to get ¬¬B), right? If that is the case, why does it matter where I assume h2 : ¬B? For example, in the following

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

I assume the negation of the RHS right away, and I don't have to write:

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

(which is actually invalid which slightly confuses me)

#### Chris Hughes (Feb 10 2019 at 16:59):

You write `show false`

when Lean was expecting a proof of `¬B`

#### Patrick Massot (Feb 10 2019 at 17:01):

What are you trying to explain with that trivial example? You could write

example : ¬ B → ¬ B := assume h1 : ¬ B, h1

#### Patrick Massot (Feb 10 2019 at 17:01):

Or, the sober version: `example : ¬ B → ¬ B := id`

#### Dominic Farolino (Feb 10 2019 at 17:03):

Well, I guess I'm just confused with the positioning of `assume`

, with regards to `show`

. In the first example of my previous message,```
assume h2: B,
show false, from h1 h2
```

is valid, but `show false, from assume h2: B, h1 h2`

is not; in both, I assume `h2: B`

, just in different places

#### Patrick Massot (Feb 10 2019 at 17:16):

Do you know how to use `_`

in order to write proof terms?

#### Patrick Massot (Feb 10 2019 at 17:17):

For instance, you can write:

example : ¬ B -> ¬ B := assume h1 : ¬ B, _

Lean will give an error message describing what was the state and what it was waiting for when you left that `_`

hole

#### Patrick Massot (Feb 10 2019 at 17:18):

You could also first try to learn tactic mode where you see everything.

#### Dominic Farolino (Feb 10 2019 at 17:36):

Sure, but this seems to error out early:

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

...not telling me why I can do:

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

...but not:

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

...I assume the answer is in Mario's statement "This reflects how the first line above an ->I rule is the consequent of the implication, without mentioning the LHS which has gone into an assumption", but I'm trying to figure out what exactly it means. Sorry, very new to lean and stuff.

#### Kevin Buzzard (Feb 10 2019 at 17:36):

Yes, the `_`

trick is really good for working out what Lean is expecting next. There is a well defined logic and syntax for everything here but it takes some getting used to. I found tactic mode much easier when learning Lean, but I have a maths not a CS background

#### Rob Lewis (Feb 10 2019 at 17:39):

If you write

example : ¬ B -> ¬ B := assume h1 : ¬ B, _

You'll see that the current goal is `¬ B`

. Writing `show false, from ...`

is telling Lean that what follows is a proof of `false`

. But Lean is expecting a proof of `¬ B`

.

#### Rob Lewis (Feb 10 2019 at 17:40):

`assume h2: B, h1 h2`

is not a proof of `false`

. It's a proof of `B -> false`

. That's what the `assume`

is doing.

#### Dominic Farolino (Feb 10 2019 at 18:34):

Ok thanks, it makes sense that `show false, from ...`

is of course a proof of `false`

, while lean is looking for `¬ B`

. So I guess this works because if if I assume `h2: B`

directly after `h1`

, and proceed to show `false`

, it becomes a proof of `¬ B`

, which is what I needed originally. Ah the ordering of assumes/shows makes more sense now :) I see how this relates to my earlier double-negation question. Thanks so much!

#### Kevin Buzzard (Feb 10 2019 at 18:41):

You shouldn't think that "assume X, ..." is somehow putting the assumption X into some database for later use and isn't doing anything else. All these things have well-defined semantics and at the end of the day you're just writing a function. At any stage in the process there is a "goal". If the goal is "X -> Y" then "assume X, " assumes X but also changes the goal to Y. If you work in tactic mode then you can see the tactic state at all times, which is all the assumptions *and the goal*, and this is what makes it so much easier to understand.

#### Kevin Buzzard (Feb 10 2019 at 18:42):

http://wwwf.imperial.ac.uk/~buzzard/xena/html/source/M1F_introduction/prop_exercises.html are some notes I wrote on doing basic logic in tactic mode.

#### Kevin Buzzard (Feb 10 2019 at 18:44):

On the other hand, I know that people with a more CS background seem to prefer term mode. The exercise in Theorem Proving In Lean seem to go down well for those people -- that book does not introduce tactic mode until chapter 5 and it does a bunch of stuff using all this "assume/show" technique before that.

#### Dominic Farolino (Feb 11 2019 at 02:48):

Thank you, that explanation makes sense, it was clear that the placement of `assume`

s was not arbitrary, but I could not quite see what the rationale always was, but that goal-based explanation helps a lot. Will also check out the notes you wrote, seems very helpful I appreciate it!

#### Dominic Farolino (Feb 11 2019 at 02:49):

Btw, with regards to the book, is there any known repository of chapter exercise solutions? For ones I'm stuck on, I think it would be helpful to see the right way to frame things sometimes

#### Mario Carneiro (Feb 11 2019 at 02:51):

I don't think there is a full solution manual, but if you post individual problems here I'm sure people will solve them before you can say "no wait"

#### Dominic Farolino (Feb 11 2019 at 02:51):

Cool, thanks for the tip, and all of the help

Last updated: May 08 2021 at 03:17 UTC