Zulip Chat Archive

Stream: general

Topic: Proving false vs double negation


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

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

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

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

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

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 10:02):

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

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

view this post on Zulip Chris Hughes (Feb 10 2019 at 16:59):

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

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

view this post on Zulip Patrick Massot (Feb 10 2019 at 17:01):

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

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

view this post on Zulip Patrick Massot (Feb 10 2019 at 17:16):

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

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

view this post on Zulip Patrick Massot (Feb 10 2019 at 17:18):

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

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

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

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

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

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

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

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

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

view this post on Zulip Dominic Farolino (Feb 11 2019 at 02:48):

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!

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

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

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