Lean4
/-- Equates pieces of the left-hand side of a goal to corresponding pieces of the right-hand side by
recursively applying congruence lemmas. For example, with `⊢ f as = g bs` we could get
two goals `⊢ f = g` and `⊢ as = bs`.
Syntax:
```
congr!
congr! n
congr! with x y z
congr! n with x y z
```
Here, `n` is a natural number and `x`, `y`, `z` are `rintro` patterns (like `h`, `rfl`, `⟨x, y⟩`,
`_`, `-`, `(h | h)`, etc.).
The `congr!` tactic is similar to `congr` but is more insistent in trying to equate left-hand sides
to right-hand sides of goals. Here is a list of things it can try:
- If `R` in `⊢ R x y` is a reflexive relation, it will convert the goal to `⊢ x = y` if possible.
The list of reflexive relations is maintained using the `@[refl]` attribute.
As a special case, `⊢ p ↔ q` is converted to `⊢ p = q` during congruence processing and then
returned to `⊢ p ↔ q` form at the end.
- If there is a user congruence lemma associated to the goal (for instance, a `@[congr]`-tagged
lemma applying to `⊢ List.map f xs = List.map g ys`), then it will use that.
- It uses a congruence lemma generator at least as capable as the one used by `congr` and `simp`.
If there is a subexpression that can be rewritten by `simp`, then `congr!` should be able
to generate an equality for it.
- It can do congruences of pi types using lemmas like `implies_congr` and `pi_congr`.
- Before applying congruences, it will run the `intros` tactic automatically.
The introduced variables can be given names using a `with` clause.
This helps when congruence lemmas provide additional assumptions in hypotheses.
- When there is an equality between functions, so long as at least one is obviously a lambda, we
apply `funext` or `Function.hfunext`, which allows for congruence of lambda bodies.
- It can try to close goals using a few strategies, including checking
definitional equality, trying to apply `Subsingleton.elim` or `proof_irrel_heq`, and using the
`assumption` tactic.
The optional parameter is the depth of the 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`.
The `congr!` tactic also takes a configuration option, for example
```lean
congr! (transparency := .default) 2
```
This overrides the default, which is to apply congruence lemmas at reducible transparency.
The `congr!` tactic is aggressive with equating two sides of everything. There is a predefined
configuration that uses a different strategy:
Try
```lean
congr! (config := .unfoldSameFun)
```
This only allows congruences between functions applications of definitionally equal functions,
and it applies congruence lemmas at default transparency (rather than just reducible).
This is somewhat like `congr`.
See `Congr!.Config` for all options.
-/
@[tactic_parser 1000]
public meta def congr! : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Congr!.congr! 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "congr!" false✝) Lean.Parser.Tactic.optConfig)
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `num))))
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " with")
(ParserDescr.unary✝ `many
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `colGt))
(ParserDescr.cat✝ `rintroPat 0))))))
