reuse previous goals?

Stream: Is there code for X?

[Kenny Lau]

Is there a way to reuse previous goals like this?

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

-- normal way (duplicate code)
example (h : foo₁) : false := by
  refine bar ?_ ?_
  · /-
    h : foo₁
    ⊢ foo₂
    -/
    exact foo h
  · exact foo h

-- clever way to reuse previous goals:
example (h : foo₁) : false := by
  refine (fun reused ↦ bar reused ?_) ?_
  · /-
    h : foo₁
    reused : foo₂
    ⊢ foo₂
    -/
    exact reused
  · exact foo h

[Markus Himmel]

How about

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

[Kenny Lau]

@Markus Himmel that is indeed new to me, i didn't know you could unify goals like that! but unfortunately this would only work if the two goals are exactly the same, so you still can't reuse stuffs

[Markus Himmel]

How so? This also works:

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 (foo ?a)
  · exact h

[Kenny Lau]

what if the proof is not as simple as (foo ?a) and you want to split it as a separate goal?

[Kenny Lau]

i guess you could do my trick but only for that argument

[Markus Himmel]

Arguably for more complex cases it is more readable to just use have for the bits that you want to refer to multiple times.

[Kenny Lau]

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 ((fun reused ↦ ?_) ?a)
  · exact h
  · exact foo reused

[Kenny Lau]

Markus Himmel said:

Arguably for more complex cases it is more readable to just use have for the bits that you want to refer to multiple times.

fair enough

[Kyle Miller]

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

[Kenny Lau]

oh wow!

[Kenny Lau]

you can't even see ?a in the context (infoview) of the second goal!

[Kyle Miller]

Yeah, caveat emptor! :slight_smile:

[Kyle Miller]

It's easy to break it:

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

The problem here is that the case tactic "consumes" the metavariable, in the sense that it removes ?a from the name->metavariable table.

[Kyle Miller]

Another way to break it is to get Lean to create another metavariable named a. The apply tactic uses a function's parameter names for the new metavariables.

def myId {α : Sort _} (a : α) : α := a

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

[Niklas Halonen]

Isn't it really unhygienic to use named metavariables? I remember reading somewhere the one must always use ?_ but couldn't find it quickly.

To demonstate how fragile named metavars can be, I came up with a small example (try uncommenting different parts of it):

example (h: True ∨ True) : True ∧ True := by
  cases h
  · -- case inl => -- try changing the bullet to case
    -- refine ⟨ ?inl, ?inl ⟩ -- inl is not fresh, causes error
    -- refine ⟨ ?inr, ?inr ⟩ -- synthetic hole has already been defined with an incompatible local context
    refine ⟨ ?a, ?a ⟩     -- a is fresh
    trivial
  · -- case inr =>
    refine ⟨ ?inl, ?inl ⟩ -- inl is still not fresh
    sorry

For example changing the bullet point to case suddenly makes ?inl a free metavariable.

I'm no metaprogramming expert so somebody can correct me if I'm wrong.

Edit: Whoops, Kyle already made this point, sorry for repeating!

[Kyle Miller]

Niklas Halonen said:

Edit: Whoops, Kyle already made this point, sorry for repeating!

It's worth reiterating how fragile they are :-)

I've been hoping for some solution to this problem. For example, perhaps tactics like refine could guarantee fresh metavariables? Or maybe there's a metavariable namespacing system so that in that second subproof ?inl will refer to a fresh name?

[Robin Arnez]

Maybe there could be some kind of meta-variable name hygiene, similar to binder names?

[Kenny Lau]

https://github.com/leanprover-community/mathlib4/issues/26044

[Kenny Lau]

https://github.com/leanprover/lean4/issues/8844

[Mario Carneiro]

Kenny Lau said:

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 ((fun reused ↦ ?_) ?a)
  · exact h
  · exact foo reused

A variation on this which avoids some of the issues around hygiene with named metavariables is:

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