scope of hypotheses from `obtain`

Stream: new members

[rzeta0]

This question is about the scope of hypotheses derived using obtain. Consider the following example proof.

-- 07 - Proof by Cases

import Mathlib.Tactic

example {x : ℤ} (h : x = 3 ∨ x = -3) : x^2 = 9 := by
  obtain ha | hb := h
  calc
    x^2 = (3)^2 := by rw [ha]
    _ = 9 := by norm_num
  calc
    x^2 = (-3)^2 := by rw [hb]
    _ = 9 := by norm_num

The Infoview shows 2 goals as follows:

case inl
x : ℤ
ha : x = 3
⊢ x ^ 2 = 9

case inr
x : ℤ
hb : x = -3
⊢ x ^ 2 = 9

What I noticed is that ha and hb are listed within a case.

I was going to assume that ha and hb can be referred to and used just like the hypotheses given in a proof header at any subsequent point in a proof.

This suggests the scope is within the case - in this case within the calc section only.

Is this correct? Is there a better mental model for thinking about these hypotheses created by obtain compared to say, have which I assume have full scope?

Should I even refer to the ha and hb from obtain as hypotheses? Is there a more official and mathematically correct term?

[Kyle Miller]

The ha and hb are hypotheses, but ha is a hypothesis in the first goal, and hb is a hypothesis in the second goal. They are two scopes.

Remember in another thread someone suggested using the dot for focusing on a goal? The accepted style is to focus on each goal one at a time to make the structure of the proof clear. For example, ha is accessible to the first calc just because that calc is applying to the first goal and it closes that goal.

By the way, the word "case" is sort of synonymous with "goal". Each goal can (optionally) have a case name. The word "case" is used to signify what the case name is.

[Kyle Miller]

With focusing dots:

example {x : ℤ} (h : x = 3 ∨ x = -3) : x^2 = 9 := by
  obtain ha | hb := h
  · calc
      x^2 = (3)^2 := by rw [ha]
      _ = 9 := by norm_num
  · calc
      x^2 = (-3)^2 := by rw [hb]
      _ = 9 := by norm_num

[Kyle Miller]

It's a wordier, but you might like the cases tactic, which enforces the proof structure and makes scopes more explicit.

example {x : ℤ} (h : x = 3 ∨ x = -3) : x^2 = 9 := by
  cases h with
  | inl ha =>
    calc
      x^2 = (3)^2 := by rw [ha]
      _ = 9 := by norm_num
  | inr hb =>
    calc
      x^2 = (-3)^2 := by rw [hb]
      _ = 9 := by norm_num

One reason the obtain tactic is useful is it lets you leave inl and inr implicit.

[Kyle Miller]

Usually in this situation people would write obtain rfl | rfl := h to immediately substitute the values of x everywhere. That way you don't even need to worry about ha or hb.

[rzeta0]

Thanks Kyle.

I asked in the other thread what the \. does, where I can read more about it, but I didn't get an answer. Can you shed any light? I don't really know what 'focussing" means specifically.

Where can I read more about what inl and inr are? I see them in the Infoview but I have never seen an explanation.

[Julian Berman]

Just to be sure to stress -- you have a disjunction, so you should never expect that you'll have access to ha and hb as hypotheses everywhere, because your disjunction says either one is true, and possibly both, but you'd need to prove both were true.

[Julian Berman]

the | syntax there in obtain is simply letting you say "give me separate goals where each one is correspondingly true"

[Julian Berman]

I don't really know what 'focussing" means specifically.

If you have 2 or more goals, "focusing" on the first one just means having Lean only show you one goal in the infoview at a time. (The dot is how you tell Lean to do this, and to temporarily hide the other ones.)

[Julian Berman]

This is good style because otherwise (e.g. in your original code) it's very hard to know when you've "finished" the proof for the first case and begun the second one without having Lean open and browsing around your code.

[Julian Berman]

Where can I read more about what inl and inr are? I see them in the Infoview but I have never seen an explanation.

They're the names of the Or type's constructors, you can type #check Or and go to definition and you'll see the 2 of them there.

[rzeta0]

Thanks Julian - both your points are very helpful.