SynthesizeUsing

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

def synthesizeUsing {u : Lean.Level} (type : Q(Sort u)) (tac : Lean.Elab.Tactic.TacticM Unit) : Lean.MetaM (List Lean.MVarId × Q(«$type»))

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.

Equations

• One or more equations did not get rendered due to their size.

def synthesizeUsing' {u : Lean.Level} (type : Q(Sort u)) (tac : Lean.Elab.Tactic.TacticM Unit) : Lean.MetaM Q(«$type»)

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

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

Equations

• One or more equations did not get rendered due to their size.

def synthesizeUsingTactic {u : Lean.Level} (type : Q(Sort u)) (tac : Lean.Syntax) : Lean.MetaM (List Lean.MVarId × Q(«$type»))

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.

Equations

• synthesizeUsingTactic type tac = synthesizeUsing type (Lean.Elab.Tactic.evalTactic tac)

def synthesizeUsingTactic' {u : Lean.Level} (type : Q(Sort u)) (tac : Lean.Syntax) : Lean.MetaM Q(«$type»)

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)

Equations

• synthesizeUsingTactic' type tac = synthesizeUsing' type (Lean.Elab.Tactic.evalTactic tac)