goal scope

Stream: general

[Johan Commelin]

Can a tactic escape the focused goals? I am trying to write a defer tactic. Intended use should be something like this:

example : ∃ n, n > 0 :=
begin
  refine ⟨by defer k, _⟩,
  exact nat.zero_lt_one,
end

[Johan Commelin]

The idea would be that by defer k adds a goal k : ℕ to the main goal, and uses that to instantiate the existential.

[Johan Commelin]

But because it's written inside the ⟨by defer k, _⟩, it can't see the main goal.

[Rob Lewis]

No. I'm not even sure what you mean by "add a goal to the main goal," or that "main goal" is well defined. For this example, at least, you get the behavior you want with apply exists.intro.

[Kevin Buzzard]

Goals are just metavariables, right? Tactic mode is just displaying them to us in a convenient way. When more than one goal is focused I've seen tactics which operate on all of them.

existsi _ I think also does what you want. Not at Lean right now, don't know if use _ does too.