Zulip Chat Archive

Stream: new members

Topic: More homework help


Jeremy Teitelbaum (Dec 11 2021 at 12:21):

I had never appreciated the significance of classical logic before trying lean. I am totally stuck on proving
‘’’
(P \to (q\or r))\to ((p\to q)\or (p\to r))
‘’’
Any hints?

Eric Rodriguez (Dec 11 2021 at 12:26):

I don't know where the link is, but a really good way to solve these sorts of thing is "the hole method", which I think @Bryan Gin-ge Chen made a post about (sorry for the tag if not!). The idea is kind of just to intro and split as much as possible, and then see what are the only things that can fit.

Yury G. Kudryashov (Dec 11 2021 at 12:46):

You should use triple #backtics, not a mix of ` and '. And it's probably better to copy the actual code with unicode symbols. Then it looks like

(P  (q  r))  ((p  q)  (p  r))

Yury G. Kudryashov (Dec 11 2021 at 12:47):

I'm not sure that this implication is true without classical logic.

Yury G. Kudryashov (Dec 11 2021 at 12:53):

If you're allowed to use classical logic, then I suggest starting with by_cases p.

Johan Commelin (Dec 11 2021 at 12:55):

#backticks -- so that the hyperlink works

Eric Rodriguez (Dec 11 2021 at 13:03):

itauto fails on it, so it seems it does need classical (or I guess if you're trying to be as non-classical as possible decidable p)

Jeremy Teitelbaum (Dec 11 2021 at 15:53):

Since this is driving me crazy, I will ask more explicitly. I have

import tactic
variables  p q r s : Prop
open classical

theorem t₈  : (p  (q  r))  ((p  q)  (p  r)) :=
begin
intro hpqr,
by_cases r,
right,
intro hp,
assumption,
left,
intro hp,
 -- now what?
sorry,
 end

At this point I have

pqr: Prop
hpqr: p  q  r
h: ¬r
hp: p
 q

and it seems like I should be able to deduce q (since I have p, so I have q \or r and \not r but I can't untangle it.

Johan Commelin (Dec 11 2021 at 15:55):

have foo := hpqr hp

Stuart Presnell (Dec 11 2021 at 16:02):

But if you're using by_cases, why not use by_cases p?

Solution

Bryan Gin-ge Chen (Dec 11 2021 at 16:04):

Eric Rodriguez said:

I don't know where the link is, but a really good way to solve these sorts of thing is "the hole method", which I think Bryan Gin-ge Chen made a post about (sorry for the tag if not!). The idea is kind of just to intro and split as much as possible, and then see what are the only things that can fit.

I don't know if I did any examples that require classical logic, but here's one post showing off the technique (searching for "chasing underscores" might pull up a few others).

Kevin Buzzard (Dec 11 2021 at 16:10):

@Jeremy Teitelbaum constructive logic is totally weird, things like de Morgan's laws aren't all true (some are, some aren't). intro, apply, exact, split etc are all constructive mathematics; by_cases is classical (it's the law of the excluded middle).

Kevin Buzzard (Dec 11 2021 at 16:10):

@Stuart Presnell you can quote code in spoilers but you have to use 4 backticks IIRC

Kevin Buzzard (Dec 11 2021 at 16:12):

If you're happy to use by_cases then you can just solve all of these by doing cases on all the variables; this is the same as drawing a truth table (exactly the proof you're not allowed to do in constructive maths)


Last updated: Dec 20 2023 at 11:08 UTC