are `obtain` hypotheses temporary?

Stream: new members

[rzeta0]

The following is a simple example of using obtain to split a disjunctive hypothesis into cases:

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

Question: Are the obtained hypotheses ha and hb temporary? That is, they only exist in the scope of the subproofs (inside the \.) or do they replace h and exist until the end of the program?

Infoview suggests h is deleted and replaced by ha and hb. But since I don't have more code after the cases, I don't know what happens after these goals are met.

[Damiano Testa]

Internally, Lean creates lots of metavariable, each one representing a goal. Roughly, you can imagine that any tactic that modifies the goal is very likely "resolving completely" the goal before that tactic application and replacing it with one or more new metavariables (possibly very similar to the one that you started with) or possibly finishing a proof.

Lean keeps track of these "implications" and knows how to solve the original goal, if you solve all the later goals and this happens in the background.

[Damiano Testa]

Without knowing the exact details of obtain, my guess is that after the obtain, the original goal is considered "solved" and two more "dependent" goals are created, each with its context (the local hypotheses). Lean knows what the resolved goals are, but is not showing them to you (and typically there are many more side-goals than the ones that you ever see, since Lean is constantly solving lots of unification, typeclass and similar such goals in the background.

[Damiano Testa]

Here is a quick test that you can do: the new tactic show_mvar_names simply prints the internal names that Lean has for the goals. These names are unique, so a different name means a different goal.

import Mathlib

open Lean Elab Tactic

open Lean Elab Tactic in
/-- prints the internal names of all the metavariables -/
elab "show_mvar_names" : tactic => do
  logInfo m!"{(← getGoals).map (·.name)}"

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

[rzeta0]

Hi Damiano

If I add show_mvar_names to the end to see if the obtained hypothesis exist after the cases, then it shows me a [].

I can understand deleting goals once they are proven, but deleting hypotheses seems wrong as they may be used again further down the proof.

---

import Mathlib

open Lean Elab Tactic

elab "show_mvar_names" : tactic => do
  let gs ← getGoals
  logInfo m!"{gs.map (·.name)}"

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

[Damiano Testa]

The tactic is showing metavariables. Each metavariable has a goal and a context that contains all the hypotheses relevant to that mvar.

[Damiano Testa]

At the end of a proof, there are no metavariables left, so no hypotheses either.

[Damiano Testa]

Roughly, a metavariable is a unique name for each one of the things that you can focus on using ·: goal, hypothesis, everything.

[Yakov Pechersky]

But also, it would be incorrect to assume ha : x = 3 outside of the scope where we're no longer in the left case of the disjunction. We can't assume x = 3 anymore once we're outside that case. So Lean helps us by keeping track of the hypotheses that still hold.

[Kyle Miller]

A "goal" consists of a "local context" (a list of hypotheses/local variables) and a "target" (the type that comes after the turnstile ⊢). While "goal" should refer to the goal itself, colloquially people tend to use it to refer to the target via a figure of speech (synecdoche). Goals and metavariables are nearly the same thing, but a goal is a metavariable that appears in the tactic state's goal list.

The local context is essential to a goal since it's necessary for interpreting the target. In your case, it answers what x is.

Your obtain creates two goals. Each focusing dot focuses on each goal one at a time. Here's how you can think of it:

• the goal (let's call it ?m.1) before obtain is used to create two new goals (let's call them ?m.2 and ?m.3) with the same local contexts but with h deleted, and furthermore ?m.2 has ha : x = 3 and ?m.3 has hb : x = -3
• internal detail: the obtain tactic does the assignment ?m.1 := Or.casesOn h (fun ha => ?m.2) (fun hb => ?m.3) (or something similar), which solves the goal ?m.1 assuming ?m.2 and ?m.3 are solved. This expression makes sense because ?m.2 has ha in its local context and ?m.3 has hb in its local context.
• obtain adds ?m.2 and ?m.3 to the front of the goal list in the current tactic state.

There is no adding or deleting local variables to the goals here. The two goals after obtain are derived from the original goal, but are otherwise independent of it, and each are independently solved by your focus tactics.

[rzeta0]

Thanks Kyle - your reply is helpful.

I have some follow on questions:

1. How does Lean know which scope which lean code corresponds to after an obtain? The above discussion mentions focussing dots, but as far as I can tell (based on Heather macBeth's course) they seem optional good style. Does lean use the point at which the sub-goal is proved to then destroy the "context" and with it the ha hypothesis?

2. Is / was there any discussion to further develop the lean syntax to make this clearer for readers, or to signal to lean where the scope was intended by the code writer? In the manner we use brackets or indents in some languages to denote function/loop/other scope?

3. Can I confirm my understanding: A yes/no would be incredibly helpful:

• 4. The goal h exists before obtain and exists again after the sub-goals created by obtain are completed ?
• 5. The goals ha and hb only exist in the scope of the sub-goals, and once proven, they no longer exist, eg if I add additional code after the my example at the top of this thread, then ha doesn't exist any more ?

[Kyle Miller]

Tactic scripts don't have scopes per se. It's all an illusion, and using good style is a way to make the scopes more real. All that really exist are the tactic states before and after each tactic, which consist of (1) the current list of goals and (2) other elaboration state, like metavariable assignments.

Each individual tactic consumes the current list of goals and outputs a new list of goals, some of which may be the same. Most tactics only operate on the first goal in the list. The focus dot · T for example is a tactic that has a tactic T as an operand. The way it works is it takes the current goal list [g1, g2, ..., gn], runs T using the goal list [g1], checks that the result of running T is the empty goal list [], and then afterwords sets the goal list to [g2, ..., gn].

[Kyle Miller]

4. h is not a goal. It is a local hypothesis in the goal. Changing this to "local hypothesis", the answer is that h exists in the goal that obtain operates on. After that obtain, the goal no longer exists. The goal does not exist anymore even after the sub-goals are complete.

5. ha and hb exist in the local contexts of the subgoals, so they are "in scope" for the tactics that operate on them. Once these goals are done, ha and hb cannot be referred to anymore, they no longer exist.

[Kyle Miller]

I'm trying to be careful here with the word "scope", because it's not very well defined here. We could equate "scope" with "local context of the goal the tactic is operating on", and that's basically how it seems to work, but using the word "scope" may lead you to think that tactic scripts use something like lexical scope, which there are no guarantees here. Individual goals have "scopes" is the best I can say, it's a dynamic not lexical concept.

[Kyle Miller]

In the manner we use brackets or indents in some languages to denote function/loop/other scope?

Yes, we use focusing dots. They are not enforced by the language, but in projects like mathlib, we require structure that eludicates the scopes.

Some tactics, like induction and cases, have special syntax to create structured proofs, which is more directly in the direction you are wanting.

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

[Kyle Miller]

By the way, if you are familiar with a stack-based language like Forth, you can think of tactic scripts as being similar to Forth programs. The goal list is a stack.

[Kyle Miller]

Just like Forth, there's no scope other than the global scope. Unlike Forth, each "value" (each goal) comes with a local context to keep track of the local variables that can be used in that context.

[rzeta0]

Your explanation as a "stack" of contexts, comparing to Forth, and the internal mechanism of working through linear list of goals [g1, g2, .. gn] is extremely helpful.

The most illuminating and helpful reply in a long time - thank you :)

[rzeta0]

( which still makes me worry that in the real world, proofs are more like trees, and a linear list then leads to ambiguous syntax ... but that's a discussion for another day )

[Kyle Miller]

There's always a question about what "is" a proof. For a low-level point of view, a tactic script is just a metaprogram that constructs the actual proof. You can see the tree-like proof term when you use by? ... (short for show_term by ...).

Lean tactic proofs are meant to be followable with editor aid, not readable on their own, but when they're written in particular ways it can be easier to read without aid (hence demanding focus dots for example). There's no harm in ambiguity to a human reader since everything is machine checked. At least when it comes to truth. When it comes to maintainability, we like things to be more readable, but not so verbose that it gets in the way of making fixes.

[rzeta0]

Kyle Miller said:

Lean tactic proofs are meant to be followable with editor aid, not readable on their own

This again is very reassuring for beginners like me - thank you.

PS - some may find it interesting that LaTeX was never intended to be written by humans, but rather generated by tools ... I think the parallels are interesting.