4.4 Congruence and Contextual Rewriting

Equality becomes useful when it propagates through larger expressions. Congruence provides this propagation. It lifts an equality a = b into equalities of the form f a = f b, and more generally into equalities inside structured contexts. In Lean, congruence is the bridge between local equalities and global goals.

The basic combinator is congrArg. Given a function f and a proof h : a = b, it produces f a = f b.

example (f : Nat -> Nat) (a b : Nat) (h : a = b) :
  f a = f b :=
  congrArg f h

For functions with multiple arguments, congruence can be applied one argument at a time, or by using higher-level combinators that lift equality across multiple positions. A simple pattern is to partially apply a function:

example (f : Nat -> Nat -> Nat) (a b c : Nat)
  (h : a = b) :
  f a c = f b c :=
  congrArg (fun x => f x c) h

This isolates the argument that changes and keeps the rest fixed.

Congruence also applies to structured expressions such as pairs, lists, and records. When a structure is built from components, equality of components induces equality of the whole. In practice, this is often handled by rewriting rather than explicit congruence, but the underlying mechanism remains the same.

Rewriting inside a context relies on congruence. When you use rw [h] in a goal, Lean identifies occurrences of the left-hand side of h and replaces them with the right-hand side. If the occurrence is nested inside a function or constructor, congruence justifies the replacement.

example (a b : Nat) (h : a = b) :
  (a + 1) * 2 = (b + 1) * 2 := by
  rw [h]

The rewrite affects only the occurrences of a that match structurally. Lean traverses the expression and applies congruence where needed.

A limitation of direct rewriting is that it does not always enter all contexts. For example, rewriting under binders or inside lambda expressions may require more explicit control. In such cases, you can restructure the goal or use specialized tactics.

example (a b : Nat) (h : a = b) :
  (fun x => x + a) 3 = (fun x => x + b) 3 := by
  rw [h]

Here rewriting works because the occurrence of a is still accessible after application. If the occurrence were hidden inside a binder, additional steps would be required.

For fine-grained control, Lean provides the congr tactic. It breaks a goal of the form f a₁ ... aₙ = f b₁ ... bₙ into subgoals a₁ = b₁, …, aₙ = bₙ.

example (a b : Nat) (h : a = b) :
  (a, a) = (b, b) := by
  congr
  · exact h
  · exact h

This tactic exposes the structure of the goal and delegates equality to components.

Another useful tool is congrArg₂, which lifts equality across binary functions:

#check congrArg₂
-- congrArg₂ : f a₁ b₁ = f a₂ b₂

It requires equalities for both arguments and produces equality of the result.

Congruence interacts closely with simplification. When simp rewrites an expression, it repeatedly applies congruence to descend into subterms. This is why well-formed simp lemmas propagate throughout a goal without explicit guidance.

A practical guideline is to design expressions so that rewriting aligns with structure. If a term is deeply nested or obscured by abstractions, rewriting becomes fragile. Exposing the relevant subterms often simplifies proofs.

In summary, congruence extends equality from local facts to entire expressions. It underlies all contextual rewriting, whether performed explicitly with combinators or implicitly through tactics. Mastery of congruence allows you to control where and how equalities apply, which is essential for scalable proof development.