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.