Documentation for the `congr` attribute

Stream: new members

[Joachim Breitner]

Is there more documentation on what the congr attribute does? <https://leanprover.github.io/reference/other_commands.html> only says

[congr] : a congruence rule for the simplifier

[Kyle Miller]

There's some documentation in the file containing docs#congr_lemma and docs#simp_lemmas.add_congr. It seems the second paper listed at tactic#cc (direct link) also gives some explanation of congruence lemmas.

[Kyle Miller]

I'm not really sure how they work, though, or what's allowed.

import data.list.basic

attribute [congr] list.map_congr

#eval do
  e ← tactic.to_expr ``(list.map (λ n, n - 5) (list.range 5)),
  cl ← tactic.mk_specialized_congr_lemma e,
  tactic.trace cl.type

-- with or without congr attribute:
-- ∀ (f f_1 : ℕ → ℕ), f = f_1 → ∀ (ᾰ ᾰ_1 : list ℕ), ᾰ = ᾰ_1 → list.map f ᾰ = list.map f_1 ᾰ_1