RFC: reusing goals

Proposal

The tactic refine (among other tactics) can create many goals, and sometimes it might be useful to use the result of a previous goal. It is currently possible to do this using a named metavariable, i.e. ?a, in the following example:

def foo₁ : Prop := sorry
def foo₂ : Prop := sorry
theorem foo : foo₁ → foo₂ := sorry
theorem bar : foo₁ → foo₂ → false := sorry

example (h : foo₁) : false := by
  refine bar ?a ?_
  · exact h
  · exact (foo ?a)

The goals created are foo₁ and foo₂, and for the proof of foo₂, one needs to reuse the previous proof of foo₁, which is where ?a comes in.

In the linked Zulip thread below, it has been expressed that ?a is a bit "unhygenic", so this proposal is to request a more hygenic version of ?a.

Community Feedback

Zulip discussion: #Is there code for X? > reuse previous goals?

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start with the linked Zulip discussion and the issue’s refine example using the named metavariable ?a. Investigate how goals and metavariables are represented in Lean’s tactic system; done means agreeing on and implementing a hygienic mechanism for reusing an earlier goal, with tests covering the demonstrated pattern.