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:

• It turns ↔ to equalities, before trying another congr lemma
• You can write congr' n to give the maximal depth of recursive applications. This is useful if congr breaks 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 congr' and ext.
• convert: like 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.
• ac_change: like convert_to, but uses ac_refl to discharge the goals.

Apply the constant iff_of_eq to the goal.

meta def tactic.congr_core'  :

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 ↔.

meta def tactic.convert_to_core (r : pexpr) :

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.by_proof_irrel  :

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