solve_aux

Stream: mathlib4

[Scott Morrison]

Do we already have a lean4 version of

/-- `solve_aux type tac` synthesize an element of 'type' using tactic 'tac' -/
meta def solve_aux {α : Type} (type : expr) (tac : tactic α) : tactic (α × expr) :=

somewhere? I remember this is something that had duplicates at various times in mathlib3, so I don't want to write yet another one in mathlib4. :-)

[Mario Carneiro]

I would guess no. But you can write one and put it in a well named location so no one else has to :)

[Mario Carneiro]

it's a bit awkward since while the input is a TacticM the output might be MetaM or TermElabM

[Scott Morrison]

Perhaps just

import Lean

open Lean Elab Tactic Meta

def solve_aux (type : Expr) (tac : TacticM Unit) : TermElabM Expr := do
  let m ← mkFreshExprMVar type
  let _ ← run m.mvarId! tac
  return m

would do.

This differs slightly from the mathlib3 version, which captures the value produced by tac as well. Looking at how it is used, in 95% of cases this is just getting in the way. Options:

1. reproduce the mathlib3 behaviour, which is simple enough by providing a variant of run.
2. keep it simple, possibly backporting this change mathlib3 to avoid confusion.

While we're at it, can we have a better name than solve_aux? (I'd leave a comment so people can still find it.) Perhaps something like synthesizeUsing?

[Mario Carneiro]

I was never really a fan of the alphas, that was a late addition

[Mario Carneiro]

especially repeat returning a list of results seems like a bad idea

[Mario Carneiro]

you should return m.instantiateMVars though

[Mario Carneiro]

or at least m.getAssignment

[Scott Morrison]

mathlib4#452