Proving false vs double negation

Stream: general

[Dominic Farolino]

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]

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]

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]

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]

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]

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

[Dominic Farolino]

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]

You write show false when Lean was expecting a proof of ¬B

[Patrick Massot]

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

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

[Patrick Massot]

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

[Dominic Farolino]

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]

Do you know how to use _ in order to write proof terms?

[Patrick Massot]

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]

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

[Dominic Farolino]

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]

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]

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]

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]

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]

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]

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]

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]

Thank you, that explanation makes sense, it was clear that the placement of assumes 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]

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]

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]

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