The convert tactic.

def Lean.MVarId.convert (e : Lean.Expr) (symm : Bool) (depth : Option ℕ := none) (config : Congr!.Config := { closePre := true, closePost := true, transparency := Lean.Meta.TransparencyMode.reducible, preTransparency := Lean.Meta.TransparencyMode.reducible, preferLHS := true, partialApp := true, sameFun := false, maxArgs := none, typeEqs := false, etaExpand := false, useCongrSimp := false, beqEq := true }) (patterns : List (Lean.TSyntax `rcasesPat) := []) (g : Lean.MVarId) : Lean.MetaM (List Lean.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.

Equations

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

def Lean.MVarId.convertLocalDecl (g : Lean.MVarId) (fvarId : Lean.FVarId) (typeNew : Lean.Expr) (symm : Bool) (depth : Option ℕ := none) (config : Congr!.Config := { closePre := true, closePost := true, transparency := Lean.Meta.TransparencyMode.reducible, preTransparency := Lean.Meta.TransparencyMode.reducible, preferLHS := true, partialApp := true, sameFun := false, maxArgs := none, typeEqs := false, etaExpand := false, useCongrSimp := false, beqEq := true }) (patterns : List (Lean.TSyntax `rcasesPat) := []) : Lean.MetaM (Lean.MVarId × List Lean.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.

Equations

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

def Mathlib.Tactic.convert : Lean.ParserDescr

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.

Equations

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

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.

Equations

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

def Mathlib.Tactic.convertTo : Lean.ParserDescr

The convert_to tactic is for changing the type of the target or a local hypothesis, but unlike the change tactic it will generate equality proof obligations using congr! to resolve discrepancies.

• convert_to ty changes the target to ty
• convert_to ty using n uses congr! n instead of congr! 1
• convert_to ty at h changes the type of the local hypothesis h to ty. Any remaining congr! goals come first.

Operating on the target, the tactic convert_to ty using n is the same as convert (?_ : ty) using n. The difference is that convert_to takes a type but convert takes a proof term.

Except for it also being able to operate on local hypotheses, the syntax for convert_to is the same as for convert, and it has variations such as convert_to ← g and convert_to (config := {transparency := .default}) g.

Note that convert_to ty at h may leave a copy of h if a later local hypotheses or the target depends on it, just like in rw or simp.

Equations

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

def Mathlib.Tactic.acChange : Lean.ParserDescr

ac_change g using n is convert_to g using n followed by ac_rfl. It is useful for rearranging/reassociating e.g. sums:

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

Equations

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