focus1 tactic

Stream: new members

[Kevin Lacker]

What does the focus1 tactic do? It is used reasonably often but I cannot find any docs on it

[Kevin Lacker]

the code is not too complicated:

meta def focus1 {α} (tac : tactic α) : tactic α :=
do g::gs ← get_goals,
   match gs with
   | [] := tac
   | _  := do
      set_goals [g],
      a ← tac,
      gs' ← get_goals,
      set_goals (gs' ++ gs),
      return a
   end

but I'm still confused. It repeatedly applies a tactic on just the head goal until there is only one goal left, then it applies the tactic one more time, and then it stops with whatever the goal state happens to be? or am I confusing goal state with return value?

[Kevin Lacker]

or am I confused that there's no repeating here. it applies the tactic once while forbidding the tactic to work on any non-head goal?

[Bryan Gin-ge Chen]

focus1 is the noninteractive version of focus.

[Bryan Gin-ge Chen]

It applies tac to the head goal, and then puts any newly generated goals on top of the previous tail.

[Kevin Lacker]

ok. what's the difference between how interactive and noninteractive tactics work, is that just like a suggestion? it doesn't seem like the code is fundamentally different afaict

[Bryan Gin-ge Chen]

You can only use interactive tactics in begin ... end or by { ... } blocks. Non-interactive tactics are used to implement interactive tactics or do other Lean metaprogramming.

[Bryan Gin-ge Chen]

See the tactic-writing tutorial if you haven't already.

[Kevin Lacker]

i mean, what makes focus and focus1 available in different contexts? I don't see anything that differs in their signatures

[Bryan Gin-ge Chen]

Well, focus1 has return type tactic \a, and you can only use things that return tactic unit interactively.

[Kevin Lacker]

ah ok that makes sense

[Bryan Gin-ge Chen]

The namespaces are also different (tactic.focus1 vs tactic.interactive.focus), but that's less of a big deal.

[Kevin Lacker]

why is their implementation totally different, is that just a historical artifact? in theory could one just implement focus by dropping the return value of focus1?

[Bryan Gin-ge Chen]

That seems to me how focus is implemented? src#tactic.interactive.focus

[Kevin Lacker]

oh. I was looking at the focus function defined here: https://github.com/leanprover-community/lean/blob/cc72964/library/init/meta/tactic.lean#L1154

[Bryan Gin-ge Chen]

You linked to the definition of tactic.focus1?

[Kevin Lacker]

yeah right above it is a method called focus

[Kevin Lacker]

I guess that one is a totally different focus from the regular focus?

[Bryan Gin-ge Chen]

Yeah, it is. Whoops, didn't know about that one.

[Kevin Lacker]

okay, that explains my confusion. I guess it is a reasonably common pattern within lean to have tactic.foo and tactic.interactive.foo with different behavior

[Kevin Lacker]

perhaps related to the "weird things" described in this chunk of the docs: "Such functions are either called by other tactics---those are typically in the tactic namespace---or called interactively by users inside tactic blocks---those must be in the tactic.interactive namespace (this is not quite necessary for very simple tactics, but weird things will happen in general when ignoring this rule)."

[Mario Carneiro]

Well the tactic.foo version will be optimized for use by tactic code, while tactic.interactive.foo will be optimized for begin end blocks

[Mario Carneiro]

BTW the "weird things" are that non-interactive tactics have a different syntax for composition than interactive tactics, so a non-interactive tactic in the middle of an interactive composition will "pollute" it and turn everything to non-interactive compositions, meaning that the interactive tactics will be parsed incorrectly

example : true :=
by { skip; exact trivial } -- fine
example : true :=
by { tactic.skip; exact trivial } -- aah errors everywhere

[Mario Carneiro]

you can use `[...] to force a return to interactive mode

example : true :=
by { tactic.skip; `[exact trivial] } -- fine