Zulip Chat Archive

Stream: general

Topic: prroblem- exercise-3.7.2-1


Jagadish Bapanapally (Jun 16 2021 at 17:39):

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 (Jun 16 2021 at 17:39):

Can you please reformat using #backticks?

Jagadish Bapanapally (Jun 16 2021 at 17:41):

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 (Jun 16 2021 at 17:42):

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

Yaël Dillies (Jun 16 2021 at 17:42):

And you can edit your messages.

Jagadish Bapanapally (Jun 16 2021 at 17:43):

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 (Jun 16 2021 at 17:49):

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

Jagadish Bapanapally (Jun 16 2021 at 17:55):

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

Thomas Browning (Jun 16 2021 at 17:56):

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

Jagadish Bapanapally (Jun 16 2021 at 17:59):

this one is throwing error:

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

Thomas Browning (Jun 16 2021 at 18:00):

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

Thomas Browning (Jun 16 2021 at 18:00):

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

Jagadish Bapanapally (Jun 16 2021 at 19:08):

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 (Jun 16 2021 at 19:10):

left (or, right!)

Jagadish Bapanapally (Jun 16 2021 at 19:20):

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 (Jun 16 2021 at 19:31):

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

Jagadish Bapanapally (Jun 16 2021 at 19:33):

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 (Jun 16 2021 at 19:38):

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

Jagadish Bapanapally (Jun 16 2021 at 19:44):

Thank you!

Kevin Buzzard (Jun 16 2021 at 19:48):

If you use mathlib then

import tactic

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

Last updated: Dec 20 2023 at 11:08 UTC