Print different goals when the cursor is scanning a tactic

Stream: lean4

[Simon Hudon]

In Lean 3, the parser of rw is implemented so that when you move your cursor through the rewrite rules, you see each intermediate goal. It's a pretty cool feature! Is there something similar in Lean 4?

[Sebastian Ullrich]

Does it not work for you? It should work basically the same.

[Simon Hudon]

Sorry I wasn't clear. I mean what if I want to use the same feature for a tactic that I'm implementing, how do I do that?

[Sebastian Ullrich]

Haha, that makes more sense! The interesting parts of the implementation are here: https://github.com/leanprover/lean4/blob/3bdb385c199ebbcc2070f8849647df35c2cc2145/src/Lean/Elab/Tactic/Rewrite.lean#L34-L41
withTacticInfoContext will record the tactic state before and after running the last argument, and then annotate the lexical range of the given syntax tree with that info. mkNullNode is used here to create a synthetic syntax tree whose lexical range spans two given syntax trees.

[Simon Hudon]

Nice! Thanks!

[Simon Hudon]

It's mostly working. I'm implementing ssreflect's move tactic and tactical and I want to show the goal between patterns. In this context, move => a b c is the same as intros a b c. I get the following odd behavior:

move => a b c
       ^
-- ⊢ T → V → U → True
move => a b c
         ^
⊢ T → V → U → True

u : T
⊢ V → U → True

Here is my elaboration code:

elab_rules : tactic
| `(tactic| $tac => $pats*) => do
  let pats' ← pats.mapM parseMoveIntroPat
  evalTactic tac
  let arrow := (← getRef)[1]
  withTacticInfoContext (mkNullNode #[arrow, pats[0]]) (pure ())
  for i in [:pats.size], pat in pats' do
    let next := pats.getD (i+1) Syntax.missing
    withTacticInfoContext (mkNullNode #[pats[i], next]) <|
      allGoals <| runMoveIntroPat pat

Can you see why in the second position I have two goals getting displayed?

[Mario Carneiro]

#mwe

[Simon Hudon]

Ok, I figured it out. I was treating the mkNullNode as an interval. It's more like a syntax tree or a set of syntax trees where we want a specific goal to be displayed. So my code should be (this time it's a #mwe, sorry about the oversight):

import Lean.Elab.Tactic

open Lean.Meta Lean.Elab.Tactic Lean

syntax "move" " => " ident+ : tactic

elab_rules : tactic
| `(tactic| move => $pats*) =>
withMainContext do
  let kw := (← getRef)[0]
  let arrow := (← getRef)[1]
  withTacticInfoContext (mkNullNode #[kw, arrow]) (pure ())
  for pat in pats do
    withTacticInfoContext pat do
      let (_, g) ←
        liftMetaMAtMain (intro . pat.getId)
      replaceMainGoal [g]

theorem foo : α → β → γ → θ := by
move => u v w

[Simon Hudon]

This time, each variable has only one goal

[Mario Carneiro]

what is the purpose of the first withTacticInfoContext? It doesn't seem to make any difference

[Mario Carneiro]

also you can do

| `(tactic| move%$kw =>%$arrow $pats*) =>

instead of that getRef stuff

[Simon Hudon]

Thanks for the neat trick! withTacticInfoContext is from @Sebastian Ullrich 's code snippet. The idea is to implement the same feature that rw has where you can move your cursor over the the rewrite rules and see the intermediate proof states. withTacticInfoContext records those proof states and associates them with the syntax trees that you're giving it.

[Mario Carneiro]

Yes I understand that. I'm saying that I don't see any difference in the goal states with or without that line

[Mario Carneiro]

the second withTacticInfoContext seems to be working as intended but you get the behavior you want even if you delete the first withTacticInfoContext

[Simon Hudon]

Ah, right! Yeah, I'm not clear on that. @Sebastian Ullrich, what's the purpose of the first withTacticInfoContext in the rw implementation?

[Sebastian Ullrich]

I believe this was from before we refined the behavior for when to show the pre/post state

[Simon Hudon]

Ok. What did it used to do and what did it get changed to?