prroblem- exercise-3.7.2-1

Stream: general

[Jagadish Bapanapally]

Hi,

I am trying to prove the below in tactic mode, and not with cc:

open classical

variables p q r s : Prop

example : (p → r ∨ s) → ((p → r) ∨ (p → s)) := sorry

I got to this point:

example : (p → r ∨ s) → ((p → r) ∨ (p → s)) :=
begin
intros prs,
left,
intro hp,
have hors := prs hp,
cases hors with hr hs,
exact hr,
have hors1 := prs hp,
end

Any help is appreciated. Thank you.

[Heather Macbeth]

Can you please reformat using #backticks?

[Jagadish Bapanapally]

example : (p → r ∨ s) → ((p → r) ∨ (p → s)) := begin intros prs, left, intro hp, have hors := prs hp, cases hors with hr hs, exact hr, have hors1 := prs hp, end

[Yaël Dillies]

Write three of them consecutive just before your code and three of them on the line just after :smile:

[Yaël Dillies]

And you can edit your messages.

[Jagadish Bapanapally]

I am trying to prove the below in tactic mode, and not with cc:

open classical

variables p q r s : Prop

example : (p → r ∨ s) → ((p → r) ∨ (p → s)) :=
begin
intros prs,
left,
intro hp,
have hors := prs hp,
cases hors with hr hs,
exact hr,
have hors1 := prs hp,
end

[Thomas Browning]

What's the math proof? Once you use left on the second line of the proof, you've lost

[Jagadish Bapanapally]

So, what's the next step after intros prs?

[Thomas Browning]

You might need to use classical logic (e.g., use the law of the excluded middle on p)

[Jagadish Bapanapally]

this one is throwing error:

example : (p → r ∨ s) → ((p → r) ∨ (p → s)) :=
begin
or.elim (em p)

[Thomas Browning]

or.elim (em p) is a Prop, not a tactic

[Thomas Browning]

you could do apply or.elim (em p) or cases em p

[Jagadish Bapanapally]

example : (p → r ∨ s) → ((p → r) ∨ (p → s)) :=
begin
intro prs,
apply or.elim (em p),
intro hp,
have hors := prs hp,
cases hors,
left,
intro hp1,
exact hors,
right,
intro hp1,
exact hors,
intro nhp,
end

what is the next step after intro nhp?

[Heather Macbeth]

left (or, right!)

[Jagadish Bapanapally]

Sorry, I did not understand that. After intro nhp, the goal I have is :
p r s : Prop,
prs : p → r ∨ s,
nhp : ¬p
⊢ (p → r) ∨ (p → s)

[Yaël Dillies]

Well use either of left and right. Both subsequent goals will be true because p is false!

[Jagadish Bapanapally]

Got it. Thanks. Below is the proof:

example : (p → r ∨ s) → ((p → r) ∨ (p → s)) :=
begin
intro prs,
apply or.elim (em p),
intro hp,
have hors := prs hp,
cases hors,
left,
intro hp1,
exact hors,
right,
intro hp1,
exact hors,
intro nhp,
left,
intro hp10,
contradiction,
end

[Yaël Dillies]

If you want to compare, here's the mathlib proof: imp_or_distrib

[Jagadish Bapanapally]

Thank you!

[Kevin Buzzard]

If you use mathlib then

import tactic

example (p r s : Prop) : (p → r ∨ s) → ((p → r) ∨ (p → s)) :=
begin
  tauto!
end