dne in book

Stream: new members

[Dave]

Hello! In section 3.5 of the github book the second code snippet says:

theorem dne {p : Prop} (h : ¬¬p) : p :=
or.elim (em p)
  (assume hp : p, hp)
  (assume hnp : ¬p, absurd hnp h)

If you hit "try it!" and delete the (assume hp:p, hp) line it complains. How is hp:p, hp used? Isn't it enough to just assume hnp and h?

[Chris Hughes]

The first line splits the proof up into two cases, the case when p is true, and the case when ¬p is true. You have to prove both. It will therefore expect two proofs as arguments, one of p -> p, and also a proof of ¬p -> p. The second line is a proof of p -> p, and the final line is the proof that ¬p -> p.

You can only assume hp : p if you're trying to prove a goal of the form p -> something

[Marc Huisinga]

it complains because or.elim requires you to provide two functions/proofs, one for the left side of the or, one for the right side of the or.
say you want to prove a proposition p, and you're given a ∨ b. then you need to provide two proofs, a → p and b → p.
in your example, you want to prove p, by eliminating the disjunction em p = p ∨ ¬p.
one of these cases is trivial (the first one), and the second one requires you to use your assumption hnp.

[Kevin Buzzard]

People wouldn't ask this sort of question if tactic mode were introduced first.

theorem dne {p : Prop} (h : ¬¬p) : p :=
begin
  apply or.elim (em p),
  -- note that there are now two goals
  { sorry},
  { sorry}
end

[Kevin Buzzard]

@Dave can look forward to chapter 5, when easy mode is unlocked :-)

[Dave]

This clears it up quite well, thank you! Would cases be useful here then? Clearly it's not necessary, but maybe to guide the eye.

[Marc Huisinga]

personally, i really liked that term mode was introduced first, because it was easier to see what was going on. that being said, my background is cs, so having seen the lambda calculus before reading the book might have influenced that perception ;)

[Kevin Buzzard]

Yes, it seems to me that it's often the mathematicians who appreciate tactic mode first and the computer scientists who appreciate term mode first.

[Dave]

People wouldn't ask this sort of question if tactic mode were introduced first.

theorem dne {p : Prop} (h : ¬¬p) : p :=
begin
  apply or.elim (em p),
  -- note that there are now two goals
  { sorry},
  { sorry}
end

Easy mode! Ok now I want to skip ahead!

[Kevin Buzzard]

I wrote a huge amount of tactic mode code before I started venturing into term mode.

[Kevin Buzzard]

Easy-if-you-dont-know-any-lambda-calculus-stuff mode. At all stages Lean displays exactly what you're trying to prove and what all your assumptions are.

[Kevin Buzzard]

If you have the right Lean messages buffer open (ctrl-shift-enter) then you can click around the proof and see what state it's in at all times.

[Dave]

Easy-if-you-dont-know-any-lambda-calculus-stuff mode. At all stages Lean displays exactly what you're trying to prove and what all your assumptions are.

I don't really know lambda calculus stuff, but the first part of the book had a nice exposition. Still, tactics sounds like magic so I am even more interested now!

[Kevin Buzzard]

I read through the book once, and then I read through it again and the second time I found chapter 3 very frustrating because I wanted to do everything in tactic mode by that point.

[Kevin Buzzard]

http://wwwf.imperial.ac.uk/~buzzard/xena/html/source/M1F_introduction/prop_exercises.html

[Kevin Buzzard]

One day I'll write "TPIL for mathematicians". Until then, there are some super-scrappy notes.

[Marc Huisinga]

@Dave right after the or.elim em example, the by_cases function is introduced, which represents the "case analysis" notion in term mode

[Dave]

Dave right after the or.elim em example, the by_cases function is introduced, which represents the "case analysis" notion in term mode

Wow, ok... forgive me, I've read through it schizophrenically and have lost the sense in which those kinds of things are introduced.

[Dave]

One day I'll write "TPIL for mathematicians". Until then, there are some super-scrappy notes.

I just realized you're the Xena Project guy on twitter! I am glad you gave me that link because I didn't know where to find your M1F notes and I wanted to for the longest time!

[Marc Huisinga]

although further down in the book you'll learn that case analysis (over inductive types) in general is quite a powerful tool.

[Marc Huisinga]

i've also found the introduction of tactic mode in the book to be quite transparent, and not that magical at all (although some of the concrete tactics might still feel like magic).

@Dave i kind of felt like drowning in syntax at some points in the book, but if you do the exercises, you'll get used to everything

[Dave]

i've also found the introduction of tactic mode in the book to be quite transparent, and not that magic at all (although some of the concrete tactics might still feel like magic).

Dave i kind of felt like drowning in syntax at some points in the book, but if you do the exercises, you'll get used to everything

Ok this is very reassuring, thanks! I'm experiencing that feeling currently. Also I don't properly know where to start with the second exercise at the bottom of the chapter. How would I remove the negation if I can't use false.elim? I believe I'm thinking about this problem altogether in the wrong way (which is why I went back to this section).

[Marc Huisinga]

you can use false.elim!
as long you don't open classical, everything you're doing is constructive.

[Dave]

Oh I was under the wrong impression that false.elim was classical, lol. Thanks once more

[Kevin Buzzard]

You can do induction on any inductive type in Lean, it's pretty crazy. Induction on the natural numbers is normal induction, induction on false is false.elim. That function or.elim is induction on or.

[Kevin Buzzard]

I am glad you gave me that link because I didn't know where to find your M1F notes and I wanted to for the longest time!

When I get my act together all this will be very well signposted. I'm hoping that I will actually have some kind of coherent story for beginners by the end of July. An alternative introduction to Lean which undergraduate mathematicians might find more accessible than theorem proving in Lean (in the sense that it will get to maths more quickly).

[matt rice]

Hmm, this doesn't give e.g. the lean names for the natural deduction inference rules, e.g. or.elim matches the last disjunction rule there, but it's something I put into a pull request the other day taken from the logic & proof book, perhaps it might help? https://gist.github.com/ratmice/ee5b2d49f8a8c141ddbe9fde798eb4e1