More homework help

Stream: new members

[Jeremy Teitelbaum]

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]

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]

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]

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

[Yury G. Kudryashov]

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

[Johan Commelin]

#backticks -- so that the hyperlink works

[Eric Rodriguez]

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]

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]

have foo := hpqr hp

[Stuart Presnell]

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

Solution

theorem t₈ : (p → (q ∨ r)) → ((p → q) ∨ (p → r)) :=
begin
intro hpqr,
by_cases hp : p,
{ cases hpqr hp,
{ left, intro, assumption },
{ right, intro, assumption } },
{ left, intro, contradiction },
end

[Bryan Gin-ge Chen]

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]

@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]

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

[Kevin Buzzard]

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)