# Documentation

Mathlib.Tactic.Convert

# The convert tactic. #

def Lean.MVarId.convert (e : Lean.Expr) (sym : Bool) (depth : optParam () none) (config : optParam 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 }) (patterns : optParam (List (Lean.TSyntax rcasesPat)) []) (g : 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 sym = 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.

Instances For

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.

Instances For

convert_to g using n attempts to change the current goal to g, but unlike change, it will generate equality proof obligations using congr! n to resolve discrepancies. convert_to g defaults to using congr! 1. convert_to is similar to convert, but convert_to takes a type (the desired subgoal) while convert takes a proof term. That is, convert_to g using n is equivalent to convert (?_ : g) using n.

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.

Instances For

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