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.

source

meta def tactic.apply_iff_congr_core :

tactic unit

Apply the constant iff_of_eq to the goal.

source

meta def tactic.congr_core' :

tactic unit

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

source

meta def tactic.convert_to_core (r : pexpr) :

tactic unit

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

source

meta def tactic.congr' (a : option ℕ) :

tactic unit

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.

source

meta def tactic.interactive.congr' (n : interactive.parse (interactive.with_desc ↑"n" lean.parser.small_nat)?) (a : interactive.parse (lean.parser.tk "with" *> prod.mk <$> (tactic.rcases_patt_parse tt) * <*> (lean.parser.tk ":" *> lean.parser.small_nat)?)?) :

tactic unit

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.

source

meta def tactic.interactive.rcongr (a : 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

source

meta def tactic.interactive.convert (sym : interactive.parse (interactive.with_desc ↑"←" (lean.parser.tk "<-")?)) (r : interactive.parse interactive.types.texpr) (n : interactive.parse (lean.parser.tk "using" *> lean.parser.small_nat)?) :

tactic unit

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.

source

meta def tactic.interactive.convert_to (r : interactive.parse interactive.types.texpr) (n : interactive.parse (lean.parser.tk "using" *> lean.parser.small_nat)?) :

tactic unit

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

source

meta def tactic.interactive.ac_change (r : interactive.parse interactive.types.texpr) (n : interactive.parse (lean.parser.tk "using" *> lean.parser.small_nat)?) :

tactic unit

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