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. For example, in the proof state
In this example, the new goal can be solved using ring.
The convert tactic applies congruence lemmas eagerly before reducing,
therefore it can fail in cases where exact succeeds:
defp(n:ℕ):=trueexample(h:p0):p1:=byexacth-- succeedsexample(h:p0):p1:=byconverth-- fails, with leftover goal `1 = 0`
If x y : t, and an instance subsingleton t is in scope, then any goals of the form
x = y are solved automatically.
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.
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.