The convert tactic. #

def Lean.MVarId.convert (e : Lean.Expr) (sym : Bool) (depth : optParam (Option Nat) 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 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