Understanding proof state

Stream: new members

[Alex Altair]

Hey all, I'm currently trying to improve my understanding of how to use Lean by building a mental model of the proof state at any given time. (This is similar to how, when you learn an imperative programming language, you'll learn to track the values of all the variables currently in scope etc.) I think the "Lean Infoview" is trying to do all this work for me, which is great, but I still find myself failing to correctly predict or understand what it's saying. For example, when I have the cursor placed inside the word calc, sometimes it says "No goals" by other times it doesn't.

Is there any kind of guide I should read on how to think about this?

[Patrick Massot]

What confuses you is that tactic state display is very sensitive to where you put your cursor. Since Lean 4 is indentation sensitive, moving your cursor inside a line containing only spaces can drastically change the displayed tactic state. We would need an example that you find confusing to be more specific.

[Kyle Miller]

There are two (easily confused) pieces of information you can see in the info view too, the "tactic state" and the "expected type". If you put your cursor at the beginning of an expression, you can see an expected type (which includes the local context for that type), and if you put your cursor at the beginning of a tactic, you can see the tactic state right before that tactic is executed.

The expected type view is sort of like a tactic state with exactly one goal.

[Patrick Massot]

That is indeed another source of confusion independent from what I was describing.

[Eric Wieser]

It would help a lot if the "expected type" pane had a different border or background color to the current goal; in a long goal state where the headings are offscreen, it's very easy to get confused

[Alex Altair]

Oh nice, thanks! I'm not sure how much the "Expected type" pane has been messing me up, but I'll keep an eye on it now

[Patrick Massot]

Note there is a VSCode extension setting asking to hide the Expected type panel by default (you can still click on its title to reveal it).

[Alex Altair]

What does it mean in the tactic state pane when something is highlighted red or green? Does it mean something like "the context that your cursor is in has just destroyed/created this object"?

[Patrick Massot]

Yes

[Alex Altair]

Okay I managed to figure out the next several confusions by thinking slightly harder, and now here's an example that I'm stuck on. This exercise is from Macbeth's "The mechanics of proof" book

[Alex Altair]

Screenshot-from-2023-09-28-10-46-30.png
Here, my cursor is on line 56, just after the :=

[Alex Altair]

Screenshot-from-2023-09-28-10-46-41.png
And here, my cursor is one character over, just before the by

[Alex Altair]

My question is, why does hxm2 pop out of scope between those? Why does hxm1 show back up into the tactic state? Why didn't hxm1 stay gone after it was used in the previous calc block?

[Kyle Miller]

I think when your cursor is immediately after the := you're seeing the tactic state after the exact calc ...

[Kyle Miller]

I tend to only trust the infoview if my cursor is immediately before a tactic or an expression. If it's somewhere in the middle of some other syntax (and especially if there is whitespace after the cursor) it might be giving you information about somewhere else.

[Kevin Buzzard]

What is that random exact on line 53? you say "why doesn't hxm1 stay gone" but you didn't close the hxm1 goal yet as far as I can see.

[Kyle Miller]

Something you could try is hovering your mouse over both locations -- do you see a faint blue highlighting in a region of the source code? When your mouse is right at the end of := I expect you'll see the whole calc block is highlighted, or at least a whole clause of the calc block. That indicates you might be getting some non-local information.

[Alex Altair]

Kevin Buzzard said:

What is that random exact on line 53? you say "why doesn't hxm1 stay gone" but you didn't close the hxm1 goal yet as far as I can see.

If I put my cursor immediately before the random exact, then it looks to me like it's showing that it will close the goal involving hxm1 (by having a vertical red line in front of it in the tactic state)

[Kevin Buzzard]

exactby itself won't do anything. The syntax is exact h. Right now you're doing exact calc (something which assume hxm2 exists already) to close the first goal.

[Alex Altair]

And then after it, in front of the have on line 54, the tactic state shows only the goal involving hxm2

[Alex Altair]

Ah, thank you, I was implicitly assuming that the newline did something there

[Kevin Buzzard]

I think the answer to "my syntax is totally screwed on line 53, why I am I confused on line 56?" is "because your syntax is totally screwed on line 53".

[Alex Altair]

(I knew I didn't know what Lean was taking to be exact, but it didn't have a red underline so I assumed it found something that worked for the local goal)

[Kevin Buzzard]

yeah I think the newline does nothing.

import Mathlib

example (x y : ℕ) (h : x = y) : x = y := by
  exact
    h -- works fine

[Alex Altair]

There seem to be lots of situations where Lean will magically fill in an argument for you so I was imagining this was one of those times

[Kevin Buzzard]

This is not the first time I've seen someone trying to close a goal with exact and your comments are beginning to make me understand why people might think this.

[Kevin Buzzard]

apply, for example, is extremely good at guessing missing information and filling it in automatically.

[Kevin Buzzard]

Similarly rw [add_zero] will just insert the missing x input to add_zero if it sees x + 0 in the goal.

[Alex Altair]

I had also tried exact hx1 before and that didn't work

[Alex Altair]

(but now I see that I can do left and then exact hx1 and that closes the goal)

[Kevin Buzzard]

That's because the goal isn't exactly hx1. You should learn to read the error messages; they don't just say "that didn't work", they tell you exactly what didn't work and why it didn't work. I know they look very daunting but they often are just the exact answer to the obvious question "why didn't it work"?

[Kevin Buzzard]

(and sometimes they're incomprehensible ;-) )

[Alex Altair]

Kyle Miller said:

I tend to only trust the infoview if my cursor is immediately before a tactic or an expression. If it's somewhere in the middle of some other syntax (and especially if there is whitespace after the cursor) it might be giving you information about somewhere else.

By the way this was also helpful to hear

[Alex Altair]

Kyle Miller said:

Something you could try is hovering your mouse over both locations -- do you see a faint blue highlighting in a region of the source code? When your mouse is right at the end of := I expect you'll see the whole calc block is highlighted, or at least a whole clause of the calc block. That indicates you might be getting some non-local information.

Oooh, nice, I had seen the window-on-hover, but I didn't notice the blue highlighting because it was too faint given my monitor's contrast. I expect that will be useful as well!

[Kyle Miller]

Kevin Buzzard said:

This is not the first time I've seen someone trying to close a goal with exact and your comments are beginning to make me understand why people might think this.

I wonder if the syntax for exact should be changed so that the term after it is optional. Then we could code exact minus the term to throw an error and put the red squiggle under all of "exact".

[Kyle Miller]

It's common in programming language implementations to put common mistakes into the grammar so that you can get more helpful error messages.

[Kevin Buzzard]

Unfortunately this is one place where Lean cannot possibly be expected to guess what happens after exact because it could be exact (some application of a theorem) or exact (some hypothesis). If your goal is precisely one of your hypotheses then you can use the assumption tactic, which tries to close the goal with every hypothesis in the local context (and is by the way this tactic the canonical first exercise to write for anyone interested in learning tactic-writing).

[Kyle Miller]

@Kevin Buzzard I think you might not have understood what I was suggesting. It wouldn't be that exact by itself would try to guess what to do, but that exact by itself would say something like "expecting a term after exact" and then put a squiggle under all of "exact" so you can't miss the error.

[Kyle Miller]

elab "my_exact " t?:(colGt term)? : tactic =>
  match t? with
  | none => throwError "expecting a term after `my_exact`"
  | some t => do Lean.Elab.Tactic.evalTactic <| ← `(tactic| exact $t)

example : False := by
  my_exact /-
  ~~~~~~~~ expecting a term after `my_exact` -/

example : True := by
  my_exact trivial -- ok

[Kevin Buzzard]

Oh sorry Kyle I completely failed to notice that it was you speaking!

[Kevin Buzzard]

But in the example above it's still going to do exact calc... right?

[Patrick Massot]

Alex's example is a really really unlucky garbage input. The unlucky part is that Lean tries to understand it for a very long time before giving up, because it sees the have hx2 as a term mode have.

[Patrick Massot]

For people who want to play with (maybe @Sebastian Ullrich since this is an interesting case study), this all happens at line 42 of https://github.com/hrmacbeth/math2001/blob/main/Math2001/02_Proofs_with_Structure/03_Or.lean where you need to write

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 hxm1 | hxm2 := h2
  have hx1 := calc
    x = x - 1 + 1 := by ring
    _ = 0 + 1 := by rw [hxm1]
    _= 1 := by ring
  exact
  have hx2 := calc
    x = x - 2 + 2 := by ring
    _ = 0 + 2 := by rw [hxm2]
    _= 2 := by ring
  exact

[Patrick Massot]

For maximal fun, try the following variation

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 hxm1 | hxm2 := h2
  have hx1 := calc
    x = x - 1 + 1 := by ring
    _ = 0 + 1 := by rw [hxm1]
    _= 1 := by ring
  exact
  have hx2 := calc
    x = x - 2 + 2 := by ring
    _ = 0 + 2 := by sorry -- rw [hxm2]
    _= 2 := by ring
  Or.inl hx1

This one does close the first goal created by obtain. I put a sorry in the second calc block which referred to hxm2 which does not exist in that branch of the proof. And then my very last line completes the proof term that the middle exact expects to see (without using hx2 which is completely irrelevant here).

[Patrick Massot]

For @Sebastian Ullrich , the very mysterious part is that, even in my "correct" proof above, putting the cursor anywhere after the e of exact if showing as tactic state the other case of obtain. An example showing this using only core Lean is

example (n : Nat) : True := by
  have fact : True ∨ False := Or.inl trivial
  apply fact.elim
  exact
  have : n = n :=
    calc n = n + 0 := n.add_zero
    _ = n := by simp
  fun _ => trivial
  exact fun _ => trivial

The apply line is creating two cases left and right. I see that putting the cursor anywhere after the e of exact shows the tactic state for case right.

[Kyle Miller]

Kevin Buzzard said:

But in the example above it's still going to do exact calc... right?

I set it to use colGt (which means "the term must start in a column after the beginning of the tactic"), so

    my_exact
    have hx2 := ...

should give you an error on my_exact rather than going down the questionable path of hoping that have hx2 := ... is the start of a term. (I didn't test this though.)

[Patrick Massot]

I cannot test this, I just ruined my copy of the book by running lake.

[Patrick Massot]

Well, I can test it elsewhere with the Mathlib-free example:

import Lean

elab "my_exact " t?:(colGt term)? : tactic =>
  match t? with
  | none => throwError "expecting a term after `my_exact`"
  | some t => do Lean.Elab.Tactic.evalTactic <| ← `(tactic| exact $t)

example (n : Nat) : True := by
  have fact : True ∨ False := Or.inl trivial
  apply fact.elim
  my_exact
  have : n = n :=
    calc n = n + 0 := n.add_zero
    _ = n := by simp
  fun _ => trivial
  exact fun _ => trivial

[Patrick Massot]

And indeed this has an error message on my_exact.

[Alex Altair]

Patrick Massot said:

I cannot test this, I just ruined my copy of the book by running lake.

Curious what "the book" means here, is that a reference to Erdős?

[Patrick Massot]

I mean Heather's book. But I'm sure she'll be happy to read your interpretation.

[Yaël Dillies]

Patrick Massot said:

I cannot test this, I just ruined my copy of the book by running lake.

(don't throw books in lakes!)

[Sebastian Ullrich]

Patrick Massot said:

For Sebastian Ullrich , the very mysterious part is that, even in my "correct" proof above, putting the cursor anywhere after the e of exact if showing as tactic state the other case of obtain.

There may not exist a heuristic that always does what people want here. The current heuristic was chosen so that on apply f (by simp) the goal view behaves the same as on apply f x -- tactics nested in terms are considered "incidental" and ignored when deciding whether to show the pre or post state of a surrounding tactic

[Patrick Massot]

I don't understand this analogy.

[Sebastian Ullrich]

They are both tactic-term-tactic nestings. Based on that, the server decides in both cases that it should show the post state after the first character

[Alex Altair]

Oh, here's another question about understanding what the tactic state means; is there a simple mental model I can use to understand what the ?m.55357 stuff is about, without grokking a bunch of stuff about dependent type theory?

[Ruben Van de Velde]

"a thing that I haven't filled in yet"

[Patrick Massot]

Sure, m stands for mystery.

[Kyle Miller]

?m.nnnn is a metavariable, and every metavariable consists of a local context and a target type. Metavariables can assigned expressions. The tactic state is just a list of metavariables. Tactics are programs that manipulate this list of metavariables. A completed theorem or definition must not contain any unassigned metavariables.

[Kevin Buzzard]

If you have a goal with ?m.37 in then you might well have another goal which just says |- Nat or something like that: that shouldn't really be a goal in a tactic proof, because it's not a theorem statement. But if you solve it with exact 42 then ?m.37 might well magically change to 42.