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.

Attempts to prove the goal by proof irrelevance, but avoids unifying universe metavariables to do so.

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.

Repeatedly and apply congr' and ext, using 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.

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`

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.

ac_change g using n is convert_to g using n 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