SynthesizeUsing

This is a slight simplification of the solve_aux tactic in Lean3.

def synthesizeUsing (type : Lean.Expr) (tac : Lean.Elab.Tactic.TacticM Unit) : Lean.MetaM (List Lean.MVarId × Lean.Expr)

synthesizeUsing type tac synthesizes an element of type type using tactic tac.

The tactic tac is allowed to leave goals open, and these remain as metavariables in the returned expression.

def synthesizeUsing' (type : Lean.Expr) (tac : Lean.Elab.Tactic.TacticM Unit) : Lean.MetaM Lean.Expr

synthesizeUsing type tac synthesizes an element of type type using tactic tac.

The tactic must solve for all goals, in contrast to synthesizeUsing.

def synthesizeUsingTactic (type : Lean.Expr) (tac : Lean.Syntax) : Lean.MetaM (List Lean.MVarId × Lean.Expr)

synthesizeUsing type tacticSyntax synthesizes an element of type type by evaluating the given tactic syntax.

Example:

let (gs, e) ← synthesizeUsingTactic ty (← `(tactic| congr!))

The tactic tac is allowed to leave goals open, and these remain as metavariables in the returned expression.

def synthesizeUsingTactic' (type : Lean.Expr) (tac : Lean.Syntax) : Lean.MetaM Lean.Expr

synthesizeUsing' type tacticSyntax synthesizes an element of type type by evaluating the given tactic syntax.

Example:

let e ← synthesizeUsingTactic' ty (← `(tactic| norm_num))

The tactic must solve for all goals, in contrast to synthesizeUsingTactic.

If you need to insert expressions into a tactic proof, then you might use synthesizeUsing' directly, since the TacticM monad has access to the TermElabM monad. For example, here is a term elaborator that wraps the simp at ... tactic:

def simpTerm (e : Expr) : MetaM Expr := do
  let mvar ← Meta.mkFreshTypeMVar
  let e' ← synthesizeUsing' mvar
    (do evalTactic (← `(tactic| have h := $(← Term.exprToSyntax e); simp at h; exact h)))
  -- Note: `simp` does not always insert type hints, so to ensure that we get a term
  -- with the simplified type (as opposed to one that is merely defeq), we should add
  -- a type hint ourselves.
  Meta.mkExpectedTypeHint e' mvar

elab "simpTerm% " t:term : term => do simpTerm (← Term.elabTerm t none)