Documentation

Mathlib.Tactic.Convert

The convert tactic. #

def Lean.MVarId.convert (e : Lean.Expr) (sym : Bool) (depth : optParam (Option Nat) none) (config : optParam Congr!.Config { transparency := Lean.Meta.TransparencyMode.reducible, preTransparency := Lean.Meta.TransparencyMode.reducible, preferLHS := true, partialApp := true, sameFun := false, maxArgs := none, typeEqs := false, etaExpand := false, useCongrSimp := false }) (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.

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

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.

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.

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.

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