Zulip Chat Archive

Stream: new members

Topic: focus1 tactic


Kevin Lacker (Oct 14 2020 at 20:48):

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

Kevin Lacker (Oct 14 2020 at 20:56):

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 (Oct 14 2020 at 20:58):

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 (Oct 14 2020 at 20:59):

focus1 is the noninteractive version of focus.

Bryan Gin-ge Chen (Oct 14 2020 at 21:00):

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

Kevin Lacker (Oct 14 2020 at 21:02):

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 (Oct 14 2020 at 21:10):

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 (Oct 14 2020 at 21:11):

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

Kevin Lacker (Oct 14 2020 at 21:12):

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 (Oct 14 2020 at 21:13):

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

Kevin Lacker (Oct 14 2020 at 21:14):

ah ok that makes sense

Bryan Gin-ge Chen (Oct 14 2020 at 21:14):

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

Kevin Lacker (Oct 14 2020 at 21:15):

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 (Oct 14 2020 at 21:17):

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

Kevin Lacker (Oct 14 2020 at 21:18):

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 (Oct 14 2020 at 21:18):

You linked to the definition of tactic.focus1?

Kevin Lacker (Oct 14 2020 at 21:18):

yeah right above it is a method called focus

Kevin Lacker (Oct 14 2020 at 21:19):

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

Bryan Gin-ge Chen (Oct 14 2020 at 21:19):

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

Kevin Lacker (Oct 14 2020 at 21:24):

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 (Oct 14 2020 at 21:26):

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 (Oct 14 2020 at 22:52):

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 (Oct 14 2020 at 22:54):

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 (Oct 14 2020 at 22:56):

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

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

Last updated: Dec 20 2023 at 11:08 UTC