what is unsolved `goals case h.inr` ?

Stream: new members

[rzeta0]

The following is an exercise from Heather MacBeth's course where the topic is introducing "or" in proofs:

example {x : ℝ} (hx : x ^ 2 - 3 * x + 2 = 0) : x = 1 ∨ x = 2 := by
  have h1 :=
    calc
    (x - 1) * (x - 2) = x ^ 2 - 3 * x + 2 := by ring
    _ = 0 := by rw [hx]
  have h2 := eq_zero_or_eq_zero_of_mul_eq_zero h1
  sorry

The following is my attempt to complete it:

example {x : ℝ} (hx : x ^ 2 - 3 * x + 2 = 0) : x = 1 ∨ x = 2 := by
  have h1 :=
    calc
    (x - 1) * (x - 2) = x ^ 2 - 3 * x + 2 := by ring
    _ = 0 := by rw [hx]
  have h2 := eq_zero_or_eq_zero_of_mul_eq_zero h1
  left
  obtain ha | hb := h2
  calc
    x = 1 := by addarith [ha]

However this seems to give an error / warning in the Infoview:

unsolved goals
case h.inr
x : ℝ
hx : x ^ 2 - 3 * x + 2 = 0
h1 : (x - 1) * (x - 2) = 0
hb : x - 2 = 0
⊢ x = 1

I don't understand what the error is telling me. My guess is it thinks I have to prove two goals not one?

The following is the reasoning behind my solution attempt:

• have gives us a disjunction x = 1 ∨ x = 2
• left signals we intend to solve the left x=1 which is sufficient
• I use obtain ha | hb := h2 to create ha : x - 1 = 0 which we'll need next
• the calc is then straightforward for obtaining the goal x=1 from ha using addarith (MacBeth's tactic) which is analogous to linarith

[Daniel Weber]

Because you have a disjunction, you can't choose to use one of the arguments. Instead obtain ha | hb := h2 splits the goal to two subgoals — one where you have the assumption ha : x - 1 = 0, and one where you have the assumption hb : x - 2 = 0. You have to solve both of them separately.
Note that using left before the obtain can't work, because before you know which of the possibilities in h2 is true you can't know which of the possibilities in the goal is true

[Eric Paul]

You are trying to prove x = 1 ∨ x = 2 and the current information you have is
h2 : x - 1 = 0 ∨ x - 2 = 0.

Notice that you don't know that x-1 = 0 and you don't know that x-2 = 0.
You only that one of those two has to be the case (aka x - 1 = 0 ∨ x - 2 = 0).

What you showed is that if you're in the first case, which is x-1=0, then you've proved the goal.
But what if you're in the second case?
You need to prove that in the second case the goal also follows and then you're done.
So in fact, you do have two goals and that is reflected by the notation ha | hb which gives a name to each goal created.

We can think about this more abstractly as well. If you are trying to prove C and you know A ∨ B,
then if you prove A → C and B → C, it follows that A ∨ B → C.

[rzeta0]

Eric - surely if you prove only A → C then you have proved A ∨ B → C ?

Here is another example that doesn't give an error:

example {x : ℝ} (hx : 2 * x + 1 = 5) : x = 1 ∨ x = 2 := by
  right
  calc
    x = (2 * x + 1 - 1) / 2 := by ring
    _ = (5 - 1) / 2 := by rw [hx]
    _ = 2 := by numbers

Here we've chosen to only prove the one of the clauses in the disjunction, that is x=2. This causes no error.

[Daniel Weber]

What you do here is prove A -> B and conclude A -> B or C, which is completely different (sorry for the lack of Unicode)

[Daniel Weber]

The other way is impossible, as False or True is true, so False or True -> False must be false, but False -> False is true

[Eric Paul]

Notice there is a critical difference between A ∨ B as a hypothesis versus A ∨ B as a goal.
If A ∨ B is a hypothesis, then you will have to handle two different cases.
If A ∨ B is a goal, then you just have to prove one of them.

Let A = "I own a cat" and B = "I own a dog".
I own a cat and do not own a dog (in other words, A is true and B is false).

So from the fact that I own a cat, it is true that "I own a cat or I own a dog", but it does not follow that "I own a dog".

Notice how in the first step I used A to show A ∨ B and that in the second step we saw that
just because A ∨ B is true, it does not follow that B is true.

[rzeta0]

thanks all for the replies - I think I am starting to understand. I will print this thread out and ponder it over a cup of tea (I am slow to learn)

[rzeta0]

Having printed out this thread, I can now see my error was logical, as explained above.

Here is my solution which seems to work. However i've never seen a lean program use both left and right - is this normal?

example {x : ℝ} (hx : x ^ 2 - 3 * x + 2 = 0) : x = 1 ∨ x = 2 := by
  have h1 :=
    calc
    (x - 1) * (x - 2) = x ^ 2 - 3 * x + 2 := by ring
    _ = 0 := by rw [hx]
  have h2 := eq_zero_or_eq_zero_of_mul_eq_zero h1
  obtain ha | hb := h2
  left
  calc
    x = x -1 + 1 := by ring
    _ = 0 + 1 := by rw [ha]
    _ = 1 := by numbers
  right
  calc
    x = x - 2 + 2 := by ring
    _ = 0 + 2 := by rw [hb]
    _ = 2 := by numbers

[Daniel Weber]

This may be clearer to you as a structured proof — the left and right appear on two distinct branches of the proof, and don't affect each other:

example {x : ℝ} (hx : x ^ 2 - 3 * x + 2 = 0) : x = 1 ∨ x = 2 := by
  have h1 :=
    calc
    (x - 1) * (x - 2) = x ^ 2 - 3 * x + 2 := by ring
    _ = 0 := by rw [hx]
  have h2 := eq_zero_or_eq_zero_of_mul_eq_zero h1
  obtain ha | hb := h2
  • left
    calc
      x = x -1 + 1 := by ring
      _ = 0 + 1 := by rw [ha]
      _ = 1 := by numbers
  • right
    calc
      x = x - 2 + 2 := by ring
      _ = 0 + 2 := by rw [hb]
      _ = 2 := by numbers

(I'm from the phone so • might be the wrong Unicode, you can type it with \.)

[rzeta0]

Thanks Daniel - what does the \. actually do? Is it purely decorative to aid readability but with no actual effect on the interpreted code?

(a quick internet search didn't help)

[Ruben Van de Velde]

It "focuses" on the current goal, so you need to solve it by the end of the block