Introduce the apply_congr conv mode tactic.

apply_congr will apply congruence lemmas inside conv mode. It is particularly useful when the automatically generated congruence lemmas are not of the optimal shape. An example, described in the doc-string is rewriting inside the operand of a Finset.sum.

def Lean.Elab.Tactic.applyCongr (q : Option Lean.Expr) : Lean.Elab.Tactic.TacticM Unit

Apply a congruence lemma inside conv mode.

When called without an argument apply_congr will try applying all lemmas marked with @[congr]. Otherwise apply_congr e will apply the lemma e.

Recall that a goal that appears as ∣ X in conv mode represents a goal of ⊢ X = ?m, i.e. an equation with a metavariable for the right hand side.

To successfully use apply_congr e, e will need to be an equation (possibly after function arguments), which can be unified with a goal of the form X = ?m. The right hand side of e will then determine the metavariable, and conv will subsequently replace X with that right hand side.

As usual, apply_congr can create new goals; any of these which are not equations with a metavariable on the right hand side will be hard to deal with in conv mode. Thus apply_congr automatically calls intros on any new goals, and fails if they are not then equations.

In particular it is useful for rewriting inside the operand of a Finset.sum, as it provides an extra hypothesis asserting we are inside the domain.

For example:

example (f g : ℤ → ℤ) (S : Finset ℤ) (h : ∀ m ∈ S, f m = g m) :
    Finset.sum S f = Finset.sum S g := by
  conv_lhs =>
    -- If we just call `congr` here, in the second goal we're helpless,
    -- because we are only given the opportunity to rewrite `f`.
    -- However `apply_congr` uses the appropriate `@[congr]` lemma,
    -- so we get to rewrite `f x`, in the presence of the crucial `H : x ∈ S` hypothesis.
    apply_congr
    · skip
    · simp [*]

In the above example, when the apply_congr tactic is called it gives the hypothesis H : x ∈ S which is then used to rewrite the f x to g x.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.applyCongr : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.