The convert tactic.

The exact e and refine e tactics require a term e whose type is definitionally equal to the goal. convert e is similar to refine e, but the type of e is not required to exactly match the goal. Instead, new goals are created for differences between the type of e and the goal using the same strategies as the congr! tactic. For example, in the proof state

n : ℕ,
e : Prime (2 * n + 1)
⊢ Prime (n + n + 1)

the tactic convert e using 2 will change the goal to

⊢ n + n = 2 * n

In this example, the new goal can be solved using ring.

The using 2 indicates it should iterate the congruence algorithm up to two times, where convert e would use an unrestricted number of iterations and lead to two impossible goals: ⊢ HAdd.hAdd = HMul.hMul and ⊢ n = 2.

A variant configuration is convert (config := .unfoldSameFun) e, which only equates function applications for the same function (while doing so at the higher default transparency). This gives the same goal of ⊢ n + n = 2 * n without needing using 2.

The convert tactic applies congruence lemmas eagerly before reducing, therefore it can fail in cases where exact succeeds:

def p (n : ℕ) := True
example (h : p 0) : p 1 := by exact h -- succeeds
example (h : p 0) : p 1 := by convert h -- fails, with leftover goal `1 = 0`

Limiting the depth of recursion can help with this. For example, convert h using 1 will work in this case.

The syntax convert ← e will reverse the direction of the new goals (producing ⊢ 2 * n = n + n in this example).

Internally, convert e works by creating a new goal asserting that the goal equals the type of e, then simplifying it using congr!. The syntax convert e using n can be used to control the depth of matching (like congr! n). In the example, convert e using 1 would produce a new goal ⊢ n + n + 1 = 2 * n + 1.

Refer to the congr! tactic to understand the congruence operations. One of its many features is that if x y : t and an instance Subsingleton t is in scope, then any goals of the form x = y are solved automatically.

Like congr!, convert takes an optional with clause of rintro patterns, for example convert e using n with x y z.

The convert tactic also takes a configuration option, for example

convert (config := {transparency := .default}) h

These are passed to congr!. See Congr!.Config for options.

def Lean.MVarId.convert (e : Expr) (symm : Bool) (depth : Option ℕ := none) (config : Congr!.Config := { }) (patterns : List (TSyntax `rcasesPat) := []) (g : MVarId) : MetaM (List MVarId)

Close the goal g using Eq.mp v e, where v is a metavariable asserting that the type of g and e are equal. Then call MVarId.congrN! (also using local hypotheses and reflexivity) on v, and return the resulting goals.

With symm = true, reverses the equality in v, and uses Eq.mpr v e instead. With depth = some n, calls MVarId.congrN! n instead, with n as the max recursion depth.

def Lean.MVarId.convertLocalDecl (g : MVarId) (fvarId : FVarId) (typeNew : Expr) (symm : Bool) (depth : Option ℕ := none) (config : Congr!.Config := { }) (patterns : List (TSyntax `rcasesPat) := []) : MetaM (MVarId × List MVarId)

Replaces the type of the local declaration fvarId with typeNew, using Lean.MVarId.congrN! to prove that the old type of fvarId is equal to typeNew. Uses Lean.MVarId.replaceLocalDecl to replace the type. Returns the new goal along with the side goals generated by congrN!.

With symm = true, reverses the equality, changing the goal to prove typeNew is equal to typeOld. With depth = some n, calls MVarId.congrN! n instead, with n as the max recursion depth.

def Mathlib.Tactic.convert : Lean.ParserDescr

convert e, where the term e is inferred to have type t, replaces the main goal ⊢ t' with new goals for proving the equality t' = t using congruence. The goals are created like congr! would. Like refine e, any holes (?_ or ?x) in e that are not solved by unification are converted into new goals, using the hole's name, if any, as the goal case name. Like congr!, convert introduces variables while applying congruence rules. These can be pattern-matched, like rintro would, using the with keyword.

See also convert_to t, where t specifies the expected type, instead of a proof term of type t. In other words, convert_to t works like convert (?_ : t). Both tactics use the same options.

• convert ← e creates equality goals in the opposite direction (with the goal type on the right).
• convert e using n, where n is a positive numeral, controls the depth with which congruence is applied. For example, if the main goal is ⊢ Prime (n + n + 1) and e : Prime (2 * n + 1), then convert e using 2 results in one goal, ⊢ n + n = 2 * n, and convert e using 3 (or more) results in two (impossible) goals ⊢ HAdd.hAdd = HMul.hMul and ⊢ n = 2. By default, the depth is unlimited.
• convert e with x ⟨y₁, y₂⟩ (z₁ | z₂) names or pattern-matches the variables introduced by congruence rules, like rintro x ⟨y₁, y₂⟩ (z₁ | z₂) would.
• convert (config := cfg) e uses the configuration options in cfg to control the congruence rules (see Congr!.Config).

Examples:

-- `convert using` controls the depth of congruence.
example {n : ℕ} (e : Prime (2 * n + 1)) :
    Prime (n + n + 1) := by
  convert e using 2
  -- One goal: ⊢ n + n = 2 * n
  ring

-- `convert` can fail where `exact` succeeds.
example (h : p 0) : p 1 := by
  fail_if_success
    convert h -- fails, left-over goal 1 = 0
    done
  exact h -- succeeds

```lean
-- `convert with` names introduced variables.
example (p q : Nat → Prop) (h : ∀ ε > 0, p ε) :
    ∀ ε > 0, q ε := by
  convert h using 2 with ε hε
  -- Goal now looks like:
  -- hε : ε > 0
  -- ⊢ q ε ↔ p ε
  sorry

def Mathlib.Tactic.elabTermForConvert (term : Lean.Syntax) (expectedType? : Option Lean.Expr) : Lean.Elab.Tactic.TacticM (Lean.Expr × List Lean.MVarId)

Elaborates term ensuring the expected type, allowing stuck metavariables. Returns stuck metavariables as additional goals.

def Mathlib.Tactic.convertTo : Lean.ParserDescr

convert_to t on a goal ⊢ t' changes the goal to ⊢ t and adds new goals for proving the equality t' = t using congruence. The goals are created like congr! would. Any remaining congruence goals come before the main goal. Like refine e, any holes (?_ or ?x) in t that are not solved by unification are converted into new goals, using the hole's name, if any, as the goal case name. Like congr!, convert_to introduces variables while applying congruence rules. These can be pattern-matched, like rintro would, using the with keyword.

convert e, where e is a term of type t, uses e to close the new main goal. In other words, convert e works like convert_to t; refine e. Both tactics use the same options.

• convert_to ty at h changes the type of the local hypothesis h to ty. If later local hypotheses or the goal depend on h, then convert_to t at h may leave a copy of h.
• convert_to ← t creates equality goals in the opposite direction (with the original goal type on the right).
• convert_to t using n, where n is a positive numeral, controls the depth with which congruence is applied. For example, if the main goal is ⊢ Prime (n + n + 1), then convert_to Prime (2 * n + 1) using 2 results in one goal, ⊢ n + n = 2 * n, and convert_to Prime (2 * n + 1) using 3 (or more) results in two (impossible) goals ⊢ HAdd.hAdd = HMul.hMul and ⊢ n = 2. The default value for n is 1.
• convert_to t with x ⟨y₁, y₂⟩ (z₁ | z₂) names or pattern-matches the variables introduced by congruence rules, like rintro x ⟨y₁, y₂⟩ (z₁ | z₂) would.
• convert_to (config := cfg) t uses the configuration options in cfg to control the congruence rules (see Congr!.Config).

def Mathlib.Tactic.acChange : Lean.ParserDescr

ac_change t on a goal ⊢ t' changes the goal to ⊢ t and adds new goals for proving the equality t' = t using congruence, then tries proving these goals by associativity and commutativity. The goals are created like congr! would. In other words, ac_change t is like convert_to t followed by ac_refl.

Like refine e, any holes (?_ or ?x) in t that are not solved by unification are converted into new goals, using the hole's name, if any, as the goal case name. Like congr!, convert_to introduces variables while applying congruence rules. These can be pattern-matched, like rintro would, using the with keyword.

• ac_change t using n, where n is a positive numeral, controls the depth with which congruence is applied. For example, if the main goal is ⊢ Prime ((a * b + 1) + c), then ac_change Prime ((1 + a * b) + c) using 2 solves the side goals, and ac_change Prime ((1 + a * b) + c) using 3 (or more) results in two (impossible) goals ⊢ 1 = a * b and ⊢ a * b = 1. The default value for n is 1.

Example:

example (a b c d e f g N : ℕ) : (a + b) + (c + d) + (e + f) + g ≤ N := by
  ac_change a + d + e + f + c + g + b ≤ _
  -- ⊢ a + d + e + f + c + g + b ≤ N