Congruence and related tactics #
This file contains the tactic
congr', which is an extension of
congr, and various tactics
congr' has some advantages over
- It turns
↔to equalities, before trying another congr lemma
- You can write
congr' nto give the maximal depth of recursive applications. This is useful if
congrbreaks down the goal to aggressively, and the resulting goals are false.
- You can write
congr' with ...to do
congr', ext ...in a single tactic.
Other tactics in this file:
rcongr: repeatedly apply
exact, but produces an equality goal if the type doesn't match.
convert_to: changes the goal, if you prove an equality between the old goal and the new goal.
convert_to, but uses
ac_reflto discharge the goals.
Same as the
congr tactic, but takes an optional argument which gives
the depth of recursive applications.
- This is useful when
congris too aggressive in breaking down the goal.
- For example, given
⊢ f (g (x + y)) = f (g (y + x)),
congr'produces the goals
⊢ x = yand
⊢ y = x, while
congr' 2produces the intended
⊢ x + y = y + x.
- If, at any point, a subgoal matches a hypothesis then the subgoal will be closed.
- You can use
congr' with p (: n)?to call
ext p (: n)?to all subgoals generated by
congr'. For example, if the goal is
⊢ f '' s = g '' sthen
congr' with xgenerates the goal
x : α ⊢ f x = g x.
exact e and
refine e tactics require a term
e whose type is
definitionally equal to the goal.
convert e is similar to
but the type of
e is not required to exactly match the
goal. Instead, new goals are created for differences between the type
e and the goal. For example, in the proof state
convert e will change the goal to
⊢ n + n = 2 * n
In this example, the new goal can be solved using
convert tactic applies congruence lemmas eagerly before reducing,
therefore it can fail in cases where
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`
x y : t, and an instance
subsingleton t is in scope, then any goals of the form
x = y are solved automatically.
convert ← e will reverse the direction of the new goals
⊢ 2 * n = n + n in this example).
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
it will generate equality proof obligations using
congr' n to resolve discrepancies.
convert_to g defaults to using
convert_to is similar to
convert_to takes a type (the desired subgoal) while
convert takes a proof term.
convert_to g using n is equivalent to
convert (_ : g) using n.