mathlib documentation

tactic.congr

Congruence and related tactics

This file contains the tactic congr', which is an extension of congr, and various tactics using congr' internally.

congr' has some advantages over congr:

Other tactics in this file:

Apply the constant iff_of_eq to the goal.

The main part of the body for the loop in congr'. This will try to replace a goal f x = f y with x = y. Also has support for == and .

The main function in convert_to. Changes the goal to r and a proof obligation that the goal is equal to r.

meta def tactic.congr'  :

Same as the congr tactic, but takes an optional argument which gives the depth of recursive applications.

  • This is useful when congr is too aggressive in breaking down the goal.
  • For example, given ⊢ f (g (x + y)) = f (g (y + x)), congr' produces the goals ⊢ x = y and ⊢ y = x, while congr' 2 produces the intended ⊢ x + y = y + x.
  • If, at any point, a subgoal matches a hypothesis then the subgoal will be closed.

Same as the congr tactic, but takes an optional argument which gives the depth of recursive applications.

  • This is useful when congr is too aggressive in breaking down the goal.
  • For example, given ⊢ f (g (x + y)) = f (g (y + x)), congr' produces the goals ⊢ x = y and ⊢ y = x, while congr' 2 produces 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 '' s then congr' with x generates the goal x : α ⊢ f x = g x.
meta def tactic.interactive.rcongr  :
interactive.parse (tactic.rcases_patt_parse tt) * tactic unit

Repeatedly and apply congr' and ext, using the the given patterns as arguments for ext.

There are two ways this tactic stops:

  • congr' fails (makes no progress), after having already applied ext.
  • congr' canceled out the last usage of ext. In this case, the state is reverted to before the congr' was applied.

For example, when the goal is

 (λ x, f x + 3) '' s = (λ x, g x + 3) '' s

then rcongr x produces the goal

x : α  f x = g x

This gives the same result as congr', ext x, congr'.

In contrast, congr' would produce

 (λ x, f x + 3) = (λ x, g x + 3)

and congr' with x (or congr', ext x) would produce

x : α  f x + 3 = g x + 3

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

n : ,
e : prime (2 * n + 1)
 prime (n + n + 1)

the tactic convert e will change the goal to

 n + n = 2 * n

In this example, the new goal can be solved using ring.

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.

ac_change is convert_to followed by ac_refl. 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 :=
begin
  ac_change a + d + e + f + c + g + b  _,
-- ⊢ a + d + e + f + c + g + b ≤ N
end

ac_change g using n is convert_to g using n; try {ac_refl}.