Documentation

Mathlib.Util.SynthesizeUsing

SynthesizeUsing #

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

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.
Instances For

    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.
    Instances For

      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
      Instances For

        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
        Instances For