semicolon and tactic state

Stream: general

[Bryan Gin-ge Chen]

Jason's post in the "ML for Lean" topic reminded me of this. It's really too bad that we can't see how the goals change before / after semicolons.

I made a half-hearted attempt to see whether there was any way to implement this for 3.5.x, but I didn't get very far. I did manage to figure out that the relevant code is around here, but I think I got stuck when I couldn't figure out how to get the cursor position to change the tactic state display using save_info (?).

Does anyone have any suggestions for this?

[Mario Carneiro]

I would actually be curious to see how the tactic state reporting after , in rw [a, b] works, since that's unlike any other tactic; maybe we can generalize that to other contexts

[Bryan Gin-ge Chen]

Yeah, I remember trying to understand that as well, I think it's around here. I guess I should study parser.

[Mario Carneiro]

I think the way it works it that when an info request is sent from a certain position, set_goal_info_pos brackets a parser such that while that parser is running, request positions are edited to the beginning position, and then save_info is used to annotate these specific target positions in the text with the current goal state.

[Mario Carneiro]

open tactic tactic.interactive interactive lean.parser interactive.types
namespace tactic.interactive
meta def have_many
  (es: parse $ list_of $ set_goal_info_pos $
    prod.mk <$> cur_pos <*> lean.parser.pexpr 0) :
  tactic unit :=
es.mmap' $ λ ⟨p, e⟩, do
  save_info p,
  e ← to_expr e,
  t ← infer_type e,
  assertv `this t e

example : true :=
begin
  have_many [
    (rfl : 2+2 = 4),
    (rfl : 2+2 = 4),
    zero_lt_one],
end

[Mario Carneiro]

However, this won't work for making ; display the goal state, because the ; is parsed by the global parser, not a custom tactic parser

[Mario Carneiro]

you would have to change lean to support this

[Bryan Gin-ge Chen]

Thanks! That definitely helps.

[Tim Daly]

(deleted)

[Alexander Bentkamp]

Another related issue is that you need to type a comma to see the next proof state. It's very confusing for beginners. Is this something that could be easily changed?

[Patrick Massot]

As a teacher I would love to see that changing. Students keep calling me to complain Lean is not happy since they don't see "goals accomplished", but they only miss one comma at the end.

[Jason Rute]

Another thing along these lines that I just discovered is that if one puts the curser right after a left curly brace {, it shows the goal state before the curly brace which could have multiple goals. Just in case this behavior isn't universal, using Lean 3.4.2 and looking at line line 40 in .../3.4.2/lean/library/init/data/fin/ops.lean if one places the curser before and after the{, one gets

2 goals
case nat.zero
a n : ℕ,
h₁ : a < n,
h₂ : 0 < n
⊢ a % 0 < n

case nat.succ
a n : ℕ,
h₁ : a < n,
b : ℕ,
h₂ : nat.succ b < n
⊢ a % nat.succ b < n

However, inside the {...} block it should just be the first goal.

[Jason Rute]

Oh, it is because there isn't a space after {. In my example, the line 40 is {simp [mod_zero], assumption},. If I add a space after the {, then the when I place the curser after the space, I do get the correct state:

1 goal
case nat.succ
a n : ℕ,
h₁ : a < n,
b : ℕ,
h₂ : nat.succ b < n
⊢ a % nat.succ b < n