The setm tactic

This module defines the setm tactic.

The setm tactic matches a pattern containing named holes to the type of a target, and creates local declarations for the hole names whose values are the assigned expressions. By default, the pattern is matched against the goal, but a local declaration can be matched instead via the using syntax. Optionally, with the syntax at loc, it also rewrites at locations loc to replace the occurrences of the matched expressions with the newly-introduced local declarations.

TODO

It would be nice if the tactic was be made to work for non-constants under binders (by adding forall binders to the local declarations).

def Mathlib.Tactic.SetM.setM : Lean.ParserDescr

setm patt matches patt, a term containing named holes (like ?a) to the goal, and creates named local declarations for the matched holes with their assigned expressions as values. Moreover, it will replace the matches with their new names. This tactic can be used to give a name to a complicated subexpression appearing in the goal or a hypothesis.

• setm patt using h matches patt with the local hypothesis named h instead of the main goal.
• setm patt at loc also rewrites by the newly-introduced local declarations at the location(s) loc.

Examples:

example : ∃ n, n = 2 ^ 10 - 1 := by
  setm ∃ _, _ = ?a
  /-
  a := 2 ^ 10 - 1
  ⊢ ∃ n, n = a
  -/
  exact .intro a rfl

using h matches against h instead of the goal:

example (h : 1 + 2 = 3) : ∃ n, n = 2 := by
  setm _ + ?a = _ using h
  /-
  a := 2
  h : 1 + a = 3
  ⊢ ∃ n, n = 2
  -/
  exact .intro a rfl

at h₂ rewrites h₂ so that it uses a:

example (h₁ : 1 + 2 = 3) (h₂ : 2 + 2 = 4) : ∃ n, n = 2 := by
  setm _ + ?a = _ using h₁ at h₂
  /-
  a : Nat := 2
  h₁ : 1 + a = 3
  h₂ : a + a = 4
  ⊢ ∃ n, n = 2
  -/
  exact .intro a rfl

Equations

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