Why does rfl fail to instantiate metavariables?

Stream: general

[Jason Gross]

Can someone explain this error to me?

def construct_by_refinement : ∃ (result : Nat), result = 5 := by
  refine ⟨?result, ?pf⟩
  case pf => rfl

What's the right way to construct metavariables and later instantiate them with tactics?

[Robin Arnez]

When you create meta-variables using ?name, they are synthetic-opaque, i.e. defeq will never assign them. Non synthetic-opaque meta-variables are created by _ but that won't work here, the constructor tactic also creates non-synthetic-opaque meta-variables though so that's what you can use.

[Jason Gross]

Thanks! Why doesn't _ work?

[Robin Arnez]

Because refine expects all non-synthetic-opaque metavariables to be assigned

[Robin Arnez]

apply doesn't have that restriction but also doesn't use the goal type so you need:

def construct_by_refinement : ∃ (result : Nat), result = 5 := by
  apply (⟨_, ?pf⟩ : ∃ (result : Nat), result = 5)
  case pf => rfl

[Adam Topaz]

This apply is not ideal IMO. But the version I came up with is also not ideal:

def construct_by_refinement : ∃ (result : Nat), result = 5 := by
  run_tac do Meta.mkFreshExprMVar (userName := `result) none
  refine ⟨?result, ?_⟩
  rfl

I hope someone else can chime in with the proper way to do this.

[Dan Velleman]

This seems to work:

def construct_by_refinement : ∃ (result : Nat), result = 5 := by
  apply Exists.intro
  rfl

[Robin Arnez]

Yeah, right, constructor, or apply Exists.intro works. I just wanted to demonstrate how refine and apply differ in handling metavariables

[Adam Topaz]

Doing something like apply ConstructorName or constructor is also not ideal, because you may want to explicitly say which parameters of the constructor you want to specify ahead of time, and which should be determined later after some unification. So IMO there should be some way to do it with refine (or at least with refine-like syntax)

[Robin Arnez]

Hmm at that point you could probably just specify them before though; having metavariables float around is less than ideal -- I even thought at some point that that was a bug in apply (putting the goal for the proof first) and decided to use refine instead for this reason (I've since understood it more but still)

[Robin Arnez]

also, apply Exists.intro _ ?prf?

[Kyle Miller]

Here's a workaround:

def construct_by_refinement : ∃ (result : Nat), result = 5 := by
  refine ⟨?result, ?pf⟩
  case pf => refine rfl

The refine tactic turns on a feature to assign synthetic opaque metavariables. (No one is expected to know this. Consider this to be a hack.) By the way, apply's current behavior is more-or-less a bug, so that's a hack too.

This is a usability problem that comes up frequently with existentials. Sometimes you want to let the value follow from the proof rather than vice versa.

I think it's possible that at some point we might have "synthetic semiopaque metavariables", and either _ would work here:

def construct_by_refinement : ∃ (result : Nat), result = 5 := by
  refine ⟨_, ?pf⟩
  case pf => rfl

or you'd write ??, or some other sigil:

def construct_by_refinement : ∃ (result : Nat), result = 5 := by
  refine ⟨??result, ?pf⟩
  case pf => rfl

This "synthetic opaque" concept is to help address issues where goals would go missing in counterintuitive ways, plus they need to be handled differently internally to make sure that they remain assignable in tactics. The design is also meant to prevent people from writing "swiss cheese proofs", with holes in all the types, since they tend to be less maintainable.

Something that would help get semiopaque metavariables into Lean is a collection of case studies demonstrating it would be a useful proof organization device.

[Adam Topaz]

Would it make sense to have something like the following for now?

import Mathlib.Tactic
import Batteries.Lean.Meta.Basic

open Lean Elab

elab "unifying" id:ident tacs:tacticSeq : tactic => commitIfNoEx do
    let some (mvarid, decl) := (← getMCtx).decls.toArray.find? fun (_, decl) =>
        decl.userName == id.getId
      | throwError "Couldn't find mvar named {id}"
    modifyMCtx fun mctx => mctx.setMVarKind mvarid .natural
    Tactic.evalTacticSeq tacs
    modifyMCtx fun mctx => mctx.setMVarKind mvarid decl.kind

def construct_by_refinement : ∃ (result : Nat), result = 5 := by
  refine ⟨?result, ?pf⟩
  unifying result
    case pf => rfl