Zulip Chat Archive

Stream: new members

Topic: Stuck on disjunction of a forall and something


Lars Ericson (Nov 26 2020 at 04:59):

I am doing exercises in Chapter 4 and I've got this one:

example : ( x, p x  r)  ( x, p x)  r :=
begin
  split,
  {
    intro h,
    left,
    assume x,
    have hpr := h x,
    cases hpr,
    exact hpr,
    have h2 := h x,
  },
  sorry,
end

Just after the have h2 := h x I am in goal state

α : Type u_1,
p : α  Prop,
r : Prop,
h :  (x : α), p x  r,
x : α,
hpr : r,
h2 : p x  r
 p x

At this point I don't have any reason to believe p x, I only know r. I got to this state reasonably though. The state is weak but not contradictory. If it was contradictory I could say exfalso and be done. So I've run out of ideas. Any hints would be greatly appreciated!

Antoine Labelle (Nov 26 2020 at 05:12):

I think you reached an impossible goal by doing left at the beginning. You will need left or right depending on the case for hpr.

Lars Ericson (Nov 26 2020 at 05:15):

@Antoine Labelle the problem is that right doesn't have any support either. right gives a goal of r but we don't have any way of proving r. Suppose I do right:

example : ( x, p x  r)  ( x, p x)  r :=
begin
  split,
  {
    intro h,
    right,
  },
  {

  },
end

then the goal state becomes

α : Type u_1,
p : α  Prop,
r : Prop,
h :  (x : α), p x  r
 r

and there is nothing there that will prove r.

Antoine Labelle (Nov 26 2020 at 05:19):

You can't do neither left or right before doing cases on your hypothesis, because which part of the disjunction in the goal is true will depend on which part of the disjunction in the hypothesis is true (for each x)

Antoine Labelle (Nov 26 2020 at 05:20):

Actually I think the simplest way to do this would be by cases on r

Lars Ericson (Nov 26 2020 at 05:32):

Thank you @Antoine Labelle that's a good point by_cases hr : r,.


Last updated: Dec 20 2023 at 11:08 UTC