mathlib3 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:

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

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

source
meta def tactic.congr'  :
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 (optional (interactive.with_desc ↑"n" lean.parser.small_nat))) :
interactive.parse (optional (lean.parser.tk "with" *> prod.mk <$> lean.parser.many tactic.rintro_patt_parse_hi <*> optional (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  :
interactive.parse (list.join <$> lean.parser.many tactic.rintro_patt_parse_hi) → tactic unit

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
source
def tactic_doc.tactic.congr'  :
tactic_doc_entry

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.convert (sym : interactive.parse (interactive.with_desc ↑"←" (optional (lean.parser.tk "<-")))) (r : interactive.parse interactive.types.texpr) (n : interactive.parse (optional (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.

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.

source
def tactic_doc.tactic.convert  :
tactic_doc_entry

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.

source
meta def tactic.interactive.convert_to (r : interactive.parse interactive.types.texpr) (n : interactive.parse (optional (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.

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.

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

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

In the case in which the expression to be changed is a sum of terms, tactic tactive.interactive.move_add can also be useful.

source
def tactic_doc.tactic.convert_to  :
tactic_doc_entry

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.