Confusing goal with unfinished `have`

[Vtec234]

Description

In the following unfinished proof:

example : ∃n, n < 1 := by
   have h : 0 < 1 := 
                   --^ cursor here
   exact ⟨0, h⟩

the goal state shows up as

h : 0 < 1
⊢ ∃ n, n < 1

with 0 < 1 as the assumption. To see the "real" goal ⊢ 0 < 1 we have to write by. This is confusing for beginners, since really at that cursor there is no goal state at all -- one should produce a term. So I suggest we show an expected type there rather than a goal state.

Versions

8df2b07

[leodemoura]

@Vtec234 Note that the example above is currently parsed as

example : ∃n, n < 1 := by
   have h : 0 < 1 := exact ⟨0, h⟩

The exact ⟨0, h⟩ is parsed as an application. The syntax tree is

(Term.app `exact [(Term.anonymousCtor "⟨" [(numLit "0") "," `h] "⟩")])

The info view shows the correct "Expected type" (0 < 1) when we hover over exact.

[leodemoura]

@Kha Any ideas?

[Kha]

Good question. If we can make it show the expected type here, do we want to hide the goal by default if we're inside of a term? We definitely don't want to always do that, e.g. when typing a simp argument.

[leodemoura]

I am inclined to mark this issue as "wontfix", and close it.

@Vtec234 I acknowledge the current behavior is confusing, but I don't see a good solution. Any suggestions on how to improve it?

[Vtec234]

It is something that confused one of the students at the course we were teaching, and it briefly confused me as well. But I agree that changing this might be more trouble than it's worth, so closing is okay with me. The only thing I could think of would be to require colGt at have .. := (haveIdDecl). I guess it depends on whether

have h :=
term

is considered acceptable or not.

EDIT: Oh well, with colGt it parses differently but the goal state still includes h.

[gebner]

I'm not sure why you expect the goal state to change here. After have h := comes a term, not a tactic. (It would be great though if the expected type was shown directly after :=.)

Would it be less confusing if we had a have h by ... syntax?

[Vtec234]

It would be great though if the expected type was shown directly after :=.

Yes, this is what I expected.

[leodemoura]

It would be great though if the expected type was shown directly after :=.

Yes, this is what I expected.

I agree. I did not have time to investigate this issue yet. Do you know why we are not getting the correct expected type here?

Would it be less confusing if we had a have h by ... syntax?

I like this idea.

[gebner]

Do you know why we are not getting the correct expected type here?

I'm pretty sure that's because we look for the smallest term node around the cursor, but there's no term node around the space after := because the space is part of :=:

import Lean
open Lean Elab Command

elab "#dump" t:term : command => do
  logInfo (repr t)

#dump by have h :=
  exact

-- ^^ newline is part of :=

[leodemoura]

I'm pretty sure that's because we look for the smallest term node around the cursor, but there's no term node around the space after := because the space is part of :=:

I agree.

@Kha @gebner Any ideas on how to fix this? The first hack that comes to mind is to move the trailing spaces for the := atom to the leading spaces for the next atom/identifier. The parser is already invoking Syntax.updateLeading to make adjustments.

[Kha]

I don't think that would work if what follows the := is either EOF or something that is definitely not a term (e.g. the next theorem). We could instead put an info node on :=, MVP for let only: https://github.com/Kha/lean4/commit/30278e8aeb50f3b508aaff98d4a0da1f0582951d However, the output is still quite confusing given the unchanged outer goal